diff --git a/src/analyze/annot.rs b/src/analyze/annot.rs
index b246df43..7a0342dd 100644
--- a/src/analyze/annot.rs
+++ b/src/analyze/annot.rs
@@ -177,6 +177,14 @@ pub fn seq_push_path() -> [Symbol; 3] {
     ]
 }
 
+pub fn seq_subsequence_path() -> [Symbol; 3] {
+    [
+        Symbol::intern("thrust"),
+        Symbol::intern("def"),
+        Symbol::intern("seq_subsequence"),
+    ]
+}
+
 pub fn seq_concat_path() -> [Symbol; 3] {
     [
         Symbol::intern("thrust"),
diff --git a/src/analyze/annot_fn.rs b/src/analyze/annot_fn.rs
index 029db1d1..16163de1 100644
--- a/src/analyze/annot_fn.rs
+++ b/src/analyze/annot_fn.rs
@@ -649,7 +649,9 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> {
                     .ty_adt_def()
                     .is_some_and(|adt| Some(adt.did()) == self.def_ids.seq_model());
                 let array_inner = if is_seq {
-                    array_term.tuple_proj(0)
+                    let offset = array_term.clone().tuple_proj(1);
+                    let array = array_term.tuple_proj(0);
+                    return FormulaOrTerm::Term(array.select(offset.add(index_term)));
                 } else {
                     array_term
                 };
@@ -675,17 +677,33 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> {
                     if Some(def_id) == self.def_ids.seq_len() {
                         assert!(args.is_empty(), "Seq::len does not take any arguments");
                         let t = self.to_term(receiver);
-                        return FormulaOrTerm::Term(t.tuple_proj(1));
+                        return FormulaOrTerm::Term(t.tuple_proj(2));
                     }
                     if Some(def_id) == self.def_ids.seq_push() {
                         assert_eq!(args.len(), 1, "Seq::push takes exactly 1 argument");
                         let t = self.to_term(receiver);
                         let v = self.to_term(&args[0]);
                         let arr = t.clone().tuple_proj(0);
-                        let len = t.tuple_proj(1);
-                        let new_arr = arr.store(len.clone(), v);
+                        let offset = t.clone().tuple_proj(1);
+                        let len = t.tuple_proj(2);
+                        let new_arr = arr.store(offset.clone().add(len.clone()), v);
                         let new_len = len.add(chc::Term::int(1));
-                        return FormulaOrTerm::Term(chc::Term::tuple(vec![new_arr, new_len]));
+                        return FormulaOrTerm::Term(chc::Term::tuple(vec![
+                            new_arr, offset, new_len,
+                        ]));
+                    }
+                    if Some(def_id) == self.def_ids.seq_subsequence() {
+                        assert_eq!(args.len(), 2, "Seq::subsequence takes exactly 2 arguments");
+                        let t = self.to_term(receiver);
+                        let start = self.to_term(&args[0]);
+                        let end = self.to_term(&args[1]);
+                        let arr = t.clone().tuple_proj(0);
+                        let offset = t.clone().tuple_proj(1);
+                        return FormulaOrTerm::Term(chc::Term::tuple(vec![
+                            arr,
+                            offset.add(start.clone()),
+                            end.sub(start),
+                        ]));
                     }
                     if Some(def_id) == self.def_ids.seq_concat() {
                         assert_eq!(args.len(), 1, "Seq::concat takes exactly 1 argument");
@@ -693,18 +711,24 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> {
                         let t = self.to_term(receiver);
                         let other = self.to_term(&args[0]);
                         let a_arr = t.clone().tuple_proj(0);
-                        let a_len = t.tuple_proj(1);
+                        let a_offset = t.clone().tuple_proj(1);
+                        let a_len = t.tuple_proj(2);
                         let b_arr = other.clone().tuple_proj(0);
-                        let b_len = other.tuple_proj(1);
+                        let b_offset = other.clone().tuple_proj(1);
+                        let b_len = other.tuple_proj(2);
                         let new_arr = chc::Term::array_concat(
                             elem_sort,
                             a_arr,
+                            a_offset.clone(),
                             a_len.clone(),
                             b_arr,
+                            b_offset,
                             b_len.clone(),
                         );
                         let new_len = a_len.add(b_len);
-                        return FormulaOrTerm::Term(chc::Term::tuple(vec![new_arr, new_len]));
+                        return FormulaOrTerm::Term(chc::Term::tuple(vec![
+                            new_arr, a_offset, new_len,
+                        ]));
                     }
                 }
                 unimplemented!("unsupported method call in formula: {:?}", method)
@@ -787,6 +811,7 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> {
                             return FormulaOrTerm::Term(chc::Term::tuple(vec![
                                 chc::Term::array_empty(chc::Sort::int(), elem_sort),
                                 chc::Term::int(0),
+                                chc::Term::int(0),
                             ]));
                         }
                         if Some(def_id) == self.def_ids.seq_singleton() {
@@ -797,6 +822,7 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> {
                                 .store(chc::Term::int(0), v);
                             return FormulaOrTerm::Term(chc::Term::tuple(vec![
                                 new_arr,
+                                chc::Term::int(0),
                                 chc::Term::int(1),
                             ]));
                         }
diff --git a/src/analyze/did_cache.rs b/src/analyze/did_cache.rs
index 4dbcf110..78b35fb5 100644
--- a/src/analyze/did_cache.rs
+++ b/src/analyze/did_cache.rs
@@ -29,6 +29,7 @@ struct DefIds {
     seq_singleton: OnceCell<Option<DefId>>,
     seq_len: OnceCell<Option<DefId>>,
     seq_push: OnceCell<Option<DefId>>,
+    seq_subsequence: OnceCell<Option<DefId>>,
     seq_concat: OnceCell<Option<DefId>>,
 
     exists: OnceCell<Option<DefId>>,
@@ -221,6 +222,13 @@ impl<'tcx> DefIdCache<'tcx> {
             .get_or_init(|| self.annotated_def(&crate::analyze::annot::seq_push_path()))
     }
 
+    pub fn seq_subsequence(&self) -> Option<DefId> {
+        *self
+            .def_ids
+            .seq_subsequence
+            .get_or_init(|| self.annotated_def(&crate::analyze::annot::seq_subsequence_path()))
+    }
+
     pub fn seq_concat(&self) -> Option<DefId> {
         *self
             .def_ids
diff --git a/src/chc.rs b/src/chc.rs
index 1dba68d5..795304c2 100644
--- a/src/chc.rs
+++ b/src/chc.rs
@@ -439,8 +439,10 @@ impl Function {
 #[derive(Debug, Clone)]
 pub struct ArrayConcatTerm<V = TermVarIdx> {
     pub array1: Term<V>,
+    pub offset1: Term<V>,
     pub len1: Term<V>,
     pub array2: Term<V>,
+    pub offset2: Term<V>,
     pub len2: Term<V>,
 }
 
@@ -457,12 +459,18 @@ where
             .append(self.array1.pretty_atom(allocator))
             .append(allocator.text(","))
             .append(allocator.line())
+            .append(self.offset1.pretty_atom(allocator))
+            .append(allocator.text(","))
+            .append(allocator.line())
             .append(self.len1.pretty_atom(allocator))
             .append(allocator.text(","))
             .append(allocator.line())
             .append(self.array2.pretty_atom(allocator))
             .append(allocator.text(","))
             .append(allocator.line())
+            .append(self.offset2.pretty_atom(allocator))
+            .append(allocator.text(","))
+            .append(allocator.line())
             .append(self.len2.pretty_atom(allocator))
             .parens()
     }
@@ -471,15 +479,19 @@ where
 impl<V> ArrayConcatTerm<V> {
     pub fn iter_args(&self) -> impl Iterator<Item = &Term<V>> {
         std::iter::once(&self.array1)
+            .chain(std::iter::once(&self.offset1))
             .chain(std::iter::once(&self.len1))
             .chain(std::iter::once(&self.array2))
+            .chain(std::iter::once(&self.offset2))
             .chain(std::iter::once(&self.len2))
     }
 
     pub fn iter_args_mut(&mut self) -> impl Iterator<Item = &mut Term<V>> {
         std::iter::once(&mut self.array1)
+            .chain(std::iter::once(&mut self.offset1))
             .chain(std::iter::once(&mut self.len1))
             .chain(std::iter::once(&mut self.array2))
+            .chain(std::iter::once(&mut self.offset2))
             .chain(std::iter::once(&mut self.len2))
     }
 
@@ -489,8 +501,10 @@ impl<V> ArrayConcatTerm<V> {
     {
         ArrayConcatTerm {
             array1: self.array1.subst_var(&mut f),
+            offset1: self.offset1.subst_var(&mut f),
             len1: self.len1.subst_var(&mut f),
             array2: self.array2.subst_var(&mut f),
+            offset2: self.offset2.subst_var(&mut f),
             len2: self.len2.subst_var(f),
         }
     }
@@ -775,16 +789,20 @@ impl<V> Term<V> {
     pub fn array_concat(
         elem_sort: Sort,
         array1: Term<V>,
+        offset1: Term<V>,
         len1: Term<V>,
         array2: Term<V>,
+        offset2: Term<V>,
         len2: Term<V>,
     ) -> Self {
         Term::ArrayConcat(
             elem_sort,
             Box::new(ArrayConcatTerm {
                 array1,
+                offset1,
                 len1,
                 array2,
+                offset2,
                 len2,
             }),
         )
@@ -899,12 +917,13 @@ impl<V> Term<V> {
         // indexed properties against the inlined ITE for *any* recursion bound, where unfolding
         // through `define-fun-rec` would require an inductive invariant pcsat can't find.
         //
-        // `select(concat_int_array(sa, sn, ta, tn), i)
-        //   ↦ ite(i < sn, select(sa, i), select(ta, i - sn))`
+        // `select(concat_int_array(sa, so, sn, ta, to, tn), i)`
+        //   ↦ ite(i < so + sn, select(sa, i), select(ta, to + i - (so + sn)))`
         if let Term::ArrayConcat(_, t) = self {
-            let cond = index.clone().lt(t.len1.clone());
+            let split = t.offset1.clone().add(t.len1.clone());
+            let cond = index.clone().lt(split.clone());
             let then_ = t.array1.select(index.clone());
-            let else_ = t.array2.select(index.sub(t.len1));
+            let else_ = t.array2.select(t.offset2.add(index.sub(split)));
             return Term::ite(cond, then_, else_);
         }
         Term::App(Function::SELECT, vec![self, index])
diff --git a/src/chc/smtlib2.rs b/src/chc/smtlib2.rs
index 89e1710d..363e43e3 100644
--- a/src/chc/smtlib2.rs
+++ b/src/chc/smtlib2.rs
@@ -644,12 +644,12 @@ impl<'a> std::fmt::Display for System<'a> {
             writeln!(
                 f,
                 "(define-fun-rec {name} \
-                  ((sa (Array Int {elem_ty})) (sn Int) (ta (Array Int {elem_ty})) (tn Int)) \
+                  ((sa (Array Int {elem_ty})) (so Int) (sn Int) (ta (Array Int {elem_ty})) (to Int) (tn Int)) \
                   (Array Int {elem_ty}) \
                   (ite (<= tn 0) sa \
-                       (store ({name} sa sn ta (- tn 1)) \
-                              (+ sn (- tn 1)) \
-                              (select ta (- tn 1)))))\n",
+                       (store ({name} sa so sn ta to (- tn 1)) \
+                              (+ so sn (- tn 1)) \
+                              (select ta (+ to (- tn 1))))))\n",
             )?;
         }
 
diff --git a/src/chc/unbox.rs b/src/chc/unbox.rs
index b13ab96c..04c95fd1 100644
--- a/src/chc/unbox.rs
+++ b/src/chc/unbox.rs
@@ -5,18 +5,24 @@ use super::*;
 fn unbox_array_concat_term(t: ArrayConcatTerm) -> ArrayConcatTerm {
     let ArrayConcatTerm {
         array1,
+        offset1,
         len1,
         array2,
+        offset2,
         len2,
     } = t;
     let array1 = unbox_term(array1);
+    let offset1 = unbox_term(offset1);
     let len1 = unbox_term(len1);
     let array2 = unbox_term(array2);
+    let offset2 = unbox_term(offset2);
     let len2 = unbox_term(len2);
     ArrayConcatTerm {
         array1,
+        offset1,
         len1,
         array2,
+        offset2,
         len2,
     }
 }
diff --git a/std.rs b/std.rs
index 32525a2b..019a5499 100644
--- a/std.rs
+++ b/std.rs
@@ -188,7 +188,7 @@ mod thrust_models {
         }
 
         #[thrust::def::seq_model]
-        pub struct Seq<T: ?Sized>(pub Array<Int, T>, pub Int);
+        pub struct Seq<T: ?Sized>(pub Array<Int, T>, pub Int, pub Int);
 
         impl<T, U> PartialEq<U> for Seq<T> where U: super::Model<Ty = Self> {
             #[thrust::ignored]
@@ -235,6 +235,17 @@ mod thrust_models {
                 unimplemented!()
             }
 
+            #[allow(dead_code)]
+            #[thrust::def::seq_subsequence]
+            #[thrust::ignored]
+            pub fn subsequence<U, V>(self, _start: U, _end: V) -> Self
+            where
+                U: super::Model<Ty = Int>,
+                V: super::Model<Ty = Int>,
+            {
+                unimplemented!()
+            }
+
             #[allow(dead_code)]
             #[thrust::def::seq_concat]
             #[thrust::ignored]
@@ -711,14 +722,14 @@ fn _extern_spec_i32_is_negative(x: i32) -> bool {
 
 #[thrust::extern_spec_fn]
 #[thrust_macros::requires(true)]
-#[thrust_macros::ensures(result.1 == 0)]
+#[thrust_macros::ensures(result.1 == 0 && result.2 == 0)]
 fn _extern_spec_vec_new<T>() -> Vec<T> where T: thrust_models::Model, T::Ty: PartialEq {
     Vec::<T>::new()
 }
 
 #[thrust::extern_spec_fn]
 #[thrust_macros::requires(true)]
-#[thrust_macros::ensures(!vec == thrust_models::model::Seq((*vec).0.store((*vec).1, elem), (*vec).1 + 1))]
+#[thrust_macros::ensures(!vec == thrust_models::model::Seq((*vec).0.store((*vec).1 + (*vec).2, elem), (*vec).1, (*vec).2 + 1))]
 fn _extern_spec_vec_push<T>(vec: &mut Vec<T>, elem: T)
     where T: thrust_models::Model, T::Ty: PartialEq
 {
@@ -727,24 +738,24 @@ fn _extern_spec_vec_push<T>(vec: &mut Vec<T>, elem: T)
 
 #[thrust::extern_spec_fn]
 #[thrust_macros::requires(true)]
-#[thrust_macros::ensures(result == vec.1)]
+#[thrust_macros::ensures(result == vec.2)]
 fn _extern_spec_vec_len<T>(vec: &Vec<T>) -> usize where T: thrust_models::Model, T::Ty: PartialEq {
     Vec::len(vec)
 }
 
 #[thrust::extern_spec_fn]
-#[thrust_macros::requires(index < vec.1)]
-#[thrust_macros::ensures(*result == vec.0[index])]
+#[thrust_macros::requires(index < vec.2)]
+#[thrust_macros::ensures(*result == vec.0[vec.1 + index])]
 fn _extern_spec_vec_index<T>(vec: &Vec<T>, index: usize) -> &T where T: thrust_models::Model, T::Ty: PartialEq {
     <Vec<T> as std::ops::Index<usize>>::index(vec, index)
 }
 
 #[thrust::extern_spec_fn]
-#[thrust_macros::requires(index < (*vec).1)]
+#[thrust_macros::requires(index < (*vec).2)]
 #[thrust_macros::ensures(
-    *result == (*vec).0[index] &&
-    !result == (!vec).0[index] &&
-    !vec == thrust_models::model::Seq((*vec).0.store(index, !result), (*vec).1)
+    *result == (*vec).0[(*vec).1 + index] &&
+    !result == (!vec).0[(!vec).1 + index] &&
+    !vec == thrust_models::model::Seq((*vec).0.store((*vec).1 + index, !result), (*vec).1, (*vec).2)
 )]
 fn _extern_spec_vec_index_mut<T>(vec: &mut Vec<T>, index: usize) -> &mut T
     where T: thrust_models::Model, T::Ty: PartialEq
@@ -754,7 +765,9 @@ fn _extern_spec_vec_index_mut<T>(vec: &mut Vec<T>, index: usize) -> &mut T
 
 #[thrust::extern_spec_fn]
 #[thrust_macros::requires(true)]
-#[thrust_macros::ensures((!vec).1 == 0)]
+#[thrust_macros::ensures(
+    (!vec).0 == (*vec).0 && (!vec).1 == (*vec).1 && (!vec).2 == 0
+)]
 fn _extern_spec_vec_clear<T>(vec: &mut Vec<T>) where T: thrust_models::Model, T::Ty: PartialEq {
     Vec::clear(vec)
 }
@@ -762,14 +775,14 @@ fn _extern_spec_vec_clear<T>(vec: &mut Vec<T>) where T: thrust_models::Model, T:
 #[thrust::extern_spec_fn]
 #[thrust_macros::requires(true)]
 #[thrust_macros::ensures(
-    (!vec).0 == (*vec).0 && (
+    (!vec).0 == (*vec).0 && (!vec).1 == (*vec).1 && (
         (
-            (*vec).1 > 0 &&
-            (!vec).1 == (*vec).1 - 1 &&
-            result == Some((*vec).0[(*vec).1 - 1])
+        (*vec).2 > 0 &&
+        (!vec).2 == (*vec).2 - 1 &&
+        result == Some((*vec).0[(*vec).1 + (*vec).2 - 1])
         ) || (
-            (*vec).1 == 0 &&
-            (!vec).1 == 0 &&
+        (*vec).2 == 0 &&
+        (!vec).2 == 0 &&
             result == None
         )
     )
@@ -780,7 +793,7 @@ fn _extern_spec_vec_pop<T>(vec: &mut Vec<T>) -> Option<T> where T: thrust_models
 
 #[thrust::extern_spec_fn]
 #[thrust_macros::requires(true)]
-#[thrust_macros::ensures(result == ((*vec).1 == 0))]
+#[thrust_macros::ensures(result == ((*vec).2 == 0))]
 fn _extern_spec_vec_is_empty<T>(vec: &Vec<T>) -> bool where T: thrust_models::Model, T::Ty: PartialEq {
     Vec::is_empty(vec)
 }
@@ -789,10 +802,10 @@ fn _extern_spec_vec_is_empty<T>(vec: &Vec<T>) -> bool where T: thrust_models::Mo
 #[thrust_macros::requires(true)]
 #[thrust_macros::ensures(
     (
-        (*vec).1 > len &&
-        !vec == thrust_models::model::Seq((*vec).0, len)
+        (*vec).2 > len &&
+        !vec == thrust_models::model::Seq((*vec).0, (*vec).1, len)
     ) || (
-        (*vec).1 <= len &&
+        (*vec).2 <= len &&
         !vec == *vec
     )
 )]
@@ -802,7 +815,7 @@ fn _extern_spec_vec_truncate<T>(vec: &mut Vec<T>, len: usize) where T: thrust_mo
 
 #[thrust::extern_spec_fn]
 #[thrust_macros::requires(true)]
-#[thrust_macros::ensures(result == slice.1)]
+#[thrust_macros::ensures(result == slice.2)]
 fn _extern_spec_slice_len<T>(slice: &[T]) -> usize
     where T: thrust_models::Model, T::Ty: PartialEq
 {
@@ -811,7 +824,7 @@ fn _extern_spec_slice_len<T>(slice: &[T]) -> usize
 
 #[thrust::extern_spec_fn]
 #[thrust_macros::requires(true)]
-#[thrust_macros::ensures(result == (slice.1 == 0))]
+#[thrust_macros::ensures(result == (slice.2 == 0))]
 fn _extern_spec_slice_is_empty<T>(slice: &[T]) -> bool
     where T: thrust_models::Model, T::Ty: PartialEq
 {
@@ -821,8 +834,8 @@ fn _extern_spec_slice_is_empty<T>(slice: &[T]) -> bool
 #[thrust::extern_spec_fn]
 #[thrust_macros::requires(true)]
 #[thrust_macros::ensures(
-    (index < slice.1 && result == Some(&slice.0[index]))
-    || (slice.1 <= index && result == None)
+    (index < slice.2 && result == Some(&slice.0[slice.1 + index]))
+    || (slice.2 <= index && result == None)
 )]
 fn _extern_spec_slice_get<T>(slice: &[T], index: usize) -> Option<&T>
     where T: thrust_models::Model, T::Ty: PartialEq
@@ -833,17 +846,18 @@ fn _extern_spec_slice_get<T>(slice: &[T], index: usize) -> Option<&T>
 #[thrust::extern_spec_fn]
 #[thrust_macros::requires(true)]
 #[thrust_macros::ensures(
-    (index < (*slice).1
+    (index < (*slice).2
         && result == Some(thrust_models::model::Mut::new(
-            (*slice).0[index],
-            (!slice).0[index],
+            (*slice).0[(*slice).1 + index],
+            (!slice).0[(*slice).1 + index],
         ))
         && !slice == thrust_models::model::Seq(
-            (*slice).0.store(index, (!slice).0[index]),
+            (*slice).0.store((*slice).1 + index, (!slice).0[(*slice).1 + index]),
             (*slice).1,
+            (*slice).2,
         )
     )
-    || ((*slice).1 <= index && result == None && !slice == *slice)
+    || ((*slice).2 <= index && result == None && !slice == *slice)
 )]
 fn _extern_spec_slice_get_mut<T>(slice: &mut [T], index: usize) -> Option<&mut T>
     where T: thrust_models::Model, T::Ty: PartialEq
@@ -854,8 +868,8 @@ fn _extern_spec_slice_get_mut<T>(slice: &mut [T], index: usize) -> Option<&mut T
 #[thrust::extern_spec_fn]
 #[thrust_macros::requires(true)]
 #[thrust_macros::ensures(
-    (slice.1 > 0 && result == Some(&slice.0[0]))
-    || (slice.1 == 0 && result == None)
+    (slice.2 > 0 && result == Some(&slice.0[slice.1]))
+    || (slice.2 == 0 && result == None)
 )]
 fn _extern_spec_slice_first<T>(slice: &[T]) -> Option<&T>
     where T: thrust_models::Model, T::Ty: PartialEq
@@ -866,17 +880,18 @@ fn _extern_spec_slice_first<T>(slice: &[T]) -> Option<&T>
 #[thrust::extern_spec_fn]
 #[thrust_macros::requires(true)]
 #[thrust_macros::ensures(
-    ((*slice).1 > 0
+    ((*slice).2 > 0
         && result == Some(thrust_models::model::Mut::new(
-            (*slice).0[0],
-            (!slice).0[0],
+            (*slice).0[(*slice).1],
+            (!slice).0[(*slice).1],
         ))
         && !slice == thrust_models::model::Seq(
-            (*slice).0.store(0, (!slice).0[0]),
+            (*slice).0.store((*slice).1, (!slice).0[(*slice).1]),
             (*slice).1,
+            (*slice).2,
         )
     )
-    || ((*slice).1 == 0 && result == None && !slice == *slice)
+    || ((*slice).2 == 0 && result == None && !slice == *slice)
 )]
 fn _extern_spec_slice_first_mut<T>(slice: &mut [T]) -> Option<&mut T>
     where T: thrust_models::Model, T::Ty: PartialEq
@@ -887,8 +902,8 @@ fn _extern_spec_slice_first_mut<T>(slice: &mut [T]) -> Option<&mut T>
 #[thrust::extern_spec_fn]
 #[thrust_macros::requires(true)]
 #[thrust_macros::ensures(
-    (slice.1 > 0 && result == Some(&slice.0[slice.1 - 1]))
-    || (slice.1 == 0 && result == None)
+    (slice.2 > 0 && result == Some(&slice.0[slice.1 + slice.2 - 1]))
+    || (slice.2 == 0 && result == None)
 )]
 fn _extern_spec_slice_last<T>(slice: &[T]) -> Option<&T>
     where T: thrust_models::Model, T::Ty: PartialEq
@@ -899,20 +914,21 @@ fn _extern_spec_slice_last<T>(slice: &[T]) -> Option<&T>
 #[thrust::extern_spec_fn]
 #[thrust_macros::requires(true)]
 #[thrust_macros::ensures(
-    ((*slice).1 > 0
+    ((*slice).2 > 0
         && result == Some(thrust_models::model::Mut::new(
-            (*slice).0[(*slice).1 - 1],
-            (!slice).0[(*slice).1 - 1],
+            (*slice).0[(*slice).1 + (*slice).2 - 1],
+            (!slice).0[(*slice).1 + (*slice).2 - 1],
         ))
         && !slice == thrust_models::model::Seq(
             (*slice).0.store(
-                (*slice).1 - 1,
-                (!slice).0[(*slice).1 - 1],
+                (*slice).1 + (*slice).2 - 1,
+                (!slice).0[(*slice).1 + (*slice).2 - 1],
             ),
             (*slice).1,
+            (*slice).2,
         )
     )
-    || ((*slice).1 == 0 && result == None && !slice == *slice)
+    || ((*slice).2 == 0 && result == None && !slice == *slice)
 )]
 fn _extern_spec_slice_last_mut<T>(slice: &mut [T]) -> Option<&mut T>
     where T: thrust_models::Model, T::Ty: PartialEq
@@ -924,8 +940,31 @@ fn _extern_spec_slice_last_mut<T>(slice: &mut [T]) -> Option<&mut T>
 //       a generic index (I: SliceIndex) that isn't specific to usize, maybe once #83 is implemented.
 
 #[thrust::extern_spec_fn]
-#[thrust_macros::requires(index < slice.1)]
-#[thrust_macros::ensures(*result == slice.0[index])]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(
+    (
+        (*slice).len() > 0
+        && (!slice).1 == (*slice).1
+        && (!slice).2 == (*slice).2
+        && result == Some((
+            thrust_models::model::Mut::new((*slice)[0], (!slice)[0]),
+            thrust_models::model::Mut::new(
+                (*slice).subsequence(1, (*slice).len()),
+                (!slice).subsequence(1, (!slice).len()),
+            ),
+        ))
+    )
+    || ((*slice).len() == 0 && result == None && !slice == *slice)
+)]
+fn _extern_spec_slice_split_first_mut<T>(slice: &mut [T]) -> Option<(&mut T, &mut [T])>
+    where T: thrust_models::Model, T::Ty: PartialEq
+{
+    <[T]>::split_first_mut(slice)
+}
+
+#[thrust::extern_spec_fn]
+#[thrust_macros::requires(index < slice.2)]
+#[thrust_macros::ensures(*result == slice.0[slice.1 + index])]
 fn _extern_spec_slice_index<T>(slice: &[T], index: usize) -> &T
     where T: thrust_models::Model, T::Ty: PartialEq
 {
@@ -933,13 +972,14 @@ fn _extern_spec_slice_index<T>(slice: &[T], index: usize) -> &T
 }
 
 #[thrust::extern_spec_fn]
-#[thrust_macros::requires(index < (*slice).1)]
+#[thrust_macros::requires(index < (*slice).2)]
 #[thrust_macros::ensures(
-    *result == (*slice).0[index] &&
-    !result == (!slice).0[index] &&
+    *result == (*slice).0[(*slice).1 + index] &&
+    !result == (!slice).0[(!slice).1 + index] &&
     !slice == thrust_models::model::Seq(
-        (*slice).0.store(index, !result),
+        (*slice).0.store((*slice).1 + index, !result),
         (*slice).1,
+        (*slice).2,
     )
 )]
 fn _extern_spec_slice_index_mut<T>(slice: &mut [T], index: usize) -> &mut T
diff --git a/tests/ui/fail/loop_invariant_fn_param_at_entry.rs b/tests/ui/fail/loop_invariant_fn_param_at_entry.rs
index 17b4554f..d394a173 100644
--- a/tests/ui/fail/loop_invariant_fn_param_at_entry.rs
+++ b/tests/ui/fail/loop_invariant_fn_param_at_entry.rs
@@ -2,7 +2,7 @@
 //@compile-flags: -C debug-assertions=off
 
 #[thrust_macros::requires(true)]
-#[thrust_macros::ensures(result.1 == v.1 + 2)]
+#[thrust_macros::ensures(result.2 == v.2 + 2)]
 #[thrust_macros::invariant_context]
 fn push_two(v: Vec<i64>) -> Vec<i64> {
     let mut w = v;
@@ -10,7 +10,7 @@ fn push_two(v: Vec<i64>) -> Vec<i64> {
     while i < 2 {
         thrust_macros::invariant!(
             |i: i64, w: Vec<i64>, v: thrust_models::FnParam<Vec<i64>>|
-                w.1 == v.at_entry().1 + i && i <= 2
+                w.2 == v.at_entry().2 + i && i <= 2
         );
         w.push(i);
         w.push(i);
diff --git a/tests/ui/fail/seq_specs_vec_build.rs b/tests/ui/fail/seq_specs_vec_build.rs
index 1f083b2f..9c1cd760 100644
--- a/tests/ui/fail/seq_specs_vec_build.rs
+++ b/tests/ui/fail/seq_specs_vec_build.rs
@@ -6,11 +6,11 @@ use thrust_models::model::Seq;
 
 #[thrust_macros::requires(true)]
 #[thrust_macros::ensures(
-    result.1 == Seq::empty().push(10).push(20).push(30).len()
-        && result.0[0] == Seq::empty().push(10).push(20).push(30)[0]
-        && result.0[1] == Seq::empty().push(10).push(20).push(30)[1]
+    result.2 == Seq::empty().push(10).push(20).push(30).len()
+        && result.0[result.1] == Seq::empty().push(10).push(20).push(30)[0]
+        && result.0[result.1 + 1] == Seq::empty().push(10).push(20).push(30)[1]
         // wrong: last element should be 30, not 99
-        && result.0[2] == Seq::empty().push(10).push(20).push(99)[2]
+        && result.0[result.1 + 2] == Seq::empty().push(10).push(20).push(99)[2]
 )]
 fn build_three() -> Vec<i64> {
     let mut v = Vec::new();
diff --git a/tests/ui/fail/seq_subsequence.rs b/tests/ui/fail/seq_subsequence.rs
new file mode 100644
index 00000000..1ed99b4c
--- /dev/null
+++ b/tests/ui/fail/seq_subsequence.rs
@@ -0,0 +1,13 @@
+//@error-in-other-file: Unsat
+//@compile-flags: -C debug-assertions=off
+//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper
+
+use thrust_models::model::{Int, Seq};
+
+#[thrust_macros::requires(0 <= start && start < end && end <= s.len())]
+#[thrust_macros::ensures(s.subsequence(start, end)[0] == s[end])]
+fn seq_subsequence(s: Seq<Int>, start: Int, end: Int) {
+    let _ = (s, start, end);
+}
+
+fn main() {}
diff --git a/tests/ui/fail/slice_first_mut.rs b/tests/ui/fail/slice_first_mut.rs
index df4bb101..476f218c 100644
--- a/tests/ui/fail/slice_first_mut.rs
+++ b/tests/ui/fail/slice_first_mut.rs
@@ -4,7 +4,7 @@
 #[thrust::trusted]
 #[thrust_macros::requires(true)]
 #[thrust_macros::ensures(
-    (*result).1 > 0 && (*result).0[0] == 10
+    (*result).2 > 0 && (*result).0[(*result).1] == 10
 )]
 fn slice() -> &'static mut [i32] {
     unimplemented!()
diff --git a/tests/ui/fail/slice_index.rs b/tests/ui/fail/slice_index.rs
index 1d780e9d..21dfd2ca 100644
--- a/tests/ui/fail/slice_index.rs
+++ b/tests/ui/fail/slice_index.rs
@@ -3,7 +3,7 @@
 
 #[thrust::trusted]
 #[thrust_macros::requires(true)]
-#[thrust_macros::ensures(result.1 == 1 && result.0[0] == 10)]
+#[thrust_macros::ensures(result.2 == 1 && result.0[result.1] == 10)]
 fn slice() -> &'static [i32] {
     unimplemented!()
 }
diff --git a/tests/ui/fail/slice_index_mut.rs b/tests/ui/fail/slice_index_mut.rs
index a9301178..ee0a6e8f 100644
--- a/tests/ui/fail/slice_index_mut.rs
+++ b/tests/ui/fail/slice_index_mut.rs
@@ -4,7 +4,7 @@
 #[thrust::trusted]
 #[thrust_macros::requires(true)]
 #[thrust_macros::ensures(
-    (*result).1 > 1 && (*result).0[1] == 20
+    (*result).2 > 1 && (*result).0[(*result).1 + 1] == 20
 )]
 fn slice() -> &'static mut [i32] {
     unimplemented!()
diff --git a/tests/ui/fail/slice_last_mut.rs b/tests/ui/fail/slice_last_mut.rs
index 9b46c333..c89488db 100644
--- a/tests/ui/fail/slice_last_mut.rs
+++ b/tests/ui/fail/slice_last_mut.rs
@@ -4,8 +4,8 @@
 #[thrust::trusted]
 #[thrust_macros::requires(true)]
 #[thrust_macros::ensures(
-    (*result).1 > 0
-        && (*result).0[(*result).1 - 1] == 30
+    (*result).2 > 0
+        && (*result).0[(*result).1 + (*result).2 - 1] == 30
 )]
 fn slice() -> &'static mut [i32] {
     unimplemented!()
diff --git a/tests/ui/fail/slice_methods.rs b/tests/ui/fail/slice_methods.rs
index 2ede1088..4620f9f7 100644
--- a/tests/ui/fail/slice_methods.rs
+++ b/tests/ui/fail/slice_methods.rs
@@ -4,9 +4,9 @@
 #[thrust::trusted]
 #[thrust_macros::requires(true)]
 #[thrust_macros::ensures(
-    result.1 == 2
-        && result.0[0] == 10
-        && result.0[1] == 20
+    result.2 == 2
+        && result.0[result.1] == 10
+        && result.0[result.1 + 1] == 20
 )]
 fn slice() -> &'static [i32] {
     unimplemented!()
diff --git a/tests/ui/fail/slice_methods_mut.rs b/tests/ui/fail/slice_methods_mut.rs
index 6783f536..473a415a 100644
--- a/tests/ui/fail/slice_methods_mut.rs
+++ b/tests/ui/fail/slice_methods_mut.rs
@@ -4,7 +4,7 @@
 #[thrust::trusted]
 #[thrust_macros::requires(true)]
 #[thrust_macros::ensures(
-    (*result).1 > 1 && (*result).0[1] == 20
+    (*result).2 > 1 && (*result).0[(*result).1 + 1] == 20
 )]
 fn slice() -> &'static mut [i32] {
     unimplemented!()
diff --git a/tests/ui/fail/slice_split_first_mut.rs b/tests/ui/fail/slice_split_first_mut.rs
new file mode 100644
index 00000000..39a04058
--- /dev/null
+++ b/tests/ui/fail/slice_split_first_mut.rs
@@ -0,0 +1,18 @@
+//@error-in-other-file: Unsat
+//@compile-flags: -C debug-assertions=off
+#[thrust::trusted]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(
+    (*result).2 == 2
+        && (*result).0[(*result).1] == 10
+        && (*result).0[(*result).1 + 1] == 20
+)]
+fn slice() -> &'static mut [i32] {
+    unimplemented!()
+}
+
+fn main() {
+    let slice = slice();
+    let (first, _tail) = slice.split_first_mut().unwrap();
+    assert!(*first == 11);
+}
diff --git a/tests/ui/fail/slice_split_first_mut_mutation_unsound.rs b/tests/ui/fail/slice_split_first_mut_mutation_unsound.rs
new file mode 100644
index 00000000..1308eb12
--- /dev/null
+++ b/tests/ui/fail/slice_split_first_mut_mutation_unsound.rs
@@ -0,0 +1,24 @@
+//@error-in-other-file: Unsat
+//@compile-flags: -C debug-assertions=off
+
+#[thrust::trusted]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(
+    (*result).2 == 2
+        && (*result).0[(*result).1] == 10
+        && (*result).0[(*result).1 + 1] == 20
+)]
+fn slice() -> &'static mut [i32] {
+    unimplemented!()
+}
+
+fn main() {
+    let slice = slice();
+    {
+        // Destructure the returned tuple, then mutate through its first reference.
+        let (first, _tail) = slice.split_first_mut().unwrap();
+        *first = 11;
+    }
+    // The mutation makes slice[0] equal to 11, so this must be rejected.
+    assert!(slice[0] == 12);
+}
diff --git a/tests/ui/pass/loop_invariant_fn_param_at_entry.rs b/tests/ui/pass/loop_invariant_fn_param_at_entry.rs
index 3ec3a4da..163d8078 100644
--- a/tests/ui/pass/loop_invariant_fn_param_at_entry.rs
+++ b/tests/ui/pass/loop_invariant_fn_param_at_entry.rs
@@ -2,7 +2,7 @@
 //@compile-flags: -C debug-assertions=off
 
 #[thrust_macros::requires(true)]
-#[thrust_macros::ensures(result.1 == v.1 + 2)]
+#[thrust_macros::ensures(result.2 == v.2 + 2)]
 #[thrust_macros::invariant_context]
 fn push_two(v: Vec<i64>) -> Vec<i64> {
     let mut w = v;
@@ -10,7 +10,7 @@ fn push_two(v: Vec<i64>) -> Vec<i64> {
     while i < 2 {
         thrust_macros::invariant!(
             |i: i64, w: Vec<i64>, v: thrust_models::FnParam<Vec<i64>>|
-                w.1 == v.at_entry().1 + i && i <= 2
+                w.2 == v.at_entry().2 + i && i <= 2
         );
         w.push(i);
         i += 1;
diff --git a/tests/ui/pass/seq_specs_vec_build.rs b/tests/ui/pass/seq_specs_vec_build.rs
index a1936ca5..3743ae6f 100644
--- a/tests/ui/pass/seq_specs_vec_build.rs
+++ b/tests/ui/pass/seq_specs_vec_build.rs
@@ -6,10 +6,10 @@ use thrust_models::model::Seq;
 
 #[thrust_macros::requires(true)]
 #[thrust_macros::ensures(
-    result.1 == Seq::empty().push(10).push(20).push(30).len()
-        && result.0[0] == Seq::empty().push(10).push(20).push(30)[0]
-        && result.0[1] == Seq::empty().push(10).push(20).push(30)[1]
-        && result.0[2] == Seq::empty().push(10).push(20).push(30)[2]
+    result.2 == Seq::empty().push(10).push(20).push(30).len()
+        && result.0[result.1] == Seq::empty().push(10).push(20).push(30)[0]
+        && result.0[result.1 + 1] == Seq::empty().push(10).push(20).push(30)[1]
+        && result.0[result.1 + 2] == Seq::empty().push(10).push(20).push(30)[2]
 )]
 fn build_three() -> Vec<i64> {
     let mut v = Vec::new();
diff --git a/tests/ui/pass/seq_subsequence.rs b/tests/ui/pass/seq_subsequence.rs
new file mode 100644
index 00000000..9ae1f819
--- /dev/null
+++ b/tests/ui/pass/seq_subsequence.rs
@@ -0,0 +1,19 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off
+//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper
+
+use thrust_models::model::{Int, Seq};
+
+#[thrust_macros::requires(0 <= start && start <= end && end <= s.len())]
+#[thrust_macros::ensures(
+    s.subsequence(start, end).len() == end - start
+        && ((start < end) ==> (s.subsequence(start, end)[0] == s[start]))
+        && ((start < end) ==> (
+            s.subsequence(start, end).concat(s.subsequence(start, end))[end - start] == s[start]
+        ))
+)]
+fn seq_subsequence(s: Seq<Int>, start: Int, end: Int) {
+    let _ = (s, start, end);
+}
+
+fn main() {}
diff --git a/tests/ui/pass/slice_first_mut.rs b/tests/ui/pass/slice_first_mut.rs
index 69c617ae..016bac39 100644
--- a/tests/ui/pass/slice_first_mut.rs
+++ b/tests/ui/pass/slice_first_mut.rs
@@ -4,7 +4,7 @@
 #[thrust::trusted]
 #[thrust_macros::requires(true)]
 #[thrust_macros::ensures(
-    (*result).1 > 0 && (*result).0[0] == 10
+    (*result).2 > 0 && (*result).0[(*result).1] == 10
 )]
 fn slice() -> &'static mut [i32] {
     unimplemented!()
diff --git a/tests/ui/pass/slice_index.rs b/tests/ui/pass/slice_index.rs
index cf425aa3..e7e7bdb2 100644
--- a/tests/ui/pass/slice_index.rs
+++ b/tests/ui/pass/slice_index.rs
@@ -4,9 +4,9 @@
 #[thrust::trusted]
 #[thrust_macros::requires(true)]
 #[thrust_macros::ensures(
-    result.1 == 2
-        && result.0[0] == 10
-        && result.0[1] == 20
+    result.2 == 2
+        && result.0[result.1] == 10
+        && result.0[result.1 + 1] == 20
 )]
 fn slice() -> &'static [i32] {
     unimplemented!()
diff --git a/tests/ui/pass/slice_index_mut.rs b/tests/ui/pass/slice_index_mut.rs
index 51ef5189..60a54ae6 100644
--- a/tests/ui/pass/slice_index_mut.rs
+++ b/tests/ui/pass/slice_index_mut.rs
@@ -4,7 +4,7 @@
 #[thrust::trusted]
 #[thrust_macros::requires(true)]
 #[thrust_macros::ensures(
-    (*result).1 > 1 && (*result).0[1] == 20
+    (*result).2 > 1 && (*result).0[(*result).1 + 1] == 20
 )]
 fn slice() -> &'static mut [i32] {
     unimplemented!()
diff --git a/tests/ui/pass/slice_last_mut.rs b/tests/ui/pass/slice_last_mut.rs
index df7ffa3a..6f297877 100644
--- a/tests/ui/pass/slice_last_mut.rs
+++ b/tests/ui/pass/slice_last_mut.rs
@@ -4,8 +4,8 @@
 #[thrust::trusted]
 #[thrust_macros::requires(true)]
 #[thrust_macros::ensures(
-    (*result).1 > 0
-        && (*result).0[(*result).1 - 1] == 30
+    (*result).2 > 0
+        && (*result).0[(*result).1 + (*result).2 - 1] == 30
 )]
 fn slice() -> &'static mut [i32] {
     unimplemented!()
diff --git a/tests/ui/pass/slice_methods.rs b/tests/ui/pass/slice_methods.rs
index 5962a63b..3f0fe5a6 100644
--- a/tests/ui/pass/slice_methods.rs
+++ b/tests/ui/pass/slice_methods.rs
@@ -4,11 +4,11 @@
 #[thrust::trusted]
 #[thrust_macros::requires(true)]
 #[thrust_macros::ensures(
-    result.1 == 4
-        && result.0[0] == 10
-        && result.0[1] == 20
-        && result.0[2] == 30
-        && result.0[3] == 40
+    result.2 == 4
+        && result.0[result.1] == 10
+        && result.0[result.1 + 1] == 20
+        && result.0[result.1 + 2] == 30
+        && result.0[result.1 + 3] == 40
 )]
 fn slice() -> &'static [i32] {
     unimplemented!()
diff --git a/tests/ui/pass/slice_methods_mut.rs b/tests/ui/pass/slice_methods_mut.rs
index b24db2a3..81a1e513 100644
--- a/tests/ui/pass/slice_methods_mut.rs
+++ b/tests/ui/pass/slice_methods_mut.rs
@@ -4,7 +4,7 @@
 #[thrust::trusted]
 #[thrust_macros::requires(true)]
 #[thrust_macros::ensures(
-    (*result).1 > 1 && (*result).0[1] == 20
+    (*result).2 > 1 && (*result).0[(*result).1 + 1] == 20
 )]
 fn slice() -> &'static mut [i32] {
     unimplemented!()
diff --git a/tests/ui/pass/slice_split_first_mut.rs b/tests/ui/pass/slice_split_first_mut.rs
new file mode 100644
index 00000000..b346585e
--- /dev/null
+++ b/tests/ui/pass/slice_split_first_mut.rs
@@ -0,0 +1,20 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off
+#[thrust::trusted]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(
+    (*result).2 == 2
+        && (*result).0[(*result).1] == 10
+        && (*result).0[(*result).1 + 1] == 20
+)]
+fn slice() -> &'static mut [i32] {
+    unimplemented!()
+}
+
+fn main() {
+    let slice = slice();
+    let (first, tail) = slice.split_first_mut().unwrap();
+    assert!(*first == 10);
+    assert!(tail.len() == 1);
+    assert!(*tail.first().unwrap() == 20);
+}