diff options
Diffstat (limited to '')
| -rw-r--r-- | tests/misc/External.Funs.fst | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/tests/misc/External.Funs.fst b/tests/misc/External.Funs.fst index aafc0cf6..874b739c 100644 --- a/tests/misc/External.Funs.fst +++ b/tests/misc/External.Funs.fst @@ -109,8 +109,7 @@ let test_swap_non_zero_fwd (x : u32) (st : state) : result (state & u32) = | Return (st0, _) -> begin match swap_back u32 x 0 st with | Fail -> Fail - | Return (x0, _) -> - begin match x0 with | 0 -> Fail | _ -> Return (st0, x0) end + | Return (x0, _) -> if x0 = 0 then Fail else Return (st0, x0) end end |