Regenerate the test files

4 files changed, 15 insertions, 19 deletions

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