diff --git a/creusot/tests/creusot-contracts/creusot-contracts.coma b/creusot/tests/creusot-contracts/creusot-contracts.coma
index 73be482c3..18ea63ee9 100644
--- a/creusot/tests/creusot-contracts/creusot-contracts.coma
+++ b/creusot/tests/creusot-contracts/creusot-contracts.coma
@@ -8789,8 +8789,8 @@ module M_creusot_contracts__logic__fmap__qyi9892930999379617882__contains_ghost
   let%span sfmap8 = "../../../creusot-contracts/src/logic/fmap.rs" 132 8 132 35
   let%span sfmap9 = "../../../creusot-contracts/src/logic/fmap.rs" 124 8 124 35
   let%span sfmap10 = "../../../creusot-contracts/src/logic/fmap.rs" 103 8 103 26
-  let%span sutil11 = "../../../creusot-contracts/src/util.rs" 43 11 43 21
-  let%span sutil12 = "../../../creusot-contracts/src/util.rs" 44 10 44 28
+  let%span sutil11 = "../../../creusot-contracts/src/util.rs" 57 11 57 21
+  let%span sutil12 = "../../../creusot-contracts/src/util.rs" 58 10 58 28
   let%span sinvariant13 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18
   let%span sfmap14 = "../../../creusot-contracts/src/logic/fmap.rs" 58 14 58 86
   let%span sfmap15 = "../../../creusot-contracts/src/logic/fmap.rs" 452 20 452 91
@@ -8830,7 +8830,7 @@ module M_creusot_contracts__logic__fmap__qyi9892930999379617882__contains_ghost
   
   predicate inv'6 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_K'0)
   
-  function unwrap'0 [#"../../../creusot-contracts/src/util.rs" 45 0 45 36] (op : t_Option'1) : t_V'0
+  function unwrap'0 [#"../../../creusot-contracts/src/util.rs" 59 0 59 36] (op : t_Option'1) : t_V'0
   
   axiom unwrap'0_spec : forall op : t_Option'1 . ([%#sutil11] op <> C_None'1)
    -> ([%#sutil12] C_Some'1 (unwrap'0 op) = op)
@@ -14129,13 +14129,13 @@ module M_creusot_contracts__snapshot__qyi5567339964777190687__clone [#"../../../
       (! return' {result}) ]
     
 end
-module M_creusot_contracts__util__unwrap [#"../../../creusot-contracts/src/util.rs" 45 0 45 36]
-  let%span sutil0 = "../../../creusot-contracts/src/util.rs" 43 11 43 21
-  let%span sutil1 = "../../../creusot-contracts/src/util.rs" 44 10 44 28
-  let%span sutil2 = "../../../creusot-contracts/src/util.rs" 33 11 33 16
-  let%span sutil3 = "../../../creusot-contracts/src/util.rs" 34 10 34 15
-  let%span sutil4 = "../../../creusot-contracts/src/util.rs" 35 10 35 11
-  let%span sutil5 = "../../../creusot-contracts/src/util.rs" 46 4 49 5
+module M_creusot_contracts__util__unwrap [#"../../../creusot-contracts/src/util.rs" 59 0 59 36]
+  let%span sutil0 = "../../../creusot-contracts/src/util.rs" 57 11 57 21
+  let%span sutil1 = "../../../creusot-contracts/src/util.rs" 58 10 58 28
+  let%span sutil2 = "../../../creusot-contracts/src/util.rs" 47 11 47 16
+  let%span sutil3 = "../../../creusot-contracts/src/util.rs" 48 10 48 15
+  let%span sutil4 = "../../../creusot-contracts/src/util.rs" 49 10 49 11
+  let%span sutil5 = "../../../creusot-contracts/src/util.rs" 60 4 63 5
   
   type t_T'0
   
@@ -14143,13 +14143,13 @@ module M_creusot_contracts__util__unwrap [#"../../../creusot-contracts/src/util.
     | C_None'0
     | C_Some'0 t_T'0
   
-  function unreachable'0 [#"../../../creusot-contracts/src/util.rs" 36 0 36 28] (_1 : ()) : t_T'0
+  function unreachable'0 [#"../../../creusot-contracts/src/util.rs" 50 0 50 28] (_1 : ()) : t_T'0
   
   axiom unreachable'0_spec : forall _1 : () . ([%#sutil2] false)  -> ([%#sutil3] false)
   
   constant op  : t_Option'0
   
-  function unwrap'0 [#"../../../creusot-contracts/src/util.rs" 45 0 45 36] (op : t_Option'0) : t_T'0
+  function unwrap'0 [#"../../../creusot-contracts/src/util.rs" 59 0 59 36] (op : t_Option'0) : t_T'0
   
   goal vc_unwrap'0 : ([%#sutil0] op <> C_None'0)
    -> match op with
@@ -24680,8 +24680,8 @@ module M_creusot_contracts__logic__fmap__qyi4648834920430559677__clone__refines
   let%span sfmap3 = "../../../creusot-contracts/src/logic/fmap.rs" 132 8 132 35
   let%span sfmap4 = "../../../creusot-contracts/src/logic/fmap.rs" 124 8 124 35
   let%span sfmap5 = "../../../creusot-contracts/src/logic/fmap.rs" 103 8 103 26
-  let%span sutil6 = "../../../creusot-contracts/src/util.rs" 43 11 43 21
-  let%span sutil7 = "../../../creusot-contracts/src/util.rs" 44 10 44 28
+  let%span sutil6 = "../../../creusot-contracts/src/util.rs" 57 11 57 21
+  let%span sutil7 = "../../../creusot-contracts/src/util.rs" 58 10 58 28
   let%span sfmap8 = "../../../creusot-contracts/src/logic/fmap.rs" 58 14 58 86
   let%span sboxed9 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
   
@@ -24719,7 +24719,7 @@ module M_creusot_contracts__logic__fmap__qyi4648834920430559677__clone__refines
   
   predicate inv'2 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_K'0)
   
-  function unwrap'0 [#"../../../creusot-contracts/src/util.rs" 45 0 45 36] (op : t_Option'0) : t_V'0
+  function unwrap'0 [#"../../../creusot-contracts/src/util.rs" 59 0 59 36] (op : t_Option'0) : t_V'0
   
   axiom unwrap'0_spec : forall op : t_Option'0 . ([%#sutil6] op <> C_None'0)
    -> ([%#sutil7] C_Some'0 (unwrap'0 op) = op)