diff --git a/creusot-contracts/src/ptr_own.rs b/creusot-contracts/src/ptr_own.rs
index 4a0974982c..86f34102f9 100644
--- a/creusot-contracts/src/ptr_own.rs
+++ b/creusot-contracts/src/ptr_own.rs
@@ -18,12 +18,14 @@ pub type RawPtr<T> = *const T;
 pub struct PtrOwn<T: ?Sized>(std::marker::PhantomData<T>);
 
 impl<T: ?Sized> PtrOwn<T> {
+    /// The raw pointer whose ownership is tracked by this [PtrOwn]
     #[trusted]
     #[logic]
     pub fn ptr(&self) -> RawPtr<T> {
         dead
     }
 
+    /// The value currently stored at address [self.ptr()]
     #[trusted]
     #[logic]
     pub fn val(&self) -> SizedW<T> {
@@ -41,61 +43,65 @@ impl<T: ?Sized> Invariant for PtrOwn<T> {
     }
 }
 
-/// Creates a new [PtrOwn] and associated [RawPtr] by allocating a new memory
-/// cell initialized with `v`.
-#[ensures(result.1.ptr() == result.0 && *result.1.val() == v)]
-pub fn new<T>(v: T) -> (RawPtr<T>, GhostBox<PtrOwn<T>>) {
-    from_box(Box::new(v))
+impl<T> PtrOwn<T> {
+    /// Creates a new [PtrOwn] and associated [RawPtr] by allocating a new memory
+    /// cell initialized with `v`.
+    #[ensures(result.1.ptr() == result.0 && *result.1.val() == v)]
+    pub fn new(v: T) -> (RawPtr<T>, GhostBox<PtrOwn<T>>) {
+        Self::from_box(Box::new(v))
+    }
 }
 
-/// Creates a ghost [PtrOwn] and associated [RawPtr] from an existing [Box].
-#[trusted]
-#[ensures(result.1.ptr() == result.0 && *result.1.val() == *val)]
-pub fn from_box<T: ?Sized>(val: Box<T>) -> (RawPtr<T>, GhostBox<PtrOwn<T>>) {
-    assert!(core::mem::size_of_val::<T>(&*val) > 0, "PtrOwn doesn't support ZSTs");
-    (Box::into_raw(val), GhostBox::conjure())
-}
+impl<T: ?Sized> PtrOwn<T> {
+    /// Creates a ghost [PtrOwn] and associated [RawPtr] from an existing [Box].
+    #[trusted]
+    #[ensures(result.1.ptr() == result.0 && *result.1.val() == *val)]
+    pub fn from_box(val: Box<T>) -> (RawPtr<T>, GhostBox<PtrOwn<T>>) {
+        assert!(core::mem::size_of_val::<T>(&*val) > 0, "PtrOwn doesn't support ZSTs");
+        (Box::into_raw(val), GhostBox::conjure())
+    }
 
-/// Immutably borrows the underlying `T`.
-#[trusted]
-#[requires(ptr == own.ptr())]
-#[ensures(*result == *own.val())]
-#[allow(unused_variables)]
-pub fn as_ref<T: ?Sized>(ptr: RawPtr<T>, own: GhostBox<&PtrOwn<T>>) -> &T {
-    unsafe { &*ptr }
-}
+    /// Immutably borrows the underlying `T`.
+    #[trusted]
+    #[requires(ptr == own.ptr())]
+    #[ensures(*result == *own.val())]
+    #[allow(unused_variables)]
+    pub fn as_ref(ptr: RawPtr<T>, own: GhostBox<&PtrOwn<T>>) -> &T {
+        unsafe { &*ptr }
+    }
 
-/// Mutably borrows the underlying `T`.
-#[trusted]
-#[allow(unused_variables)]
-#[requires(ptr == own.ptr())]
-#[ensures(*result == *own.val())]
-// Currently .inner_logic() is needed instead of *; see issue #1257
-#[ensures((^own.inner_logic()).ptr() == own.ptr())]
-#[ensures(*(^own.inner_logic()).val() == ^result)]
-pub fn as_mut<T: ?Sized>(ptr: RawPtr<T>, own: GhostBox<&mut PtrOwn<T>>) -> &mut T {
-    unsafe { &mut *(ptr as *mut _) }
-}
+    /// Mutably borrows the underlying `T`.
+    #[trusted]
+    #[allow(unused_variables)]
+    #[requires(ptr == own.ptr())]
+    #[ensures(*result == *own.val())]
+    // Currently .inner_logic() is needed instead of *; see issue #1257
+    #[ensures((^own.inner_logic()).ptr() == own.ptr())]
+    #[ensures(*(^own.inner_logic()).val() == ^result)]
+    pub fn as_mut(ptr: RawPtr<T>, own: GhostBox<&mut PtrOwn<T>>) -> &mut T {
+        unsafe { &mut *(ptr as *mut _) }
+    }
 
-/// Transfers ownership of `own` back into a [Box].
-#[trusted]
-#[requires(ptr == own.ptr())]
-#[ensures(*result == *own.val())]
-#[allow(unused_variables)]
-pub fn to_box<T: ?Sized>(ptr: RawPtr<T>, own: GhostBox<PtrOwn<T>>) -> Box<T> {
-    unsafe { Box::from_raw(ptr as *mut _) }
-}
+    /// Transfers ownership of `own` back into a [Box].
+    #[trusted]
+    #[requires(ptr == own.ptr())]
+    #[ensures(*result == *own.val())]
+    #[allow(unused_variables)]
+    pub fn to_box(ptr: RawPtr<T>, own: GhostBox<PtrOwn<T>>) -> Box<T> {
+        unsafe { Box::from_raw(ptr as *mut _) }
+    }
 
-/// Deallocates the memory pointed by `ptr`.
-#[requires(ptr == own.ptr())]
-pub fn drop<T: ?Sized>(ptr: RawPtr<T>, own: GhostBox<PtrOwn<T>>) {
-    let _ = to_box(ptr, own);
-}
+    /// Deallocates the memory pointed by `ptr`.
+    #[requires(ptr == own.ptr())]
+    pub fn drop(ptr: RawPtr<T>, own: GhostBox<PtrOwn<T>>) {
+        let _ = Self::to_box(ptr, own);
+    }
 
-/// If one owns two [PtrOwn]s in ghost code, then they are for different pointers.
-#[trusted]
-#[ensures(own1.ptr().addr_logic() != own2.ptr().addr_logic())]
-#[allow(unused_variables)]
-pub fn disjoint_lemma<T: ?Sized>(own1: &mut PtrOwn<T>, own2: &mut PtrOwn<T>) {
-    panic!()
+    /// If one owns two [PtrOwn]s in ghost code, then they are for different pointers.
+    #[trusted]
+    #[ensures(own1.ptr().addr_logic() != own2.ptr().addr_logic())]
+    #[allow(unused_variables)]
+    pub fn disjoint_lemma(own1: &mut PtrOwn<T>, own2: &mut PtrOwn<T>) {
+        panic!()
+    }
 }
diff --git a/creusot/tests/creusot-contracts/creusot-contracts.coma b/creusot/tests/creusot-contracts/creusot-contracts.coma
index a82a055090..76d6b80288 100644
--- a/creusot/tests/creusot-contracts/creusot-contracts.coma
+++ b/creusot/tests/creusot-contracts/creusot-contracts.coma
@@ -15068,16 +15068,16 @@ module M_creusot_contracts__snapshot__qyi5567339964777190687__clone [#"../../../
       (! return' {result}) ]
     
 end
-module M_creusot_contracts__ptr_own__new [#"../../../creusot-contracts/src/ptr_own.rs" 47 0 47 55]
-  let%span sptr_own0 = "../../../creusot-contracts/src/ptr_own.rs" 47 14 47 15
-  let%span sptr_own1 = "../../../creusot-contracts/src/ptr_own.rs" 47 23 47 55
-  let%span sptr_own2 = "../../../creusot-contracts/src/ptr_own.rs" 46 10 46 60
-  let%span sptr_own3 = "../../../creusot-contracts/src/ptr_own.rs" 54 27 54 30
-  let%span sptr_own4 = "../../../creusot-contracts/src/ptr_own.rs" 54 43 54 75
-  let%span sptr_own5 = "../../../creusot-contracts/src/ptr_own.rs" 53 10 53 63
+module M_creusot_contracts__ptr_own__qyi17842610664047605351__new [#"../../../creusot-contracts/src/ptr_own.rs" 50 4 50 56] (* ptr_own::PtrOwn<T> *)
+  let%span sptr_own0 = "../../../creusot-contracts/src/ptr_own.rs" 50 15 50 16
+  let%span sptr_own1 = "../../../creusot-contracts/src/ptr_own.rs" 50 24 50 56
+  let%span sptr_own2 = "../../../creusot-contracts/src/ptr_own.rs" 49 14 49 64
+  let%span sptr_own3 = "../../../creusot-contracts/src/ptr_own.rs" 59 20 59 23
+  let%span sptr_own4 = "../../../creusot-contracts/src/ptr_own.rs" 59 36 59 68
+  let%span sptr_own5 = "../../../creusot-contracts/src/ptr_own.rs" 58 14 58 67
   let%span sghost6 = "../../../creusot-contracts/src/ghost.rs" 200 9 200 15
   let%span sboxed7 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
-  let%span sptr_own8 = "../../../creusot-contracts/src/ptr_own.rs" 40 20 40 66
+  let%span sptr_own8 = "../../../creusot-contracts/src/ptr_own.rs" 42 20 42 66
   let%span sptr9 = "../../../creusot-contracts/src/std/ptr.rs" 81 8 81 30
   
   type t_T'0
@@ -15100,7 +15100,7 @@ module M_creusot_contracts__ptr_own__new [#"../../../creusot-contracts/src/ptr_o
   
   use prelude.prelude.Borrow
   
-  function ptr'0 [#"../../../creusot-contracts/src/ptr_own.rs" 23 4 23 34] (self : t_PtrOwn'0) : opaque_ptr
+  function ptr'0 [#"../../../creusot-contracts/src/ptr_own.rs" 24 4 24 34] (self : t_PtrOwn'0) : opaque_ptr
   
   use prelude.prelude.Int
   
@@ -15109,9 +15109,9 @@ module M_creusot_contracts__ptr_own__new [#"../../../creusot-contracts/src/ptr_o
   function is_null_logic'0 [#"../../../creusot-contracts/src/std/ptr.rs" 80 4 80 34] (self : opaque_ptr) : bool =
     [%#sptr9] addr_logic'0 self = 0
   
-  function val'0 [#"../../../creusot-contracts/src/ptr_own.rs" 29 4 29 34] (self : t_PtrOwn'0) : t_T'0
+  function val'0 [#"../../../creusot-contracts/src/ptr_own.rs" 31 4 31 34] (self : t_PtrOwn'0) : t_T'0
   
-  predicate invariant'2 [#"../../../creusot-contracts/src/ptr_own.rs" 39 4 39 30] (self : t_PtrOwn'0) =
+  predicate invariant'2 [#"../../../creusot-contracts/src/ptr_own.rs" 41 4 41 30] (self : t_PtrOwn'0) =
     [%#sptr_own8] not is_null_logic'0 (ptr'0 self) /\ inv'2 (val'0 self)
   
   predicate inv'5 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_PtrOwn'0)
@@ -15166,17 +15166,17 @@ module M_creusot_contracts__ptr_own__new [#"../../../creusot-contracts/src/ptr_o
       (! return' {result}) ]
     
 end
-module M_creusot_contracts__ptr_own__drop [#"../../../creusot-contracts/src/ptr_own.rs" 91 0 91 64]
-  let%span sptr_own0 = "../../../creusot-contracts/src/ptr_own.rs" 91 39 91 42
-  let%span sptr_own1 = "../../../creusot-contracts/src/ptr_own.rs" 90 11 90 27
-  let%span sptr_own2 = "../../../creusot-contracts/src/ptr_own.rs" 85 41 85 44
-  let%span sptr_own3 = "../../../creusot-contracts/src/ptr_own.rs" 82 11 82 27
-  let%span sptr_own4 = "../../../creusot-contracts/src/ptr_own.rs" 85 70 85 76
-  let%span sptr_own5 = "../../../creusot-contracts/src/ptr_own.rs" 83 10 83 31
+module M_creusot_contracts__ptr_own__qyi17842610664047605351__drop [#"../../../creusot-contracts/src/ptr_own.rs" 96 4 96 57] (* ptr_own::PtrOwn<T> *)
+  let%span sptr_own0 = "../../../creusot-contracts/src/ptr_own.rs" 96 32 96 35
+  let%span sptr_own1 = "../../../creusot-contracts/src/ptr_own.rs" 95 15 95 31
+  let%span sptr_own2 = "../../../creusot-contracts/src/ptr_own.rs" 90 34 90 37
+  let%span sptr_own3 = "../../../creusot-contracts/src/ptr_own.rs" 87 15 87 31
+  let%span sptr_own4 = "../../../creusot-contracts/src/ptr_own.rs" 90 63 90 69
+  let%span sptr_own5 = "../../../creusot-contracts/src/ptr_own.rs" 88 14 88 35
   let%span sghost6 = "../../../creusot-contracts/src/ghost.rs" 200 9 200 15
   let%span sresolve7 = "../../../creusot-contracts/src/resolve.rs" 68 8 68 23
   let%span sboxed8 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
-  let%span sptr_own9 = "../../../creusot-contracts/src/ptr_own.rs" 40 20 40 66
+  let%span sptr_own9 = "../../../creusot-contracts/src/ptr_own.rs" 42 20 42 66
   let%span sptr10 = "../../../creusot-contracts/src/std/ptr.rs" 81 8 81 30
   
   type t_PtrOwn'0
@@ -15188,7 +15188,7 @@ module M_creusot_contracts__ptr_own__drop [#"../../../creusot-contracts/src/ptr_
   
   use prelude.prelude.Opaque
   
-  function ptr'0 [#"../../../creusot-contracts/src/ptr_own.rs" 23 4 23 34] (self : t_PtrOwn'0) : opaque_ptr
+  function ptr'0 [#"../../../creusot-contracts/src/ptr_own.rs" 24 4 24 34] (self : t_PtrOwn'0) : opaque_ptr
   
   use prelude.prelude.Int
   
@@ -15199,7 +15199,7 @@ module M_creusot_contracts__ptr_own__drop [#"../../../creusot-contracts/src/ptr_
   
   type t_T'0
   
-  function val'0 [#"../../../creusot-contracts/src/ptr_own.rs" 29 4 29 34] (self : t_PtrOwn'0) : t_T'0
+  function val'0 [#"../../../creusot-contracts/src/ptr_own.rs" 31 4 31 34] (self : t_PtrOwn'0) : t_T'0
   
   predicate inv'3 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_T'0)
   
@@ -15210,7 +15210,7 @@ module M_creusot_contracts__ptr_own__drop [#"../../../creusot-contracts/src/ptr_
   
   axiom inv_axiom'0 [@rewrite] : forall x : t_T'0 [inv'0 x] . inv'0 x = invariant'0 x
   
-  predicate invariant'2 [#"../../../creusot-contracts/src/ptr_own.rs" 39 4 39 30] (self : t_PtrOwn'0) =
+  predicate invariant'2 [#"../../../creusot-contracts/src/ptr_own.rs" 41 4 41 30] (self : t_PtrOwn'0) =
     [%#sptr_own9] not is_null_logic'0 (ptr'0 self) /\ inv'0 (val'0 self)
   
   predicate inv'4 [#"../../../creusot-contracts/src/invariant.rs" 41 0 41 35] (_1 : t_PtrOwn'0)
diff --git a/creusot/tests/should_succeed/linked_list.coma b/creusot/tests/should_succeed/linked_list.coma
index 81311fe388..da0d3c179d 100644
--- a/creusot/tests/should_succeed/linked_list.coma
+++ b/creusot/tests/should_succeed/linked_list.coma
@@ -4,18 +4,17 @@ module M_linked_list__qyi14323471455460008969__new [#"linked_list.rs" 72 4 72 27
   let%span slinked_list2 = "linked_list.rs" 73 69 73 79
   let%span slinked_list3 = "linked_list.rs" 72 20 72 27
   let%span slinked_list4 = "linked_list.rs" 71 14 71 35
-  let%span sptr5 = "../../../creusot-contracts/src/std/ptr.rs" 121 22 121 44
-  let%span sseq6 = "../../../creusot-contracts/src/logic/seq.rs" 254 4 254 34
-  let%span sseq7 = "../../../creusot-contracts/src/logic/seq.rs" 252 14 252 36
+  let%span sptr5 = "../../../creusot-contracts/src/std/ptr.rs" 119 22 119 44
+  let%span sseq6 = "../../../creusot-contracts/src/logic/seq.rs" 261 4 261 34
+  let%span sseq7 = "../../../creusot-contracts/src/logic/seq.rs" 259 14 259 36
   let%span slinked_list8 = "linked_list.rs" 48 12 48 74
-  let%span sptr9 = "../../../creusot-contracts/src/std/ptr.rs" 80 14 80 48
-  let%span sptr10 = "../../../creusot-contracts/src/std/ptr.rs" 82 8 82 30
-  let%span sghost11 = "../../../creusot-contracts/src/ghost.rs" 200 9 200 15
-  let%span slinked_list12 = "linked_list.rs" 67 4 67 41
-  let%span slinked_list13 = "linked_list.rs" 26 12 36 69
-  let%span sboxed14 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
-  let%span sseq15 = "../../../creusot-contracts/src/logic/seq.rs" 444 20 444 95
-  let%span sptr_own16 = "../../../creusot-contracts/src/ptr_own.rs" 40 20 40 66
+  let%span sptr9 = "../../../creusot-contracts/src/std/ptr.rs" 81 8 81 30
+  let%span sghost10 = "../../../creusot-contracts/src/ghost.rs" 200 9 200 15
+  let%span slinked_list11 = "linked_list.rs" 67 4 67 41
+  let%span slinked_list12 = "linked_list.rs" 26 12 36 69
+  let%span sboxed13 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
+  let%span sseq14 = "../../../creusot-contracts/src/logic/seq.rs" 451 20 451 95
+  let%span sptr_own15 = "../../../creusot-contracts/src/ptr_own.rs" 42 20 42 66
   
   use prelude.prelude.Opaque
   
@@ -24,9 +23,7 @@ module M_linked_list__qyi14323471455460008969__new [#"linked_list.rs" 72 4 72 27
   function addr_logic'0 (self : opaque_ptr) : int
   
   function is_null_logic'0 (self : opaque_ptr) : bool =
-    [%#sptr10] addr_logic'0 self = 0
-  
-  axiom is_null_logic'0_spec : forall self : opaque_ptr . [%#sptr9] is_null_logic'0 self = (addr_logic'0 self = 0)
+    [%#sptr9] addr_logic'0 self = 0
   
   let rec null'0 (_1:()) (return'  (ret:opaque_ptr))= any
     [ return' (result:opaque_ptr)-> {[%#sptr5] is_null_logic'0 result} (! return' {result}) ]
@@ -64,35 +61,35 @@ module M_linked_list__qyi14323471455460008969__new [#"linked_list.rs" 72 4 72 27
     end
   
   predicate invariant'5 (self : t_Cell'0) =
-    [%#sboxed14] inv'7 self
+    [%#sboxed13] inv'7 self
   
   predicate inv'6 (_1 : t_Cell'0)
   
   axiom inv_axiom'6 [@rewrite] : forall x : t_Cell'0 [inv'6 x] . inv'6 x = invariant'5 x
   
   predicate invariant'4 (self : t_PtrOwn'0) =
-    [%#sptr_own16] not is_null_logic'0 (ptr'0 self) /\ inv'6 (val'0 self)
+    [%#sptr_own15] not is_null_logic'0 (ptr'0 self) /\ inv'6 (val'0 self)
   
   predicate inv'5 (_1 : t_PtrOwn'0)
   
   axiom inv_axiom'5 [@rewrite] : forall x : t_PtrOwn'0 [inv'5 x] . inv'5 x = invariant'4 x
   
   predicate invariant'3 (self : t_PtrOwn'0) =
-    [%#sboxed14] inv'5 self
+    [%#sboxed13] inv'5 self
   
   predicate inv'4 (_1 : t_PtrOwn'0)
   
   axiom inv_axiom'4 [@rewrite] : forall x : t_PtrOwn'0 [inv'4 x] . inv'4 x = invariant'3 x
   
   predicate invariant'2 (self : Seq.seq (t_PtrOwn'0)) =
-    [%#sseq15] forall i : int . 0 <= i /\ i < Seq.length self  -> inv'4 (Seq.get self i)
+    [%#sseq14] forall i : int . 0 <= i /\ i < Seq.length self  -> inv'4 (Seq.get self i)
   
   predicate inv'3 (_1 : Seq.seq (t_PtrOwn'0))
   
   axiom inv_axiom'3 [@rewrite] : forall x : Seq.seq (t_PtrOwn'0) [inv'3 x] . inv'3 x = invariant'2 x
   
   predicate invariant'1 (self : Seq.seq (t_PtrOwn'0)) =
-    [%#sboxed14] inv'3 self
+    [%#sboxed13] inv'3 self
   
   predicate inv'2 (_1 : Seq.seq (t_PtrOwn'0))
   
@@ -106,7 +103,7 @@ module M_linked_list__qyi14323471455460008969__new [#"linked_list.rs" 72 4 72 27
     end
   
   function inner_logic'0 (self : t_GhostBox'0) : Seq.seq (t_PtrOwn'0) =
-    [%#sghost11] self.t_GhostBox__0'0
+    [%#sghost10] self.t_GhostBox__0'0
   
   use seq.Seq
   
@@ -124,7 +121,7 @@ module M_linked_list__qyi14323471455460008969__new [#"linked_list.rs" 72 4 72 27
   use seq.Seq
   
   predicate invariant'0 [#"linked_list.rs" 24 4 24 30] (self : t_List'0) =
-    [%#slinked_list13] inner_logic'0 self.t_List__seq'0 = (Seq.empty  : Seq.seq (t_PtrOwn'0))
+    [%#slinked_list12] inner_logic'0 self.t_List__seq'0 = (Seq.empty  : Seq.seq (t_PtrOwn'0))
     /\ is_null_logic'0 self.t_List__first'0 /\ is_null_logic'0 self.t_List__last'0
     \/ Seq.length (inner_logic'0 self.t_List__seq'0) > 0
     /\ self.t_List__first'0 = ptr'0 (Seq.get (inner_logic'0 self.t_List__seq'0) 0)
@@ -159,7 +156,7 @@ module M_linked_list__qyi14323471455460008969__new [#"linked_list.rs" 72 4 72 27
   function seq_map'0 [#"linked_list.rs" 66 0 66 66] (s : Seq.seq (t_PtrOwn'0)) (f : Map.map (t_PtrOwn'0) t_T'0) : Seq.seq t_T'0
     
    =
-    [%#slinked_list12] Seq.create (Seq.length s) (Mapping.from_fn (fun (i : int) -> Map.get f (Seq.get s i)))
+    [%#slinked_list11] Seq.create (Seq.length s) (Mapping.from_fn (fun (i : int) -> Map.get f (Seq.get s i)))
   
   function view'0 [#"linked_list.rs" 46 4 46 33] (self : t_List'0) : Seq.seq t_T'0 =
     [%#slinked_list8] seq_map'0 (inner_logic'0 self.t_List__seq'0) (Mapping.from_fn (fun (ptr_own : t_PtrOwn'0) -> (val'0 ptr_own).t_Cell__v'0))
@@ -190,60 +187,59 @@ module M_linked_list__qyi14323471455460008969__push_back [#"linked_list.rs" 77 4
   let%span slinked_list1 = "linked_list.rs" 77 26 77 30
   let%span slinked_list2 = "linked_list.rs" 77 32 77 33
   let%span slinked_list3 = "linked_list.rs" 76 14 76 47
-  let%span sptr4 = "../../../creusot-contracts/src/std/ptr.rs" 121 22 121 44
-  let%span sptr_own5 = "../../../creusot-contracts/src/ptr_own.rs" 54 27 54 30
-  let%span sptr_own6 = "../../../creusot-contracts/src/ptr_own.rs" 54 0 54 75
-  let%span sptr_own7 = "../../../creusot-contracts/src/ptr_own.rs" 53 10 53 63
-  let%span sptr8 = "../../../creusot-contracts/src/std/ptr.rs" 107 18 107 48
+  let%span sptr4 = "../../../creusot-contracts/src/std/ptr.rs" 119 22 119 44
+  let%span sptr_own5 = "../../../creusot-contracts/src/ptr_own.rs" 59 20 59 23
+  let%span sptr_own6 = "../../../creusot-contracts/src/ptr_own.rs" 59 4 59 68
+  let%span sptr_own7 = "../../../creusot-contracts/src/ptr_own.rs" 58 14 58 67
+  let%span sptr8 = "../../../creusot-contracts/src/std/ptr.rs" 105 18 105 48
   let%span sghost9 = "../../../creusot-contracts/src/ghost.rs" 121 27 121 31
   let%span sghost10 = "../../../creusot-contracts/src/ghost.rs" 121 4 121 52
   let%span sghost11 = "../../../creusot-contracts/src/ghost.rs" 120 14 120 39
   let%span slinked_list12 = "linked_list.rs" 89 16 92 17
-  let%span sptr_own13 = "../../../creusot-contracts/src/ptr_own.rs" 82 41 82 44
-  let%span sptr_own14 = "../../../creusot-contracts/src/ptr_own.rs" 71 11 71 27
-  let%span sptr_own15 = "../../../creusot-contracts/src/ptr_own.rs" 82 0 82 81
-  let%span sptr_own16 = "../../../creusot-contracts/src/ptr_own.rs" 72 10 72 31
-  let%span sptr_own17 = "../../../creusot-contracts/src/ptr_own.rs" 80 10 80 49
-  let%span sptr_own18 = "../../../creusot-contracts/src/ptr_own.rs" 81 10 81 48
+  let%span sptr_own13 = "../../../creusot-contracts/src/ptr_own.rs" 81 34 81 37
+  let%span sptr_own14 = "../../../creusot-contracts/src/ptr_own.rs" 76 15 76 31
+  let%span sptr_own15 = "../../../creusot-contracts/src/ptr_own.rs" 81 4 81 74
+  let%span sptr_own16 = "../../../creusot-contracts/src/ptr_own.rs" 77 14 77 35
+  let%span sptr_own17 = "../../../creusot-contracts/src/ptr_own.rs" 79 14 79 53
+  let%span sptr_own18 = "../../../creusot-contracts/src/ptr_own.rs" 80 14 80 52
   let%span slinked_list19 = "linked_list.rs" 48 12 48 74
-  let%span sptr20 = "../../../creusot-contracts/src/std/ptr.rs" 80 14 80 48
-  let%span sptr21 = "../../../creusot-contracts/src/std/ptr.rs" 82 8 82 30
-  let%span sghost22 = "../../../creusot-contracts/src/ghost.rs" 200 9 200 15
-  let%span sghost23 = "../../../creusot-contracts/src/ghost.rs" 68 22 68 26
-  let%span sghost24 = "../../../creusot-contracts/src/ghost.rs" 68 4 68 48
-  let%span sghost25 = "../../../creusot-contracts/src/ghost.rs" 67 14 67 36
-  let%span sghost26 = "../../../creusot-contracts/src/ghost.rs" 182 22 182 26
-  let%span sghost27 = "../../../creusot-contracts/src/ghost.rs" 182 4 182 32
-  let%span sghost28 = "../../../creusot-contracts/src/ghost.rs" 180 14 180 31
-  let%span sseq29 = "../../../creusot-contracts/src/logic/seq.rs" 321 32 321 36
-  let%span sseq30 = "../../../creusot-contracts/src/logic/seq.rs" 321 38 321 39
-  let%span sseq31 = "../../../creusot-contracts/src/logic/seq.rs" 320 14 320 40
-  let%span sghost32 = "../../../creusot-contracts/src/ghost.rs" 164 15 164 16
-  let%span sghost33 = "../../../creusot-contracts/src/ghost.rs" 164 4 164 28
-  let%span sghost34 = "../../../creusot-contracts/src/ghost.rs" 162 14 162 28
-  let%span sghost35 = "../../../creusot-contracts/src/ghost.rs" 93 8 93 24
-  let%span sresolve36 = "../../../creusot-contracts/src/resolve.rs" 54 20 54 34
-  let%span sghost37 = "../../../creusot-contracts/src/ghost.rs" 52 14 52 18
-  let%span sghost38 = "../../../creusot-contracts/src/ghost.rs" 52 4 52 36
-  let%span sghost39 = "../../../creusot-contracts/src/ghost.rs" 51 14 51 35
-  let%span sseq40 = "../../../creusot-contracts/src/logic/seq.rs" 278 22 278 26
-  let%span sseq41 = "../../../creusot-contracts/src/logic/seq.rs" 277 14 277 34
-  let%span slinked_list42 = "linked_list.rs" 56 10 56 25
-  let%span sseq43 = "../../../creusot-contracts/src/logic/seq.rs" 380 30 380 34
-  let%span sseq44 = "../../../creusot-contracts/src/logic/seq.rs" 380 4 380 65
-  let%span sseq45 = "../../../creusot-contracts/src/logic/seq.rs" 374 14 377 5
-  let%span sseq46 = "../../../creusot-contracts/src/logic/seq.rs" 378 14 378 84
-  let%span sseq47 = "../../../creusot-contracts/src/logic/seq.rs" 379 14 379 44
-  let%span soption48 = "../../../creusot-contracts/src/std/option.rs" 31 0 423 1
-  let%span slinked_list49 = "linked_list.rs" 67 4 67 41
-  let%span sinvariant50 = "../../../creusot-contracts/src/invariant.rs" 34 20 34 44
-  let%span sseq51 = "../../../creusot-contracts/src/logic/seq.rs" 62 4 62 12
-  let%span sboxed52 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
-  let%span sseq53 = "../../../creusot-contracts/src/logic/seq.rs" 444 20 444 95
-  let%span sresolve54 = "../../../creusot-contracts/src/resolve.rs" 68 8 68 23
-  let%span sptr_own55 = "../../../creusot-contracts/src/ptr_own.rs" 40 20 40 66
-  let%span sinvariant56 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18
-  let%span slinked_list57 = "linked_list.rs" 26 12 36 69
+  let%span sptr20 = "../../../creusot-contracts/src/std/ptr.rs" 81 8 81 30
+  let%span sghost21 = "../../../creusot-contracts/src/ghost.rs" 200 9 200 15
+  let%span sghost22 = "../../../creusot-contracts/src/ghost.rs" 68 22 68 26
+  let%span sghost23 = "../../../creusot-contracts/src/ghost.rs" 68 4 68 48
+  let%span sghost24 = "../../../creusot-contracts/src/ghost.rs" 67 14 67 36
+  let%span sghost25 = "../../../creusot-contracts/src/ghost.rs" 182 22 182 26
+  let%span sghost26 = "../../../creusot-contracts/src/ghost.rs" 182 4 182 32
+  let%span sghost27 = "../../../creusot-contracts/src/ghost.rs" 180 14 180 31
+  let%span sseq28 = "../../../creusot-contracts/src/logic/seq.rs" 328 32 328 36
+  let%span sseq29 = "../../../creusot-contracts/src/logic/seq.rs" 328 38 328 39
+  let%span sseq30 = "../../../creusot-contracts/src/logic/seq.rs" 327 14 327 40
+  let%span sghost31 = "../../../creusot-contracts/src/ghost.rs" 164 15 164 16
+  let%span sghost32 = "../../../creusot-contracts/src/ghost.rs" 164 4 164 28
+  let%span sghost33 = "../../../creusot-contracts/src/ghost.rs" 162 14 162 28
+  let%span sghost34 = "../../../creusot-contracts/src/ghost.rs" 93 8 93 24
+  let%span sresolve35 = "../../../creusot-contracts/src/resolve.rs" 54 20 54 34
+  let%span sghost36 = "../../../creusot-contracts/src/ghost.rs" 52 14 52 18
+  let%span sghost37 = "../../../creusot-contracts/src/ghost.rs" 52 4 52 36
+  let%span sghost38 = "../../../creusot-contracts/src/ghost.rs" 51 14 51 35
+  let%span sseq39 = "../../../creusot-contracts/src/logic/seq.rs" 285 22 285 26
+  let%span sseq40 = "../../../creusot-contracts/src/logic/seq.rs" 284 14 284 34
+  let%span slinked_list41 = "linked_list.rs" 56 10 56 25
+  let%span sseq42 = "../../../creusot-contracts/src/logic/seq.rs" 387 30 387 34
+  let%span sseq43 = "../../../creusot-contracts/src/logic/seq.rs" 387 4 387 65
+  let%span sseq44 = "../../../creusot-contracts/src/logic/seq.rs" 381 14 384 5
+  let%span sseq45 = "../../../creusot-contracts/src/logic/seq.rs" 385 14 385 84
+  let%span sseq46 = "../../../creusot-contracts/src/logic/seq.rs" 386 14 386 44
+  let%span soption47 = "../../../creusot-contracts/src/std/option.rs" 31 0 423 1
+  let%span slinked_list48 = "linked_list.rs" 67 4 67 41
+  let%span sinvariant49 = "../../../creusot-contracts/src/invariant.rs" 34 20 34 44
+  let%span sseq50 = "../../../creusot-contracts/src/logic/seq.rs" 69 4 69 12
+  let%span sboxed51 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
+  let%span sseq52 = "../../../creusot-contracts/src/logic/seq.rs" 451 20 451 95
+  let%span sresolve53 = "../../../creusot-contracts/src/resolve.rs" 68 8 68 23
+  let%span sptr_own54 = "../../../creusot-contracts/src/ptr_own.rs" 42 20 42 66
+  let%span sinvariant55 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18
+  let%span slinked_list56 = "linked_list.rs" 26 12 36 69
   
   use prelude.prelude.Opaque
   
@@ -252,9 +248,7 @@ module M_linked_list__qyi14323471455460008969__push_back [#"linked_list.rs" 77 4
   function addr_logic'0 (self : opaque_ptr) : int
   
   function is_null_logic'0 (self : opaque_ptr) : bool =
-    [%#sptr21] addr_logic'0 self = 0
-  
-  axiom is_null_logic'0_spec : forall self : opaque_ptr . [%#sptr20] is_null_logic'0 self = (addr_logic'0 self = 0)
+    [%#sptr20] addr_logic'0 self = 0
   
   let rec null'0 (_1:()) (return'  (ret:opaque_ptr))= any
     [ return' (result:opaque_ptr)-> {[%#sptr4] is_null_logic'0 result} (! return' {result}) ]
@@ -275,7 +269,7 @@ module M_linked_list__qyi14323471455460008969__push_back [#"linked_list.rs" 77 4
     end
   
   predicate invariant'2 (self : t_Cell'0) =
-    [%#sboxed52] inv'29 self
+    [%#sboxed51] inv'29 self
   
   predicate inv'6 (_1 : t_Cell'0)
   
@@ -293,14 +287,14 @@ module M_linked_list__qyi14323471455460008969__push_back [#"linked_list.rs" 77 4
   function val'0 (self : t_PtrOwn'0) : t_Cell'0
   
   predicate invariant'7 (self : t_PtrOwn'0) =
-    [%#sptr_own55] not is_null_logic'0 (ptr'0 self) /\ inv'6 (val'0 self)
+    [%#sptr_own54] not is_null_logic'0 (ptr'0 self) /\ inv'6 (val'0 self)
   
   predicate inv'13 (_1 : t_PtrOwn'0)
   
   axiom inv_axiom'12 [@rewrite] : forall x : t_PtrOwn'0 [inv'13 x] . inv'13 x = invariant'7 x
   
   predicate invariant'12 (self : t_PtrOwn'0) =
-    [%#sboxed52] inv'13 self
+    [%#sboxed51] inv'13 self
   
   predicate inv'22 (_1 : t_PtrOwn'0)
   
@@ -319,7 +313,7 @@ module M_linked_list__qyi14323471455460008969__push_back [#"linked_list.rs" 77 4
   = (let (x0, x1) = x in inv'3 x1)
   
   function inner_logic'0 (self : t_GhostBox'0) : t_PtrOwn'0 =
-    [%#sghost22] self.t_GhostBox__0'0
+    [%#sghost21] self.t_GhostBox__0'0
   
   let rec from_box'0 (val':t_Cell'0) (return'  (ret:(opaque_ptr, t_GhostBox'0)))= {[@expl:from_box 'val' type invariant] [%#sptr_own5] inv'6 val'}
     any
@@ -346,14 +340,14 @@ module M_linked_list__qyi14323471455460008969__push_back [#"linked_list.rs" 77 4
   use seq.Seq
   
   predicate invariant'4 (self : Seq.seq (t_PtrOwn'0)) =
-    [%#sseq53] forall i : int . 0 <= i /\ i < Seq.length self  -> inv'22 (Seq.get self i)
+    [%#sseq52] forall i : int . 0 <= i /\ i < Seq.length self  -> inv'22 (Seq.get self i)
   
   predicate inv'9 (_1 : Seq.seq (t_PtrOwn'0))
   
   axiom inv_axiom'8 [@rewrite] : forall x : Seq.seq (t_PtrOwn'0) [inv'9 x] . inv'9 x = invariant'4 x
   
   predicate invariant'10 (self : Seq.seq (t_PtrOwn'0)) =
-    [%#sboxed52] inv'9 self
+    [%#sboxed51] inv'9 self
   
   predicate inv'18 (_1 : Seq.seq (t_PtrOwn'0))
   
@@ -367,7 +361,7 @@ module M_linked_list__qyi14323471455460008969__push_back [#"linked_list.rs" 77 4
     end
   
   predicate invariant'3 (self : borrowed (t_GhostBox'1)) =
-    [%#sinvariant50] inv'0 self.current /\ inv'0 self.final
+    [%#sinvariant49] inv'0 self.current /\ inv'0 self.final
   
   predicate inv'8 (_1 : borrowed (t_GhostBox'1))
   
@@ -377,14 +371,14 @@ module M_linked_list__qyi14323471455460008969__push_back [#"linked_list.rs" 77 4
     { t_GhostBox__0'2: borrowed (Seq.seq (t_PtrOwn'0)) }
   
   predicate invariant'8 (self : borrowed (Seq.seq (t_PtrOwn'0))) =
-    [%#sinvariant50] inv'9 self.current /\ inv'9 self.final
+    [%#sinvariant49] inv'9 self.current /\ inv'9 self.final
   
   predicate inv'14 (_1 : borrowed (Seq.seq (t_PtrOwn'0)))
   
   axiom inv_axiom'13 [@rewrite] : forall x : borrowed (Seq.seq (t_PtrOwn'0)) [inv'14 x] . inv'14 x = invariant'8 x
   
   predicate invariant'11 (self : borrowed (Seq.seq (t_PtrOwn'0))) =
-    [%#sboxed52] inv'14 self
+    [%#sboxed51] inv'14 self
   
   predicate inv'19 (_1 : borrowed (Seq.seq (t_PtrOwn'0)))
   
@@ -406,49 +400,49 @@ module M_linked_list__qyi14323471455460008969__push_back [#"linked_list.rs" 77 4
     
   
   predicate invariant'6 (self : borrowed (t_GhostBox'2)) =
-    [%#sinvariant50] inv'1 self.current /\ inv'1 self.final
+    [%#sinvariant49] inv'1 self.current /\ inv'1 self.final
   
   predicate inv'11 (_1 : borrowed (t_GhostBox'2))
   
   axiom inv_axiom'10 [@rewrite] : forall x : borrowed (t_GhostBox'2) [inv'11 x] . inv'11 x = invariant'6 x
   
   predicate invariant'5 (self : borrowed (borrowed (Seq.seq (t_PtrOwn'0)))) =
-    [%#sinvariant50] inv'14 self.current /\ inv'14 self.final
+    [%#sinvariant49] inv'14 self.current /\ inv'14 self.final
   
   predicate inv'10 (_1 : borrowed (borrowed (Seq.seq (t_PtrOwn'0))))
   
   axiom inv_axiom'9 [@rewrite] : forall x : borrowed (borrowed (Seq.seq (t_PtrOwn'0))) [inv'10 x] . inv'10 x
   = invariant'5 x
   
-  let rec deref_mut'0 (self:borrowed (t_GhostBox'2)) (return'  (ret:borrowed (borrowed (Seq.seq (t_PtrOwn'0)))))= {[@expl:deref_mut 'self' type invariant] [%#sghost23] inv'11 self}
+  let rec deref_mut'0 (self:borrowed (t_GhostBox'2)) (return'  (ret:borrowed (borrowed (Seq.seq (t_PtrOwn'0)))))= {[@expl:deref_mut 'self' type invariant] [%#sghost22] inv'11 self}
     any
-    [ return' (result:borrowed (borrowed (Seq.seq (t_PtrOwn'0))))-> {[%#sghost24] inv'10 result}
-      {[%#sghost25] result
+    [ return' (result:borrowed (borrowed (Seq.seq (t_PtrOwn'0))))-> {[%#sghost23] inv'10 result}
+      {[%#sghost24] result
       = Borrow.borrow_logic (self.current).t_GhostBox__0'2 (self.final).t_GhostBox__0'2 (Borrow.inherit_id (Borrow.get_id self) 1)}
       (! return' {result}) ]
     
   
-  let rec into_inner'0 (self:t_GhostBox'0) (return'  (ret:t_PtrOwn'0))= {[@expl:into_inner 'self' type invariant] [%#sghost26] inv'3 self}
+  let rec into_inner'0 (self:t_GhostBox'0) (return'  (ret:t_PtrOwn'0))= {[@expl:into_inner 'self' type invariant] [%#sghost25] inv'3 self}
     any
-    [ return' (result:t_PtrOwn'0)-> {[%#sghost27] inv'13 result}
-      {[%#sghost28] result = self.t_GhostBox__0'0}
+    [ return' (result:t_PtrOwn'0)-> {[%#sghost26] inv'13 result}
+      {[%#sghost27] result = self.t_GhostBox__0'0}
       (! return' {result}) ]
     
   
   use seq.Seq
   
-  let rec push_back_ghost'0 (self:borrowed (Seq.seq (t_PtrOwn'0))) (x:t_PtrOwn'0) (return'  (ret:()))= {[@expl:push_back_ghost 'self' type invariant] [%#sseq29] inv'14 self}
-    {[@expl:push_back_ghost 'x' type invariant] [%#sseq30] inv'13 x}
-    any [ return' (result:())-> {[%#sseq31] self.final = Seq.snoc self.current x} (! return' {result}) ] 
+  let rec push_back_ghost'0 (self:borrowed (Seq.seq (t_PtrOwn'0))) (x:t_PtrOwn'0) (return'  (ret:()))= {[@expl:push_back_ghost 'self' type invariant] [%#sseq28] inv'14 self}
+    {[@expl:push_back_ghost 'x' type invariant] [%#sseq29] inv'13 x}
+    any [ return' (result:())-> {[%#sseq30] self.final = Seq.snoc self.current x} (! return' {result}) ] 
   
   predicate resolve'12 (self : borrowed (borrowed (Seq.seq (t_PtrOwn'0)))) =
-    [%#sresolve36] self.final = self.current
+    [%#sresolve35] self.final = self.current
   
   predicate resolve'4 (_1 : borrowed (borrowed (Seq.seq (t_PtrOwn'0)))) =
     resolve'12 _1
   
   predicate resolve'13 (self : borrowed (t_GhostBox'2)) =
-    [%#sresolve36] self.final = self.current
+    [%#sresolve35] self.final = self.current
   
   predicate resolve'5 (_1 : borrowed (t_GhostBox'2)) =
     resolve'13 _1
@@ -464,10 +458,10 @@ module M_linked_list__qyi14323471455460008969__push_back [#"linked_list.rs" 77 4
   
   axiom inv_axiom'20 [@rewrite] : forall x : t_GhostBox'3 [inv'21 x] . inv'21 x = true
   
-  let rec new'0 (x:()) (return'  (ret:t_GhostBox'3))= {[@expl:new 'x' type invariant] [%#sghost32] inv'20 x}
+  let rec new'0 (x:()) (return'  (ret:t_GhostBox'3))= {[@expl:new 'x' type invariant] [%#sghost31] inv'20 x}
     any
-    [ return' (result:t_GhostBox'3)-> {[%#sghost33] inv'21 result}
-      {[%#sghost34] result.t_GhostBox__0'3 = x}
+    [ return' (result:t_GhostBox'3)-> {[%#sghost32] inv'21 result}
+      {[%#sghost33] result.t_GhostBox__0'3 = x}
       (! return' {result}) ]
     
   
@@ -535,32 +529,32 @@ module M_linked_list__qyi14323471455460008969__push_back [#"linked_list.rs" 77 4
      [ return' (result:t_GhostBox'3)-> return' {result} ] 
   
   predicate resolve'16 (self : borrowed (Seq.seq (t_PtrOwn'0))) =
-    [%#sresolve36] self.final = self.current
+    [%#sresolve35] self.final = self.current
   
   predicate resolve'9 (_1 : borrowed (Seq.seq (t_PtrOwn'0))) =
     resolve'16 _1
   
   predicate resolve'18 (self : borrowed (Seq.seq (t_PtrOwn'0))) =
-    [%#sresolve54] resolve'9 self
+    [%#sresolve53] resolve'9 self
   
   predicate resolve'14 (_1 : borrowed (Seq.seq (t_PtrOwn'0))) =
     resolve'18 _1
   
   predicate resolve'6 (self : t_GhostBox'2) =
-    [%#sghost35] resolve'14 self.t_GhostBox__0'2
+    [%#sghost34] resolve'14 self.t_GhostBox__0'2
   
   predicate resolve'0 (_1 : t_GhostBox'2) =
     resolve'6 _1
   
   function inner_logic'2 (self : t_GhostBox'1) : Seq.seq (t_PtrOwn'0) =
-    [%#sghost22] self.t_GhostBox__0'1
+    [%#sghost21] self.t_GhostBox__0'1
   
   use seq.Seq
   
   use seq.Seq
   
   predicate invariant'16 [#"linked_list.rs" 24 4 24 30] (self : t_List'0) =
-    [%#slinked_list57] inner_logic'2 self.t_List__seq'0 = (Seq.empty  : Seq.seq (t_PtrOwn'0))
+    [%#slinked_list56] inner_logic'2 self.t_List__seq'0 = (Seq.empty  : Seq.seq (t_PtrOwn'0))
     /\ is_null_logic'0 self.t_List__first'0 /\ is_null_logic'0 self.t_List__last'0
     \/ Seq.length (inner_logic'2 self.t_List__seq'0) > 0
     /\ self.t_List__first'0 = ptr'0 (Seq.get (inner_logic'2 self.t_List__seq'0) 0)
@@ -581,14 +575,14 @@ module M_linked_list__qyi14323471455460008969__push_back [#"linked_list.rs" 77 4
     end)
   
   predicate invariant'0 (self : borrowed (t_List'0)) =
-    [%#sinvariant50] inv'27 self.current /\ inv'27 self.final
+    [%#sinvariant49] inv'27 self.current /\ inv'27 self.final
   
   predicate inv'2 (_1 : borrowed (t_List'0))
   
   axiom inv_axiom'2 [@rewrite] : forall x : borrowed (t_List'0) [inv'2 x] . inv'2 x = invariant'0 x
   
   predicate resolve'7 (self : borrowed (t_List'0)) =
-    [%#sresolve36] self.final = self.current
+    [%#sresolve35] self.final = self.current
   
   predicate resolve'1 (_1 : borrowed (t_List'0)) =
     resolve'7 _1
@@ -597,56 +591,56 @@ module M_linked_list__qyi14323471455460008969__push_back [#"linked_list.rs" 77 4
     true
   
   predicate resolve'19 (self : t_PtrOwn'0) =
-    [%#sresolve54] resolve'20 self
+    [%#sresolve53] resolve'20 self
   
   predicate resolve'15 (_1 : t_PtrOwn'0) =
     resolve'19 _1
   
   predicate resolve'8 (self : t_GhostBox'0) =
-    [%#sghost35] resolve'15 self.t_GhostBox__0'0
+    [%#sghost34] resolve'15 self.t_GhostBox__0'0
   
   predicate resolve'2 (_1 : t_GhostBox'0) =
     resolve'8 _1
   
   predicate invariant'13 (self : t_GhostBox'2) =
-    [%#sinvariant56] inv'1 self
+    [%#sinvariant55] inv'1 self
   
   predicate inv'23 (_1 : t_GhostBox'2)
   
   axiom inv_axiom'22 [@rewrite] : forall x : t_GhostBox'2 [inv'23 x] . inv'23 x = invariant'13 x
   
   predicate invariant'14 (self : borrowed (Seq.seq (t_PtrOwn'0))) =
-    [%#sinvariant56] inv'14 self
+    [%#sinvariant55] inv'14 self
   
   predicate inv'24 (_1 : borrowed (Seq.seq (t_PtrOwn'0)))
   
   axiom inv_axiom'23 [@rewrite] : forall x : borrowed (Seq.seq (t_PtrOwn'0)) [inv'24 x] . inv'24 x = invariant'14 x
   
-  let rec deref'0 (self:t_GhostBox'2) (return'  (ret:borrowed (Seq.seq (t_PtrOwn'0))))= {[@expl:deref 'self' type invariant] [%#sghost37] inv'23 self}
+  let rec deref'0 (self:t_GhostBox'2) (return'  (ret:borrowed (Seq.seq (t_PtrOwn'0))))= {[@expl:deref 'self' type invariant] [%#sghost36] inv'23 self}
     any
-    [ return' (result:borrowed (Seq.seq (t_PtrOwn'0)))-> {[%#sghost38] inv'24 result}
-      {[%#sghost39] self.t_GhostBox__0'2 = result}
+    [ return' (result:borrowed (Seq.seq (t_PtrOwn'0)))-> {[%#sghost37] inv'24 result}
+      {[%#sghost38] self.t_GhostBox__0'2 = result}
       (! return' {result}) ]
     
   
   predicate invariant'15 (self : Seq.seq (t_PtrOwn'0)) =
-    [%#sinvariant56] inv'9 self
+    [%#sinvariant55] inv'9 self
   
   predicate inv'25 (_1 : Seq.seq (t_PtrOwn'0))
   
   axiom inv_axiom'24 [@rewrite] : forall x : Seq.seq (t_PtrOwn'0) [inv'25 x] . inv'25 x = invariant'15 x
   
-  let rec len_ghost'0 (self:Seq.seq (t_PtrOwn'0)) (return'  (ret:int))= {[@expl:len_ghost 'self' type invariant] [%#sseq40] inv'25 self}
-    any [ return' (result:int)-> {[%#sseq41] result = Seq.length self} (! return' {result}) ] 
+  let rec len_ghost'0 (self:Seq.seq (t_PtrOwn'0)) (return'  (ret:int))= {[@expl:len_ghost 'self' type invariant] [%#sseq39] inv'25 self}
+    any [ return' (result:int)-> {[%#sseq40] result = Seq.length self} (! return' {result}) ] 
   
   let rec minus_one'0 (x:int) (return'  (ret:int))= any
-    [ return' (result:int)-> {[%#slinked_list42] result = x - 1} (! return' {result}) ]
+    [ return' (result:int)-> {[%#slinked_list41] result = x - 1} (! return' {result}) ]
     
   
-  let rec into_inner'1 (self:t_GhostBox'2) (return'  (ret:borrowed (Seq.seq (t_PtrOwn'0))))= {[@expl:into_inner 'self' type invariant] [%#sghost26] inv'1 self}
+  let rec into_inner'1 (self:t_GhostBox'2) (return'  (ret:borrowed (Seq.seq (t_PtrOwn'0))))= {[@expl:into_inner 'self' type invariant] [%#sghost25] inv'1 self}
     any
-    [ return' (result:borrowed (Seq.seq (t_PtrOwn'0)))-> {[%#sghost27] inv'14 result}
-      {[%#sghost28] result = self.t_GhostBox__0'2}
+    [ return' (result:borrowed (Seq.seq (t_PtrOwn'0)))-> {[%#sghost26] inv'14 result}
+      {[%#sghost27] result = self.t_GhostBox__0'2}
       (! return' {result}) ]
     
   
@@ -655,7 +649,7 @@ module M_linked_list__qyi14323471455460008969__push_back [#"linked_list.rs" 77 4
     | C_Some'0 (borrowed (t_PtrOwn'0))
   
   predicate invariant'9 (self : borrowed (t_PtrOwn'0)) =
-    [%#sinvariant50] inv'13 self.current /\ inv'13 self.final
+    [%#sinvariant49] inv'13 self.current /\ inv'13 self.final
   
   predicate inv'15 (_1 : borrowed (t_PtrOwn'0))
   
@@ -674,25 +668,25 @@ module M_linked_list__qyi14323471455460008969__push_back [#"linked_list.rs" 77 4
     | C_Some'1 (t_PtrOwn'0)
   
   function get'0 (self : Seq.seq (t_PtrOwn'0)) (ix : int) : t_Option'1 =
-    [%#sseq51] if 0 <= ix /\ ix < Seq.length self then C_Some'1 (Seq.get self ix) else C_None'1
+    [%#sseq50] if 0 <= ix /\ ix < Seq.length self then C_Some'1 (Seq.get self ix) else C_None'1
   
-  let rec get_mut_ghost'0 (self:borrowed (Seq.seq (t_PtrOwn'0))) (index:int) (return'  (ret:t_Option'0))= {[@expl:get_mut_ghost 'self' type invariant] [%#sseq43] inv'14 self}
+  let rec get_mut_ghost'0 (self:borrowed (Seq.seq (t_PtrOwn'0))) (index:int) (return'  (ret:t_Option'0))= {[@expl:get_mut_ghost 'self' type invariant] [%#sseq42] inv'14 self}
     any
-    [ return' (result:t_Option'0)-> {[%#sseq44] inv'26 result}
-      {[%#sseq45] match result with
+    [ return' (result:t_Option'0)-> {[%#sseq43] inv'26 result}
+      {[%#sseq44] match result with
         | C_None'0 -> get'0 self.current index = C_None'1 /\ self.current = self.final
         | C_Some'0 r -> get'0 self.current index = C_Some'1 (r.current) /\ r.final = Seq.get self.final index
         end}
-      {[%#sseq46] forall i : int . i <> index  -> get'0 self.current index = get'0 self.final index}
-      {[%#sseq47] Seq.length self.current = Seq.length self.final}
+      {[%#sseq45] forall i : int . i <> index  -> get'0 self.current index = get'0 self.final index}
+      {[%#sseq46] Seq.length self.current = Seq.length self.final}
       (! return' {result}) ]
     
   
   let rec unwrap'0 (self:t_Option'0) (return'  (ret:borrowed (t_PtrOwn'0)))= {[@expl:unwrap 'self' type invariant] inv'26 self}
-    {[@expl:unwrap requires] [%#soption48] self <> C_None'0}
+    {[@expl:unwrap requires] [%#soption47] self <> C_None'0}
     any
     [ return' (result:borrowed (t_PtrOwn'0))-> {inv'15 result}
-      {[%#soption48] C_Some'0 result = self}
+      {[%#soption47] C_Some'0 result = self}
       (! return' {result}) ]
     
   
@@ -700,7 +694,7 @@ module M_linked_list__qyi14323471455460008969__push_back [#"linked_list.rs" 77 4
     { t_GhostBox__0'4: borrowed (t_PtrOwn'0) }
   
   predicate invariant'17 (self : borrowed (t_PtrOwn'0)) =
-    [%#sboxed52] inv'15 self
+    [%#sboxed51] inv'15 self
   
   predicate inv'28 (_1 : borrowed (t_PtrOwn'0))
   
@@ -713,15 +707,15 @@ module M_linked_list__qyi14323471455460008969__push_back [#"linked_list.rs" 77 4
     | {t_GhostBox__0'4 = a_0} -> inv'28 a_0
     end
   
-  let rec new'1 (x:borrowed (t_PtrOwn'0)) (return'  (ret:t_GhostBox'4))= {[@expl:new 'x' type invariant] [%#sghost32] inv'15 x}
+  let rec new'1 (x:borrowed (t_PtrOwn'0)) (return'  (ret:t_GhostBox'4))= {[@expl:new 'x' type invariant] [%#sghost31] inv'15 x}
     any
-    [ return' (result:t_GhostBox'4)-> {[%#sghost33] inv'17 result}
-      {[%#sghost34] result.t_GhostBox__0'4 = x}
+    [ return' (result:t_GhostBox'4)-> {[%#sghost32] inv'17 result}
+      {[%#sghost33] result.t_GhostBox__0'4 = x}
       (! return' {result}) ]
     
   
   predicate resolve'17 (self : borrowed (t_PtrOwn'0)) =
-    [%#sresolve36] self.final = self.current
+    [%#sresolve35] self.final = self.current
   
   predicate resolve'10 (_1 : borrowed (t_PtrOwn'0)) =
     resolve'17 _1
@@ -792,10 +786,10 @@ module M_linked_list__qyi14323471455460008969__push_back [#"linked_list.rs" 77 4
     
   
   function inner_logic'1 (self : t_GhostBox'4) : borrowed (t_PtrOwn'0) =
-    [%#sghost22] self.t_GhostBox__0'4
+    [%#sghost21] self.t_GhostBox__0'4
   
   predicate invariant'1 (self : borrowed (t_Cell'0)) =
-    [%#sinvariant50] inv'29 self.current /\ inv'29 self.final
+    [%#sinvariant49] inv'29 self.current /\ inv'29 self.final
   
   predicate inv'4 (_1 : borrowed (t_Cell'0))
   
@@ -812,7 +806,7 @@ module M_linked_list__qyi14323471455460008969__push_back [#"linked_list.rs" 77 4
     
   
   predicate resolve'11 (self : borrowed (t_Cell'0)) =
-    [%#sresolve36] self.final = self.current
+    [%#sresolve35] self.final = self.current
   
   predicate resolve'3 (_1 : borrowed (t_Cell'0)) =
     resolve'11 _1
@@ -832,7 +826,7 @@ module M_linked_list__qyi14323471455460008969__push_back [#"linked_list.rs" 77 4
   function seq_map'0 [#"linked_list.rs" 66 0 66 66] (s : Seq.seq (t_PtrOwn'0)) (f : Map.map (t_PtrOwn'0) t_T'0) : Seq.seq t_T'0
     
    =
-    [%#slinked_list49] Seq.create (Seq.length s) (Mapping.from_fn (fun (i : int) -> Map.get f (Seq.get s i)))
+    [%#slinked_list48] Seq.create (Seq.length s) (Mapping.from_fn (fun (i : int) -> Map.get f (Seq.get s i)))
   
   function view'0 [#"linked_list.rs" 46 4 46 33] (self : t_List'0) : Seq.seq t_T'0 =
     [%#slinked_list19] seq_map'0 (inner_logic'2 self.t_List__seq'0) (Mapping.from_fn (fun (ptr_own : t_PtrOwn'0) -> (val'0 ptr_own).t_Cell__v'0))
@@ -958,39 +952,38 @@ module M_linked_list__qyi14323471455460008969__push_front [#"linked_list.rs" 100
   let%span slinked_list0 = "linked_list.rs" 100 27 100 31
   let%span slinked_list1 = "linked_list.rs" 100 33 100 34
   let%span slinked_list2 = "linked_list.rs" 99 14 99 48
-  let%span sptr_own3 = "../../../creusot-contracts/src/ptr_own.rs" 47 14 47 15
-  let%span sptr_own4 = "../../../creusot-contracts/src/ptr_own.rs" 47 0 47 55
-  let%span sptr_own5 = "../../../creusot-contracts/src/ptr_own.rs" 46 10 46 60
-  let%span sptr6 = "../../../creusot-contracts/src/std/ptr.rs" 107 18 107 48
+  let%span sptr_own3 = "../../../creusot-contracts/src/ptr_own.rs" 50 15 50 16
+  let%span sptr_own4 = "../../../creusot-contracts/src/ptr_own.rs" 50 4 50 56
+  let%span sptr_own5 = "../../../creusot-contracts/src/ptr_own.rs" 49 14 49 64
+  let%span sptr6 = "../../../creusot-contracts/src/std/ptr.rs" 105 18 105 48
   let%span sghost7 = "../../../creusot-contracts/src/ghost.rs" 121 27 121 31
   let%span sghost8 = "../../../creusot-contracts/src/ghost.rs" 121 4 121 52
   let%span sghost9 = "../../../creusot-contracts/src/ghost.rs" 120 14 120 39
   let%span slinked_list10 = "linked_list.rs" 48 12 48 74
-  let%span sseq11 = "../../../creusot-contracts/src/logic/seq.rs" 143 8 143 27
+  let%span sseq11 = "../../../creusot-contracts/src/logic/seq.rs" 150 8 150 27
   let%span sghost12 = "../../../creusot-contracts/src/ghost.rs" 200 9 200 15
-  let%span sptr13 = "../../../creusot-contracts/src/std/ptr.rs" 80 14 80 48
-  let%span sptr14 = "../../../creusot-contracts/src/std/ptr.rs" 82 8 82 30
-  let%span sghost15 = "../../../creusot-contracts/src/ghost.rs" 68 22 68 26
-  let%span sghost16 = "../../../creusot-contracts/src/ghost.rs" 68 4 68 48
-  let%span sghost17 = "../../../creusot-contracts/src/ghost.rs" 67 14 67 36
-  let%span sghost18 = "../../../creusot-contracts/src/ghost.rs" 182 22 182 26
-  let%span sghost19 = "../../../creusot-contracts/src/ghost.rs" 182 4 182 32
-  let%span sghost20 = "../../../creusot-contracts/src/ghost.rs" 180 14 180 31
-  let%span sseq21 = "../../../creusot-contracts/src/logic/seq.rs" 299 33 299 37
-  let%span sseq22 = "../../../creusot-contracts/src/logic/seq.rs" 299 39 299 40
-  let%span sseq23 = "../../../creusot-contracts/src/logic/seq.rs" 298 14 298 41
-  let%span sghost24 = "../../../creusot-contracts/src/ghost.rs" 164 15 164 16
-  let%span sghost25 = "../../../creusot-contracts/src/ghost.rs" 164 4 164 28
-  let%span sghost26 = "../../../creusot-contracts/src/ghost.rs" 162 14 162 28
-  let%span sghost27 = "../../../creusot-contracts/src/ghost.rs" 93 8 93 24
-  let%span sresolve28 = "../../../creusot-contracts/src/resolve.rs" 54 20 54 34
-  let%span slinked_list29 = "linked_list.rs" 67 4 67 41
-  let%span sinvariant30 = "../../../creusot-contracts/src/invariant.rs" 34 20 34 44
-  let%span sseq31 = "../../../creusot-contracts/src/logic/seq.rs" 444 20 444 95
-  let%span sresolve32 = "../../../creusot-contracts/src/resolve.rs" 68 8 68 23
-  let%span sboxed33 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
-  let%span sptr_own34 = "../../../creusot-contracts/src/ptr_own.rs" 40 20 40 66
-  let%span slinked_list35 = "linked_list.rs" 26 12 36 69
+  let%span sptr13 = "../../../creusot-contracts/src/std/ptr.rs" 81 8 81 30
+  let%span sghost14 = "../../../creusot-contracts/src/ghost.rs" 68 22 68 26
+  let%span sghost15 = "../../../creusot-contracts/src/ghost.rs" 68 4 68 48
+  let%span sghost16 = "../../../creusot-contracts/src/ghost.rs" 67 14 67 36
+  let%span sghost17 = "../../../creusot-contracts/src/ghost.rs" 182 22 182 26
+  let%span sghost18 = "../../../creusot-contracts/src/ghost.rs" 182 4 182 32
+  let%span sghost19 = "../../../creusot-contracts/src/ghost.rs" 180 14 180 31
+  let%span sseq20 = "../../../creusot-contracts/src/logic/seq.rs" 306 33 306 37
+  let%span sseq21 = "../../../creusot-contracts/src/logic/seq.rs" 306 39 306 40
+  let%span sseq22 = "../../../creusot-contracts/src/logic/seq.rs" 305 14 305 41
+  let%span sghost23 = "../../../creusot-contracts/src/ghost.rs" 164 15 164 16
+  let%span sghost24 = "../../../creusot-contracts/src/ghost.rs" 164 4 164 28
+  let%span sghost25 = "../../../creusot-contracts/src/ghost.rs" 162 14 162 28
+  let%span sghost26 = "../../../creusot-contracts/src/ghost.rs" 93 8 93 24
+  let%span sresolve27 = "../../../creusot-contracts/src/resolve.rs" 54 20 54 34
+  let%span slinked_list28 = "linked_list.rs" 67 4 67 41
+  let%span sinvariant29 = "../../../creusot-contracts/src/invariant.rs" 34 20 34 44
+  let%span sseq30 = "../../../creusot-contracts/src/logic/seq.rs" 451 20 451 95
+  let%span sresolve31 = "../../../creusot-contracts/src/resolve.rs" 68 8 68 23
+  let%span sboxed32 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18
+  let%span sptr_own33 = "../../../creusot-contracts/src/ptr_own.rs" 42 20 42 66
+  let%span slinked_list34 = "linked_list.rs" 26 12 36 69
   
   use prelude.prelude.Opaque
   
@@ -1030,28 +1023,26 @@ module M_linked_list__qyi14323471455460008969__push_front [#"linked_list.rs" 100
   function addr_logic'0 (self : opaque_ptr) : int
   
   function is_null_logic'0 (self : opaque_ptr) : bool =
-    [%#sptr14] addr_logic'0 self = 0
-  
-  axiom is_null_logic'0_spec : forall self : opaque_ptr . [%#sptr13] is_null_logic'0 self = (addr_logic'0 self = 0)
+    [%#sptr13] addr_logic'0 self = 0
   
   function val'0 (self : t_PtrOwn'0) : t_Cell'0
   
   predicate invariant'11 (self : t_Cell'0) =
-    [%#sboxed33] inv'4 self
+    [%#sboxed32] inv'4 self
   
   predicate inv'20 (_1 : t_Cell'0)
   
   axiom inv_axiom'19 [@rewrite] : forall x : t_Cell'0 [inv'20 x] . inv'20 x = invariant'11 x
   
   predicate invariant'7 (self : t_PtrOwn'0) =
-    [%#sptr_own34] not is_null_logic'0 (ptr'0 self) /\ inv'20 (val'0 self)
+    [%#sptr_own33] not is_null_logic'0 (ptr'0 self) /\ inv'20 (val'0 self)
   
   predicate inv'14 (_1 : t_PtrOwn'0)
   
   axiom inv_axiom'13 [@rewrite] : forall x : t_PtrOwn'0 [inv'14 x] . inv'14 x = invariant'7 x
   
   predicate invariant'10 (self : t_PtrOwn'0) =
-    [%#sboxed33] inv'14 self
+    [%#sboxed32] inv'14 self
   
   predicate inv'19 (_1 : t_PtrOwn'0)
   
@@ -1089,14 +1080,14 @@ module M_linked_list__qyi14323471455460008969__push_front [#"linked_list.rs" 100
   use seq.Seq
   
   predicate invariant'2 (self : Seq.seq (t_PtrOwn'0)) =
-    [%#sseq31] forall i : int . 0 <= i /\ i < Seq.length self  -> inv'19 (Seq.get self i)
+    [%#sseq30] forall i : int . 0 <= i /\ i < Seq.length self  -> inv'19 (Seq.get self i)
   
   predicate inv'7 (_1 : Seq.seq (t_PtrOwn'0))
   
   axiom inv_axiom'6 [@rewrite] : forall x : Seq.seq (t_PtrOwn'0) [inv'7 x] . inv'7 x = invariant'2 x
   
   predicate invariant'5 (self : Seq.seq (t_PtrOwn'0)) =
-    [%#sboxed33] inv'7 self
+    [%#sboxed32] inv'7 self
   
   predicate inv'11 (_1 : Seq.seq (t_PtrOwn'0))
   
@@ -1110,7 +1101,7 @@ module M_linked_list__qyi14323471455460008969__push_front [#"linked_list.rs" 100
     end
   
   predicate invariant'1 (self : borrowed (t_GhostBox'1)) =
-    [%#sinvariant30] inv'0 self.current /\ inv'0 self.final
+    [%#sinvariant29] inv'0 self.current /\ inv'0 self.final
   
   predicate inv'6 (_1 : borrowed (t_GhostBox'1))
   
@@ -1120,14 +1111,14 @@ module M_linked_list__qyi14323471455460008969__push_front [#"linked_list.rs" 100
     { t_GhostBox__0'2: borrowed (Seq.seq (t_PtrOwn'0)) }
   
   predicate invariant'8 (self : borrowed (Seq.seq (t_PtrOwn'0))) =
-    [%#sinvariant30] inv'7 self.current /\ inv'7 self.final
+    [%#sinvariant29] inv'7 self.current /\ inv'7 self.final
   
   predicate inv'15 (_1 : borrowed (Seq.seq (t_PtrOwn'0)))
   
   axiom inv_axiom'14 [@rewrite] : forall x : borrowed (Seq.seq (t_PtrOwn'0)) [inv'15 x] . inv'15 x = invariant'8 x
   
   predicate invariant'6 (self : borrowed (Seq.seq (t_PtrOwn'0))) =
-    [%#sboxed33] inv'15 self
+    [%#sboxed32] inv'15 self
   
   predicate inv'12 (_1 : borrowed (Seq.seq (t_PtrOwn'0)))
   
@@ -1149,32 +1140,32 @@ module M_linked_list__qyi14323471455460008969__push_front [#"linked_list.rs" 100
     
   
   predicate invariant'4 (self : borrowed (t_GhostBox'2)) =
-    [%#sinvariant30] inv'1 self.current /\ inv'1 self.final
+    [%#sinvariant29] inv'1 self.current /\ inv'1 self.final
   
   predicate inv'9 (_1 : borrowed (t_GhostBox'2))
   
   axiom inv_axiom'8 [@rewrite] : forall x : borrowed (t_GhostBox'2) [inv'9 x] . inv'9 x = invariant'4 x
   
   predicate invariant'3 (self : borrowed (borrowed (Seq.seq (t_PtrOwn'0)))) =
-    [%#sinvariant30] inv'15 self.current /\ inv'15 self.final
+    [%#sinvariant29] inv'15 self.current /\ inv'15 self.final
   
   predicate inv'8 (_1 : borrowed (borrowed (Seq.seq (t_PtrOwn'0))))
   
   axiom inv_axiom'7 [@rewrite] : forall x : borrowed (borrowed (Seq.seq (t_PtrOwn'0))) [inv'8 x] . inv'8 x
   = invariant'3 x
   
-  let rec deref_mut'0 (self:borrowed (t_GhostBox'2)) (return'  (ret:borrowed (borrowed (Seq.seq (t_PtrOwn'0)))))= {[@expl:deref_mut 'self' type invariant] [%#sghost15] inv'9 self}
+  let rec deref_mut'0 (self:borrowed (t_GhostBox'2)) (return'  (ret:borrowed (borrowed (Seq.seq (t_PtrOwn'0)))))= {[@expl:deref_mut 'self' type invariant] [%#sghost14] inv'9 self}
     any
-    [ return' (result:borrowed (borrowed (Seq.seq (t_PtrOwn'0))))-> {[%#sghost16] inv'8 result}
-      {[%#sghost17] result
+    [ return' (result:borrowed (borrowed (Seq.seq (t_PtrOwn'0))))-> {[%#sghost15] inv'8 result}
+      {[%#sghost16] result
       = Borrow.borrow_logic (self.current).t_GhostBox__0'2 (self.final).t_GhostBox__0'2 (Borrow.inherit_id (Borrow.get_id self) 1)}
       (! return' {result}) ]
     
   
-  let rec into_inner'0 (self:t_GhostBox'0) (return'  (ret:t_PtrOwn'0))= {[@expl:into_inner 'self' type invariant] [%#sghost18] inv'13 self}
+  let rec into_inner'0 (self:t_GhostBox'0) (return'  (ret:t_PtrOwn'0))= {[@expl:into_inner 'self' type invariant] [%#sghost17] inv'13 self}
     any
-    [ return' (result:t_PtrOwn'0)-> {[%#sghost19] inv'14 result}
-      {[%#sghost20] result = self.t_GhostBox__0'0}
+    [ return' (result:t_PtrOwn'0)-> {[%#sghost18] inv'14 result}
+      {[%#sghost19] result = self.t_GhostBox__0'0}
       (! return' {result}) ]
     
   
@@ -1183,18 +1174,18 @@ module M_linked_list__qyi14323471455460008969__push_front [#"linked_list.rs" 100
   function push_front'2 [@inline:trivial] (self : Seq.seq (t_PtrOwn'0)) (x : t_PtrOwn'0) : Seq.seq (t_PtrOwn'0) =
     [%#sseq11] Seq.cons x self
   
-  let rec push_front_ghost'0 (self:borrowed (Seq.seq (t_PtrOwn'0))) (x:t_PtrOwn'0) (return'  (ret:()))= {[@expl:push_front_ghost 'self' type invariant] [%#sseq21] inv'15 self}
-    {[@expl:push_front_ghost 'x' type invariant] [%#sseq22] inv'14 x}
-    any [ return' (result:())-> {[%#sseq23] self.final = push_front'2 self.current x} (! return' {result}) ] 
+  let rec push_front_ghost'0 (self:borrowed (Seq.seq (t_PtrOwn'0))) (x:t_PtrOwn'0) (return'  (ret:()))= {[@expl:push_front_ghost 'self' type invariant] [%#sseq20] inv'15 self}
+    {[@expl:push_front_ghost 'x' type invariant] [%#sseq21] inv'14 x}
+    any [ return' (result:())-> {[%#sseq22] self.final = push_front'2 self.current x} (! return' {result}) ] 
   
   predicate resolve'6 (self : borrowed (borrowed (Seq.seq (t_PtrOwn'0)))) =
-    [%#sresolve28] self.final = self.current
+    [%#sresolve27] self.final = self.current
   
   predicate resolve'2 (_1 : borrowed (borrowed (Seq.seq (t_PtrOwn'0)))) =
     resolve'6 _1
   
   predicate resolve'7 (self : borrowed (t_GhostBox'2)) =
-    [%#sresolve28] self.final = self.current
+    [%#sresolve27] self.final = self.current
   
   predicate resolve'3 (_1 : borrowed (t_GhostBox'2)) =
     resolve'7 _1
@@ -1210,10 +1201,10 @@ module M_linked_list__qyi14323471455460008969__push_front [#"linked_list.rs" 100
   
   axiom inv_axiom'16 [@rewrite] : forall x : t_GhostBox'3 [inv'17 x] . inv'17 x = true
   
-  let rec new'1 (x:()) (return'  (ret:t_GhostBox'3))= {[@expl:new 'x' type invariant] [%#sghost24] inv'16 x}
+  let rec new'1 (x:()) (return'  (ret:t_GhostBox'3))= {[@expl:new 'x' type invariant] [%#sghost23] inv'16 x}
     any
-    [ return' (result:t_GhostBox'3)-> {[%#sghost25] inv'17 result}
-      {[%#sghost26] result.t_GhostBox__0'3 = x}
+    [ return' (result:t_GhostBox'3)-> {[%#sghost24] inv'17 result}
+      {[%#sghost25] result.t_GhostBox__0'3 = x}
       (! return' {result}) ]
     
   
@@ -1281,19 +1272,19 @@ module M_linked_list__qyi14323471455460008969__push_front [#"linked_list.rs" 100
      [ return' (result:t_GhostBox'3)-> return' {result} ] 
   
   predicate resolve'11 (self : borrowed (Seq.seq (t_PtrOwn'0))) =
-    [%#sresolve28] self.final = self.current
+    [%#sresolve27] self.final = self.current
   
   predicate resolve'10 (_1 : borrowed (Seq.seq (t_PtrOwn'0))) =
     resolve'11 _1
   
   predicate resolve'9 (self : borrowed (Seq.seq (t_PtrOwn'0))) =
-    [%#sresolve32] resolve'10 self
+    [%#sresolve31] resolve'10 self
   
   predicate resolve'8 (_1 : borrowed (Seq.seq (t_PtrOwn'0))) =
     resolve'9 _1
   
   predicate resolve'4 (self : t_GhostBox'2) =
-    [%#sghost27] resolve'8 self.t_GhostBox__0'2
+    [%#sghost26] resolve'8 self.t_GhostBox__0'2
   
   predicate resolve'0 (_1 : t_GhostBox'2) =
     resolve'4 _1
@@ -1306,7 +1297,7 @@ module M_linked_list__qyi14323471455460008969__push_front [#"linked_list.rs" 100
   use seq.Seq
   
   predicate invariant'9 [#"linked_list.rs" 24 4 24 30] (self : t_List'0) =
-    [%#slinked_list35] inner_logic'1 self.t_List__seq'0 = (Seq.empty  : Seq.seq (t_PtrOwn'0))
+    [%#slinked_list34] inner_logic'1 self.t_List__seq'0 = (Seq.empty  : Seq.seq (t_PtrOwn'0))
     /\ is_null_logic'0 self.t_List__first'0 /\ is_null_logic'0 self.t_List__last'0
     \/ Seq.length (inner_logic'1 self.t_List__seq'0) > 0
     /\ self.t_List__first'0 = ptr'0 (Seq.get (inner_logic'1 self.t_List__seq'0) 0)
@@ -1327,14 +1318,14 @@ module M_linked_list__qyi14323471455460008969__push_front [#"linked_list.rs" 100
     end)
   
   predicate invariant'0 (self : borrowed (t_List'0)) =
-    [%#sinvariant30] inv'18 self.current /\ inv'18 self.final
+    [%#sinvariant29] inv'18 self.current /\ inv'18 self.final
   
   predicate inv'2 (_1 : borrowed (t_List'0))
   
   axiom inv_axiom'2 [@rewrite] : forall x : borrowed (t_List'0) [inv'2 x] . inv'2 x = invariant'0 x
   
   predicate resolve'5 (self : borrowed (t_List'0)) =
-    [%#sresolve28] self.final = self.current
+    [%#sresolve27] self.final = self.current
   
   predicate resolve'1 (_1 : borrowed (t_List'0)) =
     resolve'5 _1
@@ -1354,7 +1345,7 @@ module M_linked_list__qyi14323471455460008969__push_front [#"linked_list.rs" 100
   function seq_map'0 [#"linked_list.rs" 66 0 66 66] (s : Seq.seq (t_PtrOwn'0)) (f : Map.map (t_PtrOwn'0) t_T'0) : Seq.seq t_T'0
     
    =
-    [%#slinked_list29] Seq.create (Seq.length s) (Mapping.from_fn (fun (i : int) -> Map.get f (Seq.get s i)))
+    [%#slinked_list28] Seq.create (Seq.length s) (Mapping.from_fn (fun (i : int) -> Map.get f (Seq.get s i)))
   
   function view'0 [#"linked_list.rs" 46 4 46 33] (self : t_List'0) : Seq.seq t_T'0 =
     [%#slinked_list10] seq_map'0 (inner_logic'1 self.t_List__seq'0) (Mapping.from_fn (fun (ptr_own : t_PtrOwn'0) -> (val'0 ptr_own).t_Cell__v'0))
diff --git a/creusot/tests/should_succeed/linked_list.rs b/creusot/tests/should_succeed/linked_list.rs
index 9a2d3d4025..c65ce0f79c 100644
--- a/creusot/tests/should_succeed/linked_list.rs
+++ b/creusot/tests/should_succeed/linked_list.rs
@@ -76,7 +76,7 @@ impl<T> List<T> {
     #[ensures((^self)@ == (*self)@.push_back(x))]
     pub fn push_back(&mut self, x: T) {
         let cell = Box::new(Cell { v: x, next: std::ptr::null() });
-        let (cell_ptr, cell_own) = ptr_own::from_box(cell);
+        let (cell_ptr, cell_own) = PtrOwn::from_box(cell);
         if self.last.is_null() {
             self.first = cell_ptr;
             self.last = cell_ptr;
@@ -84,7 +84,7 @@ impl<T> List<T> {
             ghost! { seq.push_back_ghost(cell_own.into_inner()) };
         } else {
             let seq = self.seq.borrow_mut();
-            let cell_last = ptr_own::as_mut(
+            let cell_last = PtrOwn::as_mut(
                 self.last,
                 ghost! {
                     let off = minus_one(seq.len_ghost());
@@ -98,7 +98,7 @@ impl<T> List<T> {
 
     #[ensures((^self)@ == (*self)@.push_front(x))]
     pub fn push_front(&mut self, x: T) {
-        let (cell_ptr, cell_own) = ptr_own::new(Cell { v: x, next: self.first });
+        let (cell_ptr, cell_own) = PtrOwn::new(Cell { v: x, next: self.first });
         self.first = cell_ptr;
         if self.last.is_null() {
             self.last = cell_ptr;
diff --git a/creusot/tests/should_succeed/linked_list/why3session.xml b/creusot/tests/should_succeed/linked_list/why3session.xml
index 8f52eae4f1..45fbc1e8f5 100644
--- a/creusot/tests/should_succeed/linked_list/why3session.xml
+++ b/creusot/tests/should_succeed/linked_list/why3session.xml
@@ -14,12 +14,12 @@
 </theory>
 <theory name="M_linked_list__qyi14323471455460008969__push_back" proved="true">
  <goal name="vc_push_back&#39;0" proved="true">
- <proof prover="1"><result status="valid" time="0.556228" steps="119109"/></proof>
+ <proof prover="1"><result status="valid" time="0.808432" steps="119021"/></proof>
  </goal>
 </theory>
 <theory name="M_linked_list__qyi14323471455460008969__push_front" proved="true">
  <goal name="vc_push_front&#39;0" proved="true">
- <proof prover="0"><result status="valid" time="0.057417" steps="242091"/></proof>
+ <proof prover="0"><result status="valid" time="0.057417" steps="116256"/></proof>
  </goal>
 </theory>
 </file>
diff --git a/creusot/tests/should_succeed/linked_list/why3shapes.gz b/creusot/tests/should_succeed/linked_list/why3shapes.gz
index 95f32350cf..ff971d66b0 100644
Binary files a/creusot/tests/should_succeed/linked_list/why3shapes.gz and b/creusot/tests/should_succeed/linked_list/why3shapes.gz differ