From 3e719defdd22b0e6c4bedce8996c2a58bb77a783 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sat, 5 Mar 2022 17:12:22 +0100
Subject: Make an update in the hash map

---
 tests/hashmap_on_disk/HashmapMain.Funs.fst | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

(limited to 'tests/hashmap_on_disk')

diff --git a/tests/hashmap_on_disk/HashmapMain.Funs.fst b/tests/hashmap_on_disk/HashmapMain.Funs.fst
index 0eda588f..89b9ef5b 100644
--- a/tests/hashmap_on_disk/HashmapMain.Funs.fst
+++ b/tests/hashmap_on_disk/HashmapMain.Funs.fst
@@ -447,13 +447,10 @@ let hashmap_hash_map_try_resize_back
               hashmap_hash_map_move_elements_back t hm
                 self.hashmap_hash_map_slots 0 st0 with
             | Fail -> Fail
-            | Return (st1, (hm0, v)) ->
-              let v0 =
-                mem_replace_back (vec (hashmap_list_t t)) v
-                  hm0.hashmap_hash_map_slots in
+            | Return (st1, (hm0, _)) ->
               Return (st1, Mkhashmap_hash_map_t
                 self.hashmap_hash_map_num_entries (i0, i1)
-                hm0.hashmap_hash_map_max_load v0)
+                hm0.hashmap_hash_map_max_load hm0.hashmap_hash_map_slots)
             end
           end
         end
-- 
cgit v1.2.3