Regenerate the files and fix the proofs

21 files changed, 1159 insertions, 1088 deletions

diff --git a/tests/coq/misc/External__Funs.v b/tests/coq/misc/External__Funs.v
index cd03ae3d..cc9e9461 100644
--- a/tests/coq/misc/External__Funs.v
+++ b/tests/coq/misc/External__Funs.v
@@ -107,7 +107,7 @@ Definition test_swap_non_zero_fwd
   p0 <- swap_back u32 x (0 %u32) st st0;
   let (st1, p1) := p0 in
   let (x0, _) := p1 in
-  if x0 s= 0 %u32 then Fail_ else Return (st1, x0)
+  if x0 s= 0 %u32 then Fail_ Failure else Return (st1, x0)
   .
 
 End External__Funs .
diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v
index 774b8a1e..6d7f7987 100644
--- a/tests/coq/misc/NoNestedBorrows.v
+++ b/tests/coq/misc/NoNestedBorrows.v
@@ -95,7 +95,7 @@ Definition test3_fwd : result unit :=
   x <- get_max_fwd (4 %u32) (3 %u32);
   y <- get_max_fwd (10 %u32) (11 %u32);
   z <- u32_add x y;
-  if negb (z s= 15 %u32) then Fail_ else Return tt
+  if negb (z s= 15 %u32) then Fail_ Failure else Return tt
   .
 
 (** Unit test for [no_nested_borrows::test3] *)
@@ -103,14 +103,16 @@ Check (test3_fwd )%return.
 
 (** [no_nested_borrows::test_neg1] *)
 Definition test_neg1_fwd : result unit :=
-  y <- i32_neg (3 %i32); if negb (y s= (-3) %i32) then Fail_ else Return tt .
+  y <- i32_neg (3 %i32);
+  if negb (y s= (-3) %i32) then Fail_ Failure else Return tt
+  .
 
 (** Unit test for [no_nested_borrows::test_neg1] *)
 Check (test_neg1_fwd )%return.
 
 (** [no_nested_borrows::refs_test1] *)
 Definition refs_test1_fwd : result unit :=
-  if negb (1 %i32 s= 1 %i32) then Fail_ else Return tt .
+  if negb (1 %i32 s= 1 %i32) then Fail_ Failure else Return tt .
 
 (** Unit test for [no_nested_borrows::refs_test1] *)
 Check (refs_test1_fwd )%return.
@@ -118,14 +120,14 @@ Check (refs_test1_fwd )%return.
 (** [no_nested_borrows::refs_test2] *)
 Definition refs_test2_fwd : result unit :=
   if negb (2 %i32 s= 2 %i32)
-  then Fail_
+  then Fail_ Failure
   else
     if negb (0 %i32 s= 0 %i32)
-    then Fail_
+    then Fail_ Failure
     else
       if negb (2 %i32 s= 2 %i32)
-      then Fail_
-      else if negb (2 %i32 s= 2 %i32) then Fail_ else Return tt
+      then Fail_ Failure
+      else if negb (2 %i32 s= 2 %i32) then Fail_ Failure else Return tt
   .
 
 (** Unit test for [no_nested_borrows::refs_test2] *)
@@ -141,7 +143,7 @@ Check (test_list1_fwd )%return.
 Definition test_box1_fwd : result unit :=
   let b := 1 %i32 in
   let x := b in
-  if negb (x s= 1 %i32) then Fail_ else Return tt
+  if negb (x s= 1 %i32) then Fail_ Failure else Return tt
   .
 
 (** Unit test for [no_nested_borrows::test_box1] *)
@@ -152,15 +154,17 @@ Definition copy_int_fwd (x : i32) : result i32 := Return x .
 
 (** [no_nested_borrows::test_unreachable] *)
 Definition test_unreachable_fwd (b : bool) : result unit :=
-  if b then Fail_ else Return tt .
+  if b then Fail_ Failure else Return tt .
 
 (** [no_nested_borrows::test_panic] *)
 Definition test_panic_fwd (b : bool) : result unit :=
-  if b then Fail_ else Return tt .
+  if b then Fail_ Failure else Return tt .
 
 (** [no_nested_borrows::test_copy_int] *)
 Definition test_copy_int_fwd : result unit :=
-  y <- copy_int_fwd (0 %i32); if negb (0 %i32 s= y) then Fail_ else Return tt .
+  y <- copy_int_fwd (0 %i32);
+  if negb (0 %i32 s= y) then Fail_ Failure else Return tt
+  .
 
 (** Unit test for [no_nested_borrows::test_copy_int] *)
 Check (test_copy_int_fwd )%return.
@@ -173,7 +177,7 @@ Definition is_cons_fwd (T : Type) (l : List_t T) : result bool :=
 Definition test_is_cons_fwd : result unit :=
   let l := ListNil in
   b <- is_cons_fwd i32 (ListCons (0 %i32) l);
-  if negb b then Fail_ else Return tt
+  if negb b then Fail_ Failure else Return tt
   .
 
 (** Unit test for [no_nested_borrows::test_is_cons] *)
@@ -182,14 +186,18 @@ Check (test_is_cons_fwd )%return.
 (** [no_nested_borrows::split_list] *)
 Definition split_list_fwd
   (T : Type) (l : List_t T) : result (T * (List_t T)) :=
-  match l with | ListCons hd tl => Return (hd, tl) | ListNil => Fail_ end .
+  match l with
+  | ListCons hd tl => Return (hd, tl)
+  | ListNil => Fail_ Failure
+  end
+  .
 
 (** [no_nested_borrows::test_split_list] *)
 Definition test_split_list_fwd : result unit :=
   let l := ListNil in
   p <- split_list_fwd i32 (ListCons (0 %i32) l);
   let (hd, _) := p in
-  if negb (hd s= 0 %i32) then Fail_ else Return tt
+  if negb (hd s= 0 %i32) then Fail_ Failure else Return tt
   .
 
 (** Unit test for [no_nested_borrows::test_split_list] *)
@@ -209,13 +217,13 @@ Definition choose_test_fwd : result unit :=
   z <- choose_fwd i32 true (0 %i32) (0 %i32);
   z0 <- i32_add z 1 %i32;
   if negb (z0 s= 1 %i32)
-  then Fail_
+  then Fail_ Failure
   else (
     p <- choose_back i32 true (0 %i32) (0 %i32) z0;
     let (x, y) := p in
     if negb (x s= 1 %i32)
-    then Fail_
-    else if negb (y s= 0 %i32) then Fail_ else Return tt)
+    then Fail_ Failure
+    else if negb (y s= 0 %i32) then Fail_ Failure else Return tt)
   .
 
 (** Unit test for [no_nested_borrows::choose_test] *)
@@ -258,7 +266,7 @@ Fixpoint list_nth_shared_fwd (T : Type) (l : List_t T) (i : u32) : result T :=
     if i s= 0 %u32
     then Return x
     else (i0 <- u32_sub i 1 %u32; t <- list_nth_shared_fwd T tl i0; Return t)
-  | ListNil => Fail_
+  | ListNil => Fail_ Failure
   end
   .
 
@@ -269,7 +277,7 @@ Fixpoint list_nth_mut_fwd (T : Type) (l : List_t T) (i : u32) : result T :=
     if i s= 0 %u32
     then Return x
     else (i0 <- u32_sub i 1 %u32; t <- list_nth_mut_fwd T tl i0; Return t)
-  | ListNil => Fail_
+  | ListNil => Fail_ Failure
   end
   .
 
@@ -284,7 +292,7 @@ Fixpoint list_nth_mut_back
       i0 <- u32_sub i 1 %u32;
       tl0 <- list_nth_mut_back T tl i0 ret;
       Return (ListCons x tl0))
-  | ListNil => Fail_
+  | ListNil => Fail_ Failure
   end
   .
 
@@ -311,31 +319,31 @@ Definition test_list_functions_fwd : result unit :=
   let l1 := ListCons (1 %i32) l0 in
   i <- list_length_fwd i32 (ListCons (0 %i32) l1);
   if negb (i s= 3 %u32)
-  then Fail_
+  then Fail_ Failure
   else (
     i0 <- list_nth_shared_fwd i32 (ListCons (0 %i32) l1) (0 %u32);
     if negb (i0 s= 0 %i32)
-    then Fail_
+    then Fail_ Failure
     else (
       i1 <- list_nth_shared_fwd i32 (ListCons (0 %i32) l1) (1 %u32);
       if negb (i1 s= 1 %i32)
-      then Fail_
+      then Fail_ Failure
       else (
         i2 <- list_nth_shared_fwd i32 (ListCons (0 %i32) l1) (2 %u32);
         if negb (i2 s= 2 %i32)
-        then Fail_
+        then Fail_ Failure
         else (
           ls <- list_nth_mut_back i32 (ListCons (0 %i32) l1) (1 %u32) (3 %i32);
           i3 <- list_nth_shared_fwd i32 ls (0 %u32);
           if negb (i3 s= 0 %i32)
-          then Fail_
+          then Fail_ Failure
           else (
             i4 <- list_nth_shared_fwd i32 ls (1 %u32);
             if negb (i4 s= 3 %i32)
-            then Fail_
+            then Fail_ Failure
             else (
               i5 <- list_nth_shared_fwd i32 ls (2 %u32);
-              if negb (i5 s= 2 %i32) then Fail_ else Return tt))))))
+              if negb (i5 s= 2 %i32) then Fail_ Failure else Return tt))))))
   .
 
 (** Unit test for [no_nested_borrows::test_list_functions] *)
@@ -436,28 +444,28 @@ Definition test_constants_fwd : result unit :=
   | mkStruct_with_tuple_t p =>
     let (i, _) := p in
     if negb (i s= 1 %u32)
-    then Fail_
+    then Fail_ Failure
     else (
       swt0 <- new_tuple2_fwd;
       match swt0 with
       | mkStruct_with_tuple_t p0 =>
         let (i0, _) := p0 in
         if negb (i0 s= 1 %i16)
-        then Fail_
+        then Fail_ Failure
         else (
           swt1 <- new_tuple3_fwd;
           match swt1 with
           | mkStruct_with_tuple_t p1 =>
             let (i1, _) := p1 in
             if negb (i1 s= 1 %u64)
-            then Fail_
+            then Fail_ Failure
             else (
               swp <- new_pair1_fwd;
               match swp with
               | mkStruct_with_pair_t p2 =>
                 match p2 with
                 | mkPair_t i2 i3 =>
-                  if negb (i2 s= 1 %u32) then Fail_ else Return tt
+                  if negb (i2 s= 1 %u32) then Fail_ Failure else Return tt
                 end
               end)
           end)
@@ -477,7 +485,7 @@ Check (test_weird_borrows1_fwd )%return.
 (** [no_nested_borrows::test_mem_replace] *)
 Definition test_mem_replace_fwd_back (px : u32) : result u32 :=
   let y := mem_replace_fwd u32 px (1 %u32) in
-  if negb (y s= 0 %u32) then Fail_ else Return (2 %u32)
+  if negb (y s= 0 %u32) then Fail_ Failure else Return (2 %u32)
   .
 
 (** [no_nested_borrows::test_shared_borrow_bool1] *)
diff --git a/tests/coq/misc/Paper.v b/tests/coq/misc/Paper.v
index 25c01d7b..d0c99883 100644
--- a/tests/coq/misc/Paper.v
+++ b/tests/coq/misc/Paper.v
@@ -13,7 +13,7 @@ Definition ref_incr_fwd_back (x : i32) : result i32 :=
 (** [paper::test_incr] *)
 Definition test_incr_fwd : result unit :=
   x <- ref_incr_fwd_back (0 %i32);
-  if negb (x s= 1 %i32) then Fail_ else Return tt
+  if negb (x s= 1 %i32) then Fail_ Failure else Return tt
   .
 
 (** Unit test for [paper::test_incr] *)
@@ -33,13 +33,13 @@ Definition test_choose_fwd : result unit :=
   z <- choose_fwd i32 true (0 %i32) (0 %i32);
   z0 <- i32_add z 1 %i32;
   if negb (z0 s= 1 %i32)
-  then Fail_
+  then Fail_ Failure
   else (
     p <- choose_back i32 true (0 %i32) (0 %i32) z0;
     let (x, y) := p in
     if negb (x s= 1 %i32)
-    then Fail_
-    else if negb (y s= 0 %i32) then Fail_ else Return tt)
+    then Fail_ Failure
+    else if negb (y s= 0 %i32) then Fail_ Failure else Return tt)
   .
 
 (** Unit test for [paper::test_choose] *)
@@ -61,7 +61,7 @@ Fixpoint list_nth_mut_fwd (T : Type) (l : List_t T) (i : u32) : result T :=
     if i s= 0 %u32
     then Return x
     else (i0 <- u32_sub i 1 %u32; t <- list_nth_mut_fwd T tl i0; Return t)
-  | ListNil => Fail_
+  | ListNil => Fail_ Failure
   end
   .
 
@@ -76,7 +76,7 @@ Fixpoint list_nth_mut_back
       i0 <- u32_sub i 1 %u32;
       tl0 <- list_nth_mut_back T tl i0 ret;
       Return (ListCons x tl0))
-  | ListNil => Fail_
+  | ListNil => Fail_ Failure
   end
   .
 
@@ -97,7 +97,7 @@ Definition test_nth_fwd : result unit :=
   x0 <- i32_add x 1 %i32;
   l2 <- list_nth_mut_back i32 (ListCons (1 %i32) l1) (2 %u32) x0;
   i <- sum_fwd l2;
-  if negb (i s= 7 %i32) then Fail_ else Return tt
+  if negb (i s= 7 %i32) then Fail_ Failure else Return tt
   .
 
 (** Unit test for [paper::test_nth] *)
diff --git a/tests/coq/misc/Primitives.v b/tests/coq/misc/Primitives.v
index c27b8aed..9a97d6c7 100644
--- a/tests/coq/misc/Primitives.v
+++ b/tests/coq/misc/Primitives.v
@@ -13,40 +13,44 @@ Module Primitives.
 Declare Scope Primitives_scope.
 
 (*** Result *)
-  
+
+Inductive error :=
+  | Failure
+  | OutOfFuel.
+
 Inductive result A :=
   | Return : A -> result A
-  | Fail_ : result A.
+  | Fail_ : error -> result A.
 
 Arguments Return {_} a.
 Arguments Fail_ {_}.
 
 Definition bind {A B} (m: result A) (f: A -> result B) : result B :=
   match m with
-  | Fail_ => Fail_
+  | Fail_ e => Fail_ e
   | Return x => f x
   end.
 
-Definition return_ {A: Type} (x: A) : result A := Return x .
-Definition fail_ {A: Type} : result A := Fail_ .
+Definition return_ {A: Type} (x: A) : result A := Return x.
+Definition fail_ {A: Type} (e: error) : result A := Fail_ e.
 
 Notation "x <- c1 ; c2" := (bind c1 (fun x => c2))
   (at level 61, c1 at next level, right associativity).
 
 (** Monadic assert *)
 Definition massert (b: bool) : result unit :=
-  if b then Return tt else Fail_.
+  if b then Return tt else Fail_ Failure.
 
 (** Normalize and unwrap a successful result (used for globals) *)
 Definition eval_result_refl {A} {x} (a: result A) (p: a = Return x) : A :=
   match a as r return (r = Return x -> A) with
   | Return a' => fun _  => a'
-  | Fail_     => fun p' =>
-      False_rect _ (eq_ind Fail_
+  | Fail_ e   => fun p' =>
+      False_rect _ (eq_ind (Fail_ e)
           (fun e : result A =>
           match e with
           | Return _ => False
-          | Fail_ => True
+          | Fail_ e => True
           end)
         I (Return x) p')
   end p.
@@ -55,7 +59,7 @@ Notation "x %global" := (eval_result_refl x eq_refl) (at level 40).
 Notation "x %return" := (eval_result_refl x eq_refl) (at level 40).
 
 (* Sanity check *)
-Check (if true then Return (1 + 2) else Fail_)%global = 3.
+Check (if true then Return (1 + 2) else Fail_ Failure)%global = 3.
 
 (*** Misc *)
 
@@ -232,7 +236,7 @@ Import Sumbool.
 Definition mk_scalar (ty: scalar_ty) (x: Z) : result (scalar ty) :=
   match sumbool_of_bool (scalar_in_bounds ty x) with
   | left H => Return (exist _ x (scalar_in_bounds_valid _ _ H))
-  | right _ => Fail_
+  | right _ => Fail_ Failure
   end.
 
 Definition scalar_add {ty} (x y: scalar ty) : result (scalar ty) := mk_scalar ty (to_Z x + to_Z y).
@@ -242,7 +246,7 @@ Definition scalar_sub {ty} (x y: scalar ty) : result (scalar ty) := mk_scalar ty
 Definition scalar_mul {ty} (x y: scalar ty) : result (scalar ty) := mk_scalar ty (to_Z x * to_Z y).
 
 Definition scalar_div {ty} (x y: scalar ty) : result (scalar ty) :=
-  if to_Z y =? 0 then Fail_ else
+  if to_Z y =? 0 then Fail_ Failure else
   mk_scalar ty (to_Z x / to_Z y).
 
 Definition scalar_rem {ty} (x y: scalar ty) : result (scalar ty) := mk_scalar ty (Z.rem (to_Z x) (to_Z y)).
@@ -433,7 +437,7 @@ Definition vec_bind {A B} (v: vec A) (f: list A -> result (list B)) : result (ve
   l <- f (vec_to_list v) ;
   match sumbool_of_bool (scalar_le_max Usize (Z.of_nat (length l))) with
   | left H => Return (exist _ l (scalar_le_max_valid _ _ H))
-  | right _ => Fail_
+  | right _ => Fail_ Failure
   end.
 
 (* The **forward** function shouldn't be used *)
@@ -444,35 +448,35 @@ Definition vec_push_back (T: Type) (v: vec T) (x: T) : result (vec T) :=
 
 (* The **forward** function shouldn't be used *)
 Definition vec_insert_fwd (T: Type) (v: vec T) (i: usize) (x: T) : result unit :=
-  if to_Z i <? vec_length v then Return tt else Fail_.
+  if to_Z i <? vec_length v then Return tt else Fail_ Failure.
 
 Definition vec_insert_back (T: Type) (v: vec T) (i: usize) (x: T) : result (vec T) :=
   vec_bind v (fun l =>
     if to_Z i <? Z.of_nat (length l)
     then Return (list_update l (usize_to_nat i) x)
-    else Fail_).
+    else Fail_ Failure).
 
 (* The **backward** function shouldn't be used *)
 Definition vec_index_fwd (T: Type) (v: vec T) (i: usize) : result T :=
   match nth_error (vec_to_list v) (usize_to_nat i) with
   | Some n => Return n
-  | None   => Fail_
+  | None   => Fail_ Failure
   end.
 
 Definition vec_index_back (T: Type) (v: vec T) (i: usize) (x: T) : result unit :=
-  if to_Z i <? vec_length v then Return tt else Fail_.
+  if to_Z i <? vec_length v then Return tt else Fail_ Failure.
 
 (* The **backward** function shouldn't be used *)
 Definition vec_index_mut_fwd (T: Type) (v: vec T) (i: usize) : result T :=
   match nth_error (vec_to_list v) (usize_to_nat i) with
   | Some n => Return n
-  | None   => Fail_
+  | None   => Fail_ Failure
   end.
 
 Definition vec_index_mut_back (T: Type) (v: vec T) (i: usize) (x: T) : result (vec T) :=
   vec_bind v (fun l =>
     if to_Z i <? Z.of_nat (length l)
     then Return (list_update l (usize_to_nat i) x)
-    else Fail_).
+    else Fail_ Failure).
 
 End Primitives.
diff --git a/tests/fstar/betree/BetreeMain.Funs.fst b/tests/fstar/betree/BetreeMain.Funs.fst
index 8cb5eb41..f6045dfd 100644
--- a/tests/fstar/betree/BetreeMain.Funs.fst
+++ b/tests/fstar/betree/BetreeMain.Funs.fst
@@ -14,7 +14,7 @@ let betree_load_internal_node_fwd
   result (state & (betree_list_t (u64 & betree_message_t)))
   =
   begin match betree_utils_load_internal_node_fwd id st with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return (st0, l) -> Return (st0, l)
   end
 
@@ -24,7 +24,7 @@ let betree_store_internal_node_fwd
   result (state & unit)
   =
   begin match betree_utils_store_internal_node_fwd id content st with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return (st0, _) -> Return (st0, ())
   end
 
@@ -32,7 +32,7 @@ let betree_store_internal_node_fwd
 let betree_load_leaf_node_fwd
   (id : u64) (st : state) : result (state & (betree_list_t (u64 & u64))) =
   begin match betree_utils_load_leaf_node_fwd id st with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return (st0, l) -> Return (st0, l)
   end
 
@@ -42,21 +42,21 @@ let betree_store_leaf_node_fwd
   result (state & unit)
   =
   begin match betree_utils_store_leaf_node_fwd id content st with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return (st0, _) -> Return (st0, ())
   end
 
 (** [betree_main::betree::fresh_node_id] *)
 let betree_fresh_node_id_fwd (counter : u64) : result u64 =
   begin match u64_add counter 1 with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return _ -> Return counter
   end
 
 (** [betree_main::betree::fresh_node_id] *)
 let betree_fresh_node_id_back (counter : u64) : result u64 =
   begin match u64_add counter 1 with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return counter0 -> Return counter0
   end
 
@@ -68,7 +68,7 @@ let betree_node_id_counter_new_fwd : result betree_node_id_counter_t =
 let betree_node_id_counter_fresh_id_fwd
   (self : betree_node_id_counter_t) : result u64 =
   begin match u64_add self.betree_node_id_counter_next_node_id 1 with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return _ -> Return self.betree_node_id_counter_next_node_id
   end
 
@@ -76,7 +76,7 @@ let betree_node_id_counter_fresh_id_fwd
 let betree_node_id_counter_fresh_id_back
   (self : betree_node_id_counter_t) : result betree_node_id_counter_t =
   begin match u64_add self.betree_node_id_counter_next_node_id 1 with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return i -> Return (Mkbetree_node_id_counter_t i)
   end
 
@@ -97,12 +97,12 @@ let betree_upsert_update_fwd
     begin match st with
     | BetreeUpsertFunStateAdd v ->
       begin match u64_sub core_num_u64_max_c prev0 with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return margin ->
         if margin >= v
         then
           begin match u64_add prev0 v with
-          | Fail -> Fail
+          | Fail e -> Fail e
           | Return i -> Return i
           end
         else Return core_num_u64_max_c
@@ -111,7 +111,7 @@ let betree_upsert_update_fwd
       if prev0 >= v
       then
         begin match u64_sub prev0 v with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return i -> Return i
         end
       else Return 0
@@ -126,9 +126,12 @@ let rec betree_list_len_fwd
   begin match self with
   | BetreeListCons x tl ->
     begin match betree_list_len_fwd t tl with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return i ->
-      begin match u64_add 1 i with | Fail -> Fail | Return i0 -> Return i0 end
+      begin match u64_add 1 i with
+      | Fail e -> Fail e
+      | Return i0 -> Return i0
+      end
     end
   | BetreeListNil -> Return 0
   end
@@ -145,17 +148,17 @@ let rec betree_list_split_at_fwd
     begin match self with
     | BetreeListCons hd tl ->
       begin match u64_sub n 1 with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return i ->
         begin match betree_list_split_at_fwd t tl i with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return p ->
           let (ls0, ls1) = p in
           let l = ls0 in
           Return (BetreeListCons hd l, ls1)
         end
       end
-    | BetreeListNil -> Fail
+    | BetreeListNil -> Fail Failure
     end
 
 (** [betree_main::betree::List::{1}::push_front] *)
@@ -170,7 +173,7 @@ let betree_list_pop_front_fwd (t : Type0) (self : betree_list_t t) : result t =
   let ls = mem_replace_fwd (betree_list_t t) self BetreeListNil in
   begin match ls with
   | BetreeListCons x tl -> Return x
-  | BetreeListNil -> Fail
+  | BetreeListNil -> Fail Failure
   end
 
 (** [betree_main::betree::List::{1}::pop_front] *)
@@ -179,14 +182,14 @@ let betree_list_pop_front_back
   let ls = mem_replace_fwd (betree_list_t t) self BetreeListNil in
   begin match ls with
   | BetreeListCons x tl -> Return tl
-  | BetreeListNil -> Fail
+  | BetreeListNil -> Fail Failure
   end
 
 (** [betree_main::betree::List::{1}::hd] *)
 let betree_list_hd_fwd (t : Type0) (self : betree_list_t t) : result t =
   begin match self with
   | BetreeListCons hd l -> Return hd
-  | BetreeListNil -> Fail
+  | BetreeListNil -> Fail Failure
   end
 
 (** [betree_main::betree::List::{2}::head_has_key] *)
@@ -210,7 +213,7 @@ let rec betree_list_partition_at_pivot_fwd
     then Return (BetreeListNil, BetreeListCons (i, x) tl)
     else
       begin match betree_list_partition_at_pivot_fwd t tl pivot with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return p ->
         let (ls0, ls1) = p in
         let l = ls0 in
@@ -229,27 +232,27 @@ let betree_leaf_split_fwd
   begin match
     betree_list_split_at_fwd (u64 & u64) content
       params.betree_params_split_size with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return p ->
     let (content0, content1) = p in
     begin match betree_list_hd_fwd (u64 & u64) content1 with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return p0 ->
       let (pivot, _) = p0 in
       begin match betree_node_id_counter_fresh_id_fwd node_id_cnt with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return id0 ->
         begin match betree_node_id_counter_fresh_id_back node_id_cnt with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return node_id_cnt0 ->
           begin match betree_node_id_counter_fresh_id_fwd node_id_cnt0 with
-          | Fail -> Fail
+          | Fail e -> Fail e
           | Return id1 ->
             begin match betree_store_leaf_node_fwd id0 content0 st with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return (st0, _) ->
               begin match betree_store_leaf_node_fwd id1 content1 st0 with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return (st1, _) ->
                 let n = BetreeNodeLeaf (Mkbetree_leaf_t id0
                   params.betree_params_split_size) in
@@ -275,30 +278,30 @@ let betree_leaf_split_back
   begin match
     betree_list_split_at_fwd (u64 & u64) content
       params.betree_params_split_size with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return p ->
     let (content0, content1) = p in
     begin match betree_list_hd_fwd (u64 & u64) content1 with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return _ ->
       begin match betree_node_id_counter_fresh_id_fwd node_id_cnt with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return id0 ->
         begin match betree_node_id_counter_fresh_id_back node_id_cnt with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return node_id_cnt0 ->
           begin match betree_node_id_counter_fresh_id_fwd node_id_cnt0 with
-          | Fail -> Fail
+          | Fail e -> Fail e
           | Return id1 ->
             begin match betree_store_leaf_node_fwd id0 content0 st with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return (st0, _) ->
               begin match betree_store_leaf_node_fwd id1 content1 st0 with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return (_, _) ->
                 begin match betree_node_id_counter_fresh_id_back node_id_cnt0
                   with
-                | Fail -> Fail
+                | Fail e -> Fail e
                 | Return node_id_cnt1 -> Return node_id_cnt1
                 end
               end
@@ -325,7 +328,7 @@ let rec betree_node_lookup_in_bindings_fwd
       then Return None
       else
         begin match betree_node_lookup_in_bindings_fwd key tl with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return opt -> Return opt
         end
   | BetreeListNil -> Return None
@@ -345,7 +348,7 @@ let rec betree_node_lookup_first_message_for_key_fwd
     else
       begin match betree_node_lookup_first_message_for_key_fwd key next_msgs
         with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return l -> Return l
       end
   | BetreeListNil -> Return BetreeListNil
@@ -366,7 +369,7 @@ let rec betree_node_lookup_first_message_for_key_back
     else
       begin match
         betree_node_lookup_first_message_for_key_back key next_msgs ret with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return next_msgs0 -> Return (BetreeListCons (i, m) next_msgs0)
       end
   | BetreeListNil -> Return ret
@@ -380,28 +383,28 @@ let rec betree_node_apply_upserts_fwd
   (decreases (betree_node_apply_upserts_decreases msgs prev key st))
   =
   begin match betree_list_head_has_key_fwd betree_message_t msgs key with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return b ->
     if b
     then
       begin match betree_list_pop_front_fwd (u64 & betree_message_t) msgs with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return msg ->
         let (_, m) = msg in
         begin match m with
-        | BetreeMessageInsert i -> Fail
-        | BetreeMessageDelete -> Fail
+        | BetreeMessageInsert i -> Fail Failure
+        | BetreeMessageDelete -> Fail Failure
         | BetreeMessageUpsert s ->
           begin match betree_upsert_update_fwd prev s with
-          | Fail -> Fail
+          | Fail e -> Fail e
           | Return v ->
             begin match
               betree_list_pop_front_back (u64 & betree_message_t) msgs with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return msgs0 ->
               begin match betree_node_apply_upserts_fwd msgs0 (Some v) key st
                 with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return (st0, i) -> Return (st0, i)
               end
             end
@@ -410,12 +413,12 @@ let rec betree_node_apply_upserts_fwd
       end
     else
       begin match core_option_option_unwrap_fwd u64 prev st with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return (st0, v) ->
         begin match
           betree_list_push_front_fwd_back (u64 & betree_message_t) msgs (key,
             BetreeMessageInsert v) with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return _ -> Return (st0, v)
         end
       end
@@ -429,28 +432,28 @@ let rec betree_node_apply_upserts_back
   (decreases (betree_node_apply_upserts_decreases msgs prev key st))
   =
   begin match betree_list_head_has_key_fwd betree_message_t msgs key with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return b ->
     if b
     then
       begin match betree_list_pop_front_fwd (u64 & betree_message_t) msgs with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return msg ->
         let (_, m) = msg in
         begin match m with
-        | BetreeMessageInsert i -> Fail
-        | BetreeMessageDelete -> Fail
+        | BetreeMessageInsert i -> Fail Failure
+        | BetreeMessageDelete -> Fail Failure
         | BetreeMessageUpsert s ->
           begin match betree_upsert_update_fwd prev s with
-          | Fail -> Fail
+          | Fail e -> Fail e
           | Return v ->
             begin match
               betree_list_pop_front_back (u64 & betree_message_t) msgs with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return msgs0 ->
               begin match betree_node_apply_upserts_back msgs0 (Some v) key st
                 with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return msgs1 -> Return msgs1
               end
             end
@@ -459,12 +462,12 @@ let rec betree_node_apply_upserts_back
       end
     else
       begin match core_option_option_unwrap_fwd u64 prev st with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return (_, v) ->
         begin match
           betree_list_push_front_fwd_back (u64 & betree_message_t) msgs (key,
             BetreeMessageInsert v) with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return msgs0 -> Return msgs0
         end
       end
@@ -479,10 +482,10 @@ let rec betree_node_lookup_fwd
   begin match self with
   | BetreeNodeInternal node ->
     begin match betree_load_internal_node_fwd node.betree_internal_id st with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return (st0, msgs) ->
       begin match betree_node_lookup_first_message_for_key_fwd key msgs with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return pending ->
         begin match pending with
         | BetreeListCons p l ->
@@ -491,12 +494,12 @@ let rec betree_node_lookup_fwd
           then
             begin match betree_internal_lookup_in_children_fwd node key st0
               with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return (st1, opt) ->
               begin match
                 betree_node_lookup_first_message_for_key_back key msgs
                   (BetreeListCons (k, msg) l) with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return _ -> Return (st1, opt)
               end
             end
@@ -506,44 +509,44 @@ let rec betree_node_lookup_fwd
               begin match
                 betree_node_lookup_first_message_for_key_back key msgs
                   (BetreeListCons (k, BetreeMessageInsert v) l) with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return _ -> Return (st0, Some v)
               end
             | BetreeMessageDelete ->
               begin match
                 betree_node_lookup_first_message_for_key_back key msgs
                   (BetreeListCons (k, BetreeMessageDelete) l) with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return _ -> Return (st0, None)
               end
             | BetreeMessageUpsert ufs ->
               begin match betree_internal_lookup_in_children_fwd node key st0
                 with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return (st1, v) ->
                 begin match
                   betree_node_apply_upserts_fwd (BetreeListCons (k,
                     BetreeMessageUpsert ufs) l) v key st1 with
-                | Fail -> Fail
+                | Fail e -> Fail e
                 | Return (st2, v0) ->
                   begin match
                     betree_internal_lookup_in_children_back node key st0 with
-                  | Fail -> Fail
+                  | Fail e -> Fail e
                   | Return node0 ->
                     begin match
                       betree_node_apply_upserts_back (BetreeListCons (k,
                         BetreeMessageUpsert ufs) l) v key st1 with
-                    | Fail -> Fail
+                    | Fail e -> Fail e
                     | Return pending0 ->
                       begin match
                         betree_node_lookup_first_message_for_key_back key msgs
                           pending0 with
-                      | Fail -> Fail
+                      | Fail e -> Fail e
                       | Return msgs0 ->
                         begin match
                           betree_store_internal_node_fwd
                             node0.betree_internal_id msgs0 st2 with
-                        | Fail -> Fail
+                        | Fail e -> Fail e
                         | Return (st3, _) -> Return (st3, Some v0)
                         end
                       end
@@ -554,12 +557,12 @@ let rec betree_node_lookup_fwd
             end
         | BetreeListNil ->
           begin match betree_internal_lookup_in_children_fwd node key st0 with
-          | Fail -> Fail
+          | Fail e -> Fail e
           | Return (st1, opt) ->
             begin match
               betree_node_lookup_first_message_for_key_back key msgs
                 BetreeListNil with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return _ -> Return (st1, opt)
             end
           end
@@ -568,10 +571,10 @@ let rec betree_node_lookup_fwd
     end
   | BetreeNodeLeaf node ->
     begin match betree_load_leaf_node_fwd node.betree_leaf_id st with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return (st0, bindings) ->
       begin match betree_node_lookup_in_bindings_fwd key bindings with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return opt -> Return (st0, opt)
       end
     end
@@ -586,10 +589,10 @@ and betree_node_lookup_back
   begin match self with
   | BetreeNodeInternal node ->
     begin match betree_load_internal_node_fwd node.betree_internal_id st with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return (st0, msgs) ->
       begin match betree_node_lookup_first_message_for_key_fwd key msgs with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return pending ->
         begin match pending with
         | BetreeListCons p l ->
@@ -599,11 +602,11 @@ and betree_node_lookup_back
             begin match
               betree_node_lookup_first_message_for_key_back key msgs
                 (BetreeListCons (k, msg) l) with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return _ ->
               begin match betree_internal_lookup_in_children_back node key st0
                 with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return node0 -> Return (BetreeNodeInternal node0)
               end
             end
@@ -613,44 +616,44 @@ and betree_node_lookup_back
               begin match
                 betree_node_lookup_first_message_for_key_back key msgs
                   (BetreeListCons (k, BetreeMessageInsert v) l) with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return _ -> Return (BetreeNodeInternal node)
               end
             | BetreeMessageDelete ->
               begin match
                 betree_node_lookup_first_message_for_key_back key msgs
                   (BetreeListCons (k, BetreeMessageDelete) l) with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return _ -> Return (BetreeNodeInternal node)
               end
             | BetreeMessageUpsert ufs ->
               begin match betree_internal_lookup_in_children_fwd node key st0
                 with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return (st1, v) ->
                 begin match
                   betree_node_apply_upserts_fwd (BetreeListCons (k,
                     BetreeMessageUpsert ufs) l) v key st1 with
-                | Fail -> Fail
+                | Fail e -> Fail e
                 | Return (st2, _) ->
                   begin match
                     betree_internal_lookup_in_children_back node key st0 with
-                  | Fail -> Fail
+                  | Fail e -> Fail e
                   | Return node0 ->
                     begin match
                       betree_node_apply_upserts_back (BetreeListCons (k,
                         BetreeMessageUpsert ufs) l) v key st1 with
-                    | Fail -> Fail
+                    | Fail e -> Fail e
                     | Return pending0 ->
                       begin match
                         betree_node_lookup_first_message_for_key_back key msgs
                           pending0 with
-                      | Fail -> Fail
+                      | Fail e -> Fail e
                       | Return msgs0 ->
                         begin match
                           betree_store_internal_node_fwd
                             node0.betree_internal_id msgs0 st2 with
-                        | Fail -> Fail
+                        | Fail e -> Fail e
                         | Return (_, _) -> Return (BetreeNodeInternal node0)
                         end
                       end
@@ -663,11 +666,11 @@ and betree_node_lookup_back
           begin match
             betree_node_lookup_first_message_for_key_back key msgs
               BetreeListNil with
-          | Fail -> Fail
+          | Fail e -> Fail e
           | Return _ ->
             begin match betree_internal_lookup_in_children_back node key st0
               with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return node0 -> Return (BetreeNodeInternal node0)
             end
           end
@@ -676,10 +679,10 @@ and betree_node_lookup_back
     end
   | BetreeNodeLeaf node ->
     begin match betree_load_leaf_node_fwd node.betree_leaf_id st with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return (_, bindings) ->
       begin match betree_node_lookup_in_bindings_fwd key bindings with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return _ -> Return (BetreeNodeLeaf node)
       end
     end
@@ -694,12 +697,12 @@ and betree_internal_lookup_in_children_fwd
   if key < self.betree_internal_pivot
   then
     begin match betree_node_lookup_fwd self.betree_internal_left key st with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return (st0, opt) -> Return (st0, opt)
     end
   else
     begin match betree_node_lookup_fwd self.betree_internal_right key st with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return (st0, opt) -> Return (st0, opt)
     end
 
@@ -712,14 +715,14 @@ and betree_internal_lookup_in_children_back
   if key < self.betree_internal_pivot
   then
     begin match betree_node_lookup_back self.betree_internal_left key st with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return n ->
       Return (Mkbetree_internal_t self.betree_internal_id
         self.betree_internal_pivot n self.betree_internal_right)
     end
   else
     begin match betree_node_lookup_back self.betree_internal_right key st with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return n ->
       Return (Mkbetree_internal_t self.betree_internal_id
         self.betree_internal_pivot self.betree_internal_left n)
@@ -738,7 +741,7 @@ let rec betree_node_lookup_mut_in_bindings_fwd
     then Return (BetreeListCons (i, i0) tl)
     else
       begin match betree_node_lookup_mut_in_bindings_fwd key tl with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return l -> Return l
       end
   | BetreeListNil -> Return BetreeListNil
@@ -758,7 +761,7 @@ let rec betree_node_lookup_mut_in_bindings_back
     then Return ret
     else
       begin match betree_node_lookup_mut_in_bindings_back key tl ret with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return tl0 -> Return (BetreeListCons (i, i0) tl0)
       end
   | BetreeListNil -> Return ret
@@ -771,62 +774,62 @@ let betree_node_apply_to_leaf_fwd_back
   result (betree_list_t (u64 & u64))
   =
   begin match betree_node_lookup_mut_in_bindings_fwd key bindings with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return bindings0 ->
     begin match betree_list_head_has_key_fwd u64 bindings0 key with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return b ->
       if b
       then
         begin match betree_list_pop_front_fwd (u64 & u64) bindings0 with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return hd ->
           begin match new_msg with
           | BetreeMessageInsert v ->
             begin match betree_list_pop_front_back (u64 & u64) bindings0 with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return bindings1 ->
               begin match
                 betree_list_push_front_fwd_back (u64 & u64) bindings1 (key, v)
                 with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return bindings2 ->
                 begin match
                   betree_node_lookup_mut_in_bindings_back key bindings
                     bindings2 with
-                | Fail -> Fail
+                | Fail e -> Fail e
                 | Return bindings3 -> Return bindings3
                 end
               end
             end
           | BetreeMessageDelete ->
             begin match betree_list_pop_front_back (u64 & u64) bindings0 with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return bindings1 ->
               begin match
                 betree_node_lookup_mut_in_bindings_back key bindings bindings1
                 with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return bindings2 -> Return bindings2
               end
             end
           | BetreeMessageUpsert s ->
             let (_, i) = hd in
             begin match betree_upsert_update_fwd (Some i) s with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return v ->
               begin match betree_list_pop_front_back (u64 & u64) bindings0 with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return bindings1 ->
                 begin match
                   betree_list_push_front_fwd_back (u64 & u64) bindings1 (key,
                     v) with
-                | Fail -> Fail
+                | Fail e -> Fail e
                 | Return bindings2 ->
                   begin match
                     betree_node_lookup_mut_in_bindings_back key bindings
                       bindings2 with
-                  | Fail -> Fail
+                  | Fail e -> Fail e
                   | Return bindings3 -> Return bindings3
                   end
                 end
@@ -839,34 +842,34 @@ let betree_node_apply_to_leaf_fwd_back
         | BetreeMessageInsert v ->
           begin match
             betree_list_push_front_fwd_back (u64 & u64) bindings0 (key, v) with
-          | Fail -> Fail
+          | Fail e -> Fail e
           | Return bindings1 ->
             begin match
               betree_node_lookup_mut_in_bindings_back key bindings bindings1
               with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return bindings2 -> Return bindings2
             end
           end
         | BetreeMessageDelete ->
           begin match
             betree_node_lookup_mut_in_bindings_back key bindings bindings0 with
-          | Fail -> Fail
+          | Fail e -> Fail e
           | Return bindings1 -> Return bindings1
           end
         | BetreeMessageUpsert s ->
           begin match betree_upsert_update_fwd None s with
-          | Fail -> Fail
+          | Fail e -> Fail e
           | Return v ->
             begin match
               betree_list_push_front_fwd_back (u64 & u64) bindings0 (key, v)
               with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return bindings1 ->
               begin match
                 betree_node_lookup_mut_in_bindings_back key bindings bindings1
                 with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return bindings2 -> Return bindings2
               end
             end
@@ -886,11 +889,11 @@ let rec betree_node_apply_messages_to_leaf_fwd_back
   | BetreeListCons new_msg new_msgs_tl ->
     let (i, m) = new_msg in
     begin match betree_node_apply_to_leaf_fwd_back bindings i m with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return bindings0 ->
       begin match
         betree_node_apply_messages_to_leaf_fwd_back bindings0 new_msgs_tl with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return bindings1 -> Return bindings1
       end
     end
@@ -911,10 +914,10 @@ let rec betree_node_filter_messages_for_key_fwd_back
       begin match
         betree_list_pop_front_back (u64 & betree_message_t) (BetreeListCons (k,
           m) l) with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return msgs0 ->
         begin match betree_node_filter_messages_for_key_fwd_back key msgs0 with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return msgs1 -> Return msgs1
         end
       end
@@ -935,7 +938,7 @@ let rec betree_node_lookup_first_message_after_key_fwd
     then
       begin match betree_node_lookup_first_message_after_key_fwd key next_msgs
         with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return l -> Return l
       end
     else Return (BetreeListCons (k, m) next_msgs)
@@ -956,7 +959,7 @@ let rec betree_node_lookup_first_message_after_key_back
     then
       begin match
         betree_node_lookup_first_message_after_key_back key next_msgs ret with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return next_msgs0 -> Return (BetreeListCons (k, m) next_msgs0)
       end
     else Return ret
@@ -970,10 +973,10 @@ let betree_node_apply_to_internal_fwd_back
   result (betree_list_t (u64 & betree_message_t))
   =
   begin match betree_node_lookup_first_message_for_key_fwd key msgs with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return msgs0 ->
     begin match betree_list_head_has_key_fwd betree_message_t msgs0 key with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return b ->
       if b
       then
@@ -981,17 +984,17 @@ let betree_node_apply_to_internal_fwd_back
         | BetreeMessageInsert i ->
           begin match betree_node_filter_messages_for_key_fwd_back key msgs0
             with
-          | Fail -> Fail
+          | Fail e -> Fail e
           | Return msgs1 ->
             begin match
               betree_list_push_front_fwd_back (u64 & betree_message_t) msgs1
                 (key, BetreeMessageInsert i) with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return msgs2 ->
               begin match
                 betree_node_lookup_first_message_for_key_back key msgs msgs2
                 with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return msgs3 -> Return msgs3
               end
             end
@@ -999,45 +1002,45 @@ let betree_node_apply_to_internal_fwd_back
         | BetreeMessageDelete ->
           begin match betree_node_filter_messages_for_key_fwd_back key msgs0
             with
-          | Fail -> Fail
+          | Fail e -> Fail e
           | Return msgs1 ->
             begin match
               betree_list_push_front_fwd_back (u64 & betree_message_t) msgs1
                 (key, BetreeMessageDelete) with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return msgs2 ->
               begin match
                 betree_node_lookup_first_message_for_key_back key msgs msgs2
                 with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return msgs3 -> Return msgs3
               end
             end
           end
         | BetreeMessageUpsert s ->
           begin match betree_list_hd_fwd (u64 & betree_message_t) msgs0 with
-          | Fail -> Fail
+          | Fail e -> Fail e
           | Return p ->
             let (_, m) = p in
             begin match m with
             | BetreeMessageInsert prev ->
               begin match betree_upsert_update_fwd (Some prev) s with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return v ->
                 begin match
                   betree_list_pop_front_back (u64 & betree_message_t) msgs0
                   with
-                | Fail -> Fail
+                | Fail e -> Fail e
                 | Return msgs1 ->
                   begin match
                     betree_list_push_front_fwd_back (u64 & betree_message_t)
                       msgs1 (key, BetreeMessageInsert v) with
-                  | Fail -> Fail
+                  | Fail e -> Fail e
                   | Return msgs2 ->
                     begin match
                       betree_node_lookup_first_message_for_key_back key msgs
                         msgs2 with
-                    | Fail -> Fail
+                    | Fail e -> Fail e
                     | Return msgs3 -> Return msgs3
                     end
                   end
@@ -1045,22 +1048,22 @@ let betree_node_apply_to_internal_fwd_back
               end
             | BetreeMessageDelete ->
               begin match betree_upsert_update_fwd None s with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return v ->
                 begin match
                   betree_list_pop_front_back (u64 & betree_message_t) msgs0
                   with
-                | Fail -> Fail
+                | Fail e -> Fail e
                 | Return msgs1 ->
                   begin match
                     betree_list_push_front_fwd_back (u64 & betree_message_t)
                       msgs1 (key, BetreeMessageInsert v) with
-                  | Fail -> Fail
+                  | Fail e -> Fail e
                   | Return msgs2 ->
                     begin match
                       betree_node_lookup_first_message_for_key_back key msgs
                         msgs2 with
-                    | Fail -> Fail
+                    | Fail e -> Fail e
                     | Return msgs3 -> Return msgs3
                     end
                   end
@@ -1069,22 +1072,22 @@ let betree_node_apply_to_internal_fwd_back
             | BetreeMessageUpsert ufs ->
               begin match
                 betree_node_lookup_first_message_after_key_fwd key msgs0 with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return msgs1 ->
                 begin match
                   betree_list_push_front_fwd_back (u64 & betree_message_t)
                     msgs1 (key, BetreeMessageUpsert s) with
-                | Fail -> Fail
+                | Fail e -> Fail e
                 | Return msgs2 ->
                   begin match
                     betree_node_lookup_first_message_after_key_back key msgs0
                       msgs2 with
-                  | Fail -> Fail
+                  | Fail e -> Fail e
                   | Return msgs3 ->
                     begin match
                       betree_node_lookup_first_message_for_key_back key msgs
                         msgs3 with
-                    | Fail -> Fail
+                    | Fail e -> Fail e
                     | Return msgs4 -> Return msgs4
                     end
                   end
@@ -1097,11 +1100,11 @@ let betree_node_apply_to_internal_fwd_back
         begin match
           betree_list_push_front_fwd_back (u64 & betree_message_t) msgs0 (key,
             new_msg) with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return msgs1 ->
           begin match
             betree_node_lookup_first_message_for_key_back key msgs msgs1 with
-          | Fail -> Fail
+          | Fail e -> Fail e
           | Return msgs2 -> Return msgs2
           end
         end
@@ -1119,11 +1122,11 @@ let rec betree_node_apply_messages_to_internal_fwd_back
   | BetreeListCons new_msg new_msgs_tl ->
     let (i, m) = new_msg in
     begin match betree_node_apply_to_internal_fwd_back msgs i m with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return msgs0 ->
       begin match
         betree_node_apply_messages_to_internal_fwd_back msgs0 new_msgs_tl with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return msgs1 -> Return msgs1
       end
     end
@@ -1142,31 +1145,31 @@ let rec betree_node_apply_messages_fwd
   begin match self with
   | BetreeNodeInternal node ->
     begin match betree_load_internal_node_fwd node.betree_internal_id st with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return (st0, content) ->
       begin match betree_node_apply_messages_to_internal_fwd_back content msgs
         with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return content0 ->
         begin match betree_list_len_fwd (u64 & betree_message_t) content0 with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return num_msgs ->
           if num_msgs >= params.betree_params_min_flush_size
           then
             begin match
               betree_internal_flush_fwd node params node_id_cnt content0 st0
               with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return (st1, content1) ->
               begin match
                 betree_internal_flush_back node params node_id_cnt content0 st0
                 with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return (node0, _) ->
                 begin match
                   betree_store_internal_node_fwd node0.betree_internal_id
                     content1 st1 with
-                | Fail -> Fail
+                | Fail e -> Fail e
                 | Return (st2, _) -> Return (st2, ())
                 end
               end
@@ -1175,7 +1178,7 @@ let rec betree_node_apply_messages_fwd
             begin match
               betree_store_internal_node_fwd node.betree_internal_id content0
                 st0 with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return (st1, _) -> Return (st1, ())
             end
         end
@@ -1183,27 +1186,27 @@ let rec betree_node_apply_messages_fwd
     end
   | BetreeNodeLeaf node ->
     begin match betree_load_leaf_node_fwd node.betree_leaf_id st with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return (st0, content) ->
       begin match betree_node_apply_messages_to_leaf_fwd_back content msgs with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return content0 ->
         begin match betree_list_len_fwd (u64 & u64) content0 with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return len ->
           begin match u64_mul 2 params.betree_params_split_size with
-          | Fail -> Fail
+          | Fail e -> Fail e
           | Return i ->
             if len >= i
             then
               begin match
                 betree_leaf_split_fwd node content0 params node_id_cnt st0 with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return (st1, _) ->
                 begin match
                   betree_store_leaf_node_fwd node.betree_leaf_id BetreeListNil
                     st1 with
-                | Fail -> Fail
+                | Fail e -> Fail e
                 | Return (st2, _) -> Return (st2, ())
                 end
               end
@@ -1211,7 +1214,7 @@ let rec betree_node_apply_messages_fwd
               begin match
                 betree_store_leaf_node_fwd node.betree_leaf_id content0 st0
                 with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return (st1, _) -> Return (st1, ())
               end
           end
@@ -1232,31 +1235,31 @@ and betree_node_apply_messages_back
   begin match self with
   | BetreeNodeInternal node ->
     begin match betree_load_internal_node_fwd node.betree_internal_id st with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return (st0, content) ->
       begin match betree_node_apply_messages_to_internal_fwd_back content msgs
         with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return content0 ->
         begin match betree_list_len_fwd (u64 & betree_message_t) content0 with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return num_msgs ->
           if num_msgs >= params.betree_params_min_flush_size
           then
             begin match
               betree_internal_flush_fwd node params node_id_cnt content0 st0
               with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return (st1, content1) ->
               begin match
                 betree_internal_flush_back node params node_id_cnt content0 st0
                 with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return (node0, node_id_cnt0) ->
                 begin match
                   betree_store_internal_node_fwd node0.betree_internal_id
                     content1 st1 with
-                | Fail -> Fail
+                | Fail e -> Fail e
                 | Return (_, _) ->
                   Return (BetreeNodeInternal node0, node_id_cnt0)
                 end
@@ -1266,7 +1269,7 @@ and betree_node_apply_messages_back
             begin match
               betree_store_internal_node_fwd node.betree_internal_id content0
                 st0 with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return (_, _) -> Return (BetreeNodeInternal node, node_id_cnt)
             end
         end
@@ -1274,32 +1277,32 @@ and betree_node_apply_messages_back
     end
   | BetreeNodeLeaf node ->
     begin match betree_load_leaf_node_fwd node.betree_leaf_id st with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return (st0, content) ->
       begin match betree_node_apply_messages_to_leaf_fwd_back content msgs with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return content0 ->
         begin match betree_list_len_fwd (u64 & u64) content0 with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return len ->
           begin match u64_mul 2 params.betree_params_split_size with
-          | Fail -> Fail
+          | Fail e -> Fail e
           | Return i ->
             if len >= i
             then
               begin match
                 betree_leaf_split_fwd node content0 params node_id_cnt st0 with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return (st1, new_node) ->
                 begin match
                   betree_store_leaf_node_fwd node.betree_leaf_id BetreeListNil
                     st1 with
-                | Fail -> Fail
+                | Fail e -> Fail e
                 | Return (_, _) ->
                   begin match
                     betree_leaf_split_back node content0 params node_id_cnt st0
                     with
-                  | Fail -> Fail
+                  | Fail e -> Fail e
                   | Return node_id_cnt0 ->
                     Return (BetreeNodeInternal new_node, node_id_cnt0)
                   end
@@ -1309,7 +1312,7 @@ and betree_node_apply_messages_back
               begin match
                 betree_store_leaf_node_fwd node.betree_leaf_id content0 st0
                 with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return (_, _) ->
                 Return (BetreeNodeLeaf (Mkbetree_leaf_t node.betree_leaf_id
                   len), node_id_cnt)
@@ -1332,39 +1335,39 @@ and betree_internal_flush_fwd
   begin match
     betree_list_partition_at_pivot_fwd betree_message_t content
       self.betree_internal_pivot with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return p ->
     let (msgs_left, msgs_right) = p in
     begin match betree_list_len_fwd (u64 & betree_message_t) msgs_left with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return len_left ->
       if len_left >= params.betree_params_min_flush_size
       then
         begin match
           betree_node_apply_messages_fwd self.betree_internal_left params
             node_id_cnt msgs_left st with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return (st0, _) ->
           begin match
             betree_node_apply_messages_back self.betree_internal_left params
               node_id_cnt msgs_left st with
-          | Fail -> Fail
+          | Fail e -> Fail e
           | Return (_, node_id_cnt0) ->
             begin match betree_list_len_fwd (u64 & betree_message_t) msgs_right
               with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return len_right ->
               if len_right >= params.betree_params_min_flush_size
               then
                 begin match
                   betree_node_apply_messages_fwd self.betree_internal_right
                     params node_id_cnt0 msgs_right st0 with
-                | Fail -> Fail
+                | Fail e -> Fail e
                 | Return (st1, _) ->
                   begin match
                     betree_node_apply_messages_back self.betree_internal_right
                       params node_id_cnt0 msgs_right st0 with
-                  | Fail -> Fail
+                  | Fail e -> Fail e
                   | Return (_, _) -> Return (st1, BetreeListNil)
                   end
                 end
@@ -1376,12 +1379,12 @@ and betree_internal_flush_fwd
         begin match
           betree_node_apply_messages_fwd self.betree_internal_right params
             node_id_cnt msgs_right st with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return (st0, _) ->
           begin match
             betree_node_apply_messages_back self.betree_internal_right params
               node_id_cnt msgs_right st with
-          | Fail -> Fail
+          | Fail e -> Fail e
           | Return (_, _) -> Return (st0, msgs_left)
           end
         end
@@ -1400,34 +1403,34 @@ and betree_internal_flush_back
   begin match
     betree_list_partition_at_pivot_fwd betree_message_t content
       self.betree_internal_pivot with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return p ->
     let (msgs_left, msgs_right) = p in
     begin match betree_list_len_fwd (u64 & betree_message_t) msgs_left with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return len_left ->
       if len_left >= params.betree_params_min_flush_size
       then
         begin match
           betree_node_apply_messages_fwd self.betree_internal_left params
             node_id_cnt msgs_left st with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return (st0, _) ->
           begin match
             betree_node_apply_messages_back self.betree_internal_left params
               node_id_cnt msgs_left st with
-          | Fail -> Fail
+          | Fail e -> Fail e
           | Return (n, node_id_cnt0) ->
             begin match betree_list_len_fwd (u64 & betree_message_t) msgs_right
               with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return len_right ->
               if len_right >= params.betree_params_min_flush_size
               then
                 begin match
                   betree_node_apply_messages_back self.betree_internal_right
                     params node_id_cnt0 msgs_right st0 with
-                | Fail -> Fail
+                | Fail e -> Fail e
                 | Return (n0, node_id_cnt1) ->
                   Return (Mkbetree_internal_t self.betree_internal_id
                     self.betree_internal_pivot n n0, node_id_cnt1)
@@ -1443,7 +1446,7 @@ and betree_internal_flush_back
         begin match
           betree_node_apply_messages_back self.betree_internal_right params
             node_id_cnt msgs_right st with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return (n, node_id_cnt0) ->
           Return (Mkbetree_internal_t self.betree_internal_id
             self.betree_internal_pivot self.betree_internal_left n,
@@ -1463,12 +1466,12 @@ let betree_node_apply_fwd
   begin match
     betree_node_apply_messages_fwd self params node_id_cnt (BetreeListCons
       (key, new_msg) l) st with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return (st0, _) ->
     begin match
       betree_node_apply_messages_back self params node_id_cnt (BetreeListCons
         (key, new_msg) l) st with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return (_, _) -> Return (st0, ())
     end
   end
@@ -1484,7 +1487,7 @@ let betree_node_apply_back
   begin match
     betree_node_apply_messages_back self params node_id_cnt (BetreeListCons
       (key, new_msg) l) st with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return (self0, node_id_cnt0) -> Return (self0, node_id_cnt0)
   end
 
@@ -1494,16 +1497,16 @@ let betree_be_tree_new_fwd
   result (state & betree_be_tree_t)
   =
   begin match betree_node_id_counter_new_fwd with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return node_id_cnt ->
     begin match betree_node_id_counter_fresh_id_fwd node_id_cnt with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return id ->
       begin match betree_store_leaf_node_fwd id BetreeListNil st with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return (st0, _) ->
         begin match betree_node_id_counter_fresh_id_back node_id_cnt with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return node_id_cnt0 ->
           Return (st0, Mkbetree_be_tree_t (Mkbetree_params_t min_flush_size
             split_size) node_id_cnt0 (BetreeNodeLeaf (Mkbetree_leaf_t id 0)))
@@ -1520,13 +1523,13 @@ let betree_be_tree_apply_fwd
   begin match
     betree_node_apply_fwd self.betree_be_tree_root self.betree_be_tree_params
       self.betree_be_tree_node_id_cnt key msg st with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return (st0, _) ->
     begin match
       betree_node_apply_back self.betree_be_tree_root
         self.betree_be_tree_params self.betree_be_tree_node_id_cnt key msg st
       with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return (_, _) -> Return (st0, ())
     end
   end
@@ -1539,7 +1542,7 @@ let betree_be_tree_apply_back
   begin match
     betree_node_apply_back self.betree_be_tree_root self.betree_be_tree_params
       self.betree_be_tree_node_id_cnt key msg st with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return (n, nic) ->
     Return (Mkbetree_be_tree_t self.betree_be_tree_params nic n)
   end
@@ -1551,11 +1554,11 @@ let betree_be_tree_insert_fwd
   =
   begin match betree_be_tree_apply_fwd self key (BetreeMessageInsert value) st
     with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return (st0, _) ->
     begin match
       betree_be_tree_apply_back self key (BetreeMessageInsert value) st with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return _ -> Return (st0, ())
     end
   end
@@ -1567,7 +1570,7 @@ let betree_be_tree_insert_back
   =
   begin match betree_be_tree_apply_back self key (BetreeMessageInsert value) st
     with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return self0 -> Return self0
   end
 
@@ -1575,10 +1578,10 @@ let betree_be_tree_insert_back
 let betree_be_tree_delete_fwd
   (self : betree_be_tree_t) (key : u64) (st : state) : result (state & unit) =
   begin match betree_be_tree_apply_fwd self key BetreeMessageDelete st with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return (st0, _) ->
     begin match betree_be_tree_apply_back self key BetreeMessageDelete st with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return _ -> Return (st0, ())
     end
   end
@@ -1589,7 +1592,7 @@ let betree_be_tree_delete_back
   result betree_be_tree_t
   =
   begin match betree_be_tree_apply_back self key BetreeMessageDelete st with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return self0 -> Return self0
   end
 
@@ -1601,11 +1604,11 @@ let betree_be_tree_upsert_fwd
   =
   begin match betree_be_tree_apply_fwd self key (BetreeMessageUpsert upd) st
     with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return (st0, _) ->
     begin match betree_be_tree_apply_back self key (BetreeMessageUpsert upd) st
       with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return _ -> Return (st0, ())
     end
   end
@@ -1618,7 +1621,7 @@ let betree_be_tree_upsert_back
   =
   begin match betree_be_tree_apply_back self key (BetreeMessageUpsert upd) st
     with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return self0 -> Return self0
   end
 
@@ -1628,7 +1631,7 @@ let betree_be_tree_lookup_fwd
   result (state & (option u64))
   =
   begin match betree_node_lookup_fwd self.betree_be_tree_root key st with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return (st0, opt) -> Return (st0, opt)
   end
 
@@ -1638,7 +1641,7 @@ let betree_be_tree_lookup_back
   result betree_be_tree_t
   =
   begin match betree_node_lookup_back self.betree_be_tree_root key st with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return n ->
     Return (Mkbetree_be_tree_t self.betree_be_tree_params
       self.betree_be_tree_node_id_cnt n)
diff --git a/tests/fstar/betree/Primitives.fst b/tests/fstar/betree/Primitives.fst
index 96138e46..82622656 100644
--- a/tests/fstar/betree/Primitives.fst
+++ b/tests/fstar/betree/Primitives.fst
@@ -18,9 +18,13 @@ let rec list_update #a ls i x =
 #pop-options
 
 (*** Result *)
+type error : Type0 =
+| Failure
+| OutOfFuel
+
 type result (a : Type0) : Type0 =
 | Return : v:a -> result a
-| Fail : result a
+| Fail : e:error -> result a
 
 // Monadic bind and return.
 // Re-definining those allows us to customize the result of the monadic notations
@@ -29,10 +33,10 @@ let return (#a : Type0) (x:a) : result a = Return x
 let bind (#a #b : Type0) (m : result a) (f : a -> result b) : result b =
     match m with
     | Return x -> f x
-    | Fail -> Fail
+    | Fail e -> Fail e
 
 // Monadic assert(...)
-let massert (b:bool) : result unit = if b then Return () else Fail
+let massert (b:bool) : result unit = if b then Return () else Fail Failure
 
 // Normalize and unwrap a successful result (used for globals).
 let eval_global (#a : Type0) (x : result a{Return? (normalize_term x)}) : a = Return?.v x
@@ -119,12 +123,12 @@ let scalar_max (ty : scalar_ty) : int =
 type scalar (ty : scalar_ty) : eqtype = x:int{scalar_min ty <= x && x <= scalar_max ty}
 
 let mk_scalar (ty : scalar_ty) (x : int) : result (scalar ty) =
-  if scalar_min ty <= x && scalar_max ty >= x then Return x else Fail
+  if scalar_min ty <= x && scalar_max ty >= x then Return x else Fail Failure
 
 let scalar_neg (#ty : scalar_ty) (x : scalar ty) : result (scalar ty) = mk_scalar ty (-x)
 
 let scalar_div (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
-  if y <> 0 then mk_scalar ty (x / y) else Fail
+  if y <> 0 then mk_scalar ty (x / y) else Fail Failure
 
 /// The remainder operation
 let int_rem (x : int) (y : int{y <> 0}) : int =
@@ -137,7 +141,7 @@ let _ = assert_norm(int_rem 1 (-2) = 1)
 let _ = assert_norm(int_rem (-1) (-2) = -1)
 
 let scalar_rem (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
-  if y <> 0 then mk_scalar ty (int_rem x y) else Fail
+  if y <> 0 then mk_scalar ty (int_rem x y) else Fail Failure
 
 let scalar_add (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
   mk_scalar ty (x + y)
@@ -258,7 +262,7 @@ let vec_push_back (a  : Type0) (v : vec a) (x : a) :
   (requires True)
   (ensures (fun res ->
     match res with
-    | Fail -> True
+    | Fail e -> e == Failure
     | Return v' -> length v' = length v + 1)) =
   if length v < usize_max then begin
     (**) assert_norm(length [x] == 1);
@@ -266,22 +270,22 @@ let vec_push_back (a  : Type0) (v : vec a) (x : a) :
     (**) assert(length (append v [x]) = length v + 1);
     Return (append v [x])
     end
-  else Fail
+  else Fail Failure
 
 // The **forward** function shouldn't be used
 let vec_insert_fwd (a : Type0) (v : vec a) (i : usize) (x : a) : result unit =
-  if i < length v then Return () else Fail
+  if i < length v then Return () else Fail Failure
 let vec_insert_back (a : Type0) (v : vec a) (i : usize) (x : a) : result (vec a) =
-  if i < length v then Return (list_update v i x) else Fail
+  if i < length v then Return (list_update v i x) else Fail Failure
 
 // The **backward** function shouldn't be used
 let vec_index_fwd (a : Type0) (v : vec a) (i : usize) : result a =
-  if i < length v then Return (index v i) else Fail
+  if i < length v then Return (index v i) else Fail Failure
 let vec_index_back (a : Type0) (v : vec a) (i : usize) (x : a) : result unit =
-  if i < length v then Return () else Fail
+  if i < length v then Return () else Fail Failure
 
 let vec_index_mut_fwd (a : Type0) (v : vec a) (i : usize) : result a =
-  if i < length v then Return (index v i) else Fail
+  if i < length v then Return (index v i) else Fail Failure
 let vec_index_mut_back (a : Type0) (v : vec a) (i : usize) (nx : a) : result (vec a) =
-  if i < length v then Return (list_update v i nx) else Fail
+  if i < length v then Return (list_update v i nx) else Fail Failure
 
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
index eebed6e6..6a2b7c09 100644
--- a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
+++ b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
@@ -14,7 +14,7 @@ let betree_load_internal_node_fwd
   result (state & (betree_list_t (u64 & betree_message_t)))
   =
   begin match betree_utils_load_internal_node_fwd id st with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return (st0, l) -> Return (st0, l)
   end
 
@@ -24,7 +24,7 @@ let betree_store_internal_node_fwd
   result (state & unit)
   =
   begin match betree_utils_store_internal_node_fwd id content st with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return (st0, _) -> Return (st0, ())
   end
 
@@ -32,7 +32,7 @@ let betree_store_internal_node_fwd
 let betree_load_leaf_node_fwd
   (id : u64) (st : state) : result (state & (betree_list_t (u64 & u64))) =
   begin match betree_utils_load_leaf_node_fwd id st with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return (st0, l) -> Return (st0, l)
   end
 
@@ -42,21 +42,21 @@ let betree_store_leaf_node_fwd
   result (state & unit)
   =
   begin match betree_utils_store_leaf_node_fwd id content st with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return (st0, _) -> Return (st0, ())
   end
 
 (** [betree_main::betree::fresh_node_id] *)
 let betree_fresh_node_id_fwd (counter : u64) : result u64 =
   begin match u64_add counter 1 with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return _ -> Return counter
   end
 
 (** [betree_main::betree::fresh_node_id] *)
 let betree_fresh_node_id_back (counter : u64) : result u64 =
   begin match u64_add counter 1 with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return counter0 -> Return counter0
   end
 
@@ -68,7 +68,7 @@ let betree_node_id_counter_new_fwd : result betree_node_id_counter_t =
 let betree_node_id_counter_fresh_id_fwd
   (self : betree_node_id_counter_t) : result u64 =
   begin match u64_add self.betree_node_id_counter_next_node_id 1 with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return _ -> Return self.betree_node_id_counter_next_node_id
   end
 
@@ -76,7 +76,7 @@ let betree_node_id_counter_fresh_id_fwd
 let betree_node_id_counter_fresh_id_back
   (self : betree_node_id_counter_t) : result betree_node_id_counter_t =
   begin match u64_add self.betree_node_id_counter_next_node_id 1 with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return i -> Return (Mkbetree_node_id_counter_t i)
   end
 
@@ -97,12 +97,12 @@ let betree_upsert_update_fwd
     begin match st with
     | BetreeUpsertFunStateAdd v ->
       begin match u64_sub core_num_u64_max_c prev0 with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return margin ->
         if margin >= v
         then
           begin match u64_add prev0 v with
-          | Fail -> Fail
+          | Fail e -> Fail e
           | Return i -> Return i
           end
         else Return core_num_u64_max_c
@@ -111,7 +111,7 @@ let betree_upsert_update_fwd
       if prev0 >= v
       then
         begin match u64_sub prev0 v with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return i -> Return i
         end
       else Return 0
@@ -126,9 +126,12 @@ let rec betree_list_len_fwd
   begin match self with
   | BetreeListCons x tl ->
     begin match betree_list_len_fwd t tl with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return i ->
-      begin match u64_add 1 i with | Fail -> Fail | Return i0 -> Return i0 end
+      begin match u64_add 1 i with
+      | Fail e -> Fail e
+      | Return i0 -> Return i0
+      end
     end
   | BetreeListNil -> Return 0
   end
@@ -145,17 +148,17 @@ let rec betree_list_split_at_fwd
     begin match self with
     | BetreeListCons hd tl ->
       begin match u64_sub n 1 with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return i ->
         begin match betree_list_split_at_fwd t tl i with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return p ->
           let (ls0, ls1) = p in
           let l = ls0 in
           Return (BetreeListCons hd l, ls1)
         end
       end
-    | BetreeListNil -> Fail
+    | BetreeListNil -> Fail Failure
     end
 
 (** [betree_main::betree::List::{1}::push_front] *)
@@ -170,7 +173,7 @@ let betree_list_pop_front_fwd (t : Type0) (self : betree_list_t t) : result t =
   let ls = mem_replace_fwd (betree_list_t t) self BetreeListNil in
   begin match ls with
   | BetreeListCons x tl -> Return x
-  | BetreeListNil -> Fail
+  | BetreeListNil -> Fail Failure
   end
 
 (** [betree_main::betree::List::{1}::pop_front] *)
@@ -179,14 +182,14 @@ let betree_list_pop_front_back
   let ls = mem_replace_fwd (betree_list_t t) self BetreeListNil in
   begin match ls with
   | BetreeListCons x tl -> Return tl
-  | BetreeListNil -> Fail
+  | BetreeListNil -> Fail Failure
   end
 
 (** [betree_main::betree::List::{1}::hd] *)
 let betree_list_hd_fwd (t : Type0) (self : betree_list_t t) : result t =
   begin match self with
   | BetreeListCons hd l -> Return hd
-  | BetreeListNil -> Fail
+  | BetreeListNil -> Fail Failure
   end
 
 (** [betree_main::betree::List::{2}::head_has_key] *)
@@ -210,7 +213,7 @@ let rec betree_list_partition_at_pivot_fwd
     then Return (BetreeListNil, BetreeListCons (i, x) tl)
     else
       begin match betree_list_partition_at_pivot_fwd t tl pivot with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return p ->
         let (ls0, ls1) = p in
         let l = ls0 in
@@ -229,27 +232,27 @@ let betree_leaf_split_fwd
   begin match
     betree_list_split_at_fwd (u64 & u64) content
       params.betree_params_split_size with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return p ->
     let (content0, content1) = p in
     begin match betree_list_hd_fwd (u64 & u64) content1 with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return p0 ->
       let (pivot, _) = p0 in
       begin match betree_node_id_counter_fresh_id_fwd node_id_cnt with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return id0 ->
         begin match betree_node_id_counter_fresh_id_back node_id_cnt with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return node_id_cnt0 ->
           begin match betree_node_id_counter_fresh_id_fwd node_id_cnt0 with
-          | Fail -> Fail
+          | Fail e -> Fail e
           | Return id1 ->
             begin match betree_store_leaf_node_fwd id0 content0 st with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return (st0, _) ->
               begin match betree_store_leaf_node_fwd id1 content1 st0 with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return (st1, _) ->
                 let n = BetreeNodeLeaf (Mkbetree_leaf_t id0
                   params.betree_params_split_size) in
@@ -275,26 +278,26 @@ let betree_leaf_split_back0
   begin match
     betree_list_split_at_fwd (u64 & u64) content
       params.betree_params_split_size with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return p ->
     let (content0, content1) = p in
     begin match betree_list_hd_fwd (u64 & u64) content1 with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return _ ->
       begin match betree_node_id_counter_fresh_id_fwd node_id_cnt with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return id0 ->
         begin match betree_node_id_counter_fresh_id_back node_id_cnt with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return node_id_cnt0 ->
           begin match betree_node_id_counter_fresh_id_fwd node_id_cnt0 with
-          | Fail -> Fail
+          | Fail e -> Fail e
           | Return id1 ->
             begin match betree_store_leaf_node_fwd id0 content0 st with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return (st1, _) ->
               begin match betree_store_leaf_node_fwd id1 content1 st1 with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return (_, _) -> Return (st0, ())
               end
             end
@@ -314,26 +317,26 @@ let betree_leaf_split_back1
   begin match
     betree_list_split_at_fwd (u64 & u64) content
       params.betree_params_split_size with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return p ->
     let (content0, content1) = p in
     begin match betree_list_hd_fwd (u64 & u64) content1 with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return _ ->
       begin match betree_node_id_counter_fresh_id_fwd node_id_cnt with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return id0 ->
         begin match betree_node_id_counter_fresh_id_back node_id_cnt with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return node_id_cnt0 ->
           begin match betree_node_id_counter_fresh_id_fwd node_id_cnt0 with
-          | Fail -> Fail
+          | Fail e -> Fail e
           | Return id1 ->
             begin match betree_store_leaf_node_fwd id0 content0 st with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return (st1, _) ->
               begin match betree_store_leaf_node_fwd id1 content1 st1 with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return (_, _) -> Return (st0, ())
               end
             end
@@ -353,30 +356,30 @@ let betree_leaf_split_back2
   begin match
     betree_list_split_at_fwd (u64 & u64) content
       params.betree_params_split_size with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return p ->
     let (content0, content1) = p in
     begin match betree_list_hd_fwd (u64 & u64) content1 with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return _ ->
       begin match betree_node_id_counter_fresh_id_fwd node_id_cnt with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return id0 ->
         begin match betree_node_id_counter_fresh_id_back node_id_cnt with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return node_id_cnt0 ->
           begin match betree_node_id_counter_fresh_id_fwd node_id_cnt0 with
-          | Fail -> Fail
+          | Fail e -> Fail e
           | Return id1 ->
             begin match betree_store_leaf_node_fwd id0 content0 st with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return (st1, _) ->
               begin match betree_store_leaf_node_fwd id1 content1 st1 with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return (_, _) ->
                 begin match betree_node_id_counter_fresh_id_back node_id_cnt0
                   with
-                | Fail -> Fail
+                | Fail e -> Fail e
                 | Return node_id_cnt1 -> Return (st0, node_id_cnt1)
                 end
               end
@@ -403,7 +406,7 @@ let rec betree_node_lookup_in_bindings_fwd
       then Return None
       else
         begin match betree_node_lookup_in_bindings_fwd key tl with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return opt -> Return opt
         end
   | BetreeListNil -> Return None
@@ -423,7 +426,7 @@ let rec betree_node_lookup_first_message_for_key_fwd
     else
       begin match betree_node_lookup_first_message_for_key_fwd key next_msgs
         with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return l -> Return l
       end
   | BetreeListNil -> Return BetreeListNil
@@ -444,7 +447,7 @@ let rec betree_node_lookup_first_message_for_key_back
     else
       begin match
         betree_node_lookup_first_message_for_key_back key next_msgs ret with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return next_msgs0 -> Return (BetreeListCons (i, m) next_msgs0)
       end
   | BetreeListNil -> Return ret
@@ -458,28 +461,28 @@ let rec betree_node_apply_upserts_fwd
   (decreases (betree_node_apply_upserts_decreases msgs prev key st))
   =
   begin match betree_list_head_has_key_fwd betree_message_t msgs key with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return b ->
     if b
     then
       begin match betree_list_pop_front_fwd (u64 & betree_message_t) msgs with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return msg ->
         let (_, m) = msg in
         begin match m with
-        | BetreeMessageInsert i -> Fail
-        | BetreeMessageDelete -> Fail
+        | BetreeMessageInsert i -> Fail Failure
+        | BetreeMessageDelete -> Fail Failure
         | BetreeMessageUpsert s ->
           begin match betree_upsert_update_fwd prev s with
-          | Fail -> Fail
+          | Fail e -> Fail e
           | Return v ->
             begin match
               betree_list_pop_front_back (u64 & betree_message_t) msgs with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return msgs0 ->
               begin match betree_node_apply_upserts_fwd msgs0 (Some v) key st
                 with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return (st0, i) -> Return (st0, i)
               end
             end
@@ -488,12 +491,12 @@ let rec betree_node_apply_upserts_fwd
       end
     else
       begin match core_option_option_unwrap_fwd u64 prev st with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return (st0, v) ->
         begin match
           betree_list_push_front_fwd_back (u64 & betree_message_t) msgs (key,
             BetreeMessageInsert v) with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return _ -> Return (st0, v)
         end
       end
@@ -507,28 +510,28 @@ let rec betree_node_apply_upserts_back
   (decreases (betree_node_apply_upserts_decreases msgs prev key st))
   =
   begin match betree_list_head_has_key_fwd betree_message_t msgs key with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return b ->
     if b
     then
       begin match betree_list_pop_front_fwd (u64 & betree_message_t) msgs with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return msg ->
         let (_, m) = msg in
         begin match m with
-        | BetreeMessageInsert i -> Fail
-        | BetreeMessageDelete -> Fail
+        | BetreeMessageInsert i -> Fail Failure
+        | BetreeMessageDelete -> Fail Failure
         | BetreeMessageUpsert s ->
           begin match betree_upsert_update_fwd prev s with
-          | Fail -> Fail
+          | Fail e -> Fail e
           | Return v ->
             begin match
               betree_list_pop_front_back (u64 & betree_message_t) msgs with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return msgs0 ->
               begin match
                 betree_node_apply_upserts_back msgs0 (Some v) key st st0 with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return (st1, msgs1) -> Return (st1, msgs1)
               end
             end
@@ -537,12 +540,12 @@ let rec betree_node_apply_upserts_back
       end
     else
       begin match core_option_option_unwrap_fwd u64 prev st with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return (_, v) ->
         begin match
           betree_list_push_front_fwd_back (u64 & betree_message_t) msgs (key,
             BetreeMessageInsert v) with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return msgs0 -> Return (st0, msgs0)
         end
       end
@@ -557,10 +560,10 @@ let rec betree_node_lookup_fwd
   begin match self with
   | BetreeNodeInternal node ->
     begin match betree_load_internal_node_fwd node.betree_internal_id st with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return (st0, msgs) ->
       begin match betree_node_lookup_first_message_for_key_fwd key msgs with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return pending ->
         begin match pending with
         | BetreeListCons p l ->
@@ -569,12 +572,12 @@ let rec betree_node_lookup_fwd
           then
             begin match betree_internal_lookup_in_children_fwd node key st0
               with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return (st1, opt) ->
               begin match
                 betree_node_lookup_first_message_for_key_back key msgs
                   (BetreeListCons (k, msg) l) with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return _ -> Return (st1, opt)
               end
             end
@@ -584,45 +587,45 @@ let rec betree_node_lookup_fwd
               begin match
                 betree_node_lookup_first_message_for_key_back key msgs
                   (BetreeListCons (k, BetreeMessageInsert v) l) with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return _ -> Return (st0, Some v)
               end
             | BetreeMessageDelete ->
               begin match
                 betree_node_lookup_first_message_for_key_back key msgs
                   (BetreeListCons (k, BetreeMessageDelete) l) with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return _ -> Return (st0, None)
               end
             | BetreeMessageUpsert ufs ->
               begin match betree_internal_lookup_in_children_fwd node key st0
                 with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return (st1, v) ->
                 begin match
                   betree_node_apply_upserts_fwd (BetreeListCons (k,
                     BetreeMessageUpsert ufs) l) v key st1 with
-                | Fail -> Fail
+                | Fail e -> Fail e
                 | Return (st2, v0) ->
                   begin match
                     betree_internal_lookup_in_children_back node key st0 st2
                     with
-                  | Fail -> Fail
+                  | Fail e -> Fail e
                   | Return (st3, node0) ->
                     begin match
                       betree_node_apply_upserts_back (BetreeListCons (k,
                         BetreeMessageUpsert ufs) l) v key st1 st3 with
-                    | Fail -> Fail
+                    | Fail e -> Fail e
                     | Return (st4, pending0) ->
                       begin match
                         betree_node_lookup_first_message_for_key_back key msgs
                           pending0 with
-                      | Fail -> Fail
+                      | Fail e -> Fail e
                       | Return msgs0 ->
                         begin match
                           betree_store_internal_node_fwd
                             node0.betree_internal_id msgs0 st4 with
-                        | Fail -> Fail
+                        | Fail e -> Fail e
                         | Return (st5, _) -> Return (st5, Some v0)
                         end
                       end
@@ -633,12 +636,12 @@ let rec betree_node_lookup_fwd
             end
         | BetreeListNil ->
           begin match betree_internal_lookup_in_children_fwd node key st0 with
-          | Fail -> Fail
+          | Fail e -> Fail e
           | Return (st1, opt) ->
             begin match
               betree_node_lookup_first_message_for_key_back key msgs
                 BetreeListNil with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return _ -> Return (st1, opt)
             end
           end
@@ -647,10 +650,10 @@ let rec betree_node_lookup_fwd
     end
   | BetreeNodeLeaf node ->
     begin match betree_load_leaf_node_fwd node.betree_leaf_id st with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return (st0, bindings) ->
       begin match betree_node_lookup_in_bindings_fwd key bindings with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return opt -> Return (st0, opt)
       end
     end
@@ -665,10 +668,10 @@ and betree_node_lookup_back
   begin match self with
   | BetreeNodeInternal node ->
     begin match betree_load_internal_node_fwd node.betree_internal_id st with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return (st1, msgs) ->
       begin match betree_node_lookup_first_message_for_key_fwd key msgs with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return pending ->
         begin match pending with
         | BetreeListCons p l ->
@@ -678,11 +681,11 @@ and betree_node_lookup_back
             begin match
               betree_node_lookup_first_message_for_key_back key msgs
                 (BetreeListCons (k, msg) l) with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return _ ->
               begin match
                 betree_internal_lookup_in_children_back node key st1 st0 with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return (st2, node0) -> Return (st2, BetreeNodeInternal node0)
               end
             end
@@ -692,45 +695,45 @@ and betree_node_lookup_back
               begin match
                 betree_node_lookup_first_message_for_key_back key msgs
                   (BetreeListCons (k, BetreeMessageInsert v) l) with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return _ -> Return (st0, BetreeNodeInternal node)
               end
             | BetreeMessageDelete ->
               begin match
                 betree_node_lookup_first_message_for_key_back key msgs
                   (BetreeListCons (k, BetreeMessageDelete) l) with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return _ -> Return (st0, BetreeNodeInternal node)
               end
             | BetreeMessageUpsert ufs ->
               begin match betree_internal_lookup_in_children_fwd node key st1
                 with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return (st2, v) ->
                 begin match
                   betree_node_apply_upserts_fwd (BetreeListCons (k,
                     BetreeMessageUpsert ufs) l) v key st2 with
-                | Fail -> Fail
+                | Fail e -> Fail e
                 | Return (st3, _) ->
                   begin match
                     betree_internal_lookup_in_children_back node key st1 st3
                     with
-                  | Fail -> Fail
+                  | Fail e -> Fail e
                   | Return (st4, node0) ->
                     begin match
                       betree_node_apply_upserts_back (BetreeListCons (k,
                         BetreeMessageUpsert ufs) l) v key st2 st4 with
-                    | Fail -> Fail
+                    | Fail e -> Fail e
                     | Return (st5, pending0) ->
                       begin match
                         betree_node_lookup_first_message_for_key_back key msgs
                           pending0 with
-                      | Fail -> Fail
+                      | Fail e -> Fail e
                       | Return msgs0 ->
                         begin match
                           betree_store_internal_node_fwd
                             node0.betree_internal_id msgs0 st5 with
-                        | Fail -> Fail
+                        | Fail e -> Fail e
                         | Return (_, _) ->
                           Return (st0, BetreeNodeInternal node0)
                         end
@@ -744,11 +747,11 @@ and betree_node_lookup_back
           begin match
             betree_node_lookup_first_message_for_key_back key msgs
               BetreeListNil with
-          | Fail -> Fail
+          | Fail e -> Fail e
           | Return _ ->
             begin match
               betree_internal_lookup_in_children_back node key st1 st0 with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return (st2, node0) -> Return (st2, BetreeNodeInternal node0)
             end
           end
@@ -757,10 +760,10 @@ and betree_node_lookup_back
     end
   | BetreeNodeLeaf node ->
     begin match betree_load_leaf_node_fwd node.betree_leaf_id st with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return (_, bindings) ->
       begin match betree_node_lookup_in_bindings_fwd key bindings with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return _ -> Return (st0, BetreeNodeLeaf node)
       end
     end
@@ -775,12 +778,12 @@ and betree_internal_lookup_in_children_fwd
   if key < self.betree_internal_pivot
   then
     begin match betree_node_lookup_fwd self.betree_internal_left key st with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return (st0, opt) -> Return (st0, opt)
     end
   else
     begin match betree_node_lookup_fwd self.betree_internal_right key st with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return (st0, opt) -> Return (st0, opt)
     end
 
@@ -794,7 +797,7 @@ and betree_internal_lookup_in_children_back
   then
     begin match betree_node_lookup_back self.betree_internal_left key st st0
       with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return (st1, n) ->
       Return (st1, Mkbetree_internal_t self.betree_internal_id
         self.betree_internal_pivot n self.betree_internal_right)
@@ -802,7 +805,7 @@ and betree_internal_lookup_in_children_back
   else
     begin match betree_node_lookup_back self.betree_internal_right key st st0
       with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return (st1, n) ->
       Return (st1, Mkbetree_internal_t self.betree_internal_id
         self.betree_internal_pivot self.betree_internal_left n)
@@ -821,7 +824,7 @@ let rec betree_node_lookup_mut_in_bindings_fwd
     then Return (BetreeListCons (i, i0) tl)
     else
       begin match betree_node_lookup_mut_in_bindings_fwd key tl with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return l -> Return l
       end
   | BetreeListNil -> Return BetreeListNil
@@ -841,7 +844,7 @@ let rec betree_node_lookup_mut_in_bindings_back
     then Return ret
     else
       begin match betree_node_lookup_mut_in_bindings_back key tl ret with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return tl0 -> Return (BetreeListCons (i, i0) tl0)
       end
   | BetreeListNil -> Return ret
@@ -854,62 +857,62 @@ let betree_node_apply_to_leaf_fwd_back
   result (betree_list_t (u64 & u64))
   =
   begin match betree_node_lookup_mut_in_bindings_fwd key bindings with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return bindings0 ->
     begin match betree_list_head_has_key_fwd u64 bindings0 key with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return b ->
       if b
       then
         begin match betree_list_pop_front_fwd (u64 & u64) bindings0 with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return hd ->
           begin match new_msg with
           | BetreeMessageInsert v ->
             begin match betree_list_pop_front_back (u64 & u64) bindings0 with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return bindings1 ->
               begin match
                 betree_list_push_front_fwd_back (u64 & u64) bindings1 (key, v)
                 with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return bindings2 ->
                 begin match
                   betree_node_lookup_mut_in_bindings_back key bindings
                     bindings2 with
-                | Fail -> Fail
+                | Fail e -> Fail e
                 | Return bindings3 -> Return bindings3
                 end
               end
             end
           | BetreeMessageDelete ->
             begin match betree_list_pop_front_back (u64 & u64) bindings0 with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return bindings1 ->
               begin match
                 betree_node_lookup_mut_in_bindings_back key bindings bindings1
                 with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return bindings2 -> Return bindings2
               end
             end
           | BetreeMessageUpsert s ->
             let (_, i) = hd in
             begin match betree_upsert_update_fwd (Some i) s with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return v ->
               begin match betree_list_pop_front_back (u64 & u64) bindings0 with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return bindings1 ->
                 begin match
                   betree_list_push_front_fwd_back (u64 & u64) bindings1 (key,
                     v) with
-                | Fail -> Fail
+                | Fail e -> Fail e
                 | Return bindings2 ->
                   begin match
                     betree_node_lookup_mut_in_bindings_back key bindings
                       bindings2 with
-                  | Fail -> Fail
+                  | Fail e -> Fail e
                   | Return bindings3 -> Return bindings3
                   end
                 end
@@ -922,34 +925,34 @@ let betree_node_apply_to_leaf_fwd_back
         | BetreeMessageInsert v ->
           begin match
             betree_list_push_front_fwd_back (u64 & u64) bindings0 (key, v) with
-          | Fail -> Fail
+          | Fail e -> Fail e
           | Return bindings1 ->
             begin match
               betree_node_lookup_mut_in_bindings_back key bindings bindings1
               with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return bindings2 -> Return bindings2
             end
           end
         | BetreeMessageDelete ->
           begin match
             betree_node_lookup_mut_in_bindings_back key bindings bindings0 with
-          | Fail -> Fail
+          | Fail e -> Fail e
           | Return bindings1 -> Return bindings1
           end
         | BetreeMessageUpsert s ->
           begin match betree_upsert_update_fwd None s with
-          | Fail -> Fail
+          | Fail e -> Fail e
           | Return v ->
             begin match
               betree_list_push_front_fwd_back (u64 & u64) bindings0 (key, v)
               with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return bindings1 ->
               begin match
                 betree_node_lookup_mut_in_bindings_back key bindings bindings1
                 with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return bindings2 -> Return bindings2
               end
             end
@@ -969,11 +972,11 @@ let rec betree_node_apply_messages_to_leaf_fwd_back
   | BetreeListCons new_msg new_msgs_tl ->
     let (i, m) = new_msg in
     begin match betree_node_apply_to_leaf_fwd_back bindings i m with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return bindings0 ->
       begin match
         betree_node_apply_messages_to_leaf_fwd_back bindings0 new_msgs_tl with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return bindings1 -> Return bindings1
       end
     end
@@ -994,10 +997,10 @@ let rec betree_node_filter_messages_for_key_fwd_back
       begin match
         betree_list_pop_front_back (u64 & betree_message_t) (BetreeListCons (k,
           m) l) with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return msgs0 ->
         begin match betree_node_filter_messages_for_key_fwd_back key msgs0 with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return msgs1 -> Return msgs1
         end
       end
@@ -1018,7 +1021,7 @@ let rec betree_node_lookup_first_message_after_key_fwd
     then
       begin match betree_node_lookup_first_message_after_key_fwd key next_msgs
         with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return l -> Return l
       end
     else Return (BetreeListCons (k, m) next_msgs)
@@ -1039,7 +1042,7 @@ let rec betree_node_lookup_first_message_after_key_back
     then
       begin match
         betree_node_lookup_first_message_after_key_back key next_msgs ret with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return next_msgs0 -> Return (BetreeListCons (k, m) next_msgs0)
       end
     else Return ret
@@ -1053,10 +1056,10 @@ let betree_node_apply_to_internal_fwd_back
   result (betree_list_t (u64 & betree_message_t))
   =
   begin match betree_node_lookup_first_message_for_key_fwd key msgs with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return msgs0 ->
     begin match betree_list_head_has_key_fwd betree_message_t msgs0 key with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return b ->
       if b
       then
@@ -1064,17 +1067,17 @@ let betree_node_apply_to_internal_fwd_back
         | BetreeMessageInsert i ->
           begin match betree_node_filter_messages_for_key_fwd_back key msgs0
             with
-          | Fail -> Fail
+          | Fail e -> Fail e
           | Return msgs1 ->
             begin match
               betree_list_push_front_fwd_back (u64 & betree_message_t) msgs1
                 (key, BetreeMessageInsert i) with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return msgs2 ->
               begin match
                 betree_node_lookup_first_message_for_key_back key msgs msgs2
                 with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return msgs3 -> Return msgs3
               end
             end
@@ -1082,45 +1085,45 @@ let betree_node_apply_to_internal_fwd_back
         | BetreeMessageDelete ->
           begin match betree_node_filter_messages_for_key_fwd_back key msgs0
             with
-          | Fail -> Fail
+          | Fail e -> Fail e
           | Return msgs1 ->
             begin match
               betree_list_push_front_fwd_back (u64 & betree_message_t) msgs1
                 (key, BetreeMessageDelete) with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return msgs2 ->
               begin match
                 betree_node_lookup_first_message_for_key_back key msgs msgs2
                 with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return msgs3 -> Return msgs3
               end
             end
           end
         | BetreeMessageUpsert s ->
           begin match betree_list_hd_fwd (u64 & betree_message_t) msgs0 with
-          | Fail -> Fail
+          | Fail e -> Fail e
           | Return p ->
             let (_, m) = p in
             begin match m with
             | BetreeMessageInsert prev ->
               begin match betree_upsert_update_fwd (Some prev) s with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return v ->
                 begin match
                   betree_list_pop_front_back (u64 & betree_message_t) msgs0
                   with
-                | Fail -> Fail
+                | Fail e -> Fail e
                 | Return msgs1 ->
                   begin match
                     betree_list_push_front_fwd_back (u64 & betree_message_t)
                       msgs1 (key, BetreeMessageInsert v) with
-                  | Fail -> Fail
+                  | Fail e -> Fail e
                   | Return msgs2 ->
                     begin match
                       betree_node_lookup_first_message_for_key_back key msgs
                         msgs2 with
-                    | Fail -> Fail
+                    | Fail e -> Fail e
                     | Return msgs3 -> Return msgs3
                     end
                   end
@@ -1128,22 +1131,22 @@ let betree_node_apply_to_internal_fwd_back
               end
             | BetreeMessageDelete ->
               begin match betree_upsert_update_fwd None s with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return v ->
                 begin match
                   betree_list_pop_front_back (u64 & betree_message_t) msgs0
                   with
-                | Fail -> Fail
+                | Fail e -> Fail e
                 | Return msgs1 ->
                   begin match
                     betree_list_push_front_fwd_back (u64 & betree_message_t)
                       msgs1 (key, BetreeMessageInsert v) with
-                  | Fail -> Fail
+                  | Fail e -> Fail e
                   | Return msgs2 ->
                     begin match
                       betree_node_lookup_first_message_for_key_back key msgs
                         msgs2 with
-                    | Fail -> Fail
+                    | Fail e -> Fail e
                     | Return msgs3 -> Return msgs3
                     end
                   end
@@ -1152,22 +1155,22 @@ let betree_node_apply_to_internal_fwd_back
             | BetreeMessageUpsert ufs ->
               begin match
                 betree_node_lookup_first_message_after_key_fwd key msgs0 with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return msgs1 ->
                 begin match
                   betree_list_push_front_fwd_back (u64 & betree_message_t)
                     msgs1 (key, BetreeMessageUpsert s) with
-                | Fail -> Fail
+                | Fail e -> Fail e
                 | Return msgs2 ->
                   begin match
                     betree_node_lookup_first_message_after_key_back key msgs0
                       msgs2 with
-                  | Fail -> Fail
+                  | Fail e -> Fail e
                   | Return msgs3 ->
                     begin match
                       betree_node_lookup_first_message_for_key_back key msgs
                         msgs3 with
-                    | Fail -> Fail
+                    | Fail e -> Fail e
                     | Return msgs4 -> Return msgs4
                     end
                   end
@@ -1180,11 +1183,11 @@ let betree_node_apply_to_internal_fwd_back
         begin match
           betree_list_push_front_fwd_back (u64 & betree_message_t) msgs0 (key,
             new_msg) with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return msgs1 ->
           begin match
             betree_node_lookup_first_message_for_key_back key msgs msgs1 with
-          | Fail -> Fail
+          | Fail e -> Fail e
           | Return msgs2 -> Return msgs2
           end
         end
@@ -1202,11 +1205,11 @@ let rec betree_node_apply_messages_to_internal_fwd_back
   | BetreeListCons new_msg new_msgs_tl ->
     let (i, m) = new_msg in
     begin match betree_node_apply_to_internal_fwd_back msgs i m with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return msgs0 ->
       begin match
         betree_node_apply_messages_to_internal_fwd_back msgs0 new_msgs_tl with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return msgs1 -> Return msgs1
       end
     end
@@ -1225,31 +1228,31 @@ let rec betree_node_apply_messages_fwd
   begin match self with
   | BetreeNodeInternal node ->
     begin match betree_load_internal_node_fwd node.betree_internal_id st with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return (st0, content) ->
       begin match betree_node_apply_messages_to_internal_fwd_back content msgs
         with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return content0 ->
         begin match betree_list_len_fwd (u64 & betree_message_t) content0 with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return num_msgs ->
           if num_msgs >= params.betree_params_min_flush_size
           then
             begin match
               betree_internal_flush_fwd node params node_id_cnt content0 st0
               with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return (st1, content1) ->
               begin match
                 betree_internal_flush_back'a node params node_id_cnt content0
                   st0 st1 with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return (st2, (node0, _)) ->
                 begin match
                   betree_store_internal_node_fwd node0.betree_internal_id
                     content1 st2 with
-                | Fail -> Fail
+                | Fail e -> Fail e
                 | Return (st3, _) -> Return (st3, ())
                 end
               end
@@ -1258,7 +1261,7 @@ let rec betree_node_apply_messages_fwd
             begin match
               betree_store_internal_node_fwd node.betree_internal_id content0
                 st0 with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return (st1, _) -> Return (st1, ())
             end
         end
@@ -1266,32 +1269,32 @@ let rec betree_node_apply_messages_fwd
     end
   | BetreeNodeLeaf node ->
     begin match betree_load_leaf_node_fwd node.betree_leaf_id st with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return (st0, content) ->
       begin match betree_node_apply_messages_to_leaf_fwd_back content msgs with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return content0 ->
         begin match betree_list_len_fwd (u64 & u64) content0 with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return len ->
           begin match u64_mul 2 params.betree_params_split_size with
-          | Fail -> Fail
+          | Fail e -> Fail e
           | Return i ->
             if len >= i
             then
               begin match
                 betree_leaf_split_fwd node content0 params node_id_cnt st0 with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return (st1, _) ->
                 begin match
                   betree_store_leaf_node_fwd node.betree_leaf_id BetreeListNil
                     st1 with
-                | Fail -> Fail
+                | Fail e -> Fail e
                 | Return (st2, _) ->
                   begin match
                     betree_leaf_split_back0 node content0 params node_id_cnt
                       st0 st2 with
-                  | Fail -> Fail
+                  | Fail e -> Fail e
                   | Return (st3, ()) -> Return (st3, ())
                   end
                 end
@@ -1300,7 +1303,7 @@ let rec betree_node_apply_messages_fwd
               begin match
                 betree_store_leaf_node_fwd node.betree_leaf_id content0 st0
                 with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return (st1, _) -> Return (st1, ())
               end
           end
@@ -1321,31 +1324,31 @@ and betree_node_apply_messages_back'a
   begin match self with
   | BetreeNodeInternal node ->
     begin match betree_load_internal_node_fwd node.betree_internal_id st with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return (st1, content) ->
       begin match betree_node_apply_messages_to_internal_fwd_back content msgs
         with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return content0 ->
         begin match betree_list_len_fwd (u64 & betree_message_t) content0 with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return num_msgs ->
           if num_msgs >= params.betree_params_min_flush_size
           then
             begin match
               betree_internal_flush_fwd node params node_id_cnt content0 st1
               with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return (st2, content1) ->
               begin match
                 betree_internal_flush_back'a node params node_id_cnt content0
                   st1 st2 with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return (st3, (node0, node_id_cnt0)) ->
                 begin match
                   betree_store_internal_node_fwd node0.betree_internal_id
                     content1 st3 with
-                | Fail -> Fail
+                | Fail e -> Fail e
                 | Return (_, _) ->
                   Return (st0, (BetreeNodeInternal node0, node_id_cnt0))
                 end
@@ -1355,7 +1358,7 @@ and betree_node_apply_messages_back'a
             begin match
               betree_store_internal_node_fwd node.betree_internal_id content0
                 st1 with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return (_, _) ->
               Return (st0, (BetreeNodeInternal node, node_id_cnt))
             end
@@ -1364,37 +1367,37 @@ and betree_node_apply_messages_back'a
     end
   | BetreeNodeLeaf node ->
     begin match betree_load_leaf_node_fwd node.betree_leaf_id st with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return (st1, content) ->
       begin match betree_node_apply_messages_to_leaf_fwd_back content msgs with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return content0 ->
         begin match betree_list_len_fwd (u64 & u64) content0 with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return len ->
           begin match u64_mul 2 params.betree_params_split_size with
-          | Fail -> Fail
+          | Fail e -> Fail e
           | Return i ->
             if len >= i
             then
               begin match
                 betree_leaf_split_fwd node content0 params node_id_cnt st1 with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return (st2, new_node) ->
                 begin match
                   betree_store_leaf_node_fwd node.betree_leaf_id BetreeListNil
                     st2 with
-                | Fail -> Fail
+                | Fail e -> Fail e
                 | Return (st3, _) ->
                   begin match
                     betree_leaf_split_back0 node content0 params node_id_cnt
                       st1 st3 with
-                  | Fail -> Fail
+                  | Fail e -> Fail e
                   | Return (_, ()) ->
                     begin match
                       betree_leaf_split_back2 node content0 params node_id_cnt
                         st1 st0 with
-                    | Fail -> Fail
+                    | Fail e -> Fail e
                     | Return (st4, node_id_cnt0) ->
                       Return (st4, (BetreeNodeInternal new_node, node_id_cnt0))
                     end
@@ -1405,7 +1408,7 @@ and betree_node_apply_messages_back'a
               begin match
                 betree_store_leaf_node_fwd node.betree_leaf_id content0 st1
                 with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return (_, _) ->
                 Return (st0, (BetreeNodeLeaf (Mkbetree_leaf_t
                   node.betree_leaf_id len), node_id_cnt))
@@ -1428,36 +1431,36 @@ and betree_node_apply_messages_back1
   begin match self with
   | BetreeNodeInternal node ->
     begin match betree_load_internal_node_fwd node.betree_internal_id st with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return (st1, content) ->
       begin match betree_node_apply_messages_to_internal_fwd_back content msgs
         with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return content0 ->
         begin match betree_list_len_fwd (u64 & betree_message_t) content0 with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return num_msgs ->
           if num_msgs >= params.betree_params_min_flush_size
           then
             begin match
               betree_internal_flush_fwd node params node_id_cnt content0 st1
               with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return (st2, content1) ->
               begin match
                 betree_internal_flush_back'a node params node_id_cnt content0
                   st1 st2 with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return (st3, (node0, _)) ->
                 begin match
                   betree_store_internal_node_fwd node0.betree_internal_id
                     content1 st3 with
-                | Fail -> Fail
+                | Fail e -> Fail e
                 | Return (_, _) ->
                   begin match
                     betree_internal_flush_back1 node params node_id_cnt
                       content0 st1 st0 with
-                  | Fail -> Fail
+                  | Fail e -> Fail e
                   | Return (st4, ()) -> Return (st4, ())
                   end
                 end
@@ -1467,7 +1470,7 @@ and betree_node_apply_messages_back1
             begin match
               betree_store_internal_node_fwd node.betree_internal_id content0
                 st1 with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return (_, _) -> Return (st0, ())
             end
         end
@@ -1475,37 +1478,37 @@ and betree_node_apply_messages_back1
     end
   | BetreeNodeLeaf node ->
     begin match betree_load_leaf_node_fwd node.betree_leaf_id st with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return (st1, content) ->
       begin match betree_node_apply_messages_to_leaf_fwd_back content msgs with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return content0 ->
         begin match betree_list_len_fwd (u64 & u64) content0 with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return len ->
           begin match u64_mul 2 params.betree_params_split_size with
-          | Fail -> Fail
+          | Fail e -> Fail e
           | Return i ->
             if len >= i
             then
               begin match
                 betree_leaf_split_fwd node content0 params node_id_cnt st1 with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return (st2, _) ->
                 begin match
                   betree_store_leaf_node_fwd node.betree_leaf_id BetreeListNil
                     st2 with
-                | Fail -> Fail
+                | Fail e -> Fail e
                 | Return (st3, _) ->
                   begin match
                     betree_leaf_split_back0 node content0 params node_id_cnt
                       st1 st3 with
-                  | Fail -> Fail
+                  | Fail e -> Fail e
                   | Return (_, ()) ->
                     begin match
                       betree_leaf_split_back1 node content0 params node_id_cnt
                         st1 st0 with
-                    | Fail -> Fail
+                    | Fail e -> Fail e
                     | Return (st4, ()) -> Return (st4, ())
                     end
                   end
@@ -1515,7 +1518,7 @@ and betree_node_apply_messages_back1
               begin match
                 betree_store_leaf_node_fwd node.betree_leaf_id content0 st1
                 with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return (_, _) -> Return (st0, ())
               end
           end
@@ -1536,51 +1539,51 @@ and betree_internal_flush_fwd
   begin match
     betree_list_partition_at_pivot_fwd betree_message_t content
       self.betree_internal_pivot with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return p ->
     let (msgs_left, msgs_right) = p in
     begin match betree_list_len_fwd (u64 & betree_message_t) msgs_left with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return len_left ->
       if len_left >= params.betree_params_min_flush_size
       then
         begin match
           betree_node_apply_messages_fwd self.betree_internal_left params
             node_id_cnt msgs_left st with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return (st0, _) ->
           begin match
             betree_node_apply_messages_back'a self.betree_internal_left params
               node_id_cnt msgs_left st st0 with
-          | Fail -> Fail
+          | Fail e -> Fail e
           | Return (st1, (_, node_id_cnt0)) ->
             begin match
               betree_node_apply_messages_back1 self.betree_internal_left params
                 node_id_cnt msgs_left st st1 with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return (st2, ()) ->
               begin match
                 betree_list_len_fwd (u64 & betree_message_t) msgs_right with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return len_right ->
                 if len_right >= params.betree_params_min_flush_size
                 then
                   begin match
                     betree_node_apply_messages_fwd self.betree_internal_right
                       params node_id_cnt0 msgs_right st2 with
-                  | Fail -> Fail
+                  | Fail e -> Fail e
                   | Return (st3, _) ->
                     begin match
                       betree_node_apply_messages_back'a
                         self.betree_internal_right params node_id_cnt0
                         msgs_right st2 st3 with
-                    | Fail -> Fail
+                    | Fail e -> Fail e
                     | Return (st4, (_, _)) ->
                       begin match
                         betree_node_apply_messages_back1
                           self.betree_internal_right params node_id_cnt0
                           msgs_right st2 st4 with
-                      | Fail -> Fail
+                      | Fail e -> Fail e
                       | Return (st5, ()) -> Return (st5, BetreeListNil)
                       end
                     end
@@ -1594,17 +1597,17 @@ and betree_internal_flush_fwd
         begin match
           betree_node_apply_messages_fwd self.betree_internal_right params
             node_id_cnt msgs_right st with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return (st0, _) ->
           begin match
             betree_node_apply_messages_back'a self.betree_internal_right params
               node_id_cnt msgs_right st st0 with
-          | Fail -> Fail
+          | Fail e -> Fail e
           | Return (st1, (_, _)) ->
             begin match
               betree_node_apply_messages_back1 self.betree_internal_right
                 params node_id_cnt msgs_right st st1 with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return (st2, ()) -> Return (st2, msgs_left)
             end
           end
@@ -1624,51 +1627,51 @@ and betree_internal_flush_back'a
   begin match
     betree_list_partition_at_pivot_fwd betree_message_t content
       self.betree_internal_pivot with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return p ->
     let (msgs_left, msgs_right) = p in
     begin match betree_list_len_fwd (u64 & betree_message_t) msgs_left with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return len_left ->
       if len_left >= params.betree_params_min_flush_size
       then
         begin match
           betree_node_apply_messages_fwd self.betree_internal_left params
             node_id_cnt msgs_left st with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return (st1, _) ->
           begin match
             betree_node_apply_messages_back'a self.betree_internal_left params
               node_id_cnt msgs_left st st1 with
-          | Fail -> Fail
+          | Fail e -> Fail e
           | Return (st2, (n, node_id_cnt0)) ->
             begin match
               betree_node_apply_messages_back1 self.betree_internal_left params
                 node_id_cnt msgs_left st st2 with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return (st3, ()) ->
               begin match
                 betree_list_len_fwd (u64 & betree_message_t) msgs_right with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return len_right ->
                 if len_right >= params.betree_params_min_flush_size
                 then
                   begin match
                     betree_node_apply_messages_fwd self.betree_internal_right
                       params node_id_cnt0 msgs_right st3 with
-                  | Fail -> Fail
+                  | Fail e -> Fail e
                   | Return (st4, _) ->
                     begin match
                       betree_node_apply_messages_back'a
                         self.betree_internal_right params node_id_cnt0
                         msgs_right st3 st4 with
-                    | Fail -> Fail
+                    | Fail e -> Fail e
                     | Return (st5, (n0, node_id_cnt1)) ->
                       begin match
                         betree_node_apply_messages_back1
                           self.betree_internal_right params node_id_cnt0
                           msgs_right st3 st5 with
-                      | Fail -> Fail
+                      | Fail e -> Fail e
                       | Return (_, ()) ->
                         Return (st0, (Mkbetree_internal_t
                           self.betree_internal_id self.betree_internal_pivot n
@@ -1688,17 +1691,17 @@ and betree_internal_flush_back'a
         begin match
           betree_node_apply_messages_fwd self.betree_internal_right params
             node_id_cnt msgs_right st with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return (st1, _) ->
           begin match
             betree_node_apply_messages_back'a self.betree_internal_right params
               node_id_cnt msgs_right st st1 with
-          | Fail -> Fail
+          | Fail e -> Fail e
           | Return (st2, (n, node_id_cnt0)) ->
             begin match
               betree_node_apply_messages_back1 self.betree_internal_right
                 params node_id_cnt msgs_right st st2 with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return (_, ()) ->
               Return (st0, (Mkbetree_internal_t self.betree_internal_id
                 self.betree_internal_pivot self.betree_internal_left n,
@@ -1721,51 +1724,51 @@ and betree_internal_flush_back1
   begin match
     betree_list_partition_at_pivot_fwd betree_message_t content
       self.betree_internal_pivot with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return p ->
     let (msgs_left, msgs_right) = p in
     begin match betree_list_len_fwd (u64 & betree_message_t) msgs_left with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return len_left ->
       if len_left >= params.betree_params_min_flush_size
       then
         begin match
           betree_node_apply_messages_fwd self.betree_internal_left params
             node_id_cnt msgs_left st with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return (st1, _) ->
           begin match
             betree_node_apply_messages_back'a self.betree_internal_left params
               node_id_cnt msgs_left st st1 with
-          | Fail -> Fail
+          | Fail e -> Fail e
           | Return (st2, (_, node_id_cnt0)) ->
             begin match
               betree_node_apply_messages_back1 self.betree_internal_left params
                 node_id_cnt msgs_left st st2 with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return (st3, ()) ->
               begin match
                 betree_list_len_fwd (u64 & betree_message_t) msgs_right with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return len_right ->
                 if len_right >= params.betree_params_min_flush_size
                 then
                   begin match
                     betree_node_apply_messages_fwd self.betree_internal_right
                       params node_id_cnt0 msgs_right st3 with
-                  | Fail -> Fail
+                  | Fail e -> Fail e
                   | Return (st4, _) ->
                     begin match
                       betree_node_apply_messages_back'a
                         self.betree_internal_right params node_id_cnt0
                         msgs_right st3 st4 with
-                    | Fail -> Fail
+                    | Fail e -> Fail e
                     | Return (st5, (_, _)) ->
                       begin match
                         betree_node_apply_messages_back1
                           self.betree_internal_right params node_id_cnt0
                           msgs_right st3 st5 with
-                      | Fail -> Fail
+                      | Fail e -> Fail e
                       | Return (_, ()) -> Return (st0, ())
                       end
                     end
@@ -1779,17 +1782,17 @@ and betree_internal_flush_back1
         begin match
           betree_node_apply_messages_fwd self.betree_internal_right params
             node_id_cnt msgs_right st with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return (st1, _) ->
           begin match
             betree_node_apply_messages_back'a self.betree_internal_right params
               node_id_cnt msgs_right st st1 with
-          | Fail -> Fail
+          | Fail e -> Fail e
           | Return (st2, (_, _)) ->
             begin match
               betree_node_apply_messages_back1 self.betree_internal_right
                 params node_id_cnt msgs_right st st2 with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return (_, ()) -> Return (st0, ())
             end
           end
@@ -1808,17 +1811,17 @@ let betree_node_apply_fwd
   begin match
     betree_node_apply_messages_fwd self params node_id_cnt (BetreeListCons
       (key, new_msg) l) st with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return (st0, _) ->
     begin match
       betree_node_apply_messages_back'a self params node_id_cnt (BetreeListCons
         (key, new_msg) l) st st0 with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return (st1, (_, _)) ->
       begin match
         betree_node_apply_messages_back1 self params node_id_cnt
           (BetreeListCons (key, new_msg) l) st st1 with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return (st2, ()) -> Return (st2, ())
       end
     end
@@ -1835,17 +1838,17 @@ let betree_node_apply_back'a
   begin match
     betree_node_apply_messages_fwd self params node_id_cnt (BetreeListCons
       (key, new_msg) l) st with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return (st1, _) ->
     begin match
       betree_node_apply_messages_back'a self params node_id_cnt (BetreeListCons
         (key, new_msg) l) st st1 with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return (st2, (self0, node_id_cnt0)) ->
       begin match
         betree_node_apply_messages_back1 self params node_id_cnt
           (BetreeListCons (key, new_msg) l) st st2 with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return (_, ()) -> Return (st0, (self0, node_id_cnt0))
       end
     end
@@ -1862,17 +1865,17 @@ let betree_node_apply_back1
   begin match
     betree_node_apply_messages_fwd self params node_id_cnt (BetreeListCons
       (key, new_msg) l) st with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return (st1, _) ->
     begin match
       betree_node_apply_messages_back'a self params node_id_cnt (BetreeListCons
         (key, new_msg) l) st st1 with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return (st2, (_, _)) ->
       begin match
         betree_node_apply_messages_back1 self params node_id_cnt
           (BetreeListCons (key, new_msg) l) st st2 with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return (_, ()) -> Return (st0, ())
       end
     end
@@ -1884,16 +1887,16 @@ let betree_be_tree_new_fwd
   result (state & betree_be_tree_t)
   =
   begin match betree_node_id_counter_new_fwd with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return node_id_cnt ->
     begin match betree_node_id_counter_fresh_id_fwd node_id_cnt with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return id ->
       begin match betree_store_leaf_node_fwd id BetreeListNil st with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return (st0, _) ->
         begin match betree_node_id_counter_fresh_id_back node_id_cnt with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return node_id_cnt0 ->
           Return (st0, Mkbetree_be_tree_t (Mkbetree_params_t min_flush_size
             split_size) node_id_cnt0 (BetreeNodeLeaf (Mkbetree_leaf_t id 0)))
@@ -1910,19 +1913,19 @@ let betree_be_tree_apply_fwd
   begin match
     betree_node_apply_fwd self.betree_be_tree_root self.betree_be_tree_params
       self.betree_be_tree_node_id_cnt key msg st with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return (st0, _) ->
     begin match
       betree_node_apply_back'a self.betree_be_tree_root
         self.betree_be_tree_params self.betree_be_tree_node_id_cnt key msg st
         st0 with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return (st1, (_, _)) ->
       begin match
         betree_node_apply_back1 self.betree_be_tree_root
           self.betree_be_tree_params self.betree_be_tree_node_id_cnt key msg st
           st1 with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return (st2, ()) -> Return (st2, ())
       end
     end
@@ -1937,19 +1940,19 @@ let betree_be_tree_apply_back
   begin match
     betree_node_apply_fwd self.betree_be_tree_root self.betree_be_tree_params
       self.betree_be_tree_node_id_cnt key msg st with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return (st1, _) ->
     begin match
       betree_node_apply_back'a self.betree_be_tree_root
         self.betree_be_tree_params self.betree_be_tree_node_id_cnt key msg st
         st1 with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return (st2, (n, nic)) ->
       begin match
         betree_node_apply_back1 self.betree_be_tree_root
           self.betree_be_tree_params self.betree_be_tree_node_id_cnt key msg st
           st2 with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return (_, ()) ->
         Return (st0, Mkbetree_be_tree_t self.betree_be_tree_params nic n)
       end
@@ -1963,12 +1966,12 @@ let betree_be_tree_insert_fwd
   =
   begin match betree_be_tree_apply_fwd self key (BetreeMessageInsert value) st
     with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return (st0, _) ->
     begin match
       betree_be_tree_apply_back self key (BetreeMessageInsert value) st st0
       with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return (st1, _) -> Return (st1, ())
     end
   end
@@ -1981,12 +1984,12 @@ let betree_be_tree_insert_back
   =
   begin match betree_be_tree_apply_fwd self key (BetreeMessageInsert value) st
     with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return (st1, _) ->
     begin match
       betree_be_tree_apply_back self key (BetreeMessageInsert value) st st1
       with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return (_, self0) -> Return (st0, self0)
     end
   end
@@ -1995,11 +1998,11 @@ let betree_be_tree_insert_back
 let betree_be_tree_delete_fwd
   (self : betree_be_tree_t) (key : u64) (st : state) : result (state & unit) =
   begin match betree_be_tree_apply_fwd self key BetreeMessageDelete st with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return (st0, _) ->
     begin match betree_be_tree_apply_back self key BetreeMessageDelete st st0
       with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return (st1, _) -> Return (st1, ())
     end
   end
@@ -2010,11 +2013,11 @@ let betree_be_tree_delete_back
   result (state & betree_be_tree_t)
   =
   begin match betree_be_tree_apply_fwd self key BetreeMessageDelete st with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return (st1, _) ->
     begin match betree_be_tree_apply_back self key BetreeMessageDelete st st1
       with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return (_, self0) -> Return (st0, self0)
     end
   end
@@ -2027,11 +2030,11 @@ let betree_be_tree_upsert_fwd
   =
   begin match betree_be_tree_apply_fwd self key (BetreeMessageUpsert upd) st
     with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return (st0, _) ->
     begin match
       betree_be_tree_apply_back self key (BetreeMessageUpsert upd) st st0 with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return (st1, _) -> Return (st1, ())
     end
   end
@@ -2044,11 +2047,11 @@ let betree_be_tree_upsert_back
   =
   begin match betree_be_tree_apply_fwd self key (BetreeMessageUpsert upd) st
     with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return (st1, _) ->
     begin match
       betree_be_tree_apply_back self key (BetreeMessageUpsert upd) st st1 with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return (_, self0) -> Return (st0, self0)
     end
   end
@@ -2059,7 +2062,7 @@ let betree_be_tree_lookup_fwd
   result (state & (option u64))
   =
   begin match betree_node_lookup_fwd self.betree_be_tree_root key st with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return (st0, opt) -> Return (st0, opt)
   end
 
@@ -2069,7 +2072,7 @@ let betree_be_tree_lookup_back
   result (state & betree_be_tree_t)
   =
   begin match betree_node_lookup_back self.betree_be_tree_root key st st0 with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return (st1, n) ->
     Return (st1, Mkbetree_be_tree_t self.betree_be_tree_params
       self.betree_be_tree_node_id_cnt n)
diff --git a/tests/fstar/betree_back_stateful/Primitives.fst b/tests/fstar/betree_back_stateful/Primitives.fst
index 96138e46..82622656 100644
--- a/tests/fstar/betree_back_stateful/Primitives.fst
+++ b/tests/fstar/betree_back_stateful/Primitives.fst
@@ -18,9 +18,13 @@ let rec list_update #a ls i x =
 #pop-options
 
 (*** Result *)
+type error : Type0 =
+| Failure
+| OutOfFuel
+
 type result (a : Type0) : Type0 =
 | Return : v:a -> result a
-| Fail : result a
+| Fail : e:error -> result a
 
 // Monadic bind and return.
 // Re-definining those allows us to customize the result of the monadic notations
@@ -29,10 +33,10 @@ let return (#a : Type0) (x:a) : result a = Return x
 let bind (#a #b : Type0) (m : result a) (f : a -> result b) : result b =
     match m with
     | Return x -> f x
-    | Fail -> Fail
+    | Fail e -> Fail e
 
 // Monadic assert(...)
-let massert (b:bool) : result unit = if b then Return () else Fail
+let massert (b:bool) : result unit = if b then Return () else Fail Failure
 
 // Normalize and unwrap a successful result (used for globals).
 let eval_global (#a : Type0) (x : result a{Return? (normalize_term x)}) : a = Return?.v x
@@ -119,12 +123,12 @@ let scalar_max (ty : scalar_ty) : int =
 type scalar (ty : scalar_ty) : eqtype = x:int{scalar_min ty <= x && x <= scalar_max ty}
 
 let mk_scalar (ty : scalar_ty) (x : int) : result (scalar ty) =
-  if scalar_min ty <= x && scalar_max ty >= x then Return x else Fail
+  if scalar_min ty <= x && scalar_max ty >= x then Return x else Fail Failure
 
 let scalar_neg (#ty : scalar_ty) (x : scalar ty) : result (scalar ty) = mk_scalar ty (-x)
 
 let scalar_div (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
-  if y <> 0 then mk_scalar ty (x / y) else Fail
+  if y <> 0 then mk_scalar ty (x / y) else Fail Failure
 
 /// The remainder operation
 let int_rem (x : int) (y : int{y <> 0}) : int =
@@ -137,7 +141,7 @@ let _ = assert_norm(int_rem 1 (-2) = 1)
 let _ = assert_norm(int_rem (-1) (-2) = -1)
 
 let scalar_rem (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
-  if y <> 0 then mk_scalar ty (int_rem x y) else Fail
+  if y <> 0 then mk_scalar ty (int_rem x y) else Fail Failure
 
 let scalar_add (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
   mk_scalar ty (x + y)
@@ -258,7 +262,7 @@ let vec_push_back (a  : Type0) (v : vec a) (x : a) :
   (requires True)
   (ensures (fun res ->
     match res with
-    | Fail -> True
+    | Fail e -> e == Failure
     | Return v' -> length v' = length v + 1)) =
   if length v < usize_max then begin
     (**) assert_norm(length [x] == 1);
@@ -266,22 +270,22 @@ let vec_push_back (a  : Type0) (v : vec a) (x : a) :
     (**) assert(length (append v [x]) = length v + 1);
     Return (append v [x])
     end
-  else Fail
+  else Fail Failure
 
 // The **forward** function shouldn't be used
 let vec_insert_fwd (a : Type0) (v : vec a) (i : usize) (x : a) : result unit =
-  if i < length v then Return () else Fail
+  if i < length v then Return () else Fail Failure
 let vec_insert_back (a : Type0) (v : vec a) (i : usize) (x : a) : result (vec a) =
-  if i < length v then Return (list_update v i x) else Fail
+  if i < length v then Return (list_update v i x) else Fail Failure
 
 // The **backward** function shouldn't be used
 let vec_index_fwd (a : Type0) (v : vec a) (i : usize) : result a =
-  if i < length v then Return (index v i) else Fail
+  if i < length v then Return (index v i) else Fail Failure
 let vec_index_back (a : Type0) (v : vec a) (i : usize) (x : a) : result unit =
-  if i < length v then Return () else Fail
+  if i < length v then Return () else Fail Failure
 
 let vec_index_mut_fwd (a : Type0) (v : vec a) (i : usize) : result a =
-  if i < length v then Return (index v i) else Fail
+  if i < length v then Return (index v i) else Fail Failure
 let vec_index_mut_back (a : Type0) (v : vec a) (i : usize) (nx : a) : result (vec a) =
-  if i < length v then Return (list_update v i nx) else Fail
+  if i < length v then Return (list_update v i nx) else Fail Failure
 
diff --git a/tests/fstar/hashmap/Hashmap.Funs.fst b/tests/fstar/hashmap/Hashmap.Funs.fst
index 6e67fca4..e3ae587f 100644
--- a/tests/fstar/hashmap/Hashmap.Funs.fst
+++ b/tests/fstar/hashmap/Hashmap.Funs.fst
@@ -20,13 +20,13 @@ let rec hash_map_allocate_slots_fwd
   then Return slots
   else
     begin match vec_push_back (list_t t) slots ListNil with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return slots0 ->
       begin match usize_sub n 1 with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return i ->
         begin match hash_map_allocate_slots_fwd t slots0 i with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return v -> Return v
         end
       end
@@ -40,13 +40,13 @@ let hash_map_new_with_capacity_fwd
   =
   let v = vec_new (list_t t) in
   begin match hash_map_allocate_slots_fwd t v capacity with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return slots ->
     begin match usize_mul capacity max_load_dividend with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return i ->
       begin match usize_div i max_load_divisor with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return i0 ->
         Return (Mkhash_map_t 0 (max_load_dividend, max_load_divisor) i0 slots)
       end
@@ -56,7 +56,7 @@ let hash_map_new_with_capacity_fwd
 (** [hashmap::HashMap::{0}::new] *)
 let hash_map_new_fwd (t : Type0) : result (hash_map_t t) =
   begin match hash_map_new_with_capacity_fwd t 32 4 5 with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return hm -> Return hm
   end
 
@@ -70,13 +70,13 @@ let rec hash_map_clear_slots_fwd_back
   if i < i0
   then
     begin match vec_index_mut_back (list_t t) slots i ListNil with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return slots0 ->
       begin match usize_add i 1 with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return i1 ->
         begin match hash_map_clear_slots_fwd_back t slots0 i1 with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return slots1 -> Return slots1
         end
       end
@@ -87,7 +87,7 @@ let rec hash_map_clear_slots_fwd_back
 let hash_map_clear_fwd_back
   (t : Type0) (self : hash_map_t t) : result (hash_map_t t) =
   begin match hash_map_clear_slots_fwd_back t self.hash_map_slots 0 with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return v ->
     Return (Mkhash_map_t 0 self.hash_map_max_load_factor self.hash_map_max_load
       v)
@@ -109,7 +109,7 @@ let rec hash_map_insert_in_list_fwd
     then Return false
     else
       begin match hash_map_insert_in_list_fwd t key value ls0 with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return b -> Return b
       end
   | ListNil -> Return true
@@ -127,7 +127,7 @@ let rec hash_map_insert_in_list_back
     then Return (ListCons ckey value ls0)
     else
       begin match hash_map_insert_in_list_back t key value ls0 with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return ls1 -> Return (ListCons ckey cvalue ls1)
       end
   | ListNil -> let l = ListNil in Return (ListCons key value l)
@@ -139,31 +139,31 @@ let hash_map_insert_no_resize_fwd_back
   result (hash_map_t t)
   =
   begin match hash_key_fwd key with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return hash ->
     let i = vec_len (list_t t) self.hash_map_slots in
     begin match usize_rem hash i with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return hash_mod ->
       begin match vec_index_mut_fwd (list_t t) self.hash_map_slots hash_mod
         with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return l ->
         begin match hash_map_insert_in_list_fwd t key value l with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return inserted ->
           if inserted
           then
             begin match usize_add self.hash_map_num_entries 1 with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return i0 ->
               begin match hash_map_insert_in_list_back t key value l with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return l0 ->
                 begin match
                   vec_index_mut_back (list_t t) self.hash_map_slots hash_mod l0
                   with
-                | Fail -> Fail
+                | Fail e -> Fail e
                 | Return v ->
                   Return (Mkhash_map_t i0 self.hash_map_max_load_factor
                     self.hash_map_max_load v)
@@ -172,12 +172,12 @@ let hash_map_insert_no_resize_fwd_back
             end
           else
             begin match hash_map_insert_in_list_back t key value l with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return l0 ->
               begin match
                 vec_index_mut_back (list_t t) self.hash_map_slots hash_mod l0
                 with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return v ->
                 Return (Mkhash_map_t self.hash_map_num_entries
                   self.hash_map_max_load_factor self.hash_map_max_load v)
@@ -201,10 +201,10 @@ let rec hash_map_move_elements_from_list_fwd_back
   begin match ls with
   | ListCons k v tl ->
     begin match hash_map_insert_no_resize_fwd_back t ntable k v with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return ntable0 ->
       begin match hash_map_move_elements_from_list_fwd_back t ntable0 tl with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return ntable1 -> Return ntable1
       end
     end
@@ -221,22 +221,22 @@ let rec hash_map_move_elements_fwd_back
   if i < i0
   then
     begin match vec_index_mut_fwd (list_t t) slots i with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return l ->
       let ls = mem_replace_fwd (list_t t) l ListNil in
       begin match hash_map_move_elements_from_list_fwd_back t ntable ls with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return ntable0 ->
         let l0 = mem_replace_back (list_t t) l ListNil in
         begin match vec_index_mut_back (list_t t) slots i l0 with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return slots0 ->
           begin match usize_add i 1 with
-          | Fail -> Fail
+          | Fail e -> Fail e
           | Return i1 ->
             begin match hash_map_move_elements_fwd_back t ntable0 slots0 i1
               with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return (ntable1, slots1) -> Return (ntable1, slots1)
             end
           end
@@ -249,28 +249,28 @@ let rec hash_map_move_elements_fwd_back
 let hash_map_try_resize_fwd_back
   (t : Type0) (self : hash_map_t t) : result (hash_map_t t) =
   begin match scalar_cast U32 Usize core_num_u32_max_c with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return max_usize ->
     let capacity = vec_len (list_t t) self.hash_map_slots in
     begin match usize_div max_usize 2 with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return n1 ->
       let (i, i0) = self.hash_map_max_load_factor in
       begin match usize_div n1 i with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return i1 ->
         if capacity <= i1
         then
           begin match usize_mul capacity 2 with
-          | Fail -> Fail
+          | Fail e -> Fail e
           | Return i2 ->
             begin match hash_map_new_with_capacity_fwd t i2 i i0 with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return ntable ->
               begin match
                 hash_map_move_elements_fwd_back t ntable self.hash_map_slots 0
                 with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return (ntable0, _) ->
                 Return (Mkhash_map_t self.hash_map_num_entries (i, i0)
                   ntable0.hash_map_max_load ntable0.hash_map_slots)
@@ -290,15 +290,15 @@ let hash_map_insert_fwd_back
   result (hash_map_t t)
   =
   begin match hash_map_insert_no_resize_fwd_back t self key value with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return self0 ->
     begin match hash_map_len_fwd t self0 with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return i ->
       if i > self0.hash_map_max_load
       then
         begin match hash_map_try_resize_fwd_back t self0 with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return self1 -> Return self1
         end
       else Return self0
@@ -317,7 +317,7 @@ let rec hash_map_contains_key_in_list_fwd
     then Return true
     else
       begin match hash_map_contains_key_in_list_fwd t key ls0 with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return b -> Return b
       end
   | ListNil -> Return false
@@ -327,17 +327,17 @@ let rec hash_map_contains_key_in_list_fwd
 let hash_map_contains_key_fwd
   (t : Type0) (self : hash_map_t t) (key : usize) : result bool =
   begin match hash_key_fwd key with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return hash ->
     let i = vec_len (list_t t) self.hash_map_slots in
     begin match usize_rem hash i with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return hash_mod ->
       begin match vec_index_fwd (list_t t) self.hash_map_slots hash_mod with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return l ->
         begin match hash_map_contains_key_in_list_fwd t key l with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return b -> Return b
         end
       end
@@ -355,27 +355,27 @@ let rec hash_map_get_in_list_fwd
     then Return cvalue
     else
       begin match hash_map_get_in_list_fwd t key ls0 with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return x -> Return x
       end
-  | ListNil -> Fail
+  | ListNil -> Fail Failure
   end
 
 (** [hashmap::HashMap::{0}::get] *)
 let hash_map_get_fwd
   (t : Type0) (self : hash_map_t t) (key : usize) : result t =
   begin match hash_key_fwd key with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return hash ->
     let i = vec_len (list_t t) self.hash_map_slots in
     begin match usize_rem hash i with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return hash_mod ->
       begin match vec_index_fwd (list_t t) self.hash_map_slots hash_mod with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return l ->
         begin match hash_map_get_in_list_fwd t key l with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return x -> Return x
         end
       end
@@ -393,10 +393,10 @@ let rec hash_map_get_mut_in_list_fwd
     then Return cvalue
     else
       begin match hash_map_get_mut_in_list_fwd t key ls0 with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return x -> Return x
       end
-  | ListNil -> Fail
+  | ListNil -> Fail Failure
   end
 
 (** [hashmap::HashMap::{0}::get_mut_in_list] *)
@@ -411,28 +411,28 @@ let rec hash_map_get_mut_in_list_back
     then Return (ListCons ckey ret ls0)
     else
       begin match hash_map_get_mut_in_list_back t key ls0 ret with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return ls1 -> Return (ListCons ckey cvalue ls1)
       end
-  | ListNil -> Fail
+  | ListNil -> Fail Failure
   end
 
 (** [hashmap::HashMap::{0}::get_mut] *)
 let hash_map_get_mut_fwd
   (t : Type0) (self : hash_map_t t) (key : usize) : result t =
   begin match hash_key_fwd key with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return hash ->
     let i = vec_len (list_t t) self.hash_map_slots in
     begin match usize_rem hash i with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return hash_mod ->
       begin match vec_index_mut_fwd (list_t t) self.hash_map_slots hash_mod
         with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return l ->
         begin match hash_map_get_mut_in_list_fwd t key l with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return x -> Return x
         end
       end
@@ -445,22 +445,22 @@ let hash_map_get_mut_back
   result (hash_map_t t)
   =
   begin match hash_key_fwd key with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return hash ->
     let i = vec_len (list_t t) self.hash_map_slots in
     begin match usize_rem hash i with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return hash_mod ->
       begin match vec_index_mut_fwd (list_t t) self.hash_map_slots hash_mod
         with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return l ->
         begin match hash_map_get_mut_in_list_back t key l ret with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return l0 ->
           begin match
             vec_index_mut_back (list_t t) self.hash_map_slots hash_mod l0 with
-          | Fail -> Fail
+          | Fail e -> Fail e
           | Return v ->
             Return (Mkhash_map_t self.hash_map_num_entries
               self.hash_map_max_load_factor self.hash_map_max_load v)
@@ -483,11 +483,11 @@ let rec hash_map_remove_from_list_fwd
       let mv_ls = mem_replace_fwd (list_t t) (ListCons ckey x tl) ListNil in
       begin match mv_ls with
       | ListCons i cvalue tl0 -> Return (Some cvalue)
-      | ListNil -> Fail
+      | ListNil -> Fail Failure
       end
     else
       begin match hash_map_remove_from_list_fwd t key tl with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return opt -> Return opt
       end
   | ListNil -> Return None
@@ -506,11 +506,11 @@ let rec hash_map_remove_from_list_back
       let mv_ls = mem_replace_fwd (list_t t) (ListCons ckey x tl) ListNil in
       begin match mv_ls with
       | ListCons i cvalue tl0 -> Return tl0
-      | ListNil -> Fail
+      | ListNil -> Fail Failure
       end
     else
       begin match hash_map_remove_from_list_back t key tl with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return tl0 -> Return (ListCons ckey x tl0)
       end
   | ListNil -> Return ListNil
@@ -520,24 +520,24 @@ let rec hash_map_remove_from_list_back
 let hash_map_remove_fwd
   (t : Type0) (self : hash_map_t t) (key : usize) : result (option t) =
   begin match hash_key_fwd key with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return hash ->
     let i = vec_len (list_t t) self.hash_map_slots in
     begin match usize_rem hash i with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return hash_mod ->
       begin match vec_index_mut_fwd (list_t t) self.hash_map_slots hash_mod
         with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return l ->
         begin match hash_map_remove_from_list_fwd t key l with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return x ->
           begin match x with
           | None -> Return None
           | Some x0 ->
             begin match usize_sub self.hash_map_num_entries 1 with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return _ -> Return (Some x0)
             end
           end
@@ -550,28 +550,28 @@ let hash_map_remove_fwd
 let hash_map_remove_back
   (t : Type0) (self : hash_map_t t) (key : usize) : result (hash_map_t t) =
   begin match hash_key_fwd key with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return hash ->
     let i = vec_len (list_t t) self.hash_map_slots in
     begin match usize_rem hash i with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return hash_mod ->
       begin match vec_index_mut_fwd (list_t t) self.hash_map_slots hash_mod
         with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return l ->
         begin match hash_map_remove_from_list_fwd t key l with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return x ->
           begin match x with
           | None ->
             begin match hash_map_remove_from_list_back t key l with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return l0 ->
               begin match
                 vec_index_mut_back (list_t t) self.hash_map_slots hash_mod l0
                 with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return v ->
                 Return (Mkhash_map_t self.hash_map_num_entries
                   self.hash_map_max_load_factor self.hash_map_max_load v)
@@ -579,15 +579,15 @@ let hash_map_remove_back
             end
           | Some x0 ->
             begin match usize_sub self.hash_map_num_entries 1 with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return i0 ->
               begin match hash_map_remove_from_list_back t key l with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return l0 ->
                 begin match
                   vec_index_mut_back (list_t t) self.hash_map_slots hash_mod l0
                   with
-                | Fail -> Fail
+                | Fail e -> Fail e
                 | Return v ->
                   Return (Mkhash_map_t i0 self.hash_map_max_load_factor
                     self.hash_map_max_load v)
@@ -603,65 +603,65 @@ let hash_map_remove_back
 (** [hashmap::test1] *)
 let test1_fwd : result unit =
   begin match hash_map_new_fwd u64 with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return hm ->
     begin match hash_map_insert_fwd_back u64 hm 0 42 with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return hm0 ->
       begin match hash_map_insert_fwd_back u64 hm0 128 18 with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return hm1 ->
         begin match hash_map_insert_fwd_back u64 hm1 1024 138 with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return hm2 ->
           begin match hash_map_insert_fwd_back u64 hm2 1056 256 with
-          | Fail -> Fail
+          | Fail e -> Fail e
           | Return hm3 ->
             begin match hash_map_get_fwd u64 hm3 128 with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return i ->
               if not (i = 18)
-              then Fail
+              then Fail Failure
               else
                 begin match hash_map_get_mut_back u64 hm3 1024 56 with
-                | Fail -> Fail
+                | Fail e -> Fail e
                 | Return hm4 ->
                   begin match hash_map_get_fwd u64 hm4 1024 with
-                  | Fail -> Fail
+                  | Fail e -> Fail e
                   | Return i0 ->
                     if not (i0 = 56)
-                    then Fail
+                    then Fail Failure
                     else
                       begin match hash_map_remove_fwd u64 hm4 1024 with
-                      | Fail -> Fail
+                      | Fail e -> Fail e
                       | Return x ->
                         begin match x with
-                        | None -> Fail
+                        | None -> Fail Failure
                         | Some x0 ->
                           if not (x0 = 56)
-                          then Fail
+                          then Fail Failure
                           else
                             begin match hash_map_remove_back u64 hm4 1024 with
-                            | Fail -> Fail
+                            | Fail e -> Fail e
                             | Return hm5 ->
                               begin match hash_map_get_fwd u64 hm5 0 with
-                              | Fail -> Fail
+                              | Fail e -> Fail e
                               | Return i1 ->
                                 if not (i1 = 42)
-                                then Fail
+                                then Fail Failure
                                 else
                                   begin match hash_map_get_fwd u64 hm5 128 with
-                                  | Fail -> Fail
+                                  | Fail e -> Fail e
                                   | Return i2 ->
                                     if not (i2 = 18)
-                                    then Fail
+                                    then Fail Failure
                                     else
                                       begin match hash_map_get_fwd u64 hm5 1056
                                         with
-                                      | Fail -> Fail
+                                      | Fail e -> Fail e
                                       | Return i3 ->
                                         if not (i3 = 256)
-                                        then Fail
+                                        then Fail Failure
                                         else Return ()
                                       end
                                   end
diff --git a/tests/fstar/hashmap/Hashmap.Properties.fst b/tests/fstar/hashmap/Hashmap.Properties.fst
index 21a46c73..0713dc7c 100644
--- a/tests/fstar/hashmap/Hashmap.Properties.fst
+++ b/tests/fstar/hashmap/Hashmap.Properties.fst
@@ -502,7 +502,7 @@ val hash_map_allocate_slots_fwd_lem
   (requires (length slots + n <= usize_max))
   (ensures (
    match hash_map_allocate_slots_fwd t slots n with
-   | Fail -> False
+   | Fail _ -> False
    | Return slots' ->
      length slots' = length slots + n /\
      // We leave the already allocated slots unchanged
@@ -517,14 +517,14 @@ let rec hash_map_allocate_slots_fwd_lem t slots n =
   | 0 -> ()
   | _ ->
     begin match vec_push_back (list_t t) slots ListNil with
-    | Fail -> ()
+    | Fail _ -> ()
     | Return slots1 ->
       begin match usize_sub n 1 with
-      | Fail -> ()
+      | Fail _ -> ()
       | Return i ->
         hash_map_allocate_slots_fwd_lem t slots1 i;
         begin match hash_map_allocate_slots_fwd t slots1 i with
-        | Fail -> ()
+        | Fail _ -> ()
         | Return slots2 ->
           assert(length slots1 = length slots + 1);
           assert(slots1 == slots @ [ListNil]); // Triggers patterns
@@ -550,7 +550,7 @@ val hash_map_new_with_capacity_fwd_lem
     capacity * max_load_dividend <= usize_max))
   (ensures (
     match hash_map_new_with_capacity_fwd t capacity max_load_dividend max_load_divisor with
-    | Fail -> False
+    | Fail _ -> False
     | Return hm ->
       // The hash map invariant is satisfied
       hash_map_t_inv hm /\
@@ -574,13 +574,13 @@ let hash_map_new_with_capacity_fwd_lem (t : Type0) (capacity : usize)
   assert(length v = 0);
   hash_map_allocate_slots_fwd_lem t v capacity;
   begin match hash_map_allocate_slots_fwd t v capacity with
-  | Fail -> assert(False)
+  | Fail _ -> assert(False)
   | Return v0 ->
     begin match usize_mul capacity max_load_dividend with
-    | Fail -> assert(False)
+    | Fail _ -> assert(False)
     | Return i ->
       begin match usize_div i max_load_divisor with
-      | Fail -> assert(False)
+      | Fail _ -> assert(False)
       | Return i0 ->
           let hm = Mkhash_map_t 0 (max_load_dividend, max_load_divisor) i0 v0 in
           slots_t_all_nil_inv_lem v0;
@@ -597,7 +597,7 @@ val hash_map_new_fwd_lem_aux (t : Type0) :
   Lemma
   (ensures (
     match hash_map_new_fwd t with
-    | Fail -> False
+    | Fail _ -> False
     | Return hm ->
       // The hash map invariant is satisfied
       hash_map_t_inv hm /\
@@ -610,7 +610,7 @@ val hash_map_new_fwd_lem_aux (t : Type0) :
 let hash_map_new_fwd_lem_aux t =
   hash_map_new_with_capacity_fwd_lem t 32 4 5;
   match hash_map_new_with_capacity_fwd t 32 4 5 with
-  | Fail -> ()
+  | Fail _ -> ()
   | Return hm -> ()
 #pop-options
 
@@ -625,7 +625,7 @@ let rec hash_map_clear_slots_fwd_back_lem
   Lemma
   (ensures (
     match hash_map_clear_slots_fwd_back t slots i with
-    | Fail -> False
+    | Fail _ -> False
     | Return slots' ->
       // The length is preserved
       length slots' == length slots /\
@@ -640,14 +640,14 @@ let rec hash_map_clear_slots_fwd_back_lem
   if b
   then
     begin match vec_index_mut_back (list_t t) slots i ListNil with
-    | Fail -> ()
+    | Fail _ -> ()
     | Return v ->
       begin match usize_add i 1 with
-      | Fail -> ()
+      | Fail _ -> ()
       | Return i1 ->
         hash_map_clear_slots_fwd_back_lem t v i1;
         begin match hash_map_clear_slots_fwd_back t v i1 with
-        | Fail -> ()
+        | Fail _ -> ()
         | Return slots1 ->
           assert(length slots1 == length slots);
           assert(forall (j:nat{i+1 <= j /\ j < length slots}). index slots1 j == ListNil);
@@ -666,7 +666,7 @@ val hash_map_clear_fwd_back_lem_aux
   (requires (hash_map_t_base_inv self))
   (ensures (
     match hash_map_clear_fwd_back t self with
-    | Fail -> False
+    | Fail _ -> False
     | Return hm ->
       // The hash map invariant is satisfied
       hash_map_t_base_inv hm /\
@@ -685,7 +685,7 @@ let hash_map_clear_fwd_back_lem_aux #t self =
   let v = self.hash_map_slots in
   hash_map_clear_slots_fwd_back_lem t v 0;
   begin match hash_map_clear_slots_fwd_back t v 0 with
-  | Fail -> ()
+  | Fail _ -> ()
   | Return slots1 ->
     slots_t_al_v_all_nil_is_empty_lem slots1;
     let hm1 = Mkhash_map_t 0 p i slots1 in
@@ -714,7 +714,7 @@ val hash_map_insert_in_list_fwd_lem
   Lemma
   (ensures (
     match hash_map_insert_in_list_fwd t key value ls with
-    | Fail -> False
+    | Fail _ -> False
     | Return b ->
       b <==> (slot_t_find_s key ls == None)))
   (decreases (hash_map_insert_in_list_decreases t key value ls))
@@ -730,7 +730,7 @@ let rec hash_map_insert_in_list_fwd_lem t key value ls =
       begin
       hash_map_insert_in_list_fwd_lem t key value ls0;
       match hash_map_insert_in_list_fwd t key value ls0 with
-      | Fail -> ()
+      | Fail _ -> ()
       | Return b0 -> ()
       end
   | ListNil ->
@@ -769,7 +769,7 @@ val hash_map_insert_in_list_back_lem_append_s
     slot_t_find_s key ls == None))
   (ensures (
     match hash_map_insert_in_list_back t key value ls with
-    | Fail -> False
+    | Fail _ -> False
     | Return ls' ->
       list_t_v ls' == list_t_v ls @ [(key,value)]))
   (decreases (hash_map_insert_in_list_decreases t key value ls))
@@ -785,7 +785,7 @@ let rec hash_map_insert_in_list_back_lem_append_s t key value ls =
       begin
       hash_map_insert_in_list_back_lem_append_s t key value ls0;
       match hash_map_insert_in_list_back t key value ls0 with
-      | Fail -> ()
+      | Fail _ -> ()
       | Return l -> ()
       end
   | ListNil -> ()
@@ -800,7 +800,7 @@ val hash_map_insert_in_list_back_lem_update_s
     Some? (find (same_key key) (list_t_v ls))))
   (ensures (
     match hash_map_insert_in_list_back t key value ls with
-    | Fail -> False
+    | Fail _ -> False
     | Return ls' ->
       list_t_v ls' == find_update (same_key key) (list_t_v ls) (key,value)))
   (decreases (hash_map_insert_in_list_decreases t key value ls))
@@ -816,7 +816,7 @@ let rec hash_map_insert_in_list_back_lem_update_s t key value ls =
       begin
       hash_map_insert_in_list_back_lem_update_s t key value ls0;
       match hash_map_insert_in_list_back t key value ls0 with
-      | Fail -> ()
+      | Fail _ -> ()
       | Return l -> ()
       end
   | ListNil -> ()
@@ -829,7 +829,7 @@ val hash_map_insert_in_list_back_lem_s
   Lemma
   (ensures (
     match hash_map_insert_in_list_back t key value ls with
-    | Fail -> False
+    | Fail _ -> False
     | Return ls' ->
       list_t_v ls' == hash_map_insert_in_list_s key value (list_t_v ls)))
 
@@ -924,7 +924,7 @@ val hash_map_insert_in_list_back_lem_append
     slot_t_find_s key ls == None))
   (ensures (
     match hash_map_insert_in_list_back t key value ls with
-    | Fail -> False
+    | Fail _ -> False
     | Return ls' ->
       list_t_v ls' == list_t_v ls @ [(key,value)] /\
       // The invariant is preserved
@@ -1044,7 +1044,7 @@ val hash_map_insert_in_list_back_lem_update
     Some? (slot_t_find_s key ls)))
   (ensures (
     match hash_map_insert_in_list_back t key value ls with
-    | Fail -> False
+    | Fail _ -> False
     | Return ls' ->
       let als = list_t_v ls in
       list_t_v ls' == find_update (same_key key) als (key,value) /\
@@ -1096,7 +1096,7 @@ val hash_map_insert_in_list_back_lem
   (requires (slot_t_inv len (hash_mod_key key len) ls))
   (ensures (
     match hash_map_insert_in_list_back t key value ls with
-    | Fail -> False
+    | Fail _ -> False
     | Return ls' ->
       // The invariant is preserved
       slot_t_inv len (hash_mod_key key len) ls' /\
@@ -1145,7 +1145,7 @@ let hash_map_insert_no_resize_s
   result (hash_map_s t) =
   // Check if the table is saturated (too many entries, and we need to insert one)
   let num_entries = length (flatten hm) in
-  if None? (hash_map_s_find hm key) && num_entries = usize_max then Fail
+  if None? (hash_map_s_find hm key) && num_entries = usize_max then Fail Failure
   else Return (hash_map_insert_no_fail_s hm key value)
 
 /// Prove that [hash_map_insert_no_resize_s] is refined by
@@ -1161,7 +1161,7 @@ val hash_map_insert_no_resize_fwd_back_lem_s
     match hash_map_insert_no_resize_fwd_back t self key value,
           hash_map_insert_no_resize_s (hash_map_t_v self) key value
     with
-    | Fail, Fail -> True
+    | Fail _, Fail _ -> True
     | Return hm, Return hm_v ->
       hash_map_t_base_inv hm /\
       hash_map_t_same_params hm self /\
@@ -1172,7 +1172,7 @@ val hash_map_insert_no_resize_fwd_back_lem_s
 
 let hash_map_insert_no_resize_fwd_back_lem_s t self key value =
   begin match hash_key_fwd key with
-  | Fail -> ()
+  | Fail _ -> ()
   | Return i ->
     let i0 = self.hash_map_num_entries in
     let p = self.hash_map_max_load_factor in
@@ -1181,31 +1181,31 @@ let hash_map_insert_no_resize_fwd_back_lem_s t self key value =
     let i2 = vec_len (list_t t) v in
     let len = length v in
     begin match usize_rem i i2 with
-    | Fail -> ()
+    | Fail _ -> ()
     | Return hash_mod ->
       begin match vec_index_mut_fwd (list_t t) v hash_mod with
-      | Fail -> ()
+      | Fail _ -> ()
       | Return l ->
         begin
         // Checking that: list_t_v (index ...) == index (hash_map_t_v ...) ...
         assert(list_t_v l == index (hash_map_t_v self) hash_mod);
         hash_map_insert_in_list_fwd_lem t key value l;
         match hash_map_insert_in_list_fwd t key value l with
-        | Fail -> ()
+        | Fail _ -> ()
         | Return b ->
           assert(b = None? (slot_s_find key (list_t_v l)));
           hash_map_insert_in_list_back_lem t len key value l;
           if b
           then
             begin match usize_add i0 1 with
-            | Fail -> ()
+            | Fail _ -> ()
             | Return i3 ->
               begin
               match hash_map_insert_in_list_back t key value l with
-              | Fail -> ()
+              | Fail _ -> ()
               | Return l0 ->
                 begin match vec_index_mut_back (list_t t) v hash_mod l0 with
-                | Fail -> ()
+                | Fail _ -> ()
                 | Return v0 ->
                   let self_v = hash_map_t_v self in
                   let hm = Mkhash_map_t i3 p i1 v0 in
@@ -1221,10 +1221,10 @@ let hash_map_insert_no_resize_fwd_back_lem_s t self key value =
           else
             begin
             match hash_map_insert_in_list_back t key value l with
-            | Fail -> ()
+            | Fail _ -> ()
             | Return l0 ->
               begin match vec_index_mut_back (list_t t) v hash_mod l0 with
-              | Fail -> ()
+              | Fail _ -> ()
               | Return v0 ->
                 let self_v = hash_map_t_v self in
                 let hm = Mkhash_map_t i0 p i1 v0 in
@@ -1285,7 +1285,7 @@ val hash_map_insert_no_resize_s_lem
   (requires (hash_map_s_inv hm))
   (ensures (
     match hash_map_insert_no_resize_s hm key value with
-    | Fail ->
+    | Fail _ ->
       // Can fail only if we need to create a new binding in
       // an already saturated map
       hash_map_s_len hm = usize_max /\
@@ -1308,7 +1308,7 @@ val hash_map_insert_no_resize_s_get_same_lem
   Lemma (requires (hash_map_s_inv hm))
   (ensures (
     match hash_map_insert_no_resize_s hm key value with
-    | Fail -> True
+    | Fail _ -> True
     | Return hm' ->
       hash_map_s_find hm' key == Some value))
 
@@ -1330,7 +1330,7 @@ val hash_map_insert_no_resize_s_get_diff_lem
   Lemma (requires (hash_map_s_inv hm))
   (ensures (
     match hash_map_insert_no_resize_s hm key value with
-    | Fail -> True
+    | Fail _ -> True
     | Return hm' ->
       hash_map_s_find hm' key' == hash_map_s_find hm key'))
 
@@ -1364,7 +1364,7 @@ let hash_map_insert_no_resize_s_get_diff_lem #t hm key value key' =
 type result_hash_map_s_nes (t : Type0) : Type0 =
   res:result (hash_map_s t) {
     match res with
-    | Fail -> True
+    | Fail _ -> True
     | Return hm -> is_pos_usize (length hm)
   }
 
@@ -1378,7 +1378,7 @@ let rec hash_map_move_elements_from_list_s
   | [] -> Return hm
   | (key, value) :: ls' ->
     match hash_map_insert_no_resize_s hm key value with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return hm' ->
       hash_map_move_elements_from_list_s hm' ls'
 
@@ -1390,7 +1390,7 @@ val hash_map_move_elements_from_list_fwd_back_lem
     match hash_map_move_elements_from_list_fwd_back t ntable ls,
           hash_map_move_elements_from_list_s (hash_map_t_v ntable) (slot_t_v ls)
     with
-    | Fail, Fail -> True
+    | Fail _, Fail _ -> True
     | Return hm', Return hm_v ->
       hash_map_t_base_inv hm' /\
       hash_map_t_v hm' == hm_v /\
@@ -1407,13 +1407,13 @@ let rec hash_map_move_elements_from_list_fwd_back_lem t ntable ls =
     let (_,_) :: tl_v = ls_v in
     hash_map_insert_no_resize_fwd_back_lem_s t ntable k v;
     begin match hash_map_insert_no_resize_fwd_back t ntable k v with
-    | Fail -> ()
+    | Fail _ -> ()
     | Return h ->
       let h_v = Return?.v (hash_map_insert_no_resize_s (hash_map_t_v ntable) k v) in
       assert(hash_map_t_v h == h_v);
       hash_map_move_elements_from_list_fwd_back_lem t h tl;
       begin match hash_map_move_elements_from_list_fwd_back t h tl with
-      | Fail -> ()
+      | Fail _ -> ()
       | Return h0 -> ()
       end
     end
@@ -1450,7 +1450,7 @@ let rec hash_map_move_elements_s_simpl
   (requires (True))
   (ensures (fun res ->
     match res, hash_map_move_elements_fwd_back t ntable slots i with
-    | Fail, Fail -> True
+    | Fail _, Fail _ -> True
     | Return (ntable1, slots1), Return (ntable2, slots2) ->
       ntable1 == ntable2 /\
       slots1 == slots2
@@ -1461,7 +1461,7 @@ let rec hash_map_move_elements_s_simpl
   then
     let slot = index slots i in
     begin match hash_map_move_elements_from_list_fwd_back t ntable slot with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return hm' ->
       let slots' = list_update slots i ListNil in
       hash_map_move_elements_s_simpl t hm' slots' (i+1)
@@ -1487,7 +1487,7 @@ let rec hash_map_move_elements_s
     begin
     let slot = index slots i in
     match hash_map_move_elements_from_list_s hm slot with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return hm' ->
       let slots' = list_update slots i [] in
       hash_map_move_elements_s hm' slots' (i+1)
@@ -1504,7 +1504,7 @@ val hash_map_move_elements_fwd_back_lem_refin
     match hash_map_move_elements_fwd_back t ntable slots i,
           hash_map_move_elements_s (hash_map_t_v ntable) (slots_t_v slots) i
     with
-    | Fail, Fail -> True // We will prove later that this is not possible
+    | Fail _, Fail _ -> True // We will prove later that this is not possible
     | Return (ntable', _), Return ntable'_v ->
       hash_map_t_base_inv ntable' /\
       hash_map_t_v ntable' == ntable'_v /\
@@ -1567,27 +1567,27 @@ let rec hash_map_move_elements_fwd_back_lem_refin t ntable slots i =
   if b
   then
     begin match vec_index_mut_fwd (list_t t) slots i with
-    | Fail -> ()
+    | Fail _ -> ()
     | Return l ->
       let l0 = mem_replace_fwd (list_t t) l ListNil in
       assert(l0 == l);
       hash_map_move_elements_from_list_fwd_back_lem t ntable l0;
       begin match hash_map_move_elements_from_list_fwd_back t ntable l0 with
-      | Fail -> ()
+      | Fail _ -> ()
       | Return h ->
         let l1 = mem_replace_back (list_t t) l ListNil in
         assert(l1 == ListNil);
         assert(slot_t_v #t ListNil == []); // THIS IS IMPORTANT
         begin match vec_index_mut_back (list_t t) slots i l1 with
-        | Fail -> ()
+        | Fail _ -> ()
         | Return v ->
           begin match usize_add i 1 with
-          | Fail -> ()
+          | Fail _ -> ()
           | Return i1 ->
             hash_map_move_elements_fwd_back_lem_refin t h v i1;
             begin match hash_map_move_elements_fwd_back t h v i1 with
-            | Fail ->
-              assert(hash_map_move_elements_fwd_back t ntable slots i == Fail);
+            | Fail _ ->
+              assert(Fail? (hash_map_move_elements_fwd_back t ntable slots i));
               ()
             | Return (ntable', v0) -> ()
             end
@@ -1617,7 +1617,7 @@ let rec hash_map_move_elements_s_flat
   | [] -> Return ntable
   | (k,v) :: slots' ->
     match hash_map_insert_no_resize_s ntable k v with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return ntable' ->
       hash_map_move_elements_s_flat ntable' slots'
 
@@ -1718,7 +1718,7 @@ let rec hash_map_move_elements_from_list_s_as_flat_lem #t hm ls =
   | [] -> ()
   | (key, value) :: ls' ->
     match hash_map_insert_no_resize_s hm key value with
-    | Fail -> ()
+    | Fail _ -> ()
     | Return hm' ->
       hash_map_move_elements_from_list_s_as_flat_lem hm' ls'
 #pop-options
@@ -1728,7 +1728,7 @@ let hash_map_move_elements_s_flat_comp
   (#t : Type0) (hm : hash_map_s_nes t) (slot0 slot1 : slot_s t) :
   Tot (result_hash_map_s_nes t) =
   match hash_map_move_elements_s_flat hm slot0 with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return hm1 -> hash_map_move_elements_s_flat hm1 slot1
 
 /// High-level desc:
@@ -1740,7 +1740,7 @@ val hash_map_move_elements_s_flat_append_lem
     match hash_map_move_elements_s_flat_comp hm slot0 slot1,
           hash_map_move_elements_s_flat hm (slot0 @ slot1)
     with
-    | Fail, Fail -> True
+    | Fail _, Fail _ -> True
     | Return hm1, Return hm2 -> hm1 == hm2
     | _ -> False))
   (decreases (slot0))
@@ -1751,7 +1751,7 @@ let rec hash_map_move_elements_s_flat_append_lem #t hm slot0 slot1 =
   | [] -> ()
   | (k,v) :: slot0' ->
     match hash_map_insert_no_resize_s hm k v with
-    | Fail -> ()
+    | Fail _ -> ()
     | Return hm' ->
       hash_map_move_elements_s_flat_append_lem hm' slot0' slot1
 #pop-options
@@ -1784,7 +1784,7 @@ val hash_map_move_elements_s_lem_refin_flat
     match hash_map_move_elements_s hm slots i,
           hash_map_move_elements_s_flat hm (flatten_i slots i)
     with
-    | Fail, Fail -> True
+    | Fail _, Fail _ -> True
     | Return hm, Return hm' -> hm == hm'
     | _ -> False))
   (decreases (length slots - i))
@@ -1797,10 +1797,10 @@ let rec hash_map_move_elements_s_lem_refin_flat #t hm slots i =
     let slot = index slots i in
     hash_map_move_elements_from_list_s_as_flat_lem hm slot;
     match hash_map_move_elements_from_list_s hm slot with
-    | Fail ->
+    | Fail _ ->
       assert(flatten_i slots i == slot @ flatten_i slots (i+1));
       hash_map_move_elements_s_flat_append_lem hm slot (flatten_i slots (i+1));
-      assert(hash_map_move_elements_s_flat hm (flatten_i slots i) == Fail)
+      assert(Fail? (hash_map_move_elements_s_flat hm (flatten_i slots i)))
     | Return hm' ->
       let slots' = list_update slots i [] in
       flatten_i_same_suffix slots slots' (i+1);
@@ -1859,7 +1859,7 @@ val hash_map_move_elements_s_flat_lem
     hash_map_s_len hm + length al <= usize_max))
   (ensures (
     match hash_map_move_elements_s_flat hm al with
-    | Fail -> False // We can't fail
+    | Fail _ -> False // We can't fail
     | Return hm' ->
       // The invariant is preserved
       hash_map_s_inv hm' /\
@@ -1876,7 +1876,7 @@ let rec hash_map_move_elements_s_flat_lem #t hm al =
   | (k,v) :: al' ->
     hash_map_insert_no_resize_s_lem hm k v;
     match hash_map_insert_no_resize_s hm k v with
-    | Fail -> ()
+    | Fail _ -> ()
     | Return hm' ->
       assert(hash_map_s_inv hm');
       assert(assoc_list_inv al');
@@ -2211,7 +2211,7 @@ let hash_map_move_elements_fwd_back_lem t ntable slots =
   match hash_map_move_elements_fwd_back t ntable slots 0,
         hash_map_move_elements_s ntable_v slots_v 0
   with
-  | Fail, Fail -> ()
+  | Fail _, Fail _ -> ()
   | Return (ntable', _), Return ntable'_v ->
     assert(hash_map_t_base_inv ntable');
     assert(hash_map_t_v ntable' == ntable'_v)
@@ -2222,7 +2222,7 @@ let hash_map_move_elements_fwd_back_lem t ntable slots =
   match hash_map_move_elements_s ntable_v slots_v 0,
         hash_map_move_elements_s_flat ntable_v (flatten_i slots_v 0)
   with
-  | Fail, Fail -> ()
+  | Fail _, Fail _ -> ()
   | Return hm, Return hm' -> assert(hm == hm')
   | _ -> assert(False)
   end;
@@ -2258,10 +2258,10 @@ let hash_map_try_resize_s_simpl
   if capacity <= (usize_max / 2) / divid then
     let ncapacity : usize = capacity * 2 in
     begin match hash_map_new_with_capacity_fwd t ncapacity divid divis with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return ntable ->
       match hash_map_move_elements_fwd_back t ntable hm.hash_map_slots 0 with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return (ntable', _) ->
         let hm =
           { hm with hash_map_slots = ntable'.hash_map_slots;
@@ -2294,7 +2294,7 @@ val hash_map_try_resize_fwd_back_lem_refin
     match hash_map_try_resize_fwd_back t self,
           hash_map_try_resize_s_simpl self
     with
-    | Fail, Fail -> True
+    | Fail _, Fail _ -> True
     | Return hm1, Return hm2 -> hm1 == hm2
     | _ -> False))
 
@@ -2420,7 +2420,7 @@ val hash_map_try_resize_s_simpl_lem (#t : Type0) (hm : hash_map_t t) :
   ))
   (ensures (
     match hash_map_try_resize_s_simpl hm with
-    | Fail -> False
+    | Fail _ -> False
     | Return hm' ->
       // The full invariant is now satisfied (the full invariant is "base
       // invariant" + the map is not overloaded (or can't be resized because
@@ -2442,7 +2442,7 @@ let hash_map_try_resize_s_simpl_lem #t hm =
     new_max_load_lem (hash_map_t_len_s hm) capacity divid divis;
     hash_map_new_with_capacity_fwd_lem t ncapacity divid divis;
     match hash_map_new_with_capacity_fwd t ncapacity divid divis with
-    | Fail -> ()
+    | Fail _ -> ()
     | Return ntable ->
       let slots = hm.hash_map_slots in
       let al = flatten (slots_t_v slots) in
@@ -2461,7 +2461,7 @@ let hash_map_try_resize_s_simpl_lem #t hm =
       assert(forall (k:key). hash_map_t_find_s ntable k  == None);
       hash_map_move_elements_fwd_back_lem t ntable hm.hash_map_slots;
       match hash_map_move_elements_fwd_back t ntable hm.hash_map_slots 0 with
-      | Fail -> ()
+      | Fail _ -> ()
       | Return (ntable', _) ->
         hash_map_is_assoc_list_lem hm;
         assert(hash_map_is_assoc_list hm (hash_map_t_al_v hm));
@@ -2502,7 +2502,7 @@ val hash_map_try_resize_fwd_back_lem (#t : Type0) (hm : hash_map_t t) :
      length hm.hash_map_slots * 2 * dividend > usize_max)))
   (ensures (
     match hash_map_try_resize_fwd_back t hm with
-    | Fail -> False
+    | Fail _ -> False
     | Return hm' ->
       // The full invariant is now satisfied (the full invariant is "base
       // invariant" + the map is not overloaded (or can't be resized because
@@ -2525,7 +2525,7 @@ let hash_map_insert_s
   (#t : Type0) (self : hash_map_t t) (key : usize) (value : t) :
   result (hash_map_t t) =
   match hash_map_insert_no_resize_fwd_back t self key value with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return hm' ->
     if hash_map_t_len_s hm' > hm'.hash_map_max_load then
       hash_map_try_resize_fwd_back t hm'
@@ -2538,7 +2538,7 @@ val hash_map_insert_fwd_back_lem_refin
     match hash_map_insert_fwd_back t self key value,
           hash_map_insert_s self key value
     with
-    | Fail, Fail -> True
+    | Fail _, Fail _ -> True
     | Return hm1, Return hm2 -> hm1 == hm2
     | _ -> False))
 
@@ -2563,7 +2563,7 @@ val hash_map_insert_fwd_back_lem_aux
   Lemma (requires (hash_map_t_inv self))
   (ensures (
     match hash_map_insert_fwd_back t self key value with
-    | Fail ->
+    | Fail _ ->
       // We can fail only if:
       // - the key is not in the map and we need to add it
       // - we are already saturated
@@ -2585,7 +2585,7 @@ let hash_map_insert_fwd_back_lem_aux #t self key value =
   hash_map_insert_no_resize_fwd_back_lem_s t self key value;
   hash_map_insert_no_resize_s_lem (hash_map_t_v self) key value;
   match hash_map_insert_no_resize_fwd_back t self key value with
-  | Fail -> ()
+  | Fail _ -> ()
   | Return hm' ->
     // Expanding the post of [hash_map_insert_no_resize_fwd_back_lem_s]
     let self_v = hash_map_t_v self in
@@ -2634,7 +2634,7 @@ val hash_map_contains_key_in_list_fwd_lem
   Lemma
   (ensures (
     match hash_map_contains_key_in_list_fwd t key ls with
-    | Fail -> False
+    | Fail _ -> False
     | Return b ->
       b = Some? (slot_t_find_s key ls)))
 
@@ -2650,7 +2650,7 @@ let rec hash_map_contains_key_in_list_fwd_lem #t key ls =
       begin
       hash_map_contains_key_in_list_fwd_lem key ls0;
       match hash_map_contains_key_in_list_fwd t key ls0 with
-      | Fail -> ()
+      | Fail _ -> ()
       | Return b0 -> ()
       end
   | ListNil -> ()
@@ -2663,24 +2663,24 @@ val hash_map_contains_key_fwd_lem_aux
   Lemma
   (ensures (
     match hash_map_contains_key_fwd t self key with
-    | Fail -> False
+    | Fail _ -> False
     | Return b -> b = Some? (hash_map_t_find_s self key)))
 
 let hash_map_contains_key_fwd_lem_aux #t self key =
   begin match hash_key_fwd key with
-  | Fail -> ()
+  | Fail _ -> ()
   | Return i ->
     let v = self.hash_map_slots in
     let i0 = vec_len (list_t t) v in
     begin match usize_rem i i0 with
-    | Fail -> ()
+    | Fail _ -> ()
     | Return hash_mod ->
       begin match vec_index_fwd (list_t t) v hash_mod with
-      | Fail -> ()
+      | Fail _ -> ()
       | Return l ->
         hash_map_contains_key_in_list_fwd_lem key l;
         begin match hash_map_contains_key_in_list_fwd t key l with
-        | Fail -> ()
+        | Fail _ -> ()
         | Return b -> ()
         end
       end
@@ -2700,7 +2700,7 @@ val hash_map_get_in_list_fwd_lem
   Lemma
   (ensures (
     match hash_map_get_in_list_fwd t key ls, slot_t_find_s key ls with
-    | Fail, None -> True
+    | Fail _, None -> True
     | Return x, Some x' -> x == x'
     | _ -> False))
 
@@ -2715,7 +2715,7 @@ let rec hash_map_get_in_list_fwd_lem #t key ls =
       begin
       hash_map_get_in_list_fwd_lem key ls0;
       match hash_map_get_in_list_fwd t key ls0 with
-      | Fail -> ()
+      | Fail _ -> ()
       | Return x -> ()
       end
   | ListNil -> ()
@@ -2729,26 +2729,26 @@ val hash_map_get_fwd_lem_aux
   Lemma
   (ensures (
     match hash_map_get_fwd t self key, hash_map_t_find_s self key with
-    | Fail, None -> True
+    | Fail _, None -> True
     | Return x, Some x' -> x == x'
     | _ -> False))
 
 let hash_map_get_fwd_lem_aux #t self key =
   begin match hash_key_fwd key with
-  | Fail -> ()
+  | Fail _ -> ()
   | Return i ->
     let v = self.hash_map_slots in
     let i0 = vec_len (list_t t) v in
     begin match usize_rem i i0 with
-    | Fail -> ()
+    | Fail _ -> ()
     | Return hash_mod ->
       begin match vec_index_fwd (list_t t) v hash_mod with
-      | Fail -> ()
+      | Fail _ -> ()
       | Return l ->
         begin
         hash_map_get_in_list_fwd_lem key l;
         match hash_map_get_in_list_fwd t key l with
-        | Fail -> ()
+        | Fail _ -> ()
         | Return x -> ()
         end
       end
@@ -2768,7 +2768,7 @@ val hash_map_get_mut_in_list_fwd_lem
   Lemma
   (ensures (
     match hash_map_get_mut_in_list_fwd t key ls, slot_t_find_s key ls with
-    | Fail, None -> True
+    | Fail _, None -> True
     | Return x, Some x' -> x == x'
     | _ -> False))
 
@@ -2783,7 +2783,7 @@ let rec hash_map_get_mut_in_list_fwd_lem #t key ls =
       begin
       hash_map_get_mut_in_list_fwd_lem key ls0;
       match hash_map_get_mut_in_list_fwd t key ls0 with
-      | Fail -> ()
+      | Fail _ -> ()
       | Return x -> ()
       end
   | ListNil -> ()
@@ -2797,26 +2797,26 @@ val hash_map_get_mut_fwd_lem_aux
   Lemma
   (ensures (
     match hash_map_get_mut_fwd t self key, hash_map_t_find_s self key with
-    | Fail, None -> True
+    | Fail _, None -> True
     | Return x, Some x' -> x == x'
     | _ -> False))
 
 let hash_map_get_mut_fwd_lem_aux #t self key =
   begin match hash_key_fwd key with
-  | Fail -> ()
+  | Fail _ -> ()
   | Return i ->
     let v = self.hash_map_slots in
     let i0 = vec_len (list_t t) v in
     begin match usize_rem i i0 with
-    | Fail -> ()
+    | Fail _ -> ()
     | Return hash_mod ->
       begin match vec_index_fwd (list_t t) v hash_mod with
-      | Fail -> ()
+      | Fail _ -> ()
       | Return l ->
         begin
         hash_map_get_mut_in_list_fwd_lem key l;
         match hash_map_get_mut_in_list_fwd t key l with
-        | Fail -> ()
+        | Fail _ -> ()
         | Return x -> ()
         end
       end
@@ -2836,7 +2836,7 @@ val hash_map_get_mut_in_list_back_lem
   (requires (Some? (slot_t_find_s key ls)))
   (ensures (
     match hash_map_get_mut_in_list_back t key ls ret with
-    | Fail -> False
+    | Fail _ -> False
     | Return ls' -> list_t_v ls' == find_update (same_key key) (list_t_v ls) (key,ret)
     | _ -> False))
 
@@ -2851,7 +2851,7 @@ let rec hash_map_get_mut_in_list_back_lem #t key ls ret =
       begin
       hash_map_get_mut_in_list_back_lem key ls0 ret;
       match hash_map_get_mut_in_list_back t key ls0 ret with
-      | Fail -> ()
+      | Fail _ -> ()
       | Return l -> let ls1 = ListCons ckey cvalue l in ()
       end
   | ListNil -> ()
@@ -2868,13 +2868,13 @@ val hash_map_get_mut_back_lem_refin
   (requires (Some? (hash_map_t_find_s self key)))
   (ensures (
     match hash_map_get_mut_back t self key ret with
-    | Fail -> False
+    | Fail _ -> False
     | Return hm' ->
       hash_map_t_v hm' == hash_map_insert_no_fail_s (hash_map_t_v self) key ret))
 
 let hash_map_get_mut_back_lem_refin #t self key ret =
   begin match hash_key_fwd key with
-  | Fail -> ()
+  | Fail _ -> ()
   | Return i ->
     let i0 = self.hash_map_num_entries in
     let p = self.hash_map_max_load_factor in
@@ -2882,18 +2882,18 @@ let hash_map_get_mut_back_lem_refin #t self key ret =
     let v = self.hash_map_slots in
     let i2 = vec_len (list_t t) v in
     begin match usize_rem i i2 with
-    | Fail -> ()
+    | Fail _ -> ()
     | Return hash_mod ->
       begin match vec_index_mut_fwd (list_t t) v hash_mod with
-      | Fail -> ()
+      | Fail _ -> ()
       | Return l ->
         begin
         hash_map_get_mut_in_list_back_lem key l ret;
         match hash_map_get_mut_in_list_back t key l ret with
-        | Fail -> ()
+        | Fail _ -> ()
         | Return l0 ->
           begin match vec_index_mut_back (list_t t) v hash_mod l0 with
-          | Fail -> ()
+          | Fail _ -> ()
           | Return v0 -> let self0 = Mkhash_map_t i0 p i1 v0 in ()
           end
         end
@@ -2911,7 +2911,7 @@ val hash_map_get_mut_back_lem_aux
     Some? (hash_map_t_find_s hm key)))
   (ensures (
     match hash_map_get_mut_back t hm key ret with
-    | Fail -> False
+    | Fail _ -> False
     | Return hm' ->
       // Functional spec
       hash_map_t_v hm' == hash_map_insert_no_fail_s (hash_map_t_v hm) key ret /\
@@ -2928,7 +2928,7 @@ let hash_map_get_mut_back_lem_aux #t hm key ret =
   let hm_v = hash_map_t_v hm in
   hash_map_get_mut_back_lem_refin hm key ret;
   match hash_map_get_mut_back t hm key ret with
-  | Fail -> assert(False)
+  | Fail _ -> assert(False)
   | Return hm' ->
     hash_map_insert_no_fail_s_lem hm_v key ret
 
@@ -2942,7 +2942,7 @@ val hash_map_remove_from_list_fwd_lem
   Lemma
   (ensures (
     match hash_map_remove_from_list_fwd t key ls with
-    | Fail -> False
+    | Fail _ -> False
     | Return opt_x ->
       opt_x == slot_t_find_s key ls /\
       (Some? opt_x ==> length (slot_t_v ls) > 0)))
@@ -2963,7 +2963,7 @@ let rec hash_map_remove_from_list_fwd_lem #t key ls =
       begin
       hash_map_remove_from_list_fwd_lem key tl;
       match hash_map_remove_from_list_fwd t key tl with
-      | Fail -> ()
+      | Fail _ -> ()
       | Return opt -> ()
       end
   | ListNil -> ()
@@ -2979,26 +2979,26 @@ val hash_map_remove_fwd_lem_aux
     hash_map_t_inv self))
   (ensures (
     match hash_map_remove_fwd t self key with
-    | Fail -> False
+    | Fail _ -> False
     | Return opt_x -> opt_x == hash_map_t_find_s self key))
 
 let hash_map_remove_fwd_lem_aux #t self key =
   begin match hash_key_fwd key with
-  | Fail -> ()
+  | Fail _ -> ()
   | Return i ->
     let i0 = self.hash_map_num_entries in
     let v = self.hash_map_slots in
     let i1 = vec_len (list_t t) v in
     begin match usize_rem i i1 with
-    | Fail -> ()
+    | Fail _ -> ()
     | Return hash_mod ->
       begin match vec_index_mut_fwd (list_t t) v hash_mod with
-      | Fail -> ()
+      | Fail _ -> ()
       | Return l ->
         begin
         hash_map_remove_from_list_fwd_lem key l;
         match hash_map_remove_from_list_fwd t key l with
-        | Fail -> ()
+        | Fail _ -> ()
         | Return x ->
           begin match x with
           | None -> ()
@@ -3008,7 +3008,7 @@ let hash_map_remove_fwd_lem_aux #t self key =
             assert(length (list_t_v #t l) > 0);
             length_flatten_index (hash_map_t_v self) hash_mod;
             match usize_sub i0 1 with
-            | Fail -> ()
+            | Fail _ -> ()
             | Return _ -> ()
             end
           end
@@ -3036,7 +3036,7 @@ val hash_map_remove_from_list_back_lem_refin
   Lemma
   (ensures (
     match hash_map_remove_from_list_back t key ls with
-    | Fail -> False
+    | Fail _ -> False
     | Return ls' ->
       list_t_v ls' == hash_map_remove_from_list_s key (list_t_v ls) /\
       // The length is decremented, iff the key was in the slot
@@ -3062,7 +3062,7 @@ let rec hash_map_remove_from_list_back_lem_refin #t key ls =
       begin
       hash_map_remove_from_list_back_lem_refin key tl;
       match hash_map_remove_from_list_back t key tl with
-      | Fail -> ()
+      | Fail _ -> ()
       | Return l -> let ls0 = ListCons ckey x l in ()
       end
   | ListNil -> ()
@@ -3089,7 +3089,7 @@ val hash_map_remove_back_lem_refin
     hash_map_t_inv self))
   (ensures (
     match hash_map_remove_back t self key with
-    | Fail -> False
+    | Fail _ -> False
     | Return hm' ->
       hash_map_t_same_params hm' self /\
       hash_map_t_v hm' == hash_map_remove_s (hash_map_t_v self) key /\
@@ -3102,7 +3102,7 @@ val hash_map_remove_back_lem_refin
 
 let hash_map_remove_back_lem_refin #t self key =
   begin match hash_key_fwd key with
-  | Fail -> ()
+  | Fail _ -> ()
   | Return i ->
     let i0 = self.hash_map_num_entries in
     let p = self.hash_map_max_load_factor in
@@ -3110,27 +3110,27 @@ let hash_map_remove_back_lem_refin #t self key =
     let v = self.hash_map_slots in
     let i2 = vec_len (list_t t) v in
     begin match usize_rem i i2 with
-    | Fail -> ()
+    | Fail _ -> ()
     | Return hash_mod ->
       begin match vec_index_mut_fwd (list_t t) v hash_mod with
-      | Fail -> ()
+      | Fail _ -> ()
       | Return l ->
         begin
         hash_map_remove_from_list_fwd_lem key l;
         match hash_map_remove_from_list_fwd t key l with
-        | Fail -> ()
+        | Fail _ -> ()
         | Return x ->
           begin match x with
           | None ->
             begin
             hash_map_remove_from_list_back_lem_refin key l;
             match hash_map_remove_from_list_back t key l with
-            | Fail -> ()
+            | Fail _ -> ()
             | Return l0 ->
               begin
               length_flatten_update (slots_t_v v) hash_mod (list_t_v l0);
               match vec_index_mut_back (list_t t) v hash_mod l0 with
-              | Fail -> ()
+              | Fail _ -> ()
               | Return v0 -> ()
               end
             end
@@ -3140,17 +3140,17 @@ let hash_map_remove_back_lem_refin #t self key =
             assert(length (list_t_v #t l) > 0);
             length_flatten_index (hash_map_t_v self) hash_mod;
             match usize_sub i0 1 with
-            | Fail -> ()
+            | Fail _ -> ()
             | Return i3 ->
               begin
               hash_map_remove_from_list_back_lem_refin key l;
               match hash_map_remove_from_list_back t key l with
-              | Fail -> ()
+              | Fail _ -> ()
               | Return l0 ->
                 begin
                 length_flatten_update (slots_t_v v) hash_mod (list_t_v l0);
                 match vec_index_mut_back (list_t t) v hash_mod l0 with
-                | Fail -> ()
+                | Fail _ -> ()
                 | Return v0 -> ()
                 end
               end
@@ -3224,7 +3224,7 @@ val hash_map_remove_back_lem_aux
   (requires (hash_map_t_inv self))
   (ensures (
     match hash_map_remove_back t self key with
-    | Fail -> False
+    | Fail _ -> False
     | Return hm' ->
       hash_map_t_inv self /\
       hash_map_t_same_params hm' self /\
diff --git a/tests/fstar/hashmap/Hashmap.Properties.fsti b/tests/fstar/hashmap/Hashmap.Properties.fsti
index 756ae687..0a4f0134 100644
--- a/tests/fstar/hashmap/Hashmap.Properties.fsti
+++ b/tests/fstar/hashmap/Hashmap.Properties.fsti
@@ -67,7 +67,7 @@ val hash_map_new_fwd_lem (t : Type0) :
   Lemma
   (ensures (
     match hash_map_new_fwd t with
-    | Fail -> False
+    | Fail _ -> False
     | Return hm ->
       // The hash map invariant is satisfied
       hash_map_t_inv hm /\
@@ -85,7 +85,7 @@ val hash_map_clear_fwd_back_lem
   (requires (hash_map_t_inv self))
   (ensures (
     match hash_map_clear_fwd_back t self with
-    | Fail -> False
+    | Fail _ -> False
     | Return hm ->
       // The hash map invariant is satisfied
       hash_map_t_inv hm /\
@@ -102,7 +102,7 @@ val hash_map_len_fwd_lem (#t : Type0) (self : hash_map_t t) :
   (requires (hash_map_t_inv self))
   (ensures (
     match hash_map_len_fwd t self with
-    | Fail -> False
+    | Fail _ -> False
     | Return l -> l = len_s self))
 
 
@@ -120,7 +120,7 @@ val hash_map_insert_fwd_back_lem
   (requires (hash_map_t_inv self))
   (ensures (
     match hash_map_insert_fwd_back t self key value with
-    | Fail ->
+    | Fail _ ->
       // We can fail only if:
       // - the key is not in the map and we thus need to add it
       None? (find_s self key) /\
@@ -151,7 +151,7 @@ val hash_map_contains_key_fwd_lem
   (requires (hash_map_t_inv self))
   (ensures (
     match hash_map_contains_key_fwd t self key with
-    | Fail -> False
+    | Fail _ -> False
     | Return b -> b = Some? (find_s self key)))
 
 (**** [get'fwd] *)
@@ -163,7 +163,7 @@ val hash_map_get_fwd_lem
   (requires (hash_map_t_inv self))
   (ensures (
     match hash_map_get_fwd t self key, find_s self key with
-    | Fail, None -> True
+    | Fail _, None -> True
     | Return x, Some x' -> x == x'
     | _ -> False))
 
@@ -181,7 +181,7 @@ val hash_map_get_mut_fwd_lem
   (requires (hash_map_t_inv self))
   (ensures (
     match hash_map_get_mut_fwd t self key, find_s self key with
-    | Fail, None -> True
+    | Fail _, None -> True
     | Return x, Some x' -> x == x'
     | _ -> False))
 
@@ -211,7 +211,7 @@ val hash_map_get_mut_back_lem
     Some? (find_s hm key)))
   (ensures (
     match hash_map_get_mut_back t hm key ret with
-    | Fail -> False // Can't fail
+    | Fail _ -> False // Can't fail
     | Return hm' ->
      // The invariant is preserved
      hash_map_t_inv hm' /\
@@ -234,7 +234,7 @@ val hash_map_remove_fwd_lem
   (requires (hash_map_t_inv self))
   (ensures (
     match hash_map_remove_fwd t self key with
-    | Fail -> False
+    | Fail _ -> False
     | Return opt_x -> opt_x == find_s self key))
 
 
@@ -249,7 +249,7 @@ val hash_map_remove_back_lem
   (requires (hash_map_t_inv self))
   (ensures (
     match hash_map_remove_back t self key with
-    | Fail -> False
+    | Fail _ -> False
     | Return hm' ->
       // The invariant is preserved
       hash_map_t_inv self /\
diff --git a/tests/fstar/hashmap/Primitives.fst b/tests/fstar/hashmap/Primitives.fst
index 96138e46..82622656 100644
--- a/tests/fstar/hashmap/Primitives.fst
+++ b/tests/fstar/hashmap/Primitives.fst
@@ -18,9 +18,13 @@ let rec list_update #a ls i x =
 #pop-options
 
 (*** Result *)
+type error : Type0 =
+| Failure
+| OutOfFuel
+
 type result (a : Type0) : Type0 =
 | Return : v:a -> result a
-| Fail : result a
+| Fail : e:error -> result a
 
 // Monadic bind and return.
 // Re-definining those allows us to customize the result of the monadic notations
@@ -29,10 +33,10 @@ let return (#a : Type0) (x:a) : result a = Return x
 let bind (#a #b : Type0) (m : result a) (f : a -> result b) : result b =
     match m with
     | Return x -> f x
-    | Fail -> Fail
+    | Fail e -> Fail e
 
 // Monadic assert(...)
-let massert (b:bool) : result unit = if b then Return () else Fail
+let massert (b:bool) : result unit = if b then Return () else Fail Failure
 
 // Normalize and unwrap a successful result (used for globals).
 let eval_global (#a : Type0) (x : result a{Return? (normalize_term x)}) : a = Return?.v x
@@ -119,12 +123,12 @@ let scalar_max (ty : scalar_ty) : int =
 type scalar (ty : scalar_ty) : eqtype = x:int{scalar_min ty <= x && x <= scalar_max ty}
 
 let mk_scalar (ty : scalar_ty) (x : int) : result (scalar ty) =
-  if scalar_min ty <= x && scalar_max ty >= x then Return x else Fail
+  if scalar_min ty <= x && scalar_max ty >= x then Return x else Fail Failure
 
 let scalar_neg (#ty : scalar_ty) (x : scalar ty) : result (scalar ty) = mk_scalar ty (-x)
 
 let scalar_div (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
-  if y <> 0 then mk_scalar ty (x / y) else Fail
+  if y <> 0 then mk_scalar ty (x / y) else Fail Failure
 
 /// The remainder operation
 let int_rem (x : int) (y : int{y <> 0}) : int =
@@ -137,7 +141,7 @@ let _ = assert_norm(int_rem 1 (-2) = 1)
 let _ = assert_norm(int_rem (-1) (-2) = -1)
 
 let scalar_rem (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
-  if y <> 0 then mk_scalar ty (int_rem x y) else Fail
+  if y <> 0 then mk_scalar ty (int_rem x y) else Fail Failure
 
 let scalar_add (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
   mk_scalar ty (x + y)
@@ -258,7 +262,7 @@ let vec_push_back (a  : Type0) (v : vec a) (x : a) :
   (requires True)
   (ensures (fun res ->
     match res with
-    | Fail -> True
+    | Fail e -> e == Failure
     | Return v' -> length v' = length v + 1)) =
   if length v < usize_max then begin
     (**) assert_norm(length [x] == 1);
@@ -266,22 +270,22 @@ let vec_push_back (a  : Type0) (v : vec a) (x : a) :
     (**) assert(length (append v [x]) = length v + 1);
     Return (append v [x])
     end
-  else Fail
+  else Fail Failure
 
 // The **forward** function shouldn't be used
 let vec_insert_fwd (a : Type0) (v : vec a) (i : usize) (x : a) : result unit =
-  if i < length v then Return () else Fail
+  if i < length v then Return () else Fail Failure
 let vec_insert_back (a : Type0) (v : vec a) (i : usize) (x : a) : result (vec a) =
-  if i < length v then Return (list_update v i x) else Fail
+  if i < length v then Return (list_update v i x) else Fail Failure
 
 // The **backward** function shouldn't be used
 let vec_index_fwd (a : Type0) (v : vec a) (i : usize) : result a =
-  if i < length v then Return (index v i) else Fail
+  if i < length v then Return (index v i) else Fail Failure
 let vec_index_back (a : Type0) (v : vec a) (i : usize) (x : a) : result unit =
-  if i < length v then Return () else Fail
+  if i < length v then Return () else Fail Failure
 
 let vec_index_mut_fwd (a : Type0) (v : vec a) (i : usize) : result a =
-  if i < length v then Return (index v i) else Fail
+  if i < length v then Return (index v i) else Fail Failure
 let vec_index_mut_back (a : Type0) (v : vec a) (i : usize) (nx : a) : result (vec a) =
-  if i < length v then Return (list_update v i nx) else Fail
+  if i < length v then Return (list_update v i nx) else Fail Failure
 
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
index 82b44dbd..d6da4562 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
@@ -21,13 +21,13 @@ let rec hashmap_hash_map_allocate_slots_fwd
   then Return slots
   else
     begin match vec_push_back (hashmap_list_t t) slots HashmapListNil with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return slots0 ->
       begin match usize_sub n 1 with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return i ->
         begin match hashmap_hash_map_allocate_slots_fwd t slots0 i with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return v -> Return v
         end
       end
@@ -41,13 +41,13 @@ let hashmap_hash_map_new_with_capacity_fwd
   =
   let v = vec_new (hashmap_list_t t) in
   begin match hashmap_hash_map_allocate_slots_fwd t v capacity with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return slots ->
     begin match usize_mul capacity max_load_dividend with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return i ->
       begin match usize_div i max_load_divisor with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return i0 ->
         Return (Mkhashmap_hash_map_t 0 (max_load_dividend, max_load_divisor) i0
           slots)
@@ -58,7 +58,7 @@ let hashmap_hash_map_new_with_capacity_fwd
 (** [hashmap_main::hashmap::HashMap::{0}::new] *)
 let hashmap_hash_map_new_fwd (t : Type0) : result (hashmap_hash_map_t t) =
   begin match hashmap_hash_map_new_with_capacity_fwd t 32 4 5 with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return hm -> Return hm
   end
 
@@ -73,13 +73,13 @@ let rec hashmap_hash_map_clear_slots_fwd_back
   then
     begin match vec_index_mut_back (hashmap_list_t t) slots i HashmapListNil
       with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return slots0 ->
       begin match usize_add i 1 with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return i1 ->
         begin match hashmap_hash_map_clear_slots_fwd_back t slots0 i1 with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return slots1 -> Return slots1
         end
       end
@@ -91,7 +91,7 @@ let hashmap_hash_map_clear_fwd_back
   (t : Type0) (self : hashmap_hash_map_t t) : result (hashmap_hash_map_t t) =
   begin match
     hashmap_hash_map_clear_slots_fwd_back t self.hashmap_hash_map_slots 0 with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return v ->
     Return (Mkhashmap_hash_map_t 0 self.hashmap_hash_map_max_load_factor
       self.hashmap_hash_map_max_load v)
@@ -114,7 +114,7 @@ let rec hashmap_hash_map_insert_in_list_fwd
     then Return false
     else
       begin match hashmap_hash_map_insert_in_list_fwd t key value ls0 with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return b -> Return b
       end
   | HashmapListNil -> Return true
@@ -132,7 +132,7 @@ let rec hashmap_hash_map_insert_in_list_back
     then Return (HashmapListCons ckey value ls0)
     else
       begin match hashmap_hash_map_insert_in_list_back t key value ls0 with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return ls1 -> Return (HashmapListCons ckey cvalue ls1)
       end
   | HashmapListNil ->
@@ -145,33 +145,33 @@ let hashmap_hash_map_insert_no_resize_fwd_back
   result (hashmap_hash_map_t t)
   =
   begin match hashmap_hash_key_fwd key with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return hash ->
     let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
     begin match usize_rem hash i with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return hash_mod ->
       begin match
         vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots
           hash_mod with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return l ->
         begin match hashmap_hash_map_insert_in_list_fwd t key value l with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return inserted ->
           if inserted
           then
             begin match usize_add self.hashmap_hash_map_num_entries 1 with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return i0 ->
               begin match hashmap_hash_map_insert_in_list_back t key value l
                 with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return l0 ->
                 begin match
                   vec_index_mut_back (hashmap_list_t t)
                     self.hashmap_hash_map_slots hash_mod l0 with
-                | Fail -> Fail
+                | Fail e -> Fail e
                 | Return v ->
                   Return (Mkhashmap_hash_map_t i0
                     self.hashmap_hash_map_max_load_factor
@@ -181,12 +181,12 @@ let hashmap_hash_map_insert_no_resize_fwd_back
             end
           else
             begin match hashmap_hash_map_insert_in_list_back t key value l with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return l0 ->
               begin match
                 vec_index_mut_back (hashmap_list_t t)
                   self.hashmap_hash_map_slots hash_mod l0 with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return v ->
                 Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries
                   self.hashmap_hash_map_max_load_factor
@@ -211,11 +211,11 @@ let rec hashmap_hash_map_move_elements_from_list_fwd_back
   begin match ls with
   | HashmapListCons k v tl ->
     begin match hashmap_hash_map_insert_no_resize_fwd_back t ntable k v with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return ntable0 ->
       begin match
         hashmap_hash_map_move_elements_from_list_fwd_back t ntable0 tl with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return ntable1 -> Return ntable1
       end
     end
@@ -233,23 +233,23 @@ let rec hashmap_hash_map_move_elements_fwd_back
   if i < i0
   then
     begin match vec_index_mut_fwd (hashmap_list_t t) slots i with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return l ->
       let ls = mem_replace_fwd (hashmap_list_t t) l HashmapListNil in
       begin match hashmap_hash_map_move_elements_from_list_fwd_back t ntable ls
         with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return ntable0 ->
         let l0 = mem_replace_back (hashmap_list_t t) l HashmapListNil in
         begin match vec_index_mut_back (hashmap_list_t t) slots i l0 with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return slots0 ->
           begin match usize_add i 1 with
-          | Fail -> Fail
+          | Fail e -> Fail e
           | Return i1 ->
             begin match
               hashmap_hash_map_move_elements_fwd_back t ntable0 slots0 i1 with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return (ntable1, slots1) -> Return (ntable1, slots1)
             end
           end
@@ -262,28 +262,28 @@ let rec hashmap_hash_map_move_elements_fwd_back
 let hashmap_hash_map_try_resize_fwd_back
   (t : Type0) (self : hashmap_hash_map_t t) : result (hashmap_hash_map_t t) =
   begin match scalar_cast U32 Usize core_num_u32_max_c with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return max_usize ->
     let capacity = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
     begin match usize_div max_usize 2 with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return n1 ->
       let (i, i0) = self.hashmap_hash_map_max_load_factor in
       begin match usize_div n1 i with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return i1 ->
         if capacity <= i1
         then
           begin match usize_mul capacity 2 with
-          | Fail -> Fail
+          | Fail e -> Fail e
           | Return i2 ->
             begin match hashmap_hash_map_new_with_capacity_fwd t i2 i i0 with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return ntable ->
               begin match
                 hashmap_hash_map_move_elements_fwd_back t ntable
                   self.hashmap_hash_map_slots 0 with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return (ntable0, _) ->
                 Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries
                   (i, i0) ntable0.hashmap_hash_map_max_load
@@ -304,15 +304,15 @@ let hashmap_hash_map_insert_fwd_back
   result (hashmap_hash_map_t t)
   =
   begin match hashmap_hash_map_insert_no_resize_fwd_back t self key value with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return self0 ->
     begin match hashmap_hash_map_len_fwd t self0 with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return i ->
       if i > self0.hashmap_hash_map_max_load
       then
         begin match hashmap_hash_map_try_resize_fwd_back t self0 with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return self1 -> Return self1
         end
       else Return self0
@@ -331,7 +331,7 @@ let rec hashmap_hash_map_contains_key_in_list_fwd
     then Return true
     else
       begin match hashmap_hash_map_contains_key_in_list_fwd t key ls0 with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return b -> Return b
       end
   | HashmapListNil -> Return false
@@ -341,19 +341,19 @@ let rec hashmap_hash_map_contains_key_in_list_fwd
 let hashmap_hash_map_contains_key_fwd
   (t : Type0) (self : hashmap_hash_map_t t) (key : usize) : result bool =
   begin match hashmap_hash_key_fwd key with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return hash ->
     let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
     begin match usize_rem hash i with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return hash_mod ->
       begin match
         vec_index_fwd (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod
         with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return l ->
         begin match hashmap_hash_map_contains_key_in_list_fwd t key l with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return b -> Return b
         end
       end
@@ -371,29 +371,29 @@ let rec hashmap_hash_map_get_in_list_fwd
     then Return cvalue
     else
       begin match hashmap_hash_map_get_in_list_fwd t key ls0 with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return x -> Return x
       end
-  | HashmapListNil -> Fail
+  | HashmapListNil -> Fail Failure
   end
 
 (** [hashmap_main::hashmap::HashMap::{0}::get] *)
 let hashmap_hash_map_get_fwd
   (t : Type0) (self : hashmap_hash_map_t t) (key : usize) : result t =
   begin match hashmap_hash_key_fwd key with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return hash ->
     let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
     begin match usize_rem hash i with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return hash_mod ->
       begin match
         vec_index_fwd (hashmap_list_t t) self.hashmap_hash_map_slots hash_mod
         with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return l ->
         begin match hashmap_hash_map_get_in_list_fwd t key l with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return x -> Return x
         end
       end
@@ -412,10 +412,10 @@ let rec hashmap_hash_map_get_mut_in_list_fwd
     then Return cvalue
     else
       begin match hashmap_hash_map_get_mut_in_list_fwd t key ls0 with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return x -> Return x
       end
-  | HashmapListNil -> Fail
+  | HashmapListNil -> Fail Failure
   end
 
 (** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
@@ -430,29 +430,29 @@ let rec hashmap_hash_map_get_mut_in_list_back
     then Return (HashmapListCons ckey ret ls0)
     else
       begin match hashmap_hash_map_get_mut_in_list_back t key ls0 ret with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return ls1 -> Return (HashmapListCons ckey cvalue ls1)
       end
-  | HashmapListNil -> Fail
+  | HashmapListNil -> Fail Failure
   end
 
 (** [hashmap_main::hashmap::HashMap::{0}::get_mut] *)
 let hashmap_hash_map_get_mut_fwd
   (t : Type0) (self : hashmap_hash_map_t t) (key : usize) : result t =
   begin match hashmap_hash_key_fwd key with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return hash ->
     let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
     begin match usize_rem hash i with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return hash_mod ->
       begin match
         vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots
           hash_mod with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return l ->
         begin match hashmap_hash_map_get_mut_in_list_fwd t key l with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return x -> Return x
         end
       end
@@ -465,24 +465,24 @@ let hashmap_hash_map_get_mut_back
   result (hashmap_hash_map_t t)
   =
   begin match hashmap_hash_key_fwd key with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return hash ->
     let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
     begin match usize_rem hash i with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return hash_mod ->
       begin match
         vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots
           hash_mod with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return l ->
         begin match hashmap_hash_map_get_mut_in_list_back t key l ret with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return l0 ->
           begin match
             vec_index_mut_back (hashmap_list_t t) self.hashmap_hash_map_slots
               hash_mod l0 with
-          | Fail -> Fail
+          | Fail e -> Fail e
           | Return v ->
             Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries
               self.hashmap_hash_map_max_load_factor
@@ -508,11 +508,11 @@ let rec hashmap_hash_map_remove_from_list_fwd
           HashmapListNil in
       begin match mv_ls with
       | HashmapListCons i cvalue tl0 -> Return (Some cvalue)
-      | HashmapListNil -> Fail
+      | HashmapListNil -> Fail Failure
       end
     else
       begin match hashmap_hash_map_remove_from_list_fwd t key tl with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return opt -> Return opt
       end
   | HashmapListNil -> Return None
@@ -533,11 +533,11 @@ let rec hashmap_hash_map_remove_from_list_back
           HashmapListNil in
       begin match mv_ls with
       | HashmapListCons i cvalue tl0 -> Return tl0
-      | HashmapListNil -> Fail
+      | HashmapListNil -> Fail Failure
       end
     else
       begin match hashmap_hash_map_remove_from_list_back t key tl with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return tl0 -> Return (HashmapListCons ckey x tl0)
       end
   | HashmapListNil -> Return HashmapListNil
@@ -547,25 +547,25 @@ let rec hashmap_hash_map_remove_from_list_back
 let hashmap_hash_map_remove_fwd
   (t : Type0) (self : hashmap_hash_map_t t) (key : usize) : result (option t) =
   begin match hashmap_hash_key_fwd key with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return hash ->
     let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
     begin match usize_rem hash i with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return hash_mod ->
       begin match
         vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots
           hash_mod with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return l ->
         begin match hashmap_hash_map_remove_from_list_fwd t key l with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return x ->
           begin match x with
           | None -> Return None
           | Some x0 ->
             begin match usize_sub self.hashmap_hash_map_num_entries 1 with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return _ -> Return (Some x0)
             end
           end
@@ -580,29 +580,29 @@ let hashmap_hash_map_remove_back
   result (hashmap_hash_map_t t)
   =
   begin match hashmap_hash_key_fwd key with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return hash ->
     let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
     begin match usize_rem hash i with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return hash_mod ->
       begin match
         vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots
           hash_mod with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return l ->
         begin match hashmap_hash_map_remove_from_list_fwd t key l with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return x ->
           begin match x with
           | None ->
             begin match hashmap_hash_map_remove_from_list_back t key l with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return l0 ->
               begin match
                 vec_index_mut_back (hashmap_list_t t)
                   self.hashmap_hash_map_slots hash_mod l0 with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return v ->
                 Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries
                   self.hashmap_hash_map_max_load_factor
@@ -611,15 +611,15 @@ let hashmap_hash_map_remove_back
             end
           | Some x0 ->
             begin match usize_sub self.hashmap_hash_map_num_entries 1 with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return i0 ->
               begin match hashmap_hash_map_remove_from_list_back t key l with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return l0 ->
                 begin match
                   vec_index_mut_back (hashmap_list_t t)
                     self.hashmap_hash_map_slots hash_mod l0 with
-                | Fail -> Fail
+                | Fail e -> Fail e
                 | Return v ->
                   Return (Mkhashmap_hash_map_t i0
                     self.hashmap_hash_map_max_load_factor
@@ -636,69 +636,69 @@ let hashmap_hash_map_remove_back
 (** [hashmap_main::hashmap::test1] *)
 let hashmap_test1_fwd : result unit =
   begin match hashmap_hash_map_new_fwd u64 with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return hm ->
     begin match hashmap_hash_map_insert_fwd_back u64 hm 0 42 with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return hm0 ->
       begin match hashmap_hash_map_insert_fwd_back u64 hm0 128 18 with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return hm1 ->
         begin match hashmap_hash_map_insert_fwd_back u64 hm1 1024 138 with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return hm2 ->
           begin match hashmap_hash_map_insert_fwd_back u64 hm2 1056 256 with
-          | Fail -> Fail
+          | Fail e -> Fail e
           | Return hm3 ->
             begin match hashmap_hash_map_get_fwd u64 hm3 128 with
-            | Fail -> Fail
+            | Fail e -> Fail e
             | Return i ->
               if not (i = 18)
-              then Fail
+              then Fail Failure
               else
                 begin match hashmap_hash_map_get_mut_back u64 hm3 1024 56 with
-                | Fail -> Fail
+                | Fail e -> Fail e
                 | Return hm4 ->
                   begin match hashmap_hash_map_get_fwd u64 hm4 1024 with
-                  | Fail -> Fail
+                  | Fail e -> Fail e
                   | Return i0 ->
                     if not (i0 = 56)
-                    then Fail
+                    then Fail Failure
                     else
                       begin match hashmap_hash_map_remove_fwd u64 hm4 1024 with
-                      | Fail -> Fail
+                      | Fail e -> Fail e
                       | Return x ->
                         begin match x with
-                        | None -> Fail
+                        | None -> Fail Failure
                         | Some x0 ->
                           if not (x0 = 56)
-                          then Fail
+                          then Fail Failure
                           else
                             begin match
                               hashmap_hash_map_remove_back u64 hm4 1024 with
-                            | Fail -> Fail
+                            | Fail e -> Fail e
                             | Return hm5 ->
                               begin match hashmap_hash_map_get_fwd u64 hm5 0
                                 with
-                              | Fail -> Fail
+                              | Fail e -> Fail e
                               | Return i1 ->
                                 if not (i1 = 42)
-                                then Fail
+                                then Fail Failure
                                 else
                                   begin match
                                     hashmap_hash_map_get_fwd u64 hm5 128 with
-                                  | Fail -> Fail
+                                  | Fail e -> Fail e
                                   | Return i2 ->
                                     if not (i2 = 18)
-                                    then Fail
+                                    then Fail Failure
                                     else
                                       begin match
                                         hashmap_hash_map_get_fwd u64 hm5 1056
                                         with
-                                      | Fail -> Fail
+                                      | Fail e -> Fail e
                                       | Return i3 ->
                                         if not (i3 = 256)
-                                        then Fail
+                                        then Fail Failure
                                         else Return ()
                                       end
                                   end
@@ -722,13 +722,13 @@ let _ = assert_norm (hashmap_test1_fwd = Return ())
 let insert_on_disk_fwd
   (key : usize) (value : u64) (st : state) : result (state & unit) =
   begin match hashmap_utils_deserialize_fwd st with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return (st0, hm) ->
     begin match hashmap_hash_map_insert_fwd_back u64 hm key value with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return hm0 ->
       begin match hashmap_utils_serialize_fwd hm0 st0 with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return (st1, _) -> Return (st1, ())
       end
     end
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Properties.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Properties.fst
index 4df039a8..106fe05a 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Properties.fst
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Properties.fst
@@ -19,7 +19,7 @@ val state_v : state -> hashmap_hash_map_t u64
 assume
 val serialize_lem (hm : hashmap_hash_map_t u64) (st : state) : Lemma (
   match hashmap_utils_serialize_fwd hm st with
-  | Fail -> True
+  | Fail _ -> True
   | Return (st', ()) -> state_v st' == hm)
   [SMTPat (hashmap_utils_serialize_fwd hm st)]
 
@@ -27,7 +27,7 @@ val serialize_lem (hm : hashmap_hash_map_t u64) (st : state) : Lemma (
 assume
 val deserialize_lem (st : state) : Lemma (
   match hashmap_utils_deserialize_fwd st with
-  | Fail -> True
+  | Fail _ -> True
   | Return (st', hm) -> hm == state_v st /\ st' == st)
   [SMTPat (hashmap_utils_deserialize_fwd st)]
 
@@ -38,11 +38,11 @@ val deserialize_lem (st : state) : Lemma (
 /// in the hash map previously stored on disk.
 val insert_on_disk_fwd_lem (key : usize) (value : u64) (st : state) : Lemma (
   match insert_on_disk_fwd key value st with
-  | Fail -> True
+  | Fail _ -> True
   | Return (st', ()) ->
     let hm = state_v st in
     match hashmap_hash_map_insert_fwd_back u64 hm key value with
-    | Fail -> False
+    | Fail _ -> False
     | Return hm' -> hm' == state_v st')
 
 let insert_on_disk_fwd_lem key value st = ()
diff --git a/tests/fstar/hashmap_on_disk/Primitives.fst b/tests/fstar/hashmap_on_disk/Primitives.fst
index 96138e46..82622656 100644
--- a/tests/fstar/hashmap_on_disk/Primitives.fst
+++ b/tests/fstar/hashmap_on_disk/Primitives.fst
@@ -18,9 +18,13 @@ let rec list_update #a ls i x =
 #pop-options
 
 (*** Result *)
+type error : Type0 =
+| Failure
+| OutOfFuel
+
 type result (a : Type0) : Type0 =
 | Return : v:a -> result a
-| Fail : result a
+| Fail : e:error -> result a
 
 // Monadic bind and return.
 // Re-definining those allows us to customize the result of the monadic notations
@@ -29,10 +33,10 @@ let return (#a : Type0) (x:a) : result a = Return x
 let bind (#a #b : Type0) (m : result a) (f : a -> result b) : result b =
     match m with
     | Return x -> f x
-    | Fail -> Fail
+    | Fail e -> Fail e
 
 // Monadic assert(...)
-let massert (b:bool) : result unit = if b then Return () else Fail
+let massert (b:bool) : result unit = if b then Return () else Fail Failure
 
 // Normalize and unwrap a successful result (used for globals).
 let eval_global (#a : Type0) (x : result a{Return? (normalize_term x)}) : a = Return?.v x
@@ -119,12 +123,12 @@ let scalar_max (ty : scalar_ty) : int =
 type scalar (ty : scalar_ty) : eqtype = x:int{scalar_min ty <= x && x <= scalar_max ty}
 
 let mk_scalar (ty : scalar_ty) (x : int) : result (scalar ty) =
-  if scalar_min ty <= x && scalar_max ty >= x then Return x else Fail
+  if scalar_min ty <= x && scalar_max ty >= x then Return x else Fail Failure
 
 let scalar_neg (#ty : scalar_ty) (x : scalar ty) : result (scalar ty) = mk_scalar ty (-x)
 
 let scalar_div (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
-  if y <> 0 then mk_scalar ty (x / y) else Fail
+  if y <> 0 then mk_scalar ty (x / y) else Fail Failure
 
 /// The remainder operation
 let int_rem (x : int) (y : int{y <> 0}) : int =
@@ -137,7 +141,7 @@ let _ = assert_norm(int_rem 1 (-2) = 1)
 let _ = assert_norm(int_rem (-1) (-2) = -1)
 
 let scalar_rem (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
-  if y <> 0 then mk_scalar ty (int_rem x y) else Fail
+  if y <> 0 then mk_scalar ty (int_rem x y) else Fail Failure
 
 let scalar_add (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
   mk_scalar ty (x + y)
@@ -258,7 +262,7 @@ let vec_push_back (a  : Type0) (v : vec a) (x : a) :
   (requires True)
   (ensures (fun res ->
     match res with
-    | Fail -> True
+    | Fail e -> e == Failure
     | Return v' -> length v' = length v + 1)) =
   if length v < usize_max then begin
     (**) assert_norm(length [x] == 1);
@@ -266,22 +270,22 @@ let vec_push_back (a  : Type0) (v : vec a) (x : a) :
     (**) assert(length (append v [x]) = length v + 1);
     Return (append v [x])
     end
-  else Fail
+  else Fail Failure
 
 // The **forward** function shouldn't be used
 let vec_insert_fwd (a : Type0) (v : vec a) (i : usize) (x : a) : result unit =
-  if i < length v then Return () else Fail
+  if i < length v then Return () else Fail Failure
 let vec_insert_back (a : Type0) (v : vec a) (i : usize) (x : a) : result (vec a) =
-  if i < length v then Return (list_update v i x) else Fail
+  if i < length v then Return (list_update v i x) else Fail Failure
 
 // The **backward** function shouldn't be used
 let vec_index_fwd (a : Type0) (v : vec a) (i : usize) : result a =
-  if i < length v then Return (index v i) else Fail
+  if i < length v then Return (index v i) else Fail Failure
 let vec_index_back (a : Type0) (v : vec a) (i : usize) (x : a) : result unit =
-  if i < length v then Return () else Fail
+  if i < length v then Return () else Fail Failure
 
 let vec_index_mut_fwd (a : Type0) (v : vec a) (i : usize) : result a =
-  if i < length v then Return (index v i) else Fail
+  if i < length v then Return (index v i) else Fail Failure
 let vec_index_mut_back (a : Type0) (v : vec a) (i : usize) (nx : a) : result (vec a) =
-  if i < length v then Return (list_update v i nx) else Fail
+  if i < length v then Return (list_update v i nx) else Fail Failure
 
diff --git a/tests/fstar/misc/Constants.fst b/tests/fstar/misc/Constants.fst
index 884d1778..a0658206 100644
--- a/tests/fstar/misc/Constants.fst
+++ b/tests/fstar/misc/Constants.fst
@@ -23,11 +23,11 @@ let x2_c : u32 = eval_global x2_body
 
 (** [constants::incr] *)
 let incr_fwd (n : u32) : result u32 =
-  begin match u32_add n 1 with | Fail -> Fail | Return i -> Return i end
+  begin match u32_add n 1 with | Fail e -> Fail e | Return i -> Return i end
 
 (** [constants::X3] *)
 let x3_body : result u32 =
-  begin match incr_fwd 32 with | Fail -> Fail | Return i -> Return i end
+  begin match incr_fwd 32 with | Fail e -> Fail e | Return i -> Return i end
 let x3_c : u32 = eval_global x3_body
 
 (** [constants::mk_pair0] *)
@@ -42,12 +42,18 @@ let mk_pair1_fwd (x : u32) (y : u32) : result (pair_t u32 u32) =
 
 (** [constants::P0] *)
 let p0_body : result (u32 & u32) =
-  begin match mk_pair0_fwd 0 1 with | Fail -> Fail | Return p -> Return p end
+  begin match mk_pair0_fwd 0 1 with
+  | Fail e -> Fail e
+  | Return p -> Return p
+  end
 let p0_c : (u32 & u32) = eval_global p0_body
 
 (** [constants::P1] *)
 let p1_body : result (pair_t u32 u32) =
-  begin match mk_pair1_fwd 0 1 with | Fail -> Fail | Return p -> Return p end
+  begin match mk_pair1_fwd 0 1 with
+  | Fail e -> Fail e
+  | Return p -> Return p
+  end
 let p1_c : pair_t u32 u32 = eval_global p1_body
 
 (** [constants::P2] *)
@@ -67,7 +73,10 @@ let wrap_new_fwd (t : Type0) (val0 : t) : result (wrap_t t) =
 
 (** [constants::Y] *)
 let y_body : result (wrap_t i32) =
-  begin match wrap_new_fwd i32 2 with | Fail -> Fail | Return w -> Return w end
+  begin match wrap_new_fwd i32 2 with
+  | Fail e -> Fail e
+  | Return w -> Return w
+  end
 let y_c : wrap_t i32 = eval_global y_body
 
 (** [constants::unwrap_y] *)
@@ -75,7 +84,7 @@ let unwrap_y_fwd : result i32 = Return y_c.wrap_val
 
 (** [constants::YVAL] *)
 let yval_body : result i32 =
-  begin match unwrap_y_fwd with | Fail -> Fail | Return i -> Return i end
+  begin match unwrap_y_fwd with | Fail e -> Fail e | Return i -> Return i end
 let yval_c : i32 = eval_global yval_body
 
 (** [constants::get_z1::Z1] *)
@@ -87,7 +96,7 @@ let get_z1_fwd : result i32 = Return get_z1_z1_c
 
 (** [constants::add] *)
 let add_fwd (a : i32) (b : i32) : result i32 =
-  begin match i32_add a b with | Fail -> Fail | Return i -> Return i end
+  begin match i32_add a b with | Fail e -> Fail e | Return i -> Return i end
 
 (** [constants::Q1] *)
 let q1_body : result i32 = Return 5
@@ -99,19 +108,19 @@ let q2_c : i32 = eval_global q2_body
 
 (** [constants::Q3] *)
 let q3_body : result i32 =
-  begin match add_fwd q2_c 3 with | Fail -> Fail | Return i -> Return i end
+  begin match add_fwd q2_c 3 with | Fail e -> Fail e | Return i -> Return i end
 let q3_c : i32 = eval_global q3_body
 
 (** [constants::get_z2] *)
 let get_z2_fwd : result i32 =
   begin match get_z1_fwd with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return i ->
     begin match add_fwd i q3_c with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return i0 ->
       begin match add_fwd q1_c i0 with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return i1 -> Return i1
       end
     end
@@ -123,7 +132,7 @@ let s1_c : u32 = eval_global s1_body
 
 (** [constants::S2] *)
 let s2_body : result u32 =
-  begin match incr_fwd s1_c with | Fail -> Fail | Return i -> Return i end
+  begin match incr_fwd s1_c with | Fail e -> Fail e | Return i -> Return i end
 let s2_c : u32 = eval_global s2_body
 
 (** [constants::S3] *)
@@ -132,6 +141,9 @@ let s3_c : pair_t u32 u32 = eval_global s3_body
 
 (** [constants::S4] *)
 let s4_body : result (pair_t u32 u32) =
-  begin match mk_pair1_fwd 7 8 with | Fail -> Fail | Return p -> Return p end
+  begin match mk_pair1_fwd 7 8 with
+  | Fail e -> Fail e
+  | Return p -> Return p
+  end
 let s4_c : pair_t u32 u32 = eval_global s4_body
 
diff --git a/tests/fstar/misc/External.Funs.fst b/tests/fstar/misc/External.Funs.fst
index 68a0061e..a57472d4 100644
--- a/tests/fstar/misc/External.Funs.fst
+++ b/tests/fstar/misc/External.Funs.fst
@@ -10,13 +10,13 @@ include External.Opaque
 (** [external::swap] *)
 let swap_fwd (t : Type0) (x : t) (y : t) (st : state) : result (state & unit) =
   begin match core_mem_swap_fwd t x y st with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return (st0, _) ->
     begin match core_mem_swap_back0 t x y st st0 with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return (st1, _) ->
       begin match core_mem_swap_back1 t x y st st1 with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return (st2, _) -> Return (st2, ())
       end
     end
@@ -28,13 +28,13 @@ let swap_back
   result (state & (t & t))
   =
   begin match core_mem_swap_fwd t x y st with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return (st1, _) ->
     begin match core_mem_swap_back0 t x y st st1 with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return (st2, x0) ->
       begin match core_mem_swap_back1 t x y st st2 with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return (_, y0) -> Return (st0, (x0, y0))
       end
     end
@@ -44,12 +44,12 @@ let swap_back
 let test_new_non_zero_u32_fwd
   (x : u32) (st : state) : result (state & core_num_nonzero_non_zero_u32_t) =
   begin match core_num_nonzero_non_zero_u32_new_fwd x st with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return (st0, opt) ->
     begin match
       core_option_option_unwrap_fwd core_num_nonzero_non_zero_u32_t opt st0
       with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return (st1, nzu) -> Return (st1, nzu)
     end
   end
@@ -58,7 +58,7 @@ let test_new_non_zero_u32_fwd
 let test_vec_fwd : result unit =
   let v = vec_new u32 in
   begin match vec_push_back u32 v 0 with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return _ -> Return ()
   end
 
@@ -69,13 +69,13 @@ let _ = assert_norm (test_vec_fwd = Return ())
 let custom_swap_fwd
   (t : Type0) (x : t) (y : t) (st : state) : result (state & t) =
   begin match core_mem_swap_fwd t x y st with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return (st0, _) ->
     begin match core_mem_swap_back0 t x y st st0 with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return (st1, x0) ->
       begin match core_mem_swap_back1 t x y st st1 with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return (st2, _) -> Return (st2, x0)
       end
     end
@@ -87,13 +87,13 @@ let custom_swap_back
   result (state & (t & t))
   =
   begin match core_mem_swap_fwd t x y st with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return (st1, _) ->
     begin match core_mem_swap_back0 t x y st st1 with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return (st2, _) ->
       begin match core_mem_swap_back1 t x y st st2 with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return (_, y0) -> Return (st0, (ret, y0))
       end
     end
@@ -103,7 +103,7 @@ let custom_swap_back
 let test_custom_swap_fwd
   (x : u32) (y : u32) (st : state) : result (state & unit) =
   begin match custom_swap_fwd u32 x y st with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return (st0, _) -> Return (st0, ())
   end
 
@@ -113,18 +113,19 @@ let test_custom_swap_back
   result (state & (u32 & u32))
   =
   begin match custom_swap_back u32 x y st 1 st0 with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return (st1, (x0, y0)) -> Return (st1, (x0, y0))
   end
 
 (** [external::test_swap_non_zero] *)
 let test_swap_non_zero_fwd (x : u32) (st : state) : result (state & u32) =
   begin match swap_fwd u32 x 0 st with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return (st0, _) ->
     begin match swap_back u32 x 0 st st0 with
-    | Fail -> Fail
-    | Return (st1, (x0, _)) -> if x0 = 0 then Fail else Return (st1, x0)
+    | Fail e -> Fail e
+    | Return (st1, (x0, _)) ->
+      if x0 = 0 then Fail Failure else Return (st1, x0)
     end
   end
 
diff --git a/tests/fstar/misc/NoNestedBorrows.fst b/tests/fstar/misc/NoNestedBorrows.fst
index 36dea95b..8424a7cc 100644
--- a/tests/fstar/misc/NoNestedBorrows.fst
+++ b/tests/fstar/misc/NoNestedBorrows.fst
@@ -32,38 +32,38 @@ type sum_t (t1 t2 : Type0) =
 
 (** [no_nested_borrows::neg_test] *)
 let neg_test_fwd (x : i32) : result i32 =
-  begin match i32_neg x with | Fail -> Fail | Return i -> Return i end
+  begin match i32_neg x with | Fail e -> Fail e | Return i -> Return i end
 
 (** [no_nested_borrows::add_test] *)
 let add_test_fwd (x : u32) (y : u32) : result u32 =
-  begin match u32_add x y with | Fail -> Fail | Return i -> Return i end
+  begin match u32_add x y with | Fail e -> Fail e | Return i -> Return i end
 
 (** [no_nested_borrows::subs_test] *)
 let subs_test_fwd (x : u32) (y : u32) : result u32 =
-  begin match u32_sub x y with | Fail -> Fail | Return i -> Return i end
+  begin match u32_sub x y with | Fail e -> Fail e | Return i -> Return i end
 
 (** [no_nested_borrows::div_test] *)
 let div_test_fwd (x : u32) (y : u32) : result u32 =
-  begin match u32_div x y with | Fail -> Fail | Return i -> Return i end
+  begin match u32_div x y with | Fail e -> Fail e | Return i -> Return i end
 
 (** [no_nested_borrows::div_test1] *)
 let div_test1_fwd (x : u32) : result u32 =
-  begin match u32_div x 2 with | Fail -> Fail | Return i -> Return i end
+  begin match u32_div x 2 with | Fail e -> Fail e | Return i -> Return i end
 
 (** [no_nested_borrows::rem_test] *)
 let rem_test_fwd (x : u32) (y : u32) : result u32 =
-  begin match u32_rem x y with | Fail -> Fail | Return i -> Return i end
+  begin match u32_rem x y with | Fail e -> Fail e | Return i -> Return i end
 
 (** [no_nested_borrows::cast_test] *)
 let cast_test_fwd (x : u32) : result i32 =
   begin match scalar_cast U32 I32 x with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return i -> Return i
   end
 
 (** [no_nested_borrows::test2] *)
 let test2_fwd : result unit =
-  begin match u32_add 23 44 with | Fail -> Fail | Return _ -> Return () end
+  begin match u32_add 23 44 with | Fail e -> Fail e | Return _ -> Return () end
 
 (** Unit test for [no_nested_borrows::test2] *)
 let _ = assert_norm (test2_fwd = Return ())
@@ -75,14 +75,14 @@ let get_max_fwd (x : u32) (y : u32) : result u32 =
 (** [no_nested_borrows::test3] *)
 let test3_fwd : result unit =
   begin match get_max_fwd 4 3 with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return x ->
     begin match get_max_fwd 10 11 with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return y ->
       begin match u32_add x y with
-      | Fail -> Fail
-      | Return z -> if not (z = 15) then Fail else Return ()
+      | Fail e -> Fail e
+      | Return z -> if not (z = 15) then Fail Failure else Return ()
       end
     end
   end
@@ -93,15 +93,16 @@ let _ = assert_norm (test3_fwd = Return ())
 (** [no_nested_borrows::test_neg1] *)
 let test_neg1_fwd : result unit =
   begin match i32_neg 3 with
-  | Fail -> Fail
-  | Return y -> if not (y = -3) then Fail else Return ()
+  | Fail e -> Fail e
+  | Return y -> if not (y = -3) then Fail Failure else Return ()
   end
 
 (** Unit test for [no_nested_borrows::test_neg1] *)
 let _ = assert_norm (test_neg1_fwd = Return ())
 
 (** [no_nested_borrows::refs_test1] *)
-let refs_test1_fwd : result unit = if not (1 = 1) then Fail else Return ()
+let refs_test1_fwd : result unit =
+  if not (1 = 1) then Fail Failure else Return ()
 
 (** Unit test for [no_nested_borrows::refs_test1] *)
 let _ = assert_norm (refs_test1_fwd = Return ())
@@ -109,11 +110,14 @@ let _ = assert_norm (refs_test1_fwd = Return ())
 (** [no_nested_borrows::refs_test2] *)
 let refs_test2_fwd : result unit =
   if not (2 = 2)
-  then Fail
+  then Fail Failure
   else
     if not (0 = 0)
-    then Fail
-    else if not (2 = 2) then Fail else if not (2 = 2) then Fail else Return ()
+    then Fail Failure
+    else
+      if not (2 = 2)
+      then Fail Failure
+      else if not (2 = 2) then Fail Failure else Return ()
 
 (** Unit test for [no_nested_borrows::refs_test2] *)
 let _ = assert_norm (refs_test2_fwd = Return ())
@@ -126,7 +130,7 @@ let _ = assert_norm (test_list1_fwd = Return ())
 
 (** [no_nested_borrows::test_box1] *)
 let test_box1_fwd : result unit =
-  let b = 1 in let x = b in if not (x = 1) then Fail else Return ()
+  let b = 1 in let x = b in if not (x = 1) then Fail Failure else Return ()
 
 (** Unit test for [no_nested_borrows::test_box1] *)
 let _ = assert_norm (test_box1_fwd = Return ())
@@ -136,16 +140,17 @@ let copy_int_fwd (x : i32) : result i32 = Return x
 
 (** [no_nested_borrows::test_unreachable] *)
 let test_unreachable_fwd (b : bool) : result unit =
-  if b then Fail else Return ()
+  if b then Fail Failure else Return ()
 
 (** [no_nested_borrows::test_panic] *)
-let test_panic_fwd (b : bool) : result unit = if b then Fail else Return ()
+let test_panic_fwd (b : bool) : result unit =
+  if b then Fail Failure else Return ()
 
 (** [no_nested_borrows::test_copy_int] *)
 let test_copy_int_fwd : result unit =
   begin match copy_int_fwd 0 with
-  | Fail -> Fail
-  | Return y -> if not (0 = y) then Fail else Return ()
+  | Fail e -> Fail e
+  | Return y -> if not (0 = y) then Fail Failure else Return ()
   end
 
 (** Unit test for [no_nested_borrows::test_copy_int] *)
@@ -162,8 +167,8 @@ let is_cons_fwd (t : Type0) (l : list_t t) : result bool =
 let test_is_cons_fwd : result unit =
   let l = ListNil in
   begin match is_cons_fwd i32 (ListCons 0 l) with
-  | Fail -> Fail
-  | Return b -> if not b then Fail else Return ()
+  | Fail e -> Fail e
+  | Return b -> if not b then Fail Failure else Return ()
   end
 
 (** Unit test for [no_nested_borrows::test_is_cons] *)
@@ -171,14 +176,18 @@ let _ = assert_norm (test_is_cons_fwd = Return ())
 
 (** [no_nested_borrows::split_list] *)
 let split_list_fwd (t : Type0) (l : list_t t) : result (t & (list_t t)) =
-  begin match l with | ListCons hd tl -> Return (hd, tl) | ListNil -> Fail end
+  begin match l with
+  | ListCons hd tl -> Return (hd, tl)
+  | ListNil -> Fail Failure
+  end
 
 (** [no_nested_borrows::test_split_list] *)
 let test_split_list_fwd : result unit =
   let l = ListNil in
   begin match split_list_fwd i32 (ListCons 0 l) with
-  | Fail -> Fail
-  | Return p -> let (hd, _) = p in if not (hd = 0) then Fail else Return ()
+  | Fail e -> Fail e
+  | Return p ->
+    let (hd, _) = p in if not (hd = 0) then Fail Failure else Return ()
   end
 
 (** Unit test for [no_nested_borrows::test_split_list] *)
@@ -196,18 +205,20 @@ let choose_back
 (** [no_nested_borrows::choose_test] *)
 let choose_test_fwd : result unit =
   begin match choose_fwd i32 true 0 0 with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return z ->
     begin match i32_add z 1 with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return z0 ->
       if not (z0 = 1)
-      then Fail
+      then Fail Failure
       else
         begin match choose_back i32 true 0 0 z0 with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return (x, y) ->
-          if not (x = 1) then Fail else if not (y = 0) then Fail else Return ()
+          if not (x = 1)
+          then Fail Failure
+          else if not (y = 0) then Fail Failure else Return ()
         end
     end
   end
@@ -233,9 +244,12 @@ let rec list_length_fwd (t : Type0) (l : list_t t) : result u32 =
   begin match l with
   | ListCons x l1 ->
     begin match list_length_fwd t l1 with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return i ->
-      begin match u32_add 1 i with | Fail -> Fail | Return i0 -> Return i0 end
+      begin match u32_add 1 i with
+      | Fail e -> Fail e
+      | Return i0 -> Return i0
+      end
     end
   | ListNil -> Return 0
   end
@@ -248,14 +262,14 @@ let rec list_nth_shared_fwd (t : Type0) (l : list_t t) (i : u32) : result t =
     then Return x
     else
       begin match u32_sub i 1 with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return i0 ->
         begin match list_nth_shared_fwd t tl i0 with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return x0 -> Return x0
         end
       end
-  | ListNil -> Fail
+  | ListNil -> Fail Failure
   end
 
 (** [no_nested_borrows::list_nth_mut] *)
@@ -266,14 +280,14 @@ let rec list_nth_mut_fwd (t : Type0) (l : list_t t) (i : u32) : result t =
     then Return x
     else
       begin match u32_sub i 1 with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return i0 ->
         begin match list_nth_mut_fwd t tl i0 with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return x0 -> Return x0
         end
       end
-  | ListNil -> Fail
+  | ListNil -> Fail Failure
   end
 
 (** [no_nested_borrows::list_nth_mut] *)
@@ -285,14 +299,14 @@ let rec list_nth_mut_back
     then Return (ListCons ret tl)
     else
       begin match u32_sub i 1 with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return i0 ->
         begin match list_nth_mut_back t tl i0 ret with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return tl0 -> Return (ListCons x tl0)
         end
       end
-  | ListNil -> Fail
+  | ListNil -> Fail Failure
   end
 
 (** [no_nested_borrows::list_rev_aux] *)
@@ -301,7 +315,7 @@ let rec list_rev_aux_fwd
   begin match li with
   | ListCons hd tl ->
     begin match list_rev_aux_fwd t tl (ListCons hd lo) with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return l -> Return l
     end
   | ListNil -> Return lo
@@ -311,7 +325,7 @@ let rec list_rev_aux_fwd
 let list_rev_fwd_back (t : Type0) (l : list_t t) : result (list_t t) =
   let li = mem_replace_fwd (list_t t) l ListNil in
   begin match list_rev_aux_fwd t li ListNil with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return l0 -> Return l0
   end
 
@@ -321,48 +335,48 @@ let test_list_functions_fwd : result unit =
   let l0 = ListCons 2 l in
   let l1 = ListCons 1 l0 in
   begin match list_length_fwd i32 (ListCons 0 l1) with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return i ->
     if not (i = 3)
-    then Fail
+    then Fail Failure
     else
       begin match list_nth_shared_fwd i32 (ListCons 0 l1) 0 with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return i0 ->
         if not (i0 = 0)
-        then Fail
+        then Fail Failure
         else
           begin match list_nth_shared_fwd i32 (ListCons 0 l1) 1 with
-          | Fail -> Fail
+          | Fail e -> Fail e
           | Return i1 ->
             if not (i1 = 1)
-            then Fail
+            then Fail Failure
             else
               begin match list_nth_shared_fwd i32 (ListCons 0 l1) 2 with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return i2 ->
                 if not (i2 = 2)
-                then Fail
+                then Fail Failure
                 else
                   begin match list_nth_mut_back i32 (ListCons 0 l1) 1 3 with
-                  | Fail -> Fail
+                  | Fail e -> Fail e
                   | Return ls ->
                     begin match list_nth_shared_fwd i32 ls 0 with
-                    | Fail -> Fail
+                    | Fail e -> Fail e
                     | Return i3 ->
                       if not (i3 = 0)
-                      then Fail
+                      then Fail Failure
                       else
                         begin match list_nth_shared_fwd i32 ls 1 with
-                        | Fail -> Fail
+                        | Fail e -> Fail e
                         | Return i4 ->
                           if not (i4 = 3)
-                          then Fail
+                          then Fail Failure
                           else
                             begin match list_nth_shared_fwd i32 ls 2 with
-                            | Fail -> Fail
+                            | Fail e -> Fail e
                             | Return i5 ->
-                              if not (i5 = 2) then Fail else Return ()
+                              if not (i5 = 2) then Fail Failure else Return ()
                             end
                         end
                     end
@@ -449,31 +463,31 @@ let new_pair1_fwd : result (struct_with_pair_t u32 u32) =
 (** [no_nested_borrows::test_constants] *)
 let test_constants_fwd : result unit =
   begin match new_tuple1_fwd with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return swt ->
     let (i, _) = swt.struct_with_tuple_p in
     if not (i = 1)
-    then Fail
+    then Fail Failure
     else
       begin match new_tuple2_fwd with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return swt0 ->
         let (i0, _) = swt0.struct_with_tuple_p in
         if not (i0 = 1)
-        then Fail
+        then Fail Failure
         else
           begin match new_tuple3_fwd with
-          | Fail -> Fail
+          | Fail e -> Fail e
           | Return swt1 ->
             let (i1, _) = swt1.struct_with_tuple_p in
             if not (i1 = 1)
-            then Fail
+            then Fail Failure
             else
               begin match new_pair1_fwd with
-              | Fail -> Fail
+              | Fail e -> Fail e
               | Return swp ->
                 if not (swp.struct_with_pair_p.pair_x = 1)
-                then Fail
+                then Fail Failure
                 else Return ()
               end
           end
@@ -491,7 +505,8 @@ let _ = assert_norm (test_weird_borrows1_fwd = Return ())
 
 (** [no_nested_borrows::test_mem_replace] *)
 let test_mem_replace_fwd_back (px : u32) : result u32 =
-  let y = mem_replace_fwd u32 px 1 in if not (y = 0) then Fail else Return 2
+  let y = mem_replace_fwd u32 px 1 in
+  if not (y = 0) then Fail Failure else Return 2
 
 (** [no_nested_borrows::test_shared_borrow_bool1] *)
 let test_shared_borrow_bool1_fwd (b : bool) : result u32 =
diff --git a/tests/fstar/misc/Paper.fst b/tests/fstar/misc/Paper.fst
index 424889ef..0f8604d1 100644
--- a/tests/fstar/misc/Paper.fst
+++ b/tests/fstar/misc/Paper.fst
@@ -7,13 +7,13 @@ open Primitives
 
 (** [paper::ref_incr] *)
 let ref_incr_fwd_back (x : i32) : result i32 =
-  begin match i32_add x 1 with | Fail -> Fail | Return x0 -> Return x0 end
+  begin match i32_add x 1 with | Fail e -> Fail e | Return x0 -> Return x0 end
 
 (** [paper::test_incr] *)
 let test_incr_fwd : result unit =
   begin match ref_incr_fwd_back 0 with
-  | Fail -> Fail
-  | Return x -> if not (x = 1) then Fail else Return ()
+  | Fail e -> Fail e
+  | Return x -> if not (x = 1) then Fail Failure else Return ()
   end
 
 (** Unit test for [paper::test_incr] *)
@@ -31,18 +31,20 @@ let choose_back
 (** [paper::test_choose] *)
 let test_choose_fwd : result unit =
   begin match choose_fwd i32 true 0 0 with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return z ->
     begin match i32_add z 1 with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return z0 ->
       if not (z0 = 1)
-      then Fail
+      then Fail Failure
       else
         begin match choose_back i32 true 0 0 z0 with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return (x, y) ->
-          if not (x = 1) then Fail else if not (y = 0) then Fail else Return ()
+          if not (x = 1)
+          then Fail Failure
+          else if not (y = 0) then Fail Failure else Return ()
         end
     end
   end
@@ -63,14 +65,14 @@ let rec list_nth_mut_fwd (t : Type0) (l : list_t t) (i : u32) : result t =
     then Return x
     else
       begin match u32_sub i 1 with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return i0 ->
         begin match list_nth_mut_fwd t tl i0 with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return x0 -> Return x0
         end
       end
-  | ListNil -> Fail
+  | ListNil -> Fail Failure
   end
 
 (** [paper::list_nth_mut] *)
@@ -82,14 +84,14 @@ let rec list_nth_mut_back
     then Return (ListCons ret tl)
     else
       begin match u32_sub i 1 with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return i0 ->
         begin match list_nth_mut_back t tl i0 ret with
-        | Fail -> Fail
+        | Fail e -> Fail e
         | Return tl0 -> Return (ListCons x tl0)
         end
       end
-  | ListNil -> Fail
+  | ListNil -> Fail Failure
   end
 
 (** [paper::sum] *)
@@ -97,9 +99,12 @@ let rec sum_fwd (l : list_t i32) : result i32 =
   begin match l with
   | ListCons x tl ->
     begin match sum_fwd tl with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return i ->
-      begin match i32_add x i with | Fail -> Fail | Return i0 -> Return i0 end
+      begin match i32_add x i with
+      | Fail e -> Fail e
+      | Return i0 -> Return i0
+      end
     end
   | ListNil -> Return 0
   end
@@ -110,17 +115,17 @@ let test_nth_fwd : result unit =
   let l0 = ListCons 3 l in
   let l1 = ListCons 2 l0 in
   begin match list_nth_mut_fwd i32 (ListCons 1 l1) 2 with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return x ->
     begin match i32_add x 1 with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return x0 ->
       begin match list_nth_mut_back i32 (ListCons 1 l1) 2 x0 with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return l2 ->
         begin match sum_fwd l2 with
-        | Fail -> Fail
-        | Return i -> if not (i = 7) then Fail else Return ()
+        | Fail e -> Fail e
+        | Return i -> if not (i = 7) then Fail Failure else Return ()
         end
       end
     end
@@ -133,13 +138,13 @@ let _ = assert_norm (test_nth_fwd = Return ())
 let call_choose_fwd (p : (u32 & u32)) : result u32 =
   let (px, py) = p in
   begin match choose_fwd u32 true px py with
-  | Fail -> Fail
+  | Fail e -> Fail e
   | Return pz ->
     begin match u32_add pz 1 with
-    | Fail -> Fail
+    | Fail e -> Fail e
     | Return pz0 ->
       begin match choose_back u32 true px py pz0 with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return (px0, _) -> Return px0
       end
     end
diff --git a/tests/fstar/misc/PoloniusList.fst b/tests/fstar/misc/PoloniusList.fst
index 73e98884..158a5fc7 100644
--- a/tests/fstar/misc/PoloniusList.fst
+++ b/tests/fstar/misc/PoloniusList.fst
@@ -18,7 +18,7 @@ let rec get_list_at_x_fwd (ls : list_t u32) (x : u32) : result (list_t u32) =
     then Return (ListCons hd tl)
     else
       begin match get_list_at_x_fwd tl x with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return l -> Return l
       end
   | ListNil -> Return ListNil
@@ -33,7 +33,7 @@ let rec get_list_at_x_back
     then Return ret
     else
       begin match get_list_at_x_back tl x ret with
-      | Fail -> Fail
+      | Fail e -> Fail e
       | Return tl0 -> Return (ListCons hd tl0)
       end
   | ListNil -> Return ret
diff --git a/tests/fstar/misc/Primitives.fst b/tests/fstar/misc/Primitives.fst
index 96138e46..82622656 100644
--- a/tests/fstar/misc/Primitives.fst
+++ b/tests/fstar/misc/Primitives.fst
@@ -18,9 +18,13 @@ let rec list_update #a ls i x =
 #pop-options
 
 (*** Result *)
+type error : Type0 =
+| Failure
+| OutOfFuel
+
 type result (a : Type0) : Type0 =
 | Return : v:a -> result a
-| Fail : result a
+| Fail : e:error -> result a
 
 // Monadic bind and return.
 // Re-definining those allows us to customize the result of the monadic notations
@@ -29,10 +33,10 @@ let return (#a : Type0) (x:a) : result a = Return x
 let bind (#a #b : Type0) (m : result a) (f : a -> result b) : result b =
     match m with
     | Return x -> f x
-    | Fail -> Fail
+    | Fail e -> Fail e
 
 // Monadic assert(...)
-let massert (b:bool) : result unit = if b then Return () else Fail
+let massert (b:bool) : result unit = if b then Return () else Fail Failure
 
 // Normalize and unwrap a successful result (used for globals).
 let eval_global (#a : Type0) (x : result a{Return? (normalize_term x)}) : a = Return?.v x
@@ -119,12 +123,12 @@ let scalar_max (ty : scalar_ty) : int =
 type scalar (ty : scalar_ty) : eqtype = x:int{scalar_min ty <= x && x <= scalar_max ty}
 
 let mk_scalar (ty : scalar_ty) (x : int) : result (scalar ty) =
-  if scalar_min ty <= x && scalar_max ty >= x then Return x else Fail
+  if scalar_min ty <= x && scalar_max ty >= x then Return x else Fail Failure
 
 let scalar_neg (#ty : scalar_ty) (x : scalar ty) : result (scalar ty) = mk_scalar ty (-x)
 
 let scalar_div (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
-  if y <> 0 then mk_scalar ty (x / y) else Fail
+  if y <> 0 then mk_scalar ty (x / y) else Fail Failure
 
 /// The remainder operation
 let int_rem (x : int) (y : int{y <> 0}) : int =
@@ -137,7 +141,7 @@ let _ = assert_norm(int_rem 1 (-2) = 1)
 let _ = assert_norm(int_rem (-1) (-2) = -1)
 
 let scalar_rem (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
-  if y <> 0 then mk_scalar ty (int_rem x y) else Fail
+  if y <> 0 then mk_scalar ty (int_rem x y) else Fail Failure
 
 let scalar_add (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
   mk_scalar ty (x + y)
@@ -258,7 +262,7 @@ let vec_push_back (a  : Type0) (v : vec a) (x : a) :
   (requires True)
   (ensures (fun res ->
     match res with
-    | Fail -> True
+    | Fail e -> e == Failure
     | Return v' -> length v' = length v + 1)) =
   if length v < usize_max then begin
     (**) assert_norm(length [x] == 1);
@@ -266,22 +270,22 @@ let vec_push_back (a  : Type0) (v : vec a) (x : a) :
     (**) assert(length (append v [x]) = length v + 1);
     Return (append v [x])
     end
-  else Fail
+  else Fail Failure
 
 // The **forward** function shouldn't be used
 let vec_insert_fwd (a : Type0) (v : vec a) (i : usize) (x : a) : result unit =
-  if i < length v then Return () else Fail
+  if i < length v then Return () else Fail Failure
 let vec_insert_back (a : Type0) (v : vec a) (i : usize) (x : a) : result (vec a) =
-  if i < length v then Return (list_update v i x) else Fail
+  if i < length v then Return (list_update v i x) else Fail Failure
 
 // The **backward** function shouldn't be used
 let vec_index_fwd (a : Type0) (v : vec a) (i : usize) : result a =
-  if i < length v then Return (index v i) else Fail
+  if i < length v then Return (index v i) else Fail Failure
 let vec_index_back (a : Type0) (v : vec a) (i : usize) (x : a) : result unit =
-  if i < length v then Return () else Fail
+  if i < length v then Return () else Fail Failure
 
 let vec_index_mut_fwd (a : Type0) (v : vec a) (i : usize) : result a =
-  if i < length v then Return (index v i) else Fail
+  if i < length v then Return (index v i) else Fail Failure
 let vec_index_mut_back (a : Type0) (v : vec a) (i : usize) (nx : a) : result (vec a) =
-  if i < length v then Return (list_update v i nx) else Fail
+  if i < length v then Return (list_update v i nx) else Fail Failure