diff options
author | Sidney Congard | 2022-08-11 10:39:04 +0200 |
---|---|---|
committer | Sidney Congard | 2022-08-11 10:39:04 +0200 |
commit | fa491861faed3ba5ed4fe806b55bea663a29579c (patch) | |
tree | 05a4e268aedfdea0b14ac9e44f8ee66210aeae65 /tests/betree/BetreeMain.Funs.fst | |
parent | cd754eabe3af025ca3465c5fc6d8cb48da66a1ae (diff) |
Correct assertion for stateless globals
Diffstat (limited to 'tests/betree/BetreeMain.Funs.fst')
-rw-r--r-- | tests/betree/BetreeMain.Funs.fst | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/tests/betree/BetreeMain.Funs.fst b/tests/betree/BetreeMain.Funs.fst index 4761b6a3..e80e96a6 100644 --- a/tests/betree/BetreeMain.Funs.fst +++ b/tests/betree/BetreeMain.Funs.fst @@ -96,17 +96,16 @@ let betree_upsert_update_fwd | Some prev0 -> begin match st with | BetreeUpsertFunStateAdd v -> - let i = core_num_u64_max_c in - begin match u64_sub i prev0 with + begin match u64_sub core_num_u64_max_c prev0 with | Fail -> Fail | Return margin -> if margin >= v then begin match u64_add prev0 v with | Fail -> Fail - | Return i0 -> Return i0 + | Return i -> Return i end - else let i0 = core_num_u64_max_c in Return i0 + else Return core_num_u64_max_c end | BetreeUpsertFunStateSub v -> if prev0 >= v |