diff --git a/tests/coq/arrays/Arrays.v b/tests/coq/arrays/Arrays.v
index 57c9de40..7e82ef8b 100644
--- a/tests/coq/arrays/Arrays.v
+++ b/tests/coq/arrays/Arrays.v
@@ -371,7 +371,7 @@ Definition non_copyable_array : result unit :=
 .
 
 (** [arrays::sum]: loop 0:
-    Source: 'tests/src/arrays.rs', lines 247:4-253:1 *)
+    Source: 'tests/src/arrays.rs', lines 248:4-251:5 *)
 Fixpoint sum_loop
   (n : nat) (s : slice u32) (sum1 : u32) (i : usize) : result u32 :=
   match n with
@@ -395,7 +395,7 @@ Definition sum (n : nat) (s : slice u32) : result u32 :=
 .
 
 (** [arrays::sum2]: loop 0:
-    Source: 'tests/src/arrays.rs', lines 258:4-264:1 *)
+    Source: 'tests/src/arrays.rs', lines 259:4-262:5 *)
 Fixpoint sum2_loop
   (n : nat) (s : slice u32) (s2 : slice u32) (sum1 : u32) (i : usize) :
   result u32
@@ -498,7 +498,7 @@ Definition ite : result unit :=
 .
 
 (** [arrays::zero_slice]: loop 0:
-    Source: 'tests/src/arrays.rs', lines 308:4-313:1 *)
+    Source: 'tests/src/arrays.rs', lines 309:4-312:5 *)
 Fixpoint zero_slice_loop
   (n : nat) (a : slice u8) (i : usize) (len : usize) : result (slice u8) :=
   match n with
@@ -522,7 +522,7 @@ Definition zero_slice (n : nat) (a : slice u8) : result (slice u8) :=
 .
 
 (** [arrays::iter_mut_slice]: loop 0:
-    Source: 'tests/src/arrays.rs', lines 317:4-321:1 *)
+    Source: 'tests/src/arrays.rs', lines 318:4-320:5 *)
 Fixpoint iter_mut_slice_loop
   (n : nat) (len : usize) (i : usize) : result unit :=
   match n with
@@ -541,7 +541,7 @@ Definition iter_mut_slice (n : nat) (a : slice u8) : result (slice u8) :=
 .
 
 (** [arrays::sum_mut_slice]: loop 0:
-    Source: 'tests/src/arrays.rs', lines 325:4-331:1 *)
+    Source: 'tests/src/arrays.rs', lines 326:4-329:5 *)
 Fixpoint sum_mut_slice_loop
   (n : nat) (a : slice u32) (i : usize) (s : u32) : result u32 :=
   match n with
diff --git a/tests/coq/betree/Betree_Funs.v b/tests/coq/betree/Betree_Funs.v
index e3def11f..7313e65b 100644
--- a/tests/coq/betree/Betree_Funs.v
+++ b/tests/coq/betree/Betree_Funs.v
@@ -89,7 +89,7 @@ Definition betree_upsert_update
 .
 
 (** [betree::betree::{betree::betree::List<T>}#1::len]: loop 0:
-    Source: 'src/betree.rs', lines 278:8-284:5 *)
+    Source: 'src/betree.rs', lines 279:8-282:9 *)
 Fixpoint betree_List_len_loop
   {T : Type} (n : nat) (self : betree_List_t T) (len : u64) : result u64 :=
   match n with
@@ -111,7 +111,7 @@ Definition betree_List_len
 .
 
 (** [betree::betree::{betree::betree::List<T>}#1::reverse]: loop 0:
-    Source: 'src/betree.rs', lines 305:8-312:5 *)
+    Source: 'src/betree.rs', lines 306:8-310:9 *)
 Fixpoint betree_List_reverse_loop
   {T : Type} (n : nat) (self : betree_List_t T) (out : betree_List_t T) :
   result (betree_List_t T)
@@ -135,7 +135,7 @@ Definition betree_List_reverse
 .
 
 (** [betree::betree::{betree::betree::List<T>}#1::split_at]: loop 0:
-    Source: 'src/betree.rs', lines 289:8-302:5 *)
+    Source: 'src/betree.rs', lines 290:8-300:9 *)
 Fixpoint betree_List_split_at_loop
   {T : Type} (n : nat) (n1 : u64) (beg : betree_List_t T)
   (self : betree_List_t T) :
@@ -204,7 +204,7 @@ Definition betree_ListPairU64T_head_has_key
 .
 
 (** [betree::betree::{betree::betree::List<(u64, T)>}#2::partition_at_pivot]: loop 0:
-    Source: 'src/betree.rs', lines 358:8-370:5 *)
+    Source: 'src/betree.rs', lines 359:8-368:9 *)
 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)) :
@@ -276,7 +276,7 @@ Definition betree_Leaf_split
 .
 
 (** [betree::betree::{betree::betree::Node}#5::lookup_first_message_for_key]: loop 0:
-    Source: 'src/betree.rs', lines 792:4-810:5 *)
+    Source: 'src/betree.rs', lines 796:8-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 *
@@ -313,7 +313,7 @@ Definition betree_Node_lookup_first_message_for_key
 .
 
 (** [betree::betree::{betree::betree::Node}#5::apply_upserts]: loop 0:
-    Source: 'src/betree.rs', lines 820:4-844:5 *)
+    Source: 'src/betree.rs', lines 821:8-838:9 *)
 Fixpoint betree_Node_apply_upserts_loop
   (n : nat) (msgs : betree_List_t (u64 * betree_Message_t)) (prev : option u64)
   (key : u64) :
@@ -353,7 +353,7 @@ Definition betree_Node_apply_upserts
 .
 
 (** [betree::betree::{betree::betree::Node}#5::lookup_in_bindings]: loop 0:
-    Source: 'src/betree.rs', lines 649:4-660:5 *)
+    Source: 'src/betree.rs', lines 650:8-660:5 *)
 Fixpoint betree_Node_lookup_in_bindings_loop
   (n : nat) (key : u64) (bindings : betree_List_t (u64 * u64)) :
   result (option u64)
@@ -476,7 +476,7 @@ with betree_Node_lookup
 .
 
 (** [betree::betree::{betree::betree::Node}#5::filter_messages_for_key]: loop 0:
-    Source: 'src/betree.rs', lines 683:4-692:5 *)
+    Source: 'src/betree.rs', lines 684:8-691:9 *)
 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))
@@ -508,7 +508,7 @@ Definition betree_Node_filter_messages_for_key
 .
 
 (** [betree::betree::{betree::betree::Node}#5::lookup_first_message_after_key]: loop 0:
-    Source: 'src/betree.rs', lines 694:4-706:5 *)
+    Source: 'src/betree.rs', lines 698:8-704:9 *)
 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 *
@@ -595,7 +595,7 @@ Definition betree_Node_apply_to_internal
 .
 
 (** [betree::betree::{betree::betree::Node}#5::apply_messages_to_internal]: loop 0:
-    Source: 'src/betree.rs', lines 518:4-526:5 *)
+    Source: 'src/betree.rs', lines 522:8-525:9 *)
 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)) :
@@ -625,7 +625,7 @@ Definition betree_Node_apply_messages_to_internal
 .
 
 (** [betree::betree::{betree::betree::Node}#5::lookup_mut_in_bindings]: loop 0:
-    Source: 'src/betree.rs', lines 664:4-677:5 *)
+    Source: 'src/betree.rs', lines 668:8-675:9 *)
 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
@@ -700,7 +700,7 @@ Definition betree_Node_apply_to_leaf
 .
 
 (** [betree::betree::{betree::betree::Node}#5::apply_messages_to_leaf]: loop 0:
-    Source: 'src/betree.rs', lines 463:4-471:5 *)
+    Source: 'src/betree.rs', lines 467:8-470:9 *)
 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)) :
diff --git a/tests/coq/demo/Demo.v b/tests/coq/demo/Demo.v
index 7fb071c1..450c279d 100644
--- a/tests/coq/demo/Demo.v
+++ b/tests/coq/demo/Demo.v
@@ -65,7 +65,7 @@ Fixpoint list_nth {T : Type} (n : nat) (l : CList_t T) (i : u32) : result T :=
 .
 
 (** [demo::list_nth1]: loop 0:
-    Source: 'tests/src/demo.rs', lines 56:0-65:1 *)
+    Source: 'tests/src/demo.rs', lines 57:4-65:1 *)
 Fixpoint list_nth1_loop
   {T : Type} (n : nat) (l : CList_t T) (i : u32) : result T :=
   match n with
diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v
index 7c2eca6b..dcb213af 100644
--- a/tests/coq/hashmap/Hashmap_Funs.v
+++ b/tests/coq/hashmap/Hashmap_Funs.v
@@ -18,7 +18,7 @@ Definition hash_key (k : usize) : result usize :=
   Ok k.
 
 (** [hashmap::{hashmap::HashMap<T>}::allocate_slots]: loop 0:
-    Source: 'tests/src/hashmap.rs', lines 63:4-69:5 *)
+    Source: 'tests/src/hashmap.rs', lines 64:8-67:9 *)
 Fixpoint hashMap_allocate_slots_loop
   {T : Type} (n : nat) (slots : alloc_vec_Vec (AList_t T)) (n1 : usize) :
   result (alloc_vec_Vec (AList_t T))
@@ -71,7 +71,7 @@ Definition hashMap_new (T : Type) (n : nat) : result (HashMap_t T) :=
 .
 
 (** [hashmap::{hashmap::HashMap<T>}::clear]: loop 0:
-    Source: 'tests/src/hashmap.rs', lines 97:8-102:5 *)
+    Source: 'tests/src/hashmap.rs', lines 98:8-101:9 *)
 Fixpoint hashMap_clear_loop
   {T : Type} (n : nat) (slots : alloc_vec_Vec (AList_t T)) (i : usize) :
   result (alloc_vec_Vec (AList_t T))
@@ -115,7 +115,7 @@ Definition hashMap_len {T : Type} (self : HashMap_t T) : result usize :=
 .
 
 (** [hashmap::{hashmap::HashMap<T>}::insert_in_list]: loop 0:
-    Source: 'tests/src/hashmap.rs', lines 111:4-128:5 *)
+    Source: 'tests/src/hashmap.rs', lines 1:0-127:9 *)
 Fixpoint hashMap_insert_in_list_loop
   {T : Type} (n : nat) (key : usize) (value : T) (ls : AList_t T) :
   result (bool * (AList_t T))
@@ -185,7 +185,7 @@ Definition hashMap_insert_no_resize
 .
 
 (** [hashmap::{hashmap::HashMap<T>}::move_elements_from_list]: loop 0:
-    Source: 'tests/src/hashmap.rs', lines 194:4-207:5 *)
+    Source: 'tests/src/hashmap.rs', lines 197:12-204:17 *)
 Fixpoint hashMap_move_elements_from_list_loop
   {T : Type} (n : nat) (ntable : HashMap_t T) (ls : AList_t T) :
   result (HashMap_t T)
@@ -212,7 +212,7 @@ Definition hashMap_move_elements_from_list
 .
 
 (** [hashmap::{hashmap::HashMap<T>}::move_elements]: loop 0:
-    Source: 'tests/src/hashmap.rs', lines 182:8-191:5 *)
+    Source: 'tests/src/hashmap.rs', lines 183:8-190:9 *)
 Fixpoint hashMap_move_elements_loop
   {T : Type} (n : nat) (ntable : HashMap_t T)
   (slots : alloc_vec_Vec (AList_t T)) (i : usize) :
@@ -313,7 +313,7 @@ Definition hashMap_insert
 .
 
 (** [hashmap::{hashmap::HashMap<T>}::contains_key_in_list]: loop 0:
-    Source: 'tests/src/hashmap.rs', lines 217:4-230:5 *)
+    Source: 'tests/src/hashmap.rs', lines 1:0-229:9 *)
 Fixpoint hashMap_contains_key_in_list_loop
   {T : Type} (n : nat) (key : usize) (ls : AList_t T) : result bool :=
   match n with
@@ -350,7 +350,7 @@ Definition hashMap_contains_key
 .
 
 (** [hashmap::{hashmap::HashMap<T>}::get_in_list]: loop 0:
-    Source: 'tests/src/hashmap.rs', lines 235:4-248:5 *)
+    Source: 'tests/src/hashmap.rs', lines 236:8-248:5 *)
 Fixpoint hashMap_get_in_list_loop
   {T : Type} (n : nat) (key : usize) (ls : AList_t T) : result T :=
   match n with
@@ -385,7 +385,7 @@ Definition hashMap_get
 .
 
 (** [hashmap::{hashmap::HashMap<T>}::get_mut_in_list]: loop 0:
-    Source: 'tests/src/hashmap.rs', lines 256:4-265:5 *)
+    Source: 'tests/src/hashmap.rs', lines 257:8-265:5 *)
 Fixpoint hashMap_get_mut_in_list_loop
   {T : Type} (n : nat) (ls : AList_t T) (key : usize) :
   result (T * (T -> result (AList_t T)))
@@ -450,7 +450,7 @@ Definition hashMap_get_mut
 .
 
 (** [hashmap::{hashmap::HashMap<T>}::remove_from_list]: loop 0:
-    Source: 'tests/src/hashmap.rs', lines 276:4-302:5 *)
+    Source: 'tests/src/hashmap.rs', lines 1:0-299:17 *)
 Fixpoint hashMap_remove_from_list_loop
   {T : Type} (n : nat) (key : usize) (ls : AList_t T) :
   result ((option T) * (AList_t T))
diff --git a/tests/coq/misc/InfiniteLoop.v b/tests/coq/misc/InfiniteLoop.v
index 5d4e195c..10703bfa 100644
--- a/tests/coq/misc/InfiniteLoop.v
+++ b/tests/coq/misc/InfiniteLoop.v
@@ -14,7 +14,7 @@ Definition bar : result unit :=
   Ok tt.
 
 (** [infinite_loop::foo]: loop 0:
-    Source: 'tests/src/infinite-loop.rs', lines 6:0-10:1 *)
+    Source: 'tests/src/infinite-loop.rs', lines 8:8-8:13 *)
 Fixpoint foo_loop (n : nat) : result unit :=
   match n with | O => Fail_ OutOfFuel | S n1 => _ <- bar; foo_loop n1 end
 .
diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v
index c0704d60..495f0e71 100644
--- a/tests/coq/misc/Loops.v
+++ b/tests/coq/misc/Loops.v
@@ -9,7 +9,7 @@ Local Open Scope Primitives_scope.
 Module Loops.
 
 (** [loops::sum]: loop 0:
-    Source: 'tests/src/loops.rs', lines 10:4-18:1 *)
+    Source: 'tests/src/loops.rs', lines 11:4-14:5 *)
 Fixpoint sum_loop (n : nat) (max : u32) (i : u32) (s : u32) : result u32 :=
   match n with
   | O => Fail_ OutOfFuel
@@ -27,7 +27,7 @@ Definition sum (n : nat) (max : u32) : result u32 :=
 .
 
 (** [loops::sum_with_mut_borrows]: loop 0:
-    Source: 'tests/src/loops.rs', lines 25:4-35:1 *)
+    Source: 'tests/src/loops.rs', lines 26:4-31:5 *)
 Fixpoint sum_with_mut_borrows_loop
   (n : nat) (max : u32) (i : u32) (s : u32) : result u32 :=
   match n with
@@ -49,7 +49,7 @@ Definition sum_with_mut_borrows (n : nat) (max : u32) : result u32 :=
 .
 
 (** [loops::sum_with_shared_borrows]: loop 0:
-    Source: 'tests/src/loops.rs', lines 40:4-52:1 *)
+    Source: 'tests/src/loops.rs', lines 41:4-48:5 *)
 Fixpoint sum_with_shared_borrows_loop
   (n : nat) (max : u32) (i : u32) (s : u32) : result u32 :=
   match n with
@@ -71,7 +71,7 @@ Definition sum_with_shared_borrows (n : nat) (max : u32) : result u32 :=
 .
 
 (** [loops::sum_array]: loop 0:
-    Source: 'tests/src/loops.rs', lines 56:4-62:1 *)
+    Source: 'tests/src/loops.rs', lines 57:4-60:5 *)
 Fixpoint sum_array_loop
   {N : usize} (n : nat) (a : array u32 N) (i : usize) (s : u32) : result u32 :=
   match n with
@@ -94,7 +94,7 @@ Definition sum_array {N : usize} (n : nat) (a : array u32 N) : result u32 :=
 .
 
 (** [loops::clear]: loop 0:
-    Source: 'tests/src/loops.rs', lines 67:4-72:1 *)
+    Source: 'tests/src/loops.rs', lines 68:4-71:5 *)
 Fixpoint clear_loop
   (n : nat) (v : alloc_vec_Vec u32) (i : usize) : result (alloc_vec_Vec u32) :=
   match n with
@@ -132,7 +132,7 @@ Arguments List_Cons { _ }.
 Arguments List_Nil { _ }.
 
 (** [loops::list_mem]: loop 0:
-    Source: 'tests/src/loops.rs', lines 80:0-89:1 *)
+    Source: 'tests/src/loops.rs', lines 81:4-89:1 *)
 Fixpoint list_mem_loop (n : nat) (x : u32) (ls : List_t u32) : result bool :=
   match n with
   | O => Fail_ OutOfFuel
@@ -151,7 +151,7 @@ Definition list_mem (n : nat) (x : u32) (ls : List_t u32) : result bool :=
 .
 
 (** [loops::list_nth_mut_loop]: loop 0:
-    Source: 'tests/src/loops.rs', lines 92:0-102:1 *)
+    Source: 'tests/src/loops.rs', lines 93:4-102:1 *)
 Fixpoint list_nth_mut_loop_loop
   {T : Type} (n : nat) (ls : List_t T) (i : u32) :
   result (T * (T -> result (List_t T)))
@@ -184,7 +184,7 @@ Definition list_nth_mut_loop
 .
 
 (** [loops::list_nth_shared_loop]: loop 0:
-    Source: 'tests/src/loops.rs', lines 105:0-115:1 *)
+    Source: 'tests/src/loops.rs', lines 106:4-115:1 *)
 Fixpoint list_nth_shared_loop_loop
   {T : Type} (n : nat) (ls : List_t T) (i : u32) : result T :=
   match n with
@@ -208,7 +208,7 @@ Definition list_nth_shared_loop
 .
 
 (** [loops::get_elem_mut]: loop 0:
-    Source: 'tests/src/loops.rs', lines 117:0-131:1 *)
+    Source: 'tests/src/loops.rs', lines 119:4-131:1 *)
 Fixpoint get_elem_mut_loop
   (n : nat) (x : usize) (ls : List_t usize) :
   result (usize * (usize -> result (List_t usize)))
@@ -249,7 +249,7 @@ Definition get_elem_mut
 .
 
 (** [loops::get_elem_shared]: loop 0:
-    Source: 'tests/src/loops.rs', lines 133:0-147:1 *)
+    Source: 'tests/src/loops.rs', lines 135:4-147:1 *)
 Fixpoint get_elem_shared_loop
   (n : nat) (x : usize) (ls : List_t usize) : result usize :=
   match n with
@@ -289,7 +289,7 @@ Definition id_shared {T : Type} (ls : List_t T) : result (List_t T) :=
   Ok ls.
 
 (** [loops::list_nth_mut_loop_with_id]: loop 0:
-    Source: 'tests/src/loops.rs', lines 158:0-169:1 *)
+    Source: 'tests/src/loops.rs', lines 160:4-169:1 *)
 Fixpoint list_nth_mut_loop_with_id_loop
   {T : Type} (n : nat) (i : u32) (ls : List_t T) :
   result (T * (T -> result (List_t T)))
@@ -327,7 +327,7 @@ Definition list_nth_mut_loop_with_id
 .
 
 (** [loops::list_nth_shared_loop_with_id]: loop 0:
-    Source: 'tests/src/loops.rs', lines 172:0-183:1 *)
+    Source: 'tests/src/loops.rs', lines 174:4-183:1 *)
 Fixpoint list_nth_shared_loop_with_id_loop
   {T : Type} (n : nat) (i : u32) (ls : List_t T) : result T :=
   match n with
@@ -351,7 +351,7 @@ Definition list_nth_shared_loop_with_id
 .
 
 (** [loops::list_nth_mut_loop_pair]: loop 0:
-    Source: 'tests/src/loops.rs', lines 188:0-209:1 *)
+    Source: 'tests/src/loops.rs', lines 194:8-194:24 *)
 Fixpoint list_nth_mut_loop_pair_loop
   {T : Type} (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result ((T * T) * (T -> result (List_t T)) * (T -> result (List_t T)))
@@ -394,7 +394,7 @@ Definition list_nth_mut_loop_pair
 .
 
 (** [loops::list_nth_shared_loop_pair]: loop 0:
-    Source: 'tests/src/loops.rs', lines 212:0-233:1 *)
+    Source: 'tests/src/loops.rs', lines 218:8-218:24 *)
 Fixpoint list_nth_shared_loop_pair_loop
   {T : Type} (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result (T * T)
@@ -427,7 +427,7 @@ Definition list_nth_shared_loop_pair
 .
 
 (** [loops::list_nth_mut_loop_pair_merge]: loop 0:
-    Source: 'tests/src/loops.rs', lines 237:0-252:1 *)
+    Source: 'tests/src/loops.rs', lines 242:4-252:1 *)
 Fixpoint list_nth_mut_loop_pair_merge_loop
   {T : Type} (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result ((T * T) * ((T * T) -> result ((List_t T) * (List_t T))))
@@ -472,7 +472,7 @@ Definition list_nth_mut_loop_pair_merge
 .
 
 (** [loops::list_nth_shared_loop_pair_merge]: loop 0:
-    Source: 'tests/src/loops.rs', lines 255:0-270:1 *)
+    Source: 'tests/src/loops.rs', lines 260:4-270:1 *)
 Fixpoint list_nth_shared_loop_pair_merge_loop
   {T : Type} (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result (T * T)
@@ -506,7 +506,7 @@ Definition list_nth_shared_loop_pair_merge
 .
 
 (** [loops::list_nth_mut_shared_loop_pair]: loop 0:
-    Source: 'tests/src/loops.rs', lines 273:0-288:1 *)
+    Source: 'tests/src/loops.rs', lines 278:4-288:1 *)
 Fixpoint list_nth_mut_shared_loop_pair_loop
   {T : Type} (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result ((T * T) * (T -> result (List_t T)))
@@ -546,7 +546,7 @@ Definition list_nth_mut_shared_loop_pair
 .
 
 (** [loops::list_nth_mut_shared_loop_pair_merge]: loop 0:
-    Source: 'tests/src/loops.rs', lines 292:0-307:1 *)
+    Source: 'tests/src/loops.rs', lines 297:4-307:1 *)
 Fixpoint list_nth_mut_shared_loop_pair_merge_loop
   {T : Type} (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result ((T * T) * (T -> result (List_t T)))
@@ -586,7 +586,7 @@ Definition list_nth_mut_shared_loop_pair_merge
 .
 
 (** [loops::list_nth_shared_mut_loop_pair]: loop 0:
-    Source: 'tests/src/loops.rs', lines 311:0-326:1 *)
+    Source: 'tests/src/loops.rs', lines 316:4-326:1 *)
 Fixpoint list_nth_shared_mut_loop_pair_loop
   {T : Type} (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result ((T * T) * (T -> result (List_t T)))
@@ -626,7 +626,7 @@ Definition list_nth_shared_mut_loop_pair
 .
 
 (** [loops::list_nth_shared_mut_loop_pair_merge]: loop 0:
-    Source: 'tests/src/loops.rs', lines 330:0-345:1 *)
+    Source: 'tests/src/loops.rs', lines 335:4-345:1 *)
 Fixpoint list_nth_shared_mut_loop_pair_merge_loop
   {T : Type} (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result ((T * T) * (T -> result (List_t T)))
@@ -666,7 +666,7 @@ Definition list_nth_shared_mut_loop_pair_merge
 .
 
 (** [loops::ignore_input_mut_borrow]: loop 0:
-    Source: 'tests/src/loops.rs', lines 349:0-353:1 *)
+    Source: 'tests/src/loops.rs', lines 350:4-352:5 *)
 Fixpoint ignore_input_mut_borrow_loop (n : nat) (i : u32) : result unit :=
   match n with
   | O => Fail_ OutOfFuel
@@ -685,7 +685,7 @@ Definition ignore_input_mut_borrow
 .
 
 (** [loops::incr_ignore_input_mut_borrow]: loop 0:
-    Source: 'tests/src/loops.rs', lines 357:0-362:1 *)
+    Source: 'tests/src/loops.rs', lines 359:4-361:5 *)
 Fixpoint incr_ignore_input_mut_borrow_loop (n : nat) (i : u32) : result unit :=
   match n with
   | O => Fail_ OutOfFuel
@@ -704,7 +704,7 @@ Definition incr_ignore_input_mut_borrow
 .
 
 (** [loops::ignore_input_shared_borrow]: loop 0:
-    Source: 'tests/src/loops.rs', lines 366:0-370:1 *)
+    Source: 'tests/src/loops.rs', lines 367:4-369:5 *)
 Fixpoint ignore_input_shared_borrow_loop (n : nat) (i : u32) : result unit :=
   match n with
   | O => Fail_ OutOfFuel
diff --git a/tests/coq/rename_attribute/RenameAttribute.v b/tests/coq/rename_attribute/RenameAttribute.v
index d3d717f1..8111a9ba 100644
--- a/tests/coq/rename_attribute/RenameAttribute.v
+++ b/tests/coq/rename_attribute/RenameAttribute.v
@@ -79,7 +79,7 @@ Fixpoint factfn (n : nat) (n1 : u64) : result u64 :=
 .
 
 (** [rename_attribute::sum]: loop 0:
-    Source: 'tests/src/rename_attribute.rs', lines 67:4-75:1 *)
+    Source: 'tests/src/rename_attribute.rs', lines 68:4-71:5 *)
 Fixpoint no_borrows_sum_loop
   (n : nat) (max : u32) (i : u32) (s : u32) : result u32 :=
   match n with
diff --git a/tests/fstar/arrays/Arrays.Clauses.Template.fst b/tests/fstar/arrays/Arrays.Clauses.Template.fst
index b5818ab6..47b0d283 100644
--- a/tests/fstar/arrays/Arrays.Clauses.Template.fst
+++ b/tests/fstar/arrays/Arrays.Clauses.Template.fst
@@ -7,31 +7,31 @@ open Arrays.Types
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
 (** [arrays::sum]: decreases clause
-    Source: 'tests/src/arrays.rs', lines 247:4-253:1 *)
+    Source: 'tests/src/arrays.rs', lines 248:4-251:5 *)
 unfold
 let sum_loop_decreases (s : slice u32) (sum1 : u32) (i : usize) : nat =
   admit ()
 
 (** [arrays::sum2]: decreases clause
-    Source: 'tests/src/arrays.rs', lines 258:4-264:1 *)
+    Source: 'tests/src/arrays.rs', lines 259:4-262:5 *)
 unfold
 let sum2_loop_decreases (s : slice u32) (s2 : slice u32) (sum1 : u32)
   (i : usize) : nat =
   admit ()
 
 (** [arrays::zero_slice]: decreases clause
-    Source: 'tests/src/arrays.rs', lines 308:4-313:1 *)
+    Source: 'tests/src/arrays.rs', lines 309:4-312:5 *)
 unfold
 let zero_slice_loop_decreases (a : slice u8) (i : usize) (len : usize) : nat =
   admit ()
 
 (** [arrays::iter_mut_slice]: decreases clause
-    Source: 'tests/src/arrays.rs', lines 317:4-321:1 *)
+    Source: 'tests/src/arrays.rs', lines 318:4-320:5 *)
 unfold
 let iter_mut_slice_loop_decreases (len : usize) (i : usize) : nat = admit ()
 
 (** [arrays::sum_mut_slice]: decreases clause
-    Source: 'tests/src/arrays.rs', lines 325:4-331:1 *)
+    Source: 'tests/src/arrays.rs', lines 326:4-329:5 *)
 unfold
 let sum_mut_slice_loop_decreases (a : slice u32) (i : usize) (s : u32) : nat =
   admit ()
diff --git a/tests/fstar/arrays/Arrays.Funs.fst b/tests/fstar/arrays/Arrays.Funs.fst
index 76a43a45..e02d433e 100644
--- a/tests/fstar/arrays/Arrays.Funs.fst
+++ b/tests/fstar/arrays/Arrays.Funs.fst
@@ -299,7 +299,7 @@ let non_copyable_array : result unit =
   take_array_t (mk_array 2 [ AB_A; AB_B ])
 
 (** [arrays::sum]: loop 0:
-    Source: 'tests/src/arrays.rs', lines 247:4-253:1 *)
+    Source: 'tests/src/arrays.rs', lines 248:4-251:5 *)
 let rec sum_loop
   (s : slice u32) (sum1 : u32) (i : usize) :
   Tot (result u32) (decreases (sum_loop_decreases s sum1 i))
@@ -319,7 +319,7 @@ let sum (s : slice u32) : result u32 =
   sum_loop s 0 0
 
 (** [arrays::sum2]: loop 0:
-    Source: 'tests/src/arrays.rs', lines 258:4-264:1 *)
+    Source: 'tests/src/arrays.rs', lines 259:4-262:5 *)
 let rec sum2_loop
   (s : slice u32) (s2 : slice u32) (sum1 : u32) (i : usize) :
   Tot (result u32) (decreases (sum2_loop_decreases s s2 sum1 i))
@@ -402,7 +402,7 @@ let ite : result unit =
   Ok ()
 
 (** [arrays::zero_slice]: loop 0:
-    Source: 'tests/src/arrays.rs', lines 308:4-313:1 *)
+    Source: 'tests/src/arrays.rs', lines 309:4-312:5 *)
 let rec zero_slice_loop
   (a : slice u8) (i : usize) (len : usize) :
   Tot (result (slice u8)) (decreases (zero_slice_loop_decreases a i len))
@@ -421,7 +421,7 @@ let zero_slice (a : slice u8) : result (slice u8) =
   let len = slice_len a in zero_slice_loop a 0 len
 
 (** [arrays::iter_mut_slice]: loop 0:
-    Source: 'tests/src/arrays.rs', lines 317:4-321:1 *)
+    Source: 'tests/src/arrays.rs', lines 318:4-320:5 *)
 let rec iter_mut_slice_loop
   (len : usize) (i : usize) :
   Tot (result unit) (decreases (iter_mut_slice_loop_decreases len i))
@@ -436,7 +436,7 @@ let iter_mut_slice (a : slice u8) : result (slice u8) =
   let len = slice_len a in let* _ = iter_mut_slice_loop len 0 in Ok a
 
 (** [arrays::sum_mut_slice]: loop 0:
-    Source: 'tests/src/arrays.rs', lines 325:4-331:1 *)
+    Source: 'tests/src/arrays.rs', lines 326:4-329:5 *)
 let rec sum_mut_slice_loop
   (a : slice u32) (i : usize) (s : u32) :
   Tot (result u32) (decreases (sum_mut_slice_loop_decreases a i s))
diff --git a/tests/fstar/betree/Betree.Clauses.Template.fst b/tests/fstar/betree/Betree.Clauses.Template.fst
index c82ecd93..648cd72b 100644
--- a/tests/fstar/betree/Betree.Clauses.Template.fst
+++ b/tests/fstar/betree/Betree.Clauses.Template.fst
@@ -7,28 +7,28 @@ 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 278:8-284:5 *)
+    Source: 'src/betree.rs', lines 279:8-282:9 *)
 unfold
 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 305:8-312:5 *)
+    Source: 'src/betree.rs', lines 306:8-310:9 *)
 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 289:8-302:5 *)
+    Source: 'src/betree.rs', lines 290:8-300:9 *)
 unfold
 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 358:8-370:5 *)
+    Source: 'src/betree.rs', lines 359:8-368:9 *)
 unfold
 let betree_ListPairU64T_partition_at_pivot_loop_decreases (#t : Type0)
   (pivot : u64) (beg : betree_List_t (u64 & t))
@@ -36,14 +36,14 @@ let betree_ListPairU64T_partition_at_pivot_loop_decreases (#t : Type0)
   admit ()
 
 (** [betree::betree::{betree::betree::Node}#5::lookup_first_message_for_key]: decreases clause
-    Source: 'src/betree.rs', lines 792:4-810:5 *)
+    Source: 'src/betree.rs', lines 796:8-810:5 *)
 unfold
 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::apply_upserts]: decreases clause
-    Source: 'src/betree.rs', lines 820:4-844:5 *)
+    Source: 'src/betree.rs', lines 821:8-838:9 *)
 unfold
 let betree_Node_apply_upserts_loop_decreases
   (msgs : betree_List_t (u64 & betree_Message_t)) (prev : option u64)
@@ -51,7 +51,7 @@ let betree_Node_apply_upserts_loop_decreases
   admit ()
 
 (** [betree::betree::{betree::betree::Node}#5::lookup_in_bindings]: decreases clause
-    Source: 'src/betree.rs', lines 649:4-660:5 *)
+    Source: 'src/betree.rs', lines 650:8-660:5 *)
 unfold
 let betree_Node_lookup_in_bindings_loop_decreases (key : u64)
   (bindings : betree_List_t (u64 & u64)) : nat =
@@ -72,21 +72,21 @@ let betree_Node_lookup_decreases (self : betree_Node_t) (key : u64)
   admit ()
 
 (** [betree::betree::{betree::betree::Node}#5::filter_messages_for_key]: decreases clause
-    Source: 'src/betree.rs', lines 683:4-692:5 *)
+    Source: 'src/betree.rs', lines 684:8-691:9 *)
 unfold
 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 694:4-706:5 *)
+    Source: 'src/betree.rs', lines 698:8-704:9 *)
 unfold
 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 518:4-526:5 *)
+    Source: 'src/betree.rs', lines 522:8-525:9 *)
 unfold
 let betree_Node_apply_messages_to_internal_loop_decreases
   (msgs : betree_List_t (u64 & betree_Message_t))
@@ -94,14 +94,14 @@ let betree_Node_apply_messages_to_internal_loop_decreases
   admit ()
 
 (** [betree::betree::{betree::betree::Node}#5::lookup_mut_in_bindings]: decreases clause
-    Source: 'src/betree.rs', lines 664:4-677:5 *)
+    Source: 'src/betree.rs', lines 668:8-675:9 *)
 unfold
 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 463:4-471:5 *)
+    Source: 'src/betree.rs', lines 467:8-470:9 *)
 unfold
 let betree_Node_apply_messages_to_leaf_loop_decreases
   (bindings : betree_List_t (u64 & u64))
diff --git a/tests/fstar/betree/Betree.Funs.fst b/tests/fstar/betree/Betree.Funs.fst
index a222260f..de20df14 100644
--- a/tests/fstar/betree/Betree.Funs.fst
+++ b/tests/fstar/betree/Betree.Funs.fst
@@ -76,7 +76,7 @@ let betree_upsert_update
   end
 
 (** [betree::betree::{betree::betree::List<T>}#1::len]: loop 0:
-    Source: 'src/betree.rs', lines 278:8-284:5 *)
+    Source: 'src/betree.rs', lines 279:8-282:9 *)
 let rec betree_List_len_loop
   (#t : Type0) (self : betree_List_t t) (len : u64) :
   Tot (result u64) (decreases (betree_List_len_loop_decreases self len))
@@ -93,7 +93,7 @@ let betree_List_len (#t : Type0) (self : betree_List_t t) : result u64 =
   betree_List_len_loop self 0
 
 (** [betree::betree::{betree::betree::List<T>}#1::reverse]: loop 0:
-    Source: 'src/betree.rs', lines 305:8-312:5 *)
+    Source: 'src/betree.rs', lines 306:8-310:9 *)
 let rec betree_List_reverse_loop
   (#t : Type0) (self : betree_List_t t) (out : betree_List_t t) :
   Tot (result (betree_List_t t))
@@ -112,7 +112,7 @@ let betree_List_reverse
   betree_List_reverse_loop self Betree_List_Nil
 
 (** [betree::betree::{betree::betree::List<T>}#1::split_at]: loop 0:
-    Source: 'src/betree.rs', lines 289:8-302:5 *)
+    Source: 'src/betree.rs', lines 290:8-300:9 *)
 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)))
@@ -171,7 +171,7 @@ let betree_ListPairU64T_head_has_key
   end
 
 (** [betree::betree::{betree::betree::List<(u64, T)>}#2::partition_at_pivot]: loop 0:
-    Source: 'src/betree.rs', lines 358:8-370:5 *)
+    Source: 'src/betree.rs', lines 359:8-368:9 *)
 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)) :
@@ -226,7 +226,7 @@ let betree_Leaf_split
     node_id_cnt2))
 
 (** [betree::betree::{betree::betree::Node}#5::lookup_first_message_for_key]: loop 0:
-    Source: 'src/betree.rs', lines 792:4-810:5 *)
+    Source: 'src/betree.rs', lines 796:8-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 &
@@ -260,7 +260,7 @@ let betree_Node_lookup_first_message_for_key
   betree_Node_lookup_first_message_for_key_loop key msgs
 
 (** [betree::betree::{betree::betree::Node}#5::apply_upserts]: loop 0:
-    Source: 'src/betree.rs', lines 820:4-844:5 *)
+    Source: 'src/betree.rs', lines 821:8-838:9 *)
 let rec betree_Node_apply_upserts_loop
   (msgs : betree_List_t (u64 & betree_Message_t)) (prev : option u64)
   (key : u64) :
@@ -294,7 +294,7 @@ let betree_Node_apply_upserts
   betree_Node_apply_upserts_loop msgs prev key
 
 (** [betree::betree::{betree::betree::Node}#5::lookup_in_bindings]: loop 0:
-    Source: 'src/betree.rs', lines 649:4-660:5 *)
+    Source: 'src/betree.rs', lines 650:8-660:5 *)
 let rec betree_Node_lookup_in_bindings_loop
   (key : u64) (bindings : betree_List_t (u64 & u64)) :
   Tot (result (option u64))
@@ -388,7 +388,7 @@ and betree_Node_lookup
   end
 
 (** [betree::betree::{betree::betree::Node}#5::filter_messages_for_key]: loop 0:
-    Source: 'src/betree.rs', lines 683:4-692:5 *)
+    Source: 'src/betree.rs', lines 684:8-691:9 *)
 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)))
@@ -414,7 +414,7 @@ let betree_Node_filter_messages_for_key
   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 *)
+    Source: 'src/betree.rs', lines 698:8-704:9 *)
 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 &
@@ -499,7 +499,7 @@ let betree_Node_apply_to_internal
     lookup_first_message_for_key_back msgs2
 
 (** [betree::betree::{betree::betree::Node}#5::apply_messages_to_internal]: loop 0:
-    Source: 'src/betree.rs', lines 518:4-526:5 *)
+    Source: 'src/betree.rs', lines 522:8-525:9 *)
 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)) :
@@ -525,7 +525,7 @@ let betree_Node_apply_messages_to_internal
   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 *)
+    Source: 'src/betree.rs', lines 668:8-675:9 *)
 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) ->
@@ -591,7 +591,7 @@ let betree_Node_apply_to_leaf
     end
 
 (** [betree::betree::{betree::betree::Node}#5::apply_messages_to_leaf]: loop 0:
-    Source: 'src/betree.rs', lines 463:4-471:5 *)
+    Source: 'src/betree.rs', lines 467:8-470:9 *)
 let rec betree_Node_apply_messages_to_leaf_loop
   (bindings : betree_List_t (u64 & u64))
   (new_msgs : betree_List_t (u64 & betree_Message_t)) :
diff --git a/tests/fstar/demo/Demo.fst b/tests/fstar/demo/Demo.fst
index b964b75a..97ffd3d2 100644
--- a/tests/fstar/demo/Demo.fst
+++ b/tests/fstar/demo/Demo.fst
@@ -55,7 +55,7 @@ let rec list_nth (#t : Type0) (n : nat) (l : cList_t t) (i : u32) : result t =
     end
 
 (** [demo::list_nth1]: loop 0:
-    Source: 'tests/src/demo.rs', lines 56:0-65:1 *)
+    Source: 'tests/src/demo.rs', lines 57:4-65:1 *)
 let rec list_nth1_loop
   (#t : Type0) (n : nat) (l : cList_t t) (i : u32) : result t =
   if is_zero n
diff --git a/tests/fstar/hashmap/Hashmap.Clauses.Template.fst b/tests/fstar/hashmap/Hashmap.Clauses.Template.fst
index ab2fc745..a81bf3da 100644
--- a/tests/fstar/hashmap/Hashmap.Clauses.Template.fst
+++ b/tests/fstar/hashmap/Hashmap.Clauses.Template.fst
@@ -7,63 +7,63 @@ open Hashmap.Types
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
 (** [hashmap::{hashmap::HashMap<T>}::allocate_slots]: decreases clause
-    Source: 'tests/src/hashmap.rs', lines 63:4-69:5 *)
+    Source: 'tests/src/hashmap.rs', lines 64:8-67:9 *)
 unfold
 let hashMap_allocate_slots_loop_decreases (#t : Type0)
   (slots : alloc_vec_Vec (aList_t t)) (n : usize) : nat =
   admit ()
 
 (** [hashmap::{hashmap::HashMap<T>}::clear]: decreases clause
-    Source: 'tests/src/hashmap.rs', lines 97:8-102:5 *)
+    Source: 'tests/src/hashmap.rs', lines 98:8-101:9 *)
 unfold
 let hashMap_clear_loop_decreases (#t : Type0)
   (slots : alloc_vec_Vec (aList_t t)) (i : usize) : nat =
   admit ()
 
 (** [hashmap::{hashmap::HashMap<T>}::insert_in_list]: decreases clause
-    Source: 'tests/src/hashmap.rs', lines 111:4-128:5 *)
+    Source: 'tests/src/hashmap.rs', lines 1:0-127:9 *)
 unfold
 let hashMap_insert_in_list_loop_decreases (#t : Type0) (key : usize)
   (value : t) (ls : aList_t t) : nat =
   admit ()
 
 (** [hashmap::{hashmap::HashMap<T>}::move_elements_from_list]: decreases clause
-    Source: 'tests/src/hashmap.rs', lines 194:4-207:5 *)
+    Source: 'tests/src/hashmap.rs', lines 197:12-204:17 *)
 unfold
 let hashMap_move_elements_from_list_loop_decreases (#t : Type0)
   (ntable : hashMap_t t) (ls : aList_t t) : nat =
   admit ()
 
 (** [hashmap::{hashmap::HashMap<T>}::move_elements]: decreases clause
-    Source: 'tests/src/hashmap.rs', lines 182:8-191:5 *)
+    Source: 'tests/src/hashmap.rs', lines 183:8-190:9 *)
 unfold
 let hashMap_move_elements_loop_decreases (#t : Type0) (ntable : hashMap_t t)
   (slots : alloc_vec_Vec (aList_t t)) (i : usize) : nat =
   admit ()
 
 (** [hashmap::{hashmap::HashMap<T>}::contains_key_in_list]: decreases clause
-    Source: 'tests/src/hashmap.rs', lines 217:4-230:5 *)
+    Source: 'tests/src/hashmap.rs', lines 1:0-229:9 *)
 unfold
 let hashMap_contains_key_in_list_loop_decreases (#t : Type0) (key : usize)
   (ls : aList_t t) : nat =
   admit ()
 
 (** [hashmap::{hashmap::HashMap<T>}::get_in_list]: decreases clause
-    Source: 'tests/src/hashmap.rs', lines 235:4-248:5 *)
+    Source: 'tests/src/hashmap.rs', lines 236:8-248:5 *)
 unfold
 let hashMap_get_in_list_loop_decreases (#t : Type0) (key : usize)
   (ls : aList_t t) : nat =
   admit ()
 
 (** [hashmap::{hashmap::HashMap<T>}::get_mut_in_list]: decreases clause
-    Source: 'tests/src/hashmap.rs', lines 256:4-265:5 *)
+    Source: 'tests/src/hashmap.rs', lines 257:8-265:5 *)
 unfold
 let hashMap_get_mut_in_list_loop_decreases (#t : Type0) (ls : aList_t t)
   (key : usize) : nat =
   admit ()
 
 (** [hashmap::{hashmap::HashMap<T>}::remove_from_list]: decreases clause
-    Source: 'tests/src/hashmap.rs', lines 276:4-302:5 *)
+    Source: 'tests/src/hashmap.rs', lines 1:0-299:17 *)
 unfold
 let hashMap_remove_from_list_loop_decreases (#t : Type0) (key : usize)
   (ls : aList_t t) : nat =
diff --git a/tests/fstar/hashmap/Hashmap.Funs.fst b/tests/fstar/hashmap/Hashmap.Funs.fst
index 0e48f645..a61beed6 100644
--- a/tests/fstar/hashmap/Hashmap.Funs.fst
+++ b/tests/fstar/hashmap/Hashmap.Funs.fst
@@ -14,7 +14,7 @@ let hash_key (k : usize) : result usize =
   Ok k
 
 (** [hashmap::{hashmap::HashMap<T>}::allocate_slots]: loop 0:
-    Source: 'tests/src/hashmap.rs', lines 63:4-69:5 *)
+    Source: 'tests/src/hashmap.rs', lines 64:8-67:9 *)
 let rec hashMap_allocate_slots_loop
   (#t : Type0) (slots : alloc_vec_Vec (aList_t t)) (n : usize) :
   Tot (result (alloc_vec_Vec (aList_t t)))
@@ -61,7 +61,7 @@ let hashMap_new (t : Type0) : result (hashMap_t t) =
   hashMap_new_with_capacity t 32 4 5
 
 (** [hashmap::{hashmap::HashMap<T>}::clear]: loop 0:
-    Source: 'tests/src/hashmap.rs', lines 97:8-102:5 *)
+    Source: 'tests/src/hashmap.rs', lines 98:8-101:9 *)
 let rec hashMap_clear_loop
   (#t : Type0) (slots : alloc_vec_Vec (aList_t t)) (i : usize) :
   Tot (result (alloc_vec_Vec (aList_t t)))
@@ -90,7 +90,7 @@ let hashMap_len (#t : Type0) (self : hashMap_t t) : result usize =
   Ok self.num_entries
 
 (** [hashmap::{hashmap::HashMap<T>}::insert_in_list]: loop 0:
-    Source: 'tests/src/hashmap.rs', lines 111:4-128:5 *)
+    Source: 'tests/src/hashmap.rs', lines 1:0-127:9 *)
 let rec hashMap_insert_in_list_loop
   (#t : Type0) (key : usize) (value : t) (ls : aList_t t) :
   Tot (result (bool & (aList_t t)))
@@ -135,7 +135,7 @@ let hashMap_insert_no_resize
   else let* v = index_mut_back a1 in Ok { self with slots = v }
 
 (** [hashmap::{hashmap::HashMap<T>}::move_elements_from_list]: loop 0:
-    Source: 'tests/src/hashmap.rs', lines 194:4-207:5 *)
+    Source: 'tests/src/hashmap.rs', lines 197:12-204:17 *)
 let rec hashMap_move_elements_from_list_loop
   (#t : Type0) (ntable : hashMap_t t) (ls : aList_t t) :
   Tot (result (hashMap_t t))
@@ -155,7 +155,7 @@ let hashMap_move_elements_from_list
   hashMap_move_elements_from_list_loop ntable ls
 
 (** [hashmap::{hashmap::HashMap<T>}::move_elements]: loop 0:
-    Source: 'tests/src/hashmap.rs', lines 182:8-191:5 *)
+    Source: 'tests/src/hashmap.rs', lines 183:8-190:9 *)
 let rec hashMap_move_elements_loop
   (#t : Type0) (ntable : hashMap_t t) (slots : alloc_vec_Vec (aList_t t))
   (i : usize) :
@@ -223,7 +223,7 @@ let hashMap_insert
   else Ok self1
 
 (** [hashmap::{hashmap::HashMap<T>}::contains_key_in_list]: loop 0:
-    Source: 'tests/src/hashmap.rs', lines 217:4-230:5 *)
+    Source: 'tests/src/hashmap.rs', lines 1:0-229:9 *)
 let rec hashMap_contains_key_in_list_loop
   (#t : Type0) (key : usize) (ls : aList_t t) :
   Tot (result bool)
@@ -254,7 +254,7 @@ let hashMap_contains_key
   hashMap_contains_key_in_list key a
 
 (** [hashmap::{hashmap::HashMap<T>}::get_in_list]: loop 0:
-    Source: 'tests/src/hashmap.rs', lines 235:4-248:5 *)
+    Source: 'tests/src/hashmap.rs', lines 236:8-248:5 *)
 let rec hashMap_get_in_list_loop
   (#t : Type0) (key : usize) (ls : aList_t t) :
   Tot (result t) (decreases (hashMap_get_in_list_loop_decreases key ls))
@@ -283,7 +283,7 @@ let hashMap_get (#t : Type0) (self : hashMap_t t) (key : usize) : result t =
   hashMap_get_in_list key a
 
 (** [hashmap::{hashmap::HashMap<T>}::get_mut_in_list]: loop 0:
-    Source: 'tests/src/hashmap.rs', lines 256:4-265:5 *)
+    Source: 'tests/src/hashmap.rs', lines 257:8-265:5 *)
 let rec hashMap_get_mut_in_list_loop
   (#t : Type0) (ls : aList_t t) (key : usize) :
   Tot (result (t & (t -> result (aList_t t))))
@@ -330,7 +330,7 @@ let hashMap_get_mut
   Ok (x, back)
 
 (** [hashmap::{hashmap::HashMap<T>}::remove_from_list]: loop 0:
-    Source: 'tests/src/hashmap.rs', lines 276:4-302:5 *)
+    Source: 'tests/src/hashmap.rs', lines 1:0-299:17 *)
 let rec hashMap_remove_from_list_loop
   (#t : Type0) (key : usize) (ls : aList_t t) :
   Tot (result ((option t) & (aList_t t)))
diff --git a/tests/fstar/misc/InfiniteLoop.fst b/tests/fstar/misc/InfiniteLoop.fst
index 64995eae..52353fd9 100644
--- a/tests/fstar/misc/InfiniteLoop.fst
+++ b/tests/fstar/misc/InfiniteLoop.fst
@@ -11,7 +11,7 @@ let bar : result unit =
   Ok ()
 
 (** [infinite_loop::foo]: loop 0:
-    Source: 'tests/src/infinite-loop.rs', lines 6:0-10:1 *)
+    Source: 'tests/src/infinite-loop.rs', lines 8:8-8:13 *)
 let rec foo_loop (n : nat) : result unit =
   if is_zero n
   then Fail OutOfFuel
diff --git a/tests/fstar/misc/Loops.Clauses.Template.fst b/tests/fstar/misc/Loops.Clauses.Template.fst
index b6ed56ff..40e7d87f 100644
--- a/tests/fstar/misc/Loops.Clauses.Template.fst
+++ b/tests/fstar/misc/Loops.Clauses.Template.fst
@@ -7,144 +7,144 @@ open Loops.Types
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
 (** [loops::sum]: decreases clause
-    Source: 'tests/src/loops.rs', lines 10:4-18:1 *)
+    Source: 'tests/src/loops.rs', lines 11:4-14:5 *)
 unfold let sum_loop_decreases (max : u32) (i : u32) (s : u32) : nat = admit ()
 
 (** [loops::sum_with_mut_borrows]: decreases clause
-    Source: 'tests/src/loops.rs', lines 25:4-35:1 *)
+    Source: 'tests/src/loops.rs', lines 26:4-31:5 *)
 unfold
 let sum_with_mut_borrows_loop_decreases (max : u32) (i : u32) (s : u32) : nat =
   admit ()
 
 (** [loops::sum_with_shared_borrows]: decreases clause
-    Source: 'tests/src/loops.rs', lines 40:4-52:1 *)
+    Source: 'tests/src/loops.rs', lines 41:4-48:5 *)
 unfold
 let sum_with_shared_borrows_loop_decreases (max : u32) (i : u32) (s : u32) :
   nat =
   admit ()
 
 (** [loops::sum_array]: decreases clause
-    Source: 'tests/src/loops.rs', lines 56:4-62:1 *)
+    Source: 'tests/src/loops.rs', lines 57:4-60:5 *)
 unfold
 let sum_array_loop_decreases (#n : usize) (a : array u32 n) (i : usize)
   (s : u32) : nat =
   admit ()
 
 (** [loops::clear]: decreases clause
-    Source: 'tests/src/loops.rs', lines 67:4-72:1 *)
+    Source: 'tests/src/loops.rs', lines 68:4-71:5 *)
 unfold
 let clear_loop_decreases (v : alloc_vec_Vec u32) (i : usize) : nat = admit ()
 
 (** [loops::list_mem]: decreases clause
-    Source: 'tests/src/loops.rs', lines 80:0-89:1 *)
+    Source: 'tests/src/loops.rs', lines 81:4-89:1 *)
 unfold let list_mem_loop_decreases (x : u32) (ls : list_t u32) : nat = admit ()
 
 (** [loops::list_nth_mut_loop]: decreases clause
-    Source: 'tests/src/loops.rs', lines 92:0-102:1 *)
+    Source: 'tests/src/loops.rs', lines 93:4-102:1 *)
 unfold
 let list_nth_mut_loop_loop_decreases (#t : Type0) (ls : list_t t) (i : u32) :
   nat =
   admit ()
 
 (** [loops::list_nth_shared_loop]: decreases clause
-    Source: 'tests/src/loops.rs', lines 105:0-115:1 *)
+    Source: 'tests/src/loops.rs', lines 106:4-115:1 *)
 unfold
 let list_nth_shared_loop_loop_decreases (#t : Type0) (ls : list_t t) 
   (i : u32) : nat =
   admit ()
 
 (** [loops::get_elem_mut]: decreases clause
-    Source: 'tests/src/loops.rs', lines 117:0-131:1 *)
+    Source: 'tests/src/loops.rs', lines 119:4-131:1 *)
 unfold
 let get_elem_mut_loop_decreases (x : usize) (ls : list_t usize) : nat =
   admit ()
 
 (** [loops::get_elem_shared]: decreases clause
-    Source: 'tests/src/loops.rs', lines 133:0-147:1 *)
+    Source: 'tests/src/loops.rs', lines 135:4-147:1 *)
 unfold
 let get_elem_shared_loop_decreases (x : usize) (ls : list_t usize) : nat =
   admit ()
 
 (** [loops::list_nth_mut_loop_with_id]: decreases clause
-    Source: 'tests/src/loops.rs', lines 158:0-169:1 *)
+    Source: 'tests/src/loops.rs', lines 160:4-169:1 *)
 unfold
 let list_nth_mut_loop_with_id_loop_decreases (#t : Type0) (i : u32)
   (ls : list_t t) : nat =
   admit ()
 
 (** [loops::list_nth_shared_loop_with_id]: decreases clause
-    Source: 'tests/src/loops.rs', lines 172:0-183:1 *)
+    Source: 'tests/src/loops.rs', lines 174:4-183:1 *)
 unfold
 let list_nth_shared_loop_with_id_loop_decreases (#t : Type0) (i : u32)
   (ls : list_t t) : nat =
   admit ()
 
 (** [loops::list_nth_mut_loop_pair]: decreases clause
-    Source: 'tests/src/loops.rs', lines 188:0-209:1 *)
+    Source: 'tests/src/loops.rs', lines 194:8-194:24 *)
 unfold
 let list_nth_mut_loop_pair_loop_decreases (#t : Type0) (ls0 : list_t t)
   (ls1 : list_t t) (i : u32) : nat =
   admit ()
 
 (** [loops::list_nth_shared_loop_pair]: decreases clause
-    Source: 'tests/src/loops.rs', lines 212:0-233:1 *)
+    Source: 'tests/src/loops.rs', lines 218:8-218:24 *)
 unfold
 let list_nth_shared_loop_pair_loop_decreases (#t : Type0) (ls0 : list_t t)
   (ls1 : list_t t) (i : u32) : nat =
   admit ()
 
 (** [loops::list_nth_mut_loop_pair_merge]: decreases clause
-    Source: 'tests/src/loops.rs', lines 237:0-252:1 *)
+    Source: 'tests/src/loops.rs', lines 242:4-252:1 *)
 unfold
 let list_nth_mut_loop_pair_merge_loop_decreases (#t : Type0) (ls0 : list_t t)
   (ls1 : list_t t) (i : u32) : nat =
   admit ()
 
 (** [loops::list_nth_shared_loop_pair_merge]: decreases clause
-    Source: 'tests/src/loops.rs', lines 255:0-270:1 *)
+    Source: 'tests/src/loops.rs', lines 260:4-270:1 *)
 unfold
 let list_nth_shared_loop_pair_merge_loop_decreases (#t : Type0)
   (ls0 : list_t t) (ls1 : list_t t) (i : u32) : nat =
   admit ()
 
 (** [loops::list_nth_mut_shared_loop_pair]: decreases clause
-    Source: 'tests/src/loops.rs', lines 273:0-288:1 *)
+    Source: 'tests/src/loops.rs', lines 278:4-288:1 *)
 unfold
 let list_nth_mut_shared_loop_pair_loop_decreases (#t : Type0) (ls0 : list_t t)
   (ls1 : list_t t) (i : u32) : nat =
   admit ()
 
 (** [loops::list_nth_mut_shared_loop_pair_merge]: decreases clause
-    Source: 'tests/src/loops.rs', lines 292:0-307:1 *)
+    Source: 'tests/src/loops.rs', lines 297:4-307:1 *)
 unfold
 let list_nth_mut_shared_loop_pair_merge_loop_decreases (#t : Type0)
   (ls0 : list_t t) (ls1 : list_t t) (i : u32) : nat =
   admit ()
 
 (** [loops::list_nth_shared_mut_loop_pair]: decreases clause
-    Source: 'tests/src/loops.rs', lines 311:0-326:1 *)
+    Source: 'tests/src/loops.rs', lines 316:4-326:1 *)
 unfold
 let list_nth_shared_mut_loop_pair_loop_decreases (#t : Type0) (ls0 : list_t t)
   (ls1 : list_t t) (i : u32) : nat =
   admit ()
 
 (** [loops::list_nth_shared_mut_loop_pair_merge]: decreases clause
-    Source: 'tests/src/loops.rs', lines 330:0-345:1 *)
+    Source: 'tests/src/loops.rs', lines 335:4-345:1 *)
 unfold
 let list_nth_shared_mut_loop_pair_merge_loop_decreases (#t : Type0)
   (ls0 : list_t t) (ls1 : list_t t) (i : u32) : nat =
   admit ()
 
 (** [loops::ignore_input_mut_borrow]: decreases clause
-    Source: 'tests/src/loops.rs', lines 349:0-353:1 *)
+    Source: 'tests/src/loops.rs', lines 350:4-352:5 *)
 unfold let ignore_input_mut_borrow_loop_decreases (i : u32) : nat = admit ()
 
 (** [loops::incr_ignore_input_mut_borrow]: decreases clause
-    Source: 'tests/src/loops.rs', lines 357:0-362:1 *)
+    Source: 'tests/src/loops.rs', lines 359:4-361:5 *)
 unfold
 let incr_ignore_input_mut_borrow_loop_decreases (i : u32) : nat = admit ()
 
 (** [loops::ignore_input_shared_borrow]: decreases clause
-    Source: 'tests/src/loops.rs', lines 366:0-370:1 *)
+    Source: 'tests/src/loops.rs', lines 367:4-369:5 *)
 unfold let ignore_input_shared_borrow_loop_decreases (i : u32) : nat = admit ()
 
diff --git a/tests/fstar/misc/Loops.Funs.fst b/tests/fstar/misc/Loops.Funs.fst
index 98f70914..0ebaa1b8 100644
--- a/tests/fstar/misc/Loops.Funs.fst
+++ b/tests/fstar/misc/Loops.Funs.fst
@@ -8,7 +8,7 @@ include Loops.Clauses
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
 (** [loops::sum]: loop 0:
-    Source: 'tests/src/loops.rs', lines 10:4-18:1 *)
+    Source: 'tests/src/loops.rs', lines 11:4-14:5 *)
 let rec sum_loop
   (max : u32) (i : u32) (s : u32) :
   Tot (result u32) (decreases (sum_loop_decreases max i s))
@@ -23,7 +23,7 @@ let sum (max : u32) : result u32 =
   sum_loop max 0 0
 
 (** [loops::sum_with_mut_borrows]: loop 0:
-    Source: 'tests/src/loops.rs', lines 25:4-35:1 *)
+    Source: 'tests/src/loops.rs', lines 26:4-31:5 *)
 let rec sum_with_mut_borrows_loop
   (max : u32) (i : u32) (s : u32) :
   Tot (result u32) (decreases (sum_with_mut_borrows_loop_decreases max i s))
@@ -41,7 +41,7 @@ let sum_with_mut_borrows (max : u32) : result u32 =
   sum_with_mut_borrows_loop max 0 0
 
 (** [loops::sum_with_shared_borrows]: loop 0:
-    Source: 'tests/src/loops.rs', lines 40:4-52:1 *)
+    Source: 'tests/src/loops.rs', lines 41:4-48:5 *)
 let rec sum_with_shared_borrows_loop
   (max : u32) (i : u32) (s : u32) :
   Tot (result u32) (decreases (sum_with_shared_borrows_loop_decreases max i s))
@@ -59,7 +59,7 @@ let sum_with_shared_borrows (max : u32) : result u32 =
   sum_with_shared_borrows_loop max 0 0
 
 (** [loops::sum_array]: loop 0:
-    Source: 'tests/src/loops.rs', lines 56:4-62:1 *)
+    Source: 'tests/src/loops.rs', lines 57:4-60:5 *)
 let rec sum_array_loop
   (#n : usize) (a : array u32 n) (i : usize) (s : u32) :
   Tot (result u32) (decreases (sum_array_loop_decreases a i s))
@@ -78,7 +78,7 @@ let sum_array (#n : usize) (a : array u32 n) : result u32 =
   sum_array_loop a 0 0
 
 (** [loops::clear]: loop 0:
-    Source: 'tests/src/loops.rs', lines 67:4-72:1 *)
+    Source: 'tests/src/loops.rs', lines 68:4-71:5 *)
 let rec clear_loop
   (v : alloc_vec_Vec u32) (i : usize) :
   Tot (result (alloc_vec_Vec u32)) (decreases (clear_loop_decreases v i))
@@ -100,7 +100,7 @@ let clear (v : alloc_vec_Vec u32) : result (alloc_vec_Vec u32) =
   clear_loop v 0
 
 (** [loops::list_mem]: loop 0:
-    Source: 'tests/src/loops.rs', lines 80:0-89:1 *)
+    Source: 'tests/src/loops.rs', lines 81:4-89:1 *)
 let rec list_mem_loop
   (x : u32) (ls : list_t u32) :
   Tot (result bool) (decreases (list_mem_loop_decreases x ls))
@@ -116,7 +116,7 @@ let list_mem (x : u32) (ls : list_t u32) : result bool =
   list_mem_loop x ls
 
 (** [loops::list_nth_mut_loop]: loop 0:
-    Source: 'tests/src/loops.rs', lines 92:0-102:1 *)
+    Source: 'tests/src/loops.rs', lines 93:4-102:1 *)
 let rec list_nth_mut_loop_loop
   (#t : Type0) (ls : list_t t) (i : u32) :
   Tot (result (t & (t -> result (list_t t))))
@@ -143,7 +143,7 @@ let list_nth_mut_loop
   list_nth_mut_loop_loop ls i
 
 (** [loops::list_nth_shared_loop]: loop 0:
-    Source: 'tests/src/loops.rs', lines 105:0-115:1 *)
+    Source: 'tests/src/loops.rs', lines 106:4-115:1 *)
 let rec list_nth_shared_loop_loop
   (#t : Type0) (ls : list_t t) (i : u32) :
   Tot (result t) (decreases (list_nth_shared_loop_loop_decreases ls i))
@@ -162,7 +162,7 @@ let list_nth_shared_loop (#t : Type0) (ls : list_t t) (i : u32) : result t =
   list_nth_shared_loop_loop ls i
 
 (** [loops::get_elem_mut]: loop 0:
-    Source: 'tests/src/loops.rs', lines 117:0-131:1 *)
+    Source: 'tests/src/loops.rs', lines 119:4-131:1 *)
 let rec get_elem_mut_loop
   (x : usize) (ls : list_t usize) :
   Tot (result (usize & (usize -> result (list_t usize))))
@@ -193,7 +193,7 @@ let get_elem_mut
   Ok (i, back1)
 
 (** [loops::get_elem_shared]: loop 0:
-    Source: 'tests/src/loops.rs', lines 133:0-147:1 *)
+    Source: 'tests/src/loops.rs', lines 135:4-147:1 *)
 let rec get_elem_shared_loop
   (x : usize) (ls : list_t usize) :
   Tot (result usize) (decreases (get_elem_shared_loop_decreases x ls))
@@ -226,7 +226,7 @@ let id_shared (#t : Type0) (ls : list_t t) : result (list_t t) =
   Ok ls
 
 (** [loops::list_nth_mut_loop_with_id]: loop 0:
-    Source: 'tests/src/loops.rs', lines 158:0-169:1 *)
+    Source: 'tests/src/loops.rs', lines 160:4-169:1 *)
 let rec list_nth_mut_loop_with_id_loop
   (#t : Type0) (i : u32) (ls : list_t t) :
   Tot (result (t & (t -> result (list_t t))))
@@ -256,7 +256,7 @@ let list_nth_mut_loop_with_id
   Ok (x, back1)
 
 (** [loops::list_nth_shared_loop_with_id]: loop 0:
-    Source: 'tests/src/loops.rs', lines 172:0-183:1 *)
+    Source: 'tests/src/loops.rs', lines 174:4-183:1 *)
 let rec list_nth_shared_loop_with_id_loop
   (#t : Type0) (i : u32) (ls : list_t t) :
   Tot (result t) (decreases (list_nth_shared_loop_with_id_loop_decreases i ls))
@@ -276,7 +276,7 @@ let list_nth_shared_loop_with_id
   let* ls1 = id_shared ls in list_nth_shared_loop_with_id_loop i ls1
 
 (** [loops::list_nth_mut_loop_pair]: loop 0:
-    Source: 'tests/src/loops.rs', lines 188:0-209:1 *)
+    Source: 'tests/src/loops.rs', lines 194:8-194:24 *)
 let rec list_nth_mut_loop_pair_loop
   (#t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
   Tot (result ((t & t) & (t -> result (list_t t)) & (t -> result (list_t t))))
@@ -313,7 +313,7 @@ let list_nth_mut_loop_pair
   list_nth_mut_loop_pair_loop ls0 ls1 i
 
 (** [loops::list_nth_shared_loop_pair]: loop 0:
-    Source: 'tests/src/loops.rs', lines 212:0-233:1 *)
+    Source: 'tests/src/loops.rs', lines 218:8-218:24 *)
 let rec list_nth_shared_loop_pair_loop
   (#t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
   Tot (result (t & t))
@@ -338,7 +338,7 @@ let list_nth_shared_loop_pair
   list_nth_shared_loop_pair_loop ls0 ls1 i
 
 (** [loops::list_nth_mut_loop_pair_merge]: loop 0:
-    Source: 'tests/src/loops.rs', lines 237:0-252:1 *)
+    Source: 'tests/src/loops.rs', lines 242:4-252:1 *)
 let rec list_nth_mut_loop_pair_merge_loop
   (#t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
   Tot (result ((t & t) & ((t & t) -> result ((list_t t) & (list_t t)))))
@@ -376,7 +376,7 @@ let list_nth_mut_loop_pair_merge
   list_nth_mut_loop_pair_merge_loop ls0 ls1 i
 
 (** [loops::list_nth_shared_loop_pair_merge]: loop 0:
-    Source: 'tests/src/loops.rs', lines 255:0-270:1 *)
+    Source: 'tests/src/loops.rs', lines 260:4-270:1 *)
 let rec list_nth_shared_loop_pair_merge_loop
   (#t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
   Tot (result (t & t))
@@ -403,7 +403,7 @@ let list_nth_shared_loop_pair_merge
   list_nth_shared_loop_pair_merge_loop ls0 ls1 i
 
 (** [loops::list_nth_mut_shared_loop_pair]: loop 0:
-    Source: 'tests/src/loops.rs', lines 273:0-288:1 *)
+    Source: 'tests/src/loops.rs', lines 278:4-288:1 *)
 let rec list_nth_mut_shared_loop_pair_loop
   (#t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
   Tot (result ((t & t) & (t -> result (list_t t))))
@@ -435,7 +435,7 @@ let list_nth_mut_shared_loop_pair
   list_nth_mut_shared_loop_pair_loop ls0 ls1 i
 
 (** [loops::list_nth_mut_shared_loop_pair_merge]: loop 0:
-    Source: 'tests/src/loops.rs', lines 292:0-307:1 *)
+    Source: 'tests/src/loops.rs', lines 297:4-307:1 *)
 let rec list_nth_mut_shared_loop_pair_merge_loop
   (#t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
   Tot (result ((t & t) & (t -> result (list_t t))))
@@ -467,7 +467,7 @@ let list_nth_mut_shared_loop_pair_merge
   list_nth_mut_shared_loop_pair_merge_loop ls0 ls1 i
 
 (** [loops::list_nth_shared_mut_loop_pair]: loop 0:
-    Source: 'tests/src/loops.rs', lines 311:0-326:1 *)
+    Source: 'tests/src/loops.rs', lines 316:4-326:1 *)
 let rec list_nth_shared_mut_loop_pair_loop
   (#t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
   Tot (result ((t & t) & (t -> result (list_t t))))
@@ -499,7 +499,7 @@ let list_nth_shared_mut_loop_pair
   list_nth_shared_mut_loop_pair_loop ls0 ls1 i
 
 (** [loops::list_nth_shared_mut_loop_pair_merge]: loop 0:
-    Source: 'tests/src/loops.rs', lines 330:0-345:1 *)
+    Source: 'tests/src/loops.rs', lines 335:4-345:1 *)
 let rec list_nth_shared_mut_loop_pair_merge_loop
   (#t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
   Tot (result ((t & t) & (t -> result (list_t t))))
@@ -531,7 +531,7 @@ let list_nth_shared_mut_loop_pair_merge
   list_nth_shared_mut_loop_pair_merge_loop ls0 ls1 i
 
 (** [loops::ignore_input_mut_borrow]: loop 0:
-    Source: 'tests/src/loops.rs', lines 349:0-353:1 *)
+    Source: 'tests/src/loops.rs', lines 350:4-352:5 *)
 let rec ignore_input_mut_borrow_loop
   (i : u32) :
   Tot (result unit) (decreases (ignore_input_mut_borrow_loop_decreases i))
@@ -546,7 +546,7 @@ let ignore_input_mut_borrow (_a : u32) (i : u32) : result u32 =
   let* _ = ignore_input_mut_borrow_loop i in Ok _a
 
 (** [loops::incr_ignore_input_mut_borrow]: loop 0:
-    Source: 'tests/src/loops.rs', lines 357:0-362:1 *)
+    Source: 'tests/src/loops.rs', lines 359:4-361:5 *)
 let rec incr_ignore_input_mut_borrow_loop
   (i : u32) :
   Tot (result unit) (decreases (incr_ignore_input_mut_borrow_loop_decreases i))
@@ -563,7 +563,7 @@ let incr_ignore_input_mut_borrow (a : u32) (i : u32) : result u32 =
   Ok a1
 
 (** [loops::ignore_input_shared_borrow]: loop 0:
-    Source: 'tests/src/loops.rs', lines 366:0-370:1 *)
+    Source: 'tests/src/loops.rs', lines 367:4-369:5 *)
 let rec ignore_input_shared_borrow_loop
   (i : u32) :
   Tot (result unit) (decreases (ignore_input_shared_borrow_loop_decreases i))
diff --git a/tests/fstar/rename_attribute/RenameAttribute.Clauses.Template.fst b/tests/fstar/rename_attribute/RenameAttribute.Clauses.Template.fst
index 66288585..76004f29 100644
--- a/tests/fstar/rename_attribute/RenameAttribute.Clauses.Template.fst
+++ b/tests/fstar/rename_attribute/RenameAttribute.Clauses.Template.fst
@@ -11,7 +11,7 @@ open RenameAttribute.Types
 unfold let factfn_decreases (n : u64) : nat = admit ()
 
 (** [rename_attribute::sum]: decreases clause
-    Source: 'tests/src/rename_attribute.rs', lines 67:4-75:1 *)
+    Source: 'tests/src/rename_attribute.rs', lines 68:4-71:5 *)
 unfold
 let no_borrows_sum_loop_decreases (max : u32) (i : u32) (s : u32) : nat =
   admit ()
diff --git a/tests/fstar/rename_attribute/RenameAttribute.Funs.fst b/tests/fstar/rename_attribute/RenameAttribute.Funs.fst
index ed5b0179..1b9b63cc 100644
--- a/tests/fstar/rename_attribute/RenameAttribute.Funs.fst
+++ b/tests/fstar/rename_attribute/RenameAttribute.Funs.fst
@@ -48,7 +48,7 @@ let rec factfn (n : u64) : Tot (result u64) (decreases (factfn_decreases n)) =
   else let* i = u64_sub n 1 in let* i1 = factfn i in u64_mul n i1
 
 (** [rename_attribute::sum]: loop 0:
-    Source: 'tests/src/rename_attribute.rs', lines 67:4-75:1 *)
+    Source: 'tests/src/rename_attribute.rs', lines 68:4-71:5 *)
 let rec no_borrows_sum_loop
   (max : u32) (i : u32) (s : u32) :
   Tot (result u32) (decreases (no_borrows_sum_loop_decreases max i s))
diff --git a/tests/lean/Arrays.lean b/tests/lean/Arrays.lean
index ebadb007..de4c0221 100644
--- a/tests/lean/Arrays.lean
+++ b/tests/lean/Arrays.lean
@@ -341,7 +341,7 @@ def non_copyable_array : Result Unit :=
   take_array_t (Array.make 2#usize [ AB.A, AB.B ])
 
 /- [arrays::sum]: loop 0:
-   Source: 'tests/src/arrays.rs', lines 247:4-253:1 -/
+   Source: 'tests/src/arrays.rs', lines 248:4-251:5 -/
 divergent def sum_loop (s : Slice U32) (sum1 : U32) (i : Usize) : Result U32 :=
   let i1 := Slice.len s
   if i < i1
@@ -359,7 +359,7 @@ def sum (s : Slice U32) : Result U32 :=
   sum_loop s 0#u32 0#usize
 
 /- [arrays::sum2]: loop 0:
-   Source: 'tests/src/arrays.rs', lines 258:4-264:1 -/
+   Source: 'tests/src/arrays.rs', lines 259:4-262:5 -/
 divergent def sum2_loop
   (s : Slice U32) (s2 : Slice U32) (sum1 : U32) (i : Usize) : Result U32 :=
   let i1 := Slice.len s
@@ -451,7 +451,7 @@ def ite : Result Unit :=
   Result.ok ()
 
 /- [arrays::zero_slice]: loop 0:
-   Source: 'tests/src/arrays.rs', lines 308:4-313:1 -/
+   Source: 'tests/src/arrays.rs', lines 309:4-312:5 -/
 divergent def zero_slice_loop
   (a : Slice U8) (i : Usize) (len : Usize) : Result (Slice U8) :=
   if i < len
@@ -470,7 +470,7 @@ def zero_slice (a : Slice U8) : Result (Slice U8) :=
   zero_slice_loop a 0#usize len
 
 /- [arrays::iter_mut_slice]: loop 0:
-   Source: 'tests/src/arrays.rs', lines 317:4-321:1 -/
+   Source: 'tests/src/arrays.rs', lines 318:4-320:5 -/
 divergent def iter_mut_slice_loop (len : Usize) (i : Usize) : Result Unit :=
   if i < len
   then do
@@ -487,7 +487,7 @@ def iter_mut_slice (a : Slice U8) : Result (Slice U8) :=
   Result.ok a
 
 /- [arrays::sum_mut_slice]: loop 0:
-   Source: 'tests/src/arrays.rs', lines 325:4-331:1 -/
+   Source: 'tests/src/arrays.rs', lines 326:4-329:5 -/
 divergent def sum_mut_slice_loop
   (a : Slice U32) (i : Usize) (s : U32) : Result U32 :=
   let i1 := Slice.len a
diff --git a/tests/lean/Avl/Funs.lean b/tests/lean/Avl/Funs.lean
index e4ef353f..a82baa03 100644
--- a/tests/lean/Avl/Funs.lean
+++ b/tests/lean/Avl/Funs.lean
@@ -205,7 +205,7 @@ def Tree.new {T : Type} (OrdInst : Ord T) : Result (Tree T) :=
   Result.ok { root := none }
 
 /- [avl::{avl::Tree<T>}#3::find]: loop 0:
-   Source: 'src/avl.rs', lines 342:4-354:5 -/
+   Source: 'src/avl.rs', lines 345:8-354:5 -/
 divergent def Tree.find_loop
   {T : Type} (OrdInst : Ord T) (value : T) (current_tree : Option (Node T)) :
   Result Bool
diff --git a/tests/lean/Betree/Funs.lean b/tests/lean/Betree/Funs.lean
index 18c7bfd1..2b77ccc3 100644
--- a/tests/lean/Betree/Funs.lean
+++ b/tests/lean/Betree/Funs.lean
@@ -83,7 +83,7 @@ def betree.upsert_update
       else Result.ok 0#u64
 
 /- [betree::betree::{betree::betree::List<T>}#1::len]: loop 0:
-   Source: 'src/betree.rs', lines 278:8-284:5 -/
+   Source: 'src/betree.rs', lines 279:8-282:9 -/
 divergent def betree.List.len_loop
   {T : Type} (self : betree.List T) (len : U64) : Result U64 :=
   match self with
@@ -99,7 +99,7 @@ def betree.List.len {T : Type} (self : betree.List T) : Result U64 :=
   betree.List.len_loop self 0#u64
 
 /- [betree::betree::{betree::betree::List<T>}#1::reverse]: loop 0:
-   Source: 'src/betree.rs', lines 305:8-312:5 -/
+   Source: 'src/betree.rs', lines 306:8-310:9 -/
 divergent def betree.List.reverse_loop
   {T : Type} (self : betree.List T) (out : betree.List T) :
   Result (betree.List T)
@@ -116,7 +116,7 @@ def betree.List.reverse
   betree.List.reverse_loop self betree.List.Nil
 
 /- [betree::betree::{betree::betree::List<T>}#1::split_at]: loop 0:
-   Source: 'src/betree.rs', lines 289:8-302:5 -/
+   Source: 'src/betree.rs', lines 290:8-300:9 -/
 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))
@@ -174,7 +174,7 @@ def betree.ListPairU64T.head_has_key
   | betree.List.Nil => Result.ok false
 
 /- [betree::betree::{betree::betree::List<(u64, T)>}#2::partition_at_pivot]: loop 0:
-   Source: 'src/betree.rs', lines 358:8-370:5 -/
+   Source: 'src/betree.rs', lines 359:8-368:9 -/
 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)) :
@@ -226,7 +226,7 @@ def betree.Leaf.split
   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]: loop 0:
-   Source: 'src/betree.rs', lines 792:4-810:5 -/
+   Source: 'src/betree.rs', lines 796:8-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 ×
@@ -260,7 +260,7 @@ def betree.Node.lookup_first_message_for_key
   betree.Node.lookup_first_message_for_key_loop key msgs
 
 /- [betree::betree::{betree::betree::Node}#5::apply_upserts]: loop 0:
-   Source: 'src/betree.rs', lines 820:4-844:5 -/
+   Source: 'src/betree.rs', lines 821:8-838:9 -/
 divergent def betree.Node.apply_upserts_loop
   (msgs : betree.List (U64 × betree.Message)) (prev : Option U64) (key : U64)
   :
@@ -297,7 +297,7 @@ def betree.Node.apply_upserts
   betree.Node.apply_upserts_loop msgs prev key
 
 /- [betree::betree::{betree::betree::Node}#5::lookup_in_bindings]: loop 0:
-   Source: 'src/betree.rs', lines 649:4-660:5 -/
+   Source: 'src/betree.rs', lines 650:8-660:5 -/
 divergent def betree.Node.lookup_in_bindings_loop
   (key : U64) (bindings : betree.List (U64 × U64)) : Result (Option U64) :=
   match bindings with
@@ -395,7 +395,7 @@ divergent def betree.Node.lookup
 end
 
 /- [betree::betree::{betree::betree::Node}#5::filter_messages_for_key]: loop 0:
-   Source: 'src/betree.rs', lines 683:4-692:5 -/
+   Source: 'src/betree.rs', lines 684:8-691:9 -/
 divergent def betree.Node.filter_messages_for_key_loop
   (key : U64) (msgs : betree.List (U64 × betree.Message)) :
   Result (betree.List (U64 × betree.Message))
@@ -421,7 +421,7 @@ def betree.Node.filter_messages_for_key
   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 -/
+   Source: 'src/betree.rs', lines 698:8-704:9 -/
 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 ×
@@ -511,7 +511,7 @@ def betree.Node.apply_to_internal
     lookup_first_message_for_key_back msgs2
 
 /- [betree::betree::{betree::betree::Node}#5::apply_messages_to_internal]: loop 0:
-   Source: 'src/betree.rs', lines 518:4-526:5 -/
+   Source: 'src/betree.rs', lines 522:8-525:9 -/
 divergent def betree.Node.apply_messages_to_internal_loop
   (msgs : betree.List (U64 × betree.Message))
   (new_msgs : betree.List (U64 × betree.Message)) :
@@ -536,7 +536,7 @@ def betree.Node.apply_messages_to_internal
   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 -/
+   Source: 'src/betree.rs', lines 668:8-675:9 -/
 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
@@ -609,7 +609,7 @@ def betree.Node.apply_to_leaf
       lookup_mut_in_bindings_back bindings2
 
 /- [betree::betree::{betree::betree::Node}#5::apply_messages_to_leaf]: loop 0:
-   Source: 'src/betree.rs', lines 463:4-471:5 -/
+   Source: 'src/betree.rs', lines 467:8-470:9 -/
 divergent def betree.Node.apply_messages_to_leaf_loop
   (bindings : betree.List (U64 × U64))
   (new_msgs : betree.List (U64 × betree.Message)) :
diff --git a/tests/lean/Demo/Demo.lean b/tests/lean/Demo/Demo.lean
index 9452a100..b3469008 100644
--- a/tests/lean/Demo/Demo.lean
+++ b/tests/lean/Demo/Demo.lean
@@ -67,7 +67,7 @@ divergent def list_nth {T : Type} (l : CList T) (i : U32) : Result T :=
   | CList.CNil => Result.fail .panic
 
 /- [demo::list_nth1]: loop 0:
-   Source: 'tests/src/demo.rs', lines 56:0-65:1 -/
+   Source: 'tests/src/demo.rs', lines 57:4-65:1 -/
 divergent def list_nth1_loop {T : Type} (l : CList T) (i : U32) : Result T :=
   match l with
   | CList.CCons x tl =>
diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean
index 3b883bb6..d601f420 100644
--- a/tests/lean/Hashmap/Funs.lean
+++ b/tests/lean/Hashmap/Funs.lean
@@ -16,7 +16,7 @@ def hash_key (k : Usize) : Result Usize :=
   Result.ok k
 
 /- [hashmap::{hashmap::HashMap<T>}::allocate_slots]: loop 0:
-   Source: 'tests/src/hashmap.rs', lines 63:4-69:5 -/
+   Source: 'tests/src/hashmap.rs', lines 64:8-67:9 -/
 divergent def HashMap.allocate_slots_loop
   {T : Type} (slots : alloc.vec.Vec (AList T)) (n : Usize) :
   Result (alloc.vec.Vec (AList T))
@@ -64,7 +64,7 @@ def HashMap.new (T : Type) : Result (HashMap T) :=
   HashMap.new_with_capacity T 32#usize 4#usize 5#usize
 
 /- [hashmap::{hashmap::HashMap<T>}::clear]: loop 0:
-   Source: 'tests/src/hashmap.rs', lines 97:8-102:5 -/
+   Source: 'tests/src/hashmap.rs', lines 98:8-101:9 -/
 divergent def HashMap.clear_loop
   {T : Type} (slots : alloc.vec.Vec (AList T)) (i : Usize) :
   Result (alloc.vec.Vec (AList T))
@@ -94,7 +94,7 @@ def HashMap.len {T : Type} (self : HashMap T) : Result Usize :=
   Result.ok self.num_entries
 
 /- [hashmap::{hashmap::HashMap<T>}::insert_in_list]: loop 0:
-   Source: 'tests/src/hashmap.rs', lines 111:4-128:5 -/
+   Source: 'tests/src/hashmap.rs', lines 1:0-127:9 -/
 divergent def HashMap.insert_in_list_loop
   {T : Type} (key : Usize) (value : T) (ls : AList T) :
   Result (Bool × (AList T))
@@ -143,7 +143,7 @@ def HashMap.insert_no_resize
        Result.ok { self with slots := v }
 
 /- [hashmap::{hashmap::HashMap<T>}::move_elements_from_list]: loop 0:
-   Source: 'tests/src/hashmap.rs', lines 194:4-207:5 -/
+   Source: 'tests/src/hashmap.rs', lines 197:12-204:17 -/
 divergent def HashMap.move_elements_from_list_loop
   {T : Type} (ntable : HashMap T) (ls : AList T) : Result (HashMap T) :=
   match ls with
@@ -161,7 +161,7 @@ def HashMap.move_elements_from_list
   HashMap.move_elements_from_list_loop ntable ls
 
 /- [hashmap::{hashmap::HashMap<T>}::move_elements]: loop 0:
-   Source: 'tests/src/hashmap.rs', lines 182:8-191:5 -/
+   Source: 'tests/src/hashmap.rs', lines 183:8-190:9 -/
 divergent def HashMap.move_elements_loop
   {T : Type} (ntable : HashMap T) (slots : alloc.vec.Vec (AList T)) (i : Usize)
   :
@@ -231,7 +231,7 @@ def HashMap.insert
   else Result.ok self1
 
 /- [hashmap::{hashmap::HashMap<T>}::contains_key_in_list]: loop 0:
-   Source: 'tests/src/hashmap.rs', lines 217:4-230:5 -/
+   Source: 'tests/src/hashmap.rs', lines 1:0-229:9 -/
 divergent def HashMap.contains_key_in_list_loop
   {T : Type} (key : Usize) (ls : AList T) : Result Bool :=
   match ls with
@@ -262,7 +262,7 @@ def HashMap.contains_key
   HashMap.contains_key_in_list key a
 
 /- [hashmap::{hashmap::HashMap<T>}::get_in_list]: loop 0:
-   Source: 'tests/src/hashmap.rs', lines 235:4-248:5 -/
+   Source: 'tests/src/hashmap.rs', lines 236:8-248:5 -/
 divergent def HashMap.get_in_list_loop
   {T : Type} (key : Usize) (ls : AList T) : Result T :=
   match ls with
@@ -291,7 +291,7 @@ def HashMap.get {T : Type} (self : HashMap T) (key : Usize) : Result T :=
   HashMap.get_in_list key a
 
 /- [hashmap::{hashmap::HashMap<T>}::get_mut_in_list]: loop 0:
-   Source: 'tests/src/hashmap.rs', lines 256:4-265:5 -/
+   Source: 'tests/src/hashmap.rs', lines 257:8-265:5 -/
 divergent def HashMap.get_mut_in_list_loop
   {T : Type} (ls : AList T) (key : Usize) :
   Result (T × (T → Result (AList T)))
@@ -345,7 +345,7 @@ def HashMap.get_mut
   Result.ok (t, back)
 
 /- [hashmap::{hashmap::HashMap<T>}::remove_from_list]: loop 0:
-   Source: 'tests/src/hashmap.rs', lines 276:4-302:5 -/
+   Source: 'tests/src/hashmap.rs', lines 1:0-299:17 -/
 divergent def HashMap.remove_from_list_loop
   {T : Type} (key : Usize) (ls : AList T) : Result ((Option T) × (AList T)) :=
   match ls with
diff --git a/tests/lean/InfiniteLoop.lean b/tests/lean/InfiniteLoop.lean
index 7056d5ca..3e981580 100644
--- a/tests/lean/InfiniteLoop.lean
+++ b/tests/lean/InfiniteLoop.lean
@@ -14,7 +14,7 @@ def bar : Result Unit :=
   Result.ok ()
 
 /- [infinite_loop::foo]: loop 0:
-   Source: 'tests/src/infinite-loop.rs', lines 6:0-10:1 -/
+   Source: 'tests/src/infinite-loop.rs', lines 8:8-8:13 -/
 divergent def foo_loop : Result Unit :=
   do
   let _ ← bar
diff --git a/tests/lean/Loops.lean b/tests/lean/Loops.lean
index 9a462345..0ff7589c 100644
--- a/tests/lean/Loops.lean
+++ b/tests/lean/Loops.lean
@@ -9,7 +9,7 @@ set_option linter.unusedVariables false
 namespace loops
 
 /- [loops::sum]: loop 0:
-   Source: 'tests/src/loops.rs', lines 10:4-18:1 -/
+   Source: 'tests/src/loops.rs', lines 11:4-14:5 -/
 divergent def sum_loop (max : U32) (i : U32) (s : U32) : Result U32 :=
   if i < max
   then do
@@ -24,7 +24,7 @@ def sum (max : U32) : Result U32 :=
   sum_loop max 0#u32 0#u32
 
 /- [loops::sum_with_mut_borrows]: loop 0:
-   Source: 'tests/src/loops.rs', lines 25:4-35:1 -/
+   Source: 'tests/src/loops.rs', lines 26:4-31:5 -/
 divergent def sum_with_mut_borrows_loop
   (max : U32) (i : U32) (s : U32) : Result U32 :=
   if i < max
@@ -41,7 +41,7 @@ def sum_with_mut_borrows (max : U32) : Result U32 :=
   sum_with_mut_borrows_loop max 0#u32 0#u32
 
 /- [loops::sum_with_shared_borrows]: loop 0:
-   Source: 'tests/src/loops.rs', lines 40:4-52:1 -/
+   Source: 'tests/src/loops.rs', lines 41:4-48:5 -/
 divergent def sum_with_shared_borrows_loop
   (max : U32) (i : U32) (s : U32) : Result U32 :=
   if i < max
@@ -58,7 +58,7 @@ def sum_with_shared_borrows (max : U32) : Result U32 :=
   sum_with_shared_borrows_loop max 0#u32 0#u32
 
 /- [loops::sum_array]: loop 0:
-   Source: 'tests/src/loops.rs', lines 56:4-62:1 -/
+   Source: 'tests/src/loops.rs', lines 57:4-60:5 -/
 divergent def sum_array_loop
   {N : Usize} (a : Array U32 N) (i : Usize) (s : U32) : Result U32 :=
   if i < N
@@ -76,7 +76,7 @@ def sum_array {N : Usize} (a : Array U32 N) : Result U32 :=
   sum_array_loop a 0#usize 0#u32
 
 /- [loops::clear]: loop 0:
-   Source: 'tests/src/loops.rs', lines 67:4-72:1 -/
+   Source: 'tests/src/loops.rs', lines 68:4-71:5 -/
 divergent def clear_loop
   (v : alloc.vec.Vec U32) (i : Usize) : Result (alloc.vec.Vec U32) :=
   let i1 := alloc.vec.Vec.len v
@@ -103,7 +103,7 @@ inductive List (T : Type) :=
 | Nil : List T
 
 /- [loops::list_mem]: loop 0:
-   Source: 'tests/src/loops.rs', lines 80:0-89:1 -/
+   Source: 'tests/src/loops.rs', lines 81:4-89:1 -/
 divergent def list_mem_loop (x : U32) (ls : List U32) : Result Bool :=
   match ls with
   | List.Cons y tl => if y = x
@@ -118,7 +118,7 @@ def list_mem (x : U32) (ls : List U32) : Result Bool :=
   list_mem_loop x ls
 
 /- [loops::list_nth_mut_loop]: loop 0:
-   Source: 'tests/src/loops.rs', lines 92:0-102:1 -/
+   Source: 'tests/src/loops.rs', lines 93:4-102:1 -/
 divergent def list_nth_mut_loop_loop
   {T : Type} (ls : List T) (i : U32) : Result (T × (T → Result (List T))) :=
   match ls with
@@ -146,7 +146,7 @@ def list_nth_mut_loop
   list_nth_mut_loop_loop ls i
 
 /- [loops::list_nth_shared_loop]: loop 0:
-   Source: 'tests/src/loops.rs', lines 105:0-115:1 -/
+   Source: 'tests/src/loops.rs', lines 106:4-115:1 -/
 divergent def list_nth_shared_loop_loop
   {T : Type} (ls : List T) (i : U32) : Result T :=
   match ls with
@@ -165,7 +165,7 @@ def list_nth_shared_loop {T : Type} (ls : List T) (i : U32) : Result T :=
   list_nth_shared_loop_loop ls i
 
 /- [loops::get_elem_mut]: loop 0:
-   Source: 'tests/src/loops.rs', lines 117:0-131:1 -/
+   Source: 'tests/src/loops.rs', lines 119:4-131:1 -/
 divergent def get_elem_mut_loop
   (x : Usize) (ls : List Usize) :
   Result (Usize × (Usize → Result (List Usize)))
@@ -203,7 +203,7 @@ def get_elem_mut
   Result.ok (i, back1)
 
 /- [loops::get_elem_shared]: loop 0:
-   Source: 'tests/src/loops.rs', lines 133:0-147:1 -/
+   Source: 'tests/src/loops.rs', lines 135:4-147:1 -/
 divergent def get_elem_shared_loop
   (x : Usize) (ls : List Usize) : Result Usize :=
   match ls with
@@ -236,7 +236,7 @@ def id_shared {T : Type} (ls : List T) : Result (List T) :=
   Result.ok ls
 
 /- [loops::list_nth_mut_loop_with_id]: loop 0:
-   Source: 'tests/src/loops.rs', lines 158:0-169:1 -/
+   Source: 'tests/src/loops.rs', lines 160:4-169:1 -/
 divergent def list_nth_mut_loop_with_id_loop
   {T : Type} (i : U32) (ls : List T) : Result (T × (T → Result (List T))) :=
   match ls with
@@ -269,7 +269,7 @@ def list_nth_mut_loop_with_id
   Result.ok (t, back1)
 
 /- [loops::list_nth_shared_loop_with_id]: loop 0:
-   Source: 'tests/src/loops.rs', lines 172:0-183:1 -/
+   Source: 'tests/src/loops.rs', lines 174:4-183:1 -/
 divergent def list_nth_shared_loop_with_id_loop
   {T : Type} (i : U32) (ls : List T) : Result T :=
   match ls with
@@ -290,7 +290,7 @@ def list_nth_shared_loop_with_id
   list_nth_shared_loop_with_id_loop i ls1
 
 /- [loops::list_nth_mut_loop_pair]: loop 0:
-   Source: 'tests/src/loops.rs', lines 188:0-209:1 -/
+   Source: 'tests/src/loops.rs', lines 194:8-194:24 -/
 divergent def list_nth_mut_loop_pair_loop
   {T : Type} (ls0 : List T) (ls1 : List T) (i : U32) :
   Result ((T × T) × (T → Result (List T)) × (T → Result (List T)))
@@ -330,7 +330,7 @@ def list_nth_mut_loop_pair
   list_nth_mut_loop_pair_loop ls0 ls1 i
 
 /- [loops::list_nth_shared_loop_pair]: loop 0:
-   Source: 'tests/src/loops.rs', lines 212:0-233:1 -/
+   Source: 'tests/src/loops.rs', lines 218:8-218:24 -/
 divergent def list_nth_shared_loop_pair_loop
   {T : Type} (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
   match ls0 with
@@ -353,7 +353,7 @@ def list_nth_shared_loop_pair
   list_nth_shared_loop_pair_loop ls0 ls1 i
 
 /- [loops::list_nth_mut_loop_pair_merge]: loop 0:
-   Source: 'tests/src/loops.rs', lines 237:0-252:1 -/
+   Source: 'tests/src/loops.rs', lines 242:4-252:1 -/
 divergent def list_nth_mut_loop_pair_merge_loop
   {T : Type} (ls0 : List T) (ls1 : List T) (i : U32) :
   Result ((T × T) × ((T × T) → Result ((List T) × (List T))))
@@ -392,7 +392,7 @@ def list_nth_mut_loop_pair_merge
   list_nth_mut_loop_pair_merge_loop ls0 ls1 i
 
 /- [loops::list_nth_shared_loop_pair_merge]: loop 0:
-   Source: 'tests/src/loops.rs', lines 255:0-270:1 -/
+   Source: 'tests/src/loops.rs', lines 260:4-270:1 -/
 divergent def list_nth_shared_loop_pair_merge_loop
   {T : Type} (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
   match ls0 with
@@ -416,7 +416,7 @@ def list_nth_shared_loop_pair_merge
   list_nth_shared_loop_pair_merge_loop ls0 ls1 i
 
 /- [loops::list_nth_mut_shared_loop_pair]: loop 0:
-   Source: 'tests/src/loops.rs', lines 273:0-288:1 -/
+   Source: 'tests/src/loops.rs', lines 278:4-288:1 -/
 divergent def list_nth_mut_shared_loop_pair_loop
   {T : Type} (ls0 : List T) (ls1 : List T) (i : U32) :
   Result ((T × T) × (T → Result (List T)))
@@ -451,7 +451,7 @@ def list_nth_mut_shared_loop_pair
   list_nth_mut_shared_loop_pair_loop ls0 ls1 i
 
 /- [loops::list_nth_mut_shared_loop_pair_merge]: loop 0:
-   Source: 'tests/src/loops.rs', lines 292:0-307:1 -/
+   Source: 'tests/src/loops.rs', lines 297:4-307:1 -/
 divergent def list_nth_mut_shared_loop_pair_merge_loop
   {T : Type} (ls0 : List T) (ls1 : List T) (i : U32) :
   Result ((T × T) × (T → Result (List T)))
@@ -486,7 +486,7 @@ def list_nth_mut_shared_loop_pair_merge
   list_nth_mut_shared_loop_pair_merge_loop ls0 ls1 i
 
 /- [loops::list_nth_shared_mut_loop_pair]: loop 0:
-   Source: 'tests/src/loops.rs', lines 311:0-326:1 -/
+   Source: 'tests/src/loops.rs', lines 316:4-326:1 -/
 divergent def list_nth_shared_mut_loop_pair_loop
   {T : Type} (ls0 : List T) (ls1 : List T) (i : U32) :
   Result ((T × T) × (T → Result (List T)))
@@ -521,7 +521,7 @@ def list_nth_shared_mut_loop_pair
   list_nth_shared_mut_loop_pair_loop ls0 ls1 i
 
 /- [loops::list_nth_shared_mut_loop_pair_merge]: loop 0:
-   Source: 'tests/src/loops.rs', lines 330:0-345:1 -/
+   Source: 'tests/src/loops.rs', lines 335:4-345:1 -/
 divergent def list_nth_shared_mut_loop_pair_merge_loop
   {T : Type} (ls0 : List T) (ls1 : List T) (i : U32) :
   Result ((T × T) × (T → Result (List T)))
@@ -556,7 +556,7 @@ def list_nth_shared_mut_loop_pair_merge
   list_nth_shared_mut_loop_pair_merge_loop ls0 ls1 i
 
 /- [loops::ignore_input_mut_borrow]: loop 0:
-   Source: 'tests/src/loops.rs', lines 349:0-353:1 -/
+   Source: 'tests/src/loops.rs', lines 350:4-352:5 -/
 divergent def ignore_input_mut_borrow_loop (i : U32) : Result Unit :=
   if i > 0#u32
   then do
@@ -572,7 +572,7 @@ def ignore_input_mut_borrow (_a : U32) (i : U32) : Result U32 :=
   Result.ok _a
 
 /- [loops::incr_ignore_input_mut_borrow]: loop 0:
-   Source: 'tests/src/loops.rs', lines 357:0-362:1 -/
+   Source: 'tests/src/loops.rs', lines 359:4-361:5 -/
 divergent def incr_ignore_input_mut_borrow_loop (i : U32) : Result Unit :=
   if i > 0#u32
   then do
@@ -589,7 +589,7 @@ def incr_ignore_input_mut_borrow (a : U32) (i : U32) : Result U32 :=
   Result.ok a1
 
 /- [loops::ignore_input_shared_borrow]: loop 0:
-   Source: 'tests/src/loops.rs', lines 366:0-370:1 -/
+   Source: 'tests/src/loops.rs', lines 367:4-369:5 -/
 divergent def ignore_input_shared_borrow_loop (i : U32) : Result Unit :=
   if i > 0#u32
   then do
diff --git a/tests/lean/MiniTree.lean b/tests/lean/MiniTree.lean
index d7a474c4..bba4af74 100644
--- a/tests/lean/MiniTree.lean
+++ b/tests/lean/MiniTree.lean
@@ -26,7 +26,7 @@ structure Tree where
   root : Option Node
 
 /- [mini_tree::{mini_tree::Tree}::explore]: loop 0:
-   Source: 'tests/src/mini_tree.rs', lines 15:8-20:5 -/
+   Source: 'tests/src/mini_tree.rs', lines 17:8-19:9 -/
 divergent def Tree.explore_loop (current_tree : Option Node) : Result Unit :=
   match current_tree with
   | none => Result.ok ()
diff --git a/tests/lean/RenameAttribute.lean b/tests/lean/RenameAttribute.lean
index 6a192f63..ff7b746a 100644
--- a/tests/lean/RenameAttribute.lean
+++ b/tests/lean/RenameAttribute.lean
@@ -75,7 +75,7 @@ divergent def Factfn (n : U64) : Result U64 :=
        n * i1
 
 /- [rename_attribute::sum]: loop 0:
-   Source: 'tests/src/rename_attribute.rs', lines 67:4-75:1 -/
+   Source: 'tests/src/rename_attribute.rs', lines 68:4-71:5 -/
 divergent def No_borrows_sum_loop
   (max : U32) (i : U32) (s : U32) : Result U32 :=
   if i < max
diff --git a/tests/lean/Tutorial/Tutorial.lean b/tests/lean/Tutorial/Tutorial.lean
index d1338e08..b16c5754 100644
--- a/tests/lean/Tutorial/Tutorial.lean
+++ b/tests/lean/Tutorial/Tutorial.lean
@@ -91,7 +91,7 @@ divergent def list_nth_mut
   | CList.CNil => Result.fail .panic
 
 /- [tutorial::list_nth1]: loop 0:
-   Source: 'src/lib.rs', lines 65:0-74:1 -/
+   Source: 'src/lib.rs', lines 66:4-74:1 -/
 divergent def list_nth1_loop {T : Type} (l : CList T) (i : U32) : Result T :=
   match l with
   | CList.CCons x tl =>
@@ -164,7 +164,7 @@ def use_counter
   CounterInst.incr cnt
 
 /- [tutorial::list_nth_mut1]: loop 0:
-   Source: 'src/lib.rs', lines 123:0-132:1 -/
+   Source: 'src/lib.rs', lines 124:4-132:1 -/
 divergent def list_nth_mut1_loop
   {T : Type} (l : CList T) (i : U32) :
   Result (T × (T → Result (CList T)))
@@ -196,7 +196,7 @@ def list_nth_mut1
   list_nth_mut1_loop l i
 
 /- [tutorial::list_tail]: loop 0:
-   Source: 'src/lib.rs', lines 134:0-139:1 -/
+   Source: 'src/lib.rs', lines 135:4-137:5 -/
 divergent def list_tail_loop
   {T : Type} (l : CList T) :
   Result ((CList T) × (CList T → Result (CList T)))
@@ -230,7 +230,7 @@ def append_in_place
   list_tail_back l1
 
 /- [tutorial::reverse]: loop 0:
-   Source: 'src/lib.rs', lines 147:4-154:1 -/
+   Source: 'src/lib.rs', lines 148:4-152:5 -/
 divergent def reverse_loop
   {T : Type} (l : CList T) (out : CList T) : Result (CList T) :=
   match l with
@@ -243,7 +243,7 @@ def reverse {T : Type} (l : CList T) : Result (CList T) :=
   reverse_loop l CList.CNil
 
 /- [tutorial::zero]: loop 0:
-   Source: 'src/lib.rs', lines 163:4-168:1 -/
+   Source: 'src/lib.rs', lines 164:4-167:5 -/
 divergent def zero_loop
   (x : alloc.vec.Vec U32) (i : Usize) : Result (alloc.vec.Vec U32) :=
   let i1 := alloc.vec.Vec.len x
@@ -264,7 +264,7 @@ def zero (x : alloc.vec.Vec U32) : Result (alloc.vec.Vec U32) :=
   zero_loop x 0#usize
 
 /- [tutorial::add_no_overflow]: loop 0:
-   Source: 'src/lib.rs', lines 176:4-181:1 -/
+   Source: 'src/lib.rs', lines 177:4-180:5 -/
 divergent def add_no_overflow_loop
   (x : alloc.vec.Vec U32) (y : alloc.vec.Vec U32) (i : Usize) :
   Result (alloc.vec.Vec U32)
@@ -293,7 +293,7 @@ def add_no_overflow
   add_no_overflow_loop x y 0#usize
 
 /- [tutorial::add_with_carry]: loop 0:
-   Source: 'src/lib.rs', lines 188:4-199:1 -/
+   Source: 'src/lib.rs', lines 190:4-197:5 -/
 divergent def add_with_carry_loop
   (x : alloc.vec.Vec U32) (y : alloc.vec.Vec U32) (c0 : U8) (i : Usize) :
   Result (U8 × (alloc.vec.Vec U32))
@@ -346,7 +346,7 @@ def get_or_zero (y : alloc.vec.Vec U32) (i : Usize) : Result U32 :=
   else Result.ok 0#u32
 
 /- [tutorial::add]: loop 0:
-   Source: 'src/lib.rs', lines 219:4-235:1 -/
+   Source: 'src/lib.rs', lines 221:4-229:5 -/
 divergent def add_loop
   (x : alloc.vec.Vec U32) (y : alloc.vec.Vec U32) (max1 : Usize) (c0 : U8)
   (i : Usize) :
diff --git a/tests/src/borrow-check-negative.borrow-check.out b/tests/src/borrow-check-negative.borrow-check.out
index 03d41b1d..ed135506 100644
--- a/tests/src/borrow-check-negative.borrow-check.out
+++ b/tests/src/borrow-check-negative.borrow-check.out
@@ -1,15 +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
+Source: 'tests/src/borrow-check-negative.rs', lines 23:12-23:14
 [Error] Can't end abstraction 8 as it is set as non-endable
 Source: 'tests/src/borrow-check-negative.rs', lines 26:0-32:1
 [Error] Can not apply a projection to the ⊥ value
-Source: 'tests/src/borrow-check-negative.rs', lines 37:4-41:1
+Source: 'tests/src/borrow-check-negative.rs', lines 40:4-40:11
 [Error] Can not apply a projection to the ⊥ value
-Source: 'tests/src/borrow-check-negative.rs', lines 47:4-50:1
+Source: 'tests/src/borrow-check-negative.rs', lines 49:12-49:14
 [Error] Can not apply a projection to the ⊥ value
-Source: 'tests/src/borrow-check-negative.rs', lines 60:4-64:1
+Source: 'tests/src/borrow-check-negative.rs', lines 63:12-63:17
 [Error] Can not apply a projection to the ⊥ value
-Source: 'tests/src/borrow-check-negative.rs', lines 71:4-79:1
+Source: 'tests/src/borrow-check-negative.rs', lines 78:12-78:17
 [Error] Can not apply a projection to the ⊥ value
-Source: 'tests/src/borrow-check-negative.rs', lines 87:4-90:1
+Source: 'tests/src/borrow-check-negative.rs', lines 89:12-89:15
diff --git a/tests/src/loops-borrow-check-fail.borrow-check.out b/tests/src/loops-borrow-check-fail.borrow-check.out
index 34eb75f8..28d9e563 100644
--- a/tests/src/loops-borrow-check-fail.borrow-check.out
+++ b/tests/src/loops-borrow-check-fail.borrow-check.out
@@ -1,5 +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
+Source: 'tests/src/loops-borrow-check-fail.rs', lines 8:10-8:13
 [Error] Can not apply a projection to the ⊥ value
-Source: 'tests/src/loops-borrow-check-fail.rs', lines 17:4-21:1
+Source: 'tests/src/loops-borrow-check-fail.rs', lines 19:12-19:17