3 files changed, 10 insertions, 10 deletions
diff --git a/tests/fstar/hashmap/Hashmap.Funs.fst b/tests/fstar/hashmap/Hashmap.Funs.fst
index a85be4ed..0e991720 100644
--- a/tests/fstar/hashmap/Hashmap.Funs.fst
+++ b/tests/fstar/hashmap/Hashmap.Funs.fst
@@ -380,9 +380,9 @@ let hashMap_remove
     Source: 'tests/src/hashmap.rs', lines 335:0-335:43 *)
 let insert_on_disk
   (key : usize) (value : u64) (st : state) : result (state & unit) =
-  let* (st1, hm) = hashmap_utils_deserialize st in
+  let* (st1, hm) = utils_deserialize st in
   let* hm1 = hashMap_insert u64 hm key value in
-  hashmap_utils_serialize hm1 st1
+  utils_serialize hm1 st1
 
 (** [hashmap::test1]:
     Source: 'tests/src/hashmap.rs', lines 350:0-350:10 *)
diff --git a/tests/fstar/hashmap/Hashmap.FunsExternal.fsti b/tests/fstar/hashmap/Hashmap.FunsExternal.fsti
index 6e3964c7..f2f305e6 100644
--- a/tests/fstar/hashmap/Hashmap.FunsExternal.fsti
+++ b/tests/fstar/hashmap/Hashmap.FunsExternal.fsti
@@ -6,11 +6,11 @@ include Hashmap.Types
 
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
-(** [hashmap::hashmap_utils::deserialize]:
+(** [hashmap::utils::deserialize]:
     Source: 'tests/src/hashmap.rs', lines 330:4-330:47 *)
-val hashmap_utils_deserialize : state -> result (state & (hashMap_t u64))
+val utils_deserialize : state -> result (state & (hashMap_t u64))
 
-(** [hashmap::hashmap_utils::serialize]:
+(** [hashmap::utils::serialize]:
     Source: 'tests/src/hashmap.rs', lines 325:4-325:46 *)
-val hashmap_utils_serialize : hashMap_t u64 -> state -> result (state & unit)
+val utils_serialize : hashMap_t u64 -> state -> result (state & unit)
 
diff --git a/tests/fstar/hashmap/Hashmap.Properties.fst b/tests/fstar/hashmap/Hashmap.Properties.fst
index 0d6372c1..ed118c46 100644
--- a/tests/fstar/hashmap/Hashmap.Properties.fst
+++ b/tests/fstar/hashmap/Hashmap.Properties.fst
@@ -18,18 +18,18 @@ val state_v : state -> hashMap_t u64
 /// [serialize] updates the hash map stored on disk
 assume
 val serialize_lem (hm : hashMap_t u64) (st : state) : Lemma (
-  match hashmap_utils_serialize hm st with
+  match utils_serialize hm st with
   | Fail _ -> True
   | Ok (st', ()) -> state_v st' == hm)
-  [SMTPat (hashmap_utils_serialize hm st)]
+  [SMTPat (utils_serialize hm st)]
 
 /// [deserialize] gives us the hash map stored on disk, without updating it
 assume
 val deserialize_lem (st : state) : Lemma (
-  match hashmap_utils_deserialize st with
+  match utils_deserialize st with
   | Fail _ -> True
   | Ok (st', hm) -> hm == state_v st /\ st' == st)
-  [SMTPat (hashmap_utils_deserialize st)]
+  [SMTPat (utils_deserialize st)]
 
 (*** Lemmas *)