diff --git a/creusot-contracts-proc/src/pretyping.rs b/creusot-contracts-proc/src/pretyping.rs
index 7a85f6c4aa..d61fce197d 100644
--- a/creusot-contracts-proc/src/pretyping.rs
+++ b/creusot-contracts-proc/src/pretyping.rs
@@ -149,7 +149,18 @@ pub fn encode_term(term: &RT) -> Result<TokenStream, EncodeError> {
             Ok(quote_spanned! {sp=> (#term) })
         }
         RT::Path(_) => Ok(quote_spanned! {sp=> #term }),
-        RT::Range(_) => Err(EncodeError::Unsupported(term.span(), "Range".into())),
+        RT::Range(TermRange { from, limits, to }) => {
+            let from = match from {
+                None => None,
+                Some(from) => Some(encode_term(from)?),
+            };
+            let to = match to {
+                None => None,
+                Some(to) => Some(encode_term(to)?),
+            };
+            let limits = limits;
+            Ok(quote_spanned! {sp=>#from #limits #to})
+        }
         RT::Reference(TermReference { mutability, expr, .. }) => {
             let term = encode_term(expr)?;
             Ok(quote! {
diff --git a/creusot-contracts/src/logic/seq.rs b/creusot-contracts/src/logic/seq.rs
index 2d60f8e206..49c7d0820f 100644
--- a/creusot-contracts/src/logic/seq.rs
+++ b/creusot-contracts/src/logic/seq.rs
@@ -1,3 +1,5 @@
+use ::std::ops::Range;
+
 use crate::{logic::ops::IndexLogic, *};
 
 #[cfg_attr(creusot, creusot::builtins = "seq.Seq.seq")]
@@ -165,3 +167,14 @@ impl<T> IndexLogic<Int> for Seq<T> {
         absurd
     }
 }
+
+impl<T> IndexLogic<Range<Int>> for Seq<T> {
+    type Item = Seq<T>;
+
+    #[ghost]
+    #[open]
+    #[why3::attr = "inline:trivial"]
+    fn index_logic(self, r: Range<Int>) -> Self::Item {
+        self.subsequence(r.start, r.end)
+    }
+}
diff --git a/creusot-contracts/src/std/deque.rs b/creusot-contracts/src/std/deque.rs
index 1f5ca787e1..e654ffb072 100644
--- a/creusot-contracts/src/std/deque.rs
+++ b/creusot-contracts/src/std/deque.rs
@@ -1,4 +1,5 @@
-use crate::{logic::IndexLogic, std::alloc::Allocator, *};
+use crate::{invariant::Invariant, logic::IndexLogic, std::alloc::Allocator, *};
+use ::std::collections::vec_deque::{IntoIter, Iter};
 pub use ::std::collections::VecDeque;
 
 impl<T, A: Allocator> ShallowModel for VecDeque<T, A> {
@@ -13,6 +14,131 @@ impl<T, A: Allocator> ShallowModel for VecDeque<T, A> {
     }
 }
 
+impl<'a, T> Invariant for Iter<'a, T> {}
+
+impl<T, A: Allocator> ShallowModel for IntoIter<T, A> {
+    type ShallowModelTy = Seq<T>;
+
+    #[open(self)]
+    #[ghost]
+    #[trusted]
+    fn shallow_model(self) -> Self::ShallowModelTy {
+        absurd
+    }
+}
+
+impl<'a, T> ShallowModel for Iter<'a, T> {
+    // TODO : This seems wrong
+    type ShallowModelTy = &'a [T];
+
+    #[ghost]
+    #[open(self)]
+    #[trusted]
+    fn shallow_model(self) -> Self::ShallowModelTy {
+        absurd
+    }
+}
+
+impl<'a, T> Iterator for Iter<'a, T> {
+    #[predicate]
+    #[open]
+    fn completed(&mut self) -> bool {
+        pearlite! { self.resolve() && (*self)@@ == Seq::EMPTY }
+    }
+
+    #[predicate]
+    #[open]
+    fn produces(self, visited: Seq<Self::Item>, tl: Self) -> bool {
+        pearlite! {
+            self@.to_ref_seq() == visited.concat(tl@.to_ref_seq())
+        }
+    }
+
+    #[law]
+    #[open]
+    #[ensures(a.produces(Seq::EMPTY, a))]
+    fn produces_refl(a: Self) {}
+
+    #[law]
+    #[open]
+    #[requires(a.produces(ab, b))]
+    #[requires(b.produces(bc, c))]
+    #[ensures(a.produces(ab.concat(bc), c))]
+    fn produces_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {}
+}
+
+impl<T, A: Allocator> Invariant for IntoIter<T, A> {}
+
+impl<T, A: Allocator> Iterator for IntoIter<T, A> {
+    #[predicate]
+    #[open]
+    fn completed(&mut self) -> bool {
+        pearlite! { self.resolve() && self@ == Seq::EMPTY }
+    }
+
+    #[predicate]
+    #[open]
+    fn produces(self, visited: Seq<T>, rhs: Self) -> bool {
+        pearlite! {
+            self@ == visited.concat(rhs@)
+        }
+    }
+
+    #[law]
+    #[open]
+    #[ensures(a.produces(Seq::EMPTY, a))]
+    fn produces_refl(a: Self) {}
+
+    #[law]
+    #[open]
+    #[requires(a.produces(ab, b))]
+    #[requires(b.produces(bc, c))]
+    #[ensures(a.produces(ab.concat(bc), c))]
+    fn produces_trans(a: Self, ab: Seq<T>, b: Self, bc: Seq<T>, c: Self) {}
+}
+
+impl<T, A: Allocator> IntoIterator for VecDeque<T, A> {
+    #[predicate]
+    #[open]
+    fn into_iter_pre(self) -> bool {
+        pearlite! { true }
+    }
+
+    #[predicate]
+    #[open]
+    fn into_iter_post(self, res: Self::IntoIter) -> bool {
+        pearlite! { self@ == res@ }
+    }
+}
+
+impl<T, A: Allocator> IntoIterator for &VecDeque<T, A> {
+    #[predicate]
+    #[open]
+    fn into_iter_pre(self) -> bool {
+        pearlite! { true }
+    }
+
+    #[predicate]
+    #[open]
+    fn into_iter_post(self, res: Self::IntoIter) -> bool {
+        pearlite! { self@ == res@@ }
+    }
+}
+
+// impl<T, A: Allocator> IntoIterator for &mut VecDeque<T, A> {
+//     #[predicate]
+//     #[open]
+//     fn into_iter_pre(self) -> bool {
+//         pearlite! { true }
+//     }
+
+//     #[predicate]
+//     #[open]
+//     fn into_iter_post(self, res: Self::IntoIter) -> bool {
+//         pearlite! { self@ == res@@ }
+//     }
+// }
+
 impl<T: DeepModel, A: Allocator> DeepModel for VecDeque<T, A> {
     type DeepModelTy = Seq<T::DeepModelTy>;
 
diff --git a/creusot-contracts/src/std/ops.rs b/creusot-contracts/src/std/ops.rs
index f4769a50f2..ac01d404e7 100644
--- a/creusot-contracts/src/std/ops.rs
+++ b/creusot-contracts/src/std/ops.rs
@@ -247,12 +247,12 @@ extern_spec! {
 extern_spec! {
     mod std {
         mod ops {
-            trait IndexMut<Idx>  {
+            trait IndexMut<Idx> where Self : ?Sized  {
                 #[requires(false)]
                 fn index_mut(&mut self, _ix : Idx) -> &mut Self::Output;
             }
 
-            trait Index<Idx> {
+            trait Index<Idx> where Self : ?Sized {
                 #[requires(false)]
                 fn index(&self, _ix : Idx) -> &Self::Output;
             }
diff --git a/creusot-contracts/src/std/slice.rs b/creusot-contracts/src/std/slice.rs
index 10f4995799..8830e30890 100644
--- a/creusot-contracts/src/std/slice.rs
+++ b/creusot-contracts/src/std/slice.rs
@@ -231,6 +231,11 @@ impl<T> SliceIndex<[T]> for RangeToInclusive<usize> {
 
 extern_spec! {
     impl<T> [T] {
+        #[requires(self@.len() == src@.len())]
+        #[ensures((^self)@ == src@)]
+        fn copy_from_slice(&mut self, src: &[T])
+            where T : Copy;
+
         #[ensures(self@.len() == result@)]
         fn len(&self) -> usize;
 
diff --git a/creusot/tests/should_succeed/bug/217.mlcfg b/creusot/tests/should_succeed/bug/217.mlcfg
index 68e28d219a..af5719df2d 100644
--- a/creusot/tests/should_succeed/bug/217.mlcfg
+++ b/creusot/tests/should_succeed/bug/217.mlcfg
@@ -17,7 +17,7 @@ module CreusotContracts_Logic_Seq_Impl0_Tail
   use seq.Seq
   use seq_ext.SeqExt
   function tail (self : Seq.seq t) : Seq.seq t =
-    [#"../../../../../creusot-contracts/src/logic/seq.rs" 47 8 47 39] SeqExt.subsequence self 1 (Seq.length self)
+    [#"../../../../../creusot-contracts/src/logic/seq.rs" 49 8 49 39] SeqExt.subsequence self 1 (Seq.length self)
   val tail (self : Seq.seq t) : Seq.seq t
     ensures { result = tail self }
     
diff --git a/creusot/tests/should_succeed/heapsort_generic.mlcfg b/creusot/tests/should_succeed/heapsort_generic.mlcfg
index 37588eee47..ceb02bd917 100644
--- a/creusot/tests/should_succeed/heapsort_generic.mlcfg
+++ b/creusot/tests/should_succeed/heapsort_generic.mlcfg
@@ -1082,7 +1082,7 @@ module CreusotContracts_Logic_Seq_Impl0_PermutationOf
   use seq.Seq
   use seq.Permut
   predicate permutation_of (self : Seq.seq t) (o : Seq.seq t) =
-    [#"../../../../creusot-contracts/src/logic/seq.rs" 101 8 101 37] Permut.permut self o 0 (Seq.length self)
+    [#"../../../../creusot-contracts/src/logic/seq.rs" 103 8 103 37] Permut.permut self o 0 (Seq.length self)
   val permutation_of (self : Seq.seq t) (o : Seq.seq t) : bool
     ensures { result = permutation_of self o }
     
@@ -1490,10 +1490,10 @@ module Core_Slice_Impl0_Swap_Interface
     type t = slice t,
     type ShallowModelTy0.shallowModelTy = Seq.seq t
   val swap (self : borrowed (slice t)) (a : usize) (b : usize) : ()
-    requires {[#"../../../../creusot-contracts/src/std/slice.rs" 237 19 237 35] UIntSize.to_int a < Seq.length (ShallowModel0.shallow_model self)}
-    requires {[#"../../../../creusot-contracts/src/std/slice.rs" 238 19 238 35] UIntSize.to_int b < Seq.length (ShallowModel0.shallow_model self)}
+    requires {[#"../../../../creusot-contracts/src/std/slice.rs" 242 19 242 35] UIntSize.to_int a < Seq.length (ShallowModel0.shallow_model self)}
+    requires {[#"../../../../creusot-contracts/src/std/slice.rs" 243 19 243 35] UIntSize.to_int b < Seq.length (ShallowModel0.shallow_model self)}
     requires {Inv0.inv self}
-    ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 239 8 239 52] Permut.exchange (ShallowModel1.shallow_model ( ^ self)) (ShallowModel0.shallow_model self) (UIntSize.to_int a) (UIntSize.to_int b) }
+    ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 244 8 244 52] Permut.exchange (ShallowModel1.shallow_model ( ^ self)) (ShallowModel0.shallow_model self) (UIntSize.to_int a) (UIntSize.to_int b) }
     
 end
 module CreusotContracts_Std1_Slice_Impl5_InBounds_Stub
diff --git a/creusot/tests/should_succeed/hillel.mlcfg b/creusot/tests/should_succeed/hillel.mlcfg
index 4c1df098a2..0a348341be 100644
--- a/creusot/tests/should_succeed/hillel.mlcfg
+++ b/creusot/tests/should_succeed/hillel.mlcfg
@@ -1323,7 +1323,7 @@ module CreusotContracts_Std1_Slice_Impl15_Produces
   predicate produces (self : Core_Slice_Iter_Iter_Type.t_iter t) (visited : Seq.seq t) (tl : Core_Slice_Iter_Iter_Type.t_iter t)
     
    =
-    [#"../../../../creusot-contracts/src/std/slice.rs" 378 12 378 66] ToRefSeq0.to_ref_seq (ShallowModel0.shallow_model self) = Seq.(++) visited (ToRefSeq0.to_ref_seq (ShallowModel0.shallow_model tl))
+    [#"../../../../creusot-contracts/src/std/slice.rs" 383 12 383 66] ToRefSeq0.to_ref_seq (ShallowModel0.shallow_model self) = Seq.(++) visited (ToRefSeq0.to_ref_seq (ShallowModel0.shallow_model tl))
   val produces (self : Core_Slice_Iter_Iter_Type.t_iter t) (visited : Seq.seq t) (tl : Core_Slice_Iter_Iter_Type.t_iter t) : bool
     ensures { result = produces self visited tl }
     
@@ -1433,7 +1433,7 @@ module Core_Slice_Impl0_Iter_Interface
     type t = slice t
   val iter (self : slice t) : Core_Slice_Iter_Iter_Type.t_iter t
     requires {Inv0.inv self}
-    ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 232 0 324 1] ShallowModel0.shallow_model result = self }
+    ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 232 0 329 1] ShallowModel0.shallow_model result = self }
     
 end
 module CreusotContracts_Std1_Iter_IntoIterator_IntoIterPre_Stub
@@ -1534,7 +1534,7 @@ module CreusotContracts_Std1_Slice_Impl15_Completed
   clone CreusotContracts_Resolve_Impl1_Resolve_Stub as Resolve0 with
     type t = Core_Slice_Iter_Iter_Type.t_iter t
   predicate completed (self : borrowed (Core_Slice_Iter_Iter_Type.t_iter t)) =
-    [#"../../../../creusot-contracts/src/std/slice.rs" 371 20 371 61] Resolve0.resolve self /\ ShallowModel1.shallow_model (ShallowModel0.shallow_model self) = Seq.empty 
+    [#"../../../../creusot-contracts/src/std/slice.rs" 376 20 376 61] Resolve0.resolve self /\ ShallowModel1.shallow_model (ShallowModel0.shallow_model self) = Seq.empty 
   val completed (self : borrowed (Core_Slice_Iter_Iter_Type.t_iter t)) : bool
     ensures { result = completed self }
     
@@ -1641,10 +1641,10 @@ module CreusotContracts_Std1_Slice_Impl15_ProducesRefl_Interface
     type t = t
   function produces_refl (a : Core_Slice_Iter_Iter_Type.t_iter t) : ()
   val produces_refl (a : Core_Slice_Iter_Iter_Type.t_iter t) : ()
-    ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 384 14 384 39] Produces0.produces a (Seq.empty ) a }
+    ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 389 14 389 39] Produces0.produces a (Seq.empty ) a }
     ensures { result = produces_refl a }
     
-  axiom produces_refl_spec : forall a : Core_Slice_Iter_Iter_Type.t_iter t . [#"../../../../creusot-contracts/src/std/slice.rs" 384 14 384 39] Produces0.produces a (Seq.empty ) a
+  axiom produces_refl_spec : forall a : Core_Slice_Iter_Iter_Type.t_iter t . [#"../../../../creusot-contracts/src/std/slice.rs" 389 14 389 39] Produces0.produces a (Seq.empty ) a
 end
 module CreusotContracts_Std1_Slice_Impl15_ProducesRefl
   type t
@@ -1653,12 +1653,12 @@ module CreusotContracts_Std1_Slice_Impl15_ProducesRefl
   clone CreusotContracts_Std1_Slice_Impl15_Produces_Stub as Produces0 with
     type t = t
   function produces_refl (a : Core_Slice_Iter_Iter_Type.t_iter t) : () =
-    [#"../../../../creusot-contracts/src/std/slice.rs" 382 4 382 10] ()
+    [#"../../../../creusot-contracts/src/std/slice.rs" 387 4 387 10] ()
   val produces_refl (a : Core_Slice_Iter_Iter_Type.t_iter t) : ()
-    ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 384 14 384 39] Produces0.produces a (Seq.empty ) a }
+    ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 389 14 389 39] Produces0.produces a (Seq.empty ) a }
     ensures { result = produces_refl a }
     
-  axiom produces_refl_spec : forall a : Core_Slice_Iter_Iter_Type.t_iter t . [#"../../../../creusot-contracts/src/std/slice.rs" 384 14 384 39] Produces0.produces a (Seq.empty ) a
+  axiom produces_refl_spec : forall a : Core_Slice_Iter_Iter_Type.t_iter t . [#"../../../../creusot-contracts/src/std/slice.rs" 389 14 389 39] Produces0.produces a (Seq.empty ) a
 end
 module CreusotContracts_Std1_Slice_Impl15_ProducesTrans_Stub
   type t
@@ -1680,12 +1680,12 @@ module CreusotContracts_Std1_Slice_Impl15_ProducesTrans_Interface
   function produces_trans (a : Core_Slice_Iter_Iter_Type.t_iter t) (ab : Seq.seq t) (b : Core_Slice_Iter_Iter_Type.t_iter t) (bc : Seq.seq t) (c : Core_Slice_Iter_Iter_Type.t_iter t) : ()
     
   val produces_trans (a : Core_Slice_Iter_Iter_Type.t_iter t) (ab : Seq.seq t) (b : Core_Slice_Iter_Iter_Type.t_iter t) (bc : Seq.seq t) (c : Core_Slice_Iter_Iter_Type.t_iter t) : ()
-    requires {[#"../../../../creusot-contracts/src/std/slice.rs" 389 15 389 32] Produces0.produces a ab b}
-    requires {[#"../../../../creusot-contracts/src/std/slice.rs" 390 15 390 32] Produces0.produces b bc c}
-    ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 391 14 391 42] Produces0.produces a (Seq.(++) ab bc) c }
+    requires {[#"../../../../creusot-contracts/src/std/slice.rs" 394 15 394 32] Produces0.produces a ab b}
+    requires {[#"../../../../creusot-contracts/src/std/slice.rs" 395 15 395 32] Produces0.produces b bc c}
+    ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 396 14 396 42] Produces0.produces a (Seq.(++) ab bc) c }
     ensures { result = produces_trans a ab b bc c }
     
-  axiom produces_trans_spec : forall a : Core_Slice_Iter_Iter_Type.t_iter t, ab : Seq.seq t, b : Core_Slice_Iter_Iter_Type.t_iter t, bc : Seq.seq t, c : Core_Slice_Iter_Iter_Type.t_iter t . ([#"../../../../creusot-contracts/src/std/slice.rs" 389 15 389 32] Produces0.produces a ab b) -> ([#"../../../../creusot-contracts/src/std/slice.rs" 390 15 390 32] Produces0.produces b bc c) -> ([#"../../../../creusot-contracts/src/std/slice.rs" 391 14 391 42] Produces0.produces a (Seq.(++) ab bc) c)
+  axiom produces_trans_spec : forall a : Core_Slice_Iter_Iter_Type.t_iter t, ab : Seq.seq t, b : Core_Slice_Iter_Iter_Type.t_iter t, bc : Seq.seq t, c : Core_Slice_Iter_Iter_Type.t_iter t . ([#"../../../../creusot-contracts/src/std/slice.rs" 394 15 394 32] Produces0.produces a ab b) -> ([#"../../../../creusot-contracts/src/std/slice.rs" 395 15 395 32] Produces0.produces b bc c) -> ([#"../../../../creusot-contracts/src/std/slice.rs" 396 14 396 42] Produces0.produces a (Seq.(++) ab bc) c)
 end
 module CreusotContracts_Std1_Slice_Impl15_ProducesTrans
   type t
@@ -1697,14 +1697,14 @@ module CreusotContracts_Std1_Slice_Impl15_ProducesTrans
   function produces_trans (a : Core_Slice_Iter_Iter_Type.t_iter t) (ab : Seq.seq t) (b : Core_Slice_Iter_Iter_Type.t_iter t) (bc : Seq.seq t) (c : Core_Slice_Iter_Iter_Type.t_iter t) : ()
     
    =
-    [#"../../../../creusot-contracts/src/std/slice.rs" 387 4 387 10] ()
+    [#"../../../../creusot-contracts/src/std/slice.rs" 392 4 392 10] ()
   val produces_trans (a : Core_Slice_Iter_Iter_Type.t_iter t) (ab : Seq.seq t) (b : Core_Slice_Iter_Iter_Type.t_iter t) (bc : Seq.seq t) (c : Core_Slice_Iter_Iter_Type.t_iter t) : ()
-    requires {[#"../../../../creusot-contracts/src/std/slice.rs" 389 15 389 32] Produces0.produces a ab b}
-    requires {[#"../../../../creusot-contracts/src/std/slice.rs" 390 15 390 32] Produces0.produces b bc c}
-    ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 391 14 391 42] Produces0.produces a (Seq.(++) ab bc) c }
+    requires {[#"../../../../creusot-contracts/src/std/slice.rs" 394 15 394 32] Produces0.produces a ab b}
+    requires {[#"../../../../creusot-contracts/src/std/slice.rs" 395 15 395 32] Produces0.produces b bc c}
+    ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 396 14 396 42] Produces0.produces a (Seq.(++) ab bc) c }
     ensures { result = produces_trans a ab b bc c }
     
-  axiom produces_trans_spec : forall a : Core_Slice_Iter_Iter_Type.t_iter t, ab : Seq.seq t, b : Core_Slice_Iter_Iter_Type.t_iter t, bc : Seq.seq t, c : Core_Slice_Iter_Iter_Type.t_iter t . ([#"../../../../creusot-contracts/src/std/slice.rs" 389 15 389 32] Produces0.produces a ab b) -> ([#"../../../../creusot-contracts/src/std/slice.rs" 390 15 390 32] Produces0.produces b bc c) -> ([#"../../../../creusot-contracts/src/std/slice.rs" 391 14 391 42] Produces0.produces a (Seq.(++) ab bc) c)
+  axiom produces_trans_spec : forall a : Core_Slice_Iter_Iter_Type.t_iter t, ab : Seq.seq t, b : Core_Slice_Iter_Iter_Type.t_iter t, bc : Seq.seq t, c : Core_Slice_Iter_Iter_Type.t_iter t . ([#"../../../../creusot-contracts/src/std/slice.rs" 394 15 394 32] Produces0.produces a ab b) -> ([#"../../../../creusot-contracts/src/std/slice.rs" 395 15 395 32] Produces0.produces b bc c) -> ([#"../../../../creusot-contracts/src/std/slice.rs" 396 14 396 42] Produces0.produces a (Seq.(++) ab bc) c)
 end
 module Hillel_InsertUnique_Interface
   type t
@@ -2209,7 +2209,7 @@ module CreusotContracts_Logic_Seq_Impl0_New
   type t
   use seq.Seq
   function new (_1 : ()) : Seq.seq t =
-    [#"../../../../creusot-contracts/src/logic/seq.rs" 15 8 15 19] Seq.empty 
+    [#"../../../../creusot-contracts/src/logic/seq.rs" 17 8 17 19] Seq.empty 
   val new (_1 : ()) : Seq.seq t
     ensures { result = new _1 }
     
@@ -2335,7 +2335,7 @@ module Core_Slice_Impl0_Len_Interface
     type t = slice t
   val len (self : slice t) : usize
     requires {Inv0.inv self}
-    ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 232 0 324 1] Seq.length (ShallowModel0.shallow_model self) = UIntSize.to_int result }
+    ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 232 0 329 1] Seq.length (ShallowModel0.shallow_model self) = UIntSize.to_int result }
     
 end
 module CreusotContracts_Std1_Iter_Iterator_Completed_Stub
@@ -3257,7 +3257,7 @@ module CreusotContracts_Std1_Slice_Impl11_IntoIterPre
   use prelude.Borrow
   use prelude.Slice
   predicate into_iter_pre (self : slice t) =
-    [#"../../../../creusot-contracts/src/std/slice.rs" 330 20 330 24] true
+    [#"../../../../creusot-contracts/src/std/slice.rs" 335 20 335 24] true
   val into_iter_pre (self : slice t) : bool
     ensures { result = into_iter_pre self }
     
@@ -3287,7 +3287,7 @@ module CreusotContracts_Std1_Slice_Impl11_IntoIterPost
   clone CreusotContracts_Std1_Slice_Impl13_ShallowModel_Stub as ShallowModel0 with
     type t = t
   predicate into_iter_post (self : slice t) (res : Core_Slice_Iter_Iter_Type.t_iter t) =
-    [#"../../../../creusot-contracts/src/std/slice.rs" 336 20 336 32] self = ShallowModel0.shallow_model res
+    [#"../../../../creusot-contracts/src/std/slice.rs" 341 20 341 32] self = ShallowModel0.shallow_model res
   val into_iter_post (self : slice t) (res : Core_Slice_Iter_Iter_Type.t_iter t) : bool
     ensures { result = into_iter_post self res }
     
diff --git a/creusot/tests/should_succeed/index_range.mlcfg b/creusot/tests/should_succeed/index_range.mlcfg
index c321597416..3c6d559960 100644
--- a/creusot/tests/should_succeed/index_range.mlcfg
+++ b/creusot/tests/should_succeed/index_range.mlcfg
@@ -665,7 +665,7 @@ module Core_Slice_Impl0_Len_Interface
     type t = slice t
   val len (self : slice t) : usize
     requires {Inv0.inv self}
-    ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 232 0 324 1] Seq.length (ShallowModel0.shallow_model self) = UIntSize.to_int result }
+    ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 232 0 329 1] Seq.length (ShallowModel0.shallow_model self) = UIntSize.to_int result }
     
 end
 module Alloc_Vec_Impl8_Deref_Interface
@@ -726,8 +726,8 @@ module Core_Slice_Impl0_Get_Interface
   val get (self : slice t) (index : i) : Core_Option_Option_Type.t_option Output0.output
     requires {Inv0.inv self}
     requires {Inv1.inv index}
-    ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 242 8 242 102] InBounds0.in_bounds index (ShallowModel0.shallow_model self) -> (exists r : Output0.output . Inv2.inv r /\ result = Core_Option_Option_Type.C_Some r /\ HasValue0.has_value index (ShallowModel0.shallow_model self) r) }
-    ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 243 18 243 55] InBounds0.in_bounds index (ShallowModel0.shallow_model self) \/ result = Core_Option_Option_Type.C_None }
+    ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 247 8 247 102] InBounds0.in_bounds index (ShallowModel0.shallow_model self) -> (exists r : Output0.output . Inv2.inv r /\ result = Core_Option_Option_Type.C_Some r /\ HasValue0.has_value index (ShallowModel0.shallow_model self) r) }
+    ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 248 18 248 55] InBounds0.in_bounds index (ShallowModel0.shallow_model self) \/ result = Core_Option_Option_Type.C_None }
     ensures { Inv3.inv result }
     
 end
diff --git a/creusot/tests/should_succeed/iterators/02_iter_mut.mlcfg b/creusot/tests/should_succeed/iterators/02_iter_mut.mlcfg
index 314a2ddc0c..a73bbe03fa 100644
--- a/creusot/tests/should_succeed/iterators/02_iter_mut.mlcfg
+++ b/creusot/tests/should_succeed/iterators/02_iter_mut.mlcfg
@@ -678,7 +678,7 @@ module CreusotContracts_Logic_Seq_Impl0_Tail
   use seq.Seq
   use seq_ext.SeqExt
   function tail (self : Seq.seq t) : Seq.seq t =
-    [#"../../../../../creusot-contracts/src/logic/seq.rs" 47 8 47 39] SeqExt.subsequence self 1 (Seq.length self)
+    [#"../../../../../creusot-contracts/src/logic/seq.rs" 49 8 49 39] SeqExt.subsequence self 1 (Seq.length self)
   val tail (self : Seq.seq t) : Seq.seq t
     ensures { result = tail self }
     
@@ -708,7 +708,7 @@ module Core_Slice_Impl0_TakeFirstMut_Interface
     type t = borrowed (borrowed (slice t))
   val take_first_mut (self : borrowed (borrowed (slice t))) : Core_Option_Option_Type.t_option (borrowed t)
     requires {Inv0.inv self}
-    ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 268 18 275 9] match (result) with
+    ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 273 18 280 9] match (result) with
       | Core_Option_Option_Type.C_Some r ->  * r = IndexLogic0.index_logic ( *  * self) 0 /\  ^ r = IndexLogic0.index_logic ( ^  * self) 0 /\ Seq.length (ShallowModel0.shallow_model ( *  * self)) > 0 /\ Seq.length (ShallowModel0.shallow_model ( ^  * self)) > 0 /\ ShallowModel0.shallow_model ( *  ^ self) = Tail0.tail (ShallowModel0.shallow_model ( *  * self)) /\ ShallowModel0.shallow_model ( ^  ^ self) = Tail0.tail (ShallowModel0.shallow_model ( ^  * self))
       | Core_Option_Option_Type.C_None ->  ^ self =  * self /\ Seq.length (ShallowModel0.shallow_model ( *  * self)) = 0
       end }
diff --git a/creusot/tests/should_succeed/iterators/03_std_iterators.mlcfg b/creusot/tests/should_succeed/iterators/03_std_iterators.mlcfg
index 108059842d..d57cbeb044 100644
--- a/creusot/tests/should_succeed/iterators/03_std_iterators.mlcfg
+++ b/creusot/tests/should_succeed/iterators/03_std_iterators.mlcfg
@@ -340,7 +340,7 @@ module CreusotContracts_Std1_Slice_Impl15_Produces
   predicate produces (self : Core_Slice_Iter_Iter_Type.t_iter t) (visited : Seq.seq t) (tl : Core_Slice_Iter_Iter_Type.t_iter t)
     
    =
-    [#"../../../../../creusot-contracts/src/std/slice.rs" 378 12 378 66] ToRefSeq0.to_ref_seq (ShallowModel0.shallow_model self) = Seq.(++) visited (ToRefSeq0.to_ref_seq (ShallowModel0.shallow_model tl))
+    [#"../../../../../creusot-contracts/src/std/slice.rs" 383 12 383 66] ToRefSeq0.to_ref_seq (ShallowModel0.shallow_model self) = Seq.(++) visited (ToRefSeq0.to_ref_seq (ShallowModel0.shallow_model tl))
   val produces (self : Core_Slice_Iter_Iter_Type.t_iter t) (visited : Seq.seq t) (tl : Core_Slice_Iter_Iter_Type.t_iter t) : bool
     ensures { result = produces self visited tl }
     
@@ -395,7 +395,7 @@ module Core_Slice_Impl0_Iter_Interface
     type t = slice t
   val iter (self : slice t) : Core_Slice_Iter_Iter_Type.t_iter t
     requires {Inv0.inv self}
-    ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 232 0 324 1] ShallowModel0.shallow_model result = self }
+    ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 232 0 329 1] ShallowModel0.shallow_model result = self }
     
 end
 module CreusotContracts_Std1_Iter_IntoIterator_IntoIterPre_Stub
@@ -527,7 +527,7 @@ module CreusotContracts_Std1_Slice_Impl15_Completed
   clone CreusotContracts_Resolve_Impl1_Resolve_Stub as Resolve0 with
     type t = Core_Slice_Iter_Iter_Type.t_iter t
   predicate completed (self : borrowed (Core_Slice_Iter_Iter_Type.t_iter t)) =
-    [#"../../../../../creusot-contracts/src/std/slice.rs" 371 20 371 61] Resolve0.resolve self /\ ShallowModel1.shallow_model (ShallowModel0.shallow_model self) = Seq.empty 
+    [#"../../../../../creusot-contracts/src/std/slice.rs" 376 20 376 61] Resolve0.resolve self /\ ShallowModel1.shallow_model (ShallowModel0.shallow_model self) = Seq.empty 
   val completed (self : borrowed (Core_Slice_Iter_Iter_Type.t_iter t)) : bool
     ensures { result = completed self }
     
@@ -612,10 +612,10 @@ module CreusotContracts_Std1_Slice_Impl15_ProducesRefl_Interface
     type t = t
   function produces_refl (a : Core_Slice_Iter_Iter_Type.t_iter t) : ()
   val produces_refl (a : Core_Slice_Iter_Iter_Type.t_iter t) : ()
-    ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 384 14 384 39] Produces0.produces a (Seq.empty ) a }
+    ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 389 14 389 39] Produces0.produces a (Seq.empty ) a }
     ensures { result = produces_refl a }
     
-  axiom produces_refl_spec : forall a : Core_Slice_Iter_Iter_Type.t_iter t . [#"../../../../../creusot-contracts/src/std/slice.rs" 384 14 384 39] Produces0.produces a (Seq.empty ) a
+  axiom produces_refl_spec : forall a : Core_Slice_Iter_Iter_Type.t_iter t . [#"../../../../../creusot-contracts/src/std/slice.rs" 389 14 389 39] Produces0.produces a (Seq.empty ) a
 end
 module CreusotContracts_Std1_Slice_Impl15_ProducesRefl
   type t
@@ -624,12 +624,12 @@ module CreusotContracts_Std1_Slice_Impl15_ProducesRefl
   clone CreusotContracts_Std1_Slice_Impl15_Produces_Stub as Produces0 with
     type t = t
   function produces_refl (a : Core_Slice_Iter_Iter_Type.t_iter t) : () =
-    [#"../../../../../creusot-contracts/src/std/slice.rs" 382 4 382 10] ()
+    [#"../../../../../creusot-contracts/src/std/slice.rs" 387 4 387 10] ()
   val produces_refl (a : Core_Slice_Iter_Iter_Type.t_iter t) : ()
-    ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 384 14 384 39] Produces0.produces a (Seq.empty ) a }
+    ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 389 14 389 39] Produces0.produces a (Seq.empty ) a }
     ensures { result = produces_refl a }
     
-  axiom produces_refl_spec : forall a : Core_Slice_Iter_Iter_Type.t_iter t . [#"../../../../../creusot-contracts/src/std/slice.rs" 384 14 384 39] Produces0.produces a (Seq.empty ) a
+  axiom produces_refl_spec : forall a : Core_Slice_Iter_Iter_Type.t_iter t . [#"../../../../../creusot-contracts/src/std/slice.rs" 389 14 389 39] Produces0.produces a (Seq.empty ) a
 end
 module CreusotContracts_Std1_Slice_Impl15_ProducesTrans_Stub
   type t
@@ -651,12 +651,12 @@ module CreusotContracts_Std1_Slice_Impl15_ProducesTrans_Interface
   function produces_trans (a : Core_Slice_Iter_Iter_Type.t_iter t) (ab : Seq.seq t) (b : Core_Slice_Iter_Iter_Type.t_iter t) (bc : Seq.seq t) (c : Core_Slice_Iter_Iter_Type.t_iter t) : ()
     
   val produces_trans (a : Core_Slice_Iter_Iter_Type.t_iter t) (ab : Seq.seq t) (b : Core_Slice_Iter_Iter_Type.t_iter t) (bc : Seq.seq t) (c : Core_Slice_Iter_Iter_Type.t_iter t) : ()
-    requires {[#"../../../../../creusot-contracts/src/std/slice.rs" 389 15 389 32] Produces0.produces a ab b}
-    requires {[#"../../../../../creusot-contracts/src/std/slice.rs" 390 15 390 32] Produces0.produces b bc c}
-    ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 391 14 391 42] Produces0.produces a (Seq.(++) ab bc) c }
+    requires {[#"../../../../../creusot-contracts/src/std/slice.rs" 394 15 394 32] Produces0.produces a ab b}
+    requires {[#"../../../../../creusot-contracts/src/std/slice.rs" 395 15 395 32] Produces0.produces b bc c}
+    ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 396 14 396 42] Produces0.produces a (Seq.(++) ab bc) c }
     ensures { result = produces_trans a ab b bc c }
     
-  axiom produces_trans_spec : forall a : Core_Slice_Iter_Iter_Type.t_iter t, ab : Seq.seq t, b : Core_Slice_Iter_Iter_Type.t_iter t, bc : Seq.seq t, c : Core_Slice_Iter_Iter_Type.t_iter t . ([#"../../../../../creusot-contracts/src/std/slice.rs" 389 15 389 32] Produces0.produces a ab b) -> ([#"../../../../../creusot-contracts/src/std/slice.rs" 390 15 390 32] Produces0.produces b bc c) -> ([#"../../../../../creusot-contracts/src/std/slice.rs" 391 14 391 42] Produces0.produces a (Seq.(++) ab bc) c)
+  axiom produces_trans_spec : forall a : Core_Slice_Iter_Iter_Type.t_iter t, ab : Seq.seq t, b : Core_Slice_Iter_Iter_Type.t_iter t, bc : Seq.seq t, c : Core_Slice_Iter_Iter_Type.t_iter t . ([#"../../../../../creusot-contracts/src/std/slice.rs" 394 15 394 32] Produces0.produces a ab b) -> ([#"../../../../../creusot-contracts/src/std/slice.rs" 395 15 395 32] Produces0.produces b bc c) -> ([#"../../../../../creusot-contracts/src/std/slice.rs" 396 14 396 42] Produces0.produces a (Seq.(++) ab bc) c)
 end
 module CreusotContracts_Std1_Slice_Impl15_ProducesTrans
   type t
@@ -668,14 +668,14 @@ module CreusotContracts_Std1_Slice_Impl15_ProducesTrans
   function produces_trans (a : Core_Slice_Iter_Iter_Type.t_iter t) (ab : Seq.seq t) (b : Core_Slice_Iter_Iter_Type.t_iter t) (bc : Seq.seq t) (c : Core_Slice_Iter_Iter_Type.t_iter t) : ()
     
    =
-    [#"../../../../../creusot-contracts/src/std/slice.rs" 387 4 387 10] ()
+    [#"../../../../../creusot-contracts/src/std/slice.rs" 392 4 392 10] ()
   val produces_trans (a : Core_Slice_Iter_Iter_Type.t_iter t) (ab : Seq.seq t) (b : Core_Slice_Iter_Iter_Type.t_iter t) (bc : Seq.seq t) (c : Core_Slice_Iter_Iter_Type.t_iter t) : ()
-    requires {[#"../../../../../creusot-contracts/src/std/slice.rs" 389 15 389 32] Produces0.produces a ab b}
-    requires {[#"../../../../../creusot-contracts/src/std/slice.rs" 390 15 390 32] Produces0.produces b bc c}
-    ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 391 14 391 42] Produces0.produces a (Seq.(++) ab bc) c }
+    requires {[#"../../../../../creusot-contracts/src/std/slice.rs" 394 15 394 32] Produces0.produces a ab b}
+    requires {[#"../../../../../creusot-contracts/src/std/slice.rs" 395 15 395 32] Produces0.produces b bc c}
+    ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 396 14 396 42] Produces0.produces a (Seq.(++) ab bc) c }
     ensures { result = produces_trans a ab b bc c }
     
-  axiom produces_trans_spec : forall a : Core_Slice_Iter_Iter_Type.t_iter t, ab : Seq.seq t, b : Core_Slice_Iter_Iter_Type.t_iter t, bc : Seq.seq t, c : Core_Slice_Iter_Iter_Type.t_iter t . ([#"../../../../../creusot-contracts/src/std/slice.rs" 389 15 389 32] Produces0.produces a ab b) -> ([#"../../../../../creusot-contracts/src/std/slice.rs" 390 15 390 32] Produces0.produces b bc c) -> ([#"../../../../../creusot-contracts/src/std/slice.rs" 391 14 391 42] Produces0.produces a (Seq.(++) ab bc) c)
+  axiom produces_trans_spec : forall a : Core_Slice_Iter_Iter_Type.t_iter t, ab : Seq.seq t, b : Core_Slice_Iter_Iter_Type.t_iter t, bc : Seq.seq t, c : Core_Slice_Iter_Iter_Type.t_iter t . ([#"../../../../../creusot-contracts/src/std/slice.rs" 394 15 394 32] Produces0.produces a ab b) -> ([#"../../../../../creusot-contracts/src/std/slice.rs" 395 15 395 32] Produces0.produces b bc c) -> ([#"../../../../../creusot-contracts/src/std/slice.rs" 396 14 396 42] Produces0.produces a (Seq.(++) ab bc) c)
 end
 module C03StdIterators_SliceIter_Interface
   type t
@@ -1428,10 +1428,10 @@ module CreusotContracts_Std1_Slice_Impl16_ShallowModel_Interface
     axiom .
   function shallow_model (self : Core_Slice_Iter_IterMut_Type.t_itermut t) : borrowed (slice t)
   val shallow_model (self : Core_Slice_Iter_IterMut_Type.t_itermut t) : borrowed (slice t)
-    ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 401 14 401 50] Seq.length (ShallowModel0.shallow_model ( ^ result)) = Seq.length (ShallowModel0.shallow_model ( * result)) }
+    ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 406 14 406 50] Seq.length (ShallowModel0.shallow_model ( ^ result)) = Seq.length (ShallowModel0.shallow_model ( * result)) }
     ensures { result = shallow_model self }
     
-  axiom shallow_model_spec : forall self : Core_Slice_Iter_IterMut_Type.t_itermut t . [#"../../../../../creusot-contracts/src/std/slice.rs" 401 14 401 50] Seq.length (ShallowModel0.shallow_model ( ^ shallow_model self)) = Seq.length (ShallowModel0.shallow_model ( * shallow_model self))
+  axiom shallow_model_spec : forall self : Core_Slice_Iter_IterMut_Type.t_itermut t . [#"../../../../../creusot-contracts/src/std/slice.rs" 406 14 406 50] Seq.length (ShallowModel0.shallow_model ( ^ shallow_model self)) = Seq.length (ShallowModel0.shallow_model ( * shallow_model self))
 end
 module CreusotContracts_Std1_Slice_Impl16_ShallowModel
   type t
@@ -1449,10 +1449,10 @@ module CreusotContracts_Std1_Slice_Impl16_ShallowModel
     axiom .
   function shallow_model (self : Core_Slice_Iter_IterMut_Type.t_itermut t) : borrowed (slice t)
   val shallow_model (self : Core_Slice_Iter_IterMut_Type.t_itermut t) : borrowed (slice t)
-    ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 401 14 401 50] Seq.length (ShallowModel0.shallow_model ( ^ result)) = Seq.length (ShallowModel0.shallow_model ( * result)) }
+    ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 406 14 406 50] Seq.length (ShallowModel0.shallow_model ( ^ result)) = Seq.length (ShallowModel0.shallow_model ( * result)) }
     ensures { result = shallow_model self }
     
-  axiom shallow_model_spec : forall self : Core_Slice_Iter_IterMut_Type.t_itermut t . [#"../../../../../creusot-contracts/src/std/slice.rs" 401 14 401 50] Seq.length (ShallowModel0.shallow_model ( ^ shallow_model self)) = Seq.length (ShallowModel0.shallow_model ( * shallow_model self))
+  axiom shallow_model_spec : forall self : Core_Slice_Iter_IterMut_Type.t_itermut t . [#"../../../../../creusot-contracts/src/std/slice.rs" 406 14 406 50] Seq.length (ShallowModel0.shallow_model ( ^ shallow_model self)) = Seq.length (ShallowModel0.shallow_model ( * shallow_model self))
 end
 module CreusotContracts_Std1_Slice_Impl4_ToMutSeq_Stub
   type t
@@ -1574,7 +1574,7 @@ module CreusotContracts_Std1_Slice_Impl18_Produces
   predicate produces (self : Core_Slice_Iter_IterMut_Type.t_itermut t) (visited : Seq.seq (borrowed t)) (tl : Core_Slice_Iter_IterMut_Type.t_itermut t)
     
    =
-    [#"../../../../../creusot-contracts/src/std/slice.rs" 437 12 437 66] ToMutSeq0.to_mut_seq (ShallowModel0.shallow_model self) = Seq.(++) visited (ToMutSeq0.to_mut_seq (ShallowModel0.shallow_model tl))
+    [#"../../../../../creusot-contracts/src/std/slice.rs" 442 12 442 66] ToMutSeq0.to_mut_seq (ShallowModel0.shallow_model self) = Seq.(++) visited (ToMutSeq0.to_mut_seq (ShallowModel0.shallow_model tl))
   val produces (self : Core_Slice_Iter_IterMut_Type.t_itermut t) (visited : Seq.seq (borrowed t)) (tl : Core_Slice_Iter_IterMut_Type.t_itermut t) : bool
     ensures { result = produces self visited tl }
     
@@ -1640,7 +1640,7 @@ module CreusotContracts_Std1_Slice_Impl19_Resolve
     val Max0.mAX' = Max0.mAX',
     axiom .
   predicate resolve (self : Core_Slice_Iter_IterMut_Type.t_itermut t) =
-    [#"../../../../../creusot-contracts/src/std/slice.rs" 413 20 413 36]  * ShallowModel0.shallow_model self =  ^ ShallowModel0.shallow_model self
+    [#"../../../../../creusot-contracts/src/std/slice.rs" 418 20 418 36]  * ShallowModel0.shallow_model self =  ^ ShallowModel0.shallow_model self
   val resolve (self : Core_Slice_Iter_IterMut_Type.t_itermut t) : bool
     ensures { result = resolve self }
     
@@ -1711,7 +1711,7 @@ module Core_Slice_Impl0_IterMut_Interface
     type t = borrowed (slice t)
   val iter_mut (self : borrowed (slice t)) : Core_Slice_Iter_IterMut_Type.t_itermut t
     requires {Inv0.inv self}
-    ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 232 0 324 1] ShallowModel0.shallow_model result = self }
+    ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 232 0 329 1] ShallowModel0.shallow_model result = self }
     ensures { Inv1.inv result }
     
 end
@@ -1749,7 +1749,7 @@ module CreusotContracts_Std1_Slice_Impl17_Invariant
     val Max0.mAX' = Max0.mAX',
     axiom .
   predicate invariant' (self : Core_Slice_Iter_IterMut_Type.t_itermut t) =
-    [#"../../../../../creusot-contracts/src/std/slice.rs" 422 20 422 54] Seq.length (ShallowModel1.shallow_model ( ^ ShallowModel0.shallow_model self)) = Seq.length (ShallowModel1.shallow_model ( * ShallowModel0.shallow_model self))
+    [#"../../../../../creusot-contracts/src/std/slice.rs" 427 20 427 54] Seq.length (ShallowModel1.shallow_model ( ^ ShallowModel0.shallow_model self)) = Seq.length (ShallowModel1.shallow_model ( * ShallowModel0.shallow_model self))
   val invariant' (self : Core_Slice_Iter_IterMut_Type.t_itermut t) : bool
     ensures { result = invariant' self }
     
@@ -1798,7 +1798,7 @@ module CreusotContracts_Std1_Slice_Impl18_Completed
   clone CreusotContracts_Resolve_Impl1_Resolve_Stub as Resolve0 with
     type t = Core_Slice_Iter_IterMut_Type.t_itermut t
   predicate completed (self : borrowed (Core_Slice_Iter_IterMut_Type.t_itermut t)) =
-    [#"../../../../../creusot-contracts/src/std/slice.rs" 430 20 430 61] Resolve0.resolve self /\ ShallowModel1.shallow_model ( * ShallowModel0.shallow_model self) = Seq.empty 
+    [#"../../../../../creusot-contracts/src/std/slice.rs" 435 20 435 61] Resolve0.resolve self /\ ShallowModel1.shallow_model ( * ShallowModel0.shallow_model self) = Seq.empty 
   val completed (self : borrowed (Core_Slice_Iter_IterMut_Type.t_itermut t)) : bool
     ensures { result = completed self }
     
@@ -1857,11 +1857,11 @@ module CreusotContracts_Std1_Slice_Impl18_ProducesRefl_Interface
     type t = Core_Slice_Iter_IterMut_Type.t_itermut t
   function produces_refl (a : Core_Slice_Iter_IterMut_Type.t_itermut t) : ()
   val produces_refl (a : Core_Slice_Iter_IterMut_Type.t_itermut t) : ()
-    requires {[#"../../../../../creusot-contracts/src/std/slice.rs" 444 21 444 22] Inv0.inv a}
-    ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 443 14 443 39] Produces0.produces a (Seq.empty ) a }
+    requires {[#"../../../../../creusot-contracts/src/std/slice.rs" 449 21 449 22] Inv0.inv a}
+    ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 448 14 448 39] Produces0.produces a (Seq.empty ) a }
     ensures { result = produces_refl a }
     
-  axiom produces_refl_spec : forall a : Core_Slice_Iter_IterMut_Type.t_itermut t . ([#"../../../../../creusot-contracts/src/std/slice.rs" 444 21 444 22] Inv0.inv a) -> ([#"../../../../../creusot-contracts/src/std/slice.rs" 443 14 443 39] Produces0.produces a (Seq.empty ) a)
+  axiom produces_refl_spec : forall a : Core_Slice_Iter_IterMut_Type.t_itermut t . ([#"../../../../../creusot-contracts/src/std/slice.rs" 449 21 449 22] Inv0.inv a) -> ([#"../../../../../creusot-contracts/src/std/slice.rs" 448 14 448 39] Produces0.produces a (Seq.empty ) a)
 end
 module CreusotContracts_Std1_Slice_Impl18_ProducesRefl
   type t
@@ -1872,13 +1872,13 @@ module CreusotContracts_Std1_Slice_Impl18_ProducesRefl
   clone CreusotContracts_Invariant_Inv_Stub as Inv0 with
     type t = Core_Slice_Iter_IterMut_Type.t_itermut t
   function produces_refl (a : Core_Slice_Iter_IterMut_Type.t_itermut t) : () =
-    [#"../../../../../creusot-contracts/src/std/slice.rs" 441 4 441 10] ()
+    [#"../../../../../creusot-contracts/src/std/slice.rs" 446 4 446 10] ()
   val produces_refl (a : Core_Slice_Iter_IterMut_Type.t_itermut t) : ()
-    requires {[#"../../../../../creusot-contracts/src/std/slice.rs" 444 21 444 22] Inv0.inv a}
-    ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 443 14 443 39] Produces0.produces a (Seq.empty ) a }
+    requires {[#"../../../../../creusot-contracts/src/std/slice.rs" 449 21 449 22] Inv0.inv a}
+    ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 448 14 448 39] Produces0.produces a (Seq.empty ) a }
     ensures { result = produces_refl a }
     
-  axiom produces_refl_spec : forall a : Core_Slice_Iter_IterMut_Type.t_itermut t . ([#"../../../../../creusot-contracts/src/std/slice.rs" 444 21 444 22] Inv0.inv a) -> ([#"../../../../../creusot-contracts/src/std/slice.rs" 443 14 443 39] Produces0.produces a (Seq.empty ) a)
+  axiom produces_refl_spec : forall a : Core_Slice_Iter_IterMut_Type.t_itermut t . ([#"../../../../../creusot-contracts/src/std/slice.rs" 449 21 449 22] Inv0.inv a) -> ([#"../../../../../creusot-contracts/src/std/slice.rs" 448 14 448 39] Produces0.produces a (Seq.empty ) a)
 end
 module CreusotContracts_Std1_Slice_Impl18_ProducesTrans_Stub
   type t
@@ -1904,15 +1904,15 @@ module CreusotContracts_Std1_Slice_Impl18_ProducesTrans_Interface
   function produces_trans (a : Core_Slice_Iter_IterMut_Type.t_itermut t) (ab : Seq.seq (borrowed t)) (b : Core_Slice_Iter_IterMut_Type.t_itermut t) (bc : Seq.seq (borrowed t)) (c : Core_Slice_Iter_IterMut_Type.t_itermut t) : ()
     
   val produces_trans (a : Core_Slice_Iter_IterMut_Type.t_itermut t) (ab : Seq.seq (borrowed t)) (b : Core_Slice_Iter_IterMut_Type.t_itermut t) (bc : Seq.seq (borrowed t)) (c : Core_Slice_Iter_IterMut_Type.t_itermut t) : ()
-    requires {[#"../../../../../creusot-contracts/src/std/slice.rs" 448 15 448 32] Produces0.produces a ab b}
-    requires {[#"../../../../../creusot-contracts/src/std/slice.rs" 449 15 449 32] Produces0.produces b bc c}
-    requires {[#"../../../../../creusot-contracts/src/std/slice.rs" 451 22 451 23] Inv0.inv a}
-    requires {[#"../../../../../creusot-contracts/src/std/slice.rs" 451 52 451 53] Inv0.inv b}
-    requires {[#"../../../../../creusot-contracts/src/std/slice.rs" 451 82 451 83] Inv0.inv c}
-    ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 450 14 450 42] Produces0.produces a (Seq.(++) ab bc) c }
+    requires {[#"../../../../../creusot-contracts/src/std/slice.rs" 453 15 453 32] Produces0.produces a ab b}
+    requires {[#"../../../../../creusot-contracts/src/std/slice.rs" 454 15 454 32] Produces0.produces b bc c}
+    requires {[#"../../../../../creusot-contracts/src/std/slice.rs" 456 22 456 23] Inv0.inv a}
+    requires {[#"../../../../../creusot-contracts/src/std/slice.rs" 456 52 456 53] Inv0.inv b}
+    requires {[#"../../../../../creusot-contracts/src/std/slice.rs" 456 82 456 83] Inv0.inv c}
+    ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 455 14 455 42] Produces0.produces a (Seq.(++) ab bc) c }
     ensures { result = produces_trans a ab b bc c }
     
-  axiom produces_trans_spec : forall a : Core_Slice_Iter_IterMut_Type.t_itermut t, ab : Seq.seq (borrowed t), b : Core_Slice_Iter_IterMut_Type.t_itermut t, bc : Seq.seq (borrowed t), c : Core_Slice_Iter_IterMut_Type.t_itermut t . ([#"../../../../../creusot-contracts/src/std/slice.rs" 448 15 448 32] Produces0.produces a ab b) -> ([#"../../../../../creusot-contracts/src/std/slice.rs" 449 15 449 32] Produces0.produces b bc c) -> ([#"../../../../../creusot-contracts/src/std/slice.rs" 451 22 451 23] Inv0.inv a) -> ([#"../../../../../creusot-contracts/src/std/slice.rs" 451 52 451 53] Inv0.inv b) -> ([#"../../../../../creusot-contracts/src/std/slice.rs" 451 82 451 83] Inv0.inv c) -> ([#"../../../../../creusot-contracts/src/std/slice.rs" 450 14 450 42] Produces0.produces a (Seq.(++) ab bc) c)
+  axiom produces_trans_spec : forall a : Core_Slice_Iter_IterMut_Type.t_itermut t, ab : Seq.seq (borrowed t), b : Core_Slice_Iter_IterMut_Type.t_itermut t, bc : Seq.seq (borrowed t), c : Core_Slice_Iter_IterMut_Type.t_itermut t . ([#"../../../../../creusot-contracts/src/std/slice.rs" 453 15 453 32] Produces0.produces a ab b) -> ([#"../../../../../creusot-contracts/src/std/slice.rs" 454 15 454 32] Produces0.produces b bc c) -> ([#"../../../../../creusot-contracts/src/std/slice.rs" 456 22 456 23] Inv0.inv a) -> ([#"../../../../../creusot-contracts/src/std/slice.rs" 456 52 456 53] Inv0.inv b) -> ([#"../../../../../creusot-contracts/src/std/slice.rs" 456 82 456 83] Inv0.inv c) -> ([#"../../../../../creusot-contracts/src/std/slice.rs" 455 14 455 42] Produces0.produces a (Seq.(++) ab bc) c)
 end
 module CreusotContracts_Std1_Slice_Impl18_ProducesTrans
   type t
@@ -1926,17 +1926,17 @@ module CreusotContracts_Std1_Slice_Impl18_ProducesTrans
   function produces_trans (a : Core_Slice_Iter_IterMut_Type.t_itermut t) (ab : Seq.seq (borrowed t)) (b : Core_Slice_Iter_IterMut_Type.t_itermut t) (bc : Seq.seq (borrowed t)) (c : Core_Slice_Iter_IterMut_Type.t_itermut t) : ()
     
    =
-    [#"../../../../../creusot-contracts/src/std/slice.rs" 446 4 446 10] ()
+    [#"../../../../../creusot-contracts/src/std/slice.rs" 451 4 451 10] ()
   val produces_trans (a : Core_Slice_Iter_IterMut_Type.t_itermut t) (ab : Seq.seq (borrowed t)) (b : Core_Slice_Iter_IterMut_Type.t_itermut t) (bc : Seq.seq (borrowed t)) (c : Core_Slice_Iter_IterMut_Type.t_itermut t) : ()
-    requires {[#"../../../../../creusot-contracts/src/std/slice.rs" 448 15 448 32] Produces0.produces a ab b}
-    requires {[#"../../../../../creusot-contracts/src/std/slice.rs" 449 15 449 32] Produces0.produces b bc c}
-    requires {[#"../../../../../creusot-contracts/src/std/slice.rs" 451 22 451 23] Inv0.inv a}
-    requires {[#"../../../../../creusot-contracts/src/std/slice.rs" 451 52 451 53] Inv0.inv b}
-    requires {[#"../../../../../creusot-contracts/src/std/slice.rs" 451 82 451 83] Inv0.inv c}
-    ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 450 14 450 42] Produces0.produces a (Seq.(++) ab bc) c }
+    requires {[#"../../../../../creusot-contracts/src/std/slice.rs" 453 15 453 32] Produces0.produces a ab b}
+    requires {[#"../../../../../creusot-contracts/src/std/slice.rs" 454 15 454 32] Produces0.produces b bc c}
+    requires {[#"../../../../../creusot-contracts/src/std/slice.rs" 456 22 456 23] Inv0.inv a}
+    requires {[#"../../../../../creusot-contracts/src/std/slice.rs" 456 52 456 53] Inv0.inv b}
+    requires {[#"../../../../../creusot-contracts/src/std/slice.rs" 456 82 456 83] Inv0.inv c}
+    ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 455 14 455 42] Produces0.produces a (Seq.(++) ab bc) c }
     ensures { result = produces_trans a ab b bc c }
     
-  axiom produces_trans_spec : forall a : Core_Slice_Iter_IterMut_Type.t_itermut t, ab : Seq.seq (borrowed t), b : Core_Slice_Iter_IterMut_Type.t_itermut t, bc : Seq.seq (borrowed t), c : Core_Slice_Iter_IterMut_Type.t_itermut t . ([#"../../../../../creusot-contracts/src/std/slice.rs" 448 15 448 32] Produces0.produces a ab b) -> ([#"../../../../../creusot-contracts/src/std/slice.rs" 449 15 449 32] Produces0.produces b bc c) -> ([#"../../../../../creusot-contracts/src/std/slice.rs" 451 22 451 23] Inv0.inv a) -> ([#"../../../../../creusot-contracts/src/std/slice.rs" 451 52 451 53] Inv0.inv b) -> ([#"../../../../../creusot-contracts/src/std/slice.rs" 451 82 451 83] Inv0.inv c) -> ([#"../../../../../creusot-contracts/src/std/slice.rs" 450 14 450 42] Produces0.produces a (Seq.(++) ab bc) c)
+  axiom produces_trans_spec : forall a : Core_Slice_Iter_IterMut_Type.t_itermut t, ab : Seq.seq (borrowed t), b : Core_Slice_Iter_IterMut_Type.t_itermut t, bc : Seq.seq (borrowed t), c : Core_Slice_Iter_IterMut_Type.t_itermut t . ([#"../../../../../creusot-contracts/src/std/slice.rs" 453 15 453 32] Produces0.produces a ab b) -> ([#"../../../../../creusot-contracts/src/std/slice.rs" 454 15 454 32] Produces0.produces b bc c) -> ([#"../../../../../creusot-contracts/src/std/slice.rs" 456 22 456 23] Inv0.inv a) -> ([#"../../../../../creusot-contracts/src/std/slice.rs" 456 52 456 53] Inv0.inv b) -> ([#"../../../../../creusot-contracts/src/std/slice.rs" 456 82 456 83] Inv0.inv c) -> ([#"../../../../../creusot-contracts/src/std/slice.rs" 455 14 455 42] Produces0.produces a (Seq.(++) ab bc) c)
 end
 module C03StdIterators_AllZero_Interface
   use prelude.Borrow
@@ -5868,7 +5868,7 @@ module Core_Slice_Impl0_Len_Interface
     type t = slice t
   val len (self : slice t) : usize
     requires {Inv0.inv self}
-    ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 232 0 324 1] Seq.length (ShallowModel0.shallow_model self) = UIntSize.to_int result }
+    ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 232 0 329 1] Seq.length (ShallowModel0.shallow_model self) = UIntSize.to_int result }
     
 end
 module Core_Iter_Traits_Iterator_Iterator_Zip_Interface
@@ -5957,10 +5957,10 @@ module Core_Slice_Impl0_Swap_Interface
     type t = slice t,
     type ShallowModelTy0.shallowModelTy = Seq.seq t
   val swap (self : borrowed (slice t)) (a : usize) (b : usize) : ()
-    requires {[#"../../../../../creusot-contracts/src/std/slice.rs" 237 19 237 35] UIntSize.to_int a < Seq.length (ShallowModel0.shallow_model self)}
-    requires {[#"../../../../../creusot-contracts/src/std/slice.rs" 238 19 238 35] UIntSize.to_int b < Seq.length (ShallowModel0.shallow_model self)}
+    requires {[#"../../../../../creusot-contracts/src/std/slice.rs" 242 19 242 35] UIntSize.to_int a < Seq.length (ShallowModel0.shallow_model self)}
+    requires {[#"../../../../../creusot-contracts/src/std/slice.rs" 243 19 243 35] UIntSize.to_int b < Seq.length (ShallowModel0.shallow_model self)}
     requires {Inv0.inv self}
-    ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 239 8 239 52] Permut.exchange (ShallowModel1.shallow_model ( ^ self)) (ShallowModel0.shallow_model self) (UIntSize.to_int a) (UIntSize.to_int b) }
+    ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 244 8 244 52] Permut.exchange (ShallowModel1.shallow_model ( ^ self)) (ShallowModel0.shallow_model self) (UIntSize.to_int a) (UIntSize.to_int b) }
     
 end
 module CreusotContracts_Std1_Iter_Zip_Impl1_ProducesRefl_Stub
diff --git a/creusot/tests/should_succeed/selection_sort_generic.mlcfg b/creusot/tests/should_succeed/selection_sort_generic.mlcfg
index 7d57770ee1..3a4fe868c7 100644
--- a/creusot/tests/should_succeed/selection_sort_generic.mlcfg
+++ b/creusot/tests/should_succeed/selection_sort_generic.mlcfg
@@ -471,7 +471,7 @@ module CreusotContracts_Logic_Seq_Impl0_PermutationOf
   use seq.Seq
   use seq.Permut
   predicate permutation_of (self : Seq.seq t) (o : Seq.seq t) =
-    [#"../../../../creusot-contracts/src/logic/seq.rs" 101 8 101 37] Permut.permut self o 0 (Seq.length self)
+    [#"../../../../creusot-contracts/src/logic/seq.rs" 103 8 103 37] Permut.permut self o 0 (Seq.length self)
   val permutation_of (self : Seq.seq t) (o : Seq.seq t) : bool
     ensures { result = permutation_of self o }
     
@@ -1132,10 +1132,10 @@ module Core_Slice_Impl0_Swap_Interface
     type t = slice t,
     type ShallowModelTy0.shallowModelTy = Seq.seq t
   val swap (self : borrowed (slice t)) (a : usize) (b : usize) : ()
-    requires {[#"../../../../creusot-contracts/src/std/slice.rs" 237 19 237 35] UIntSize.to_int a < Seq.length (ShallowModel0.shallow_model self)}
-    requires {[#"../../../../creusot-contracts/src/std/slice.rs" 238 19 238 35] UIntSize.to_int b < Seq.length (ShallowModel0.shallow_model self)}
+    requires {[#"../../../../creusot-contracts/src/std/slice.rs" 242 19 242 35] UIntSize.to_int a < Seq.length (ShallowModel0.shallow_model self)}
+    requires {[#"../../../../creusot-contracts/src/std/slice.rs" 243 19 243 35] UIntSize.to_int b < Seq.length (ShallowModel0.shallow_model self)}
     requires {Inv0.inv self}
-    ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 239 8 239 52] Permut.exchange (ShallowModel1.shallow_model ( ^ self)) (ShallowModel0.shallow_model self) (UIntSize.to_int a) (UIntSize.to_int b) }
+    ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 244 8 244 52] Permut.exchange (ShallowModel1.shallow_model ( ^ self)) (ShallowModel0.shallow_model self) (UIntSize.to_int a) (UIntSize.to_int b) }
     
 end
 module CreusotContracts_Std1_Iter_Impl0_IntoIterPre_Stub
diff --git a/creusot/tests/should_succeed/slices/01.mlcfg b/creusot/tests/should_succeed/slices/01.mlcfg
index f83d1594a7..332334a025 100644
--- a/creusot/tests/should_succeed/slices/01.mlcfg
+++ b/creusot/tests/should_succeed/slices/01.mlcfg
@@ -402,7 +402,7 @@ module Core_Slice_Impl0_Len_Interface
     type t = slice t
   val len (self : slice t) : usize
     requires {Inv0.inv self}
-    ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 232 0 324 1] Seq.length (ShallowModel0.shallow_model self) = UIntSize.to_int result }
+    ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 232 0 329 1] Seq.length (ShallowModel0.shallow_model self) = UIntSize.to_int result }
     
 end
 module C01_SliceFirst_Interface
diff --git a/creusot/tests/should_succeed/slices/02_std.mlcfg b/creusot/tests/should_succeed/slices/02_std.mlcfg
index 09d4a43e14..b1f13ee0cf 100644
--- a/creusot/tests/should_succeed/slices/02_std.mlcfg
+++ b/creusot/tests/should_succeed/slices/02_std.mlcfg
@@ -306,7 +306,7 @@ module CreusotContracts_Logic_Seq_Impl0_SortedRange
   clone CreusotContracts_Logic_Ord_OrdLogic_LeLog_Stub as LeLog0 with
     type self = t
   predicate sorted_range (self : Seq.seq t) (l : int) (u : int) =
-    [#"../../../../../creusot-contracts/src/logic/seq.rs" 132 8 134 9] forall j : int . forall i : int . l <= i /\ i <= j /\ j < u -> LeLog0.le_log (Seq.get self i) (Seq.get self j)
+    [#"../../../../../creusot-contracts/src/logic/seq.rs" 134 8 136 9] forall j : int . forall i : int . l <= i /\ i <= j /\ j < u -> LeLog0.le_log (Seq.get self i) (Seq.get self j)
   val sorted_range (self : Seq.seq t) (l : int) (u : int) : bool
     ensures { result = sorted_range self l u }
     
@@ -330,7 +330,7 @@ module CreusotContracts_Logic_Seq_Impl0_Sorted
   clone CreusotContracts_Logic_Seq_Impl0_SortedRange_Stub as SortedRange0 with
     type t = t
   predicate sorted (self : Seq.seq t) =
-    [#"../../../../../creusot-contracts/src/logic/seq.rs" 143 8 143 40] SortedRange0.sorted_range self 0 (Seq.length self)
+    [#"../../../../../creusot-contracts/src/logic/seq.rs" 145 8 145 40] SortedRange0.sorted_range self 0 (Seq.length self)
   val sorted (self : Seq.seq t) : bool
     ensures { result = sorted self }
     
@@ -488,13 +488,13 @@ module Core_Slice_Impl0_BinarySearch_Interface
     type t = slice t,
     type DeepModelTy0.deepModelTy = Seq.seq DeepModelTy0.deepModelTy
   val binary_search (self : slice t) (x : t) : Core_Result_Result_Type.t_result usize usize
-    requires {[#"../../../../../creusot-contracts/src/std/slice.rs" 232 0 324 1] Sorted0.sorted (DeepModel0.deep_model self)}
+    requires {[#"../../../../../creusot-contracts/src/std/slice.rs" 232 0 329 1] Sorted0.sorted (DeepModel0.deep_model self)}
     requires {Inv0.inv self}
     requires {Inv1.inv x}
-    ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 294 8 294 118] forall i : usize . result = Core_Result_Result_Type.C_Ok i -> UIntSize.to_int i < Seq.length (ShallowModel0.shallow_model self) /\ Seq.get (DeepModel1.deep_model self) (UIntSize.to_int i) = DeepModel2.deep_model x }
-    ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 295 8 296 96] forall i : usize . result = Core_Result_Result_Type.C_Err i -> UIntSize.to_int i <= Seq.length (ShallowModel0.shallow_model self) /\ (forall j : int . 0 <= j /\ j < Seq.length (ShallowModel0.shallow_model self) -> Seq.get (DeepModel0.deep_model self) j <> DeepModel2.deep_model x) }
-    ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 297 8 298 78] forall i : usize . result = Core_Result_Result_Type.C_Err i -> (forall j : usize . j < i -> LtLog0.lt_log (Seq.get (DeepModel0.deep_model self) (UIntSize.to_int j)) (DeepModel2.deep_model x)) }
-    ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 299 8 300 99] forall i : usize . result = Core_Result_Result_Type.C_Err i -> (forall j : usize . i <= j /\ UIntSize.to_int j < Seq.length (ShallowModel0.shallow_model self) -> LtLog0.lt_log (DeepModel2.deep_model x) (Seq.get (DeepModel0.deep_model self) (UIntSize.to_int j))) }
+    ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 299 8 299 118] forall i : usize . result = Core_Result_Result_Type.C_Ok i -> UIntSize.to_int i < Seq.length (ShallowModel0.shallow_model self) /\ Seq.get (DeepModel1.deep_model self) (UIntSize.to_int i) = DeepModel2.deep_model x }
+    ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 300 8 301 96] forall i : usize . result = Core_Result_Result_Type.C_Err i -> UIntSize.to_int i <= Seq.length (ShallowModel0.shallow_model self) /\ (forall j : int . 0 <= j /\ j < Seq.length (ShallowModel0.shallow_model self) -> Seq.get (DeepModel0.deep_model self) j <> DeepModel2.deep_model x) }
+    ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 302 8 303 78] forall i : usize . result = Core_Result_Result_Type.C_Err i -> (forall j : usize . j < i -> LtLog0.lt_log (Seq.get (DeepModel0.deep_model self) (UIntSize.to_int j)) (DeepModel2.deep_model x)) }
+    ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 304 8 305 99] forall i : usize . result = Core_Result_Result_Type.C_Err i -> (forall j : usize . i <= j /\ UIntSize.to_int j < Seq.length (ShallowModel0.shallow_model self) -> LtLog0.lt_log (DeepModel2.deep_model x) (Seq.get (DeepModel0.deep_model self) (UIntSize.to_int j))) }
     
 end
 module Core_Result_Impl0_Unwrap_Interface
diff --git a/creusot/tests/should_succeed/syntax/13_vec_macro.mlcfg b/creusot/tests/should_succeed/syntax/13_vec_macro.mlcfg
index 7304bcb512..ad5cea1f3b 100644
--- a/creusot/tests/should_succeed/syntax/13_vec_macro.mlcfg
+++ b/creusot/tests/should_succeed/syntax/13_vec_macro.mlcfg
@@ -341,7 +341,7 @@ module Alloc_Slice_Impl0_IntoVec_Interface
     type t = slice t
   val into_vec (self : slice t) : Alloc_Vec_Vec_Type.t_vec t a
     requires {Inv0.inv self}
-    ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 304 18 304 35] ShallowModel0.shallow_model result = ShallowModel1.shallow_model self }
+    ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 309 18 309 35] ShallowModel0.shallow_model result = ShallowModel1.shallow_model self }
     ensures { Inv1.inv result }
     
 end
diff --git a/creusot/tests/should_succeed/take_first_mut.mlcfg b/creusot/tests/should_succeed/take_first_mut.mlcfg
index 59caf69953..822ab69a49 100644
--- a/creusot/tests/should_succeed/take_first_mut.mlcfg
+++ b/creusot/tests/should_succeed/take_first_mut.mlcfg
@@ -139,7 +139,7 @@ module CreusotContracts_Logic_Seq_Impl0_Tail
   use seq.Seq
   use seq_ext.SeqExt
   function tail (self : Seq.seq t) : Seq.seq t =
-    [#"../../../../creusot-contracts/src/logic/seq.rs" 47 8 47 39] SeqExt.subsequence self 1 (Seq.length self)
+    [#"../../../../creusot-contracts/src/logic/seq.rs" 49 8 49 39] SeqExt.subsequence self 1 (Seq.length self)
   val tail (self : Seq.seq t) : Seq.seq t
     ensures { result = tail self }
     
@@ -312,7 +312,7 @@ module Core_Slice_Impl0_SplitFirstMut_Interface
     type t = borrowed (slice t)
   val split_first_mut (self : borrowed (slice t)) : Core_Option_Option_Type.t_option (borrowed t, borrowed (slice t))
     requires {Inv0.inv self}
-    ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 257 18 265 9] match (result) with
+    ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 262 18 270 9] match (result) with
       | Core_Option_Option_Type.C_Some (first, tail) ->  * first = IndexLogic0.index_logic ( * self) 0 /\  ^ first = IndexLogic0.index_logic ( ^ self) 0 /\ Seq.length (ShallowModel0.shallow_model ( * self)) > 0 /\ Seq.length (ShallowModel0.shallow_model ( ^ self)) > 0 /\ ShallowModel0.shallow_model ( * tail) = Tail0.tail (ShallowModel0.shallow_model ( * self)) /\ ShallowModel0.shallow_model ( ^ tail) = Tail0.tail (ShallowModel0.shallow_model ( ^ self))
       | Core_Option_Option_Type.C_None -> Seq.length (ShallowModel1.shallow_model self) = 0 /\  ^ self =  * self /\ ShallowModel1.shallow_model self = Seq.empty 
       end }
diff --git a/creusot/tests/should_succeed/vecdeque.mlcfg b/creusot/tests/should_succeed/vecdeque.mlcfg
index 75d19f1332..9028a17264 100644
--- a/creusot/tests/should_succeed/vecdeque.mlcfg
+++ b/creusot/tests/should_succeed/vecdeque.mlcfg
@@ -98,11 +98,11 @@ module CreusotContracts_Std1_Deque_Impl0_ShallowModel_Interface
     type t = Alloc_Collections_VecDeque_VecDeque_Type.t_vecdeque t a
   function shallow_model (self : Alloc_Collections_VecDeque_VecDeque_Type.t_vecdeque t a) : Seq.seq t
   val shallow_model (self : Alloc_Collections_VecDeque_VecDeque_Type.t_vecdeque t a) : Seq.seq t
-    requires {[#"../../../../creusot-contracts/src/std/deque.rs" 11 21 11 25] Inv0.inv self}
-    ensures { [#"../../../../creusot-contracts/src/std/deque.rs" 10 14 10 41] Seq.length result <= UIntSize.to_int Max0.mAX' }
+    requires {[#"../../../../creusot-contracts/src/std/deque.rs" 12 21 12 25] Inv0.inv self}
+    ensures { [#"../../../../creusot-contracts/src/std/deque.rs" 11 14 11 41] Seq.length result <= UIntSize.to_int Max0.mAX' }
     ensures { result = shallow_model self }
     
-  axiom shallow_model_spec : forall self : Alloc_Collections_VecDeque_VecDeque_Type.t_vecdeque t a . ([#"../../../../creusot-contracts/src/std/deque.rs" 11 21 11 25] Inv0.inv self) -> ([#"../../../../creusot-contracts/src/std/deque.rs" 10 14 10 41] Seq.length (shallow_model self) <= UIntSize.to_int Max0.mAX')
+  axiom shallow_model_spec : forall self : Alloc_Collections_VecDeque_VecDeque_Type.t_vecdeque t a . ([#"../../../../creusot-contracts/src/std/deque.rs" 12 21 12 25] Inv0.inv self) -> ([#"../../../../creusot-contracts/src/std/deque.rs" 11 14 11 41] Seq.length (shallow_model self) <= UIntSize.to_int Max0.mAX')
 end
 module CreusotContracts_Std1_Deque_Impl0_ShallowModel
   type t
@@ -116,11 +116,11 @@ module CreusotContracts_Std1_Deque_Impl0_ShallowModel
     type t = Alloc_Collections_VecDeque_VecDeque_Type.t_vecdeque t a
   function shallow_model (self : Alloc_Collections_VecDeque_VecDeque_Type.t_vecdeque t a) : Seq.seq t
   val shallow_model (self : Alloc_Collections_VecDeque_VecDeque_Type.t_vecdeque t a) : Seq.seq t
-    requires {[#"../../../../creusot-contracts/src/std/deque.rs" 11 21 11 25] Inv0.inv self}
-    ensures { [#"../../../../creusot-contracts/src/std/deque.rs" 10 14 10 41] Seq.length result <= UIntSize.to_int Max0.mAX' }
+    requires {[#"../../../../creusot-contracts/src/std/deque.rs" 12 21 12 25] Inv0.inv self}
+    ensures { [#"../../../../creusot-contracts/src/std/deque.rs" 11 14 11 41] Seq.length result <= UIntSize.to_int Max0.mAX' }
     ensures { result = shallow_model self }
     
-  axiom shallow_model_spec : forall self : Alloc_Collections_VecDeque_VecDeque_Type.t_vecdeque t a . ([#"../../../../creusot-contracts/src/std/deque.rs" 11 21 11 25] Inv0.inv self) -> ([#"../../../../creusot-contracts/src/std/deque.rs" 10 14 10 41] Seq.length (shallow_model self) <= UIntSize.to_int Max0.mAX')
+  axiom shallow_model_spec : forall self : Alloc_Collections_VecDeque_VecDeque_Type.t_vecdeque t a . ([#"../../../../creusot-contracts/src/std/deque.rs" 12 21 12 25] Inv0.inv self) -> ([#"../../../../creusot-contracts/src/std/deque.rs" 11 14 11 41] Seq.length (shallow_model self) <= UIntSize.to_int Max0.mAX')
 end
 module Alloc_Collections_VecDeque_Impl4_WithCapacity_Interface
   type t
@@ -139,7 +139,7 @@ module Alloc_Collections_VecDeque_Impl4_WithCapacity_Interface
     val Max0.mAX' = Max0.mAX',
     axiom .
   val with_capacity (capacity : usize) : Alloc_Collections_VecDeque_VecDeque_Type.t_vecdeque t (Alloc_Alloc_Global_Type.t_global)
-    ensures { [#"../../../../creusot-contracts/src/std/deque.rs" 59 26 59 44] Seq.length (ShallowModel0.shallow_model result) = 0 }
+    ensures { [#"../../../../creusot-contracts/src/std/deque.rs" 185 26 185 44] Seq.length (ShallowModel0.shallow_model result) = 0 }
     
 end
 module CreusotContracts_Model_ShallowModel_ShallowModelTy_Type
@@ -215,7 +215,7 @@ module Alloc_Collections_VecDeque_Impl5_IsEmpty_Interface
     type t = Alloc_Collections_VecDeque_VecDeque_Type.t_vecdeque t a
   val is_empty (self : Alloc_Collections_VecDeque_VecDeque_Type.t_vecdeque t a) : bool
     requires {Inv0.inv self}
-    ensures { [#"../../../../creusot-contracts/src/std/deque.rs" 67 26 67 54] result = (Seq.length (ShallowModel0.shallow_model self) = 0) }
+    ensures { [#"../../../../creusot-contracts/src/std/deque.rs" 193 26 193 54] result = (Seq.length (ShallowModel0.shallow_model self) = 0) }
     
 end
 module Alloc_Collections_VecDeque_Impl5_Len_Interface
@@ -234,7 +234,7 @@ module Alloc_Collections_VecDeque_Impl5_Len_Interface
     type t = Alloc_Collections_VecDeque_VecDeque_Type.t_vecdeque t a
   val len (self : Alloc_Collections_VecDeque_VecDeque_Type.t_vecdeque t a) : usize
     requires {Inv0.inv self}
-    ensures { [#"../../../../creusot-contracts/src/std/deque.rs" 64 26 64 48] UIntSize.to_int result = Seq.length (ShallowModel0.shallow_model self) }
+    ensures { [#"../../../../creusot-contracts/src/std/deque.rs" 190 26 190 48] UIntSize.to_int result = Seq.length (ShallowModel0.shallow_model self) }
     
 end
 module Alloc_Collections_VecDeque_Impl4_New_Interface
@@ -252,7 +252,7 @@ module Alloc_Collections_VecDeque_Impl4_New_Interface
     val Max0.mAX' = Max0.mAX',
     axiom .
   val new (_1 : ()) : Alloc_Collections_VecDeque_VecDeque_Type.t_vecdeque t (Alloc_Alloc_Global_Type.t_global)
-    ensures { [#"../../../../creusot-contracts/src/std/deque.rs" 56 26 56 44] Seq.length (ShallowModel0.shallow_model result) = 0 }
+    ensures { [#"../../../../creusot-contracts/src/std/deque.rs" 182 26 182 44] Seq.length (ShallowModel0.shallow_model result) = 0 }
     
 end
 module CreusotContracts_Model_Impl7_ShallowModel_Stub
@@ -313,7 +313,7 @@ module Alloc_Collections_VecDeque_Impl5_PopFront_Interface
     type t = borrowed (Alloc_Collections_VecDeque_VecDeque_Type.t_vecdeque t a)
   val pop_front (self : borrowed (Alloc_Collections_VecDeque_VecDeque_Type.t_vecdeque t a)) : Core_Option_Option_Type.t_option t
     requires {Inv0.inv self}
-    ensures { [#"../../../../creusot-contracts/src/std/deque.rs" 73 26 78 17] match (result) with
+    ensures { [#"../../../../creusot-contracts/src/std/deque.rs" 199 26 204 17] match (result) with
       | Core_Option_Option_Type.C_Some t -> ShallowModel0.shallow_model ( ^ self) = SeqExt.subsequence (ShallowModel1.shallow_model self) 1 (Seq.length (ShallowModel1.shallow_model self)) /\ ShallowModel1.shallow_model self = Seq.(++) (Seq.singleton t) (ShallowModel0.shallow_model ( ^ self))
       | Core_Option_Option_Type.C_None ->  * self =  ^ self /\ Seq.length (ShallowModel1.shallow_model self) = 0
       end }
@@ -424,7 +424,7 @@ module Alloc_Collections_VecDeque_Impl5_PopBack_Interface
     type t = borrowed (Alloc_Collections_VecDeque_VecDeque_Type.t_vecdeque t a)
   val pop_back (self : borrowed (Alloc_Collections_VecDeque_VecDeque_Type.t_vecdeque t a)) : Core_Option_Option_Type.t_option t
     requires {Inv0.inv self}
-    ensures { [#"../../../../creusot-contracts/src/std/deque.rs" 81 26 86 17] match (result) with
+    ensures { [#"../../../../creusot-contracts/src/std/deque.rs" 207 26 212 17] match (result) with
       | Core_Option_Option_Type.C_Some t -> ShallowModel0.shallow_model ( ^ self) = SeqExt.subsequence (ShallowModel1.shallow_model self) 0 (Seq.length (ShallowModel1.shallow_model self) - 1) /\ ShallowModel1.shallow_model self = Seq.snoc (ShallowModel0.shallow_model ( ^ self)) t
       | Core_Option_Option_Type.C_None ->  * self =  ^ self /\ Seq.length (ShallowModel1.shallow_model self) = 0
       end }
@@ -458,8 +458,8 @@ module Alloc_Collections_VecDeque_Impl5_PushFront_Interface
   val push_front (self : borrowed (Alloc_Collections_VecDeque_VecDeque_Type.t_vecdeque t a)) (value : t) : ()
     requires {Inv0.inv self}
     requires {Inv1.inv value}
-    ensures { [#"../../../../creusot-contracts/src/std/deque.rs" 89 26 89 59] Seq.length (ShallowModel0.shallow_model ( ^ self)) = Seq.length (ShallowModel1.shallow_model self) + 1 }
-    ensures { [#"../../../../creusot-contracts/src/std/deque.rs" 90 26 90 73] ShallowModel0.shallow_model ( ^ self) = Seq.(++) (Seq.singleton value) (ShallowModel1.shallow_model self) }
+    ensures { [#"../../../../creusot-contracts/src/std/deque.rs" 215 26 215 59] Seq.length (ShallowModel0.shallow_model ( ^ self)) = Seq.length (ShallowModel1.shallow_model self) + 1 }
+    ensures { [#"../../../../creusot-contracts/src/std/deque.rs" 216 26 216 73] ShallowModel0.shallow_model ( ^ self) = Seq.(++) (Seq.singleton value) (ShallowModel1.shallow_model self) }
     
 end
 module Alloc_Collections_VecDeque_Impl5_PushBack_Interface
@@ -488,7 +488,7 @@ module Alloc_Collections_VecDeque_Impl5_PushBack_Interface
   val push_back (self : borrowed (Alloc_Collections_VecDeque_VecDeque_Type.t_vecdeque t a)) (value : t) : ()
     requires {Inv0.inv self}
     requires {Inv1.inv value}
-    ensures { [#"../../../../creusot-contracts/src/std/deque.rs" 93 26 93 55] ShallowModel0.shallow_model ( ^ self) = Seq.snoc (ShallowModel1.shallow_model self) value }
+    ensures { [#"../../../../creusot-contracts/src/std/deque.rs" 219 26 219 55] ShallowModel0.shallow_model ( ^ self) = Seq.snoc (ShallowModel1.shallow_model self) value }
     
 end
 module Alloc_Collections_VecDeque_Impl5_Clear_Interface
@@ -510,7 +510,7 @@ module Alloc_Collections_VecDeque_Impl5_Clear_Interface
     type t = borrowed (Alloc_Collections_VecDeque_VecDeque_Type.t_vecdeque t a)
   val clear (self : borrowed (Alloc_Collections_VecDeque_VecDeque_Type.t_vecdeque t a)) : ()
     requires {Inv0.inv self}
-    ensures { [#"../../../../creusot-contracts/src/std/deque.rs" 70 26 70 45] Seq.length (ShallowModel0.shallow_model ( ^ self)) = 0 }
+    ensures { [#"../../../../creusot-contracts/src/std/deque.rs" 196 26 196 45] Seq.length (ShallowModel0.shallow_model ( ^ self)) = 0 }
     
 end
 module TyInv_Trivial
diff --git a/creusot/tests/should_succeed/vector/02_gnome.mlcfg b/creusot/tests/should_succeed/vector/02_gnome.mlcfg
index 82fa15c43e..50fe3acab3 100644
--- a/creusot/tests/should_succeed/vector/02_gnome.mlcfg
+++ b/creusot/tests/should_succeed/vector/02_gnome.mlcfg
@@ -444,7 +444,7 @@ module CreusotContracts_Logic_Seq_Impl0_PermutationOf
   use seq.Seq
   use seq.Permut
   predicate permutation_of (self : Seq.seq t) (o : Seq.seq t) =
-    [#"../../../../../creusot-contracts/src/logic/seq.rs" 101 8 101 37] Permut.permut self o 0 (Seq.length self)
+    [#"../../../../../creusot-contracts/src/logic/seq.rs" 103 8 103 37] Permut.permut self o 0 (Seq.length self)
   val permutation_of (self : Seq.seq t) (o : Seq.seq t) : bool
     ensures { result = permutation_of self o }
     
@@ -884,10 +884,10 @@ module Core_Slice_Impl0_Swap_Interface
     type t = slice t,
     type ShallowModelTy0.shallowModelTy = Seq.seq t
   val swap (self : borrowed (slice t)) (a : usize) (b : usize) : ()
-    requires {[#"../../../../../creusot-contracts/src/std/slice.rs" 237 19 237 35] UIntSize.to_int a < Seq.length (ShallowModel0.shallow_model self)}
-    requires {[#"../../../../../creusot-contracts/src/std/slice.rs" 238 19 238 35] UIntSize.to_int b < Seq.length (ShallowModel0.shallow_model self)}
+    requires {[#"../../../../../creusot-contracts/src/std/slice.rs" 242 19 242 35] UIntSize.to_int a < Seq.length (ShallowModel0.shallow_model self)}
+    requires {[#"../../../../../creusot-contracts/src/std/slice.rs" 243 19 243 35] UIntSize.to_int b < Seq.length (ShallowModel0.shallow_model self)}
     requires {Inv0.inv self}
-    ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 239 8 239 52] Permut.exchange (ShallowModel1.shallow_model ( ^ self)) (ShallowModel0.shallow_model self) (UIntSize.to_int a) (UIntSize.to_int b) }
+    ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 244 8 244 52] Permut.exchange (ShallowModel1.shallow_model ( ^ self)) (ShallowModel0.shallow_model self) (UIntSize.to_int a) (UIntSize.to_int b) }
     
 end
 module CreusotContracts_Std1_Slice_Impl5_InBounds_Stub
diff --git a/creusot/tests/should_succeed/vector/03_knuth_shuffle.mlcfg b/creusot/tests/should_succeed/vector/03_knuth_shuffle.mlcfg
index 0d506a88db..a8dfee2ce4 100644
--- a/creusot/tests/should_succeed/vector/03_knuth_shuffle.mlcfg
+++ b/creusot/tests/should_succeed/vector/03_knuth_shuffle.mlcfg
@@ -196,7 +196,7 @@ module CreusotContracts_Logic_Seq_Impl0_PermutationOf
   use seq.Seq
   use seq.Permut
   predicate permutation_of (self : Seq.seq t) (o : Seq.seq t) =
-    [#"../../../../../creusot-contracts/src/logic/seq.rs" 101 8 101 37] Permut.permut self o 0 (Seq.length self)
+    [#"../../../../../creusot-contracts/src/logic/seq.rs" 103 8 103 37] Permut.permut self o 0 (Seq.length self)
   val permutation_of (self : Seq.seq t) (o : Seq.seq t) : bool
     ensures { result = permutation_of self o }
     
@@ -671,10 +671,10 @@ module Core_Slice_Impl0_Swap_Interface
     type t = slice t,
     type ShallowModelTy0.shallowModelTy = Seq.seq t
   val swap (self : borrowed (slice t)) (a : usize) (b : usize) : ()
-    requires {[#"../../../../../creusot-contracts/src/std/slice.rs" 237 19 237 35] UIntSize.to_int a < Seq.length (ShallowModel0.shallow_model self)}
-    requires {[#"../../../../../creusot-contracts/src/std/slice.rs" 238 19 238 35] UIntSize.to_int b < Seq.length (ShallowModel0.shallow_model self)}
+    requires {[#"../../../../../creusot-contracts/src/std/slice.rs" 242 19 242 35] UIntSize.to_int a < Seq.length (ShallowModel0.shallow_model self)}
+    requires {[#"../../../../../creusot-contracts/src/std/slice.rs" 243 19 243 35] UIntSize.to_int b < Seq.length (ShallowModel0.shallow_model self)}
     requires {Inv0.inv self}
-    ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 239 8 239 52] Permut.exchange (ShallowModel1.shallow_model ( ^ self)) (ShallowModel0.shallow_model self) (UIntSize.to_int a) (UIntSize.to_int b) }
+    ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 244 8 244 52] Permut.exchange (ShallowModel1.shallow_model ( ^ self)) (ShallowModel0.shallow_model self) (UIntSize.to_int a) (UIntSize.to_int b) }
     
 end
 module CreusotContracts_Std1_Iter_Impl0_IntoIterPre_Stub
diff --git a/creusot/tests/should_succeed/vector/06_knights_tour.mlcfg b/creusot/tests/should_succeed/vector/06_knights_tour.mlcfg
index 3f2c23a25d..8acfaed360 100644
--- a/creusot/tests/should_succeed/vector/06_knights_tour.mlcfg
+++ b/creusot/tests/should_succeed/vector/06_knights_tour.mlcfg
@@ -3645,7 +3645,7 @@ module CreusotContracts_Std1_Slice_Impl15_Produces
   predicate produces (self : Core_Slice_Iter_Iter_Type.t_iter t) (visited : Seq.seq t) (tl : Core_Slice_Iter_Iter_Type.t_iter t)
     
    =
-    [#"../../../../../creusot-contracts/src/std/slice.rs" 378 12 378 66] ToRefSeq0.to_ref_seq (ShallowModel0.shallow_model self) = Seq.(++) visited (ToRefSeq0.to_ref_seq (ShallowModel0.shallow_model tl))
+    [#"../../../../../creusot-contracts/src/std/slice.rs" 383 12 383 66] ToRefSeq0.to_ref_seq (ShallowModel0.shallow_model self) = Seq.(++) visited (ToRefSeq0.to_ref_seq (ShallowModel0.shallow_model tl))
   val produces (self : Core_Slice_Iter_Iter_Type.t_iter t) (visited : Seq.seq t) (tl : Core_Slice_Iter_Iter_Type.t_iter t) : bool
     ensures { result = produces self visited tl }
     
@@ -3775,7 +3775,7 @@ module CreusotContracts_Std1_Slice_Impl15_Completed
   clone CreusotContracts_Resolve_Impl1_Resolve_Stub as Resolve0 with
     type t = Core_Slice_Iter_Iter_Type.t_iter t
   predicate completed (self : borrowed (Core_Slice_Iter_Iter_Type.t_iter t)) =
-    [#"../../../../../creusot-contracts/src/std/slice.rs" 371 20 371 61] Resolve0.resolve self /\ ShallowModel1.shallow_model (ShallowModel0.shallow_model self) = Seq.empty 
+    [#"../../../../../creusot-contracts/src/std/slice.rs" 376 20 376 61] Resolve0.resolve self /\ ShallowModel1.shallow_model (ShallowModel0.shallow_model self) = Seq.empty 
   val completed (self : borrowed (Core_Slice_Iter_Iter_Type.t_iter t)) : bool
     ensures { result = completed self }
     
@@ -3818,10 +3818,10 @@ module CreusotContracts_Std1_Slice_Impl15_ProducesRefl_Interface
     type t = t
   function produces_refl (a : Core_Slice_Iter_Iter_Type.t_iter t) : ()
   val produces_refl (a : Core_Slice_Iter_Iter_Type.t_iter t) : ()
-    ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 384 14 384 39] Produces0.produces a (Seq.empty ) a }
+    ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 389 14 389 39] Produces0.produces a (Seq.empty ) a }
     ensures { result = produces_refl a }
     
-  axiom produces_refl_spec : forall a : Core_Slice_Iter_Iter_Type.t_iter t . [#"../../../../../creusot-contracts/src/std/slice.rs" 384 14 384 39] Produces0.produces a (Seq.empty ) a
+  axiom produces_refl_spec : forall a : Core_Slice_Iter_Iter_Type.t_iter t . [#"../../../../../creusot-contracts/src/std/slice.rs" 389 14 389 39] Produces0.produces a (Seq.empty ) a
 end
 module CreusotContracts_Std1_Slice_Impl15_ProducesRefl
   type t
@@ -3830,12 +3830,12 @@ module CreusotContracts_Std1_Slice_Impl15_ProducesRefl
   clone CreusotContracts_Std1_Slice_Impl15_Produces_Stub as Produces0 with
     type t = t
   function produces_refl (a : Core_Slice_Iter_Iter_Type.t_iter t) : () =
-    [#"../../../../../creusot-contracts/src/std/slice.rs" 382 4 382 10] ()
+    [#"../../../../../creusot-contracts/src/std/slice.rs" 387 4 387 10] ()
   val produces_refl (a : Core_Slice_Iter_Iter_Type.t_iter t) : ()
-    ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 384 14 384 39] Produces0.produces a (Seq.empty ) a }
+    ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 389 14 389 39] Produces0.produces a (Seq.empty ) a }
     ensures { result = produces_refl a }
     
-  axiom produces_refl_spec : forall a : Core_Slice_Iter_Iter_Type.t_iter t . [#"../../../../../creusot-contracts/src/std/slice.rs" 384 14 384 39] Produces0.produces a (Seq.empty ) a
+  axiom produces_refl_spec : forall a : Core_Slice_Iter_Iter_Type.t_iter t . [#"../../../../../creusot-contracts/src/std/slice.rs" 389 14 389 39] Produces0.produces a (Seq.empty ) a
 end
 module CreusotContracts_Std1_Slice_Impl15_ProducesTrans_Stub
   type t
@@ -3857,12 +3857,12 @@ module CreusotContracts_Std1_Slice_Impl15_ProducesTrans_Interface
   function produces_trans (a : Core_Slice_Iter_Iter_Type.t_iter t) (ab : Seq.seq t) (b : Core_Slice_Iter_Iter_Type.t_iter t) (bc : Seq.seq t) (c : Core_Slice_Iter_Iter_Type.t_iter t) : ()
     
   val produces_trans (a : Core_Slice_Iter_Iter_Type.t_iter t) (ab : Seq.seq t) (b : Core_Slice_Iter_Iter_Type.t_iter t) (bc : Seq.seq t) (c : Core_Slice_Iter_Iter_Type.t_iter t) : ()
-    requires {[#"../../../../../creusot-contracts/src/std/slice.rs" 389 15 389 32] Produces0.produces a ab b}
-    requires {[#"../../../../../creusot-contracts/src/std/slice.rs" 390 15 390 32] Produces0.produces b bc c}
-    ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 391 14 391 42] Produces0.produces a (Seq.(++) ab bc) c }
+    requires {[#"../../../../../creusot-contracts/src/std/slice.rs" 394 15 394 32] Produces0.produces a ab b}
+    requires {[#"../../../../../creusot-contracts/src/std/slice.rs" 395 15 395 32] Produces0.produces b bc c}
+    ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 396 14 396 42] Produces0.produces a (Seq.(++) ab bc) c }
     ensures { result = produces_trans a ab b bc c }
     
-  axiom produces_trans_spec : forall a : Core_Slice_Iter_Iter_Type.t_iter t, ab : Seq.seq t, b : Core_Slice_Iter_Iter_Type.t_iter t, bc : Seq.seq t, c : Core_Slice_Iter_Iter_Type.t_iter t . ([#"../../../../../creusot-contracts/src/std/slice.rs" 389 15 389 32] Produces0.produces a ab b) -> ([#"../../../../../creusot-contracts/src/std/slice.rs" 390 15 390 32] Produces0.produces b bc c) -> ([#"../../../../../creusot-contracts/src/std/slice.rs" 391 14 391 42] Produces0.produces a (Seq.(++) ab bc) c)
+  axiom produces_trans_spec : forall a : Core_Slice_Iter_Iter_Type.t_iter t, ab : Seq.seq t, b : Core_Slice_Iter_Iter_Type.t_iter t, bc : Seq.seq t, c : Core_Slice_Iter_Iter_Type.t_iter t . ([#"../../../../../creusot-contracts/src/std/slice.rs" 394 15 394 32] Produces0.produces a ab b) -> ([#"../../../../../creusot-contracts/src/std/slice.rs" 395 15 395 32] Produces0.produces b bc c) -> ([#"../../../../../creusot-contracts/src/std/slice.rs" 396 14 396 42] Produces0.produces a (Seq.(++) ab bc) c)
 end
 module CreusotContracts_Std1_Slice_Impl15_ProducesTrans
   type t
@@ -3874,14 +3874,14 @@ module CreusotContracts_Std1_Slice_Impl15_ProducesTrans
   function produces_trans (a : Core_Slice_Iter_Iter_Type.t_iter t) (ab : Seq.seq t) (b : Core_Slice_Iter_Iter_Type.t_iter t) (bc : Seq.seq t) (c : Core_Slice_Iter_Iter_Type.t_iter t) : ()
     
    =
-    [#"../../../../../creusot-contracts/src/std/slice.rs" 387 4 387 10] ()
+    [#"../../../../../creusot-contracts/src/std/slice.rs" 392 4 392 10] ()
   val produces_trans (a : Core_Slice_Iter_Iter_Type.t_iter t) (ab : Seq.seq t) (b : Core_Slice_Iter_Iter_Type.t_iter t) (bc : Seq.seq t) (c : Core_Slice_Iter_Iter_Type.t_iter t) : ()
-    requires {[#"../../../../../creusot-contracts/src/std/slice.rs" 389 15 389 32] Produces0.produces a ab b}
-    requires {[#"../../../../../creusot-contracts/src/std/slice.rs" 390 15 390 32] Produces0.produces b bc c}
-    ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 391 14 391 42] Produces0.produces a (Seq.(++) ab bc) c }
+    requires {[#"../../../../../creusot-contracts/src/std/slice.rs" 394 15 394 32] Produces0.produces a ab b}
+    requires {[#"../../../../../creusot-contracts/src/std/slice.rs" 395 15 395 32] Produces0.produces b bc c}
+    ensures { [#"../../../../../creusot-contracts/src/std/slice.rs" 396 14 396 42] Produces0.produces a (Seq.(++) ab bc) c }
     ensures { result = produces_trans a ab b bc c }
     
-  axiom produces_trans_spec : forall a : Core_Slice_Iter_Iter_Type.t_iter t, ab : Seq.seq t, b : Core_Slice_Iter_Iter_Type.t_iter t, bc : Seq.seq t, c : Core_Slice_Iter_Iter_Type.t_iter t . ([#"../../../../../creusot-contracts/src/std/slice.rs" 389 15 389 32] Produces0.produces a ab b) -> ([#"../../../../../creusot-contracts/src/std/slice.rs" 390 15 390 32] Produces0.produces b bc c) -> ([#"../../../../../creusot-contracts/src/std/slice.rs" 391 14 391 42] Produces0.produces a (Seq.(++) ab bc) c)
+  axiom produces_trans_spec : forall a : Core_Slice_Iter_Iter_Type.t_iter t, ab : Seq.seq t, b : Core_Slice_Iter_Iter_Type.t_iter t, bc : Seq.seq t, c : Core_Slice_Iter_Iter_Type.t_iter t . ([#"../../../../../creusot-contracts/src/std/slice.rs" 394 15 394 32] Produces0.produces a ab b) -> ([#"../../../../../creusot-contracts/src/std/slice.rs" 395 15 395 32] Produces0.produces b bc c) -> ([#"../../../../../creusot-contracts/src/std/slice.rs" 396 14 396 42] Produces0.produces a (Seq.(++) ab bc) c)
 end
 module C06KnightsTour_Min_Interface
   use prelude.Borrow
diff --git a/pearlite-syn/src/term.rs b/pearlite-syn/src/term.rs
index 7981a3de2f..a0ec32192f 100644
--- a/pearlite-syn/src/term.rs
+++ b/pearlite-syn/src/term.rs
@@ -971,6 +971,34 @@ pub(crate) mod parsing {
                     }
                 }
                 lhs = Term::Binary(TermBinary { left: Box::new(lhs), op, right: Box::new(rhs) });
+            } else if Precedence::Range >= base && input.peek(Token![..]) {
+                let limits: RangeLimits = input.parse()?;
+                let rhs = if matches!(limits, RangeLimits::HalfOpen(_))
+                    && (input.is_empty()
+                        || input.peek(Token![,])
+                        || input.peek(Token![;])
+                        || input.peek(Token![.]) && !input.peek(Token![..])
+                        || !allow_struct.0 && input.peek(token::Brace))
+                {
+                    None
+                } else {
+                    let mut rhs = unary_term(input, allow_struct)?;
+                    loop {
+                        let next = peek_precedence(input);
+                        if next > Precedence::Range {
+                            rhs = parse_term(input, rhs, allow_struct, next)?;
+                        } else {
+                            break;
+                        }
+                    }
+                    Some(rhs)
+                };
+                lhs = Term::Range(TermRange {
+                    // attrs: Vec::new(),
+                    from: Some(Box::new(lhs)),
+                    limits,
+                    to: rhs.map(Box::new),
+                });
             } else if Precedence::Cast >= base && input.peek(Token![as]) {
                 let as_token: Token![as] = input.parse()?;
                 let ty = input.call(Type::without_plus)?;
diff --git a/pearlite-syn/tests/test_term.rs b/pearlite-syn/tests/test_term.rs
index 3f5ff8d780..f4b24af01e 100644
--- a/pearlite-syn/tests/test_term.rs
+++ b/pearlite-syn/tests/test_term.rs
@@ -4,6 +4,121 @@ mod macros;
 use pearlite_syn::Term;
 use quote::quote;
 
+#[test]
+fn test_range() {
+    snapshot!(quote!(x[0..]) as Term, @r###"
+    TermIndex {
+        expr: TermPath {
+            inner: ExprPath {
+                attrs: [],
+                qself: None,
+                path: Path {
+                    leading_colon: None,
+                    segments: [
+                        PathSegment {
+                            ident: Ident(
+                                x,
+                            ),
+                            arguments: PathArguments::None,
+                        },
+                    ],
+                },
+            },
+        },
+        bracket_token: Bracket,
+        index: TermRange {
+            from: Some(
+                TermLit {
+                    lit: Lit::Int {
+                        token: 0,
+                    },
+                },
+            ),
+            limits: RangeLimits::HalfOpen(
+                DotDot,
+            ),
+            to: None,
+        },
+    }
+    "###);
+    snapshot!(quote!(x[0..5]) as Term, @r###"
+    TermIndex {
+        expr: TermPath {
+            inner: ExprPath {
+                attrs: [],
+                qself: None,
+                path: Path {
+                    leading_colon: None,
+                    segments: [
+                        PathSegment {
+                            ident: Ident(
+                                x,
+                            ),
+                            arguments: PathArguments::None,
+                        },
+                    ],
+                },
+            },
+        },
+        bracket_token: Bracket,
+        index: TermRange {
+            from: Some(
+                TermLit {
+                    lit: Lit::Int {
+                        token: 0,
+                    },
+                },
+            ),
+            limits: RangeLimits::HalfOpen(
+                DotDot,
+            ),
+            to: Some(
+                TermLit {
+                    lit: Lit::Int {
+                        token: 5,
+                    },
+                },
+            ),
+        },
+    }
+    "###);
+    snapshot!(quote!(x[..5]) as Term, @r###"
+    TermIndex {
+        expr: TermPath {
+            inner: ExprPath {
+                attrs: [],
+                qself: None,
+                path: Path {
+                    leading_colon: None,
+                    segments: [
+                        PathSegment {
+                            ident: Ident(
+                                x,
+                            ),
+                            arguments: PathArguments::None,
+                        },
+                    ],
+                },
+            },
+        },
+        bracket_token: Bracket,
+        index: TermRange {
+            from: None,
+            limits: RangeLimits::HalfOpen(
+                DotDot,
+            ),
+            to: Some(
+                TermLit {
+                    lit: Lit::Int {
+                        token: 5,
+                    },
+                },
+            ),
+        },
+    }
+    "###);
+}
+
 #[test]
 fn test_impl() {
     snapshot!(quote!(false ==> true) as Term, @r###"