Merge pull request #233 from AeneasVerif/son/borrow-check

Add a `-borrow-check` option

27 files changed, 1042 insertions, 456 deletions

diff --git a/tests/coq/betree/Betree_Funs.v b/tests/coq/betree/Betree_Funs.v
index b965d423..1c6092ba 100644
--- a/tests/coq/betree/Betree_Funs.v
+++ b/tests/coq/betree/Betree_Funs.v
@@ -88,45 +88,85 @@ Definition betree_upsert_update
   end
 .
 
+(** [betree::betree::{betree::betree::List<T>#1}::len]: loop 0:
+    Source: 'src/betree.rs', lines 276:4-284:5 *)
+Fixpoint betree_List_len_loop
+  (T : Type) (n : nat) (self : betree_List_t T) (len : u64) : result u64 :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n1 =>
+    match self with
+    | Betree_List_Cons _ tl =>
+      len1 <- u64_add len 1%u64; betree_List_len_loop T n1 tl len1
+    | Betree_List_Nil => Ok len
+    end
+  end
+.
+
 (** [betree::betree::{betree::betree::List<T>#1}::len]:
     Source: 'src/betree.rs', lines 276:4-276:24 *)
-Fixpoint betree_List_len
+Definition betree_List_len
   (T : Type) (n : nat) (self : betree_List_t T) : result u64 :=
+  betree_List_len_loop T n self 0%u64
+.
+
+(** [betree::betree::{betree::betree::List<T>#1}::reverse]: loop 0:
+    Source: 'src/betree.rs', lines 304:4-312:5 *)
+Fixpoint betree_List_reverse_loop
+  (T : Type) (n : nat) (self : betree_List_t T) (out : betree_List_t T) :
+  result (betree_List_t T)
+  :=
   match n with
   | O => Fail_ OutOfFuel
   | S n1 =>
     match self with
-    | Betree_List_Cons _ tl => i <- betree_List_len T n1 tl; u64_add 1%u64 i
-    | Betree_List_Nil => Ok 0%u64
+    | Betree_List_Cons hd tl =>
+      betree_List_reverse_loop T n1 tl (Betree_List_Cons hd out)
+    | Betree_List_Nil => Ok out
     end
   end
 .
 
-(** [betree::betree::{betree::betree::List<T>#1}::split_at]:
-    Source: 'src/betree.rs', lines 284:4-284:51 *)
-Fixpoint betree_List_split_at
-  (T : Type) (n : nat) (self : betree_List_t T) (n1 : u64) :
+(** [betree::betree::{betree::betree::List<T>#1}::reverse]:
+    Source: 'src/betree.rs', lines 304:4-304:32 *)
+Definition betree_List_reverse
+  (T : Type) (n : nat) (self : betree_List_t T) : result (betree_List_t T) :=
+  betree_List_reverse_loop T n self Betree_List_Nil
+.
+
+(** [betree::betree::{betree::betree::List<T>#1}::split_at]: loop 0:
+    Source: 'src/betree.rs', lines 287:4-302:5 *)
+Fixpoint betree_List_split_at_loop
+  (T : Type) (n : nat) (n1 : u64) (beg : betree_List_t T)
+  (self : betree_List_t T) :
   result ((betree_List_t T) * (betree_List_t T))
   :=
   match n with
   | O => Fail_ OutOfFuel
   | S n2 =>
-    if n1 s= 0%u64
-    then Ok (Betree_List_Nil, self)
-    else
+    if n1 s> 0%u64
+    then
       match self with
       | Betree_List_Cons hd tl =>
-        i <- u64_sub n1 1%u64;
-        p <- betree_List_split_at T n2 tl i;
-        let (ls0, ls1) := p in
-        Ok (Betree_List_Cons hd ls0, ls1)
+        n3 <- u64_sub n1 1%u64;
+        betree_List_split_at_loop T n2 n3 (Betree_List_Cons hd beg) tl
       | Betree_List_Nil => Fail_ Failure
       end
+    else (l <- betree_List_reverse T n2 beg; Ok (l, self))
   end
 .
 
+(** [betree::betree::{betree::betree::List<T>#1}::split_at]:
+    Source: 'src/betree.rs', lines 287:4-287:55 *)
+Definition betree_List_split_at
+  (T : Type) (n : nat) (self : betree_List_t T) (n1 : u64) :
+  result ((betree_List_t T) * (betree_List_t T))
+  :=
+  betree_List_split_at_loop T n n1 Betree_List_Nil self
+.
+
 (** [betree::betree::{betree::betree::List<T>#1}::push_front]:
-    Source: 'src/betree.rs', lines 299:4-299:34 *)
+    Source: 'src/betree.rs', lines 315:4-315:34 *)
 Definition betree_List_push_front
   (T : Type) (self : betree_List_t T) (x : T) : result (betree_List_t T) :=
   let (tl, _) := core_mem_replace (betree_List_t T) self Betree_List_Nil in
@@ -134,7 +174,7 @@ Definition betree_List_push_front
 .
 
 (** [betree::betree::{betree::betree::List<T>#1}::pop_front]:
-    Source: 'src/betree.rs', lines 306:4-306:32 *)
+    Source: 'src/betree.rs', lines 322:4-322:32 *)
 Definition betree_List_pop_front
   (T : Type) (self : betree_List_t T) : result (T * (betree_List_t T)) :=
   let (ls, _) := core_mem_replace (betree_List_t T) self Betree_List_Nil in
@@ -145,7 +185,7 @@ Definition betree_List_pop_front
 .
 
 (** [betree::betree::{betree::betree::List<T>#1}::hd]:
-    Source: 'src/betree.rs', lines 318:4-318:22 *)
+    Source: 'src/betree.rs', lines 334:4-334:22 *)
 Definition betree_List_hd (T : Type) (self : betree_List_t T) : result T :=
   match self with
   | Betree_List_Cons hd _ => Ok hd
@@ -154,7 +194,7 @@ Definition betree_List_hd (T : Type) (self : betree_List_t T) : result T :=
 .
 
 (** [betree::betree::{betree::betree::List<(u64, T)>#2}::head_has_key]:
-    Source: 'src/betree.rs', lines 327:4-327:44 *)
+    Source: 'src/betree.rs', lines 343:4-343:44 *)
 Definition betree_ListPairU64T_head_has_key
   (T : Type) (self : betree_List_t (u64 * T)) (key : u64) : result bool :=
   match self with
@@ -163,10 +203,11 @@ Definition betree_ListPairU64T_head_has_key
   end
 .
 
-(** [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]:
-    Source: 'src/betree.rs', lines 339:4-339:73 *)
-Fixpoint betree_ListPairU64T_partition_at_pivot
-  (T : Type) (n : nat) (self : betree_List_t (u64 * T)) (pivot : u64) :
+(** [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]: loop 0:
+    Source: 'src/betree.rs', lines 355:4-370:5 *)
+Fixpoint betree_ListPairU64T_partition_at_pivot_loop
+  (T : Type) (n : nat) (pivot : u64) (beg : betree_List_t (u64 * T))
+  (end1 : betree_List_t (u64 * T)) (self : betree_List_t (u64 * T)) :
   result ((betree_List_t (u64 * T)) * (betree_List_t (u64 * T)))
   :=
   match n with
@@ -176,18 +217,32 @@ Fixpoint betree_ListPairU64T_partition_at_pivot
     | Betree_List_Cons hd tl =>
       let (i, t) := hd in
       if i s>= pivot
-      then Ok (Betree_List_Nil, Betree_List_Cons (i, t) tl)
-      else (
-        p <- betree_ListPairU64T_partition_at_pivot T n1 tl pivot;
-        let (ls0, ls1) := p in
-        Ok (Betree_List_Cons (i, t) ls0, ls1))
-    | Betree_List_Nil => Ok (Betree_List_Nil, Betree_List_Nil)
+      then
+        betree_ListPairU64T_partition_at_pivot_loop T n1 pivot beg
+          (Betree_List_Cons (i, t) end1) tl
+      else
+        betree_ListPairU64T_partition_at_pivot_loop T n1 pivot
+          (Betree_List_Cons (i, t) beg) end1 tl
+    | Betree_List_Nil =>
+      l <- betree_List_reverse (u64 * T) n1 beg;
+      l1 <- betree_List_reverse (u64 * T) n1 end1;
+      Ok (l, l1)
     end
   end
 .
 
+(** [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]:
+    Source: 'src/betree.rs', lines 355:4-355:73 *)
+Definition betree_ListPairU64T_partition_at_pivot
+  (T : Type) (n : nat) (self : betree_List_t (u64 * T)) (pivot : u64) :
+  result ((betree_List_t (u64 * T)) * (betree_List_t (u64 * T)))
+  :=
+  betree_ListPairU64T_partition_at_pivot_loop T n pivot Betree_List_Nil
+    Betree_List_Nil self
+.
+
 (** [betree::betree::{betree::betree::Leaf#3}::split]:
-    Source: 'src/betree.rs', lines 359:4-364:17 *)
+    Source: 'src/betree.rs', lines 378:4-383:17 *)
 Definition betree_Leaf_split
   (n : nat) (self : betree_Leaf_t) (content : betree_List_t (u64 * u64))
   (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t)
@@ -222,9 +277,9 @@ Definition betree_Leaf_split
     node_id_cnt2))
 .
 
-(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_for_key]:
-    Source: 'src/betree.rs', lines 789:4-792:34 *)
-Fixpoint betree_Node_lookup_first_message_for_key
+(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_for_key]: loop 0:
+    Source: 'src/betree.rs', lines 792:4-810:5 *)
+Fixpoint betree_Node_lookup_first_message_for_key_loop
   (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) :
   result ((betree_List_t (u64 * betree_Message_t)) * (betree_List_t (u64 *
     betree_Message_t) -> result (betree_List_t (u64 * betree_Message_t))))
@@ -238,21 +293,30 @@ Fixpoint betree_Node_lookup_first_message_for_key
       if i s>= key
       then Ok (Betree_List_Cons (i, m) next_msgs, Ok)
       else (
-        p <- betree_Node_lookup_first_message_for_key n1 key next_msgs;
-        let (l, lookup_first_message_for_key_back) := p in
-        let back :=
+        p <- betree_Node_lookup_first_message_for_key_loop n1 key next_msgs;
+        let (l, back) := p in
+        let back1 :=
           fun (ret : betree_List_t (u64 * betree_Message_t)) =>
-            next_msgs1 <- lookup_first_message_for_key_back ret;
-            Ok (Betree_List_Cons (i, m) next_msgs1) in
-        Ok (l, back))
+            next_msgs1 <- back ret; Ok (Betree_List_Cons (i, m) next_msgs1) in
+        Ok (l, back1))
     | Betree_List_Nil => Ok (Betree_List_Nil, Ok)
     end
   end
 .
 
-(** [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]:
-    Source: 'src/betree.rs', lines 636:4-636:80 *)
-Fixpoint betree_Node_lookup_in_bindings
+(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_for_key]:
+    Source: 'src/betree.rs', lines 792:4-795:34 *)
+Definition betree_Node_lookup_first_message_for_key
+  (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) :
+  result ((betree_List_t (u64 * betree_Message_t)) * (betree_List_t (u64 *
+    betree_Message_t) -> result (betree_List_t (u64 * betree_Message_t))))
+  :=
+  betree_Node_lookup_first_message_for_key_loop n key msgs
+.
+
+(** [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]: loop 0:
+    Source: 'src/betree.rs', lines 649:4-660:5 *)
+Fixpoint betree_Node_lookup_in_bindings_loop
   (n : nat) (key : u64) (bindings : betree_List_t (u64 * u64)) :
   result (option u64)
   :=
@@ -265,15 +329,26 @@ Fixpoint betree_Node_lookup_in_bindings
       if i s= key
       then Ok (Some i1)
       else
-        if i s> key then Ok None else betree_Node_lookup_in_bindings n1 key tl
+        if i s> key
+        then Ok None
+        else betree_Node_lookup_in_bindings_loop n1 key tl
     | Betree_List_Nil => Ok None
     end
   end
 .
 
-(** [betree::betree::{betree::betree::Node#5}::apply_upserts]:
-    Source: 'src/betree.rs', lines 819:4-819:90 *)
-Fixpoint betree_Node_apply_upserts
+(** [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]:
+    Source: 'src/betree.rs', lines 649:4-649:84 *)
+Definition betree_Node_lookup_in_bindings
+  (n : nat) (key : u64) (bindings : betree_List_t (u64 * u64)) :
+  result (option u64)
+  :=
+  betree_Node_lookup_in_bindings_loop n key bindings
+.
+
+(** [betree::betree::{betree::betree::Node#5}::apply_upserts]: loop 0:
+    Source: 'src/betree.rs', lines 820:4-844:5 *)
+Fixpoint betree_Node_apply_upserts_loop
   (n : nat) (msgs : betree_List_t (u64 * betree_Message_t)) (prev : option u64)
   (key : u64) :
   result (u64 * (betree_List_t (u64 * betree_Message_t)))
@@ -292,7 +367,7 @@ Fixpoint betree_Node_apply_upserts
       | Betree_Message_Delete => Fail_ Failure
       | Betree_Message_Upsert s =>
         v <- betree_upsert_update prev s;
-        betree_Node_apply_upserts n1 msgs1 (Some v) key
+        betree_Node_apply_upserts_loop n1 msgs1 (Some v) key
       end)
     else (
       v <- core_option_Option_unwrap u64 prev;
@@ -303,8 +378,18 @@ Fixpoint betree_Node_apply_upserts
   end
 .
 
+(** [betree::betree::{betree::betree::Node#5}::apply_upserts]:
+    Source: 'src/betree.rs', lines 820:4-820:94 *)
+Definition betree_Node_apply_upserts
+  (n : nat) (msgs : betree_List_t (u64 * betree_Message_t)) (prev : option u64)
+  (key : u64) :
+  result (u64 * (betree_List_t (u64 * betree_Message_t)))
+  :=
+  betree_Node_apply_upserts_loop n msgs prev key
+.
+
 (** [betree::betree::{betree::betree::Internal#4}::lookup_in_children]:
-    Source: 'src/betree.rs', lines 395:4-395:63 *)
+    Source: 'src/betree.rs', lines 414:4-414:63 *)
 Fixpoint betree_Internal_lookup_in_children
   (n : nat) (self : betree_Internal_t) (key : u64) (st : state) :
   result (state * ((option u64) * betree_Internal_t))
@@ -328,7 +413,7 @@ Fixpoint betree_Internal_lookup_in_children
   end
 
 (** [betree::betree::{betree::betree::Node#5}::lookup]:
-    Source: 'src/betree.rs', lines 709:4-709:58 *)
+    Source: 'src/betree.rs', lines 712:4-712:58 *)
 with betree_Node_lookup
   (n : nat) (self : betree_Node_t) (key : u64) (st : state) :
   result (state * ((option u64) * betree_Node_t))
@@ -394,9 +479,9 @@ with betree_Node_lookup
   end
 .
 
-(** [betree::betree::{betree::betree::Node#5}::filter_messages_for_key]:
-    Source: 'src/betree.rs', lines 674:4-674:77 *)
-Fixpoint betree_Node_filter_messages_for_key
+(** [betree::betree::{betree::betree::Node#5}::filter_messages_for_key]: loop 0:
+    Source: 'src/betree.rs', lines 683:4-692:5 *)
+Fixpoint betree_Node_filter_messages_for_key_loop
   (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) :
   result (betree_List_t (u64 * betree_Message_t))
   :=
@@ -412,16 +497,25 @@ Fixpoint betree_Node_filter_messages_for_key
           betree_List_pop_front (u64 * betree_Message_t) (Betree_List_Cons (k,
             m) l);
         let (_, msgs1) := p1 in
-        betree_Node_filter_messages_for_key n1 key msgs1)
+        betree_Node_filter_messages_for_key_loop n1 key msgs1)
       else Ok (Betree_List_Cons (k, m) l)
     | Betree_List_Nil => Ok Betree_List_Nil
     end
   end
 .
 
-(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_after_key]:
-    Source: 'src/betree.rs', lines 689:4-692:34 *)
-Fixpoint betree_Node_lookup_first_message_after_key
+(** [betree::betree::{betree::betree::Node#5}::filter_messages_for_key]:
+    Source: 'src/betree.rs', lines 683:4-683:77 *)
+Definition betree_Node_filter_messages_for_key
+  (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) :
+  result (betree_List_t (u64 * betree_Message_t))
+  :=
+  betree_Node_filter_messages_for_key_loop n key msgs
+.
+
+(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_after_key]: loop 0:
+    Source: 'src/betree.rs', lines 694:4-706:5 *)
+Fixpoint betree_Node_lookup_first_message_after_key_loop
   (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) :
   result ((betree_List_t (u64 * betree_Message_t)) * (betree_List_t (u64 *
     betree_Message_t) -> result (betree_List_t (u64 * betree_Message_t))))
@@ -434,21 +528,30 @@ Fixpoint betree_Node_lookup_first_message_after_key
       let (k, m) := p in
       if k s= key
       then (
-        p1 <- betree_Node_lookup_first_message_after_key n1 key next_msgs;
-        let (l, lookup_first_message_after_key_back) := p1 in
-        let back :=
+        p1 <- betree_Node_lookup_first_message_after_key_loop n1 key next_msgs;
+        let (l, back) := p1 in
+        let back1 :=
           fun (ret : betree_List_t (u64 * betree_Message_t)) =>
-            next_msgs1 <- lookup_first_message_after_key_back ret;
-            Ok (Betree_List_Cons (k, m) next_msgs1) in
-        Ok (l, back))
+            next_msgs1 <- back ret; Ok (Betree_List_Cons (k, m) next_msgs1) in
+        Ok (l, back1))
       else Ok (Betree_List_Cons (k, m) next_msgs, Ok)
     | Betree_List_Nil => Ok (Betree_List_Nil, Ok)
     end
   end
 .
 
+(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_after_key]:
+    Source: 'src/betree.rs', lines 694:4-697:34 *)
+Definition betree_Node_lookup_first_message_after_key
+  (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) :
+  result ((betree_List_t (u64 * betree_Message_t)) * (betree_List_t (u64 *
+    betree_Message_t) -> result (betree_List_t (u64 * betree_Message_t))))
+  :=
+  betree_Node_lookup_first_message_after_key_loop n key msgs
+.
+
 (** [betree::betree::{betree::betree::Node#5}::apply_to_internal]:
-    Source: 'src/betree.rs', lines 521:4-521:89 *)
+    Source: 'src/betree.rs', lines 534:4-534:89 *)
 Definition betree_Node_apply_to_internal
   (n : nat) (msgs : betree_List_t (u64 * betree_Message_t)) (key : u64)
   (new_msg : betree_Message_t) :
@@ -508,9 +611,9 @@ Definition betree_Node_apply_to_internal
     lookup_first_message_for_key_back msgs2)
 .
 
-(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_internal]:
-    Source: 'src/betree.rs', lines 502:4-505:5 *)
-Fixpoint betree_Node_apply_messages_to_internal
+(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_internal]: loop 0:
+    Source: 'src/betree.rs', lines 518:4-526:5 *)
+Fixpoint betree_Node_apply_messages_to_internal_loop
   (n : nat) (msgs : betree_List_t (u64 * betree_Message_t))
   (new_msgs : betree_List_t (u64 * betree_Message_t)) :
   result (betree_List_t (u64 * betree_Message_t))
@@ -522,15 +625,25 @@ Fixpoint betree_Node_apply_messages_to_internal
     | Betree_List_Cons new_msg new_msgs_tl =>
       let (i, m) := new_msg in
       msgs1 <- betree_Node_apply_to_internal n1 msgs i m;
-      betree_Node_apply_messages_to_internal n1 msgs1 new_msgs_tl
+      betree_Node_apply_messages_to_internal_loop n1 msgs1 new_msgs_tl
     | Betree_List_Nil => Ok msgs
     end
   end
 .
 
-(** [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]:
-    Source: 'src/betree.rs', lines 653:4-656:32 *)
-Fixpoint betree_Node_lookup_mut_in_bindings
+(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_internal]:
+    Source: 'src/betree.rs', lines 518:4-521:5 *)
+Definition betree_Node_apply_messages_to_internal
+  (n : nat) (msgs : betree_List_t (u64 * betree_Message_t))
+  (new_msgs : betree_List_t (u64 * betree_Message_t)) :
+  result (betree_List_t (u64 * betree_Message_t))
+  :=
+  betree_Node_apply_messages_to_internal_loop n msgs new_msgs
+.
+
+(** [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]: loop 0:
+    Source: 'src/betree.rs', lines 664:4-677:5 *)
+Fixpoint betree_Node_lookup_mut_in_bindings_loop
   (n : nat) (key : u64) (bindings : betree_List_t (u64 * u64)) :
   result ((betree_List_t (u64 * u64)) * (betree_List_t (u64 * u64) -> result
     (betree_List_t (u64 * u64))))
@@ -544,20 +657,29 @@ Fixpoint betree_Node_lookup_mut_in_bindings
       if i s>= key
       then Ok (Betree_List_Cons (i, i1) tl, Ok)
       else (
-        p <- betree_Node_lookup_mut_in_bindings n1 key tl;
-        let (l, lookup_mut_in_bindings_back) := p in
-        let back :=
+        p <- betree_Node_lookup_mut_in_bindings_loop n1 key tl;
+        let (l, back) := p in
+        let back1 :=
           fun (ret : betree_List_t (u64 * u64)) =>
-            tl1 <- lookup_mut_in_bindings_back ret;
-            Ok (Betree_List_Cons (i, i1) tl1) in
-        Ok (l, back))
+            tl1 <- back ret; Ok (Betree_List_Cons (i, i1) tl1) in
+        Ok (l, back1))
     | Betree_List_Nil => Ok (Betree_List_Nil, Ok)
     end
   end
 .
 
+(** [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]:
+    Source: 'src/betree.rs', lines 664:4-667:32 *)
+Definition betree_Node_lookup_mut_in_bindings
+  (n : nat) (key : u64) (bindings : betree_List_t (u64 * u64)) :
+  result ((betree_List_t (u64 * u64)) * (betree_List_t (u64 * u64) -> result
+    (betree_List_t (u64 * u64))))
+  :=
+  betree_Node_lookup_mut_in_bindings_loop n key bindings
+.
+
 (** [betree::betree::{betree::betree::Node#5}::apply_to_leaf]:
-    Source: 'src/betree.rs', lines 460:4-460:87 *)
+    Source: 'src/betree.rs', lines 476:4-476:87 *)
 Definition betree_Node_apply_to_leaf
   (n : nat) (bindings : betree_List_t (u64 * u64)) (key : u64)
   (new_msg : betree_Message_t) :
@@ -594,9 +716,9 @@ Definition betree_Node_apply_to_leaf
     end
 .
 
-(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_leaf]:
-    Source: 'src/betree.rs', lines 444:4-447:5 *)
-Fixpoint betree_Node_apply_messages_to_leaf
+(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_leaf]: loop 0:
+    Source: 'src/betree.rs', lines 463:4-471:5 *)
+Fixpoint betree_Node_apply_messages_to_leaf_loop
   (n : nat) (bindings : betree_List_t (u64 * u64))
   (new_msgs : betree_List_t (u64 * betree_Message_t)) :
   result (betree_List_t (u64 * u64))
@@ -608,14 +730,24 @@ Fixpoint betree_Node_apply_messages_to_leaf
     | Betree_List_Cons new_msg new_msgs_tl =>
       let (i, m) := new_msg in
       bindings1 <- betree_Node_apply_to_leaf n1 bindings i m;
-      betree_Node_apply_messages_to_leaf n1 bindings1 new_msgs_tl
+      betree_Node_apply_messages_to_leaf_loop n1 bindings1 new_msgs_tl
     | Betree_List_Nil => Ok bindings
     end
   end
 .
 
+(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_leaf]:
+    Source: 'src/betree.rs', lines 463:4-466:5 *)
+Definition betree_Node_apply_messages_to_leaf
+  (n : nat) (bindings : betree_List_t (u64 * u64))
+  (new_msgs : betree_List_t (u64 * betree_Message_t)) :
+  result (betree_List_t (u64 * u64))
+  :=
+  betree_Node_apply_messages_to_leaf_loop n bindings new_msgs
+.
+
 (** [betree::betree::{betree::betree::Internal#4}::flush]:
-    Source: 'src/betree.rs', lines 410:4-415:26 *)
+    Source: 'src/betree.rs', lines 429:4-434:26 *)
 Fixpoint betree_Internal_flush
   (n : nat) (self : betree_Internal_t) (params : betree_Params_t)
   (node_id_cnt : betree_NodeIdCounter_t)
@@ -665,7 +797,7 @@ Fixpoint betree_Internal_flush
   end
 
 (** [betree::betree::{betree::betree::Node#5}::apply_messages]:
-    Source: 'src/betree.rs', lines 588:4-593:5 *)
+    Source: 'src/betree.rs', lines 601:4-606:5 *)
 with betree_Node_apply_messages
   (n : nat) (self : betree_Node_t) (params : betree_Params_t)
   (node_id_cnt : betree_NodeIdCounter_t)
@@ -721,7 +853,7 @@ with betree_Node_apply_messages
 .
 
 (** [betree::betree::{betree::betree::Node#5}::apply]:
-    Source: 'src/betree.rs', lines 576:4-582:5 *)
+    Source: 'src/betree.rs', lines 589:4-595:5 *)
 Definition betree_Node_apply
   (n : nat) (self : betree_Node_t) (params : betree_Params_t)
   (node_id_cnt : betree_NodeIdCounter_t) (key : u64)
@@ -737,7 +869,7 @@ Definition betree_Node_apply
 .
 
 (** [betree::betree::{betree::betree::BeTree#6}::new]:
-    Source: 'src/betree.rs', lines 849:4-849:60 *)
+    Source: 'src/betree.rs', lines 848:4-848:60 *)
 Definition betree_BeTree_new
   (min_flush_size : u64) (split_size : u64) (st : state) :
   result (state * betree_BeTree_t)
@@ -762,7 +894,7 @@ Definition betree_BeTree_new
 .
 
 (** [betree::betree::{betree::betree::BeTree#6}::apply]:
-    Source: 'src/betree.rs', lines 868:4-868:47 *)
+    Source: 'src/betree.rs', lines 867:4-867:47 *)
 Definition betree_BeTree_apply
   (n : nat) (self : betree_BeTree_t) (key : u64) (msg : betree_Message_t)
   (st : state) :
@@ -782,7 +914,7 @@ Definition betree_BeTree_apply
 .
 
 (** [betree::betree::{betree::betree::BeTree#6}::insert]:
-    Source: 'src/betree.rs', lines 874:4-874:52 *)
+    Source: 'src/betree.rs', lines 873:4-873:52 *)
 Definition betree_BeTree_insert
   (n : nat) (self : betree_BeTree_t) (key : u64) (value : u64) (st : state) :
   result (state * betree_BeTree_t)
@@ -791,7 +923,7 @@ Definition betree_BeTree_insert
 .
 
 (** [betree::betree::{betree::betree::BeTree#6}::delete]:
-    Source: 'src/betree.rs', lines 880:4-880:38 *)
+    Source: 'src/betree.rs', lines 879:4-879:38 *)
 Definition betree_BeTree_delete
   (n : nat) (self : betree_BeTree_t) (key : u64) (st : state) :
   result (state * betree_BeTree_t)
@@ -800,7 +932,7 @@ Definition betree_BeTree_delete
 .
 
 (** [betree::betree::{betree::betree::BeTree#6}::upsert]:
-    Source: 'src/betree.rs', lines 886:4-886:59 *)
+    Source: 'src/betree.rs', lines 885:4-885:59 *)
 Definition betree_BeTree_upsert
   (n : nat) (self : betree_BeTree_t) (key : u64)
   (upd : betree_UpsertFunState_t) (st : state) :
@@ -810,7 +942,7 @@ Definition betree_BeTree_upsert
 .
 
 (** [betree::betree::{betree::betree::BeTree#6}::lookup]:
-    Source: 'src/betree.rs', lines 895:4-895:62 *)
+    Source: 'src/betree.rs', lines 894:4-894:62 *)
 Definition betree_BeTree_lookup
   (n : nat) (self : betree_BeTree_t) (key : u64) (st : state) :
   result (state * ((option u64) * betree_BeTree_t))
diff --git a/tests/fstar/betree/Betree.Clauses.Template.fst b/tests/fstar/betree/Betree.Clauses.Template.fst
index fad8c5ba..d3e07c7e 100644
--- a/tests/fstar/betree/Betree.Clauses.Template.fst
+++ b/tests/fstar/betree/Betree.Clauses.Template.fst
@@ -7,100 +7,109 @@ open Betree.Types
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
 (** [betree::betree::{betree::betree::List<T>#1}::len]: decreases clause
-    Source: 'src/betree.rs', lines 276:4-276:24 *)
+    Source: 'src/betree.rs', lines 276:4-284:5 *)
 unfold
-let betree_List_len_decreases (t : Type0) (self : betree_List_t t) : nat =
+let betree_List_len_loop_decreases (t : Type0) (self : betree_List_t t)
+  (len : u64) : nat =
+  admit ()
+
+(** [betree::betree::{betree::betree::List<T>#1}::reverse]: decreases clause
+    Source: 'src/betree.rs', lines 304:4-312:5 *)
+unfold
+let betree_List_reverse_loop_decreases (t : Type0) (self : betree_List_t t)
+  (out : betree_List_t t) : nat =
   admit ()
 
 (** [betree::betree::{betree::betree::List<T>#1}::split_at]: decreases clause
-    Source: 'src/betree.rs', lines 284:4-284:51 *)
+    Source: 'src/betree.rs', lines 287:4-302:5 *)
 unfold
-let betree_List_split_at_decreases (t : Type0) (self : betree_List_t t)
-  (n : u64) : nat =
+let betree_List_split_at_loop_decreases (t : Type0) (n : u64)
+  (beg : betree_List_t t) (self : betree_List_t t) : nat =
   admit ()
 
 (** [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]: decreases clause
-    Source: 'src/betree.rs', lines 339:4-339:73 *)
+    Source: 'src/betree.rs', lines 355:4-370:5 *)
 unfold
-let betree_ListPairU64T_partition_at_pivot_decreases (t : Type0)
-  (self : betree_List_t (u64 & t)) (pivot : u64) : nat =
+let betree_ListPairU64T_partition_at_pivot_loop_decreases (t : Type0)
+  (pivot : u64) (beg : betree_List_t (u64 & t))
+  (end1 : betree_List_t (u64 & t)) (self : betree_List_t (u64 & t)) : nat =
   admit ()
 
 (** [betree::betree::{betree::betree::Node#5}::lookup_first_message_for_key]: decreases clause
-    Source: 'src/betree.rs', lines 789:4-792:34 *)
+    Source: 'src/betree.rs', lines 792:4-810:5 *)
 unfold
-let betree_Node_lookup_first_message_for_key_decreases (key : u64)
+let betree_Node_lookup_first_message_for_key_loop_decreases (key : u64)
   (msgs : betree_List_t (u64 & betree_Message_t)) : nat =
   admit ()
 
 (** [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]: decreases clause
-    Source: 'src/betree.rs', lines 636:4-636:80 *)
+    Source: 'src/betree.rs', lines 649:4-660:5 *)
 unfold
-let betree_Node_lookup_in_bindings_decreases (key : u64)
+let betree_Node_lookup_in_bindings_loop_decreases (key : u64)
   (bindings : betree_List_t (u64 & u64)) : nat =
   admit ()
 
 (** [betree::betree::{betree::betree::Node#5}::apply_upserts]: decreases clause
-    Source: 'src/betree.rs', lines 819:4-819:90 *)
+    Source: 'src/betree.rs', lines 820:4-844:5 *)
 unfold
-let betree_Node_apply_upserts_decreases
+let betree_Node_apply_upserts_loop_decreases
   (msgs : betree_List_t (u64 & betree_Message_t)) (prev : option u64)
   (key : u64) : nat =
   admit ()
 
 (** [betree::betree::{betree::betree::Internal#4}::lookup_in_children]: decreases clause
-    Source: 'src/betree.rs', lines 395:4-395:63 *)
+    Source: 'src/betree.rs', lines 414:4-414:63 *)
 unfold
 let betree_Internal_lookup_in_children_decreases (self : betree_Internal_t)
   (key : u64) (st : state) : nat =
   admit ()
 
 (** [betree::betree::{betree::betree::Node#5}::lookup]: decreases clause
-    Source: 'src/betree.rs', lines 709:4-709:58 *)
+    Source: 'src/betree.rs', lines 712:4-712:58 *)
 unfold
 let betree_Node_lookup_decreases (self : betree_Node_t) (key : u64)
   (st : state) : nat =
   admit ()
 
 (** [betree::betree::{betree::betree::Node#5}::filter_messages_for_key]: decreases clause
-    Source: 'src/betree.rs', lines 674:4-674:77 *)
+    Source: 'src/betree.rs', lines 683:4-692:5 *)
 unfold
-let betree_Node_filter_messages_for_key_decreases (key : u64)
+let betree_Node_filter_messages_for_key_loop_decreases (key : u64)
   (msgs : betree_List_t (u64 & betree_Message_t)) : nat =
   admit ()
 
 (** [betree::betree::{betree::betree::Node#5}::lookup_first_message_after_key]: decreases clause
-    Source: 'src/betree.rs', lines 689:4-692:34 *)
+    Source: 'src/betree.rs', lines 694:4-706:5 *)
 unfold
-let betree_Node_lookup_first_message_after_key_decreases (key : u64)
+let betree_Node_lookup_first_message_after_key_loop_decreases (key : u64)
   (msgs : betree_List_t (u64 & betree_Message_t)) : nat =
   admit ()
 
 (** [betree::betree::{betree::betree::Node#5}::apply_messages_to_internal]: decreases clause
-    Source: 'src/betree.rs', lines 502:4-505:5 *)
+    Source: 'src/betree.rs', lines 518:4-526:5 *)
 unfold
-let betree_Node_apply_messages_to_internal_decreases
+let betree_Node_apply_messages_to_internal_loop_decreases
   (msgs : betree_List_t (u64 & betree_Message_t))
   (new_msgs : betree_List_t (u64 & betree_Message_t)) : nat =
   admit ()
 
 (** [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]: decreases clause
-    Source: 'src/betree.rs', lines 653:4-656:32 *)
+    Source: 'src/betree.rs', lines 664:4-677:5 *)
 unfold
-let betree_Node_lookup_mut_in_bindings_decreases (key : u64)
+let betree_Node_lookup_mut_in_bindings_loop_decreases (key : u64)
   (bindings : betree_List_t (u64 & u64)) : nat =
   admit ()
 
 (** [betree::betree::{betree::betree::Node#5}::apply_messages_to_leaf]: decreases clause
-    Source: 'src/betree.rs', lines 444:4-447:5 *)
+    Source: 'src/betree.rs', lines 463:4-471:5 *)
 unfold
-let betree_Node_apply_messages_to_leaf_decreases
+let betree_Node_apply_messages_to_leaf_loop_decreases
   (bindings : betree_List_t (u64 & u64))
   (new_msgs : betree_List_t (u64 & betree_Message_t)) : nat =
   admit ()
 
 (** [betree::betree::{betree::betree::Internal#4}::flush]: decreases clause
-    Source: 'src/betree.rs', lines 410:4-415:26 *)
+    Source: 'src/betree.rs', lines 429:4-434:26 *)
 unfold
 let betree_Internal_flush_decreases (self : betree_Internal_t)
   (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t)
@@ -108,7 +117,7 @@ let betree_Internal_flush_decreases (self : betree_Internal_t)
   admit ()
 
 (** [betree::betree::{betree::betree::Node#5}::apply_messages]: decreases clause
-    Source: 'src/betree.rs', lines 588:4-593:5 *)
+    Source: 'src/betree.rs', lines 601:4-606:5 *)
 unfold
 let betree_Node_apply_messages_decreases (self : betree_Node_t)
   (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t)
diff --git a/tests/fstar/betree/Betree.Clauses.fst b/tests/fstar/betree/Betree.Clauses.fst
index ae201cee..c50bf421 100644
--- a/tests/fstar/betree/Betree.Clauses.fst
+++ b/tests/fstar/betree/Betree.Clauses.fst
@@ -103,36 +103,46 @@ let wf_nat_pair_lem (p0 p1 : nat_pair) :
 
 (** [betree_main::betree::List::{1}::len]: decreases clause *)
 unfold
-let betree_List_len_decreases (t : Type0) (self : betree_List_t t) : betree_List_t t =
+let betree_List_len_loop_decreases (t : Type0) (self : betree_List_t t) (len : u64) : betree_List_t t =
   self
 
-(** [betree_main::betree::List::{1}::split_at]: decreases clause *)
+(** [betree::betree::{betree::betree::List<T>#1}::reverse]: decreases clause
+    Source: 'src/betree.rs', lines 304:4-312:5 *)
 unfold
-let betree_List_split_at_decreases (t : Type0) (self : betree_List_t t)
-  (n : u64) : nat =
+let betree_List_reverse_loop_decreases (t : Type0) (self : betree_List_t t)
+  (out : betree_List_t t) =
+  self
+
+(** [betree::betree::{betree::betree::List<T>#1}::split_at]: decreases clause
+    Source: 'src/betree.rs', lines 287:4-302:5 *)
+unfold
+let betree_List_split_at_loop_decreases (t : Type0) (n : u64)
+  (beg : betree_List_t t) (self : betree_List_t t) : nat =
   n
 
-(** [betree_main::betree::List::{2}::partition_at_pivot]: decreases clause *)
+(** [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]: decreases clause
+    Source: 'src/betree.rs', lines 355:4-370:5 *)
 unfold
-let betree_ListPairU64T_partition_at_pivot_decreases (t : Type0)
-  (self : betree_List_t (u64 & t)) (pivot : u64) : betree_List_t (u64 & t) =
+let betree_ListPairU64T_partition_at_pivot_loop_decreases (t : Type0)
+  (pivot : u64) (beg : betree_List_t (u64 & t)) (end0 : betree_List_t (u64 & t))
+  (self : betree_List_t (u64 & t)) =
   self
 
 (** [betree_main::betree::Node::{5}::lookup_in_bindings]: decreases clause *)
 unfold
-let betree_Node_lookup_in_bindings_decreases (key : u64)
+let betree_Node_lookup_in_bindings_loop_decreases (key : u64)
   (bindings : betree_List_t (u64 & u64)) : betree_List_t (u64 & u64) =
   bindings
 
 (** [betree_main::betree::Node::{5}::lookup_first_message_for_key]: decreases clause *)
 unfold
-let betree_Node_lookup_first_message_for_key_decreases (key : u64)
+let betree_Node_lookup_first_message_for_key_loop_decreases (key : u64)
   (msgs : betree_List_t (u64 & betree_Message_t)) : betree_List_t (u64 & betree_Message_t) =
   msgs
 
 (** [betree_main::betree::Node::{5}::apply_upserts]: decreases clause *)
 unfold
-let betree_Node_apply_upserts_decreases
+let betree_Node_apply_upserts_loop_decreases
   (msgs : betree_List_t (u64 & betree_Message_t)) (prev : option u64)
   (key : u64) : betree_List_t (u64 & betree_Message_t) =
   msgs
@@ -151,29 +161,29 @@ let betree_Node_lookup_decreases (self : betree_Node_t) (key : u64)
 
 (** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: decreases clause *)
 unfold
-let betree_Node_lookup_mut_in_bindings_decreases (key : u64)
+let betree_Node_lookup_mut_in_bindings_loop_decreases (key : u64)
   (bindings : betree_List_t (u64 & u64)) : betree_List_t (u64 & u64) =
   bindings
 
 unfold
-let betree_Node_apply_messages_to_leaf_decreases
+let betree_Node_apply_messages_to_leaf_loop_decreases
   (bindings : betree_List_t (u64 & u64))
   (new_msgs : betree_List_t (u64 & betree_Message_t)) : betree_List_t (u64 & betree_Message_t) =
   new_msgs
 
 (** [betree_main::betree::Node::{5}::filter_messages_for_key]: decreases clause *)
 unfold
-let betree_Node_filter_messages_for_key_decreases (key : u64)
+let betree_Node_filter_messages_for_key_loop_decreases (key : u64)
   (msgs : betree_List_t (u64 & betree_Message_t)) : betree_List_t (u64 & betree_Message_t) =
   msgs
 
 (** [betree_main::betree::Node::{5}::lookup_first_message_after_key]: decreases clause *)
 unfold
-let betree_Node_lookup_first_message_after_key_decreases (key : u64)
+let betree_Node_lookup_first_message_after_key_loop_decreases (key : u64)
   (msgs : betree_List_t (u64 & betree_Message_t)) : betree_List_t (u64 & betree_Message_t) =
   msgs
 
-let betree_Node_apply_messages_to_internal_decreases
+let betree_Node_apply_messages_to_internal_loop_decreases
   (msgs : betree_List_t (u64 & betree_Message_t))
   (new_msgs : betree_List_t (u64 & betree_Message_t)) : betree_List_t (u64 & betree_Message_t) =
   new_msgs
diff --git a/tests/fstar/betree/Betree.Funs.fst b/tests/fstar/betree/Betree.Funs.fst
index 07f561f5..de3ac13c 100644
--- a/tests/fstar/betree/Betree.Funs.fst
+++ b/tests/fstar/betree/Betree.Funs.fst
@@ -75,45 +75,76 @@ let betree_upsert_update
     end
   end
 
+(** [betree::betree::{betree::betree::List<T>#1}::len]: loop 0:
+    Source: 'src/betree.rs', lines 276:4-284:5 *)
+let rec betree_List_len_loop
+  (t : Type0) (self : betree_List_t t) (len : u64) :
+  Tot (result u64) (decreases (betree_List_len_loop_decreases t self len))
+  =
+  begin match self with
+  | Betree_List_Cons _ tl ->
+    let* len1 = u64_add len 1 in betree_List_len_loop t tl len1
+  | Betree_List_Nil -> Ok len
+  end
+
 (** [betree::betree::{betree::betree::List<T>#1}::len]:
     Source: 'src/betree.rs', lines 276:4-276:24 *)
-let rec betree_List_len
-  (t : Type0) (self : betree_List_t t) :
-  Tot (result u64) (decreases (betree_List_len_decreases t self))
+let betree_List_len (t : Type0) (self : betree_List_t t) : result u64 =
+  betree_List_len_loop t self 0
+
+(** [betree::betree::{betree::betree::List<T>#1}::reverse]: loop 0:
+    Source: 'src/betree.rs', lines 304:4-312:5 *)
+let rec betree_List_reverse_loop
+  (t : Type0) (self : betree_List_t t) (out : betree_List_t t) :
+  Tot (result (betree_List_t t))
+  (decreases (betree_List_reverse_loop_decreases t self out))
   =
   begin match self with
-  | Betree_List_Cons _ tl -> let* i = betree_List_len t tl in u64_add 1 i
-  | Betree_List_Nil -> Ok 0
+  | Betree_List_Cons hd tl ->
+    betree_List_reverse_loop t tl (Betree_List_Cons hd out)
+  | Betree_List_Nil -> Ok out
   end
 
-(** [betree::betree::{betree::betree::List<T>#1}::split_at]:
-    Source: 'src/betree.rs', lines 284:4-284:51 *)
-let rec betree_List_split_at
-  (t : Type0) (self : betree_List_t t) (n : u64) :
+(** [betree::betree::{betree::betree::List<T>#1}::reverse]:
+    Source: 'src/betree.rs', lines 304:4-304:32 *)
+let betree_List_reverse
+  (t : Type0) (self : betree_List_t t) : result (betree_List_t t) =
+  betree_List_reverse_loop t self Betree_List_Nil
+
+(** [betree::betree::{betree::betree::List<T>#1}::split_at]: loop 0:
+    Source: 'src/betree.rs', lines 287:4-302:5 *)
+let rec betree_List_split_at_loop
+  (t : Type0) (n : u64) (beg : betree_List_t t) (self : betree_List_t t) :
   Tot (result ((betree_List_t t) & (betree_List_t t)))
-  (decreases (betree_List_split_at_decreases t self n))
+  (decreases (betree_List_split_at_loop_decreases t n beg self))
   =
-  if n = 0
-  then Ok (Betree_List_Nil, self)
-  else
+  if n > 0
+  then
     begin match self with
     | Betree_List_Cons hd tl ->
-      let* i = u64_sub n 1 in
-      let* p = betree_List_split_at t tl i in
-      let (ls0, ls1) = p in
-      Ok (Betree_List_Cons hd ls0, ls1)
+      let* n1 = u64_sub n 1 in
+      betree_List_split_at_loop t n1 (Betree_List_Cons hd beg) tl
     | Betree_List_Nil -> Fail Failure
     end
+  else let* l = betree_List_reverse t beg in Ok (l, self)
+
+(** [betree::betree::{betree::betree::List<T>#1}::split_at]:
+    Source: 'src/betree.rs', lines 287:4-287:55 *)
+let betree_List_split_at
+  (t : Type0) (self : betree_List_t t) (n : u64) :
+  result ((betree_List_t t) & (betree_List_t t))
+  =
+  betree_List_split_at_loop t n Betree_List_Nil self
 
 (** [betree::betree::{betree::betree::List<T>#1}::push_front]:
-    Source: 'src/betree.rs', lines 299:4-299:34 *)
+    Source: 'src/betree.rs', lines 315:4-315:34 *)
 let betree_List_push_front
   (t : Type0) (self : betree_List_t t) (x : t) : result (betree_List_t t) =
   let (tl, _) = core_mem_replace (betree_List_t t) self Betree_List_Nil in
   Ok (Betree_List_Cons x tl)
 
 (** [betree::betree::{betree::betree::List<T>#1}::pop_front]:
-    Source: 'src/betree.rs', lines 306:4-306:32 *)
+    Source: 'src/betree.rs', lines 322:4-322:32 *)
 let betree_List_pop_front
   (t : Type0) (self : betree_List_t t) : result (t & (betree_List_t t)) =
   let (ls, _) = core_mem_replace (betree_List_t t) self Betree_List_Nil in
@@ -123,7 +154,7 @@ let betree_List_pop_front
   end
 
 (** [betree::betree::{betree::betree::List<T>#1}::hd]:
-    Source: 'src/betree.rs', lines 318:4-318:22 *)
+    Source: 'src/betree.rs', lines 334:4-334:22 *)
 let betree_List_hd (t : Type0) (self : betree_List_t t) : result t =
   begin match self with
   | Betree_List_Cons hd _ -> Ok hd
@@ -131,7 +162,7 @@ let betree_List_hd (t : Type0) (self : betree_List_t t) : result t =
   end
 
 (** [betree::betree::{betree::betree::List<(u64, T)>#2}::head_has_key]:
-    Source: 'src/betree.rs', lines 327:4-327:44 *)
+    Source: 'src/betree.rs', lines 343:4-343:44 *)
 let betree_ListPairU64T_head_has_key
   (t : Type0) (self : betree_List_t (u64 & t)) (key : u64) : result bool =
   begin match self with
@@ -139,27 +170,43 @@ let betree_ListPairU64T_head_has_key
   | Betree_List_Nil -> Ok false
   end
 
-(** [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]:
-    Source: 'src/betree.rs', lines 339:4-339:73 *)
-let rec betree_ListPairU64T_partition_at_pivot
-  (t : Type0) (self : betree_List_t (u64 & t)) (pivot : u64) :
+(** [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]: loop 0:
+    Source: 'src/betree.rs', lines 355:4-370:5 *)
+let rec betree_ListPairU64T_partition_at_pivot_loop
+  (t : Type0) (pivot : u64) (beg : betree_List_t (u64 & t))
+  (end1 : betree_List_t (u64 & t)) (self : betree_List_t (u64 & t)) :
   Tot (result ((betree_List_t (u64 & t)) & (betree_List_t (u64 & t))))
-  (decreases (betree_ListPairU64T_partition_at_pivot_decreases t self pivot))
+  (decreases (
+    betree_ListPairU64T_partition_at_pivot_loop_decreases t pivot beg end1
+      self))
   =
   begin match self with
   | Betree_List_Cons hd tl ->
     let (i, x) = hd in
     if i >= pivot
-    then Ok (Betree_List_Nil, Betree_List_Cons (i, x) tl)
+    then
+      betree_ListPairU64T_partition_at_pivot_loop t pivot beg (Betree_List_Cons
+        (i, x) end1) tl
     else
-      let* p = betree_ListPairU64T_partition_at_pivot t tl pivot in
-      let (ls0, ls1) = p in
-      Ok (Betree_List_Cons (i, x) ls0, ls1)
-  | Betree_List_Nil -> Ok (Betree_List_Nil, Betree_List_Nil)
+      betree_ListPairU64T_partition_at_pivot_loop t pivot (Betree_List_Cons (i,
+        x) beg) end1 tl
+  | Betree_List_Nil ->
+    let* l = betree_List_reverse (u64 & t) beg in
+    let* l1 = betree_List_reverse (u64 & t) end1 in
+    Ok (l, l1)
   end
 
+(** [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]:
+    Source: 'src/betree.rs', lines 355:4-355:73 *)
+let betree_ListPairU64T_partition_at_pivot
+  (t : Type0) (self : betree_List_t (u64 & t)) (pivot : u64) :
+  result ((betree_List_t (u64 & t)) & (betree_List_t (u64 & t)))
+  =
+  betree_ListPairU64T_partition_at_pivot_loop t pivot Betree_List_Nil
+    Betree_List_Nil self
+
 (** [betree::betree::{betree::betree::Leaf#3}::split]:
-    Source: 'src/betree.rs', lines 359:4-364:17 *)
+    Source: 'src/betree.rs', lines 378:4-383:17 *)
 let betree_Leaf_split
   (self : betree_Leaf_t) (content : betree_List_t (u64 & u64))
   (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t)
@@ -179,13 +226,14 @@ let betree_Leaf_split
   Ok (st2, ({ id = self.id; pivot = pivot; left = n; right = n1 },
     node_id_cnt2))
 
-(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_for_key]:
-    Source: 'src/betree.rs', lines 789:4-792:34 *)
-let rec betree_Node_lookup_first_message_for_key
+(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_for_key]: loop 0:
+    Source: 'src/betree.rs', lines 792:4-810:5 *)
+let rec betree_Node_lookup_first_message_for_key_loop
   (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) :
   Tot (result ((betree_List_t (u64 & betree_Message_t)) & (betree_List_t (u64 &
     betree_Message_t) -> result (betree_List_t (u64 & betree_Message_t)))))
-  (decreases (betree_Node_lookup_first_message_for_key_decreases key msgs))
+  (decreases (
+    betree_Node_lookup_first_message_for_key_loop_decreases key msgs))
   =
   begin match msgs with
   | Betree_List_Cons x next_msgs ->
@@ -193,39 +241,55 @@ let rec betree_Node_lookup_first_message_for_key
     if i >= key
     then Ok (Betree_List_Cons (i, m) next_msgs, Ok)
     else
-      let* (l, lookup_first_message_for_key_back) =
-        betree_Node_lookup_first_message_for_key key next_msgs in
-      let back =
+      let* (l, back) =
+        betree_Node_lookup_first_message_for_key_loop key next_msgs in
+      let back1 =
         fun ret ->
-          let* next_msgs1 = lookup_first_message_for_key_back ret in
-          Ok (Betree_List_Cons (i, m) next_msgs1) in
-      Ok (l, back)
+          let* next_msgs1 = back ret in Ok (Betree_List_Cons (i, m) next_msgs1)
+        in
+      Ok (l, back1)
   | Betree_List_Nil -> Ok (Betree_List_Nil, Ok)
   end
 
-(** [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]:
-    Source: 'src/betree.rs', lines 636:4-636:80 *)
-let rec betree_Node_lookup_in_bindings
+(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_for_key]:
+    Source: 'src/betree.rs', lines 792:4-795:34 *)
+let betree_Node_lookup_first_message_for_key
+  (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) :
+  result ((betree_List_t (u64 & betree_Message_t)) & (betree_List_t (u64 &
+    betree_Message_t) -> result (betree_List_t (u64 & betree_Message_t))))
+  =
+  betree_Node_lookup_first_message_for_key_loop key msgs
+
+(** [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]: loop 0:
+    Source: 'src/betree.rs', lines 649:4-660:5 *)
+let rec betree_Node_lookup_in_bindings_loop
   (key : u64) (bindings : betree_List_t (u64 & u64)) :
   Tot (result (option u64))
-  (decreases (betree_Node_lookup_in_bindings_decreases key bindings))
+  (decreases (betree_Node_lookup_in_bindings_loop_decreases key bindings))
   =
   begin match bindings with
   | Betree_List_Cons hd tl ->
     let (i, i1) = hd in
     if i = key
     then Ok (Some i1)
-    else if i > key then Ok None else betree_Node_lookup_in_bindings key tl
+    else
+      if i > key then Ok None else betree_Node_lookup_in_bindings_loop key tl
   | Betree_List_Nil -> Ok None
   end
 
-(** [betree::betree::{betree::betree::Node#5}::apply_upserts]:
-    Source: 'src/betree.rs', lines 819:4-819:90 *)
-let rec betree_Node_apply_upserts
+(** [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]:
+    Source: 'src/betree.rs', lines 649:4-649:84 *)
+let betree_Node_lookup_in_bindings
+  (key : u64) (bindings : betree_List_t (u64 & u64)) : result (option u64) =
+  betree_Node_lookup_in_bindings_loop key bindings
+
+(** [betree::betree::{betree::betree::Node#5}::apply_upserts]: loop 0:
+    Source: 'src/betree.rs', lines 820:4-844:5 *)
+let rec betree_Node_apply_upserts_loop
   (msgs : betree_List_t (u64 & betree_Message_t)) (prev : option u64)
   (key : u64) :
   Tot (result (u64 & (betree_List_t (u64 & betree_Message_t))))
-  (decreases (betree_Node_apply_upserts_decreases msgs prev key))
+  (decreases (betree_Node_apply_upserts_loop_decreases msgs prev key))
   =
   let* b = betree_ListPairU64T_head_has_key betree_Message_t msgs key in
   if b
@@ -237,7 +301,7 @@ let rec betree_Node_apply_upserts
     | Betree_Message_Delete -> Fail Failure
     | Betree_Message_Upsert s ->
       let* v = betree_upsert_update prev s in
-      betree_Node_apply_upserts msgs1 (Some v) key
+      betree_Node_apply_upserts_loop msgs1 (Some v) key
     end
   else
     let* v = core_option_Option_unwrap u64 prev in
@@ -246,8 +310,17 @@ let rec betree_Node_apply_upserts
         Betree_Message_Insert v) in
     Ok (v, msgs1)
 
+(** [betree::betree::{betree::betree::Node#5}::apply_upserts]:
+    Source: 'src/betree.rs', lines 820:4-820:94 *)
+let betree_Node_apply_upserts
+  (msgs : betree_List_t (u64 & betree_Message_t)) (prev : option u64)
+  (key : u64) :
+  result (u64 & (betree_List_t (u64 & betree_Message_t)))
+  =
+  betree_Node_apply_upserts_loop msgs prev key
+
 (** [betree::betree::{betree::betree::Internal#4}::lookup_in_children]:
-    Source: 'src/betree.rs', lines 395:4-395:63 *)
+    Source: 'src/betree.rs', lines 414:4-414:63 *)
 let rec betree_Internal_lookup_in_children
   (self : betree_Internal_t) (key : u64) (st : state) :
   Tot (result (state & ((option u64) & betree_Internal_t)))
@@ -262,7 +335,7 @@ let rec betree_Internal_lookup_in_children
     Ok (st1, (o, { self with right = n }))
 
 (** [betree::betree::{betree::betree::Node#5}::lookup]:
-    Source: 'src/betree.rs', lines 709:4-709:58 *)
+    Source: 'src/betree.rs', lines 712:4-712:58 *)
 and betree_Node_lookup
   (self : betree_Node_t) (key : u64) (st : state) :
   Tot (result (state & ((option u64) & betree_Node_t)))
@@ -317,12 +390,12 @@ and betree_Node_lookup
     Ok (st1, (o, Betree_Node_Leaf node))
   end
 
-(** [betree::betree::{betree::betree::Node#5}::filter_messages_for_key]:
-    Source: 'src/betree.rs', lines 674:4-674:77 *)
-let rec betree_Node_filter_messages_for_key
+(** [betree::betree::{betree::betree::Node#5}::filter_messages_for_key]: loop 0:
+    Source: 'src/betree.rs', lines 683:4-692:5 *)
+let rec betree_Node_filter_messages_for_key_loop
   (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) :
   Tot (result (betree_List_t (u64 & betree_Message_t)))
-  (decreases (betree_Node_filter_messages_for_key_decreases key msgs))
+  (decreases (betree_Node_filter_messages_for_key_loop_decreases key msgs))
   =
   begin match msgs with
   | Betree_List_Cons p l ->
@@ -332,37 +405,55 @@ let rec betree_Node_filter_messages_for_key
       let* (_, msgs1) =
         betree_List_pop_front (u64 & betree_Message_t) (Betree_List_Cons (k, m)
           l) in
-      betree_Node_filter_messages_for_key key msgs1
+      betree_Node_filter_messages_for_key_loop key msgs1
     else Ok (Betree_List_Cons (k, m) l)
   | Betree_List_Nil -> Ok Betree_List_Nil
   end
 
-(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_after_key]:
-    Source: 'src/betree.rs', lines 689:4-692:34 *)
-let rec betree_Node_lookup_first_message_after_key
+(** [betree::betree::{betree::betree::Node#5}::filter_messages_for_key]:
+    Source: 'src/betree.rs', lines 683:4-683:77 *)
+let betree_Node_filter_messages_for_key
+  (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) :
+  result (betree_List_t (u64 & betree_Message_t))
+  =
+  betree_Node_filter_messages_for_key_loop key msgs
+
+(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_after_key]: loop 0:
+    Source: 'src/betree.rs', lines 694:4-706:5 *)
+let rec betree_Node_lookup_first_message_after_key_loop
   (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) :
   Tot (result ((betree_List_t (u64 & betree_Message_t)) & (betree_List_t (u64 &
     betree_Message_t) -> result (betree_List_t (u64 & betree_Message_t)))))
-  (decreases (betree_Node_lookup_first_message_after_key_decreases key msgs))
+  (decreases (
+    betree_Node_lookup_first_message_after_key_loop_decreases key msgs))
   =
   begin match msgs with
   | Betree_List_Cons p next_msgs ->
     let (k, m) = p in
     if k = key
     then
-      let* (l, lookup_first_message_after_key_back) =
-        betree_Node_lookup_first_message_after_key key next_msgs in
-      let back =
+      let* (l, back) =
+        betree_Node_lookup_first_message_after_key_loop key next_msgs in
+      let back1 =
         fun ret ->
-          let* next_msgs1 = lookup_first_message_after_key_back ret in
-          Ok (Betree_List_Cons (k, m) next_msgs1) in
-      Ok (l, back)
+          let* next_msgs1 = back ret in Ok (Betree_List_Cons (k, m) next_msgs1)
+        in
+      Ok (l, back1)
     else Ok (Betree_List_Cons (k, m) next_msgs, Ok)
   | Betree_List_Nil -> Ok (Betree_List_Nil, Ok)
   end
 
+(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_after_key]:
+    Source: 'src/betree.rs', lines 694:4-697:34 *)
+let betree_Node_lookup_first_message_after_key
+  (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) :
+  result ((betree_List_t (u64 & betree_Message_t)) & (betree_List_t (u64 &
+    betree_Message_t) -> result (betree_List_t (u64 & betree_Message_t))))
+  =
+  betree_Node_lookup_first_message_after_key_loop key msgs
+
 (** [betree::betree::{betree::betree::Node#5}::apply_to_internal]:
-    Source: 'src/betree.rs', lines 521:4-521:89 *)
+    Source: 'src/betree.rs', lines 534:4-534:89 *)
 let betree_Node_apply_to_internal
   (msgs : betree_List_t (u64 & betree_Message_t)) (key : u64)
   (new_msg : betree_Message_t) :
@@ -421,29 +512,39 @@ let betree_Node_apply_to_internal
       betree_List_push_front (u64 & betree_Message_t) msgs1 (key, new_msg) in
     lookup_first_message_for_key_back msgs2
 
-(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_internal]:
-    Source: 'src/betree.rs', lines 502:4-505:5 *)
-let rec betree_Node_apply_messages_to_internal
+(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_internal]: loop 0:
+    Source: 'src/betree.rs', lines 518:4-526:5 *)
+let rec betree_Node_apply_messages_to_internal_loop
   (msgs : betree_List_t (u64 & betree_Message_t))
   (new_msgs : betree_List_t (u64 & betree_Message_t)) :
   Tot (result (betree_List_t (u64 & betree_Message_t)))
-  (decreases (betree_Node_apply_messages_to_internal_decreases msgs new_msgs))
+  (decreases (
+    betree_Node_apply_messages_to_internal_loop_decreases msgs new_msgs))
   =
   begin match new_msgs with
   | Betree_List_Cons new_msg new_msgs_tl ->
     let (i, m) = new_msg in
     let* msgs1 = betree_Node_apply_to_internal msgs i m in
-    betree_Node_apply_messages_to_internal msgs1 new_msgs_tl
+    betree_Node_apply_messages_to_internal_loop msgs1 new_msgs_tl
   | Betree_List_Nil -> Ok msgs
   end
 
-(** [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]:
-    Source: 'src/betree.rs', lines 653:4-656:32 *)
-let rec betree_Node_lookup_mut_in_bindings
+(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_internal]:
+    Source: 'src/betree.rs', lines 518:4-521:5 *)
+let betree_Node_apply_messages_to_internal
+  (msgs : betree_List_t (u64 & betree_Message_t))
+  (new_msgs : betree_List_t (u64 & betree_Message_t)) :
+  result (betree_List_t (u64 & betree_Message_t))
+  =
+  betree_Node_apply_messages_to_internal_loop msgs new_msgs
+
+(** [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]: loop 0:
+    Source: 'src/betree.rs', lines 664:4-677:5 *)
+let rec betree_Node_lookup_mut_in_bindings_loop
   (key : u64) (bindings : betree_List_t (u64 & u64)) :
   Tot (result ((betree_List_t (u64 & u64)) & (betree_List_t (u64 & u64) ->
     result (betree_List_t (u64 & u64)))))
-  (decreases (betree_Node_lookup_mut_in_bindings_decreases key bindings))
+  (decreases (betree_Node_lookup_mut_in_bindings_loop_decreases key bindings))
   =
   begin match bindings with
   | Betree_List_Cons hd tl ->
@@ -451,18 +552,24 @@ let rec betree_Node_lookup_mut_in_bindings
     if i >= key
     then Ok (Betree_List_Cons (i, i1) tl, Ok)
     else
-      let* (l, lookup_mut_in_bindings_back) =
-        betree_Node_lookup_mut_in_bindings key tl in
-      let back =
-        fun ret ->
-          let* tl1 = lookup_mut_in_bindings_back ret in
-          Ok (Betree_List_Cons (i, i1) tl1) in
-      Ok (l, back)
+      let* (l, back) = betree_Node_lookup_mut_in_bindings_loop key tl in
+      let back1 =
+        fun ret -> let* tl1 = back ret in Ok (Betree_List_Cons (i, i1) tl1) in
+      Ok (l, back1)
   | Betree_List_Nil -> Ok (Betree_List_Nil, Ok)
   end
 
+(** [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]:
+    Source: 'src/betree.rs', lines 664:4-667:32 *)
+let betree_Node_lookup_mut_in_bindings
+  (key : u64) (bindings : betree_List_t (u64 & u64)) :
+  result ((betree_List_t (u64 & u64)) & (betree_List_t (u64 & u64) -> result
+    (betree_List_t (u64 & u64))))
+  =
+  betree_Node_lookup_mut_in_bindings_loop key bindings
+
 (** [betree::betree::{betree::betree::Node#5}::apply_to_leaf]:
-    Source: 'src/betree.rs', lines 460:4-460:87 *)
+    Source: 'src/betree.rs', lines 476:4-476:87 *)
 let betree_Node_apply_to_leaf
   (bindings : betree_List_t (u64 & u64)) (key : u64)
   (new_msg : betree_Message_t) :
@@ -497,24 +604,34 @@ let betree_Node_apply_to_leaf
       lookup_mut_in_bindings_back bindings2
     end
 
-(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_leaf]:
-    Source: 'src/betree.rs', lines 444:4-447:5 *)
-let rec betree_Node_apply_messages_to_leaf
+(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_leaf]: loop 0:
+    Source: 'src/betree.rs', lines 463:4-471:5 *)
+let rec betree_Node_apply_messages_to_leaf_loop
   (bindings : betree_List_t (u64 & u64))
   (new_msgs : betree_List_t (u64 & betree_Message_t)) :
   Tot (result (betree_List_t (u64 & u64)))
-  (decreases (betree_Node_apply_messages_to_leaf_decreases bindings new_msgs))
+  (decreases (
+    betree_Node_apply_messages_to_leaf_loop_decreases bindings new_msgs))
   =
   begin match new_msgs with
   | Betree_List_Cons new_msg new_msgs_tl ->
     let (i, m) = new_msg in
     let* bindings1 = betree_Node_apply_to_leaf bindings i m in
-    betree_Node_apply_messages_to_leaf bindings1 new_msgs_tl
+    betree_Node_apply_messages_to_leaf_loop bindings1 new_msgs_tl
   | Betree_List_Nil -> Ok bindings
   end
 
+(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_leaf]:
+    Source: 'src/betree.rs', lines 463:4-466:5 *)
+let betree_Node_apply_messages_to_leaf
+  (bindings : betree_List_t (u64 & u64))
+  (new_msgs : betree_List_t (u64 & betree_Message_t)) :
+  result (betree_List_t (u64 & u64))
+  =
+  betree_Node_apply_messages_to_leaf_loop bindings new_msgs
+
 (** [betree::betree::{betree::betree::Internal#4}::flush]:
-    Source: 'src/betree.rs', lines 410:4-415:26 *)
+    Source: 'src/betree.rs', lines 429:4-434:26 *)
 let rec betree_Internal_flush
   (self : betree_Internal_t) (params : betree_Params_t)
   (node_id_cnt : betree_NodeIdCounter_t)
@@ -551,7 +668,7 @@ let rec betree_Internal_flush
     Ok (st1, (msgs_left, ({ self with right = n }, node_id_cnt1)))
 
 (** [betree::betree::{betree::betree::Node#5}::apply_messages]:
-    Source: 'src/betree.rs', lines 588:4-593:5 *)
+    Source: 'src/betree.rs', lines 601:4-606:5 *)
 and betree_Node_apply_messages
   (self : betree_Node_t) (params : betree_Params_t)
   (node_id_cnt : betree_NodeIdCounter_t)
@@ -592,7 +709,7 @@ and betree_Node_apply_messages
   end
 
 (** [betree::betree::{betree::betree::Node#5}::apply]:
-    Source: 'src/betree.rs', lines 576:4-582:5 *)
+    Source: 'src/betree.rs', lines 589:4-595:5 *)
 let betree_Node_apply
   (self : betree_Node_t) (params : betree_Params_t)
   (node_id_cnt : betree_NodeIdCounter_t) (key : u64)
@@ -606,7 +723,7 @@ let betree_Node_apply
   Ok (st1, (self1, node_id_cnt1))
 
 (** [betree::betree::{betree::betree::BeTree#6}::new]:
-    Source: 'src/betree.rs', lines 849:4-849:60 *)
+    Source: 'src/betree.rs', lines 848:4-848:60 *)
 let betree_BeTree_new
   (min_flush_size : u64) (split_size : u64) (st : state) :
   result (state & betree_BeTree_t)
@@ -622,7 +739,7 @@ let betree_BeTree_new
     })
 
 (** [betree::betree::{betree::betree::BeTree#6}::apply]:
-    Source: 'src/betree.rs', lines 868:4-868:47 *)
+    Source: 'src/betree.rs', lines 867:4-867:47 *)
 let betree_BeTree_apply
   (self : betree_BeTree_t) (key : u64) (msg : betree_Message_t) (st : state) :
   result (state & betree_BeTree_t)
@@ -633,7 +750,7 @@ let betree_BeTree_apply
   Ok (st1, { self with node_id_cnt = nic; root = n })
 
 (** [betree::betree::{betree::betree::BeTree#6}::insert]:
-    Source: 'src/betree.rs', lines 874:4-874:52 *)
+    Source: 'src/betree.rs', lines 873:4-873:52 *)
 let betree_BeTree_insert
   (self : betree_BeTree_t) (key : u64) (value : u64) (st : state) :
   result (state & betree_BeTree_t)
@@ -641,7 +758,7 @@ let betree_BeTree_insert
   betree_BeTree_apply self key (Betree_Message_Insert value) st
 
 (** [betree::betree::{betree::betree::BeTree#6}::delete]:
-    Source: 'src/betree.rs', lines 880:4-880:38 *)
+    Source: 'src/betree.rs', lines 879:4-879:38 *)
 let betree_BeTree_delete
   (self : betree_BeTree_t) (key : u64) (st : state) :
   result (state & betree_BeTree_t)
@@ -649,7 +766,7 @@ let betree_BeTree_delete
   betree_BeTree_apply self key Betree_Message_Delete st
 
 (** [betree::betree::{betree::betree::BeTree#6}::upsert]:
-    Source: 'src/betree.rs', lines 886:4-886:59 *)
+    Source: 'src/betree.rs', lines 885:4-885:59 *)
 let betree_BeTree_upsert
   (self : betree_BeTree_t) (key : u64) (upd : betree_UpsertFunState_t)
   (st : state) :
@@ -658,7 +775,7 @@ let betree_BeTree_upsert
   betree_BeTree_apply self key (Betree_Message_Upsert upd) st
 
 (** [betree::betree::{betree::betree::BeTree#6}::lookup]:
-    Source: 'src/betree.rs', lines 895:4-895:62 *)
+    Source: 'src/betree.rs', lines 894:4-894:62 *)
 let betree_BeTree_lookup
   (self : betree_BeTree_t) (key : u64) (st : state) :
   result (state & ((option u64) & betree_BeTree_t))
diff --git a/tests/lean/Betree/Funs.lean b/tests/lean/Betree/Funs.lean
index 8612ccbc..7d8b4714 100644
--- a/tests/lean/Betree/Funs.lean
+++ b/tests/lean/Betree/Funs.lean
@@ -79,42 +79,74 @@ def betree.upsert_update
       then prev1 - v
       else Result.ok 0#u64
 
+/- [betree::betree::{betree::betree::List<T>#1}::len]: loop 0:
+   Source: 'src/betree.rs', lines 276:4-284:5 -/
+divergent def betree.List.len_loop
+  (T : Type) (self : betree.List T) (len : U64) : Result U64 :=
+  match self with
+  | betree.List.Cons _ tl =>
+    do
+    let len1 ← len + 1#u64
+    betree.List.len_loop T tl len1
+  | betree.List.Nil => Result.ok len
+
 /- [betree::betree::{betree::betree::List<T>#1}::len]:
    Source: 'src/betree.rs', lines 276:4-276:24 -/
-divergent def betree.List.len (T : Type) (self : betree.List T) : Result U64 :=
+def betree.List.len (T : Type) (self : betree.List T) : Result U64 :=
+  betree.List.len_loop T self 0#u64
+
+/- [betree::betree::{betree::betree::List<T>#1}::reverse]: loop 0:
+   Source: 'src/betree.rs', lines 304:4-312:5 -/
+divergent def betree.List.reverse_loop
+  (T : Type) (self : betree.List T) (out : betree.List T) :
+  Result (betree.List T)
+  :=
   match self with
-  | betree.List.Cons _ tl => do
-                             let i ← betree.List.len T tl
-                             1#u64 + i
-  | betree.List.Nil => Result.ok 0#u64
-
-/- [betree::betree::{betree::betree::List<T>#1}::split_at]:
-   Source: 'src/betree.rs', lines 284:4-284:51 -/
-divergent def betree.List.split_at
-  (T : Type) (self : betree.List T) (n : U64) :
+  | betree.List.Cons hd tl =>
+    betree.List.reverse_loop T tl (betree.List.Cons hd out)
+  | betree.List.Nil => Result.ok out
+
+/- [betree::betree::{betree::betree::List<T>#1}::reverse]:
+   Source: 'src/betree.rs', lines 304:4-304:32 -/
+def betree.List.reverse
+  (T : Type) (self : betree.List T) : Result (betree.List T) :=
+  betree.List.reverse_loop T self betree.List.Nil
+
+/- [betree::betree::{betree::betree::List<T>#1}::split_at]: loop 0:
+   Source: 'src/betree.rs', lines 287:4-302:5 -/
+divergent def betree.List.split_at_loop
+  (T : Type) (n : U64) (beg : betree.List T) (self : betree.List T) :
   Result ((betree.List T) × (betree.List T))
   :=
-  if n = 0#u64
-  then Result.ok (betree.List.Nil, self)
-  else
+  if n > 0#u64
+  then
     match self with
     | betree.List.Cons hd tl =>
       do
-      let i ← n - 1#u64
-      let p ← betree.List.split_at T tl i
-      let (ls0, ls1) := p
-      Result.ok (betree.List.Cons hd ls0, ls1)
+      let n1 ← n - 1#u64
+      betree.List.split_at_loop T n1 (betree.List.Cons hd beg) tl
     | betree.List.Nil => Result.fail .panic
+  else do
+       let l ← betree.List.reverse T beg
+       Result.ok (l, self)
+
+/- [betree::betree::{betree::betree::List<T>#1}::split_at]:
+   Source: 'src/betree.rs', lines 287:4-287:55 -/
+def betree.List.split_at
+  (T : Type) (self : betree.List T) (n : U64) :
+  Result ((betree.List T) × (betree.List T))
+  :=
+  betree.List.split_at_loop T n betree.List.Nil self
 
 /- [betree::betree::{betree::betree::List<T>#1}::push_front]:
-   Source: 'src/betree.rs', lines 299:4-299:34 -/
+   Source: 'src/betree.rs', lines 315:4-315:34 -/
 def betree.List.push_front
   (T : Type) (self : betree.List T) (x : T) : Result (betree.List T) :=
   let (tl, _) := core.mem.replace (betree.List T) self betree.List.Nil
   Result.ok (betree.List.Cons x tl)
 
 /- [betree::betree::{betree::betree::List<T>#1}::pop_front]:
-   Source: 'src/betree.rs', lines 306:4-306:32 -/
+   Source: 'src/betree.rs', lines 322:4-322:32 -/
 def betree.List.pop_front
   (T : Type) (self : betree.List T) : Result (T × (betree.List T)) :=
   let (ls, _) := core.mem.replace (betree.List T) self betree.List.Nil
@@ -123,14 +155,14 @@ def betree.List.pop_front
   | betree.List.Nil => Result.fail .panic
 
 /- [betree::betree::{betree::betree::List<T>#1}::hd]:
-   Source: 'src/betree.rs', lines 318:4-318:22 -/
+   Source: 'src/betree.rs', lines 334:4-334:22 -/
 def betree.List.hd (T : Type) (self : betree.List T) : Result T :=
   match self with
   | betree.List.Cons hd _ => Result.ok hd
   | betree.List.Nil => Result.fail .panic
 
 /- [betree::betree::{betree::betree::List<(u64, T)>#2}::head_has_key]:
-   Source: 'src/betree.rs', lines 327:4-327:44 -/
+   Source: 'src/betree.rs', lines 343:4-343:44 -/
 def betree.ListPairU64T.head_has_key
   (T : Type) (self : betree.List (U64 × T)) (key : U64) : Result Bool :=
   match self with
@@ -138,26 +170,40 @@ def betree.ListPairU64T.head_has_key
                              Result.ok (i = key)
   | betree.List.Nil => Result.ok false
 
-/- [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]:
-   Source: 'src/betree.rs', lines 339:4-339:73 -/
-divergent def betree.ListPairU64T.partition_at_pivot
-  (T : Type) (self : betree.List (U64 × T)) (pivot : U64) :
+/- [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]: loop 0:
+   Source: 'src/betree.rs', lines 355:4-370:5 -/
+divergent def betree.ListPairU64T.partition_at_pivot_loop
+  (T : Type) (pivot : U64) (beg : betree.List (U64 × T))
+  (end1 : betree.List (U64 × T)) (self : betree.List (U64 × T)) :
   Result ((betree.List (U64 × T)) × (betree.List (U64 × T)))
   :=
   match self with
   | betree.List.Cons hd tl =>
     let (i, t) := hd
     if i >= pivot
-    then Result.ok (betree.List.Nil, betree.List.Cons (i, t) tl)
+    then
+      betree.ListPairU64T.partition_at_pivot_loop T pivot beg (betree.List.Cons
+        (i, t) end1) tl
     else
-      do
-      let p ← betree.ListPairU64T.partition_at_pivot T tl pivot
-      let (ls0, ls1) := p
-      Result.ok (betree.List.Cons (i, t) ls0, ls1)
-  | betree.List.Nil => Result.ok (betree.List.Nil, betree.List.Nil)
+      betree.ListPairU64T.partition_at_pivot_loop T pivot (betree.List.Cons (i,
+        t) beg) end1 tl
+  | betree.List.Nil =>
+    do
+    let l ← betree.List.reverse (U64 × T) beg
+    let l1 ← betree.List.reverse (U64 × T) end1
+    Result.ok (l, l1)
+
+/- [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]:
+   Source: 'src/betree.rs', lines 355:4-355:73 -/
+def betree.ListPairU64T.partition_at_pivot
+  (T : Type) (self : betree.List (U64 × T)) (pivot : U64) :
+  Result ((betree.List (U64 × T)) × (betree.List (U64 × T)))
+  :=
+  betree.ListPairU64T.partition_at_pivot_loop T pivot betree.List.Nil
+    betree.List.Nil self
 
 /- [betree::betree::{betree::betree::Leaf#3}::split]:
-   Source: 'src/betree.rs', lines 359:4-364:17 -/
+   Source: 'src/betree.rs', lines 378:4-383:17 -/
 def betree.Leaf.split
   (self : betree.Leaf) (content : betree.List (U64 × U64))
   (params : betree.Params) (node_id_cnt : betree.NodeIdCounter) (st : State) :
@@ -176,9 +222,9 @@ def betree.Leaf.split
   let n1 := betree.Node.Leaf { id := id1, size := params.split_size }
   Result.ok (st2, (betree.Internal.mk self.id pivot n n1, node_id_cnt2))
 
-/- [betree::betree::{betree::betree::Node#5}::lookup_first_message_for_key]:
-   Source: 'src/betree.rs', lines 789:4-792:34 -/
-divergent def betree.Node.lookup_first_message_for_key
+/- [betree::betree::{betree::betree::Node#5}::lookup_first_message_for_key]: loop 0:
+   Source: 'src/betree.rs', lines 792:4-810:5 -/
+divergent def betree.Node.lookup_first_message_for_key_loop
   (key : U64) (msgs : betree.List (U64 × betree.Message)) :
   Result ((betree.List (U64 × betree.Message)) × (betree.List (U64 ×
     betree.Message) → Result (betree.List (U64 × betree.Message))))
@@ -190,19 +236,28 @@ divergent def betree.Node.lookup_first_message_for_key
     then Result.ok (betree.List.Cons (i, m) next_msgs, Result.ok)
     else
       do
-      let (l, lookup_first_message_for_key_back) ←
-        betree.Node.lookup_first_message_for_key key next_msgs
-      let back :=
+      let (l, back) ←
+        betree.Node.lookup_first_message_for_key_loop key next_msgs
+      let back1 :=
         fun ret =>
           do
-          let next_msgs1 ← lookup_first_message_for_key_back ret
+          let next_msgs1 ← back ret
           Result.ok (betree.List.Cons (i, m) next_msgs1)
-      Result.ok (l, back)
+      Result.ok (l, back1)
   | betree.List.Nil => Result.ok (betree.List.Nil, Result.ok)
 
-/- [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]:
-   Source: 'src/betree.rs', lines 636:4-636:80 -/
-divergent def betree.Node.lookup_in_bindings
+/- [betree::betree::{betree::betree::Node#5}::lookup_first_message_for_key]:
+   Source: 'src/betree.rs', lines 792:4-795:34 -/
+def betree.Node.lookup_first_message_for_key
+  (key : U64) (msgs : betree.List (U64 × betree.Message)) :
+  Result ((betree.List (U64 × betree.Message)) × (betree.List (U64 ×
+    betree.Message) → Result (betree.List (U64 × betree.Message))))
+  :=
+  betree.Node.lookup_first_message_for_key_loop key msgs
+
+/- [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]: loop 0:
+   Source: 'src/betree.rs', lines 649:4-660:5 -/
+divergent def betree.Node.lookup_in_bindings_loop
   (key : U64) (bindings : betree.List (U64 × U64)) : Result (Option U64) :=
   match bindings with
   | betree.List.Cons hd tl =>
@@ -212,12 +267,18 @@ divergent def betree.Node.lookup_in_bindings
     else
       if i > key
       then Result.ok none
-      else betree.Node.lookup_in_bindings key tl
+      else betree.Node.lookup_in_bindings_loop key tl
   | betree.List.Nil => Result.ok none
 
-/- [betree::betree::{betree::betree::Node#5}::apply_upserts]:
-   Source: 'src/betree.rs', lines 819:4-819:90 -/
-divergent def betree.Node.apply_upserts
+/- [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]:
+   Source: 'src/betree.rs', lines 649:4-649:84 -/
+def betree.Node.lookup_in_bindings
+  (key : U64) (bindings : betree.List (U64 × U64)) : Result (Option U64) :=
+  betree.Node.lookup_in_bindings_loop key bindings
+
+/- [betree::betree::{betree::betree::Node#5}::apply_upserts]: loop 0:
+   Source: 'src/betree.rs', lines 820:4-844:5 -/
+divergent def betree.Node.apply_upserts_loop
   (msgs : betree.List (U64 × betree.Message)) (prev : Option U64) (key : U64)
   :
   Result (U64 × (betree.List (U64 × betree.Message)))
@@ -235,7 +296,7 @@ divergent def betree.Node.apply_upserts
     | betree.Message.Upsert s =>
       do
       let v ← betree.upsert_update prev s
-      betree.Node.apply_upserts msgs1 (some v) key
+      betree.Node.apply_upserts_loop msgs1 (some v) key
   else
     do
     let v ← core.option.Option.unwrap U64 prev
@@ -244,8 +305,17 @@ divergent def betree.Node.apply_upserts
         betree.Message.Insert v)
     Result.ok (v, msgs1)
 
+/- [betree::betree::{betree::betree::Node#5}::apply_upserts]:
+   Source: 'src/betree.rs', lines 820:4-820:94 -/
+def betree.Node.apply_upserts
+  (msgs : betree.List (U64 × betree.Message)) (prev : Option U64) (key : U64)
+  :
+  Result (U64 × (betree.List (U64 × betree.Message)))
+  :=
+  betree.Node.apply_upserts_loop msgs prev key
+
 /- [betree::betree::{betree::betree::Internal#4}::lookup_in_children]:
-   Source: 'src/betree.rs', lines 395:4-395:63 -/
+   Source: 'src/betree.rs', lines 414:4-414:63 -/
 mutual divergent def betree.Internal.lookup_in_children
   (self : betree.Internal) (key : U64) (st : State) :
   Result (State × ((Option U64) × betree.Internal))
@@ -261,7 +331,7 @@ mutual divergent def betree.Internal.lookup_in_children
     Result.ok (st1, (o, betree.Internal.mk self.id self.pivot self.left n))
 
 /- [betree::betree::{betree::betree::Node#5}::lookup]:
-   Source: 'src/betree.rs', lines 709:4-709:58 -/
+   Source: 'src/betree.rs', lines 712:4-712:58 -/
 divergent def betree.Node.lookup
   (self : betree.Node) (key : U64) (st : State) :
   Result (State × ((Option U64) × betree.Node))
@@ -320,9 +390,9 @@ divergent def betree.Node.lookup
 
 end
 
-/- [betree::betree::{betree::betree::Node#5}::filter_messages_for_key]:
-   Source: 'src/betree.rs', lines 674:4-674:77 -/
-divergent def betree.Node.filter_messages_for_key
+/- [betree::betree::{betree::betree::Node#5}::filter_messages_for_key]: loop 0:
+   Source: 'src/betree.rs', lines 683:4-692:5 -/
+divergent def betree.Node.filter_messages_for_key_loop
   (key : U64) (msgs : betree.List (U64 × betree.Message)) :
   Result (betree.List (U64 × betree.Message))
   :=
@@ -335,13 +405,21 @@ divergent def betree.Node.filter_messages_for_key
       let (_, msgs1) ←
         betree.List.pop_front (U64 × betree.Message) (betree.List.Cons (k, m)
           l)
-      betree.Node.filter_messages_for_key key msgs1
+      betree.Node.filter_messages_for_key_loop key msgs1
     else Result.ok (betree.List.Cons (k, m) l)
   | betree.List.Nil => Result.ok betree.List.Nil
 
-/- [betree::betree::{betree::betree::Node#5}::lookup_first_message_after_key]:
-   Source: 'src/betree.rs', lines 689:4-692:34 -/
-divergent def betree.Node.lookup_first_message_after_key
+/- [betree::betree::{betree::betree::Node#5}::filter_messages_for_key]:
+   Source: 'src/betree.rs', lines 683:4-683:77 -/
+def betree.Node.filter_messages_for_key
+  (key : U64) (msgs : betree.List (U64 × betree.Message)) :
+  Result (betree.List (U64 × betree.Message))
+  :=
+  betree.Node.filter_messages_for_key_loop key msgs
+
+/- [betree::betree::{betree::betree::Node#5}::lookup_first_message_after_key]: loop 0:
+   Source: 'src/betree.rs', lines 694:4-706:5 -/
+divergent def betree.Node.lookup_first_message_after_key_loop
   (key : U64) (msgs : betree.List (U64 × betree.Message)) :
   Result ((betree.List (U64 × betree.Message)) × (betree.List (U64 ×
     betree.Message) → Result (betree.List (U64 × betree.Message))))
@@ -352,19 +430,28 @@ divergent def betree.Node.lookup_first_message_after_key
     if k = key
     then
       do
-      let (l, lookup_first_message_after_key_back) ←
-        betree.Node.lookup_first_message_after_key key next_msgs
-      let back :=
+      let (l, back) ←
+        betree.Node.lookup_first_message_after_key_loop key next_msgs
+      let back1 :=
         fun ret =>
           do
-          let next_msgs1 ← lookup_first_message_after_key_back ret
+          let next_msgs1 ← back ret
           Result.ok (betree.List.Cons (k, m) next_msgs1)
-      Result.ok (l, back)
+      Result.ok (l, back1)
     else Result.ok (betree.List.Cons (k, m) next_msgs, Result.ok)
   | betree.List.Nil => Result.ok (betree.List.Nil, Result.ok)
 
+/- [betree::betree::{betree::betree::Node#5}::lookup_first_message_after_key]:
+   Source: 'src/betree.rs', lines 694:4-697:34 -/
+def betree.Node.lookup_first_message_after_key
+  (key : U64) (msgs : betree.List (U64 × betree.Message)) :
+  Result ((betree.List (U64 × betree.Message)) × (betree.List (U64 ×
+    betree.Message) → Result (betree.List (U64 × betree.Message))))
+  :=
+  betree.Node.lookup_first_message_after_key_loop key msgs
+
 /- [betree::betree::{betree::betree::Node#5}::apply_to_internal]:
-   Source: 'src/betree.rs', lines 521:4-521:89 -/
+   Source: 'src/betree.rs', lines 534:4-534:89 -/
 def betree.Node.apply_to_internal
   (msgs : betree.List (U64 × betree.Message)) (key : U64)
   (new_msg : betree.Message) :
@@ -427,9 +514,9 @@ def betree.Node.apply_to_internal
       betree.List.push_front (U64 × betree.Message) msgs1 (key, new_msg)
     lookup_first_message_for_key_back msgs2
 
-/- [betree::betree::{betree::betree::Node#5}::apply_messages_to_internal]:
-   Source: 'src/betree.rs', lines 502:4-505:5 -/
-divergent def betree.Node.apply_messages_to_internal
+/- [betree::betree::{betree::betree::Node#5}::apply_messages_to_internal]: loop 0:
+   Source: 'src/betree.rs', lines 518:4-526:5 -/
+divergent def betree.Node.apply_messages_to_internal_loop
   (msgs : betree.List (U64 × betree.Message))
   (new_msgs : betree.List (U64 × betree.Message)) :
   Result (betree.List (U64 × betree.Message))
@@ -439,12 +526,21 @@ divergent def betree.Node.apply_messages_to_internal
     do
     let (i, m) := new_msg
     let msgs1 ← betree.Node.apply_to_internal msgs i m
-    betree.Node.apply_messages_to_internal msgs1 new_msgs_tl
+    betree.Node.apply_messages_to_internal_loop msgs1 new_msgs_tl
   | betree.List.Nil => Result.ok msgs
 
-/- [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]:
-   Source: 'src/betree.rs', lines 653:4-656:32 -/
-divergent def betree.Node.lookup_mut_in_bindings
+/- [betree::betree::{betree::betree::Node#5}::apply_messages_to_internal]:
+   Source: 'src/betree.rs', lines 518:4-521:5 -/
+def betree.Node.apply_messages_to_internal
+  (msgs : betree.List (U64 × betree.Message))
+  (new_msgs : betree.List (U64 × betree.Message)) :
+  Result (betree.List (U64 × betree.Message))
+  :=
+  betree.Node.apply_messages_to_internal_loop msgs new_msgs
+
+/- [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]: loop 0:
+   Source: 'src/betree.rs', lines 664:4-677:5 -/
+divergent def betree.Node.lookup_mut_in_bindings_loop
   (key : U64) (bindings : betree.List (U64 × U64)) :
   Result ((betree.List (U64 × U64)) × (betree.List (U64 × U64) → Result
     (betree.List (U64 × U64))))
@@ -456,18 +552,26 @@ divergent def betree.Node.lookup_mut_in_bindings
     then Result.ok (betree.List.Cons (i, i1) tl, Result.ok)
     else
       do
-      let (l, lookup_mut_in_bindings_back) ←
-        betree.Node.lookup_mut_in_bindings key tl
-      let back :=
+      let (l, back) ← betree.Node.lookup_mut_in_bindings_loop key tl
+      let back1 :=
         fun ret =>
           do
-          let tl1 ← lookup_mut_in_bindings_back ret
+          let tl1 ← back ret
           Result.ok (betree.List.Cons (i, i1) tl1)
-      Result.ok (l, back)
+      Result.ok (l, back1)
   | betree.List.Nil => Result.ok (betree.List.Nil, Result.ok)
 
+/- [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]:
+   Source: 'src/betree.rs', lines 664:4-667:32 -/
+def betree.Node.lookup_mut_in_bindings
+  (key : U64) (bindings : betree.List (U64 × U64)) :
+  Result ((betree.List (U64 × U64)) × (betree.List (U64 × U64) → Result
+    (betree.List (U64 × U64))))
+  :=
+  betree.Node.lookup_mut_in_bindings_loop key bindings
+
 /- [betree::betree::{betree::betree::Node#5}::apply_to_leaf]:
-   Source: 'src/betree.rs', lines 460:4-460:87 -/
+   Source: 'src/betree.rs', lines 476:4-476:87 -/
 def betree.Node.apply_to_leaf
   (bindings : betree.List (U64 × U64)) (key : U64) (new_msg : betree.Message)
   :
@@ -506,9 +610,9 @@ def betree.Node.apply_to_leaf
       let bindings2 ← betree.List.push_front (U64 × U64) bindings1 (key, v)
       lookup_mut_in_bindings_back bindings2
 
-/- [betree::betree::{betree::betree::Node#5}::apply_messages_to_leaf]:
-   Source: 'src/betree.rs', lines 444:4-447:5 -/
-divergent def betree.Node.apply_messages_to_leaf
+/- [betree::betree::{betree::betree::Node#5}::apply_messages_to_leaf]: loop 0:
+   Source: 'src/betree.rs', lines 463:4-471:5 -/
+divergent def betree.Node.apply_messages_to_leaf_loop
   (bindings : betree.List (U64 × U64))
   (new_msgs : betree.List (U64 × betree.Message)) :
   Result (betree.List (U64 × U64))
@@ -518,11 +622,20 @@ divergent def betree.Node.apply_messages_to_leaf
     do
     let (i, m) := new_msg
     let bindings1 ← betree.Node.apply_to_leaf bindings i m
-    betree.Node.apply_messages_to_leaf bindings1 new_msgs_tl
+    betree.Node.apply_messages_to_leaf_loop bindings1 new_msgs_tl
   | betree.List.Nil => Result.ok bindings
 
+/- [betree::betree::{betree::betree::Node#5}::apply_messages_to_leaf]:
+   Source: 'src/betree.rs', lines 463:4-466:5 -/
+def betree.Node.apply_messages_to_leaf
+  (bindings : betree.List (U64 × U64))
+  (new_msgs : betree.List (U64 × betree.Message)) :
+  Result (betree.List (U64 × U64))
+  :=
+  betree.Node.apply_messages_to_leaf_loop bindings new_msgs
+
 /- [betree::betree::{betree::betree::Internal#4}::flush]:
-   Source: 'src/betree.rs', lines 410:4-415:26 -/
+   Source: 'src/betree.rs', lines 429:4-434:26 -/
 mutual divergent def betree.Internal.flush
   (self : betree.Internal) (params : betree.Params)
   (node_id_cnt : betree.NodeIdCounter)
@@ -563,7 +676,7 @@ mutual divergent def betree.Internal.flush
       self.left n, node_id_cnt1)))
 
 /- [betree::betree::{betree::betree::Node#5}::apply_messages]:
-   Source: 'src/betree.rs', lines 588:4-593:5 -/
+   Source: 'src/betree.rs', lines 601:4-606:5 -/
 divergent def betree.Node.apply_messages
   (self : betree.Node) (params : betree.Params)
   (node_id_cnt : betree.NodeIdCounter)
@@ -610,7 +723,7 @@ divergent def betree.Node.apply_messages
 end
 
 /- [betree::betree::{betree::betree::Node#5}::apply]:
-   Source: 'src/betree.rs', lines 576:4-582:5 -/
+   Source: 'src/betree.rs', lines 589:4-595:5 -/
 def betree.Node.apply
   (self : betree.Node) (params : betree.Params)
   (node_id_cnt : betree.NodeIdCounter) (key : U64) (new_msg : betree.Message)
@@ -625,7 +738,7 @@ def betree.Node.apply
   Result.ok (st1, (self1, node_id_cnt1))
 
 /- [betree::betree::{betree::betree::BeTree#6}::new]:
-   Source: 'src/betree.rs', lines 849:4-849:60 -/
+   Source: 'src/betree.rs', lines 848:4-848:60 -/
 def betree.BeTree.new
   (min_flush_size : U64) (split_size : U64) (st : State) :
   Result (State × betree.BeTree)
@@ -642,7 +755,7 @@ def betree.BeTree.new
     })
 
 /- [betree::betree::{betree::betree::BeTree#6}::apply]:
-   Source: 'src/betree.rs', lines 868:4-868:47 -/
+   Source: 'src/betree.rs', lines 867:4-867:47 -/
 def betree.BeTree.apply
   (self : betree.BeTree) (key : U64) (msg : betree.Message) (st : State) :
   Result (State × betree.BeTree)
@@ -654,7 +767,7 @@ def betree.BeTree.apply
   Result.ok (st1, { self with node_id_cnt := nic, root := n })
 
 /- [betree::betree::{betree::betree::BeTree#6}::insert]:
-   Source: 'src/betree.rs', lines 874:4-874:52 -/
+   Source: 'src/betree.rs', lines 873:4-873:52 -/
 def betree.BeTree.insert
   (self : betree.BeTree) (key : U64) (value : U64) (st : State) :
   Result (State × betree.BeTree)
@@ -662,7 +775,7 @@ def betree.BeTree.insert
   betree.BeTree.apply self key (betree.Message.Insert value) st
 
 /- [betree::betree::{betree::betree::BeTree#6}::delete]:
-   Source: 'src/betree.rs', lines 880:4-880:38 -/
+   Source: 'src/betree.rs', lines 879:4-879:38 -/
 def betree.BeTree.delete
   (self : betree.BeTree) (key : U64) (st : State) :
   Result (State × betree.BeTree)
@@ -670,7 +783,7 @@ def betree.BeTree.delete
   betree.BeTree.apply self key betree.Message.Delete st
 
 /- [betree::betree::{betree::betree::BeTree#6}::upsert]:
-   Source: 'src/betree.rs', lines 886:4-886:59 -/
+   Source: 'src/betree.rs', lines 885:4-885:59 -/
 def betree.BeTree.upsert
   (self : betree.BeTree) (key : U64) (upd : betree.UpsertFunState) (st : State)
   :
@@ -679,7 +792,7 @@ def betree.BeTree.upsert
   betree.BeTree.apply self key (betree.Message.Upsert upd) st
 
 /- [betree::betree::{betree::betree::BeTree#6}::lookup]:
-   Source: 'src/betree.rs', lines 895:4-895:62 -/
+   Source: 'src/betree.rs', lines 894:4-894:62 -/
 def betree.BeTree.lookup
   (self : betree.BeTree) (key : U64) (st : State) :
   Result (State × ((Option U64) × betree.BeTree))
diff --git a/tests/src/betree/aeneas-test-options b/tests/src/betree/aeneas-test-options
index c71e01df..5a1e4180 100644
--- a/tests/src/betree/aeneas-test-options
+++ b/tests/src/betree/aeneas-test-options
@@ -1,4 +1,4 @@
 charon-args=--polonius --opaque=betree_utils
-aeneas-args=-backward-no-state-update -test-trans-units -state -split-files
+[!borrow-check] aeneas-args=-backward-no-state-update -test-trans-units -state -split-files
 [coq] aeneas-args=-use-fuel
 [fstar] aeneas-args=-decreases-clauses -template-clauses
diff --git a/tests/src/betree/src/betree.rs b/tests/src/betree/src/betree.rs
index 12f2847d..8ba07824 100644
--- a/tests/src/betree/src/betree.rs
+++ b/tests/src/betree/src/betree.rs
@@ -274,25 +274,41 @@ pub fn upsert_update(prev: Option<Value>, st: UpsertFunState) -> Value {
 
 impl<T> List<T> {
     fn len(&self) -> u64 {
-        match self {
-            List::Nil => 0,
-            List::Cons(_, tl) => 1 + tl.len(),
+        let mut l = self;
+        let mut len = 0;
+        while let List::Cons(_, tl) = l {
+            len += 1;
+            l = tl;
         }
+        len
     }
 
     /// Split a list at a given length
-    fn split_at(self, n: u64) -> (List<T>, List<T>) {
-        if n == 0 {
-            (List::Nil, self)
-        } else {
-            match self {
+    fn split_at(self, mut n: u64) -> (List<T>, List<T>) {
+        let mut beg = List::Nil;
+        let mut end = self;
+        while n > 0 {
+            match end {
                 List::Nil => unreachable!(),
-                List::Cons(hd, tl) => {
-                    let (ls0, ls1) = tl.split_at(n - 1);
-                    (List::Cons(hd, Box::new(ls0)), ls1)
+                List::Cons(hd, mut tl) => {
+                    n -= 1;
+                    end = *tl;
+                    *tl = beg;
+                    beg = List::Cons(hd, tl);
                 }
             }
         }
+        (beg.reverse(), end)
+    }
+
+    fn reverse(mut self) -> Self {
+        let mut out = List::Nil;
+        while let List::Cons(hd, mut tl) = self {
+            self = *tl;
+            *tl = out;
+            out = List::Cons(hd, tl);
+        }
+        out
     }
 
     /// Push an element at the front of the list.
@@ -337,17 +353,20 @@ impl<T> Map<Key, T> {
     /// Note that the bindings in the map are supposed to be sorted in
     /// order of increasing keys.
     fn partition_at_pivot(self, pivot: Key) -> (Map<Key, T>, Map<Key, T>) {
-        match self {
-            List::Nil => (List::Nil, List::Nil),
-            List::Cons(hd, tl) => {
-                if hd.0 >= pivot {
-                    (List::Nil, List::Cons(hd, tl))
-                } else {
-                    let (ls0, ls1) = tl.partition_at_pivot(pivot);
-                    (List::Cons(hd, Box::new(ls0)), ls1)
-                }
+        let mut beg = List::Nil;
+        let mut end = List::Nil;
+        let mut curr = self;
+        while let List::Cons(hd, mut tl) = curr {
+            curr = *tl;
+            if hd.0 >= pivot {
+                *tl = end;
+                end = List::Cons(hd, tl);
+            } else {
+                *tl = beg;
+                beg = List::Cons(hd, tl);
             }
         }
+        (beg.reverse(), end.reverse())
     }
 }
 
@@ -443,14 +462,11 @@ impl Node {
     /// Apply a list of message to ourselves: leaf node case
     fn apply_messages_to_leaf<'a>(
         bindings: &'a mut Map<Key, Value>,
-        new_msgs: List<(Key, Message)>,
+        mut new_msgs: List<(Key, Message)>,
     ) {
-        match new_msgs {
-            List::Nil => (),
-            List::Cons(new_msg, new_msgs_tl) => {
-                Node::apply_to_leaf(bindings, new_msg.0, new_msg.1);
-                Node::apply_messages_to_leaf(bindings, *new_msgs_tl);
-            }
+        while let List::Cons(new_msg, new_msgs_tl) = new_msgs {
+            Node::apply_to_leaf(bindings, new_msg.0, new_msg.1);
+            new_msgs = *new_msgs_tl;
         }
     }
 
@@ -501,14 +517,11 @@ impl Node {
     /// Apply a list of message to ourselves: internal node case
     fn apply_messages_to_internal<'a>(
         msgs: &'a mut Map<Key, Message>,
-        new_msgs: List<(Key, Message)>,
+        mut new_msgs: List<(Key, Message)>,
     ) {
-        match new_msgs {
-            List::Nil => (),
-            List::Cons(new_msg, new_msgs_tl) => {
-                Node::apply_to_internal(msgs, new_msg.0, new_msg.1);
-                Node::apply_messages_to_internal(msgs, *new_msgs_tl);
-            }
+        while let List::Cons(new_msg, new_msgs_tl) = new_msgs {
+            Node::apply_to_internal(msgs, new_msg.0, new_msg.1);
+            new_msgs = *new_msgs_tl;
         }
     }
 
@@ -633,38 +646,34 @@ impl Node {
 
     /// Lookup a value in a list of bindings.
     /// Note that the values should be stored in order of increasing key.
-    fn lookup_in_bindings(key: Key, bindings: &Map<Key, Value>) -> Option<Value> {
-        match bindings {
-            List::Nil => Option::None,
-            List::Cons(hd, tl) => {
-                if hd.0 == key {
-                    Option::Some(hd.1)
-                } else if hd.0 > key {
-                    Option::None
-                } else {
-                    Node::lookup_in_bindings(key, tl)
-                }
+    fn lookup_in_bindings(key: Key, mut bindings: &Map<Key, Value>) -> Option<Value> {
+        while let List::Cons(hd, tl) = bindings {
+            if hd.0 == key {
+                return Option::Some(hd.1);
+            } else if hd.0 > key {
+                return Option::None;
+            } else {
+                bindings = tl;
             }
         }
+        Option::None
     }
 
     /// Lookup a value in a list of bindings, and return a borrow to the position
     /// where the value is (or should be inserted, if the key is not in the bindings).
     fn lookup_mut_in_bindings<'a>(
         key: Key,
-        bindings: &'a mut Map<Key, Value>,
+        mut bindings: &'a mut Map<Key, Value>,
     ) -> &'a mut Map<Key, Value> {
-        match bindings {
-            List::Nil => bindings,
-            List::Cons(hd, tl) => {
-                // This requires Polonius
-                if hd.0 >= key {
-                    bindings
-                } else {
-                    Node::lookup_mut_in_bindings(key, tl)
-                }
+        while let List::Cons(hd, tl) = bindings {
+            // This requires Polonius
+            if hd.0 >= key {
+                break;
+            } else {
+                bindings = tl;
             }
         }
+        bindings
     }
 
     /// Filter all the messages which concern [key].
@@ -672,34 +681,28 @@ impl Node {
     /// Note that the stack of messages must start with a message for [key]:
     /// we stop filtering at the first message which is not about [key].
     fn filter_messages_for_key<'a>(key: Key, msgs: &'a mut Map<Key, Message>) {
-        match msgs {
-            List::Nil => (),
-            List::Cons((k, _), _) => {
-                if *k == key {
-                    msgs.pop_front();
-                    Node::filter_messages_for_key(key, msgs);
-                } else {
-                    // Stop
-                    ()
-                }
+        while let List::Cons((k, _), _) = msgs {
+            if *k == key {
+                msgs.pop_front();
+            } else {
+                // Stop
+                break;
             }
         }
     }
 
     fn lookup_first_message_after_key<'a>(
         key: Key,
-        msgs: &'a mut Map<Key, Message>,
+        mut msgs: &'a mut Map<Key, Message>,
     ) -> &'a mut Map<Key, Message> {
-        match msgs {
-            List::Nil => msgs,
-            List::Cons((k, _), next_msgs) => {
-                if *k == key {
-                    Node::lookup_first_message_after_key(key, next_msgs)
-                } else {
-                    msgs
-                }
+        while let List::Cons((k, _), next_msgs) = msgs {
+            if *k == key {
+                msgs = next_msgs;
+            } else {
+                break;
             }
         }
+        return msgs;
     }
 
     /// Returns the value bound to a key.
@@ -788,24 +791,22 @@ impl Node {
     /// of the list).
     fn lookup_first_message_for_key<'a>(
         key: Key,
-        msgs: &'a mut Map<Key, Message>,
+        mut msgs: &'a mut Map<Key, Message>,
     ) -> &'a mut Map<Key, Message> {
-        match msgs {
-            List::Nil => msgs,
-            List::Cons(x, next_msgs) => {
-                // Rk.: we need Polonius here
-                // We wouldn't need Polonius if directly called the proper
-                // function to make the modifications here (because we wouldn't
-                // need to return anything). However, it would not be very
-                // idiomatic, especially with regards to the fact that we will
-                // rewrite everything with loops at some point.
-                if x.0 >= key {
-                    msgs
-                } else {
-                    Node::lookup_first_message_for_key(key, next_msgs)
-                }
+        while let List::Cons(x, next_msgs) = msgs {
+            // Rk.: we need Polonius here
+            // We wouldn't need Polonius if directly called the proper
+            // function to make the modifications here (because we wouldn't
+            // need to return anything). However, it would not be very
+            // idiomatic, especially with regards to the fact that we will
+            // rewrite everything with loops at some point.
+            if x.0 >= key {
+                return msgs;
+            } else {
+                msgs = next_msgs;
             }
         }
+        msgs
     }
 
     /// Apply the upserts from the current messages stack to a looked up value.
@@ -816,8 +817,8 @@ impl Node {
     /// Note that if there are no more upserts to apply, then the value must be
     /// `Some`. Also note that we use the invariant that in the message stack,
     /// upsert messages are sorted from the first to the last to apply.
-    fn apply_upserts(msgs: &mut Map<Key, Message>, prev: Option<Value>, key: Key) -> Value {
-        if msgs.head_has_key(key) {
+    fn apply_upserts(msgs: &mut Map<Key, Message>, mut prev: Option<Value>, key: Key) -> Value {
+        while msgs.head_has_key(key) {
             // Pop the front message.
             // Note that it *must* be an upsert.
             let msg = msgs.pop_front();
@@ -825,9 +826,8 @@ impl Node {
                 Message::Upsert(s) => {
                     // Apply the update
                     let v = upsert_update(prev, s);
-                    let prev = Option::Some(v);
+                    prev = Option::Some(v);
                     // Continue
-                    Node::apply_upserts(msgs, prev, key)
                 }
                 _ => {
                     // Unreachable: we can only have [Upsert] messages
@@ -835,13 +835,12 @@ impl Node {
                     unreachable!();
                 }
             }
-        } else {
-            // We applied all the upsert messages: simply put an [Insert]
-            // message and return the value.
-            let v = prev.unwrap();
-            msgs.push_front((key, Message::Insert(v)));
-            return v;
         }
+        // We applied all the upsert messages: simply put an [Insert]
+        // message and return the value.
+        let v = prev.unwrap();
+        msgs.push_front((key, Message::Insert(v)));
+        v
     }
 }
 
diff --git a/tests/src/bitwise.rs b/tests/src/bitwise.rs
index fda8eff3..be12cea0 100644
--- a/tests/src/bitwise.rs
+++ b/tests/src/bitwise.rs
@@ -1,4 +1,4 @@
-//@ aeneas-args=-test-trans-units
+//@ [!borrow-check] aeneas-args=-test-trans-units
 //@ [coq,fstar] subdir=misc
 //! Exercise the bitwise operations
 
diff --git a/tests/src/borrow-check-negative.borrow-check.out b/tests/src/borrow-check-negative.borrow-check.out
new file mode 100644
index 00000000..dc9dd5a7
--- /dev/null
+++ b/tests/src/borrow-check-negative.borrow-check.out
@@ -0,0 +1,15 @@
+[Info ] Imported: tests/llbc/borrow_check_negative.llbc
+[Error] Can not apply a projection to the ⊥ value
+Source: 'tests/src/borrow-check-negative.rs', lines 17:4-24:1
+[Error] Can't end abstraction 8 as it is set as non-endable
+Source: 'tests/src/borrow-check-negative.rs', lines 26:0-26:76
+[Error] Can not apply a projection to the ⊥ value
+Source: 'tests/src/borrow-check-negative.rs', lines 37:4-41:1
+[Error] Can not apply a projection to the ⊥ value
+Source: 'tests/src/borrow-check-negative.rs', lines 47:4-50:1
+[Error] Can not apply a projection to the ⊥ value
+Source: 'tests/src/borrow-check-negative.rs', lines 60:4-64:1
+[Error] Can not apply a projection to the ⊥ value
+Source: 'tests/src/borrow-check-negative.rs', lines 71:4-79:1
+[Error] Can not apply a projection to the ⊥ value
+Source: 'tests/src/borrow-check-negative.rs', lines 87:4-90:1
diff --git a/tests/src/borrow-check-negative.rs b/tests/src/borrow-check-negative.rs
new file mode 100644
index 00000000..697546dd
--- /dev/null
+++ b/tests/src/borrow-check-negative.rs
@@ -0,0 +1,90 @@
+//@ [!borrow-check] skip
+//@ [borrow-check] known-failure
+// Some negative tests for borrow checking
+
+// This succeeds
+fn choose<'a, T>(b: bool, x: &'a mut T, y: &'a mut T) -> &'a mut T {
+    if b {
+        x
+    } else {
+        y
+    }
+}
+
+pub fn choose_test() {
+    let mut x = 0;
+    let mut y = 0;
+    let z = choose(true, &mut x, &mut y);
+    *z += 1;
+    assert!(*z == 1);
+    // drop(z)
+    assert!(x == 1);
+    assert!(y == 0);
+    assert!(*z == 1); // z is not valid anymore
+}
+
+fn choose_wrong<'a, 'b, T>(b: bool, x: &'a mut T, y: &'b mut T) -> &'a mut T {
+    if b {
+        x
+    } else {
+        y // Expected lifetime 'a
+    }
+}
+
+fn test_mut1(b: bool) {
+    let mut x = 0;
+    let mut y = 1;
+    let z = if b { &mut x } else { &mut y };
+    *z += 1;
+    assert!(x >= 0);
+    *z += 1; // z is not valid anymore
+}
+
+#[allow(unused_assignments)]
+fn test_mut2(b: bool) {
+    let mut x = 0;
+    let mut y = 1;
+    let z = if b { &x } else { &y };
+    x += 1;
+    assert!(*z == 0); // z is not valid anymore
+}
+
+fn test_move1<T>(x: T) -> T {
+    let _ = x;
+    return x; // x has been moved
+}
+
+pub fn refs_test1() {
+    let mut x = 0;
+    let mut px = &mut x;
+    let ppx = &mut px;
+    **ppx = 1;
+    assert!(x == 1);
+    assert!(**ppx == 1); // ppx has ended
+}
+
+pub fn refs_test2() {
+    let mut x = 0;
+    let mut y = 1;
+    let mut px = &mut x;
+    let py = &mut y;
+    let ppx = &mut px;
+    *ppx = py;
+    **ppx = 2;
+    assert!(*px == 2);
+    assert!(x == 0);
+    assert!(*py == 2);
+    assert!(y == 2);
+    assert!(**ppx == 2); // ppx has ended
+}
+
+pub fn test_box1() {
+    use std::ops::Deref;
+    use std::ops::DerefMut;
+    let mut b: Box<i32> = Box::new(0);
+    let x0 = b.deref_mut();
+    *x0 = 1;
+    let x1 = b.deref();
+    assert!(*x1 == 1);
+    assert!(*x0 == 1); // x0 has ended
+}
diff --git a/tests/src/constants.rs b/tests/src/constants.rs
index ac24dcd4..71d7c557 100644
--- a/tests/src/constants.rs
+++ b/tests/src/constants.rs
@@ -1,5 +1,5 @@
 //@ charon-args=--no-code-duplication
-//@ aeneas-args=-test-trans-units
+//@ [!borrow-check] aeneas-args=-test-trans-units
 //@ [coq,fstar] subdir=misc
 //! Tests with constants
 
diff --git a/tests/src/external.rs b/tests/src/external.rs
index baea76e4..00acdb0b 100644
--- a/tests/src/external.rs
+++ b/tests/src/external.rs
@@ -1,6 +1,6 @@
 //@ charon-args=--no-code-duplication
-//@ aeneas-args=-state -split-files
-//@ aeneas-args=-test-trans-units
+//@ [!borrow-check] aeneas-args=-state -split-files
+//@ [!borrow-check] aeneas-args=-test-trans-units
 //@ [coq,fstar] subdir=misc
 //! This module uses external types and functions
 
diff --git a/tests/src/hashmap.rs b/tests/src/hashmap.rs
index 19832a84..7dda2404 100644
--- a/tests/src/hashmap.rs
+++ b/tests/src/hashmap.rs
@@ -1,5 +1,5 @@
 //@ charon-args=--opaque=utils
-//@ aeneas-args=-state -split-files
+//@ [!borrow-check] aeneas-args=-state -split-files
 //@ [coq] aeneas-args=-use-fuel
 //@ [fstar] aeneas-args=-decreases-clauses -template-clauses
 //@ [lean] aeneas-args=-no-gen-lib-entry
diff --git a/tests/src/loops-borrow-check-fail.borrow-check.out b/tests/src/loops-borrow-check-fail.borrow-check.out
new file mode 100644
index 00000000..34eb75f8
--- /dev/null
+++ b/tests/src/loops-borrow-check-fail.borrow-check.out
@@ -0,0 +1,5 @@
+[Info ] Imported: tests/llbc/loops_borrow_check_fail.llbc
+[Error] Can not apply a projection to the ⊥ value
+Source: 'tests/src/loops-borrow-check-fail.rs', lines 7:4-12:1
+[Error] Can not apply a projection to the ⊥ value
+Source: 'tests/src/loops-borrow-check-fail.rs', lines 17:4-21:1
diff --git a/tests/src/loops-borrow-check-fail.rs b/tests/src/loops-borrow-check-fail.rs
new file mode 100644
index 00000000..24be052c
--- /dev/null
+++ b/tests/src/loops-borrow-check-fail.rs
@@ -0,0 +1,21 @@
+//@ [!borrow-check] skip
+//@ [borrow-check] known-failure
+
+// We need to use the general rules for joining the loans
+fn loop_reborrow_mut() {
+    let mut x = 0;
+    let mut px = &mut x;
+    while *px > 0 {
+        x += 1;
+        px = &mut x;
+    }
+}
+
+// We need to imrpove [prepare_ashared_loans]
+fn iter_local_shared_borrow() {
+    let mut x = 0;
+    let mut p = &x;
+    loop {
+        p = &(*p);
+    }
+}
diff --git a/tests/src/loops-borrow-check-negative.borrow-check.out b/tests/src/loops-borrow-check-negative.borrow-check.out
new file mode 100644
index 00000000..093d8b8a
--- /dev/null
+++ b/tests/src/loops-borrow-check-negative.borrow-check.out
@@ -0,0 +1,3 @@
+[Info ] Imported: tests/llbc/loops_borrow_check_negative.llbc
+[Error] Can't end abstraction 16 as it is set as non-endable
+Source: 'tests/src/loops-borrow-check-negative.rs', lines 18:0-18:66
diff --git a/tests/src/loops-borrow-check-negative.rs b/tests/src/loops-borrow-check-negative.rs
new file mode 100644
index 00000000..3386d581
--- /dev/null
+++ b/tests/src/loops-borrow-check-negative.rs
@@ -0,0 +1,28 @@
+//@ [!borrow-check] skip
+//@ [borrow-check] known-failure
+
+// This succeeds
+fn loop_a<'a>(a: &'a mut u32, b: &'a mut u32) -> &'a mut u32 {
+    let mut x = 0;
+    while x > 0 {
+        x += 1;
+    }
+    if x > 0 {
+        a
+    } else {
+        b
+    }
+}
+
+// This fails
+fn loop_a_b<'a, 'b>(a: &'a mut u32, b: &'b mut u32) -> &'a mut u32 {
+    let mut x = 0;
+    while x > 0 {
+        x += 1;
+    }
+    if x > 0 {
+        a
+    } else {
+        b // Expect lifetime 'a
+    }
+}
diff --git a/tests/src/loops-borrow-check.rs b/tests/src/loops-borrow-check.rs
new file mode 100644
index 00000000..ab300b37
--- /dev/null
+++ b/tests/src/loops-borrow-check.rs
@@ -0,0 +1,10 @@
+//@ [!borrow-check] skip
+
+fn iter_local_mut_borrow() {
+    let mut x = 0;
+    let mut p = &mut x;
+    loop {
+        p = &mut (*p);
+        *p += 1;
+    }
+}
diff --git a/tests/src/mutually-recursive-traits.lean.out b/tests/src/mutually-recursive-traits.lean.out
index 6d638644..e2ed3abc 100644
--- a/tests/src/mutually-recursive-traits.lean.out
+++ b/tests/src/mutually-recursive-traits.lean.out
@@ -1,17 +1,17 @@
 [Info ] Imported: tests/llbc/mutually_recursive_traits.llbc
-[Error] In file Translate.ml, line 812:
+[Error] In file Translate.ml, line 813:
 Mutually recursive trait declarations are not supported
 
 Uncaught exception:
   
   (Failure
-    "In file Translate.ml, line 812:\
-   \nIn file Translate.ml, line 812:\
+    "In file Translate.ml, line 813:\
+   \nIn file Translate.ml, line 813:\
    \nMutually recursive trait declarations are not supported")
 
 Raised at Aeneas__Errors.craise_opt_span in file "Errors.ml", line 46, characters 4-76
 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15
-Called from Aeneas__Translate.extract_definitions in file "Translate.ml", line 835, characters 2-52
-Called from Aeneas__Translate.extract_file in file "Translate.ml", line 953, characters 2-36
-Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 1501, characters 5-42
-Called from Dune__exe__Main in file "Main.ml", line 276, characters 9-61
+Called from Aeneas__Translate.extract_definitions in file "Translate.ml", line 836, characters 2-52
+Called from Aeneas__Translate.extract_file in file "Translate.ml", line 954, characters 2-36
+Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 1503, characters 5-42
+Called from Dune__exe__Main in file "Main.ml", line 314, characters 14-66
diff --git a/tests/src/mutually-recursive-traits.rs b/tests/src/mutually-recursive-traits.rs
index 351763b2..9bc4ca63 100644
--- a/tests/src/mutually-recursive-traits.rs
+++ b/tests/src/mutually-recursive-traits.rs
@@ -1,6 +1,6 @@
 //@ [lean] known-failure
-//@ [coq,fstar] skip
-//@ subdir=misc
+//@ [!lean] skip
+//@ [lean] subdir=misc
 pub trait Trait1 {
     type T: Trait2;
 }
diff --git a/tests/src/no_nested_borrows.rs b/tests/src/no_nested_borrows.rs
index 6d3074ef..11c4a695 100644
--- a/tests/src/no_nested_borrows.rs
+++ b/tests/src/no_nested_borrows.rs
@@ -1,5 +1,5 @@
 //@ charon-args=--no-code-duplication
-//@ aeneas-args=-test-trans-units
+//@ [!borrow-check] aeneas-args=-test-trans-units
 //@ [coq,fstar] subdir=misc
 //! This module doesn't contain **functions which use nested borrows in their
 //! signatures**, and doesn't contain functions with loops.
diff --git a/tests/src/paper.rs b/tests/src/paper.rs
index 6a4a7c31..d9fb1032 100644
--- a/tests/src/paper.rs
+++ b/tests/src/paper.rs
@@ -1,5 +1,5 @@
 //@ charon-args=--no-code-duplication
-//@ aeneas-args=-test-trans-units
+//@ [!borrow-check] aeneas-args=-test-trans-units
 //@ [coq,fstar] subdir=misc
 //! The examples from the ICFP submission, all in one place.
 
diff --git a/tests/src/polonius_list.rs b/tests/src/polonius_list.rs
index b029ad02..084441aa 100644
--- a/tests/src/polonius_list.rs
+++ b/tests/src/polonius_list.rs
@@ -1,5 +1,5 @@
 //@ charon-args=--polonius
-//@ aeneas-args=-test-trans-units
+//@ [!borrow-check] aeneas-args=-test-trans-units
 //@ [coq,fstar] subdir=misc
 #![allow(dead_code)]
 
diff --git a/tests/src/string-chars.rs b/tests/src/string-chars.rs
index f8490e76..9fd91752 100644
--- a/tests/src/string-chars.rs
+++ b/tests/src/string-chars.rs
@@ -1,5 +1,5 @@
 //@ [lean] known-failure
-//@ [coq,fstar] skip
+//@ [!lean] skip
 //@ no-check-output
 fn main() {
     let s = "hello";
diff --git a/tests/test_runner/Backend.ml b/tests/test_runner/Backend.ml
index d21a46fc..819081a2 100644
--- a/tests/test_runner/Backend.ml
+++ b/tests/test_runner/Backend.ml
@@ -1,15 +1,24 @@
 (*** Define the backends we support as an enum *)
 
-type t = Coq | Lean | FStar | HOL4 [@@deriving ord, sexp]
+type t =
+  | Coq
+  | Lean
+  | FStar
+  | HOL4
+  | BorrowCheck
+      (** Borrow check: no backend.
+          We use this when we only want to borrow-check the program *)
+[@@deriving ord, sexp]
 
 (* TODO: reactivate HOL4 once traits are parameterized by their associated types *)
-let all = [ Coq; Lean; FStar ]
+let all = [ Coq; Lean; FStar; BorrowCheck ]
 
 let of_string = function
   | "coq" -> Coq
   | "lean" -> Lean
   | "fstar" -> FStar
   | "hol4" -> HOL4
+  | "borrow-check" -> BorrowCheck
   | backend -> failwith ("Unknown backend: `" ^ backend ^ "`")
 
 let to_string = function
@@ -17,6 +26,11 @@ let to_string = function
   | Lean -> "lean"
   | FStar -> "fstar"
   | HOL4 -> "hol4"
+  | BorrowCheck -> "borrow-check"
+
+let to_command = function
+  | BorrowCheck -> [ "-borrow-check" ]
+  | x -> [ "-backend"; to_string x ]
 
 module Map = struct
   (* Hack to be able to include things from the parent module with the same names *)
diff --git a/tests/test_runner/Input.ml b/tests/test_runner/Input.ml
index 960ffe8d..e35be96f 100644
--- a/tests/test_runner/Input.ml
+++ b/tests/test_runner/Input.ml
@@ -7,7 +7,7 @@ type action = Normal | Skip | KnownFailure
 type per_backend = {
   action : action;
   aeneas_options : string list;
-  subdir : string;
+  subdir : string option;
   (* Whether to store the command output to a file. Only available for known-failure tests. *)
   check_output : bool;
 }
@@ -22,8 +22,11 @@ type t = {
 }
 
 (* The default subdirectory in which to store the outputs. *)
-let default_subdir backend test_name =
-  match backend with Backend.Lean -> "." | _ -> test_name
+let default_subdir backend test_name : string option =
+  match backend with
+  | Backend.Lean -> Some "."
+  | Backend.BorrowCheck -> None
+  | _ -> Some test_name
 
 (* Parse lines that start `//@`. Each of them modifies the options we use for the test.
    Supported comments:
@@ -39,14 +42,21 @@ let default_subdir backend test_name =
 let apply_special_comment comment input =
   let comment = String.trim comment in
   (* Parse the backends if any *)
-  let re = Re.compile (Re.Pcre.re "^\\[([a-zA-Z,]+)\\](.*)$") in
+  let re = Re.compile (Re.Pcre.re "^\\[(!)?([a-zA-Z,-]+)\\](.*)$") in
   let comment, (backends : Backend.t list) =
     match Re.exec_opt re comment with
     | Some groups ->
-        let backends = Re.Group.get groups 1 in
+        let exclude = Re.Group.get_opt groups 1 <> None in
+        let backends = Re.Group.get groups 2 in
         let backends = String.split_on_char ',' backends in
         let backends = List.map Backend.of_string backends in
-        let rest = Re.Group.get groups 2 in
+        let rest = Re.Group.get groups 3 in
+        (* If [exclude]: we take all the backends *but* the list provided. *)
+        let backends =
+          if exclude then
+            List.filter (fun x -> not (List.mem x backends)) Backend.all
+          else backends
+        in
         (String.trim rest, backends)
     | None -> (comment, Backend.all)
   in
@@ -83,9 +93,9 @@ let apply_special_comment comment input =
     let args = String.split_on_char ' ' args in
     per_backend (fun x ->
         { x with aeneas_options = List.append x.aeneas_options args })
-  else if Option.is_some subdir then
-    let subdir = Option.get subdir in
-    per_backend (fun x -> { x with subdir })
+  else if Option.is_some subdir then (
+    assert (not (List.mem Backend.BorrowCheck backends));
+    per_backend (fun x -> { x with subdir }))
   else failwith ("Unrecognized special comment: `" ^ comment ^ "`")
 
 (* Given a path to a rust file or crate, gather the details and options about how to build the test. *)
diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml
index c17c17be..0c3426c5 100644
--- a/tests/test_runner/run_test.ml
+++ b/tests/test_runner/run_test.ml
@@ -50,25 +50,35 @@ end
 (* Run Aeneas on a specific input with the given options *)
 let run_aeneas (env : runner_env) (case : Input.t) (backend : Backend.t) =
   let backend_str = Backend.to_string backend in
+  let backend_command = Backend.to_command backend in
   let input_file = concat_path [ env.llbc_dir; case.name ] ^ ".llbc" in
   let output_file =
     Filename.remove_extension case.path ^ "." ^ backend_str ^ ".out"
   in
+
   let per_backend = Backend.Map.find backend case.per_backend in
   let subdir = per_backend.subdir in
   let check_output = per_backend.check_output in
   let aeneas_options = per_backend.aeneas_options in
   let action = per_backend.action in
-  let dest_dir = concat_path [ env.dest_dir; backend_str; subdir ] in
+  (* No destination directory if we borrow-check *)
+  let dest_command =
+    match backend with
+    | Backend.BorrowCheck -> []
+    | _ ->
+        let subdir = match subdir with None -> [] | Some x -> [ x ] in
+        [ "-dest"; concat_path ([ env.dest_dir; backend_str ] @ subdir) ]
+  in
 
   (* Build the command *)
-  let args =
-    [ env.aeneas_path; input_file; "-dest"; dest_dir; "-backend"; backend_str ]
-  in
+  let args = [ env.aeneas_path; input_file ] @ dest_command @ backend_command in
+  (* If we target a specific backend and the test is known to fail, we abort
+     on error so as not to generate any files *)
   let abort_on_error =
     match action with
     | Skip | Normal -> []
-    | KnownFailure -> [ "-abort-on-error" ]
+    | KnownFailure ->
+        if backend = Backend.BorrowCheck then [] else [ "-abort-on-error" ]
   in
   let args = List.concat [ args; aeneas_options; abort_on_error ] in
   let cmd = Command.make args in