diff options
Diffstat (limited to '')
| -rw-r--r-- | tests/hashmap/Hashmap.Properties.fst | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/tests/hashmap/Hashmap.Properties.fst b/tests/hashmap/Hashmap.Properties.fst index 40a3361f..272819dc 100644 --- a/tests/hashmap/Hashmap.Properties.fst +++ b/tests/hashmap/Hashmap.Properties.fst @@ -1377,6 +1377,7 @@ val hash_map_insert_no_resize_fwd_back_lem_s | Fail, Fail -> True | Return hm, Return hm_v -> hash_map_t_inv hm /\ + hash_map_same_params hm self /\ hash_map_t_slots_v hm == hm_v /\ hash_map_slots_s_len hm_v == hash_map_t_len_s hm | _ -> False |