3 files changed, 17 insertions, 24 deletions
diff --git a/tests/fstar-split/misc/External.Funs.fst b/tests/fstar-split/misc/External.Funs.fst
index 3b84697e..65382549 100644
--- a/tests/fstar-split/misc/External.Funs.fst
+++ b/tests/fstar-split/misc/External.Funs.fst
@@ -36,9 +36,7 @@ let test_new_non_zero_u32
 (** [external::test_vec]: forward function
     Source: 'src/external.rs', lines 17:0-17:17 *)
 let test_vec : result unit =
-  let v = alloc_vec_Vec_new u32 in
-  let* _ = alloc_vec_Vec_push u32 v 0 in
-  Return ()
+  let* _ = alloc_vec_Vec_push u32 (alloc_vec_Vec_new u32) 0 in Return ()
 
 (** Unit test for [external::test_vec] *)
 let _ = assert_norm (test_vec = Return ())
diff --git a/tests/fstar-split/misc/NoNestedBorrows.fst b/tests/fstar-split/misc/NoNestedBorrows.fst
index 41bb7a06..53e1d300 100644
--- a/tests/fstar-split/misc/NoNestedBorrows.fst
+++ b/tests/fstar-split/misc/NoNestedBorrows.fst
@@ -220,9 +220,8 @@ let _ = assert_norm (test_list1 = Return ())
 (** [no_nested_borrows::test_box1]: forward function
     Source: 'src/no_nested_borrows.rs', lines 208:0-208:18 *)
 let test_box1 : result unit =
-  let b = 0 in
-  let* b1 = alloc_boxed_Box_deref_mut_back i32 b 1 in
-  let* x = alloc_boxed_Box_deref i32 b1 in
+  let* b = alloc_boxed_Box_deref_mut_back i32 0 1 in
+  let* x = alloc_boxed_Box_deref i32 b in
   if not (x = 1) then Fail Failure else Return ()
 
 (** Unit test for [no_nested_borrows::test_box1] *)
@@ -262,8 +261,7 @@ let is_cons (t : Type0) (l : list_t t) : result bool =
 (** [no_nested_borrows::test_is_cons]: forward function
     Source: 'src/no_nested_borrows.rs', lines 253:0-253:21 *)
 let test_is_cons : result unit =
-  let l = List_Nil in
-  let* b = is_cons i32 (List_Cons 0 l) in
+  let* b = is_cons i32 (List_Cons 0 List_Nil) in
   if not b then Fail Failure else Return ()
 
 (** Unit test for [no_nested_borrows::test_is_cons] *)
@@ -280,8 +278,7 @@ let split_list (t : Type0) (l : list_t t) : result (t & (list_t t)) =
 (** [no_nested_borrows::test_split_list]: forward function
     Source: 'src/no_nested_borrows.rs', lines 267:0-267:24 *)
 let test_split_list : result unit =
-  let l = List_Nil in
-  let* p = split_list i32 (List_Cons 0 l) in
+  let* p = split_list i32 (List_Cons 0 List_Nil) in
   let (hd, _) = p in
   if not (hd = 0) then Fail Failure else Return ()
 
@@ -393,26 +390,25 @@ let list_rev (t : Type0) (l : list_t t) : result (list_t t) =
 (** [no_nested_borrows::test_list_functions]: forward function
     Source: 'src/no_nested_borrows.rs', lines 398:0-398:28 *)
 let test_list_functions : result unit =
-  let l = List_Nil in
-  let l1 = List_Cons 2 l in
-  let l2 = List_Cons 1 l1 in
-  let* i = list_length i32 (List_Cons 0 l2) in
+  let l = List_Cons 2 List_Nil in
+  let l1 = List_Cons 1 l in
+  let* i = list_length i32 (List_Cons 0 l1) in
   if not (i = 3)
   then Fail Failure
   else
-    let* i1 = list_nth_shared i32 (List_Cons 0 l2) 0 in
+    let* i1 = list_nth_shared i32 (List_Cons 0 l1) 0 in
     if not (i1 = 0)
     then Fail Failure
     else
-      let* i2 = list_nth_shared i32 (List_Cons 0 l2) 1 in
+      let* i2 = list_nth_shared i32 (List_Cons 0 l1) 1 in
       if not (i2 = 1)
       then Fail Failure
       else
-        let* i3 = list_nth_shared i32 (List_Cons 0 l2) 2 in
+        let* i3 = list_nth_shared i32 (List_Cons 0 l1) 2 in
         if not (i3 = 2)
         then Fail Failure
         else
-          let* ls = list_nth_mut_back i32 (List_Cons 0 l2) 1 3 in
+          let* ls = list_nth_mut_back i32 (List_Cons 0 l1) 1 3 in
           let* i4 = list_nth_shared i32 ls 0 in
           if not (i4 = 0)
           then Fail Failure
diff --git a/tests/fstar-split/misc/Paper.fst b/tests/fstar-split/misc/Paper.fst
index 2dc804de..0c44d78b 100644
--- a/tests/fstar-split/misc/Paper.fst
+++ b/tests/fstar-split/misc/Paper.fst
@@ -87,13 +87,12 @@ let rec sum (l : list_t i32) : result i32 =
 (** [paper::test_nth]: forward function
     Source: 'src/paper.rs', lines 68:0-68:17 *)
 let test_nth : result unit =
-  let l = List_Nil in
-  let l1 = List_Cons 3 l in
-  let l2 = List_Cons 2 l1 in
-  let* x = list_nth_mut i32 (List_Cons 1 l2) 2 in
+  let l = List_Cons 3 List_Nil in
+  let l1 = List_Cons 2 l in
+  let* x = list_nth_mut i32 (List_Cons 1 l1) 2 in
   let* x1 = i32_add x 1 in
-  let* l3 = list_nth_mut_back i32 (List_Cons 1 l2) 2 x1 in
-  let* i = sum l3 in
+  let* l2 = list_nth_mut_back i32 (List_Cons 1 l1) 2 x1 in
+  let* i = sum l2 in
   if not (i = 7) then Fail Failure else Return ()
 
 (** Unit test for [paper::test_nth] *)