Improve the heuristic to find pretty names for the variables in the loops

9 files changed, 387 insertions, 377 deletions

diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v
index 5ec021d1..1cbff379 100644
--- a/tests/coq/hashmap/Hashmap_Funs.v
+++ b/tests/coq/hashmap/Hashmap_Funs.v
@@ -13,7 +13,7 @@ Definition hash_key_fwd (k : usize) : result usize := Return k.
 
 (** [hashmap::HashMap::{0}::allocate_slots] *)
 Fixpoint hash_map_allocate_slots_loop_fwd
-  (T : Type) (n : nat) (v : vec (List_t T)) (n0 : usize) :
+  (T : Type) (n : nat) (slots : vec (List_t T)) (n0 : usize) :
   result (vec (List_t T))
   :=
   match n with
@@ -21,10 +21,10 @@ Fixpoint hash_map_allocate_slots_loop_fwd
   | S n1 =>
     if n0 s> 0%usize
     then (
-      slots <- vec_push_back (List_t T) v ListNil;
+      slots0 <- vec_push_back (List_t T) slots ListNil;
       n2 <- usize_sub n0 1%usize;
-      hash_map_allocate_slots_loop_fwd T n1 slots n2)
-    else Return v
+      hash_map_allocate_slots_loop_fwd T n1 slots0 n2)
+    else Return slots
   end
 .
 
@@ -57,19 +57,19 @@ Definition hash_map_new_fwd (T : Type) (n : nat) : result (Hash_map_t T) :=
 
 (** [hashmap::HashMap::{0}::clear_slots] *)
 Fixpoint hash_map_clear_slots_loop_fwd_back
-  (T : Type) (n : nat) (v : vec (List_t T)) (i : usize) :
+  (T : Type) (n : nat) (slots : vec (List_t T)) (i : usize) :
   result (vec (List_t T))
   :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
-    let i0 := vec_len (List_t T) v in
+    let i0 := vec_len (List_t T) slots in
     if i s< i0
     then (
       i1 <- usize_add i 1%usize;
-      slots <- vec_index_mut_back (List_t T) v i ListNil;
-      hash_map_clear_slots_loop_fwd_back T n0 slots i1)
-    else Return v
+      slots0 <- vec_index_mut_back (List_t T) slots i ListNil;
+      hash_map_clear_slots_loop_fwd_back T n0 slots0 i1)
+    else Return slots
   end
 .
 
@@ -176,7 +176,7 @@ Definition core_num_u32_max_c : u32 := core_num_u32_max_body%global.
 
 (** [hashmap::HashMap::{0}::move_elements_from_list] *)
 Fixpoint hash_map_move_elements_from_list_loop_fwd_back
-  (T : Type) (n : nat) (hm : Hash_map_t T) (ls : List_t T) :
+  (T : Type) (n : nat) (ntable : Hash_map_t T) (ls : List_t T) :
   result (Hash_map_t T)
   :=
   match n with
@@ -184,9 +184,9 @@ Fixpoint hash_map_move_elements_from_list_loop_fwd_back
   | S n0 =>
     match ls with
     | ListCons k v tl =>
-      ntable <- hash_map_insert_no_resize_fwd_back T n0 hm k v;
-      hash_map_move_elements_from_list_loop_fwd_back T n0 ntable tl
-    | ListNil => Return hm
+      ntable0 <- hash_map_insert_no_resize_fwd_back T n0 ntable k v;
+      hash_map_move_elements_from_list_loop_fwd_back T n0 ntable0 tl
+    | ListNil => Return ntable
     end
   end
 .
@@ -201,23 +201,24 @@ Definition hash_map_move_elements_from_list_fwd_back
 
 (** [hashmap::HashMap::{0}::move_elements] *)
 Fixpoint hash_map_move_elements_loop_fwd_back
-  (T : Type) (n : nat) (hm : Hash_map_t T) (v : vec (List_t T)) (i : usize) :
+  (T : Type) (n : nat) (ntable : Hash_map_t T) (slots : vec (List_t T))
+  (i : usize) :
   result ((Hash_map_t T) * (vec (List_t T)))
   :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
-    let i0 := vec_len (List_t T) v in
+    let i0 := vec_len (List_t T) slots in
     if i s< i0
     then (
-      l <- vec_index_mut_fwd (List_t T) v i;
+      l <- vec_index_mut_fwd (List_t T) slots i;
       let ls := mem_replace_fwd (List_t T) l ListNil in
-      ntable <- hash_map_move_elements_from_list_fwd_back T n0 hm ls;
+      ntable0 <- hash_map_move_elements_from_list_fwd_back T n0 ntable ls;
       i1 <- usize_add i 1%usize;
       let l0 := mem_replace_back (List_t T) l ListNil in
-      slots <- vec_index_mut_back (List_t T) v i l0;
-      hash_map_move_elements_loop_fwd_back T n0 ntable slots i1)
-    else Return (hm, v)
+      slots0 <- vec_index_mut_back (List_t T) slots i l0;
+      hash_map_move_elements_loop_fwd_back T n0 ntable0 slots0 i1)
+    else Return (ntable, slots)
   end
 .
 
@@ -267,15 +268,15 @@ Definition hash_map_insert_fwd_back
 
 (** [hashmap::HashMap::{0}::contains_key_in_list] *)
 Fixpoint hash_map_contains_key_in_list_loop_fwd
-  (T : Type) (n : nat) (i : usize) (ls : List_t T) : result bool :=
+  (T : Type) (n : nat) (key : usize) (ls : List_t T) : result bool :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
     match ls with
     | ListCons ckey t tl =>
-      if ckey s= i
+      if ckey s= key
       then Return true
-      else hash_map_contains_key_in_list_loop_fwd T n0 i tl
+      else hash_map_contains_key_in_list_loop_fwd T n0 key tl
     | ListNil => Return false
     end
   end
@@ -299,15 +300,15 @@ Definition hash_map_contains_key_fwd
 
 (** [hashmap::HashMap::{0}::get_in_list] *)
 Fixpoint hash_map_get_in_list_loop_fwd
-  (T : Type) (n : nat) (i : usize) (ls : List_t T) : result T :=
+  (T : Type) (n : nat) (key : usize) (ls : List_t T) : result T :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
     match ls with
     | ListCons ckey cvalue tl =>
-      if ckey s= i
+      if ckey s= key
       then Return cvalue
-      else hash_map_get_in_list_loop_fwd T n0 i tl
+      else hash_map_get_in_list_loop_fwd T n0 key tl
     | ListNil => Fail_ Failure
     end
   end
@@ -331,15 +332,15 @@ Definition hash_map_get_fwd
 
 (** [hashmap::HashMap::{0}::get_mut_in_list] *)
 Fixpoint hash_map_get_mut_in_list_loop_fwd
-  (T : Type) (n : nat) (i : usize) (ls : List_t T) : result T :=
+  (T : Type) (n : nat) (key : usize) (ls : List_t T) : result T :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
     match ls with
     | ListCons ckey cvalue tl =>
-      if ckey s= i
+      if ckey s= key
       then Return cvalue
-      else hash_map_get_mut_in_list_loop_fwd T n0 i tl
+      else hash_map_get_mut_in_list_loop_fwd T n0 key tl
     | ListNil => Fail_ Failure
     end
   end
@@ -353,7 +354,7 @@ Definition hash_map_get_mut_in_list_fwd
 
 (** [hashmap::HashMap::{0}::get_mut_in_list] *)
 Fixpoint hash_map_get_mut_in_list_loop_back
-  (T : Type) (n : nat) (i : usize) (ls : List_t T) (ret : T) :
+  (T : Type) (n : nat) (key : usize) (ls : List_t T) (ret : T) :
   result (List_t T)
   :=
   match n with
@@ -361,10 +362,10 @@ Fixpoint hash_map_get_mut_in_list_loop_back
   | S n0 =>
     match ls with
     | ListCons ckey cvalue tl =>
-      if ckey s= i
+      if ckey s= key
       then Return (ListCons ckey ret tl)
       else (
-        l <- hash_map_get_mut_in_list_loop_back T n0 i tl ret;
+        l <- hash_map_get_mut_in_list_loop_back T n0 key tl ret;
         Return (ListCons ckey cvalue l))
     | ListNil => Fail_ Failure
     end
@@ -406,20 +407,20 @@ Definition hash_map_get_mut_back
 
 (** [hashmap::HashMap::{0}::remove_from_list] *)
 Fixpoint hash_map_remove_from_list_loop_fwd
-  (T : Type) (n : nat) (i : usize) (ls : List_t T) : result (option T) :=
+  (T : Type) (n : nat) (key : usize) (ls : List_t T) : result (option T) :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
     match ls with
     | ListCons ckey t tl =>
-      if ckey s= i
+      if ckey s= key
       then
         let mv_ls := mem_replace_fwd (List_t T) (ListCons ckey t tl) ListNil in
         match mv_ls with
-        | ListCons i0 cvalue tl0 => Return (Some cvalue)
+        | ListCons i cvalue tl0 => Return (Some cvalue)
         | ListNil => Fail_ Failure
         end
-      else hash_map_remove_from_list_loop_fwd T n0 i tl
+      else hash_map_remove_from_list_loop_fwd T n0 key tl
     | ListNil => Return None
     end
   end
@@ -433,21 +434,21 @@ Definition hash_map_remove_from_list_fwd
 
 (** [hashmap::HashMap::{0}::remove_from_list] *)
 Fixpoint hash_map_remove_from_list_loop_back
-  (T : Type) (n : nat) (i : usize) (ls : List_t T) : result (List_t T) :=
+  (T : Type) (n : nat) (key : usize) (ls : List_t T) : result (List_t T) :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
     match ls with
     | ListCons ckey t tl =>
-      if ckey s= i
+      if ckey s= key
       then
         let mv_ls := mem_replace_fwd (List_t T) (ListCons ckey t tl) ListNil in
         match mv_ls with
-        | ListCons i0 cvalue tl0 => Return tl0
+        | ListCons i cvalue tl0 => Return tl0
         | ListNil => Fail_ Failure
         end
       else (
-        l <- hash_map_remove_from_list_loop_back T n0 i tl;
+        l <- hash_map_remove_from_list_loop_back T n0 key tl;
         Return (ListCons ckey t l))
     | ListNil => Return ListNil
     end
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
index 9ae7942c..2a8ab5b5 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
+++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
@@ -15,7 +15,7 @@ Definition hashmap_hash_key_fwd (k : usize) : result usize := Return k.
 
 (** [hashmap_main::hashmap::HashMap::{0}::allocate_slots] *)
 Fixpoint hashmap_hash_map_allocate_slots_loop_fwd
-  (T : Type) (n : nat) (v : vec (Hashmap_list_t T)) (n0 : usize) :
+  (T : Type) (n : nat) (slots : vec (Hashmap_list_t T)) (n0 : usize) :
   result (vec (Hashmap_list_t T))
   :=
   match n with
@@ -23,10 +23,10 @@ Fixpoint hashmap_hash_map_allocate_slots_loop_fwd
   | S n1 =>
     if n0 s> 0%usize
     then (
-      slots <- vec_push_back (Hashmap_list_t T) v HashmapListNil;
+      slots0 <- vec_push_back (Hashmap_list_t T) slots HashmapListNil;
       n2 <- usize_sub n0 1%usize;
-      hashmap_hash_map_allocate_slots_loop_fwd T n1 slots n2)
-    else Return v
+      hashmap_hash_map_allocate_slots_loop_fwd T n1 slots0 n2)
+    else Return slots
   end
 .
 
@@ -60,19 +60,19 @@ Definition hashmap_hash_map_new_fwd
 
 (** [hashmap_main::hashmap::HashMap::{0}::clear_slots] *)
 Fixpoint hashmap_hash_map_clear_slots_loop_fwd_back
-  (T : Type) (n : nat) (v : vec (Hashmap_list_t T)) (i : usize) :
+  (T : Type) (n : nat) (slots : vec (Hashmap_list_t T)) (i : usize) :
   result (vec (Hashmap_list_t T))
   :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
-    let i0 := vec_len (Hashmap_list_t T) v in
+    let i0 := vec_len (Hashmap_list_t T) slots in
     if i s< i0
     then (
       i1 <- usize_add i 1%usize;
-      slots <- vec_index_mut_back (Hashmap_list_t T) v i HashmapListNil;
-      hashmap_hash_map_clear_slots_loop_fwd_back T n0 slots i1)
-    else Return v
+      slots0 <- vec_index_mut_back (Hashmap_list_t T) slots i HashmapListNil;
+      hashmap_hash_map_clear_slots_loop_fwd_back T n0 slots0 i1)
+    else Return slots
   end
 .
 
@@ -192,7 +192,8 @@ Definition core_num_u32_max_c : u32 := core_num_u32_max_body%global.
 
 (** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] *)
 Fixpoint hashmap_hash_map_move_elements_from_list_loop_fwd_back
-  (T : Type) (n : nat) (hm : Hashmap_hash_map_t T) (ls : Hashmap_list_t T) :
+  (T : Type) (n : nat) (ntable : Hashmap_hash_map_t T) (ls : Hashmap_list_t T)
+  :
   result (Hashmap_hash_map_t T)
   :=
   match n with
@@ -200,9 +201,9 @@ Fixpoint hashmap_hash_map_move_elements_from_list_loop_fwd_back
   | S n0 =>
     match ls with
     | HashmapListCons k v tl =>
-      ntable <- hashmap_hash_map_insert_no_resize_fwd_back T n0 hm k v;
-      hashmap_hash_map_move_elements_from_list_loop_fwd_back T n0 ntable tl
-    | HashmapListNil => Return hm
+      ntable0 <- hashmap_hash_map_insert_no_resize_fwd_back T n0 ntable k v;
+      hashmap_hash_map_move_elements_from_list_loop_fwd_back T n0 ntable0 tl
+    | HashmapListNil => Return ntable
     end
   end
 .
@@ -218,24 +219,25 @@ Definition hashmap_hash_map_move_elements_from_list_fwd_back
 
 (** [hashmap_main::hashmap::HashMap::{0}::move_elements] *)
 Fixpoint hashmap_hash_map_move_elements_loop_fwd_back
-  (T : Type) (n : nat) (hm : Hashmap_hash_map_t T) (v : vec (Hashmap_list_t T))
-  (i : usize) :
+  (T : Type) (n : nat) (ntable : Hashmap_hash_map_t T)
+  (slots : vec (Hashmap_list_t T)) (i : usize) :
   result ((Hashmap_hash_map_t T) * (vec (Hashmap_list_t T)))
   :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
-    let i0 := vec_len (Hashmap_list_t T) v in
+    let i0 := vec_len (Hashmap_list_t T) slots in
     if i s< i0
     then (
-      l <- vec_index_mut_fwd (Hashmap_list_t T) v i;
+      l <- vec_index_mut_fwd (Hashmap_list_t T) slots i;
       let ls := mem_replace_fwd (Hashmap_list_t T) l HashmapListNil in
-      ntable <- hashmap_hash_map_move_elements_from_list_fwd_back T n0 hm ls;
+      ntable0 <-
+        hashmap_hash_map_move_elements_from_list_fwd_back T n0 ntable ls;
       i1 <- usize_add i 1%usize;
       let l0 := mem_replace_back (Hashmap_list_t T) l HashmapListNil in
-      slots <- vec_index_mut_back (Hashmap_list_t T) v i l0;
-      hashmap_hash_map_move_elements_loop_fwd_back T n0 ntable slots i1)
-    else Return (hm, v)
+      slots0 <- vec_index_mut_back (Hashmap_list_t T) slots i l0;
+      hashmap_hash_map_move_elements_loop_fwd_back T n0 ntable0 slots0 i1)
+    else Return (ntable, slots)
   end
 .
 
@@ -288,15 +290,15 @@ Definition hashmap_hash_map_insert_fwd_back
 
 (** [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] *)
 Fixpoint hashmap_hash_map_contains_key_in_list_loop_fwd
-  (T : Type) (n : nat) (i : usize) (ls : Hashmap_list_t T) : result bool :=
+  (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) : result bool :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
     match ls with
     | HashmapListCons ckey t tl =>
-      if ckey s= i
+      if ckey s= key
       then Return true
-      else hashmap_hash_map_contains_key_in_list_loop_fwd T n0 i tl
+      else hashmap_hash_map_contains_key_in_list_loop_fwd T n0 key tl
     | HashmapListNil => Return false
     end
   end
@@ -322,15 +324,15 @@ Definition hashmap_hash_map_contains_key_fwd
 
 (** [hashmap_main::hashmap::HashMap::{0}::get_in_list] *)
 Fixpoint hashmap_hash_map_get_in_list_loop_fwd
-  (T : Type) (n : nat) (i : usize) (ls : Hashmap_list_t T) : result T :=
+  (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) : result T :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
     match ls with
     | HashmapListCons ckey cvalue tl =>
-      if ckey s= i
+      if ckey s= key
       then Return cvalue
-      else hashmap_hash_map_get_in_list_loop_fwd T n0 i tl
+      else hashmap_hash_map_get_in_list_loop_fwd T n0 key tl
     | HashmapListNil => Fail_ Failure
     end
   end
@@ -356,15 +358,15 @@ Definition hashmap_hash_map_get_fwd
 
 (** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
 Fixpoint hashmap_hash_map_get_mut_in_list_loop_fwd
-  (T : Type) (n : nat) (i : usize) (ls : Hashmap_list_t T) : result T :=
+  (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) : result T :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
     match ls with
     | HashmapListCons ckey cvalue tl =>
-      if ckey s= i
+      if ckey s= key
       then Return cvalue
-      else hashmap_hash_map_get_mut_in_list_loop_fwd T n0 i tl
+      else hashmap_hash_map_get_mut_in_list_loop_fwd T n0 key tl
     | HashmapListNil => Fail_ Failure
     end
   end
@@ -378,7 +380,7 @@ Definition hashmap_hash_map_get_mut_in_list_fwd
 
 (** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
 Fixpoint hashmap_hash_map_get_mut_in_list_loop_back
-  (T : Type) (n : nat) (i : usize) (ls : Hashmap_list_t T) (ret : T) :
+  (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) (ret : T) :
   result (Hashmap_list_t T)
   :=
   match n with
@@ -386,10 +388,10 @@ Fixpoint hashmap_hash_map_get_mut_in_list_loop_back
   | S n0 =>
     match ls with
     | HashmapListCons ckey cvalue tl =>
-      if ckey s= i
+      if ckey s= key
       then Return (HashmapListCons ckey ret tl)
       else (
-        l <- hashmap_hash_map_get_mut_in_list_loop_back T n0 i tl ret;
+        l <- hashmap_hash_map_get_mut_in_list_loop_back T n0 key tl ret;
         Return (HashmapListCons ckey cvalue l))
     | HashmapListNil => Fail_ Failure
     end
@@ -437,7 +439,7 @@ Definition hashmap_hash_map_get_mut_back
 
 (** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *)
 Fixpoint hashmap_hash_map_remove_from_list_loop_fwd
-  (T : Type) (n : nat) (i : usize) (ls : Hashmap_list_t T) :
+  (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) :
   result (option T)
   :=
   match n with
@@ -445,16 +447,16 @@ Fixpoint hashmap_hash_map_remove_from_list_loop_fwd
   | S n0 =>
     match ls with
     | HashmapListCons ckey t tl =>
-      if ckey s= i
+      if ckey s= key
       then
         let mv_ls :=
           mem_replace_fwd (Hashmap_list_t T) (HashmapListCons ckey t tl)
             HashmapListNil in
         match mv_ls with
-        | HashmapListCons i0 cvalue tl0 => Return (Some cvalue)
+        | HashmapListCons i cvalue tl0 => Return (Some cvalue)
         | HashmapListNil => Fail_ Failure
         end
-      else hashmap_hash_map_remove_from_list_loop_fwd T n0 i tl
+      else hashmap_hash_map_remove_from_list_loop_fwd T n0 key tl
     | HashmapListNil => Return None
     end
   end
@@ -470,7 +472,7 @@ Definition hashmap_hash_map_remove_from_list_fwd
 
 (** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *)
 Fixpoint hashmap_hash_map_remove_from_list_loop_back
-  (T : Type) (n : nat) (i : usize) (ls : Hashmap_list_t T) :
+  (T : Type) (n : nat) (key : usize) (ls : Hashmap_list_t T) :
   result (Hashmap_list_t T)
   :=
   match n with
@@ -478,17 +480,17 @@ Fixpoint hashmap_hash_map_remove_from_list_loop_back
   | S n0 =>
     match ls with
     | HashmapListCons ckey t tl =>
-      if ckey s= i
+      if ckey s= key
       then
         let mv_ls :=
           mem_replace_fwd (Hashmap_list_t T) (HashmapListCons ckey t tl)
             HashmapListNil in
         match mv_ls with
-        | HashmapListCons i0 cvalue tl0 => Return tl0
+        | HashmapListCons i cvalue tl0 => Return tl0
         | HashmapListNil => Fail_ Failure
         end
       else (
-        l <- hashmap_hash_map_remove_from_list_loop_back T n0 i tl;
+        l <- hashmap_hash_map_remove_from_list_loop_back T n0 key tl;
         Return (HashmapListCons ckey t l))
     | HashmapListNil => Return HashmapListNil
     end
diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v
index 22c2fd19..4fbb7da0 100644
--- a/tests/coq/misc/Loops.v
+++ b/tests/coq/misc/Loops.v
@@ -94,13 +94,13 @@ Arguments ListNil {T}.
 
 (** [loops::list_mem] *)
 Fixpoint list_mem_loop_fwd
-  (n : nat) (i : u32) (ls : List_t u32) : result bool :=
+  (n : nat) (x : u32) (ls : List_t u32) : result bool :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
     match ls with
     | ListCons y tl =>
-      if y s= i then Return true else list_mem_loop_fwd n0 i tl
+      if y s= x then Return true else list_mem_loop_fwd n0 x tl
     | ListNil => Return false
     end
   end
@@ -235,16 +235,16 @@ Definition get_elem_mut_back
 
 (** [loops::get_elem_shared] *)
 Fixpoint get_elem_shared_loop_fwd
-  (n : nat) (x : usize) (v : vec (List_t usize)) (l : List_t usize)
-  (ls : List_t usize) :
+  (n : nat) (x : usize) (slots : vec (List_t usize)) (ls : List_t usize)
+  (ls0 : List_t usize) :
   result usize
   :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
-    match ls with
+    match ls0 with
     | ListCons y tl =>
-      if y s= x then Return y else get_elem_shared_loop_fwd n0 x v l tl
+      if y s= x then Return y else get_elem_shared_loop_fwd n0 x slots ls tl
     | ListNil => Fail_ Failure
     end
   end
@@ -329,17 +329,17 @@ Definition list_nth_mut_loop_with_id_back
 
 (** [loops::list_nth_shared_loop_with_id] *)
 Fixpoint list_nth_shared_loop_with_id_loop_fwd
-  (T : Type) (n : nat) (l : List_t T) (i : u32) (ls : List_t T) : result T :=
+  (T : Type) (n : nat) (ls : List_t T) (i : u32) (ls0 : List_t T) : result T :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
-    match ls with
+    match ls0 with
     | ListCons x tl =>
       if i s= 0%u32
       then Return x
       else (
         i0 <- u32_sub i 1%u32;
-        list_nth_shared_loop_with_id_loop_fwd T n0 l i0 tl)
+        list_nth_shared_loop_with_id_loop_fwd T n0 ls i0 tl)
     | ListNil => Fail_ Failure
     end
   end
@@ -353,15 +353,15 @@ Definition list_nth_shared_loop_with_id_fwd
 
 (** [loops::list_nth_mut_loop_pair] *)
 Fixpoint list_nth_mut_loop_pair_loop_fwd
-  (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) :
+  (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result (T * T)
   :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
-    match l with
+    match ls0 with
     | ListCons x0 tl0 =>
-      match l0 with
+      match ls1 with
       | ListCons x1 tl1 =>
         if i s= 0%u32
         then Return (x0, x1)
@@ -385,22 +385,22 @@ Definition list_nth_mut_loop_pair_fwd
 
 (** [loops::list_nth_mut_loop_pair] *)
 Fixpoint list_nth_mut_loop_pair_loop_back'a
-  (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) (ret : T) :
+  (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) :
   result (List_t T)
   :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
-    match l with
+    match ls0 with
     | ListCons x0 tl0 =>
-      match l0 with
+      match ls1 with
       | ListCons x1 tl1 =>
         if i s= 0%u32
         then Return (ListCons ret tl0)
         else (
           i0 <- u32_sub i 1%u32;
-          l1 <- list_nth_mut_loop_pair_loop_back'a T n0 tl0 tl1 i0 ret;
-          Return (ListCons x0 l1))
+          l <- list_nth_mut_loop_pair_loop_back'a T n0 tl0 tl1 i0 ret;
+          Return (ListCons x0 l))
       | ListNil => Fail_ Failure
       end
     | ListNil => Fail_ Failure
@@ -418,22 +418,22 @@ Definition list_nth_mut_loop_pair_back'a
 
 (** [loops::list_nth_mut_loop_pair] *)
 Fixpoint list_nth_mut_loop_pair_loop_back'b
-  (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) (ret : T) :
+  (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) :
   result (List_t T)
   :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
-    match l with
+    match ls0 with
     | ListCons x0 tl0 =>
-      match l0 with
+      match ls1 with
       | ListCons x1 tl1 =>
         if i s= 0%u32
         then Return (ListCons ret tl1)
         else (
           i0 <- u32_sub i 1%u32;
-          l1 <- list_nth_mut_loop_pair_loop_back'b T n0 tl0 tl1 i0 ret;
-          Return (ListCons x1 l1))
+          l <- list_nth_mut_loop_pair_loop_back'b T n0 tl0 tl1 i0 ret;
+          Return (ListCons x1 l))
       | ListNil => Fail_ Failure
       end
     | ListNil => Fail_ Failure
@@ -451,15 +451,15 @@ Definition list_nth_mut_loop_pair_back'b
 
 (** [loops::list_nth_shared_loop_pair] *)
 Fixpoint list_nth_shared_loop_pair_loop_fwd
-  (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) :
+  (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result (T * T)
   :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
-    match l with
+    match ls0 with
     | ListCons x0 tl0 =>
-      match l0 with
+      match ls1 with
       | ListCons x1 tl1 =>
         if i s= 0%u32
         then Return (x0, x1)
@@ -483,15 +483,15 @@ Definition list_nth_shared_loop_pair_fwd
 
 (** [loops::list_nth_mut_loop_pair_merge] *)
 Fixpoint list_nth_mut_loop_pair_merge_loop_fwd
-  (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) :
+  (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result (T * T)
   :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
-    match l with
+    match ls0 with
     | ListCons x0 tl0 =>
-      match l0 with
+      match ls1 with
       | ListCons x1 tl1 =>
         if i s= 0%u32
         then Return (x0, x1)
@@ -515,24 +515,24 @@ Definition list_nth_mut_loop_pair_merge_fwd
 
 (** [loops::list_nth_mut_loop_pair_merge] *)
 Fixpoint list_nth_mut_loop_pair_merge_loop_back
-  (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) (ret : (T * T))
-  :
+  (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32)
+  (ret : (T * T)) :
   result ((List_t T) * (List_t T))
   :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
-    match l with
+    match ls0 with
     | ListCons x0 tl0 =>
-      match l0 with
+      match ls1 with
       | ListCons x1 tl1 =>
         if i s= 0%u32
         then let (t, t0) := ret in Return (ListCons t tl0, ListCons t0 tl1)
         else (
           i0 <- u32_sub i 1%u32;
           p <- list_nth_mut_loop_pair_merge_loop_back T n0 tl0 tl1 i0 ret;
-          let (l1, l2) := p in
-          Return (ListCons x0 l1, ListCons x1 l2))
+          let (l, l0) := p in
+          Return (ListCons x0 l, ListCons x1 l0))
       | ListNil => Fail_ Failure
       end
     | ListNil => Fail_ Failure
@@ -551,15 +551,15 @@ Definition list_nth_mut_loop_pair_merge_back
 
 (** [loops::list_nth_shared_loop_pair_merge] *)
 Fixpoint list_nth_shared_loop_pair_merge_loop_fwd
-  (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) :
+  (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result (T * T)
   :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
-    match l with
+    match ls0 with
     | ListCons x0 tl0 =>
-      match l0 with
+      match ls1 with
       | ListCons x1 tl1 =>
         if i s= 0%u32
         then Return (x0, x1)
@@ -583,15 +583,15 @@ Definition list_nth_shared_loop_pair_merge_fwd
 
 (** [loops::list_nth_mut_shared_loop_pair] *)
 Fixpoint list_nth_mut_shared_loop_pair_loop_fwd
-  (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) :
+  (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result (T * T)
   :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
-    match l with
+    match ls0 with
     | ListCons x0 tl0 =>
-      match l0 with
+      match ls1 with
       | ListCons x1 tl1 =>
         if i s= 0%u32
         then Return (x0, x1)
@@ -615,22 +615,22 @@ Definition list_nth_mut_shared_loop_pair_fwd
 
 (** [loops::list_nth_mut_shared_loop_pair] *)
 Fixpoint list_nth_mut_shared_loop_pair_loop_back
-  (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) (ret : T) :
+  (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) :
   result (List_t T)
   :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
-    match l with
+    match ls0 with
     | ListCons x0 tl0 =>
-      match l0 with
+      match ls1 with
       | ListCons x1 tl1 =>
         if i s= 0%u32
         then Return (ListCons ret tl0)
         else (
           i0 <- u32_sub i 1%u32;
-          l1 <- list_nth_mut_shared_loop_pair_loop_back T n0 tl0 tl1 i0 ret;
-          Return (ListCons x0 l1))
+          l <- list_nth_mut_shared_loop_pair_loop_back T n0 tl0 tl1 i0 ret;
+          Return (ListCons x0 l))
       | ListNil => Fail_ Failure
       end
     | ListNil => Fail_ Failure
@@ -648,15 +648,15 @@ Definition list_nth_mut_shared_loop_pair_back
 
 (** [loops::list_nth_mut_shared_loop_pair_merge] *)
 Fixpoint list_nth_mut_shared_loop_pair_merge_loop_fwd
-  (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) :
+  (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result (T * T)
   :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
-    match l with
+    match ls0 with
     | ListCons x0 tl0 =>
-      match l0 with
+      match ls1 with
       | ListCons x1 tl1 =>
         if i s= 0%u32
         then Return (x0, x1)
@@ -680,23 +680,23 @@ Definition list_nth_mut_shared_loop_pair_merge_fwd
 
 (** [loops::list_nth_mut_shared_loop_pair_merge] *)
 Fixpoint list_nth_mut_shared_loop_pair_merge_loop_back
-  (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) (ret : T) :
+  (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) :
   result (List_t T)
   :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
-    match l with
+    match ls0 with
     | ListCons x0 tl0 =>
-      match l0 with
+      match ls1 with
       | ListCons x1 tl1 =>
         if i s= 0%u32
         then Return (ListCons ret tl0)
         else (
           i0 <- u32_sub i 1%u32;
-          l1 <-
+          l <-
             list_nth_mut_shared_loop_pair_merge_loop_back T n0 tl0 tl1 i0 ret;
-          Return (ListCons x0 l1))
+          Return (ListCons x0 l))
       | ListNil => Fail_ Failure
       end
     | ListNil => Fail_ Failure
@@ -714,15 +714,15 @@ Definition list_nth_mut_shared_loop_pair_merge_back
 
 (** [loops::list_nth_shared_mut_loop_pair] *)
 Fixpoint list_nth_shared_mut_loop_pair_loop_fwd
-  (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) :
+  (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result (T * T)
   :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
-    match l with
+    match ls0 with
     | ListCons x0 tl0 =>
-      match l0 with
+      match ls1 with
       | ListCons x1 tl1 =>
         if i s= 0%u32
         then Return (x0, x1)
@@ -746,22 +746,22 @@ Definition list_nth_shared_mut_loop_pair_fwd
 
 (** [loops::list_nth_shared_mut_loop_pair] *)
 Fixpoint list_nth_shared_mut_loop_pair_loop_back
-  (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) (ret : T) :
+  (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) :
   result (List_t T)
   :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
-    match l with
+    match ls0 with
     | ListCons x0 tl0 =>
-      match l0 with
+      match ls1 with
       | ListCons x1 tl1 =>
         if i s= 0%u32
         then Return (ListCons ret tl1)
         else (
           i0 <- u32_sub i 1%u32;
-          l1 <- list_nth_shared_mut_loop_pair_loop_back T n0 tl0 tl1 i0 ret;
-          Return (ListCons x1 l1))
+          l <- list_nth_shared_mut_loop_pair_loop_back T n0 tl0 tl1 i0 ret;
+          Return (ListCons x1 l))
       | ListNil => Fail_ Failure
       end
     | ListNil => Fail_ Failure
@@ -779,15 +779,15 @@ Definition list_nth_shared_mut_loop_pair_back
 
 (** [loops::list_nth_shared_mut_loop_pair_merge] *)
 Fixpoint list_nth_shared_mut_loop_pair_merge_loop_fwd
-  (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) :
+  (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
   result (T * T)
   :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
-    match l with
+    match ls0 with
     | ListCons x0 tl0 =>
-      match l0 with
+      match ls1 with
       | ListCons x1 tl1 =>
         if i s= 0%u32
         then Return (x0, x1)
@@ -811,23 +811,23 @@ Definition list_nth_shared_mut_loop_pair_merge_fwd
 
 (** [loops::list_nth_shared_mut_loop_pair_merge] *)
 Fixpoint list_nth_shared_mut_loop_pair_merge_loop_back
-  (T : Type) (n : nat) (l : List_t T) (l0 : List_t T) (i : u32) (ret : T) :
+  (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) (ret : T) :
   result (List_t T)
   :=
   match n with
   | O => Fail_ OutOfFuel
   | S n0 =>
-    match l with
+    match ls0 with
     | ListCons x0 tl0 =>
-      match l0 with
+      match ls1 with
       | ListCons x1 tl1 =>
         if i s= 0%u32
         then Return (ListCons ret tl1)
         else (
           i0 <- u32_sub i 1%u32;
-          l1 <-
+          l <-
             list_nth_shared_mut_loop_pair_merge_loop_back T n0 tl0 tl1 i0 ret;
-          Return (ListCons x1 l1))
+          Return (ListCons x1 l))
       | ListNil => Fail_ Failure
       end
     | ListNil => Fail_ Failure
diff --git a/tests/fstar/hashmap/Hashmap.Clauses.Template.fst b/tests/fstar/hashmap/Hashmap.Clauses.Template.fst
index b8890f86..3e51c6f1 100644
--- a/tests/fstar/hashmap/Hashmap.Clauses.Template.fst
+++ b/tests/fstar/hashmap/Hashmap.Clauses.Template.fst
@@ -8,14 +8,14 @@ open Hashmap.Types
 
 (** [hashmap::HashMap::{0}::allocate_slots]: decreases clause *)
 unfold
-let hash_map_allocate_slots_decreases (t : Type0) (v : vec (list_t t))
+let hash_map_allocate_slots_decreases (t : Type0) (slots : vec (list_t t))
   (n : usize) : nat =
   admit ()
 
 (** [hashmap::HashMap::{0}::clear_slots]: decreases clause *)
 unfold
-let hash_map_clear_slots_decreases (t : Type0) (v : vec (list_t t)) (i : usize)
-  : nat =
+let hash_map_clear_slots_decreases (t : Type0) (slots : vec (list_t t))
+  (i : usize) : nat =
   admit ()
 
 (** [hashmap::HashMap::{0}::insert_in_list]: decreases clause *)
@@ -30,37 +30,37 @@ let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body
 
 (** [hashmap::HashMap::{0}::move_elements_from_list]: decreases clause *)
 unfold
-let hash_map_move_elements_from_list_decreases (t : Type0) (hm : hash_map_t t)
-  (ls : list_t t) : nat =
+let hash_map_move_elements_from_list_decreases (t : Type0)
+  (ntable : hash_map_t t) (ls : list_t t) : nat =
   admit ()
 
 (** [hashmap::HashMap::{0}::move_elements]: decreases clause *)
 unfold
-let hash_map_move_elements_decreases (t : Type0) (hm : hash_map_t t)
-  (v : vec (list_t t)) (i : usize) : nat =
+let hash_map_move_elements_decreases (t : Type0) (ntable : hash_map_t t)
+  (slots : vec (list_t t)) (i : usize) : nat =
   admit ()
 
 (** [hashmap::HashMap::{0}::contains_key_in_list]: decreases clause *)
 unfold
-let hash_map_contains_key_in_list_decreases (t : Type0) (i : usize)
+let hash_map_contains_key_in_list_decreases (t : Type0) (key : usize)
   (ls : list_t t) : nat =
   admit ()
 
 (** [hashmap::HashMap::{0}::get_in_list]: decreases clause *)
 unfold
-let hash_map_get_in_list_decreases (t : Type0) (i : usize) (ls : list_t t) :
+let hash_map_get_in_list_decreases (t : Type0) (key : usize) (ls : list_t t) :
   nat =
   admit ()
 
 (** [hashmap::HashMap::{0}::get_mut_in_list]: decreases clause *)
 unfold
-let hash_map_get_mut_in_list_decreases (t : Type0) (i : usize) (ls : list_t t)
-  : nat =
+let hash_map_get_mut_in_list_decreases (t : Type0) (key : usize)
+  (ls : list_t t) : nat =
   admit ()
 
 (** [hashmap::HashMap::{0}::remove_from_list]: decreases clause *)
 unfold
-let hash_map_remove_from_list_decreases (t : Type0) (i : usize) (ls : list_t t)
-  : nat =
+let hash_map_remove_from_list_decreases (t : Type0) (key : usize)
+  (ls : list_t t) : nat =
   admit ()
 
diff --git a/tests/fstar/hashmap/Hashmap.Funs.fst b/tests/fstar/hashmap/Hashmap.Funs.fst
index d81da40b..81b253ad 100644
--- a/tests/fstar/hashmap/Hashmap.Funs.fst
+++ b/tests/fstar/hashmap/Hashmap.Funs.fst
@@ -12,21 +12,21 @@ let hash_key_fwd (k : usize) : result usize = Return k
 
 (** [hashmap::HashMap::{0}::allocate_slots] *)
 let rec hash_map_allocate_slots_loop_fwd
-  (t : Type0) (v : vec (list_t t)) (n : usize) :
+  (t : Type0) (slots : vec (list_t t)) (n : usize) :
   Tot (result (vec (list_t t)))
-  (decreases (hash_map_allocate_slots_decreases t v n))
+  (decreases (hash_map_allocate_slots_decreases t slots n))
   =
   if n > 0
   then
-    begin match vec_push_back (list_t t) v ListNil with
+    begin match vec_push_back (list_t t) slots ListNil with
     | Fail e -> Fail e
-    | Return slots ->
+    | Return slots0 ->
       begin match usize_sub n 1 with
       | Fail e -> Fail e
-      | Return n0 -> hash_map_allocate_slots_loop_fwd t slots n0
+      | Return n0 -> hash_map_allocate_slots_loop_fwd t slots0 n0
       end
     end
-  else Return v
+  else Return slots
 
 (** [hashmap::HashMap::{0}::allocate_slots] *)
 let hash_map_allocate_slots_fwd
@@ -60,22 +60,22 @@ let hash_map_new_fwd (t : Type0) : result (hash_map_t t) =
 
 (** [hashmap::HashMap::{0}::clear_slots] *)
 let rec hash_map_clear_slots_loop_fwd_back
-  (t : Type0) (v : vec (list_t t)) (i : usize) :
+  (t : Type0) (slots : vec (list_t t)) (i : usize) :
   Tot (result (vec (list_t t)))
-  (decreases (hash_map_clear_slots_decreases t v i))
+  (decreases (hash_map_clear_slots_decreases t slots i))
   =
-  let i0 = vec_len (list_t t) v in
+  let i0 = vec_len (list_t t) slots in
   if i < i0
   then
     begin match usize_add i 1 with
     | Fail e -> Fail e
     | Return i1 ->
-      begin match vec_index_mut_back (list_t t) v i ListNil with
+      begin match vec_index_mut_back (list_t t) slots i ListNil with
       | Fail e -> Fail e
-      | Return slots -> hash_map_clear_slots_loop_fwd_back t slots i1
+      | Return slots0 -> hash_map_clear_slots_loop_fwd_back t slots0 i1
       end
     end
-  else Return v
+  else Return slots
 
 (** [hashmap::HashMap::{0}::clear_slots] *)
 let hash_map_clear_slots_fwd_back
@@ -199,18 +199,18 @@ let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body
 
 (** [hashmap::HashMap::{0}::move_elements_from_list] *)
 let rec hash_map_move_elements_from_list_loop_fwd_back
-  (t : Type0) (hm : hash_map_t t) (ls : list_t t) :
+  (t : Type0) (ntable : hash_map_t t) (ls : list_t t) :
   Tot (result (hash_map_t t))
-  (decreases (hash_map_move_elements_from_list_decreases t hm ls))
+  (decreases (hash_map_move_elements_from_list_decreases t ntable ls))
   =
   begin match ls with
   | ListCons k v tl ->
-    begin match hash_map_insert_no_resize_fwd_back t hm k v with
+    begin match hash_map_insert_no_resize_fwd_back t ntable k v with
     | Fail e -> Fail e
-    | Return ntable ->
-      hash_map_move_elements_from_list_loop_fwd_back t ntable tl
+    | Return ntable0 ->
+      hash_map_move_elements_from_list_loop_fwd_back t ntable0 tl
     end
-  | ListNil -> Return hm
+  | ListNil -> Return ntable
   end
 
 (** [hashmap::HashMap::{0}::move_elements_from_list] *)
@@ -220,33 +220,33 @@ let hash_map_move_elements_from_list_fwd_back
 
 (** [hashmap::HashMap::{0}::move_elements] *)
 let rec hash_map_move_elements_loop_fwd_back
-  (t : Type0) (hm : hash_map_t t) (v : vec (list_t t)) (i : usize) :
+  (t : Type0) (ntable : hash_map_t t) (slots : vec (list_t t)) (i : usize) :
   Tot (result ((hash_map_t t) & (vec (list_t t))))
-  (decreases (hash_map_move_elements_decreases t hm v i))
+  (decreases (hash_map_move_elements_decreases t ntable slots i))
   =
-  let i0 = vec_len (list_t t) v in
+  let i0 = vec_len (list_t t) slots in
   if i < i0
   then
-    begin match vec_index_mut_fwd (list_t t) v i with
+    begin match vec_index_mut_fwd (list_t t) slots i with
     | Fail e -> Fail e
     | Return l ->
       let ls = mem_replace_fwd (list_t t) l ListNil in
-      begin match hash_map_move_elements_from_list_fwd_back t hm ls with
+      begin match hash_map_move_elements_from_list_fwd_back t ntable ls with
       | Fail e -> Fail e
-      | Return ntable ->
+      | Return ntable0 ->
         begin match usize_add i 1 with
         | Fail e -> Fail e
         | Return i1 ->
           let l0 = mem_replace_back (list_t t) l ListNil in
-          begin match vec_index_mut_back (list_t t) v i l0 with
+          begin match vec_index_mut_back (list_t t) slots i l0 with
           | Fail e -> Fail e
-          | Return slots ->
-            hash_map_move_elements_loop_fwd_back t ntable slots i1
+          | Return slots0 ->
+            hash_map_move_elements_loop_fwd_back t ntable0 slots0 i1
           end
         end
       end
     end
-  else Return (hm, v)
+  else Return (ntable, slots)
 
 (** [hashmap::HashMap::{0}::move_elements] *)
 let hash_map_move_elements_fwd_back
@@ -313,15 +313,15 @@ let hash_map_insert_fwd_back
 
 (** [hashmap::HashMap::{0}::contains_key_in_list] *)
 let rec hash_map_contains_key_in_list_loop_fwd
-  (t : Type0) (i : usize) (ls : list_t t) :
+  (t : Type0) (key : usize) (ls : list_t t) :
   Tot (result bool)
-  (decreases (hash_map_contains_key_in_list_decreases t i ls))
+  (decreases (hash_map_contains_key_in_list_decreases t key ls))
   =
   begin match ls with
   | ListCons ckey x tl ->
-    if ckey = i
+    if ckey = key
     then Return true
-    else hash_map_contains_key_in_list_loop_fwd t i tl
+    else hash_map_contains_key_in_list_loop_fwd t key tl
   | ListNil -> Return false
   end
 
@@ -349,12 +349,14 @@ let hash_map_contains_key_fwd
 
 (** [hashmap::HashMap::{0}::get_in_list] *)
 let rec hash_map_get_in_list_loop_fwd
-  (t : Type0) (i : usize) (ls : list_t t) :
-  Tot (result t) (decreases (hash_map_get_in_list_decreases t i ls))
+  (t : Type0) (key : usize) (ls : list_t t) :
+  Tot (result t) (decreases (hash_map_get_in_list_decreases t key ls))
   =
   begin match ls with
   | ListCons ckey cvalue tl ->
-    if ckey = i then Return cvalue else hash_map_get_in_list_loop_fwd t i tl
+    if ckey = key
+    then Return cvalue
+    else hash_map_get_in_list_loop_fwd t key tl
   | ListNil -> Fail Failure
   end
 
@@ -382,14 +384,14 @@ let hash_map_get_fwd
 
 (** [hashmap::HashMap::{0}::get_mut_in_list] *)
 let rec hash_map_get_mut_in_list_loop_fwd
-  (t : Type0) (i : usize) (ls : list_t t) :
-  Tot (result t) (decreases (hash_map_get_mut_in_list_decreases t i ls))
+  (t : Type0) (key : usize) (ls : list_t t) :
+  Tot (result t) (decreases (hash_map_get_mut_in_list_decreases t key ls))
   =
   begin match ls with
   | ListCons ckey cvalue tl ->
-    if ckey = i
+    if ckey = key
     then Return cvalue
-    else hash_map_get_mut_in_list_loop_fwd t i tl
+    else hash_map_get_mut_in_list_loop_fwd t key tl
   | ListNil -> Fail Failure
   end
 
@@ -400,16 +402,16 @@ let hash_map_get_mut_in_list_fwd
 
 (** [hashmap::HashMap::{0}::get_mut_in_list] *)
 let rec hash_map_get_mut_in_list_loop_back
-  (t : Type0) (i : usize) (ls : list_t t) (ret : t) :
+  (t : Type0) (key : usize) (ls : list_t t) (ret : t) :
   Tot (result (list_t t))
-  (decreases (hash_map_get_mut_in_list_decreases t i ls))
+  (decreases (hash_map_get_mut_in_list_decreases t key ls))
   =
   begin match ls with
   | ListCons ckey cvalue tl ->
-    if ckey = i
+    if ckey = key
     then Return (ListCons ckey ret tl)
     else
-      begin match hash_map_get_mut_in_list_loop_back t i tl ret with
+      begin match hash_map_get_mut_in_list_loop_back t key tl ret with
       | Fail e -> Fail e
       | Return l -> Return (ListCons ckey cvalue l)
       end
@@ -472,20 +474,20 @@ let hash_map_get_mut_back
 
 (** [hashmap::HashMap::{0}::remove_from_list] *)
 let rec hash_map_remove_from_list_loop_fwd
-  (t : Type0) (i : usize) (ls : list_t t) :
+  (t : Type0) (key : usize) (ls : list_t t) :
   Tot (result (option t))
-  (decreases (hash_map_remove_from_list_decreases t i ls))
+  (decreases (hash_map_remove_from_list_decreases t key ls))
   =
   begin match ls with
   | ListCons ckey x tl ->
-    if ckey = i
+    if ckey = key
     then
       let mv_ls = mem_replace_fwd (list_t t) (ListCons ckey x tl) ListNil in
       begin match mv_ls with
-      | ListCons i0 cvalue tl0 -> Return (Some cvalue)
+      | ListCons i cvalue tl0 -> Return (Some cvalue)
       | ListNil -> Fail Failure
       end
-    else hash_map_remove_from_list_loop_fwd t i tl
+    else hash_map_remove_from_list_loop_fwd t key tl
   | ListNil -> Return None
   end
 
@@ -496,21 +498,21 @@ let hash_map_remove_from_list_fwd
 
 (** [hashmap::HashMap::{0}::remove_from_list] *)
 let rec hash_map_remove_from_list_loop_back
-  (t : Type0) (i : usize) (ls : list_t t) :
+  (t : Type0) (key : usize) (ls : list_t t) :
   Tot (result (list_t t))
-  (decreases (hash_map_remove_from_list_decreases t i ls))
+  (decreases (hash_map_remove_from_list_decreases t key ls))
   =
   begin match ls with
   | ListCons ckey x tl ->
-    if ckey = i
+    if ckey = key
     then
       let mv_ls = mem_replace_fwd (list_t t) (ListCons ckey x tl) ListNil in
       begin match mv_ls with
-      | ListCons i0 cvalue tl0 -> Return tl0
+      | ListCons i cvalue tl0 -> Return tl0
       | ListNil -> Fail Failure
       end
     else
-      begin match hash_map_remove_from_list_loop_back t i tl with
+      begin match hash_map_remove_from_list_loop_back t key tl with
       | Fail e -> Fail e
       | Return l -> Return (ListCons ckey x l)
       end
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.Template.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.Template.fst
index b3081cd6..55685114 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.Template.fst
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.Template.fst
@@ -9,13 +9,13 @@ open HashmapMain.Types
 (** [hashmap_main::hashmap::HashMap::{0}::allocate_slots]: decreases clause *)
 unfold
 let hashmap_hash_map_allocate_slots_decreases (t : Type0)
-  (v : vec (hashmap_list_t t)) (n : usize) : nat =
+  (slots : vec (hashmap_list_t t)) (n : usize) : nat =
   admit ()
 
 (** [hashmap_main::hashmap::HashMap::{0}::clear_slots]: decreases clause *)
 unfold
 let hashmap_hash_map_clear_slots_decreases (t : Type0)
-  (v : vec (hashmap_list_t t)) (i : usize) : nat =
+  (slots : vec (hashmap_list_t t)) (i : usize) : nat =
   admit ()
 
 (** [hashmap_main::hashmap::HashMap::{0}::insert_in_list]: decreases clause *)
@@ -31,36 +31,37 @@ let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body
 (** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list]: decreases clause *)
 unfold
 let hashmap_hash_map_move_elements_from_list_decreases (t : Type0)
-  (hm : hashmap_hash_map_t t) (ls : hashmap_list_t t) : nat =
+  (ntable : hashmap_hash_map_t t) (ls : hashmap_list_t t) : nat =
   admit ()
 
 (** [hashmap_main::hashmap::HashMap::{0}::move_elements]: decreases clause *)
 unfold
 let hashmap_hash_map_move_elements_decreases (t : Type0)
-  (hm : hashmap_hash_map_t t) (v : vec (hashmap_list_t t)) (i : usize) : nat =
+  (ntable : hashmap_hash_map_t t) (slots : vec (hashmap_list_t t)) (i : usize)
+  : nat =
   admit ()
 
 (** [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list]: decreases clause *)
 unfold
-let hashmap_hash_map_contains_key_in_list_decreases (t : Type0) (i : usize)
+let hashmap_hash_map_contains_key_in_list_decreases (t : Type0) (key : usize)
   (ls : hashmap_list_t t) : nat =
   admit ()
 
 (** [hashmap_main::hashmap::HashMap::{0}::get_in_list]: decreases clause *)
 unfold
-let hashmap_hash_map_get_in_list_decreases (t : Type0) (i : usize)
+let hashmap_hash_map_get_in_list_decreases (t : Type0) (key : usize)
   (ls : hashmap_list_t t) : nat =
   admit ()
 
 (** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list]: decreases clause *)
 unfold
-let hashmap_hash_map_get_mut_in_list_decreases (t : Type0) (i : usize)
+let hashmap_hash_map_get_mut_in_list_decreases (t : Type0) (key : usize)
   (ls : hashmap_list_t t) : nat =
   admit ()
 
 (** [hashmap_main::hashmap::HashMap::{0}::remove_from_list]: decreases clause *)
 unfold
-let hashmap_hash_map_remove_from_list_decreases (t : Type0) (i : usize)
+let hashmap_hash_map_remove_from_list_decreases (t : Type0) (key : usize)
   (ls : hashmap_list_t t) : nat =
   admit ()
 
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
index 3da56f41..fdbf1404 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
@@ -13,21 +13,21 @@ let hashmap_hash_key_fwd (k : usize) : result usize = Return k
 
 (** [hashmap_main::hashmap::HashMap::{0}::allocate_slots] *)
 let rec hashmap_hash_map_allocate_slots_loop_fwd
-  (t : Type0) (v : vec (hashmap_list_t t)) (n : usize) :
+  (t : Type0) (slots : vec (hashmap_list_t t)) (n : usize) :
   Tot (result (vec (hashmap_list_t t)))
-  (decreases (hashmap_hash_map_allocate_slots_decreases t v n))
+  (decreases (hashmap_hash_map_allocate_slots_decreases t slots n))
   =
   if n > 0
   then
-    begin match vec_push_back (hashmap_list_t t) v HashmapListNil with
+    begin match vec_push_back (hashmap_list_t t) slots HashmapListNil with
     | Fail e -> Fail e
-    | Return slots ->
+    | Return slots0 ->
       begin match usize_sub n 1 with
       | Fail e -> Fail e
-      | Return n0 -> hashmap_hash_map_allocate_slots_loop_fwd t slots n0
+      | Return n0 -> hashmap_hash_map_allocate_slots_loop_fwd t slots0 n0
       end
     end
-  else Return v
+  else Return slots
 
 (** [hashmap_main::hashmap::HashMap::{0}::allocate_slots] *)
 let hashmap_hash_map_allocate_slots_fwd
@@ -64,22 +64,23 @@ let hashmap_hash_map_new_fwd (t : Type0) : result (hashmap_hash_map_t t) =
 
 (** [hashmap_main::hashmap::HashMap::{0}::clear_slots] *)
 let rec hashmap_hash_map_clear_slots_loop_fwd_back
-  (t : Type0) (v : vec (hashmap_list_t t)) (i : usize) :
+  (t : Type0) (slots : vec (hashmap_list_t t)) (i : usize) :
   Tot (result (vec (hashmap_list_t t)))
-  (decreases (hashmap_hash_map_clear_slots_decreases t v i))
+  (decreases (hashmap_hash_map_clear_slots_decreases t slots i))
   =
-  let i0 = vec_len (hashmap_list_t t) v in
+  let i0 = vec_len (hashmap_list_t t) slots in
   if i < i0
   then
     begin match usize_add i 1 with
     | Fail e -> Fail e
     | Return i1 ->
-      begin match vec_index_mut_back (hashmap_list_t t) v i HashmapListNil with
+      begin match vec_index_mut_back (hashmap_list_t t) slots i HashmapListNil
+        with
       | Fail e -> Fail e
-      | Return slots -> hashmap_hash_map_clear_slots_loop_fwd_back t slots i1
+      | Return slots0 -> hashmap_hash_map_clear_slots_loop_fwd_back t slots0 i1
       end
     end
-  else Return v
+  else Return slots
 
 (** [hashmap_main::hashmap::HashMap::{0}::clear_slots] *)
 let hashmap_hash_map_clear_slots_fwd_back
@@ -214,18 +215,18 @@ let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body
 
 (** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] *)
 let rec hashmap_hash_map_move_elements_from_list_loop_fwd_back
-  (t : Type0) (hm : hashmap_hash_map_t t) (ls : hashmap_list_t t) :
+  (t : Type0) (ntable : hashmap_hash_map_t t) (ls : hashmap_list_t t) :
   Tot (result (hashmap_hash_map_t t))
-  (decreases (hashmap_hash_map_move_elements_from_list_decreases t hm ls))
+  (decreases (hashmap_hash_map_move_elements_from_list_decreases t ntable ls))
   =
   begin match ls with
   | HashmapListCons k v tl ->
-    begin match hashmap_hash_map_insert_no_resize_fwd_back t hm k v with
+    begin match hashmap_hash_map_insert_no_resize_fwd_back t ntable k v with
     | Fail e -> Fail e
-    | Return ntable ->
-      hashmap_hash_map_move_elements_from_list_loop_fwd_back t ntable tl
+    | Return ntable0 ->
+      hashmap_hash_map_move_elements_from_list_loop_fwd_back t ntable0 tl
     end
-  | HashmapListNil -> Return hm
+  | HashmapListNil -> Return ntable
   end
 
 (** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] *)
@@ -237,35 +238,35 @@ let hashmap_hash_map_move_elements_from_list_fwd_back
 
 (** [hashmap_main::hashmap::HashMap::{0}::move_elements] *)
 let rec hashmap_hash_map_move_elements_loop_fwd_back
-  (t : Type0) (hm : hashmap_hash_map_t t) (v : vec (hashmap_list_t t))
+  (t : Type0) (ntable : hashmap_hash_map_t t) (slots : vec (hashmap_list_t t))
   (i : usize) :
   Tot (result ((hashmap_hash_map_t t) & (vec (hashmap_list_t t))))
-  (decreases (hashmap_hash_map_move_elements_decreases t hm v i))
+  (decreases (hashmap_hash_map_move_elements_decreases t ntable slots i))
   =
-  let i0 = vec_len (hashmap_list_t t) v in
+  let i0 = vec_len (hashmap_list_t t) slots in
   if i < i0
   then
-    begin match vec_index_mut_fwd (hashmap_list_t t) v i with
+    begin match vec_index_mut_fwd (hashmap_list_t t) slots i with
     | Fail e -> Fail e
     | Return l ->
       let ls = mem_replace_fwd (hashmap_list_t t) l HashmapListNil in
-      begin match hashmap_hash_map_move_elements_from_list_fwd_back t hm ls
+      begin match hashmap_hash_map_move_elements_from_list_fwd_back t ntable ls
         with
       | Fail e -> Fail e
-      | Return ntable ->
+      | Return ntable0 ->
         begin match usize_add i 1 with
         | Fail e -> Fail e
         | Return i1 ->
           let l0 = mem_replace_back (hashmap_list_t t) l HashmapListNil in
-          begin match vec_index_mut_back (hashmap_list_t t) v i l0 with
+          begin match vec_index_mut_back (hashmap_list_t t) slots i l0 with
           | Fail e -> Fail e
-          | Return slots ->
-            hashmap_hash_map_move_elements_loop_fwd_back t ntable slots i1
+          | Return slots0 ->
+            hashmap_hash_map_move_elements_loop_fwd_back t ntable0 slots0 i1
           end
         end
       end
     end
-  else Return (hm, v)
+  else Return (ntable, slots)
 
 (** [hashmap_main::hashmap::HashMap::{0}::move_elements] *)
 let hashmap_hash_map_move_elements_fwd_back
@@ -334,15 +335,15 @@ let hashmap_hash_map_insert_fwd_back
 
 (** [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] *)
 let rec hashmap_hash_map_contains_key_in_list_loop_fwd
-  (t : Type0) (i : usize) (ls : hashmap_list_t t) :
+  (t : Type0) (key : usize) (ls : hashmap_list_t t) :
   Tot (result bool)
-  (decreases (hashmap_hash_map_contains_key_in_list_decreases t i ls))
+  (decreases (hashmap_hash_map_contains_key_in_list_decreases t key ls))
   =
   begin match ls with
   | HashmapListCons ckey x tl ->
-    if ckey = i
+    if ckey = key
     then Return true
-    else hashmap_hash_map_contains_key_in_list_loop_fwd t i tl
+    else hashmap_hash_map_contains_key_in_list_loop_fwd t key tl
   | HashmapListNil -> Return false
   end
 
@@ -372,14 +373,14 @@ let hashmap_hash_map_contains_key_fwd
 
 (** [hashmap_main::hashmap::HashMap::{0}::get_in_list] *)
 let rec hashmap_hash_map_get_in_list_loop_fwd
-  (t : Type0) (i : usize) (ls : hashmap_list_t t) :
-  Tot (result t) (decreases (hashmap_hash_map_get_in_list_decreases t i ls))
+  (t : Type0) (key : usize) (ls : hashmap_list_t t) :
+  Tot (result t) (decreases (hashmap_hash_map_get_in_list_decreases t key ls))
   =
   begin match ls with
   | HashmapListCons ckey cvalue tl ->
-    if ckey = i
+    if ckey = key
     then Return cvalue
-    else hashmap_hash_map_get_in_list_loop_fwd t i tl
+    else hashmap_hash_map_get_in_list_loop_fwd t key tl
   | HashmapListNil -> Fail Failure
   end
 
@@ -409,15 +410,15 @@ let hashmap_hash_map_get_fwd
 
 (** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
 let rec hashmap_hash_map_get_mut_in_list_loop_fwd
-  (t : Type0) (i : usize) (ls : hashmap_list_t t) :
+  (t : Type0) (key : usize) (ls : hashmap_list_t t) :
   Tot (result t)
-  (decreases (hashmap_hash_map_get_mut_in_list_decreases t i ls))
+  (decreases (hashmap_hash_map_get_mut_in_list_decreases t key ls))
   =
   begin match ls with
   | HashmapListCons ckey cvalue tl ->
-    if ckey = i
+    if ckey = key
     then Return cvalue
-    else hashmap_hash_map_get_mut_in_list_loop_fwd t i tl
+    else hashmap_hash_map_get_mut_in_list_loop_fwd t key tl
   | HashmapListNil -> Fail Failure
   end
 
@@ -428,16 +429,16 @@ let hashmap_hash_map_get_mut_in_list_fwd
 
 (** [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] *)
 let rec hashmap_hash_map_get_mut_in_list_loop_back
-  (t : Type0) (i : usize) (ls : hashmap_list_t t) (ret : t) :
+  (t : Type0) (key : usize) (ls : hashmap_list_t t) (ret : t) :
   Tot (result (hashmap_list_t t))
-  (decreases (hashmap_hash_map_get_mut_in_list_decreases t i ls))
+  (decreases (hashmap_hash_map_get_mut_in_list_decreases t key ls))
   =
   begin match ls with
   | HashmapListCons ckey cvalue tl ->
-    if ckey = i
+    if ckey = key
     then Return (HashmapListCons ckey ret tl)
     else
-      begin match hashmap_hash_map_get_mut_in_list_loop_back t i tl ret with
+      begin match hashmap_hash_map_get_mut_in_list_loop_back t key tl ret with
       | Fail e -> Fail e
       | Return l -> Return (HashmapListCons ckey cvalue l)
       end
@@ -506,22 +507,22 @@ let hashmap_hash_map_get_mut_back
 
 (** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *)
 let rec hashmap_hash_map_remove_from_list_loop_fwd
-  (t : Type0) (i : usize) (ls : hashmap_list_t t) :
+  (t : Type0) (key : usize) (ls : hashmap_list_t t) :
   Tot (result (option t))
-  (decreases (hashmap_hash_map_remove_from_list_decreases t i ls))
+  (decreases (hashmap_hash_map_remove_from_list_decreases t key ls))
   =
   begin match ls with
   | HashmapListCons ckey x tl ->
-    if ckey = i
+    if ckey = key
     then
       let mv_ls =
         mem_replace_fwd (hashmap_list_t t) (HashmapListCons ckey x tl)
           HashmapListNil in
       begin match mv_ls with
-      | HashmapListCons i0 cvalue tl0 -> Return (Some cvalue)
+      | HashmapListCons i cvalue tl0 -> Return (Some cvalue)
       | HashmapListNil -> Fail Failure
       end
-    else hashmap_hash_map_remove_from_list_loop_fwd t i tl
+    else hashmap_hash_map_remove_from_list_loop_fwd t key tl
   | HashmapListNil -> Return None
   end
 
@@ -532,23 +533,23 @@ let hashmap_hash_map_remove_from_list_fwd
 
 (** [hashmap_main::hashmap::HashMap::{0}::remove_from_list] *)
 let rec hashmap_hash_map_remove_from_list_loop_back
-  (t : Type0) (i : usize) (ls : hashmap_list_t t) :
+  (t : Type0) (key : usize) (ls : hashmap_list_t t) :
   Tot (result (hashmap_list_t t))
-  (decreases (hashmap_hash_map_remove_from_list_decreases t i ls))
+  (decreases (hashmap_hash_map_remove_from_list_decreases t key ls))
   =
   begin match ls with
   | HashmapListCons ckey x tl ->
-    if ckey = i
+    if ckey = key
     then
       let mv_ls =
         mem_replace_fwd (hashmap_list_t t) (HashmapListCons ckey x tl)
           HashmapListNil in
       begin match mv_ls with
-      | HashmapListCons i0 cvalue tl0 -> Return tl0
+      | HashmapListCons i cvalue tl0 -> Return tl0
       | HashmapListNil -> Fail Failure
       end
     else
-      begin match hashmap_hash_map_remove_from_list_loop_back t i tl with
+      begin match hashmap_hash_map_remove_from_list_loop_back t key tl with
       | Fail e -> Fail e
       | Return l -> Return (HashmapListCons ckey x l)
       end
diff --git a/tests/fstar/misc/Loops.Clauses.Template.fst b/tests/fstar/misc/Loops.Clauses.Template.fst
index 3d475d20..1b141d64 100644
--- a/tests/fstar/misc/Loops.Clauses.Template.fst
+++ b/tests/fstar/misc/Loops.Clauses.Template.fst
@@ -23,7 +23,7 @@ let sum_with_shared_borrows_decreases (max : u32) (i : u32) (s : u32) : nat =
 unfold let clear_decreases (v : vec u32) (i : usize) : nat = admit ()
 
 (** [loops::list_mem]: decreases clause *)
-unfold let list_mem_decreases (i : u32) (ls : list_t u32) : nat = admit ()
+unfold let list_mem_decreases (x : u32) (ls : list_t u32) : nat = admit ()
 
 (** [loops::list_nth_mut_loop]: decreases clause *)
 unfold
@@ -42,8 +42,8 @@ let get_elem_mut_decreases (x : usize) (ls : list_t usize) : nat = admit ()
 
 (** [loops::get_elem_shared]: decreases clause *)
 unfold
-let get_elem_shared_decreases (x : usize) (v : vec (list_t usize))
-  (l : list_t usize) (ls : list_t usize) : nat =
+let get_elem_shared_decreases (x : usize) (slots : vec (list_t usize))
+  (ls : list_t usize) (ls0 : list_t usize) : nat =
   admit ()
 
 (** [loops::list_nth_mut_loop_with_id]: decreases clause *)
@@ -54,55 +54,55 @@ let list_nth_mut_loop_with_id_decreases (t : Type0) (i : u32) (ls : list_t t) :
 
 (** [loops::list_nth_shared_loop_with_id]: decreases clause *)
 unfold
-let list_nth_shared_loop_with_id_decreases (t : Type0) (l : list_t t) 
-  (i : u32) (ls : list_t t) : nat =
+let list_nth_shared_loop_with_id_decreases (t : Type0) (ls : list_t t)
+  (i : u32) (ls0 : list_t t) : nat =
   admit ()
 
 (** [loops::list_nth_mut_loop_pair]: decreases clause *)
 unfold
-let list_nth_mut_loop_pair_decreases (t : Type0) (l : list_t t) (l0 : list_t t)
-  (i : u32) : nat =
+let list_nth_mut_loop_pair_decreases (t : Type0) (ls0 : list_t t)
+  (ls1 : list_t t) (i : u32) : nat =
   admit ()
 
 (** [loops::list_nth_shared_loop_pair]: decreases clause *)
 unfold
-let list_nth_shared_loop_pair_decreases (t : Type0) (l : list_t t)
-  (l0 : list_t t) (i : u32) : nat =
+let list_nth_shared_loop_pair_decreases (t : Type0) (ls0 : list_t t)
+  (ls1 : list_t t) (i : u32) : nat =
   admit ()
 
 (** [loops::list_nth_mut_loop_pair_merge]: decreases clause *)
 unfold
-let list_nth_mut_loop_pair_merge_decreases (t : Type0) (l : list_t t)
-  (l0 : list_t t) (i : u32) : nat =
+let list_nth_mut_loop_pair_merge_decreases (t : Type0) (ls0 : list_t t)
+  (ls1 : list_t t) (i : u32) : nat =
   admit ()
 
 (** [loops::list_nth_shared_loop_pair_merge]: decreases clause *)
 unfold
-let list_nth_shared_loop_pair_merge_decreases (t : Type0) (l : list_t t)
-  (l0 : list_t t) (i : u32) : nat =
+let list_nth_shared_loop_pair_merge_decreases (t : Type0) (ls0 : list_t t)
+  (ls1 : list_t t) (i : u32) : nat =
   admit ()
 
 (** [loops::list_nth_mut_shared_loop_pair]: decreases clause *)
 unfold
-let list_nth_mut_shared_loop_pair_decreases (t : Type0) (l : list_t t)
-  (l0 : list_t t) (i : u32) : nat =
+let list_nth_mut_shared_loop_pair_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 *)
 unfold
-let list_nth_mut_shared_loop_pair_merge_decreases (t : Type0) (l : list_t t)
-  (l0 : list_t t) (i : u32) : nat =
+let list_nth_mut_shared_loop_pair_merge_decreases (t : Type0) (ls0 : list_t t)
+  (ls1 : list_t t) (i : u32) : nat =
   admit ()
 
 (** [loops::list_nth_shared_mut_loop_pair]: decreases clause *)
 unfold
-let list_nth_shared_mut_loop_pair_decreases (t : Type0) (l : list_t t)
-  (l0 : list_t t) (i : u32) : nat =
+let list_nth_shared_mut_loop_pair_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 *)
 unfold
-let list_nth_shared_mut_loop_pair_merge_decreases (t : Type0) (l : list_t t)
-  (l0 : list_t t) (i : u32) : nat =
+let list_nth_shared_mut_loop_pair_merge_decreases (t : Type0) (ls0 : list_t t)
+  (ls1 : list_t t) (i : u32) : nat =
   admit ()
 
diff --git a/tests/fstar/misc/Loops.Funs.fst b/tests/fstar/misc/Loops.Funs.fst
index b7dcd045..ca918e35 100644
--- a/tests/fstar/misc/Loops.Funs.fst
+++ b/tests/fstar/misc/Loops.Funs.fst
@@ -92,11 +92,11 @@ let clear_fwd_back (v : vec u32) : result (vec u32) = clear_loop_fwd_back v 0
 
 (** [loops::list_mem] *)
 let rec list_mem_loop_fwd
-  (i : u32) (ls : list_t u32) :
-  Tot (result bool) (decreases (list_mem_decreases i ls))
+  (x : u32) (ls : list_t u32) :
+  Tot (result bool) (decreases (list_mem_decreases x ls))
   =
   begin match ls with
-  | ListCons y tl -> if y = i then Return true else list_mem_loop_fwd i tl
+  | ListCons y tl -> if y = x then Return true else list_mem_loop_fwd x tl
   | ListNil -> Return false
   end
 
@@ -222,12 +222,13 @@ let get_elem_mut_back
 
 (** [loops::get_elem_shared] *)
 let rec get_elem_shared_loop_fwd
-  (x : usize) (v : vec (list_t usize)) (l : list_t usize) (ls : list_t usize) :
-  Tot (result usize) (decreases (get_elem_shared_decreases x v l ls))
+  (x : usize) (slots : vec (list_t usize)) (ls : list_t usize)
+  (ls0 : list_t usize) :
+  Tot (result usize) (decreases (get_elem_shared_decreases x slots ls ls0))
   =
-  begin match ls with
+  begin match ls0 with
   | ListCons y tl ->
-    if y = x then Return y else get_elem_shared_loop_fwd x v l tl
+    if y = x then Return y else get_elem_shared_loop_fwd x slots ls tl
   | ListNil -> Fail Failure
   end
 
@@ -311,17 +312,18 @@ let list_nth_mut_loop_with_id_back
 
 (** [loops::list_nth_shared_loop_with_id] *)
 let rec list_nth_shared_loop_with_id_loop_fwd
-  (t : Type0) (l : list_t t) (i : u32) (ls : list_t t) :
-  Tot (result t) (decreases (list_nth_shared_loop_with_id_decreases t l i ls))
+  (t : Type0) (ls : list_t t) (i : u32) (ls0 : list_t t) :
+  Tot (result t)
+  (decreases (list_nth_shared_loop_with_id_decreases t ls i ls0))
   =
-  begin match ls with
+  begin match ls0 with
   | ListCons x tl ->
     if i = 0
     then Return x
     else
       begin match u32_sub i 1 with
       | Fail e -> Fail e
-      | Return i0 -> list_nth_shared_loop_with_id_loop_fwd t l i0 tl
+      | Return i0 -> list_nth_shared_loop_with_id_loop_fwd t ls i0 tl
       end
   | ListNil -> Fail Failure
   end
@@ -336,12 +338,13 @@ let list_nth_shared_loop_with_id_fwd
 
 (** [loops::list_nth_mut_loop_pair] *)
 let rec list_nth_mut_loop_pair_loop_fwd
-  (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) :
-  Tot (result (t & t)) (decreases (list_nth_mut_loop_pair_decreases t l l0 i))
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
+  Tot (result (t & t))
+  (decreases (list_nth_mut_loop_pair_decreases t ls0 ls1 i))
   =
-  begin match l with
+  begin match ls0 with
   | ListCons x0 tl0 ->
-    begin match l0 with
+    begin match ls1 with
     | ListCons x1 tl1 ->
       if i = 0
       then Return (x0, x1)
@@ -362,13 +365,13 @@ let list_nth_mut_loop_pair_fwd
 
 (** [loops::list_nth_mut_loop_pair] *)
 let rec list_nth_mut_loop_pair_loop_back'a
-  (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) (ret : t) :
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) :
   Tot (result (list_t t))
-  (decreases (list_nth_mut_loop_pair_decreases t l l0 i))
+  (decreases (list_nth_mut_loop_pair_decreases t ls0 ls1 i))
   =
-  begin match l with
+  begin match ls0 with
   | ListCons x0 tl0 ->
-    begin match l0 with
+    begin match ls1 with
     | ListCons x1 tl1 ->
       if i = 0
       then Return (ListCons ret tl0)
@@ -378,7 +381,7 @@ let rec list_nth_mut_loop_pair_loop_back'a
         | Return i0 ->
           begin match list_nth_mut_loop_pair_loop_back'a t tl0 tl1 i0 ret with
           | Fail e -> Fail e
-          | Return l1 -> Return (ListCons x0 l1)
+          | Return l -> Return (ListCons x0 l)
           end
         end
     | ListNil -> Fail Failure
@@ -395,13 +398,13 @@ let list_nth_mut_loop_pair_back'a
 
 (** [loops::list_nth_mut_loop_pair] *)
 let rec list_nth_mut_loop_pair_loop_back'b
-  (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) (ret : t) :
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) :
   Tot (result (list_t t))
-  (decreases (list_nth_mut_loop_pair_decreases t l l0 i))
+  (decreases (list_nth_mut_loop_pair_decreases t ls0 ls1 i))
   =
-  begin match l with
+  begin match ls0 with
   | ListCons x0 tl0 ->
-    begin match l0 with
+    begin match ls1 with
     | ListCons x1 tl1 ->
       if i = 0
       then Return (ListCons ret tl1)
@@ -411,7 +414,7 @@ let rec list_nth_mut_loop_pair_loop_back'b
         | Return i0 ->
           begin match list_nth_mut_loop_pair_loop_back'b t tl0 tl1 i0 ret with
           | Fail e -> Fail e
-          | Return l1 -> Return (ListCons x1 l1)
+          | Return l -> Return (ListCons x1 l)
           end
         end
     | ListNil -> Fail Failure
@@ -428,13 +431,13 @@ let list_nth_mut_loop_pair_back'b
 
 (** [loops::list_nth_shared_loop_pair] *)
 let rec list_nth_shared_loop_pair_loop_fwd
-  (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) :
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
   Tot (result (t & t))
-  (decreases (list_nth_shared_loop_pair_decreases t l l0 i))
+  (decreases (list_nth_shared_loop_pair_decreases t ls0 ls1 i))
   =
-  begin match l with
+  begin match ls0 with
   | ListCons x0 tl0 ->
-    begin match l0 with
+    begin match ls1 with
     | ListCons x1 tl1 ->
       if i = 0
       then Return (x0, x1)
@@ -455,13 +458,13 @@ let list_nth_shared_loop_pair_fwd
 
 (** [loops::list_nth_mut_loop_pair_merge] *)
 let rec list_nth_mut_loop_pair_merge_loop_fwd
-  (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) :
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
   Tot (result (t & t))
-  (decreases (list_nth_mut_loop_pair_merge_decreases t l l0 i))
+  (decreases (list_nth_mut_loop_pair_merge_decreases t ls0 ls1 i))
   =
-  begin match l with
+  begin match ls0 with
   | ListCons x0 tl0 ->
-    begin match l0 with
+    begin match ls1 with
     | ListCons x1 tl1 ->
       if i = 0
       then Return (x0, x1)
@@ -482,13 +485,13 @@ let list_nth_mut_loop_pair_merge_fwd
 
 (** [loops::list_nth_mut_loop_pair_merge] *)
 let rec list_nth_mut_loop_pair_merge_loop_back
-  (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) (ret : (t & t)) :
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : (t & t)) :
   Tot (result ((list_t t) & (list_t t)))
-  (decreases (list_nth_mut_loop_pair_merge_decreases t l l0 i))
+  (decreases (list_nth_mut_loop_pair_merge_decreases t ls0 ls1 i))
   =
-  begin match l with
+  begin match ls0 with
   | ListCons x0 tl0 ->
-    begin match l0 with
+    begin match ls1 with
     | ListCons x1 tl1 ->
       if i = 0
       then let (x, x2) = ret in Return (ListCons x tl0, ListCons x2 tl1)
@@ -499,7 +502,7 @@ let rec list_nth_mut_loop_pair_merge_loop_back
           begin match list_nth_mut_loop_pair_merge_loop_back t tl0 tl1 i0 ret
             with
           | Fail e -> Fail e
-          | Return (l1, l2) -> Return (ListCons x0 l1, ListCons x1 l2)
+          | Return (l, l0) -> Return (ListCons x0 l, ListCons x1 l0)
           end
         end
     | ListNil -> Fail Failure
@@ -516,13 +519,13 @@ let list_nth_mut_loop_pair_merge_back
 
 (** [loops::list_nth_shared_loop_pair_merge] *)
 let rec list_nth_shared_loop_pair_merge_loop_fwd
-  (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) :
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
   Tot (result (t & t))
-  (decreases (list_nth_shared_loop_pair_merge_decreases t l l0 i))
+  (decreases (list_nth_shared_loop_pair_merge_decreases t ls0 ls1 i))
   =
-  begin match l with
+  begin match ls0 with
   | ListCons x0 tl0 ->
-    begin match l0 with
+    begin match ls1 with
     | ListCons x1 tl1 ->
       if i = 0
       then Return (x0, x1)
@@ -543,13 +546,13 @@ let list_nth_shared_loop_pair_merge_fwd
 
 (** [loops::list_nth_mut_shared_loop_pair] *)
 let rec list_nth_mut_shared_loop_pair_loop_fwd
-  (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) :
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
   Tot (result (t & t))
-  (decreases (list_nth_mut_shared_loop_pair_decreases t l l0 i))
+  (decreases (list_nth_mut_shared_loop_pair_decreases t ls0 ls1 i))
   =
-  begin match l with
+  begin match ls0 with
   | ListCons x0 tl0 ->
-    begin match l0 with
+    begin match ls1 with
     | ListCons x1 tl1 ->
       if i = 0
       then Return (x0, x1)
@@ -570,13 +573,13 @@ let list_nth_mut_shared_loop_pair_fwd
 
 (** [loops::list_nth_mut_shared_loop_pair] *)
 let rec list_nth_mut_shared_loop_pair_loop_back
-  (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) (ret : t) :
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) :
   Tot (result (list_t t))
-  (decreases (list_nth_mut_shared_loop_pair_decreases t l l0 i))
+  (decreases (list_nth_mut_shared_loop_pair_decreases t ls0 ls1 i))
   =
-  begin match l with
+  begin match ls0 with
   | ListCons x0 tl0 ->
-    begin match l0 with
+    begin match ls1 with
     | ListCons x1 tl1 ->
       if i = 0
       then Return (ListCons ret tl0)
@@ -587,7 +590,7 @@ let rec list_nth_mut_shared_loop_pair_loop_back
           begin match list_nth_mut_shared_loop_pair_loop_back t tl0 tl1 i0 ret
             with
           | Fail e -> Fail e
-          | Return l1 -> Return (ListCons x0 l1)
+          | Return l -> Return (ListCons x0 l)
           end
         end
     | ListNil -> Fail Failure
@@ -604,13 +607,13 @@ let list_nth_mut_shared_loop_pair_back
 
 (** [loops::list_nth_mut_shared_loop_pair_merge] *)
 let rec list_nth_mut_shared_loop_pair_merge_loop_fwd
-  (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) :
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
   Tot (result (t & t))
-  (decreases (list_nth_mut_shared_loop_pair_merge_decreases t l l0 i))
+  (decreases (list_nth_mut_shared_loop_pair_merge_decreases t ls0 ls1 i))
   =
-  begin match l with
+  begin match ls0 with
   | ListCons x0 tl0 ->
-    begin match l0 with
+    begin match ls1 with
     | ListCons x1 tl1 ->
       if i = 0
       then Return (x0, x1)
@@ -632,13 +635,13 @@ let list_nth_mut_shared_loop_pair_merge_fwd
 
 (** [loops::list_nth_mut_shared_loop_pair_merge] *)
 let rec list_nth_mut_shared_loop_pair_merge_loop_back
-  (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) (ret : t) :
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) :
   Tot (result (list_t t))
-  (decreases (list_nth_mut_shared_loop_pair_merge_decreases t l l0 i))
+  (decreases (list_nth_mut_shared_loop_pair_merge_decreases t ls0 ls1 i))
   =
-  begin match l with
+  begin match ls0 with
   | ListCons x0 tl0 ->
-    begin match l0 with
+    begin match ls1 with
     | ListCons x1 tl1 ->
       if i = 0
       then Return (ListCons ret tl0)
@@ -649,7 +652,7 @@ let rec list_nth_mut_shared_loop_pair_merge_loop_back
           begin match
             list_nth_mut_shared_loop_pair_merge_loop_back t tl0 tl1 i0 ret with
           | Fail e -> Fail e
-          | Return l1 -> Return (ListCons x0 l1)
+          | Return l -> Return (ListCons x0 l)
           end
         end
     | ListNil -> Fail Failure
@@ -666,13 +669,13 @@ let list_nth_mut_shared_loop_pair_merge_back
 
 (** [loops::list_nth_shared_mut_loop_pair] *)
 let rec list_nth_shared_mut_loop_pair_loop_fwd
-  (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) :
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
   Tot (result (t & t))
-  (decreases (list_nth_shared_mut_loop_pair_decreases t l l0 i))
+  (decreases (list_nth_shared_mut_loop_pair_decreases t ls0 ls1 i))
   =
-  begin match l with
+  begin match ls0 with
   | ListCons x0 tl0 ->
-    begin match l0 with
+    begin match ls1 with
     | ListCons x1 tl1 ->
       if i = 0
       then Return (x0, x1)
@@ -693,13 +696,13 @@ let list_nth_shared_mut_loop_pair_fwd
 
 (** [loops::list_nth_shared_mut_loop_pair] *)
 let rec list_nth_shared_mut_loop_pair_loop_back
-  (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) (ret : t) :
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) :
   Tot (result (list_t t))
-  (decreases (list_nth_shared_mut_loop_pair_decreases t l l0 i))
+  (decreases (list_nth_shared_mut_loop_pair_decreases t ls0 ls1 i))
   =
-  begin match l with
+  begin match ls0 with
   | ListCons x0 tl0 ->
-    begin match l0 with
+    begin match ls1 with
     | ListCons x1 tl1 ->
       if i = 0
       then Return (ListCons ret tl1)
@@ -710,7 +713,7 @@ let rec list_nth_shared_mut_loop_pair_loop_back
           begin match list_nth_shared_mut_loop_pair_loop_back t tl0 tl1 i0 ret
             with
           | Fail e -> Fail e
-          | Return l1 -> Return (ListCons x1 l1)
+          | Return l -> Return (ListCons x1 l)
           end
         end
     | ListNil -> Fail Failure
@@ -727,13 +730,13 @@ let list_nth_shared_mut_loop_pair_back
 
 (** [loops::list_nth_shared_mut_loop_pair_merge] *)
 let rec list_nth_shared_mut_loop_pair_merge_loop_fwd
-  (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) :
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
   Tot (result (t & t))
-  (decreases (list_nth_shared_mut_loop_pair_merge_decreases t l l0 i))
+  (decreases (list_nth_shared_mut_loop_pair_merge_decreases t ls0 ls1 i))
   =
-  begin match l with
+  begin match ls0 with
   | ListCons x0 tl0 ->
-    begin match l0 with
+    begin match ls1 with
     | ListCons x1 tl1 ->
       if i = 0
       then Return (x0, x1)
@@ -755,13 +758,13 @@ let list_nth_shared_mut_loop_pair_merge_fwd
 
 (** [loops::list_nth_shared_mut_loop_pair_merge] *)
 let rec list_nth_shared_mut_loop_pair_merge_loop_back
-  (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) (ret : t) :
+  (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) :
   Tot (result (list_t t))
-  (decreases (list_nth_shared_mut_loop_pair_merge_decreases t l l0 i))
+  (decreases (list_nth_shared_mut_loop_pair_merge_decreases t ls0 ls1 i))
   =
-  begin match l with
+  begin match ls0 with
   | ListCons x0 tl0 ->
-    begin match l0 with
+    begin match ls1 with
     | ListCons x1 tl1 ->
       if i = 0
       then Return (ListCons ret tl1)
@@ -772,7 +775,7 @@ let rec list_nth_shared_mut_loop_pair_merge_loop_back
           begin match
             list_nth_shared_mut_loop_pair_merge_loop_back t tl0 tl1 i0 ret with
           | Fail e -> Fail e
-          | Return l1 -> Return (ListCons x1 l1)
+          | Return l -> Return (ListCons x1 l)
           end
         end
     | ListNil -> Fail Failure