Regenerate the files and fix the proofs

1 files changed, 212 insertions, 209 deletions

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)