From 63694b5d29c9f54b0d8a386474dd8551889197cc Mon Sep 17 00:00:00 2001
From: Son Ho <hosonmarc@gmail.com>
Date: Wed, 27 Nov 2024 15:44:07 +0000
Subject: [PATCH] Regenerate the tests

---
 tests/coq/arrays/Arrays.v            |   3 +-
 tests/coq/hashmap/Hashmap_Funs.v     |  48 ++++-----
 tests/coq/misc/AdtBorrows.v          |  31 +++---
 tests/coq/misc/NoNestedBorrows.v     | 112 ++++++++-------------
 tests/coq/misc/Paper.v               |  15 ++-
 tests/fstar/arrays/Arrays.Funs.fst   |   3 +-
 tests/fstar/hashmap/Hashmap.Funs.fst |  44 ++++-----
 tests/fstar/misc/AdtBorrows.fst      |  19 ++--
 tests/fstar/misc/NoNestedBorrows.fst |  99 ++++++++-----------
 tests/fstar/misc/Paper.fst           |  13 ++-
 tests/lean/AdtBorrows.lean           |  33 ++-----
 tests/lean/Arrays.lean               |   6 +-
 tests/lean/Hashmap/Funs.lean         |  48 +++------
 tests/lean/NoNestedBorrows.lean      | 143 ++++++++-------------------
 tests/lean/Paper.lean                |  21 ++--
 15 files changed, 234 insertions(+), 404 deletions(-)

diff --git a/tests/coq/arrays/Arrays.v b/tests/coq/arrays/Arrays.v
index c2308943f..8cca932bc 100644
--- a/tests/coq/arrays/Arrays.v
+++ b/tests/coq/arrays/Arrays.v
@@ -428,7 +428,8 @@ Fixpoint sum2_loop
 Definition sum2 (n : nat) (s : slice u32) (s2 : slice u32) : result u32 :=
   let i := slice_len s in
   let i1 := slice_len s2 in
-  if i s= i1 then sum2_loop n s s2 0%u32 0%usize else Fail_ Failure
+  _ <- massert (i s= i1);
+  sum2_loop n s s2 0%u32 0%usize
 .
 
 (** [arrays::f0]:
diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v
index e3202892f..4ff7553f6 100644
--- a/tests/coq/hashmap/Hashmap_Funs.v
+++ b/tests/coq/hashmap/Hashmap_Funs.v
@@ -543,35 +543,25 @@ Definition test1 (n : nat) : result unit :=
   hm3 <- hashMap_insert n hm2 1024%usize 138%u64;
   hm4 <- hashMap_insert n hm3 1056%usize 256%u64;
   i <- hashMap_get n hm4 128%usize;
-  if i s= 18%u64
-  then (
-    p <- hashMap_get_mut n hm4 1024%usize;
-    let (_, get_mut_back) := p in
-    let hm5 := get_mut_back 56%u64 in
-    i1 <- hashMap_get n hm5 1024%usize;
-    if i1 s= 56%u64
-    then (
-      p1 <- hashMap_remove n hm5 1024%usize;
-      let (x, hm6) := p1 in
-      match x with
-      | None => Fail_ Failure
-      | Some x1 =>
-        if x1 s= 56%u64
-        then (
-          i2 <- hashMap_get n hm6 0%usize;
-          if i2 s= 42%u64
-          then (
-            i3 <- hashMap_get n hm6 128%usize;
-            if i3 s= 18%u64
-            then (
-              i4 <- hashMap_get n hm6 1056%usize;
-              if i4 s= 256%u64 then Ok tt else Fail_ Failure)
-            else Fail_ Failure)
-          else Fail_ Failure)
-        else Fail_ Failure
-      end)
-    else Fail_ Failure)
-  else Fail_ Failure
+  _ <- massert (i s= 18%u64);
+  p <- hashMap_get_mut n hm4 1024%usize;
+  let (_, get_mut_back) := p in
+  let hm5 := get_mut_back 56%u64 in
+  i1 <- hashMap_get n hm5 1024%usize;
+  _ <- massert (i1 s= 56%u64);
+  p1 <- hashMap_remove n hm5 1024%usize;
+  let (x, hm6) := p1 in
+  match x with
+  | None => Fail_ Failure
+  | Some x1 =>
+    _ <- massert (x1 s= 56%u64);
+    i2 <- hashMap_get n hm6 0%usize;
+    _ <- massert (i2 s= 42%u64);
+    i3 <- hashMap_get n hm6 128%usize;
+    _ <- massert (i3 s= 18%u64);
+    i4 <- hashMap_get n hm6 1056%usize;
+    massert (i4 s= 256%u64)
+  end
 .
 
 End Hashmap_Funs.
diff --git a/tests/coq/misc/AdtBorrows.v b/tests/coq/misc/AdtBorrows.v
index c648ec79e..75ad9ebe5 100644
--- a/tests/coq/misc/AdtBorrows.v
+++ b/tests/coq/misc/AdtBorrows.v
@@ -31,7 +31,7 @@ Definition sharedWrapper_unwrap
 Definition use_shared_wrapper : result unit :=
   w <- sharedWrapper_create 0%i32;
   p <- sharedWrapper_unwrap w;
-  if 0%i32 s= p then Ok tt else Fail_ Failure
+  massert (0%i32 s= p)
 .
 
 (** [adt_borrows::SharedWrapper1]
@@ -64,7 +64,7 @@ Definition sharedWrapper1_unwrap
 Definition use_shared_wrapper1 : result unit :=
   w <- sharedWrapper1_create 0%i32;
   p <- sharedWrapper1_unwrap w;
-  if 0%i32 s= p then Ok tt else Fail_ Failure
+  massert (0%i32 s= p)
 .
 
 (** [adt_borrows::SharedWrapper2]
@@ -99,9 +99,8 @@ Definition use_shared_wrapper2 : result unit :=
   w <- sharedWrapper2_create 0%i32 1%i32;
   p <- sharedWrapper2_unwrap w;
   let (px, py) := p in
-  if 0%i32 s= px
-  then if 1%i32 s= py then Ok tt else Fail_ Failure
-  else Fail_ Failure
+  _ <- massert (0%i32 s= px);
+  massert (1%i32 s= py)
 .
 
 (** [adt_borrows::MutWrapper]
@@ -131,7 +130,7 @@ Definition use_mut_wrapper : result unit :=
   let (p2, unwrap_back) := p1 in
   p3 <- i32_add p2 1%i32;
   let x := create_back (unwrap_back p3) in
-  if x s= 1%i32 then Ok tt else Fail_ Failure
+  massert (x s= 1%i32)
 .
 
 (** [adt_borrows::MutWrapper1]
@@ -166,7 +165,7 @@ Definition use_mut_wrapper1 : result unit :=
   let (p2, unwrap_back) := p1 in
   p3 <- i32_add p2 1%i32;
   let x := create_back (unwrap_back p3) in
-  if x s= 1%i32 then Ok tt else Fail_ Failure
+  massert (x s= 1%i32)
 .
 
 (** [adt_borrows::MutWrapper2]
@@ -223,16 +222,14 @@ Definition use_mut_wrapper2 : result unit :=
         mutWrapper2_x := (unwrap_back px1).(mutWrapper2_x);
         mutWrapper2_y := w.(mutWrapper2_y)
       |} in
-  if x s= 1%i32
-  then
-    let y :=
-      create_back1
-        {|
-          mutWrapper2_x := w.(mutWrapper2_x);
-          mutWrapper2_y := (unwrap_back1 py1).(mutWrapper2_y)
-        |} in
-    if y s= 11%i32 then Ok tt else Fail_ Failure
-  else Fail_ Failure
+  _ <- massert (x s= 1%i32);
+  let y :=
+    create_back1
+      {|
+        mutWrapper2_x := w.(mutWrapper2_x);
+        mutWrapper2_y := (unwrap_back1 py1).(mutWrapper2_y)
+      |} in
+  massert (y s= 11%i32)
 .
 
 End AdtBorrows.
diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v
index 1c5dc7322..39027a337 100644
--- a/tests/coq/misc/NoNestedBorrows.v
+++ b/tests/coq/misc/NoNestedBorrows.v
@@ -93,7 +93,7 @@ Definition test3 : result unit :=
   x <- get_max 4%u32 3%u32;
   y <- get_max 10%u32 11%u32;
   z <- u32_add x y;
-  if z s= 15%u32 then Ok tt else Fail_ Failure
+  massert (z s= 15%u32)
 .
 
 (** Unit test for [no_nested_borrows::test3] *)
@@ -102,7 +102,7 @@ Check (test3)%return.
 (** [no_nested_borrows::test_neg1]:
     Source: 'tests/src/no_nested_borrows.rs', lines 90:0-94:1 *)
 Definition test_neg1 : result unit :=
-  y <- i32_neg 3%i32; if y s= (-3)%i32 then Ok tt else Fail_ Failure
+  y <- i32_neg 3%i32; massert (y s= (-3)%i32)
 .
 
 (** Unit test for [no_nested_borrows::test_neg1] *)
@@ -111,8 +111,7 @@ Check (test_neg1)%return.
 (** [no_nested_borrows::refs_test1]:
     Source: 'tests/src/no_nested_borrows.rs', lines 97:0-106:1 *)
 Definition refs_test1 : result unit :=
-  if 1%i32 s= 1%i32 then Ok tt else Fail_ Failure
-.
+  massert (1%i32 s= 1%i32).
 
 (** Unit test for [no_nested_borrows::refs_test1] *)
 Check (refs_test1)%return.
@@ -120,15 +119,10 @@ Check (refs_test1)%return.
 (** [no_nested_borrows::refs_test2]:
     Source: 'tests/src/no_nested_borrows.rs', lines 108:0-120:1 *)
 Definition refs_test2 : result unit :=
-  if 2%i32 s= 2%i32
-  then
-    if 0%i32 s= 0%i32
-    then
-      if 2%i32 s= 2%i32
-      then if 2%i32 s= 2%i32 then Ok tt else Fail_ Failure
-      else Fail_ Failure
-    else Fail_ Failure
-  else Fail_ Failure
+  _ <- massert (2%i32 s= 2%i32);
+  _ <- massert (0%i32 s= 0%i32);
+  _ <- massert (2%i32 s= 2%i32);
+  massert (2%i32 s= 2%i32)
 .
 
 (** Unit test for [no_nested_borrows::refs_test2] *)
@@ -149,7 +143,7 @@ Definition test_box1 : result unit :=
   let (_, deref_mut_back) := p in
   let b := deref_mut_back 1%i32 in
   x <- alloc_boxed_Box_deref b;
-  if x s= 1%i32 then Ok tt else Fail_ Failure
+  massert (x s= 1%i32)
 .
 
 (** Unit test for [no_nested_borrows::test_box1] *)
@@ -181,7 +175,7 @@ Definition test_panic_msg (b : bool) : result unit :=
 (** [no_nested_borrows::test_copy_int]:
     Source: 'tests/src/no_nested_borrows.rs', lines 167:0-172:1 *)
 Definition test_copy_int : result unit :=
-  y <- copy_int 0%i32; if 0%i32 s= y then Ok tt else Fail_ Failure
+  y <- copy_int 0%i32; massert (0%i32 s= y)
 .
 
 (** Unit test for [no_nested_borrows::test_copy_int] *)
@@ -196,7 +190,7 @@ Definition is_cons {T : Type} (l : List_t T) : result bool :=
 (** [no_nested_borrows::test_is_cons]:
     Source: 'tests/src/no_nested_borrows.rs', lines 181:0-185:1 *)
 Definition test_is_cons : result unit :=
-  b <- is_cons (List_Cons 0%i32 List_Nil); if b then Ok tt else Fail_ Failure
+  b <- is_cons (List_Cons 0%i32 List_Nil); massert b
 .
 
 (** Unit test for [no_nested_borrows::test_is_cons] *)
@@ -213,7 +207,7 @@ Definition split_list {T : Type} (l : List_t T) : result (T * (List_t T)) :=
 Definition test_split_list : result unit :=
   p <- split_list (List_Cons 0%i32 List_Nil);
   let (hd, _) := p in
-  if hd s= 0%i32 then Ok tt else Fail_ Failure
+  massert (hd s= 0%i32)
 .
 
 (** Unit test for [no_nested_borrows::test_split_list] *)
@@ -234,13 +228,10 @@ Definition choose_test : result unit :=
   p <- choose true 0%i32 0%i32;
   let (z, choose_back) := p in
   z1 <- i32_add z 1%i32;
-  if z1 s= 1%i32
-  then
-    let (x, y) := choose_back z1 in
-    if x s= 1%i32
-    then if y s= 0%i32 then Ok tt else Fail_ Failure
-    else Fail_ Failure
-  else Fail_ Failure
+  _ <- massert (z1 s= 1%i32);
+  let (x, y) := choose_back z1 in
+  _ <- massert (x s= 1%i32);
+  massert (y s= 0%i32)
 .
 
 (** Unit test for [no_nested_borrows::choose_test] *)
@@ -335,34 +326,22 @@ Definition test_list_functions : result unit :=
   let l := List_Cons 2%i32 List_Nil in
   let l1 := List_Cons 1%i32 l in
   i <- list_length (List_Cons 0%i32 l1);
-  if i s= 3%u32
-  then (
-    i1 <- list_nth_shared (List_Cons 0%i32 l1) 0%u32;
-    if i1 s= 0%i32
-    then (
-      i2 <- list_nth_shared (List_Cons 0%i32 l1) 1%u32;
-      if i2 s= 1%i32
-      then (
-        i3 <- list_nth_shared (List_Cons 0%i32 l1) 2%u32;
-        if i3 s= 2%i32
-        then (
-          p <- list_nth_mut (List_Cons 0%i32 l1) 1%u32;
-          let (_, list_nth_mut_back) := p in
-          let ls := list_nth_mut_back 3%i32 in
-          i4 <- list_nth_shared ls 0%u32;
-          if i4 s= 0%i32
-          then (
-            i5 <- list_nth_shared ls 1%u32;
-            if i5 s= 3%i32
-            then (
-              i6 <- list_nth_shared ls 2%u32;
-              if i6 s= 2%i32 then Ok tt else Fail_ Failure)
-            else Fail_ Failure)
-          else Fail_ Failure)
-        else Fail_ Failure)
-      else Fail_ Failure)
-    else Fail_ Failure)
-  else Fail_ Failure
+  _ <- massert (i s= 3%u32);
+  i1 <- list_nth_shared (List_Cons 0%i32 l1) 0%u32;
+  _ <- massert (i1 s= 0%i32);
+  i2 <- list_nth_shared (List_Cons 0%i32 l1) 1%u32;
+  _ <- massert (i2 s= 1%i32);
+  i3 <- list_nth_shared (List_Cons 0%i32 l1) 2%u32;
+  _ <- massert (i3 s= 2%i32);
+  p <- list_nth_mut (List_Cons 0%i32 l1) 1%u32;
+  let (_, list_nth_mut_back) := p in
+  let ls := list_nth_mut_back 3%i32 in
+  i4 <- list_nth_shared ls 0%u32;
+  _ <- massert (i4 s= 0%i32);
+  i5 <- list_nth_shared ls 1%u32;
+  _ <- massert (i5 s= 3%i32);
+  i6 <- list_nth_shared ls 2%u32;
+  massert (i6 s= 2%i32)
 .
 
 (** Unit test for [no_nested_borrows::test_list_functions] *)
@@ -459,23 +438,15 @@ Definition new_pair1 : result (StructWithPair_t u32 u32) :=
 Definition test_constants : result unit :=
   swt <- new_tuple1;
   let (i, _) := swt.(structWithTuple_p) in
-  if i s= 1%u32
-  then (
-    swt1 <- new_tuple2;
-    let (i1, _) := swt1.(structWithTuple_p) in
-    if i1 s= 1%i16
-    then (
-      swt2 <- new_tuple3;
-      let (i2, _) := swt2.(structWithTuple_p) in
-      if i2 s= 1%u64
-      then (
-        swp <- new_pair1;
-        if swp.(structWithPair_p).(pair_x) s= 1%u32
-        then Ok tt
-        else Fail_ Failure)
-      else Fail_ Failure)
-    else Fail_ Failure)
-  else Fail_ Failure
+  _ <- massert (i s= 1%u32);
+  swt1 <- new_tuple2;
+  let (i1, _) := swt1.(structWithTuple_p) in
+  _ <- massert (i1 s= 1%i16);
+  swt2 <- new_tuple3;
+  let (i2, _) := swt2.(structWithTuple_p) in
+  _ <- massert (i2 s= 1%u64);
+  swp <- new_pair1;
+  massert (swp.(structWithPair_p).(pair_x) s= 1%u32)
 .
 
 (** Unit test for [no_nested_borrows::test_constants] *)
@@ -493,7 +464,8 @@ Check (test_weird_borrows1)%return.
     Source: 'tests/src/no_nested_borrows.rs', lines 414:0-418:1 *)
 Definition test_mem_replace (px : u32) : result u32 :=
   let (y, _) := core_mem_replace px 1%u32 in
-  if y s= 0%u32 then Ok 2%u32 else Fail_ Failure
+  _ <- massert (y s= 0%u32);
+  Ok 2%u32
 .
 
 (** [no_nested_borrows::test_shared_borrow_bool1]:
diff --git a/tests/coq/misc/Paper.v b/tests/coq/misc/Paper.v
index 65730b3ac..1d6b44fc3 100644
--- a/tests/coq/misc/Paper.v
+++ b/tests/coq/misc/Paper.v
@@ -16,7 +16,7 @@ Definition ref_incr (x : i32) : result i32 :=
 (** [paper::test_incr]:
     Source: 'tests/src/paper.rs', lines 11:0-15:1 *)
 Definition test_incr : result unit :=
-  x <- ref_incr 0%i32; if x s= 1%i32 then Ok tt else Fail_ Failure
+  x <- ref_incr 0%i32; massert (x s= 1%i32)
 .
 
 (** Unit test for [paper::test_incr] *)
@@ -37,13 +37,10 @@ Definition test_choose : result unit :=
   p <- choose true 0%i32 0%i32;
   let (z, choose_back) := p in
   z1 <- i32_add z 1%i32;
-  if z1 s= 1%i32
-  then
-    let (x, y) := choose_back z1 in
-    if x s= 1%i32
-    then if y s= 0%i32 then Ok tt else Fail_ Failure
-    else Fail_ Failure
-  else Fail_ Failure
+  _ <- massert (z1 s= 1%i32);
+  let (x, y) := choose_back z1 in
+  _ <- massert (x s= 1%i32);
+  massert (y s= 0%i32)
 .
 
 (** Unit test for [paper::test_choose] *)
@@ -97,7 +94,7 @@ Definition test_nth : result unit :=
   x1 <- i32_add x 1%i32;
   let l2 := list_nth_mut_back x1 in
   i <- sum l2;
-  if i s= 7%i32 then Ok tt else Fail_ Failure
+  massert (i s= 7%i32)
 .
 
 (** Unit test for [paper::test_nth] *)
diff --git a/tests/fstar/arrays/Arrays.Funs.fst b/tests/fstar/arrays/Arrays.Funs.fst
index 7052d1cf7..fa63dcc9e 100644
--- a/tests/fstar/arrays/Arrays.Funs.fst
+++ b/tests/fstar/arrays/Arrays.Funs.fst
@@ -343,7 +343,8 @@ let rec sum2_loop
 let sum2 (s : slice u32) (s2 : slice u32) : result u32 =
   let i = slice_len s in
   let i1 = slice_len s2 in
-  if i = i1 then sum2_loop s s2 0 0 else Fail Failure
+  let* _ = massert (i = i1) in
+  sum2_loop s s2 0 0
 
 (** [arrays::f0]:
     Source: 'tests/src/arrays.rs', lines 274:0-277:1 *)
diff --git a/tests/fstar/hashmap/Hashmap.Funs.fst b/tests/fstar/hashmap/Hashmap.Funs.fst
index 26edb6a83..4e7627ed4 100644
--- a/tests/fstar/hashmap/Hashmap.Funs.fst
+++ b/tests/fstar/hashmap/Hashmap.Funs.fst
@@ -385,31 +385,21 @@ let test1 : result unit =
   let* hm3 = hashMap_insert hm2 1024 138 in
   let* hm4 = hashMap_insert hm3 1056 256 in
   let* i = hashMap_get hm4 128 in
-  if i = 18
-  then
-    let* (_, get_mut_back) = hashMap_get_mut hm4 1024 in
-    let hm5 = get_mut_back 56 in
-    let* i1 = hashMap_get hm5 1024 in
-    if i1 = 56
-    then
-      let* (x, hm6) = hashMap_remove hm5 1024 in
-      begin match x with
-      | None -> Fail Failure
-      | Some x1 ->
-        if x1 = 56
-        then
-          let* i2 = hashMap_get hm6 0 in
-          if i2 = 42
-          then
-            let* i3 = hashMap_get hm6 128 in
-            if i3 = 18
-            then
-              let* i4 = hashMap_get hm6 1056 in
-              if i4 = 256 then Ok () else Fail Failure
-            else Fail Failure
-          else Fail Failure
-        else Fail Failure
-      end
-    else Fail Failure
-  else Fail Failure
+  let* _ = massert (i = 18) in
+  let* (_, get_mut_back) = hashMap_get_mut hm4 1024 in
+  let hm5 = get_mut_back 56 in
+  let* i1 = hashMap_get hm5 1024 in
+  let* _ = massert (i1 = 56) in
+  let* (x, hm6) = hashMap_remove hm5 1024 in
+  begin match x with
+  | None -> Fail Failure
+  | Some x1 ->
+    let* _ = massert (x1 = 56) in
+    let* i2 = hashMap_get hm6 0 in
+    let* _ = massert (i2 = 42) in
+    let* i3 = hashMap_get hm6 128 in
+    let* _ = massert (i3 = 18) in
+    let* i4 = hashMap_get hm6 1056 in
+    massert (i4 = 256)
+  end
 
diff --git a/tests/fstar/misc/AdtBorrows.fst b/tests/fstar/misc/AdtBorrows.fst
index 9fadfa49d..12fb7a530 100644
--- a/tests/fstar/misc/AdtBorrows.fst
+++ b/tests/fstar/misc/AdtBorrows.fst
@@ -24,7 +24,7 @@ let sharedWrapper_unwrap (#t : Type0) (self : sharedWrapper_t t) : result t =
 let use_shared_wrapper : result unit =
   let* w = sharedWrapper_create 0 in
   let* p = sharedWrapper_unwrap w in
-  if 0 = p then Ok () else Fail Failure
+  massert (0 = p)
 
 (** [adt_borrows::SharedWrapper1]
     Source: 'tests/src/adt-borrows.rs', lines 23:0-25:1 *)
@@ -45,7 +45,7 @@ let sharedWrapper1_unwrap (#t : Type0) (self : sharedWrapper1_t t) : result t =
 let use_shared_wrapper1 : result unit =
   let* w = sharedWrapper1_create 0 in
   let* p = sharedWrapper1_unwrap w in
-  if 0 = p then Ok () else Fail Failure
+  massert (0 = p)
 
 (** [adt_borrows::SharedWrapper2]
     Source: 'tests/src/adt-borrows.rs', lines 44:0-47:1 *)
@@ -69,7 +69,8 @@ let use_shared_wrapper2 : result unit =
   let* w = sharedWrapper2_create 0 1 in
   let* p = sharedWrapper2_unwrap w in
   let (px, py) = p in
-  if 0 = px then if 1 = py then Ok () else Fail Failure else Fail Failure
+  let* _ = massert (0 = px) in
+  massert (1 = py)
 
 (** [adt_borrows::MutWrapper]
     Source: 'tests/src/adt-borrows.rs', lines 68:0-68:36 *)
@@ -94,7 +95,7 @@ let use_mut_wrapper : result unit =
   let* (p, unwrap_back) = mutWrapper_unwrap w in
   let* p1 = i32_add p 1 in
   let x = create_back (unwrap_back p1) in
-  if x = 1 then Ok () else Fail Failure
+  massert (x = 1)
 
 (** [adt_borrows::MutWrapper1]
     Source: 'tests/src/adt-borrows.rs', lines 88:0-90:1 *)
@@ -119,7 +120,7 @@ let use_mut_wrapper1 : result unit =
   let* (p, unwrap_back) = mutWrapper1_unwrap w in
   let* p1 = i32_add p 1 in
   let x = create_back (unwrap_back p1) in
-  if x = 1 then Ok () else Fail Failure
+  massert (x = 1)
 
 (** [adt_borrows::MutWrapper2]
     Source: 'tests/src/adt-borrows.rs', lines 110:0-113:1 *)
@@ -154,9 +155,7 @@ let use_mut_wrapper2 : result unit =
   let* px1 = i32_add px 1 in
   let* py1 = i32_add py 1 in
   let x = create_back { w with x = (unwrap_back px1).x } in
-  if x = 1
-  then
-    let y = create_back1 { w with y = (unwrap_back1 py1).y } in
-    if y = 11 then Ok () else Fail Failure
-  else Fail Failure
+  let* _ = massert (x = 1) in
+  let y = create_back1 { w with y = (unwrap_back1 py1).y } in
+  massert (y = 11)
 
diff --git a/tests/fstar/misc/NoNestedBorrows.fst b/tests/fstar/misc/NoNestedBorrows.fst
index 73e1d4183..47a06c854 100644
--- a/tests/fstar/misc/NoNestedBorrows.fst
+++ b/tests/fstar/misc/NoNestedBorrows.fst
@@ -71,7 +71,7 @@ let test3 : result unit =
   let* x = get_max 4 3 in
   let* y = get_max 10 11 in
   let* z = u32_add x y in
-  if z = 15 then Ok () else Fail Failure
+  massert (z = 15)
 
 (** Unit test for [no_nested_borrows::test3] *)
 let _ = assert_norm (test3 = Ok ())
@@ -79,7 +79,7 @@ let _ = assert_norm (test3 = Ok ())
 (** [no_nested_borrows::test_neg1]:
     Source: 'tests/src/no_nested_borrows.rs', lines 90:0-94:1 *)
 let test_neg1 : result unit =
-  let* y = i32_neg 3 in if y = -3 then Ok () else Fail Failure
+  let* y = i32_neg 3 in massert (y = -3)
 
 (** Unit test for [no_nested_borrows::test_neg1] *)
 let _ = assert_norm (test_neg1 = Ok ())
@@ -87,7 +87,7 @@ let _ = assert_norm (test_neg1 = Ok ())
 (** [no_nested_borrows::refs_test1]:
     Source: 'tests/src/no_nested_borrows.rs', lines 97:0-106:1 *)
 let refs_test1 : result unit =
-  if 1 = 1 then Ok () else Fail Failure
+  massert (1 = 1)
 
 (** Unit test for [no_nested_borrows::refs_test1] *)
 let _ = assert_norm (refs_test1 = Ok ())
@@ -95,12 +95,10 @@ let _ = assert_norm (refs_test1 = Ok ())
 (** [no_nested_borrows::refs_test2]:
     Source: 'tests/src/no_nested_borrows.rs', lines 108:0-120:1 *)
 let refs_test2 : result unit =
-  if 2 = 2
-  then
-    if 0 = 0
-    then if 2 = 2 then if 2 = 2 then Ok () else Fail Failure else Fail Failure
-    else Fail Failure
-  else Fail Failure
+  let* _ = massert (2 = 2) in
+  let* _ = massert (0 = 0) in
+  let* _ = massert (2 = 2) in
+  massert (2 = 2)
 
 (** Unit test for [no_nested_borrows::refs_test2] *)
 let _ = assert_norm (refs_test2 = Ok ())
@@ -119,7 +117,7 @@ let test_box1 : result unit =
   let* (_, deref_mut_back) = alloc_boxed_Box_deref_mut 0 in
   let b = deref_mut_back 1 in
   let* x = alloc_boxed_Box_deref b in
-  if x = 1 then Ok () else Fail Failure
+  massert (x = 1)
 
 (** Unit test for [no_nested_borrows::test_box1] *)
 let _ = assert_norm (test_box1 = Ok ())
@@ -147,7 +145,7 @@ let test_panic_msg (b : bool) : result unit =
 (** [no_nested_borrows::test_copy_int]:
     Source: 'tests/src/no_nested_borrows.rs', lines 167:0-172:1 *)
 let test_copy_int : result unit =
-  let* y = copy_int 0 in if 0 = y then Ok () else Fail Failure
+  let* y = copy_int 0 in massert (0 = y)
 
 (** Unit test for [no_nested_borrows::test_copy_int] *)
 let _ = assert_norm (test_copy_int = Ok ())
@@ -160,7 +158,7 @@ let is_cons (#t : Type0) (l : list_t t) : result bool =
 (** [no_nested_borrows::test_is_cons]:
     Source: 'tests/src/no_nested_borrows.rs', lines 181:0-185:1 *)
 let test_is_cons : result unit =
-  let* b = is_cons (List_Cons 0 List_Nil) in if b then Ok () else Fail Failure
+  let* b = is_cons (List_Cons 0 List_Nil) in massert b
 
 (** Unit test for [no_nested_borrows::test_is_cons] *)
 let _ = assert_norm (test_is_cons = Ok ())
@@ -178,7 +176,7 @@ let split_list (#t : Type0) (l : list_t t) : result (t & (list_t t)) =
 let test_split_list : result unit =
   let* p = split_list (List_Cons 0 List_Nil) in
   let (hd, _) = p in
-  if hd = 0 then Ok () else Fail Failure
+  massert (hd = 0)
 
 (** Unit test for [no_nested_borrows::test_split_list] *)
 let _ = assert_norm (test_split_list = Ok ())
@@ -196,11 +194,10 @@ let choose
 let choose_test : result unit =
   let* (z, choose_back) = choose true 0 0 in
   let* z1 = i32_add z 1 in
-  if z1 = 1
-  then
-    let (x, y) = choose_back z1 in
-    if x = 1 then if y = 0 then Ok () else Fail Failure else Fail Failure
-  else Fail Failure
+  let* _ = massert (z1 = 1) in
+  let (x, y) = choose_back z1 in
+  let* _ = massert (x = 1) in
+  massert (y = 0)
 
 (** Unit test for [no_nested_borrows::choose_test] *)
 let _ = assert_norm (choose_test = Ok ())
@@ -281,33 +278,21 @@ let test_list_functions : result unit =
   let l = List_Cons 2 List_Nil in
   let l1 = List_Cons 1 l in
   let* i = list_length (List_Cons 0 l1) in
-  if i = 3
-  then
-    let* i1 = list_nth_shared (List_Cons 0 l1) 0 in
-    if i1 = 0
-    then
-      let* i2 = list_nth_shared (List_Cons 0 l1) 1 in
-      if i2 = 1
-      then
-        let* i3 = list_nth_shared (List_Cons 0 l1) 2 in
-        if i3 = 2
-        then
-          let* (_, list_nth_mut_back) = list_nth_mut (List_Cons 0 l1) 1 in
-          let ls = list_nth_mut_back 3 in
-          let* i4 = list_nth_shared ls 0 in
-          if i4 = 0
-          then
-            let* i5 = list_nth_shared ls 1 in
-            if i5 = 3
-            then
-              let* i6 = list_nth_shared ls 2 in
-              if i6 = 2 then Ok () else Fail Failure
-            else Fail Failure
-          else Fail Failure
-        else Fail Failure
-      else Fail Failure
-    else Fail Failure
-  else Fail Failure
+  let* _ = massert (i = 3) in
+  let* i1 = list_nth_shared (List_Cons 0 l1) 0 in
+  let* _ = massert (i1 = 0) in
+  let* i2 = list_nth_shared (List_Cons 0 l1) 1 in
+  let* _ = massert (i2 = 1) in
+  let* i3 = list_nth_shared (List_Cons 0 l1) 2 in
+  let* _ = massert (i3 = 2) in
+  let* (_, list_nth_mut_back) = list_nth_mut (List_Cons 0 l1) 1 in
+  let ls = list_nth_mut_back 3 in
+  let* i4 = list_nth_shared ls 0 in
+  let* _ = massert (i4 = 0) in
+  let* i5 = list_nth_shared ls 1 in
+  let* _ = massert (i5 = 3) in
+  let* i6 = list_nth_shared ls 2 in
+  massert (i6 = 2)
 
 (** Unit test for [no_nested_borrows::test_list_functions] *)
 let _ = assert_norm (test_list_functions = Ok ())
@@ -381,19 +366,15 @@ let new_pair1 : result (structWithPair_t u32 u32) =
 let test_constants : result unit =
   let* swt = new_tuple1 in
   let (i, _) = swt.p in
-  if i = 1
-  then
-    let* swt1 = new_tuple2 in
-    let (i1, _) = swt1.p in
-    if i1 = 1
-    then
-      let* swt2 = new_tuple3 in
-      let (i2, _) = swt2.p in
-      if i2 = 1
-      then let* swp = new_pair1 in if swp.p.x = 1 then Ok () else Fail Failure
-      else Fail Failure
-    else Fail Failure
-  else Fail Failure
+  let* _ = massert (i = 1) in
+  let* swt1 = new_tuple2 in
+  let (i1, _) = swt1.p in
+  let* _ = massert (i1 = 1) in
+  let* swt2 = new_tuple3 in
+  let (i2, _) = swt2.p in
+  let* _ = massert (i2 = 1) in
+  let* swp = new_pair1 in
+  massert (swp.p.x = 1)
 
 (** Unit test for [no_nested_borrows::test_constants] *)
 let _ = assert_norm (test_constants = Ok ())
@@ -409,7 +390,7 @@ let _ = assert_norm (test_weird_borrows1 = Ok ())
 (** [no_nested_borrows::test_mem_replace]:
     Source: 'tests/src/no_nested_borrows.rs', lines 414:0-418:1 *)
 let test_mem_replace (px : u32) : result u32 =
-  let (y, _) = core_mem_replace px 1 in if y = 0 then Ok 2 else Fail Failure
+  let (y, _) = core_mem_replace px 1 in let* _ = massert (y = 0) in Ok 2
 
 (** [no_nested_borrows::test_shared_borrow_bool1]:
     Source: 'tests/src/no_nested_borrows.rs', lines 421:0-430:1 *)
diff --git a/tests/fstar/misc/Paper.fst b/tests/fstar/misc/Paper.fst
index 9e029786e..80d3706a7 100644
--- a/tests/fstar/misc/Paper.fst
+++ b/tests/fstar/misc/Paper.fst
@@ -13,7 +13,7 @@ let ref_incr (x : i32) : result i32 =
 (** [paper::test_incr]:
     Source: 'tests/src/paper.rs', lines 11:0-15:1 *)
 let test_incr : result unit =
-  let* x = ref_incr 0 in if x = 1 then Ok () else Fail Failure
+  let* x = ref_incr 0 in massert (x = 1)
 
 (** Unit test for [paper::test_incr] *)
 let _ = assert_norm (test_incr = Ok ())
@@ -31,11 +31,10 @@ let choose
 let test_choose : result unit =
   let* (z, choose_back) = choose true 0 0 in
   let* z1 = i32_add z 1 in
-  if z1 = 1
-  then
-    let (x, y) = choose_back z1 in
-    if x = 1 then if y = 0 then Ok () else Fail Failure else Fail Failure
-  else Fail Failure
+  let* _ = massert (z1 = 1) in
+  let (x, y) = choose_back z1 in
+  let* _ = massert (x = 1) in
+  massert (y = 0)
 
 (** Unit test for [paper::test_choose] *)
 let _ = assert_norm (test_choose = Ok ())
@@ -80,7 +79,7 @@ let test_nth : result unit =
   let* x1 = i32_add x 1 in
   let l2 = list_nth_mut_back x1 in
   let* i = sum l2 in
-  if i = 7 then Ok () else Fail Failure
+  massert (i = 7)
 
 (** Unit test for [paper::test_nth] *)
 let _ = assert_norm (test_nth = Ok ())
diff --git a/tests/lean/AdtBorrows.lean b/tests/lean/AdtBorrows.lean
index 21aa1e2f6..6b070fb30 100644
--- a/tests/lean/AdtBorrows.lean
+++ b/tests/lean/AdtBorrows.lean
@@ -28,9 +28,7 @@ def use_shared_wrapper : Result Unit :=
   do
   let w ← SharedWrapper.create 0#i32
   let p ← SharedWrapper.unwrap w
-  if 0#i32 = p
-  then Result.ok ()
-  else Result.fail .panic
+  massert (0#i32 = p)
 
 /- [adt_borrows::SharedWrapper1]
    Source: 'tests/src/adt-borrows.rs', lines 23:0-25:1 -/
@@ -53,9 +51,7 @@ def use_shared_wrapper1 : Result Unit :=
   do
   let w ← SharedWrapper1.create 0#i32
   let p ← SharedWrapper1.unwrap w
-  if 0#i32 = p
-  then Result.ok ()
-  else Result.fail .panic
+  massert (0#i32 = p)
 
 /- [adt_borrows::SharedWrapper2]
    Source: 'tests/src/adt-borrows.rs', lines 44:0-47:1 -/
@@ -82,11 +78,8 @@ def use_shared_wrapper2 : Result Unit :=
   let w ← SharedWrapper2.create 0#i32 1#i32
   let p ← SharedWrapper2.unwrap w
   let (px, py) := p
-  if 0#i32 = px
-  then if 1#i32 = py
-       then Result.ok ()
-       else Result.fail .panic
-  else Result.fail .panic
+  let _ ← massert (0#i32 = px)
+  massert (1#i32 = py)
 
 /- [adt_borrows::MutWrapper]
    Source: 'tests/src/adt-borrows.rs', lines 68:0-68:36 -/
@@ -114,9 +107,7 @@ def use_mut_wrapper : Result Unit :=
   let (p, unwrap_back) ← MutWrapper.unwrap w
   let p1 ← p + 1#i32
   let x := create_back (unwrap_back p1)
-  if x = 1#i32
-  then Result.ok ()
-  else Result.fail .panic
+  massert (x = 1#i32)
 
 /- [adt_borrows::MutWrapper1]
    Source: 'tests/src/adt-borrows.rs', lines 88:0-90:1 -/
@@ -145,9 +136,7 @@ def use_mut_wrapper1 : Result Unit :=
   let (p, unwrap_back) ← MutWrapper1.unwrap w
   let p1 ← p + 1#i32
   let x := create_back (unwrap_back p1)
-  if x = 1#i32
-  then Result.ok ()
-  else Result.fail .panic
+  massert (x = 1#i32)
 
 /- [adt_borrows::MutWrapper2]
    Source: 'tests/src/adt-borrows.rs', lines 110:0-113:1 -/
@@ -185,12 +174,8 @@ def use_mut_wrapper2 : Result Unit :=
   let px1 ← px + 1#i32
   let py1 ← py + 1#i32
   let x := create_back { w with x := (unwrap_back px1).x }
-  if x = 1#i32
-  then
-    let y := create_back1 { w with y := (unwrap_back1 py1).y }
-    if y = 11#i32
-    then Result.ok ()
-    else Result.fail .panic
-  else Result.fail .panic
+  let _ ← massert (x = 1#i32)
+  let y := create_back1 { w with y := (unwrap_back1 py1).y }
+  massert (y = 11#i32)
 
 end adt_borrows
diff --git a/tests/lean/Arrays.lean b/tests/lean/Arrays.lean
index 1c597cecd..d9fc688dd 100644
--- a/tests/lean/Arrays.lean
+++ b/tests/lean/Arrays.lean
@@ -383,11 +383,11 @@ divergent def sum2_loop
 /- [arrays::sum2]:
    Source: 'tests/src/arrays.rs', lines 263:0-272:1 -/
 def sum2 (s : Slice U32) (s2 : Slice U32) : Result U32 :=
+  do
   let i := Slice.len s
   let i1 := Slice.len s2
-  if i = i1
-  then sum2_loop s s2 0#u32 0#usize
-  else Result.fail .panic
+  let _ ← massert (i = i1)
+  sum2_loop s s2 0#u32 0#usize
 
 /- [arrays::f0]:
    Source: 'tests/src/arrays.rs', lines 274:0-277:1 -/
diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean
index af186b5f8..3bc0ed7a3 100644
--- a/tests/lean/Hashmap/Funs.lean
+++ b/tests/lean/Hashmap/Funs.lean
@@ -395,38 +395,22 @@ def test1 : Result Unit :=
   let hm3 ← HashMap.insert hm2 1024#usize 138#u64
   let hm4 ← HashMap.insert hm3 1056#usize 256#u64
   let i ← HashMap.get hm4 128#usize
-  if i = 18#u64
-  then
+  let _ ← massert (i = 18#u64)
+  let (_, get_mut_back) ← HashMap.get_mut hm4 1024#usize
+  let hm5 := get_mut_back 56#u64
+  let i1 ← HashMap.get hm5 1024#usize
+  let _ ← massert (i1 = 56#u64)
+  let (x, hm6) ← HashMap.remove hm5 1024#usize
+  match x with
+  | none => Result.fail .panic
+  | some x1 =>
     do
-    let (_, get_mut_back) ← HashMap.get_mut hm4 1024#usize
-    let hm5 := get_mut_back 56#u64
-    let i1 ← HashMap.get hm5 1024#usize
-    if i1 = 56#u64
-    then
-      do
-      let (x, hm6) ← HashMap.remove hm5 1024#usize
-      match x with
-      | none => Result.fail .panic
-      | some x1 =>
-        if x1 = 56#u64
-        then
-          do
-          let i2 ← HashMap.get hm6 0#usize
-          if i2 = 42#u64
-          then
-            do
-            let i3 ← HashMap.get hm6 128#usize
-            if i3 = 18#u64
-            then
-              do
-              let i4 ← HashMap.get hm6 1056#usize
-              if i4 = 256#u64
-              then Result.ok ()
-              else Result.fail .panic
-            else Result.fail .panic
-          else Result.fail .panic
-        else Result.fail .panic
-    else Result.fail .panic
-  else Result.fail .panic
+    let _ ← massert (x1 = 56#u64)
+    let i2 ← HashMap.get hm6 0#usize
+    let _ ← massert (i2 = 42#u64)
+    let i3 ← HashMap.get hm6 128#usize
+    let _ ← massert (i3 = 18#u64)
+    let i4 ← HashMap.get hm6 1056#usize
+    massert (i4 = 256#u64)
 
 end hashmap
diff --git a/tests/lean/NoNestedBorrows.lean b/tests/lean/NoNestedBorrows.lean
index 363b4d066..39c761935 100644
--- a/tests/lean/NoNestedBorrows.lean
+++ b/tests/lean/NoNestedBorrows.lean
@@ -85,9 +85,7 @@ def test3 : Result Unit :=
   let x ← get_max 4#u32 3#u32
   let y ← get_max 10#u32 11#u32
   let z ← x + y
-  if z = 15#u32
-  then Result.ok ()
-  else Result.fail .panic
+  massert (z = 15#u32)
 
 /- Unit test for [no_nested_borrows::test3] -/
 #assert (test3 == Result.ok ())
@@ -97,9 +95,7 @@ def test3 : Result Unit :=
 def test_neg1 : Result Unit :=
   do
   let y ← -. 3#i32
-  if y = (-3)#i32
-  then Result.ok ()
-  else Result.fail .panic
+  massert (y = (-3)#i32)
 
 /- Unit test for [no_nested_borrows::test_neg1] -/
 #assert (test_neg1 == Result.ok ())
@@ -107,9 +103,7 @@ def test_neg1 : Result Unit :=
 /- [no_nested_borrows::refs_test1]:
    Source: 'tests/src/no_nested_borrows.rs', lines 97:0-106:1 -/
 def refs_test1 : Result Unit :=
-  if 1#i32 = 1#i32
-  then Result.ok ()
-  else Result.fail .panic
+  massert (1#i32 = 1#i32)
 
 /- Unit test for [no_nested_borrows::refs_test1] -/
 #assert (refs_test1 == Result.ok ())
@@ -117,17 +111,11 @@ def refs_test1 : Result Unit :=
 /- [no_nested_borrows::refs_test2]:
    Source: 'tests/src/no_nested_borrows.rs', lines 108:0-120:1 -/
 def refs_test2 : Result Unit :=
-  if 2#i32 = 2#i32
-  then
-    if 0#i32 = 0#i32
-    then
-      if 2#i32 = 2#i32
-      then if 2#i32 = 2#i32
-           then Result.ok ()
-           else Result.fail .panic
-      else Result.fail .panic
-    else Result.fail .panic
-  else Result.fail .panic
+  do
+  let _ ← massert (2#i32 = 2#i32)
+  let _ ← massert (0#i32 = 0#i32)
+  let _ ← massert (2#i32 = 2#i32)
+  massert (2#i32 = 2#i32)
 
 /- Unit test for [no_nested_borrows::refs_test2] -/
 #assert (refs_test2 == Result.ok ())
@@ -147,9 +135,7 @@ def test_box1 : Result Unit :=
   let (_, deref_mut_back) ← alloc.boxed.Box.deref_mut 0#i32
   let b := deref_mut_back 1#i32
   let x ← alloc.boxed.Box.deref b
-  if x = 1#i32
-  then Result.ok ()
-  else Result.fail .panic
+  massert (x = 1#i32)
 
 /- Unit test for [no_nested_borrows::test_box1] -/
 #assert (test_box1 == Result.ok ())
@@ -185,9 +171,7 @@ def test_panic_msg (b : Bool) : Result Unit :=
 def test_copy_int : Result Unit :=
   do
   let y ← copy_int 0#i32
-  if 0#i32 = y
-  then Result.ok ()
-  else Result.fail .panic
+  massert (0#i32 = y)
 
 /- Unit test for [no_nested_borrows::test_copy_int] -/
 #assert (test_copy_int == Result.ok ())
@@ -204,9 +188,7 @@ def is_cons {T : Type} (l : List T) : Result Bool :=
 def test_is_cons : Result Unit :=
   do
   let b ← is_cons (List.Cons 0#i32 List.Nil)
-  if b
-  then Result.ok ()
-  else Result.fail .panic
+  massert b
 
 /- Unit test for [no_nested_borrows::test_is_cons] -/
 #assert (test_is_cons == Result.ok ())
@@ -224,9 +206,7 @@ def test_split_list : Result Unit :=
   do
   let p ← split_list (List.Cons 0#i32 List.Nil)
   let (hd, _) := p
-  if hd = 0#i32
-  then Result.ok ()
-  else Result.fail .panic
+  massert (hd = 0#i32)
 
 /- Unit test for [no_nested_borrows::test_split_list] -/
 #assert (test_split_list == Result.ok ())
@@ -247,15 +227,10 @@ def choose_test : Result Unit :=
   do
   let (z, choose_back) ← choose true 0#i32 0#i32
   let z1 ← z + 1#i32
-  if z1 = 1#i32
-  then
-    let (x, y) := choose_back z1
-    if x = 1#i32
-    then if y = 0#i32
-         then Result.ok ()
-         else Result.fail .panic
-    else Result.fail .panic
-  else Result.fail .panic
+  let _ ← massert (z1 = 1#i32)
+  let (x, y) := choose_back z1
+  let _ ← massert (x = 1#i32)
+  massert (y = 0#i32)
 
 /- Unit test for [no_nested_borrows::choose_test] -/
 #assert (choose_test == Result.ok ())
@@ -346,42 +321,21 @@ def test_list_functions : Result Unit :=
   let l := List.Cons 2#i32 List.Nil
   let l1 := List.Cons 1#i32 l
   let i ← list_length (List.Cons 0#i32 l1)
-  if i = 3#u32
-  then
-    do
-    let i1 ← list_nth_shared (List.Cons 0#i32 l1) 0#u32
-    if i1 = 0#i32
-    then
-      do
-      let i2 ← list_nth_shared (List.Cons 0#i32 l1) 1#u32
-      if i2 = 1#i32
-      then
-        do
-        let i3 ← list_nth_shared (List.Cons 0#i32 l1) 2#u32
-        if i3 = 2#i32
-        then
-          do
-          let (_, list_nth_mut_back) ←
-            list_nth_mut (List.Cons 0#i32 l1) 1#u32
-          let ls := list_nth_mut_back 3#i32
-          let i4 ← list_nth_shared ls 0#u32
-          if i4 = 0#i32
-          then
-            do
-            let i5 ← list_nth_shared ls 1#u32
-            if i5 = 3#i32
-            then
-              do
-              let i6 ← list_nth_shared ls 2#u32
-              if i6 = 2#i32
-              then Result.ok ()
-              else Result.fail .panic
-            else Result.fail .panic
-          else Result.fail .panic
-        else Result.fail .panic
-      else Result.fail .panic
-    else Result.fail .panic
-  else Result.fail .panic
+  let _ ← massert (i = 3#u32)
+  let i1 ← list_nth_shared (List.Cons 0#i32 l1) 0#u32
+  let _ ← massert (i1 = 0#i32)
+  let i2 ← list_nth_shared (List.Cons 0#i32 l1) 1#u32
+  let _ ← massert (i2 = 1#i32)
+  let i3 ← list_nth_shared (List.Cons 0#i32 l1) 2#u32
+  let _ ← massert (i3 = 2#i32)
+  let (_, list_nth_mut_back) ← list_nth_mut (List.Cons 0#i32 l1) 1#u32
+  let ls := list_nth_mut_back 3#i32
+  let i4 ← list_nth_shared ls 0#u32
+  let _ ← massert (i4 = 0#i32)
+  let i5 ← list_nth_shared ls 1#u32
+  let _ ← massert (i5 = 3#i32)
+  let i6 ← list_nth_shared ls 2#u32
+  massert (i6 = 2#i32)
 
 /- Unit test for [no_nested_borrows::test_list_functions] -/
 #assert (test_list_functions == Result.ok ())
@@ -460,26 +414,15 @@ def test_constants : Result Unit :=
   do
   let swt ← new_tuple1
   let (i, _) := swt.p
-  if i = 1#u32
-  then
-    do
-    let swt1 ← new_tuple2
-    let (i1, _) := swt1.p
-    if i1 = 1#i16
-    then
-      do
-      let swt2 ← new_tuple3
-      let (i2, _) := swt2.p
-      if i2 = 1#u64
-      then
-        do
-        let swp ← new_pair1
-        if swp.p.x = 1#u32
-        then Result.ok ()
-        else Result.fail .panic
-      else Result.fail .panic
-    else Result.fail .panic
-  else Result.fail .panic
+  let _ ← massert (i = 1#u32)
+  let swt1 ← new_tuple2
+  let (i1, _) := swt1.p
+  let _ ← massert (i1 = 1#i16)
+  let swt2 ← new_tuple3
+  let (i2, _) := swt2.p
+  let _ ← massert (i2 = 1#u64)
+  let swp ← new_pair1
+  massert (swp.p.x = 1#u32)
 
 /- Unit test for [no_nested_borrows::test_constants] -/
 #assert (test_constants == Result.ok ())
@@ -495,10 +438,10 @@ def test_weird_borrows1 : Result Unit :=
 /- [no_nested_borrows::test_mem_replace]:
    Source: 'tests/src/no_nested_borrows.rs', lines 414:0-418:1 -/
 def test_mem_replace (px : U32) : Result U32 :=
+  do
   let (y, _) := core.mem.replace px 1#u32
-  if y = 0#u32
-  then Result.ok 2#u32
-  else Result.fail .panic
+  let _ ← massert (y = 0#u32)
+  Result.ok 2#u32
 
 /- [no_nested_borrows::test_shared_borrow_bool1]:
    Source: 'tests/src/no_nested_borrows.rs', lines 421:0-430:1 -/
diff --git a/tests/lean/Paper.lean b/tests/lean/Paper.lean
index 9decb92d5..418ecf63a 100644
--- a/tests/lean/Paper.lean
+++ b/tests/lean/Paper.lean
@@ -18,9 +18,7 @@ def ref_incr (x : I32) : Result I32 :=
 def test_incr : Result Unit :=
   do
   let x ← ref_incr 0#i32
-  if x = 1#i32
-  then Result.ok ()
-  else Result.fail .panic
+  massert (x = 1#i32)
 
 /- Unit test for [paper::test_incr] -/
 #assert (test_incr == Result.ok ())
@@ -41,15 +39,10 @@ def test_choose : Result Unit :=
   do
   let (z, choose_back) ← choose true 0#i32 0#i32
   let z1 ← z + 1#i32
-  if z1 = 1#i32
-  then
-    let (x, y) := choose_back z1
-    if x = 1#i32
-    then if y = 0#i32
-         then Result.ok ()
-         else Result.fail .panic
-    else Result.fail .panic
-  else Result.fail .panic
+  let _ ← massert (z1 = 1#i32)
+  let (x, y) := choose_back z1
+  let _ ← massert (x = 1#i32)
+  massert (y = 0#i32)
 
 /- Unit test for [paper::test_choose] -/
 #assert (test_choose == Result.ok ())
@@ -97,9 +90,7 @@ def test_nth : Result Unit :=
   let x1 ← x + 1#i32
   let l2 := list_nth_mut_back x1
   let i ← sum l2
-  if i = 7#i32
-  then Result.ok ()
-  else Result.fail .panic
+  massert (i = 7#i32)
 
 /- Unit test for [paper::test_nth] -/
 #assert (test_nth == Result.ok ())