From f3e16bb43a8ff27a5184d9fa452277cc6a59410f Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 19 Mar 2024 05:29:29 +0100
Subject: Regenerate the tests

---
 tests/fstar/betree_back_stateful/BetreeMain.Funs.fst | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

(limited to 'tests/fstar/betree_back_stateful/BetreeMain.Funs.fst')

diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
index ec042fb3..74044961 100644
--- a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
+++ b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
@@ -22,8 +22,7 @@ let betree_store_internal_node
   (id : u64) (content : betree_List_t (u64 & betree_Message_t)) (st : state) :
   result (state & unit)
   =
-  let* (st1, _) = betree_utils_store_internal_node id content st in
-  Return (st1, ())
+  betree_utils_store_internal_node id content st
 
 (** [betree_main::betree::load_leaf_node]:
     Source: 'src/betree.rs', lines 46:0-46:44 *)
@@ -37,8 +36,7 @@ let betree_store_leaf_node
   (id : u64) (content : betree_List_t (u64 & u64)) (st : state) :
   result (state & unit)
   =
-  let* (st1, _) = betree_utils_store_leaf_node id content st in
-  Return (st1, ())
+  betree_utils_store_leaf_node id content st
 
 (** [betree_main::betree::fresh_node_id]:
     Source: 'src/betree.rs', lines 55:0-55:48 *)
-- 
cgit v1.2.3