Regenerate the tests

1 files changed, 2 insertions, 4 deletions

diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
index b16dcada..9b5baaeb 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
@@ -324,8 +324,7 @@ let hashmap_HashMap_get_mut_in_list
   (t : Type0) (ls : hashmap_List_t t) (key : usize) :
   result (t & (t -> result (hashmap_List_t t)))
   =
-  let* (x, back_'a) = hashmap_HashMap_get_mut_in_list_loop t ls key in
-  Return (x, back_'a)
+  hashmap_HashMap_get_mut_in_list_loop t ls key
 
 (** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_mut]:
     Source: 'src/hashmap.rs', lines 257:4-257:67 *)
@@ -446,8 +445,7 @@ let insert_on_disk
   (key : usize) (value : u64) (st : state) : result (state & unit) =
   let* (st1, hm) = hashmap_utils_deserialize st in
   let* hm1 = hashmap_HashMap_insert u64 hm key value in
-  let* (st2, _) = hashmap_utils_serialize hm1 st1 in
-  Return (st2, ())
+  hashmap_utils_serialize hm1 st1
 
 (** [hashmap_main::main]:
     Source: 'src/hashmap_main.rs', lines 16:0-16:13 *)