Regenerate the test files

6 files changed, 93 insertions, 86 deletions

diff --git a/tests/hashmap/Hashmap.Funs.fst b/tests/hashmap/Hashmap.Funs.fst
index 80783781..f75a0c01 100644
--- a/tests/hashmap/Hashmap.Funs.fst
+++ b/tests/hashmap/Hashmap.Funs.fst
@@ -21,13 +21,13 @@ let rec hash_map_allocate_slots_fwd
   | _ ->
     begin match vec_push_back (list_t t) slots ListNil with
     | Fail -> Fail
-    | Return v ->
+    | Return slots0 ->
       begin match usize_sub n 1 with
       | Fail -> Fail
       | Return i ->
-        begin match hash_map_allocate_slots_fwd t v i with
+        begin match hash_map_allocate_slots_fwd t slots0 i with
         | Fail -> Fail
-        | Return v0 -> Return v0
+        | Return v -> Return v
         end
       end
     end
@@ -72,13 +72,13 @@ let rec hash_map_clear_slots_fwd_back
   then
     begin match vec_index_mut_back (list_t t) slots i ListNil with
     | Fail -> Fail
-    | Return v ->
+    | Return slots0 ->
       begin match usize_add i 1 with
       | Fail -> Fail
       | Return i1 ->
-        begin match hash_map_clear_slots_fwd_back t v i1 with
+        begin match hash_map_clear_slots_fwd_back t slots0 i1 with
         | Fail -> Fail
-        | Return v0 -> Return v0
+        | Return slots1 -> Return slots1
         end
       end
     end
@@ -129,7 +129,7 @@ let rec hash_map_insert_in_list_back
     else
       begin match hash_map_insert_in_list_back t key value ls0 with
       | Fail -> Fail
-      | Return l -> Return (ListCons ckey cvalue l)
+      | Return ls1 -> Return (ListCons ckey cvalue ls1)
       end
   | ListNil -> let l = ListNil in Return (ListCons key value l)
   end
@@ -200,10 +200,10 @@ let rec hash_map_move_elements_from_list_fwd_back
   | ListCons k v tl ->
     begin match hash_map_insert_no_resize_fwd_back t ntable k v with
     | Fail -> Fail
-    | Return hm ->
-      begin match hash_map_move_elements_from_list_fwd_back t hm tl with
+    | Return ntable0 ->
+      begin match hash_map_move_elements_from_list_fwd_back t ntable0 tl with
       | Fail -> Fail
-      | Return hm0 -> Return hm0
+      | Return ntable1 -> Return ntable1
       end
     end
   | ListNil -> Return ntable
@@ -224,17 +224,18 @@ let rec hash_map_move_elements_fwd_back
       let ls = mem_replace_fwd (list_t t) l ListNil in
       begin match hash_map_move_elements_from_list_fwd_back t ntable ls with
       | Fail -> Fail
-      | Return hm ->
+      | Return ntable0 ->
         let l0 = mem_replace_back (list_t t) l ListNil in
         begin match vec_index_mut_back (list_t t) slots i l0 with
         | Fail -> Fail
-        | Return v ->
+        | Return slots0 ->
           begin match usize_add i 1 with
           | Fail -> Fail
           | Return i1 ->
-            begin match hash_map_move_elements_fwd_back t hm v i1 with
+            begin match hash_map_move_elements_fwd_back t ntable0 slots0 i1
+              with
             | Fail -> Fail
-            | Return (hm0, v0) -> Return (hm0, v0)
+            | Return (ntable1, slots1) -> Return (ntable1, slots1)
             end
           end
         end
@@ -265,9 +266,9 @@ let hash_map_try_resize_fwd_back
               hash_map_move_elements_fwd_back t ntable self.hash_map_slots 0
               with
             | Fail -> Fail
-            | Return (hm, _) ->
+            | Return (ntable0, _) ->
               Return (Mkhash_map_t self.hash_map_num_entries (i, i0)
-                hm.hash_map_max_load hm.hash_map_slots)
+                ntable0.hash_map_max_load ntable0.hash_map_slots)
             end
           end
         end
@@ -284,22 +285,23 @@ let hash_map_insert_fwd_back
   =
   begin match hash_map_insert_no_resize_fwd_back t self key value with
   | Fail -> Fail
-  | Return hm ->
-    begin match hash_map_len_fwd t hm with
+  | Return self0 ->
+    begin match hash_map_len_fwd t self0 with
     | Fail -> Fail
     | Return i ->
-      if i > hm.hash_map_max_load
+      if i > self0.hash_map_max_load
       then
         begin match
-          hash_map_try_resize_fwd_back t (Mkhash_map_t hm.hash_map_num_entries
-            hm.hash_map_max_load_factor hm.hash_map_max_load hm.hash_map_slots)
-          with
+          hash_map_try_resize_fwd_back t (Mkhash_map_t
+            self0.hash_map_num_entries self0.hash_map_max_load_factor
+            self0.hash_map_max_load self0.hash_map_slots) with
         | Fail -> Fail
-        | Return hm0 -> Return hm0
+        | Return self1 -> Return self1
         end
       else
-        Return (Mkhash_map_t hm.hash_map_num_entries
-          hm.hash_map_max_load_factor hm.hash_map_max_load hm.hash_map_slots)
+        Return (Mkhash_map_t self0.hash_map_num_entries
+          self0.hash_map_max_load_factor self0.hash_map_max_load
+          self0.hash_map_slots)
     end
   end
 
@@ -410,7 +412,7 @@ let rec hash_map_get_mut_in_list_back
     else
       begin match hash_map_get_mut_in_list_back t key ls0 ret with
       | Fail -> Fail
-      | Return l -> Return (ListCons ckey cvalue l)
+      | Return ls1 -> Return (ListCons ckey cvalue ls1)
       end
   | ListNil -> Fail
   end
@@ -509,7 +511,7 @@ let rec hash_map_remove_from_list_back
     else
       begin match hash_map_remove_from_list_back t key tl with
       | Fail -> Fail
-      | Return l -> Return (ListCons ckey x l)
+      | Return tl0 -> Return (ListCons ckey x tl0)
       end
   | ListNil -> Return ListNil
   end
diff --git a/tests/hashmap_on_disk/HashmapMain.Funs.fst b/tests/hashmap_on_disk/HashmapMain.Funs.fst
index cf0df7a7..a4167186 100644
--- a/tests/hashmap_on_disk/HashmapMain.Funs.fst
+++ b/tests/hashmap_on_disk/HashmapMain.Funs.fst
@@ -23,13 +23,13 @@ let rec hashmap_hash_map_allocate_slots_fwd
   | _ ->
     begin match vec_push_back (hashmap_list_t t) slots HashmapListNil with
     | Fail -> Fail
-    | Return v ->
+    | Return slots0 ->
       begin match usize_sub n 1 with
       | Fail -> Fail
       | Return i ->
-        begin match hashmap_hash_map_allocate_slots_fwd t v i st with
+        begin match hashmap_hash_map_allocate_slots_fwd t slots0 i st with
         | Fail -> Fail
-        | Return (st0, v0) -> Return (st0, v0)
+        | Return (st0, v) -> Return (st0, v)
         end
       end
     end
@@ -77,11 +77,11 @@ let rec hashmap_hash_map_clear_slots_fwd
     begin match vec_index_mut_back (hashmap_list_t t) slots i HashmapListNil
       with
     | Fail -> Fail
-    | Return v ->
+    | Return slots0 ->
       begin match usize_add i 1 with
       | Fail -> Fail
       | Return i1 ->
-        begin match hashmap_hash_map_clear_slots_fwd t v i1 st with
+        begin match hashmap_hash_map_clear_slots_fwd t slots0 i1 st with
         | Fail -> Fail
         | Return (st0, _) -> Return (st0, ())
         end
@@ -101,13 +101,13 @@ let rec hashmap_hash_map_clear_slots_back
     begin match vec_index_mut_back (hashmap_list_t t) slots i HashmapListNil
       with
     | Fail -> Fail
-    | Return v ->
+    | Return slots0 ->
       begin match usize_add i 1 with
       | Fail -> Fail
       | Return i1 ->
-        begin match hashmap_hash_map_clear_slots_back t v i1 st with
+        begin match hashmap_hash_map_clear_slots_back t slots0 i1 st with
         | Fail -> Fail
-        | Return (st0, v0) -> Return (st0, v0)
+        | Return (st0, slots1) -> Return (st0, slots1)
         end
       end
     end
@@ -175,7 +175,7 @@ let rec hashmap_hash_map_insert_in_list_back
     else
       begin match hashmap_hash_map_insert_in_list_back t key value ls0 st with
       | Fail -> Fail
-      | Return (st0, l) -> Return (st0, HashmapListCons ckey cvalue l)
+      | Return (st0, ls1) -> Return (st0, HashmapListCons ckey cvalue ls1)
       end
   | HashmapListNil ->
     let l = HashmapListNil in Return (st, HashmapListCons key value l)
@@ -288,8 +288,9 @@ let rec hashmap_hash_map_move_elements_from_list_fwd
   | HashmapListCons k v tl ->
     begin match hashmap_hash_map_insert_no_resize_back t ntable k v st with
     | Fail -> Fail
-    | Return (st0, hm) ->
-      begin match hashmap_hash_map_move_elements_from_list_fwd t hm tl st0 with
+    | Return (st0, ntable0) ->
+      begin match hashmap_hash_map_move_elements_from_list_fwd t ntable0 tl st0
+        with
       | Fail -> Fail
       | Return (st1, _) -> Return (st1, ())
       end
@@ -309,11 +310,11 @@ let rec hashmap_hash_map_move_elements_from_list_back
   | HashmapListCons k v tl ->
     begin match hashmap_hash_map_insert_no_resize_back t ntable k v st with
     | Fail -> Fail
-    | Return (st0, hm) ->
-      begin match hashmap_hash_map_move_elements_from_list_back t hm tl st0
-        with
+    | Return (st0, ntable0) ->
+      begin match
+        hashmap_hash_map_move_elements_from_list_back t ntable0 tl st0 with
       | Fail -> Fail
-      | Return (st1, hm0) -> Return (st1, hm0)
+      | Return (st1, ntable1) -> Return (st1, ntable1)
       end
     end
   | HashmapListNil -> Return (st, ntable)
@@ -336,15 +337,16 @@ let rec hashmap_hash_map_move_elements_fwd
       begin match hashmap_hash_map_move_elements_from_list_back t ntable ls st
         with
       | Fail -> Fail
-      | Return (st0, hm) ->
+      | Return (st0, ntable0) ->
         let l0 = mem_replace_back (hashmap_list_t t) l HashmapListNil in
         begin match vec_index_mut_back (hashmap_list_t t) slots i l0 with
         | Fail -> Fail
-        | Return v ->
+        | Return slots0 ->
           begin match usize_add i 1 with
           | Fail -> Fail
           | Return i1 ->
-            begin match hashmap_hash_map_move_elements_fwd t hm v i1 st0 with
+            begin match
+              hashmap_hash_map_move_elements_fwd t ntable0 slots0 i1 st0 with
             | Fail -> Fail
             | Return (st1, _) -> Return (st1, ())
             end
@@ -371,17 +373,19 @@ let rec hashmap_hash_map_move_elements_back
       begin match hashmap_hash_map_move_elements_from_list_back t ntable ls st
         with
       | Fail -> Fail
-      | Return (st0, hm) ->
+      | Return (st0, ntable0) ->
         let l0 = mem_replace_back (hashmap_list_t t) l HashmapListNil in
         begin match vec_index_mut_back (hashmap_list_t t) slots i l0 with
         | Fail -> Fail
-        | Return v ->
+        | Return slots0 ->
           begin match usize_add i 1 with
           | Fail -> Fail
           | Return i1 ->
-            begin match hashmap_hash_map_move_elements_back t hm v i1 st0 with
+            begin match
+              hashmap_hash_map_move_elements_back t ntable0 slots0 i1 st0 with
             | Fail -> Fail
-            | Return (st1, (hm0, v0)) -> Return (st1, (hm0, v0))
+            | Return (st1, (ntable1, slots1)) ->
+              Return (st1, (ntable1, slots1))
             end
           end
         end
@@ -447,10 +451,11 @@ let hashmap_hash_map_try_resize_back
               hashmap_hash_map_move_elements_back t ntable
                 self.hashmap_hash_map_slots 0 st0 with
             | Fail -> Fail
-            | Return (st1, (hm, _)) ->
+            | Return (st1, (ntable0, _)) ->
               Return (st1, Mkhashmap_hash_map_t
                 self.hashmap_hash_map_num_entries (i, i0)
-                hm.hashmap_hash_map_max_load hm.hashmap_hash_map_slots)
+                ntable0.hashmap_hash_map_max_load
+                ntable0.hashmap_hash_map_slots)
             end
           end
         end
@@ -468,16 +473,18 @@ let hashmap_hash_map_insert_fwd
   =
   begin match hashmap_hash_map_insert_no_resize_back t self key value st with
   | Fail -> Fail
-  | Return (st0, hm) ->
-    begin match hashmap_hash_map_len_fwd t hm st0 with
+  | Return (st0, self0) ->
+    begin match hashmap_hash_map_len_fwd t self0 st0 with
     | Fail -> Fail
     | Return (st1, i) ->
-      if i > hm.hashmap_hash_map_max_load
+      if i > self0.hashmap_hash_map_max_load
       then
         begin match
           hashmap_hash_map_try_resize_fwd t (Mkhashmap_hash_map_t
-            hm.hashmap_hash_map_num_entries hm.hashmap_hash_map_max_load_factor
-            hm.hashmap_hash_map_max_load hm.hashmap_hash_map_slots) st1 with
+            self0.hashmap_hash_map_num_entries
+            self0.hashmap_hash_map_max_load_factor
+            self0.hashmap_hash_map_max_load self0.hashmap_hash_map_slots) 
+            st1 with
         | Fail -> Fail
         | Return (st2, _) -> Return (st2, ())
         end
@@ -493,23 +500,25 @@ let hashmap_hash_map_insert_back
   =
   begin match hashmap_hash_map_insert_no_resize_back t self key value st with
   | Fail -> Fail
-  | Return (st0, hm) ->
-    begin match hashmap_hash_map_len_fwd t hm st0 with
+  | Return (st0, self0) ->
+    begin match hashmap_hash_map_len_fwd t self0 st0 with
     | Fail -> Fail
     | Return (st1, i) ->
-      if i > hm.hashmap_hash_map_max_load
+      if i > self0.hashmap_hash_map_max_load
       then
         begin match
           hashmap_hash_map_try_resize_back t (Mkhashmap_hash_map_t
-            hm.hashmap_hash_map_num_entries hm.hashmap_hash_map_max_load_factor
-            hm.hashmap_hash_map_max_load hm.hashmap_hash_map_slots) st1 with
+            self0.hashmap_hash_map_num_entries
+            self0.hashmap_hash_map_max_load_factor
+            self0.hashmap_hash_map_max_load self0.hashmap_hash_map_slots) 
+            st1 with
         | Fail -> Fail
-        | Return (st2, hm0) -> Return (st2, hm0)
+        | Return (st2, self1) -> Return (st2, self1)
         end
       else
-        Return (st1, Mkhashmap_hash_map_t hm.hashmap_hash_map_num_entries
-          hm.hashmap_hash_map_max_load_factor hm.hashmap_hash_map_max_load
-          hm.hashmap_hash_map_slots)
+        Return (st1, Mkhashmap_hash_map_t self0.hashmap_hash_map_num_entries
+          self0.hashmap_hash_map_max_load_factor
+          self0.hashmap_hash_map_max_load self0.hashmap_hash_map_slots)
     end
   end
 
@@ -630,7 +639,7 @@ let rec hashmap_hash_map_get_mut_in_list_back
     else
       begin match hashmap_hash_map_get_mut_in_list_back t key ls0 ret st with
       | Fail -> Fail
-      | Return (st0, l) -> Return (st0, HashmapListCons ckey cvalue l)
+      | Return (st0, ls1) -> Return (st0, HashmapListCons ckey cvalue ls1)
       end
   | HashmapListNil -> Fail
   end
@@ -740,7 +749,7 @@ let rec hashmap_hash_map_remove_from_list_back
     else
       begin match hashmap_hash_map_remove_from_list_back t key tl st with
       | Fail -> Fail
-      | Return (st0, l) -> Return (st0, HashmapListCons ckey x l)
+      | Return (st0, tl0) -> Return (st0, HashmapListCons ckey x tl0)
       end
   | HashmapListNil -> Return (st, HashmapListNil)
   end
diff --git a/tests/misc/BetreeNll.fst b/tests/misc/BetreeNll.fst
index ae35827c..14c1d2ba 100644
--- a/tests/misc/BetreeNll.fst
+++ b/tests/misc/BetreeNll.fst
@@ -34,7 +34,7 @@ let rec get_list_at_x_back
     else
       begin match get_list_at_x_back tl x ret with
       | Fail -> Fail
-      | Return l -> Return (ListCons hd l)
+      | Return tl0 -> Return (ListCons hd tl0)
       end
   | ListNil -> Return ret
   end
diff --git a/tests/misc/External.Funs.fst b/tests/misc/External.Funs.fst
index 927dad9c..57e9deee 100644
--- a/tests/misc/External.Funs.fst
+++ b/tests/misc/External.Funs.fst
@@ -22,7 +22,7 @@ let swap_back
   | Return (st0, x0) ->
     begin match core_mem_swap_back1 t x y st0 with
     | Fail -> Fail
-    | Return (st1, x1) -> Return (st1, (x0, x1))
+    | Return (st1, y0) -> Return (st1, (x0, y0))
     end
   end
 
diff --git a/tests/misc/NoNestedBorrows.fst b/tests/misc/NoNestedBorrows.fst
index e2457a72..8620f7e9 100644
--- a/tests/misc/NoNestedBorrows.fst
+++ b/tests/misc/NoNestedBorrows.fst
@@ -112,7 +112,7 @@ let _ = assert_norm (test_list1_fwd = Return ())
 
 (** [no_nested_borrows::test_box1] *)
 let test_box1_fwd : result unit =
-  let i = 1 in let x = i in if not (x = 1) then Fail else Return ()
+  let b = 1 in let x = b in if not (x = 1) then Fail else Return ()
 
 (** Unit test for [no_nested_borrows::test_box1] *)
 let _ = assert_norm (test_box1_fwd = Return ())
@@ -192,10 +192,8 @@ let get_elem_test_fwd : result unit =
       else
         begin match get_elem_back i32 true 0 0 z0 with
         | Fail -> Fail
-        | Return (i, i0) ->
-          if not (i = 1)
-          then Fail
-          else if not (i0 = 0) then Fail else Return ()
+        | Return (x, y) ->
+          if not (x = 1) then Fail else if not (y = 0) then Fail else Return ()
         end
     end
   end
@@ -334,7 +332,7 @@ let rec list_nth_mut_back
       | Return i0 ->
         begin match list_nth_mut_back t tl i0 ret with
         | Fail -> Fail
-        | Return l0 -> Return (ListCons x l0)
+        | Return tl0 -> Return (ListCons x tl0)
         end
       end
     end
@@ -392,20 +390,20 @@ let test_list_functions_fwd : result unit =
                 else
                   begin match list_nth_mut_back i32 (ListCons 0 l1) 1 3 with
                   | Fail -> Fail
-                  | Return l2 ->
-                    begin match list_nth_shared_fwd i32 l2 0 with
+                  | Return ls ->
+                    begin match list_nth_shared_fwd i32 ls 0 with
                     | Fail -> Fail
                     | Return i3 ->
                       if not (i3 = 0)
                       then Fail
                       else
-                        begin match list_nth_shared_fwd i32 l2 1 with
+                        begin match list_nth_shared_fwd i32 ls 1 with
                         | Fail -> Fail
                         | Return i4 ->
                           if not (i4 = 3)
                           then Fail
                           else
-                            begin match list_nth_shared_fwd i32 l2 2 with
+                            begin match list_nth_shared_fwd i32 ls 2 with
                             | Fail -> Fail
                             | Return i5 ->
                               if not (i5 = 2) then Fail else Return ()
diff --git a/tests/misc/Paper.fst b/tests/misc/Paper.fst
index a6ec184c..205227be 100644
--- a/tests/misc/Paper.fst
+++ b/tests/misc/Paper.fst
@@ -13,7 +13,7 @@ let ref_incr_fwd_back (x : i32) : result i32 =
 let test_incr_fwd : result unit =
   begin match ref_incr_fwd_back 0 with
   | Fail -> Fail
-  | Return i -> if not (i = 1) then Fail else Return ()
+  | Return x -> if not (x = 1) then Fail else Return ()
   end
 
 (** Unit test for [paper::test_incr] *)
@@ -41,10 +41,8 @@ let test_choose_fwd : result unit =
       else
         begin match choose_back i32 true 0 0 z0 with
         | Fail -> Fail
-        | Return (i, i0) ->
-          if not (i = 1)
-          then Fail
-          else if not (i0 = 0) then Fail else Return ()
+        | Return (x, y) ->
+          if not (x = 1) then Fail else if not (y = 0) then Fail else Return ()
         end
     end
   end
@@ -89,7 +87,7 @@ let rec list_nth_mut_back
       | Return i0 ->
         begin match list_nth_mut_back t tl i0 ret with
         | Fail -> Fail
-        | Return l0 -> Return (ListCons x l0)
+        | Return tl0 -> Return (ListCons x tl0)
         end
       end
     end
@@ -144,7 +142,7 @@ let call_choose_fwd (p : (u32 & u32)) : result u32 =
     | Return pz0 ->
       begin match choose_back u32 true px py pz0 with
       | Fail -> Fail
-      | Return (i, _) -> Return i
+      | Return (px0, _) -> Return px0
       end
     end
   end