diff --git a/creusot/tests/should_succeed/hashmap.coma b/creusot/tests/should_succeed/hashmap.coma
index d72549f31a..7cb911505c 100644
--- a/creusot/tests/should_succeed/hashmap.coma
+++ b/creusot/tests/should_succeed/hashmap.coma
@@ -1,8 +1,8 @@
-module M_hashmap__qyi15610519155507183510__resolve_coherence [#"hashmap.rs" 64 4 64 31] (* <List<(K, V)> as creusot_contracts::Resolve> *)
-  let%span shashmap0 = "hashmap.rs" 62 15 62 39
-  let%span shashmap1 = "hashmap.rs" 63 14 63 31
-  let%span shashmap2 = "hashmap.rs" 61 4 61 23
-  let%span shashmap3 = "hashmap.rs" 56 12 56 59
+module M_hashmap__qyi15610519155507183510__resolve_coherence [#"hashmap.rs" 63 4 63 31] (* <List<(K, V)> as creusot_contracts::Resolve> *)
+  let%span shashmap0 = "hashmap.rs" 61 15 61 39
+  let%span shashmap1 = "hashmap.rs" 62 14 62 31
+  let%span shashmap2 = "hashmap.rs" 60 4 60 23
+  let%span shashmap3 = "hashmap.rs" 55 12 55 59
   let%span shashmap4 = "hashmap.rs" 31 12 34 13
   let%span sresolve5 = "../../../creusot-contracts/src/resolve.rs" 68 8 68 23
   let%span sresolve6 = "../../../creusot-contracts/src/resolve.rs" 40 8 40 44
@@ -43,7 +43,7 @@ module M_hashmap__qyi15610519155507183510__resolve_coherence [#"hashmap.rs" 64 4
   predicate resolve'3 (_1 : t_Option'0) =
     resolve'6 _1
   
-  predicate resolve'0 [#"hashmap.rs" 53 4 53 28] (self : t_List'0) =
+  predicate resolve'0 [#"hashmap.rs" 52 4 52 28] (self : t_List'0) =
     [%#shashmap3] forall k : t_DeepModelTy'0 . resolve'3 (get'0 self k)
   
   predicate resolve'7 (_1 : t_List'0) =
@@ -71,14 +71,14 @@ module M_hashmap__qyi15610519155507183510__resolve_coherence [#"hashmap.rs" 64 4
   
   constant self  : t_List'0
   
-  function resolve_coherence'0 [#"hashmap.rs" 64 4 64 31] (self : t_List'0) : ()
+  function resolve_coherence'0 [#"hashmap.rs" 63 4 63 31] (self : t_List'0) : ()
   
   goal vc_resolve_coherence'0 : ([%#shashmap0] structural_resolve'0 self)  -> ([%#shashmap1] resolve'0 self)
 end
-module M_hashmap__qyi9060063638777358169__hash [#"hashmap.rs" 78 4 78 25] (* <usize as Hash> *)
-  let%span shashmap0 = "hashmap.rs" 77 14 77 58
+module M_hashmap__qyi9060063638777358169__hash [#"hashmap.rs" 77 4 77 25] (* <usize as Hash> *)
+  let%span shashmap0 = "hashmap.rs" 76 14 76 58
   let%span smodel1 = "../../../creusot-contracts/src/model.rs" 79 8 79 28
-  let%span shashmap2 = "hashmap.rs" 84 20 84 21
+  let%span shashmap2 = "hashmap.rs" 83 20 83 21
   let%span snum3 = "../../../creusot-contracts/src/std/num.rs" 21 28 21 33
   
   use prelude.prelude.UIntSize
@@ -101,7 +101,7 @@ module M_hashmap__qyi9060063638777358169__hash [#"hashmap.rs" 78 4 78 25] (* <us
   function deep_model'0 (self : usize) : int =
     [%#smodel1] deep_model'1 self
   
-  function hash_log'0 [#"hashmap.rs" 83 4 83 30] (x : int) : int =
+  function hash_log'0 [#"hashmap.rs" 82 4 82 30] (x : int) : int =
     [%#shashmap2] x
   
   meta "compute_max_steps" 1000000
@@ -116,24 +116,24 @@ module M_hashmap__qyi9060063638777358169__hash [#"hashmap.rs" 78 4 78 25] (* <us
       (! return' {result}) ]
     
 end
-module M_hashmap__qyi15467499327297494705__resolve_coherence [#"hashmap.rs" 117 4 117 31] (* <MyHashMap<K, V> as creusot_contracts::Resolve> *)
-  let%span shashmap0 = "hashmap.rs" 114 15 114 24
-  let%span shashmap1 = "hashmap.rs" 115 15 115 39
-  let%span shashmap2 = "hashmap.rs" 116 14 116 31
-  let%span shashmap3 = "hashmap.rs" 113 4 113 23
-  let%span shashmap4 = "hashmap.rs" 108 12 108 60
-  let%span shashmap5 = "hashmap.rs" 98 8 98 33
+module M_hashmap__qyi15467499327297494705__resolve_coherence [#"hashmap.rs" 116 4 116 31] (* <MyHashMap<K, V> as creusot_contracts::Resolve> *)
+  let%span shashmap0 = "hashmap.rs" 113 15 113 24
+  let%span shashmap1 = "hashmap.rs" 114 15 114 39
+  let%span shashmap2 = "hashmap.rs" 115 14 115 31
+  let%span shashmap3 = "hashmap.rs" 112 4 112 23
+  let%span shashmap4 = "hashmap.rs" 107 12 107 60
+  let%span shashmap5 = "hashmap.rs" 97 8 97 33
   let%span sinvariant6 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18
   let%span svec7 = "../../../creusot-contracts/src/std/vec.rs" 49 20 49 83
-  let%span shashmap8 = "hashmap.rs" 123 8 123 53
+  let%span shashmap8 = "hashmap.rs" 122 8 122 53
   let%span shashmap9 = "hashmap.rs" 31 12 34 13
   let%span sresolve10 = "../../../creusot-contracts/src/resolve.rs" 82 8 85 9
   let%span svec11 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41
   let%span sindex12 = "../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31
-  let%span shashmap13 = "hashmap.rs" 128 20 128 66
-  let%span shashmap14 = "hashmap.rs" 56 12 56 59
-  let%span shashmap15 = "hashmap.rs" 144 12 145 139
-  let%span shashmap16 = "hashmap.rs" 134 12 134 91
+  let%span shashmap13 = "hashmap.rs" 127 20 127 66
+  let%span shashmap14 = "hashmap.rs" 55 12 55 59
+  let%span shashmap15 = "hashmap.rs" 143 12 144 139
+  let%span shashmap16 = "hashmap.rs" 133 12 133 91
   let%span shashmap17 = "hashmap.rs" 41 12 44 13
   let%span svec18 = "../../../creusot-contracts/src/std/vec.rs" 65 20 65 41
   let%span sseq19 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95
@@ -204,14 +204,14 @@ module M_hashmap__qyi15467499327297494705__resolve_coherence [#"hashmap.rs" 117
       | C_Cons'0 (k, v) tl -> if deep_model'0 k = index then C_Some'0 v else get'0 tl index
       end
   
-  function hash_log'0 [#"hashmap.rs" 73 4 73 45] (_1 : t_DeepModelTy'0) : int
+  function hash_log'0 [#"hashmap.rs" 72 4 72 45] (_1 : t_DeepModelTy'0) : int
   
   use int.EuclideanDivision
   
-  function bucket_ix'0 [#"hashmap.rs" 127 4 127 48] (self : t_MyHashMap'0) (k : t_DeepModelTy'0) : int =
+  function bucket_ix'0 [#"hashmap.rs" 126 4 126 48] (self : t_MyHashMap'0) (k : t_DeepModelTy'0) : int =
     [%#shashmap13] EuclideanDivision.mod (hash_log'0 k) (Seq.length (view'1 self.t_MyHashMap__buckets'0))
   
-  predicate good_bucket'0 [#"hashmap.rs" 132 4 132 57] (self : t_MyHashMap'0) (l : t_List'0) (h : int) =
+  predicate good_bucket'0 [#"hashmap.rs" 131 4 131 57] (self : t_MyHashMap'0) (l : t_List'0) (h : int) =
     [%#shashmap16] forall k : t_DeepModelTy'0, v : t_V'0 . get'0 l k = C_Some'0 v  -> bucket_ix'0 self k = h
   
   predicate no_double_binding'0 [#"hashmap.rs" 39 4 39 38] (self : t_List'0) =
@@ -220,7 +220,7 @@ module M_hashmap__qyi15467499327297494705__resolve_coherence [#"hashmap.rs" 117
       | C_Cons'0 (k, _) tl -> get'0 tl (deep_model'0 k) = C_None'0 /\ no_double_binding'0 tl
       end
   
-  predicate invariant'1 [#"hashmap.rs" 142 4 142 30] (self : t_MyHashMap'0) =
+  predicate invariant'1 [#"hashmap.rs" 141 4 141 30] (self : t_MyHashMap'0) =
     [%#shashmap15] 0 < Seq.length (view'1 self.t_MyHashMap__buckets'0)
     /\ (forall i : int . 0 <= i /\ i < Seq.length (view'1 self.t_MyHashMap__buckets'0)
      -> good_bucket'0 self (index_logic'0 self.t_MyHashMap__buckets'0 i) i
@@ -292,7 +292,7 @@ module M_hashmap__qyi15467499327297494705__resolve_coherence [#"hashmap.rs" 117
   predicate resolve'2 (_1 : t_Option'0) =
     resolve'4 _1
   
-  predicate resolve'7 [#"hashmap.rs" 53 4 53 28] (self : t_List'0) =
+  predicate resolve'7 [#"hashmap.rs" 52 4 52 28] (self : t_List'0) =
     [%#shashmap14] forall k : t_DeepModelTy'0 . resolve'2 (get'0 self k)
   
   predicate resolve'5 (_1 : t_List'0) =
@@ -311,41 +311,41 @@ module M_hashmap__qyi15467499327297494705__resolve_coherence [#"hashmap.rs" 117
   
   use map.Map
   
-  function bucket'0 [#"hashmap.rs" 122 4 122 54] (self : t_MyHashMap'0) (k : t_DeepModelTy'0) : t_List'0 =
+  function bucket'0 [#"hashmap.rs" 121 4 121 54] (self : t_MyHashMap'0) (k : t_DeepModelTy'0) : t_List'0 =
     [%#shashmap8] index_logic'0 self.t_MyHashMap__buckets'0 (bucket_ix'0 self k)
   
   use prelude.prelude.Mapping
   
-  function view'0 [#"hashmap.rs" 97 4 97 33] (self : t_MyHashMap'0) : Map.map t_DeepModelTy'0 (t_Option'0) =
+  function view'0 [#"hashmap.rs" 96 4 96 33] (self : t_MyHashMap'0) : Map.map t_DeepModelTy'0 (t_Option'0) =
     [%#shashmap5] Mapping.from_fn (fun (k : t_DeepModelTy'0) -> get'0 (bucket'0 self k) k)
   
   use map.Map
   
-  predicate resolve'0 [#"hashmap.rs" 105 4 105 28] (self : t_MyHashMap'0) =
+  predicate resolve'0 [#"hashmap.rs" 104 4 104 28] (self : t_MyHashMap'0) =
     [%#shashmap4] forall k : t_DeepModelTy'0 . resolve'2 (Map.get (view'0 self) k)
   
   constant self  : t_MyHashMap'0
   
-  function resolve_coherence'0 [#"hashmap.rs" 117 4 117 31] (self : t_MyHashMap'0) : ()
+  function resolve_coherence'0 [#"hashmap.rs" 116 4 116 31] (self : t_MyHashMap'0) : ()
   
   goal vc_resolve_coherence'0 : ([%#shashmap1] structural_resolve'0 self)
    -> ([%#shashmap0] inv'0 self)  -> ([%#shashmap2] resolve'0 self)
 end
-module M_hashmap__qyi7664122466964245986__new [#"hashmap.rs" 153 4 153 46] (* MyHashMap<K, V> *)
-  let%span shashmap0 = "hashmap.rs" 151 15 151 24
-  let%span shashmap1 = "hashmap.rs" 153 31 153 46
-  let%span shashmap2 = "hashmap.rs" 152 14 152 62
+module M_hashmap__qyi7664122466964245986__new [#"hashmap.rs" 152 4 152 46] (* MyHashMap<K, V> *)
+  let%span shashmap0 = "hashmap.rs" 150 15 150 24
+  let%span shashmap1 = "hashmap.rs" 152 31 152 46
+  let%span shashmap2 = "hashmap.rs" 151 14 151 62
   let%span svec3 = "../../../creusot-contracts/src/std/vec.rs" 180 22 180 41
   let%span svec4 = "../../../creusot-contracts/src/std/vec.rs" 181 22 181 76
-  let%span shashmap5 = "hashmap.rs" 98 8 98 33
+  let%span shashmap5 = "hashmap.rs" 97 8 97 33
   let%span svec6 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41
   let%span sindex7 = "../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31
-  let%span shashmap8 = "hashmap.rs" 123 8 123 53
+  let%span shashmap8 = "hashmap.rs" 122 8 122 53
   let%span shashmap9 = "hashmap.rs" 31 12 34 13
-  let%span shashmap10 = "hashmap.rs" 144 12 145 139
-  let%span shashmap11 = "hashmap.rs" 128 20 128 66
+  let%span shashmap10 = "hashmap.rs" 143 12 144 139
+  let%span shashmap11 = "hashmap.rs" 127 20 127 66
   let%span svec12 = "../../../creusot-contracts/src/std/vec.rs" 65 20 65 41
-  let%span shashmap13 = "hashmap.rs" 134 12 134 91
+  let%span shashmap13 = "hashmap.rs" 133 12 133 91
   let%span shashmap14 = "hashmap.rs" 41 12 44 13
   let%span sboxed15 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
   let%span sseq16 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95
@@ -463,14 +463,14 @@ module M_hashmap__qyi7664122466964245986__new [#"hashmap.rs" 153 4 153 46] (* My
       | C_Cons'0 (k, v) tl -> if deep_model'0 k = index then C_Some'0 v else get'0 tl index
       end
   
-  function hash_log'0 [#"hashmap.rs" 73 4 73 45] (_1 : t_DeepModelTy'0) : int
+  function hash_log'0 [#"hashmap.rs" 72 4 72 45] (_1 : t_DeepModelTy'0) : int
   
   use int.EuclideanDivision
   
-  function bucket_ix'0 [#"hashmap.rs" 127 4 127 48] (self : t_MyHashMap'0) (k : t_DeepModelTy'0) : int =
+  function bucket_ix'0 [#"hashmap.rs" 126 4 126 48] (self : t_MyHashMap'0) (k : t_DeepModelTy'0) : int =
     [%#shashmap11] EuclideanDivision.mod (hash_log'0 k) (Seq.length (view'1 self.t_MyHashMap__buckets'0))
   
-  predicate good_bucket'0 [#"hashmap.rs" 132 4 132 57] (self : t_MyHashMap'0) (l : t_List'0) (h : int) =
+  predicate good_bucket'0 [#"hashmap.rs" 131 4 131 57] (self : t_MyHashMap'0) (l : t_List'0) (h : int) =
     [%#shashmap13] forall k : t_DeepModelTy'0, v : t_V'0 . get'0 l k = C_Some'0 v  -> bucket_ix'0 self k = h
   
   predicate no_double_binding'0 [#"hashmap.rs" 39 4 39 38] (self : t_List'0) =
@@ -479,7 +479,7 @@ module M_hashmap__qyi7664122466964245986__new [#"hashmap.rs" 153 4 153 46] (* My
       | C_Cons'0 (k, _) tl -> get'0 tl (deep_model'0 k) = C_None'0 /\ no_double_binding'0 tl
       end
   
-  predicate invariant'0 [#"hashmap.rs" 142 4 142 30] (self : t_MyHashMap'0) =
+  predicate invariant'0 [#"hashmap.rs" 141 4 141 30] (self : t_MyHashMap'0) =
     [%#shashmap10] 0 < Seq.length (view'1 self.t_MyHashMap__buckets'0)
     /\ (forall i : int . 0 <= i /\ i < Seq.length (view'1 self.t_MyHashMap__buckets'0)
      -> good_bucket'0 self (index_logic'0 self.t_MyHashMap__buckets'0 i) i
@@ -495,12 +495,12 @@ module M_hashmap__qyi7664122466964245986__new [#"hashmap.rs" 153 4 153 46] (* My
   
   use map.Map
   
-  function bucket'0 [#"hashmap.rs" 122 4 122 54] (self : t_MyHashMap'0) (k : t_DeepModelTy'0) : t_List'0 =
+  function bucket'0 [#"hashmap.rs" 121 4 121 54] (self : t_MyHashMap'0) (k : t_DeepModelTy'0) : t_List'0 =
     [%#shashmap8] index_logic'0 self.t_MyHashMap__buckets'0 (bucket_ix'0 self k)
   
   use prelude.prelude.Mapping
   
-  function view'0 [#"hashmap.rs" 97 4 97 33] (self : t_MyHashMap'0) : Map.map t_DeepModelTy'0 (t_Option'0) =
+  function view'0 [#"hashmap.rs" 96 4 96 33] (self : t_MyHashMap'0) : Map.map t_DeepModelTy'0 (t_Option'0) =
     [%#shashmap5] Mapping.from_fn (fun (k : t_DeepModelTy'0) -> get'0 (bucket'0 self k) k)
   
   use map.Map
@@ -530,24 +530,24 @@ module M_hashmap__qyi7664122466964245986__new [#"hashmap.rs" 153 4 153 46] (* My
       (! return' {result}) ]
     
 end
-module M_hashmap__qyi7664122466964245986__add [#"hashmap.rs" 159 4 159 41] (* MyHashMap<K, V> *)
-  let%span shashmap0 = "hashmap.rs" 161 23 161 41
-  let%span shashmap1 = "hashmap.rs" 163 27 163 55
-  let%span shashmap2 = "hashmap.rs" 165 20 165 35
-  let%span shashmap3 = "hashmap.rs" 173 20 174 51
-  let%span shashmap4 = "hashmap.rs" 172 20 172 44
-  let%span shashmap5 = "hashmap.rs" 171 20 171 96
-  let%span shashmap6 = "hashmap.rs" 170 20 170 108
-  let%span shashmap7 = "hashmap.rs" 169 20 169 101
-  let%span shashmap8 = "hashmap.rs" 168 20 168 52
-  let%span shashmap9 = "hashmap.rs" 167 20 167 26
-  let%span shashmap10 = "hashmap.rs" 159 20 159 24
-  let%span shashmap11 = "hashmap.rs" 159 26 159 29
-  let%span shashmap12 = "hashmap.rs" 159 34 159 37
-  let%span shashmap13 = "hashmap.rs" 158 14 158 122
+module M_hashmap__qyi7664122466964245986__add [#"hashmap.rs" 158 4 158 41] (* MyHashMap<K, V> *)
+  let%span shashmap0 = "hashmap.rs" 160 23 160 41
+  let%span shashmap1 = "hashmap.rs" 162 27 162 55
+  let%span shashmap2 = "hashmap.rs" 164 20 164 35
+  let%span shashmap3 = "hashmap.rs" 172 20 173 51
+  let%span shashmap4 = "hashmap.rs" 171 20 171 44
+  let%span shashmap5 = "hashmap.rs" 170 20 170 96
+  let%span shashmap6 = "hashmap.rs" 169 20 169 108
+  let%span shashmap7 = "hashmap.rs" 168 20 168 101
+  let%span shashmap8 = "hashmap.rs" 167 20 167 52
+  let%span shashmap9 = "hashmap.rs" 166 20 166 26
+  let%span shashmap10 = "hashmap.rs" 158 20 158 24
+  let%span shashmap11 = "hashmap.rs" 158 26 158 29
+  let%span shashmap12 = "hashmap.rs" 158 34 158 37
+  let%span shashmap13 = "hashmap.rs" 157 14 157 122
   let%span svec14 = "../../../creusot-contracts/src/std/vec.rs" 83 26 83 48
-  let%span shashmap15 = "hashmap.rs" 70 13 70 17
-  let%span shashmap16 = "hashmap.rs" 69 14 69 58
+  let%span shashmap15 = "hashmap.rs" 69 13 69 17
+  let%span shashmap16 = "hashmap.rs" 68 14 68 58
   let%span svec17 = "../../../creusot-contracts/src/std/vec.rs" 152 27 152 46
   let%span svec18 = "../../../creusot-contracts/src/std/vec.rs" 153 26 153 54
   let%span svec19 = "../../../creusot-contracts/src/std/vec.rs" 154 26 154 57
@@ -555,9 +555,9 @@ module M_hashmap__qyi7664122466964245986__add [#"hashmap.rs" 159 4 159 41] (* My
   let%span svec21 = "../../../creusot-contracts/src/std/vec.rs" 156 26 156 55
   let%span shashmap22 = "hashmap.rs" 31 12 34 13
   let%span shashmap23 = "hashmap.rs" 41 12 44 13
-  let%span shashmap24 = "hashmap.rs" 134 12 134 91
+  let%span shashmap24 = "hashmap.rs" 133 12 133 91
   let%span scmp25 = "../../../creusot-contracts/src/std/cmp.rs" 11 26 11 75
-  let%span shashmap26 = "hashmap.rs" 98 8 98 33
+  let%span shashmap26 = "hashmap.rs" 97 8 97 33
   let%span smodel27 = "../../../creusot-contracts/src/model.rs" 106 8 106 22
   let%span smodel28 = "../../../creusot-contracts/src/model.rs" 88 8 88 22
   let%span smodel29 = "../../../creusot-contracts/src/model.rs" 79 8 79 28
@@ -566,9 +566,9 @@ module M_hashmap__qyi7664122466964245986__add [#"hashmap.rs" 159 4 159 41] (* My
   let%span svec32 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41
   let%span sslice33 = "../../../creusot-contracts/src/std/slice.rs" 136 20 136 94
   let%span sresolve34 = "../../../creusot-contracts/src/resolve.rs" 54 20 54 34
-  let%span shashmap35 = "hashmap.rs" 128 20 128 66
-  let%span shashmap36 = "hashmap.rs" 56 12 56 59
-  let%span shashmap37 = "hashmap.rs" 123 8 123 53
+  let%span shashmap35 = "hashmap.rs" 127 20 127 66
+  let%span shashmap36 = "hashmap.rs" 55 12 55 59
+  let%span shashmap37 = "hashmap.rs" 122 8 122 53
   let%span svec38 = "../../../creusot-contracts/src/std/vec.rs" 65 20 65 41
   let%span sinvariant39 = "../../../creusot-contracts/src/invariant.rs" 34 20 34 44
   let%span sboxed40 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
@@ -576,7 +576,7 @@ module M_hashmap__qyi7664122466964245986__add [#"hashmap.rs" 159 4 159 41] (* My
   let%span sinvariant42 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18
   let%span sresolve43 = "../../../creusot-contracts/src/resolve.rs" 82 8 85 9
   let%span sseq44 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95
-  let%span shashmap45 = "hashmap.rs" 144 12 145 139
+  let%span shashmap45 = "hashmap.rs" 143 12 144 139
   
   use prelude.prelude.Snapshot
   
@@ -697,7 +697,7 @@ module M_hashmap__qyi7664122466964245986__add [#"hashmap.rs" 159 4 159 41] (* My
   function deep_model'1 (self : t_K'0) : t_DeepModelTy'0 =
     [%#smodel29] deep_model'0 self
   
-  function hash_log'0 [#"hashmap.rs" 73 4 73 45] (_1 : t_DeepModelTy'0) : int
+  function hash_log'0 [#"hashmap.rs" 72 4 72 45] (_1 : t_DeepModelTy'0) : int
   
   use prelude.prelude.UInt64
   
@@ -782,10 +782,10 @@ module M_hashmap__qyi7664122466964245986__add [#"hashmap.rs" 159 4 159 41] (* My
   
   use int.EuclideanDivision
   
-  function bucket_ix'0 [#"hashmap.rs" 127 4 127 48] (self : t_MyHashMap'0) (k : t_DeepModelTy'0) : int =
+  function bucket_ix'0 [#"hashmap.rs" 126 4 126 48] (self : t_MyHashMap'0) (k : t_DeepModelTy'0) : int =
     [%#shashmap35] EuclideanDivision.mod (hash_log'0 k) (Seq.length (view'4 self.t_MyHashMap__buckets'0))
   
-  predicate good_bucket'0 [#"hashmap.rs" 132 4 132 57] (self : t_MyHashMap'0) (l : t_List'0) (h : int) =
+  predicate good_bucket'0 [#"hashmap.rs" 131 4 131 57] (self : t_MyHashMap'0) (l : t_List'0) (h : int) =
     [%#shashmap24] forall k : t_DeepModelTy'0, v : t_V'0 . get'0 l k = C_Some'0 v  -> bucket_ix'0 self k = h
   
   use prelude.prelude.Snapshot
@@ -852,7 +852,7 @@ module M_hashmap__qyi7664122466964245986__add [#"hashmap.rs" 159 4 159 41] (* My
   predicate resolve'12 (_1 : t_Option'0) =
     resolve'13 _1
   
-  predicate resolve'10 [#"hashmap.rs" 53 4 53 28] (self : t_List'0) =
+  predicate resolve'10 [#"hashmap.rs" 52 4 52 28] (self : t_List'0) =
     [%#shashmap36] forall k : t_DeepModelTy'0 . resolve'12 (get'0 self k)
   
   predicate resolve'4 (_1 : t_List'0) =
@@ -861,7 +861,7 @@ module M_hashmap__qyi7664122466964245986__add [#"hashmap.rs" 159 4 159 41] (* My
   function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : t_List'0 =
     [%#sindex41] Seq.get (view'4 self) ix
   
-  predicate invariant'11 [#"hashmap.rs" 142 4 142 30] (self : t_MyHashMap'0) =
+  predicate invariant'11 [#"hashmap.rs" 141 4 141 30] (self : t_MyHashMap'0) =
     [%#shashmap45] 0 < Seq.length (view'4 self.t_MyHashMap__buckets'0)
     /\ (forall i : int . 0 <= i /\ i < Seq.length (view'4 self.t_MyHashMap__buckets'0)
      -> good_bucket'0 self (index_logic'0 self.t_MyHashMap__buckets'0 i) i
@@ -896,12 +896,12 @@ module M_hashmap__qyi7664122466964245986__add [#"hashmap.rs" 159 4 159 41] (* My
   
   use map.Map
   
-  function bucket'0 [#"hashmap.rs" 122 4 122 54] (self : t_MyHashMap'0) (k : t_DeepModelTy'0) : t_List'0 =
+  function bucket'0 [#"hashmap.rs" 121 4 121 54] (self : t_MyHashMap'0) (k : t_DeepModelTy'0) : t_List'0 =
     [%#shashmap37] index_logic'0 self.t_MyHashMap__buckets'0 (bucket_ix'0 self k)
   
   use prelude.prelude.Mapping
   
-  function view'0 [#"hashmap.rs" 97 4 97 33] (self : t_MyHashMap'0) : Map.map t_DeepModelTy'0 (t_Option'0) =
+  function view'0 [#"hashmap.rs" 96 4 96 33] (self : t_MyHashMap'0) : Map.map t_DeepModelTy'0 (t_Option'0) =
     [%#shashmap26] Mapping.from_fn (fun (k : t_DeepModelTy'0) -> get'0 (bucket'0 self k) k)
   
   use map.Map
@@ -1122,34 +1122,34 @@ module M_hashmap__qyi7664122466964245986__add [#"hashmap.rs" 159 4 159 41] (* My
       (! return' {result}) ]
     
 end
-module M_hashmap__qyi7664122466964245986__get [#"hashmap.rs" 191 4 191 43] (* MyHashMap<K, V> *)
-  let%span shashmap0 = "hashmap.rs" 192 27 192 67
-  let%span shashmap1 = "hashmap.rs" 196 20 196 101
-  let%span shashmap2 = "hashmap.rs" 195 20 195 26
-  let%span shashmap3 = "hashmap.rs" 191 16 191 20
-  let%span shashmap4 = "hashmap.rs" 191 22 191 25
-  let%span shashmap5 = "hashmap.rs" 191 33 191 43
-  let%span shashmap6 = "hashmap.rs" 187 14 190 5
-  let%span shashmap7 = "hashmap.rs" 70 13 70 17
-  let%span shashmap8 = "hashmap.rs" 69 14 69 58
+module M_hashmap__qyi7664122466964245986__get [#"hashmap.rs" 190 4 190 43] (* MyHashMap<K, V> *)
+  let%span shashmap0 = "hashmap.rs" 191 27 191 67
+  let%span shashmap1 = "hashmap.rs" 195 20 195 101
+  let%span shashmap2 = "hashmap.rs" 194 20 194 26
+  let%span shashmap3 = "hashmap.rs" 190 16 190 20
+  let%span shashmap4 = "hashmap.rs" 190 22 190 25
+  let%span shashmap5 = "hashmap.rs" 190 33 190 43
+  let%span shashmap6 = "hashmap.rs" 186 14 189 5
+  let%span shashmap7 = "hashmap.rs" 69 13 69 17
+  let%span shashmap8 = "hashmap.rs" 68 14 68 58
   let%span svec9 = "../../../creusot-contracts/src/std/vec.rs" 83 26 83 48
   let%span svec10 = "../../../creusot-contracts/src/std/vec.rs" 162 27 162 46
   let%span svec11 = "../../../creusot-contracts/src/std/vec.rs" 163 26 163 54
-  let%span shashmap12 = "hashmap.rs" 123 8 123 53
+  let%span shashmap12 = "hashmap.rs" 122 8 122 53
   let%span shashmap13 = "hashmap.rs" 31 12 34 13
   let%span scmp14 = "../../../creusot-contracts/src/std/cmp.rs" 11 26 11 75
   let%span smodel15 = "../../../creusot-contracts/src/model.rs" 88 8 88 22
   let%span smodel16 = "../../../creusot-contracts/src/model.rs" 79 8 79 28
   let%span sslice17 = "../../../creusot-contracts/src/std/slice.rs" 122 20 122 37
   let%span sslice18 = "../../../creusot-contracts/src/std/slice.rs" 129 20 129 37
-  let%span shashmap19 = "hashmap.rs" 128 20 128 66
+  let%span shashmap19 = "hashmap.rs" 127 20 127 66
   let%span sindex20 = "../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31
-  let%span shashmap21 = "hashmap.rs" 98 8 98 33
+  let%span shashmap21 = "hashmap.rs" 97 8 97 33
   let%span svec22 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41
   let%span sinvariant23 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18
-  let%span shashmap24 = "hashmap.rs" 144 12 145 139
+  let%span shashmap24 = "hashmap.rs" 143 12 144 139
   let%span svec25 = "../../../creusot-contracts/src/std/vec.rs" 65 20 65 41
-  let%span shashmap26 = "hashmap.rs" 134 12 134 91
+  let%span shashmap26 = "hashmap.rs" 133 12 133 91
   let%span shashmap27 = "hashmap.rs" 41 12 44 13
   let%span sboxed28 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
   let%span sseq29 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95
@@ -1178,7 +1178,7 @@ module M_hashmap__qyi7664122466964245986__get [#"hashmap.rs" 191 4 191 43] (* My
   
   use prelude.prelude.Int
   
-  function hash_log'0 [#"hashmap.rs" 73 4 73 45] (_1 : t_DeepModelTy'0) : int
+  function hash_log'0 [#"hashmap.rs" 72 4 72 45] (_1 : t_DeepModelTy'0) : int
   
   use prelude.prelude.UInt64
   
@@ -1309,13 +1309,13 @@ module M_hashmap__qyi7664122466964245986__get [#"hashmap.rs" 191 4 191 43] (* My
   
   use int.EuclideanDivision
   
-  function bucket_ix'0 [#"hashmap.rs" 127 4 127 48] (self : t_MyHashMap'0) (k : t_DeepModelTy'0) : int =
+  function bucket_ix'0 [#"hashmap.rs" 126 4 126 48] (self : t_MyHashMap'0) (k : t_DeepModelTy'0) : int =
     [%#shashmap19] EuclideanDivision.mod (hash_log'0 k) (Seq.length (view'3 self.t_MyHashMap__buckets'0))
   
   function index_logic'0 [@inline:trivial] (self : t_Vec'0) (ix : int) : t_List'0 =
     [%#sindex20] Seq.get (view'3 self) ix
   
-  function bucket'0 [#"hashmap.rs" 122 4 122 54] (self : t_MyHashMap'0) (k : t_DeepModelTy'0) : t_List'0 =
+  function bucket'0 [#"hashmap.rs" 121 4 121 54] (self : t_MyHashMap'0) (k : t_DeepModelTy'0) : t_List'0 =
     [%#shashmap12] index_logic'0 self.t_MyHashMap__buckets'0 (bucket_ix'0 self k)
   
   type t_Option'1  =
@@ -1346,7 +1346,7 @@ module M_hashmap__qyi7664122466964245986__get [#"hashmap.rs" 191 4 191 43] (* My
   
   use prelude.prelude.Intrinsic
   
-  predicate good_bucket'0 [#"hashmap.rs" 132 4 132 57] (self : t_MyHashMap'0) (l : t_List'0) (h : int) =
+  predicate good_bucket'0 [#"hashmap.rs" 131 4 131 57] (self : t_MyHashMap'0) (l : t_List'0) (h : int) =
     [%#shashmap26] forall k : t_DeepModelTy'0, v : t_V'0 . get'1 l k = C_Some'1 v  -> bucket_ix'0 self k = h
   
   predicate no_double_binding'0 [#"hashmap.rs" 39 4 39 38] (self : t_List'0) =
@@ -1355,7 +1355,7 @@ module M_hashmap__qyi7664122466964245986__get [#"hashmap.rs" 191 4 191 43] (* My
       | C_Cons'0 (k, _) tl -> get'1 tl (deep_model'0 k) = C_None'1 /\ no_double_binding'0 tl
       end
   
-  predicate invariant'5 [#"hashmap.rs" 142 4 142 30] (self : t_MyHashMap'0) =
+  predicate invariant'5 [#"hashmap.rs" 141 4 141 30] (self : t_MyHashMap'0) =
     [%#shashmap24] 0 < Seq.length (view'3 self.t_MyHashMap__buckets'0)
     /\ (forall i : int . 0 <= i /\ i < Seq.length (view'3 self.t_MyHashMap__buckets'0)
      -> good_bucket'0 self (index_logic'0 self.t_MyHashMap__buckets'0 i) i
@@ -1395,7 +1395,7 @@ module M_hashmap__qyi7664122466964245986__get [#"hashmap.rs" 191 4 191 43] (* My
   
   use prelude.prelude.Mapping
   
-  function view'2 [#"hashmap.rs" 97 4 97 33] (self : t_MyHashMap'0) : Map.map t_DeepModelTy'0 (t_Option'1) =
+  function view'2 [#"hashmap.rs" 96 4 96 33] (self : t_MyHashMap'0) : Map.map t_DeepModelTy'0 (t_Option'1) =
     [%#shashmap21] Mapping.from_fn (fun (k : t_DeepModelTy'0) -> get'1 (bucket'0 self k) k)
   
   function view'0 (self : t_MyHashMap'0) : Map.map t_DeepModelTy'0 (t_Option'1) =
@@ -1473,37 +1473,37 @@ module M_hashmap__qyi7664122466964245986__get [#"hashmap.rs" 191 4 191 43] (* My
       (! return' {result}) ]
     
 end
-module M_hashmap__qyi7664122466964245986__resize [#"hashmap.rs" 210 4 210 24] (* MyHashMap<K, V> *)
-  let%span shashmap0 = "hashmap.rs" 211 23 211 41
-  let%span shashmap1 = "hashmap.rs" 212 53 212 54
-  let%span shashmap2 = "hashmap.rs" 214 27 214 28
-  let%span shashmap3 = "hashmap.rs" 224 20 224 45
-  let%span shashmap4 = "hashmap.rs" 223 20 223 66
-  let%span shashmap5 = "hashmap.rs" 222 20 222 117
-  let%span shashmap6 = "hashmap.rs" 218 20 220 92
-  let%span shashmap7 = "hashmap.rs" 217 20 217 109
-  let%span shashmap8 = "hashmap.rs" 216 20 216 28
-  let%span shashmap9 = "hashmap.rs" 215 20 215 29
-  let%span shashmap10 = "hashmap.rs" 237 24 237 51
-  let%span shashmap11 = "hashmap.rs" 236 24 236 45
-  let%span shashmap12 = "hashmap.rs" 234 24 235 102
-  let%span shashmap13 = "hashmap.rs" 231 24 232 119
-  let%span shashmap14 = "hashmap.rs" 230 24 230 113
-  let%span shashmap15 = "hashmap.rs" 229 24 229 30
-  let%span shashmap16 = "hashmap.rs" 228 24 228 32
-  let%span shashmap17 = "hashmap.rs" 242 28 242 119
-  let%span shashmap18 = "hashmap.rs" 243 17 243 18
-  let%span shashmap19 = "hashmap.rs" 210 19 210 23
-  let%span shashmap20 = "hashmap.rs" 207 15 207 41
-  let%span shashmap21 = "hashmap.rs" 208 14 208 72
+module M_hashmap__qyi7664122466964245986__resize [#"hashmap.rs" 209 4 209 24] (* MyHashMap<K, V> *)
+  let%span shashmap0 = "hashmap.rs" 210 23 210 41
+  let%span shashmap1 = "hashmap.rs" 211 53 211 54
+  let%span shashmap2 = "hashmap.rs" 213 27 213 28
+  let%span shashmap3 = "hashmap.rs" 223 20 223 45
+  let%span shashmap4 = "hashmap.rs" 222 20 222 66
+  let%span shashmap5 = "hashmap.rs" 221 20 221 117
+  let%span shashmap6 = "hashmap.rs" 217 20 219 92
+  let%span shashmap7 = "hashmap.rs" 216 20 216 109
+  let%span shashmap8 = "hashmap.rs" 215 20 215 28
+  let%span shashmap9 = "hashmap.rs" 214 20 214 29
+  let%span shashmap10 = "hashmap.rs" 236 24 236 51
+  let%span shashmap11 = "hashmap.rs" 235 24 235 45
+  let%span shashmap12 = "hashmap.rs" 233 24 234 102
+  let%span shashmap13 = "hashmap.rs" 230 24 231 119
+  let%span shashmap14 = "hashmap.rs" 229 24 229 113
+  let%span shashmap15 = "hashmap.rs" 228 24 228 30
+  let%span shashmap16 = "hashmap.rs" 227 24 227 32
+  let%span shashmap17 = "hashmap.rs" 241 28 241 119
+  let%span shashmap18 = "hashmap.rs" 242 17 242 18
+  let%span shashmap19 = "hashmap.rs" 209 19 209 23
+  let%span shashmap20 = "hashmap.rs" 206 15 206 41
+  let%span shashmap21 = "hashmap.rs" 207 14 207 72
   let%span svec22 = "../../../creusot-contracts/src/std/vec.rs" 83 26 83 48
-  let%span shashmap23 = "hashmap.rs" 151 15 151 24
-  let%span shashmap24 = "hashmap.rs" 153 31 153 46
-  let%span shashmap25 = "hashmap.rs" 152 14 152 62
+  let%span shashmap23 = "hashmap.rs" 150 15 150 24
+  let%span shashmap24 = "hashmap.rs" 152 31 152 46
+  let%span shashmap25 = "hashmap.rs" 151 14 151 62
   let%span svec26 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41
   let%span sindex27 = "../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31
-  let%span shashmap28 = "hashmap.rs" 128 20 128 66
-  let%span shashmap29 = "hashmap.rs" 98 8 98 33
+  let%span shashmap28 = "hashmap.rs" 127 20 127 66
+  let%span shashmap29 = "hashmap.rs" 97 8 97 33
   let%span ssnapshot30 = "../../../creusot-contracts/src/snapshot.rs" 52 20 52 39
   let%span svec31 = "../../../creusot-contracts/src/std/vec.rs" 152 27 152 46
   let%span svec32 = "../../../creusot-contracts/src/std/vec.rs" 153 26 153 54
@@ -1512,23 +1512,23 @@ module M_hashmap__qyi7664122466964245986__resize [#"hashmap.rs" 210 4 210 24] (*
   let%span svec35 = "../../../creusot-contracts/src/std/vec.rs" 156 26 156 55
   let%span smem36 = "../../../creusot-contracts/src/std/mem.rs" 8 22 8 34
   let%span smem37 = "../../../creusot-contracts/src/std/mem.rs" 9 22 9 37
-  let%span shashmap38 = "hashmap.rs" 134 12 134 91
+  let%span shashmap38 = "hashmap.rs" 133 12 133 91
   let%span shashmap39 = "hashmap.rs" 41 12 44 13
   let%span shashmap40 = "hashmap.rs" 31 12 34 13
-  let%span shashmap41 = "hashmap.rs" 159 20 159 24
-  let%span shashmap42 = "hashmap.rs" 159 26 159 29
-  let%span shashmap43 = "hashmap.rs" 159 34 159 37
-  let%span shashmap44 = "hashmap.rs" 158 14 158 122
+  let%span shashmap41 = "hashmap.rs" 158 20 158 24
+  let%span shashmap42 = "hashmap.rs" 158 26 158 29
+  let%span shashmap43 = "hashmap.rs" 158 34 158 37
+  let%span shashmap44 = "hashmap.rs" 157 14 157 122
   let%span smodel45 = "../../../creusot-contracts/src/model.rs" 106 8 106 22
   let%span smodel46 = "../../../creusot-contracts/src/model.rs" 88 8 88 22
-  let%span shashmap47 = "hashmap.rs" 123 8 123 53
+  let%span shashmap47 = "hashmap.rs" 122 8 122 53
   let%span sslice48 = "../../../creusot-contracts/src/std/slice.rs" 122 20 122 37
   let%span sslice49 = "../../../creusot-contracts/src/std/slice.rs" 129 20 129 37
   let%span sslice50 = "../../../creusot-contracts/src/std/slice.rs" 136 20 136 94
   let%span sresolve51 = "../../../creusot-contracts/src/resolve.rs" 54 20 54 34
-  let%span shashmap52 = "hashmap.rs" 56 12 56 59
-  let%span shashmap53 = "hashmap.rs" 108 12 108 60
-  let%span shashmap54 = "hashmap.rs" 144 12 145 139
+  let%span shashmap52 = "hashmap.rs" 55 12 55 59
+  let%span shashmap53 = "hashmap.rs" 107 12 107 60
+  let%span shashmap54 = "hashmap.rs" 143 12 144 139
   let%span sinvariant55 = "../../../creusot-contracts/src/invariant.rs" 34 20 34 44
   let%span svec56 = "../../../creusot-contracts/src/std/vec.rs" 65 20 65 41
   let%span sinvariant57 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18
@@ -1658,14 +1658,14 @@ module M_hashmap__qyi7664122466964245986__resize [#"hashmap.rs" 210 4 210 24] (*
       | C_Cons'0 (k, v) tl -> if deep_model'0 k = index then C_Some'0 v else get'0 tl index
       end
   
-  function hash_log'0 [#"hashmap.rs" 73 4 73 45] (_1 : t_DeepModelTy'0) : int
+  function hash_log'0 [#"hashmap.rs" 72 4 72 45] (_1 : t_DeepModelTy'0) : int
   
   use int.EuclideanDivision
   
-  function bucket_ix'0 [#"hashmap.rs" 127 4 127 48] (self : t_MyHashMap'0) (k : t_DeepModelTy'0) : int =
+  function bucket_ix'0 [#"hashmap.rs" 126 4 126 48] (self : t_MyHashMap'0) (k : t_DeepModelTy'0) : int =
     [%#shashmap28] EuclideanDivision.mod (hash_log'0 k) (Seq.length (view'0 self.t_MyHashMap__buckets'0))
   
-  predicate good_bucket'0 [#"hashmap.rs" 132 4 132 57] (self : t_MyHashMap'0) (l : t_List'0) (h : int) =
+  predicate good_bucket'0 [#"hashmap.rs" 131 4 131 57] (self : t_MyHashMap'0) (l : t_List'0) (h : int) =
     [%#shashmap38] forall k : t_DeepModelTy'0, v : t_V'0 . get'0 l k = C_Some'0 v  -> bucket_ix'0 self k = h
   
   predicate no_double_binding'0 [#"hashmap.rs" 39 4 39 38] (self : t_List'0) =
@@ -1674,7 +1674,7 @@ module M_hashmap__qyi7664122466964245986__resize [#"hashmap.rs" 210 4 210 24] (*
       | C_Cons'0 (k, _) tl -> get'0 tl (deep_model'0 k) = C_None'0 /\ no_double_binding'0 tl
       end
   
-  predicate invariant'0 [#"hashmap.rs" 142 4 142 30] (self : t_MyHashMap'0) =
+  predicate invariant'0 [#"hashmap.rs" 141 4 141 30] (self : t_MyHashMap'0) =
     [%#shashmap54] 0 < Seq.length (view'0 self.t_MyHashMap__buckets'0)
     /\ (forall i : int . 0 <= i /\ i < Seq.length (view'0 self.t_MyHashMap__buckets'0)
      -> good_bucket'0 self (index_logic'0 self.t_MyHashMap__buckets'0 i) i
@@ -1690,12 +1690,12 @@ module M_hashmap__qyi7664122466964245986__resize [#"hashmap.rs" 210 4 210 24] (*
   
   use map.Map
   
-  function bucket'0 [#"hashmap.rs" 122 4 122 54] (self : t_MyHashMap'0) (k : t_DeepModelTy'0) : t_List'0 =
+  function bucket'0 [#"hashmap.rs" 121 4 121 54] (self : t_MyHashMap'0) (k : t_DeepModelTy'0) : t_List'0 =
     [%#shashmap47] index_logic'0 self.t_MyHashMap__buckets'0 (bucket_ix'0 self k)
   
   use prelude.prelude.Mapping
   
-  function view'1 [#"hashmap.rs" 97 4 97 33] (self : t_MyHashMap'0) : Map.map t_DeepModelTy'0 (t_Option'0) =
+  function view'1 [#"hashmap.rs" 96 4 96 33] (self : t_MyHashMap'0) : Map.map t_DeepModelTy'0 (t_Option'0) =
     [%#shashmap29] Mapping.from_fn (fun (k : t_DeepModelTy'0) -> get'0 (bucket'0 self k) k)
   
   use map.Map
@@ -1814,13 +1814,13 @@ module M_hashmap__qyi7664122466964245986__resize [#"hashmap.rs" 210 4 210 24] (*
   predicate resolve'8 (_1 : t_Option'0) =
     resolve'9 _1
   
-  predicate resolve'5 [#"hashmap.rs" 53 4 53 28] (self : t_List'0) =
+  predicate resolve'5 [#"hashmap.rs" 52 4 52 28] (self : t_List'0) =
     [%#shashmap52] forall k : t_DeepModelTy'0 . resolve'8 (get'0 self k)
   
   predicate resolve'1 (_1 : t_List'0) =
     resolve'5 _1
   
-  predicate resolve'6 [#"hashmap.rs" 105 4 105 28] (self : t_MyHashMap'0) =
+  predicate resolve'6 [#"hashmap.rs" 104 4 104 28] (self : t_MyHashMap'0) =
     [%#shashmap53] forall k : t_DeepModelTy'0 . resolve'8 (Map.get (view'1 self) k)
   
   predicate resolve'2 (_1 : t_MyHashMap'0) =
@@ -2030,51 +2030,51 @@ module M_hashmap__qyi7664122466964245986__resize [#"hashmap.rs" 210 4 210 24] (*
       (! return' {result}) ]
     
 end
-module M_hashmap__main [#"hashmap.rs" 250 0 250 13]
-  let%span shashmap0 = "hashmap.rs" 257 57 257 59
-  let%span shashmap1 = "hashmap.rs" 258 57 258 59
-  let%span shashmap2 = "hashmap.rs" 259 24 259 25
-  let%span shashmap3 = "hashmap.rs" 260 24 260 25
-  let%span shashmap4 = "hashmap.rs" 261 24 261 25
-  let%span shashmap5 = "hashmap.rs" 262 24 262 25
-  let%span shashmap6 = "hashmap.rs" 266 11 266 12
-  let%span shashmap7 = "hashmap.rs" 266 14 266 16
-  let%span shashmap8 = "hashmap.rs" 267 16 267 17
-  let%span shashmap9 = "hashmap.rs" 268 16 268 17
-  let%span shashmap10 = "hashmap.rs" 269 16 269 17
-  let%span shashmap11 = "hashmap.rs" 270 16 270 17
-  let%span shashmap12 = "hashmap.rs" 273 11 273 12
-  let%span shashmap13 = "hashmap.rs" 273 14 273 16
-  let%span shashmap14 = "hashmap.rs" 274 16 274 17
-  let%span shashmap15 = "hashmap.rs" 275 16 275 17
-  let%span shashmap16 = "hashmap.rs" 276 16 276 17
-  let%span shashmap17 = "hashmap.rs" 277 16 277 17
-  let%span shashmap18 = "hashmap.rs" 151 15 151 24
-  let%span shashmap19 = "hashmap.rs" 153 31 153 46
-  let%span shashmap20 = "hashmap.rs" 152 14 152 62
-  let%span shashmap21 = "hashmap.rs" 191 16 191 20
-  let%span shashmap22 = "hashmap.rs" 191 22 191 25
-  let%span shashmap23 = "hashmap.rs" 191 33 191 43
-  let%span shashmap24 = "hashmap.rs" 187 14 190 5
-  let%span shashmap25 = "hashmap.rs" 159 20 159 24
-  let%span shashmap26 = "hashmap.rs" 159 26 159 29
-  let%span shashmap27 = "hashmap.rs" 159 34 159 37
-  let%span shashmap28 = "hashmap.rs" 158 14 158 122
-  let%span shashmap29 = "hashmap.rs" 98 8 98 33
+module M_hashmap__main [#"hashmap.rs" 249 0 249 13]
+  let%span shashmap0 = "hashmap.rs" 256 57 256 59
+  let%span shashmap1 = "hashmap.rs" 257 57 257 59
+  let%span shashmap2 = "hashmap.rs" 258 24 258 25
+  let%span shashmap3 = "hashmap.rs" 259 24 259 25
+  let%span shashmap4 = "hashmap.rs" 260 24 260 25
+  let%span shashmap5 = "hashmap.rs" 261 24 261 25
+  let%span shashmap6 = "hashmap.rs" 265 11 265 12
+  let%span shashmap7 = "hashmap.rs" 265 14 265 16
+  let%span shashmap8 = "hashmap.rs" 266 16 266 17
+  let%span shashmap9 = "hashmap.rs" 267 16 267 17
+  let%span shashmap10 = "hashmap.rs" 268 16 268 17
+  let%span shashmap11 = "hashmap.rs" 269 16 269 17
+  let%span shashmap12 = "hashmap.rs" 272 11 272 12
+  let%span shashmap13 = "hashmap.rs" 272 14 272 16
+  let%span shashmap14 = "hashmap.rs" 273 16 273 17
+  let%span shashmap15 = "hashmap.rs" 274 16 274 17
+  let%span shashmap16 = "hashmap.rs" 275 16 275 17
+  let%span shashmap17 = "hashmap.rs" 276 16 276 17
+  let%span shashmap18 = "hashmap.rs" 150 15 150 24
+  let%span shashmap19 = "hashmap.rs" 152 31 152 46
+  let%span shashmap20 = "hashmap.rs" 151 14 151 62
+  let%span shashmap21 = "hashmap.rs" 190 16 190 20
+  let%span shashmap22 = "hashmap.rs" 190 22 190 25
+  let%span shashmap23 = "hashmap.rs" 190 33 190 43
+  let%span shashmap24 = "hashmap.rs" 186 14 189 5
+  let%span shashmap25 = "hashmap.rs" 158 20 158 24
+  let%span shashmap26 = "hashmap.rs" 158 26 158 29
+  let%span shashmap27 = "hashmap.rs" 158 34 158 37
+  let%span shashmap28 = "hashmap.rs" 157 14 157 122
+  let%span shashmap29 = "hashmap.rs" 97 8 97 33
   let%span smodel30 = "../../../creusot-contracts/src/model.rs" 88 8 88 22
   let%span snum31 = "../../../creusot-contracts/src/std/num.rs" 21 28 21 33
   let%span smodel32 = "../../../creusot-contracts/src/model.rs" 106 8 106 22
-  let%span shashmap33 = "hashmap.rs" 123 8 123 53
+  let%span shashmap33 = "hashmap.rs" 122 8 122 53
   let%span shashmap34 = "hashmap.rs" 31 12 34 13
-  let%span shashmap35 = "hashmap.rs" 144 12 145 139
-  let%span shashmap36 = "hashmap.rs" 128 20 128 66
+  let%span shashmap35 = "hashmap.rs" 143 12 144 139
+  let%span shashmap36 = "hashmap.rs" 127 20 127 66
   let%span sindex37 = "../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31
   let%span sinvariant38 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18
   let%span svec39 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41
-  let%span shashmap40 = "hashmap.rs" 134 12 134 91
+  let%span shashmap40 = "hashmap.rs" 133 12 133 91
   let%span shashmap41 = "hashmap.rs" 41 12 44 13
   let%span sinvariant42 = "../../../creusot-contracts/src/invariant.rs" 34 20 34 44
-  let%span shashmap43 = "hashmap.rs" 84 20 84 21
+  let%span shashmap43 = "hashmap.rs" 83 20 83 21
   
   use prelude.prelude.UIntSize
   
@@ -2136,15 +2136,15 @@ module M_hashmap__main [#"hashmap.rs" 250 0 250 13]
       | C_Cons'0 (k, v) tl -> if deep_model'0 k = index then C_Some'1 v else get'1 tl index
       end
   
-  function hash_log'0 [#"hashmap.rs" 83 4 83 30] (x : int) : int =
+  function hash_log'0 [#"hashmap.rs" 82 4 82 30] (x : int) : int =
     [%#shashmap43] x
   
   use int.EuclideanDivision
   
-  function bucket_ix'0 [#"hashmap.rs" 127 4 127 48] (self : t_MyHashMap'0) (k : int) : int =
+  function bucket_ix'0 [#"hashmap.rs" 126 4 126 48] (self : t_MyHashMap'0) (k : int) : int =
     [%#shashmap36] EuclideanDivision.mod (hash_log'0 k) (Seq.length (view'3 self.t_MyHashMap__buckets'0))
   
-  predicate good_bucket'0 [#"hashmap.rs" 132 4 132 57] (self : t_MyHashMap'0) (l : t_List'0) (h : int) =
+  predicate good_bucket'0 [#"hashmap.rs" 131 4 131 57] (self : t_MyHashMap'0) (l : t_List'0) (h : int) =
     [%#shashmap40] forall k : int, v : isize . get'1 l k = C_Some'1 v  -> bucket_ix'0 self k = h
   
   predicate no_double_binding'0 [#"hashmap.rs" 39 4 39 38] (self : t_List'0) =
@@ -2153,7 +2153,7 @@ module M_hashmap__main [#"hashmap.rs" 250 0 250 13]
       | C_Cons'0 (k, _) tl -> get'1 tl (deep_model'0 k) = C_None'0 /\ no_double_binding'0 tl
       end
   
-  predicate invariant'0 [#"hashmap.rs" 142 4 142 30] (self : t_MyHashMap'0) =
+  predicate invariant'0 [#"hashmap.rs" 141 4 141 30] (self : t_MyHashMap'0) =
     [%#shashmap35] 0 < Seq.length (view'3 self.t_MyHashMap__buckets'0)
     /\ (forall i : int . 0 <= i /\ i < Seq.length (view'3 self.t_MyHashMap__buckets'0)
      -> good_bucket'0 self (index_logic'0 self.t_MyHashMap__buckets'0 i) i
@@ -2169,12 +2169,12 @@ module M_hashmap__main [#"hashmap.rs" 250 0 250 13]
   
   use map.Map
   
-  function bucket'0 [#"hashmap.rs" 122 4 122 54] (self : t_MyHashMap'0) (k : int) : t_List'0 =
+  function bucket'0 [#"hashmap.rs" 121 4 121 54] (self : t_MyHashMap'0) (k : int) : t_List'0 =
     [%#shashmap33] index_logic'0 self.t_MyHashMap__buckets'0 (bucket_ix'0 self k)
   
   use prelude.prelude.Mapping
   
-  function view'0 [#"hashmap.rs" 97 4 97 33] (self : t_MyHashMap'0) : Map.map int (t_Option'1) =
+  function view'0 [#"hashmap.rs" 96 4 96 33] (self : t_MyHashMap'0) : Map.map int (t_Option'1) =
     [%#shashmap29] Mapping.from_fn (fun (k : int) -> get'1 (bucket'0 self k) k)
   
   use map.Map
@@ -2386,9 +2386,9 @@ module M_hashmap__qyi11479661188956547742__clone__refines [#"hashmap.rs" 17 4 17
   goal refines : [%#shashmap0] forall self : t_List'0 . inv'0 self
    -> inv'0 self /\ (forall result : t_List'0 . result = self /\ inv'1 result  -> result = self /\ inv'1 result)
 end
-module M_hashmap__qyi15610519155507183510__resolve_coherence__refines [#"hashmap.rs" 64 4 64 31] (* <List<(K, V)> as creusot_contracts::Resolve> *)
-  let%span shashmap0 = "hashmap.rs" 64 4 64 31
-  let%span shashmap1 = "hashmap.rs" 56 12 56 59
+module M_hashmap__qyi15610519155507183510__resolve_coherence__refines [#"hashmap.rs" 63 4 63 31] (* <List<(K, V)> as creusot_contracts::Resolve> *)
+  let%span shashmap0 = "hashmap.rs" 63 4 63 31
+  let%span shashmap1 = "hashmap.rs" 55 12 55 59
   let%span shashmap2 = "hashmap.rs" 31 12 34 13
   let%span sresolve3 = "../../../creusot-contracts/src/resolve.rs" 68 8 68 23
   let%span sresolve4 = "../../../creusot-contracts/src/resolve.rs" 40 8 40 44
@@ -2431,7 +2431,7 @@ module M_hashmap__qyi15610519155507183510__resolve_coherence__refines [#"hashmap
   predicate resolve'3 (_1 : t_Option'0) =
     resolve'6 _1
   
-  predicate resolve'0 [#"hashmap.rs" 53 4 53 28] (self : t_List'0) =
+  predicate resolve'0 [#"hashmap.rs" 52 4 52 28] (self : t_List'0) =
     [%#shashmap1] forall k : t_DeepModelTy'0 . resolve'3 (get'0 self k)
   
   predicate resolve'7 (_1 : t_List'0) =
@@ -2491,21 +2491,21 @@ module M_hashmap__qyi15610519155507183510__resolve_coherence__refines [#"hashmap
   goal refines : [%#shashmap0] forall self : t_List'0 . structural_resolve'0 self /\ inv'0 self
    -> structural_resolve'0 self /\ (forall result : () . resolve'0 self  -> resolve'0 self)
 end
-module M_hashmap__qyi15467499327297494705__resolve_coherence__refines [#"hashmap.rs" 117 4 117 31] (* <MyHashMap<K, V> as creusot_contracts::Resolve> *)
-  let%span shashmap0 = "hashmap.rs" 117 4 117 31
-  let%span shashmap1 = "hashmap.rs" 108 12 108 60
-  let%span shashmap2 = "hashmap.rs" 98 8 98 33
+module M_hashmap__qyi15467499327297494705__resolve_coherence__refines [#"hashmap.rs" 116 4 116 31] (* <MyHashMap<K, V> as creusot_contracts::Resolve> *)
+  let%span shashmap0 = "hashmap.rs" 116 4 116 31
+  let%span shashmap1 = "hashmap.rs" 107 12 107 60
+  let%span shashmap2 = "hashmap.rs" 97 8 97 33
   let%span svec3 = "../../../creusot-contracts/src/std/vec.rs" 49 20 49 83
   let%span sinvariant4 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18
-  let%span shashmap5 = "hashmap.rs" 123 8 123 53
+  let%span shashmap5 = "hashmap.rs" 122 8 122 53
   let%span shashmap6 = "hashmap.rs" 31 12 34 13
   let%span sresolve7 = "../../../creusot-contracts/src/resolve.rs" 82 8 85 9
   let%span svec8 = "../../../creusot-contracts/src/std/vec.rs" 18 14 18 41
   let%span sindex9 = "../../../creusot-contracts/src/logic/ops/index.rs" 23 8 23 31
-  let%span shashmap10 = "hashmap.rs" 128 20 128 66
-  let%span shashmap11 = "hashmap.rs" 56 12 56 59
-  let%span shashmap12 = "hashmap.rs" 144 12 145 139
-  let%span shashmap13 = "hashmap.rs" 134 12 134 91
+  let%span shashmap10 = "hashmap.rs" 127 20 127 66
+  let%span shashmap11 = "hashmap.rs" 55 12 55 59
+  let%span shashmap12 = "hashmap.rs" 143 12 144 139
+  let%span shashmap13 = "hashmap.rs" 133 12 133 91
   let%span shashmap14 = "hashmap.rs" 41 12 44 13
   let%span svec15 = "../../../creusot-contracts/src/std/vec.rs" 65 20 65 41
   let%span sseq16 = "../../../creusot-contracts/src/logic/seq.rs" 611 20 611 95
@@ -2587,7 +2587,7 @@ module M_hashmap__qyi15467499327297494705__resolve_coherence__refines [#"hashmap
   predicate resolve'2 (_1 : t_Option'0) =
     resolve'4 _1
   
-  predicate resolve'7 [#"hashmap.rs" 53 4 53 28] (self : t_List'0) =
+  predicate resolve'7 [#"hashmap.rs" 52 4 52 28] (self : t_List'0) =
     [%#shashmap11] forall k : t_DeepModelTy'0 . resolve'2 (get'0 self k)
   
   predicate resolve'5 (_1 : t_List'0) =
@@ -2604,14 +2604,14 @@ module M_hashmap__qyi15467499327297494705__resolve_coherence__refines [#"hashmap
       | {t_MyHashMap__buckets'0 = x0} -> resolve'1 x0
       end
   
-  function hash_log'0 [#"hashmap.rs" 73 4 73 45] (_1 : t_DeepModelTy'0) : int
+  function hash_log'0 [#"hashmap.rs" 72 4 72 45] (_1 : t_DeepModelTy'0) : int
   
   use int.EuclideanDivision
   
-  function bucket_ix'0 [#"hashmap.rs" 127 4 127 48] (self : t_MyHashMap'0) (k : t_DeepModelTy'0) : int =
+  function bucket_ix'0 [#"hashmap.rs" 126 4 126 48] (self : t_MyHashMap'0) (k : t_DeepModelTy'0) : int =
     [%#shashmap10] EuclideanDivision.mod (hash_log'0 k) (Seq.length (view'1 self.t_MyHashMap__buckets'0))
   
-  predicate good_bucket'0 [#"hashmap.rs" 132 4 132 57] (self : t_MyHashMap'0) (l : t_List'0) (h : int) =
+  predicate good_bucket'0 [#"hashmap.rs" 131 4 131 57] (self : t_MyHashMap'0) (l : t_List'0) (h : int) =
     [%#shashmap13] forall k : t_DeepModelTy'0, v : t_V'0 . get'0 l k = C_Some'0 v  -> bucket_ix'0 self k = h
   
   predicate no_double_binding'0 [#"hashmap.rs" 39 4 39 38] (self : t_List'0) =
@@ -2620,7 +2620,7 @@ module M_hashmap__qyi15467499327297494705__resolve_coherence__refines [#"hashmap
       | C_Cons'0 (k, _) tl -> get'0 tl (deep_model'0 k) = C_None'0 /\ no_double_binding'0 tl
       end
   
-  predicate invariant'1 [#"hashmap.rs" 142 4 142 30] (self : t_MyHashMap'0) =
+  predicate invariant'1 [#"hashmap.rs" 141 4 141 30] (self : t_MyHashMap'0) =
     [%#shashmap12] 0 < Seq.length (view'1 self.t_MyHashMap__buckets'0)
     /\ (forall i : int . 0 <= i /\ i < Seq.length (view'1 self.t_MyHashMap__buckets'0)
      -> good_bucket'0 self (index_logic'0 self.t_MyHashMap__buckets'0 i) i
@@ -2683,26 +2683,26 @@ module M_hashmap__qyi15467499327297494705__resolve_coherence__refines [#"hashmap
   
   use map.Map
   
-  function bucket'0 [#"hashmap.rs" 122 4 122 54] (self : t_MyHashMap'0) (k : t_DeepModelTy'0) : t_List'0 =
+  function bucket'0 [#"hashmap.rs" 121 4 121 54] (self : t_MyHashMap'0) (k : t_DeepModelTy'0) : t_List'0 =
     [%#shashmap5] index_logic'0 self.t_MyHashMap__buckets'0 (bucket_ix'0 self k)
   
   use prelude.prelude.Mapping
   
-  function view'0 [#"hashmap.rs" 97 4 97 33] (self : t_MyHashMap'0) : Map.map t_DeepModelTy'0 (t_Option'0) =
+  function view'0 [#"hashmap.rs" 96 4 96 33] (self : t_MyHashMap'0) : Map.map t_DeepModelTy'0 (t_Option'0) =
     [%#shashmap2] Mapping.from_fn (fun (k : t_DeepModelTy'0) -> get'0 (bucket'0 self k) k)
   
   use map.Map
   
-  predicate resolve'0 [#"hashmap.rs" 105 4 105 28] (self : t_MyHashMap'0) =
+  predicate resolve'0 [#"hashmap.rs" 104 4 104 28] (self : t_MyHashMap'0) =
     [%#shashmap1] forall k : t_DeepModelTy'0 . resolve'2 (Map.get (view'0 self) k)
   
   goal refines : [%#shashmap0] forall self : t_MyHashMap'0 . structural_resolve'0 self /\ inv'0 self
    -> structural_resolve'0 self /\ inv'0 self /\ (forall result : () . resolve'0 self  -> resolve'0 self)
 end
-module M_hashmap__qyi9060063638777358169__hash__refines [#"hashmap.rs" 78 4 78 25] (* <usize as Hash> *)
-  let%span shashmap0 = "hashmap.rs" 78 4 78 25
+module M_hashmap__qyi9060063638777358169__hash__refines [#"hashmap.rs" 77 4 77 25] (* <usize as Hash> *)
+  let%span shashmap0 = "hashmap.rs" 77 4 77 25
   let%span smodel1 = "../../../creusot-contracts/src/model.rs" 79 8 79 28
-  let%span shashmap2 = "hashmap.rs" 84 20 84 21
+  let%span shashmap2 = "hashmap.rs" 83 20 83 21
   let%span snum3 = "../../../creusot-contracts/src/std/num.rs" 21 28 21 33
   
   use prelude.prelude.Borrow
@@ -2727,7 +2727,7 @@ module M_hashmap__qyi9060063638777358169__hash__refines [#"hashmap.rs" 78 4 78 2
   function deep_model'0 (self : usize) : int =
     [%#smodel1] deep_model'1 self
   
-  function hash_log'0 [#"hashmap.rs" 83 4 83 30] (x : int) : int =
+  function hash_log'0 [#"hashmap.rs" 82 4 82 30] (x : int) : int =
     [%#shashmap2] x
   
   goal refines : [%#shashmap0] forall self : usize . inv'0 self