diff --git a/src/analyze/annot_fn.rs b/src/analyze/annot_fn.rs
index aa733308..9cb6bc91 100644
--- a/src/analyze/annot_fn.rs
+++ b/src/analyze/annot_fn.rs
@@ -670,12 +670,15 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> {
                 let is_seq = array_ty
                     .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)
+                if is_seq {
+                    // Indexing a sequence is offset-aware: `s[i]` reads the underlying array at
+                    // `offset + i`.
+                    let offset = array_term.clone().tuple_proj(1);
+                    let array_inner = array_term.tuple_proj(0);
+                    FormulaOrTerm::Term(array_inner.select(offset.add(index_term)))
                 } else {
-                    array_term
-                };
-                FormulaOrTerm::Term(array_inner.select(index_term))
+                    FormulaOrTerm::Term(array_term.select(index_term))
+                }
             }
             ExprKind::MethodCall(method, receiver, args, _) => {
                 if let Some(def_id) = self.typeck.type_dependent_def_id(hir.hir_id) {
@@ -697,28 +700,34 @@ 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_concat() {
                         assert_eq!(args.len(), 1, "Seq::concat takes exactly 1 argument");
                         let elem_sort = self.adt_arg_type_at(receiver, 0).to_sort();
                         let t = self.to_term(receiver);
                         let other = self.to_term(&args[0]);
-                        let a_len = t.clone().tuple_proj(1);
-                        let b_len = other.clone().tuple_proj(1);
+                        let a_offset = t.clone().tuple_proj(1);
+                        let a_len = t.clone().tuple_proj(2);
+                        let b_len = other.clone().tuple_proj(2);
                         let new_arr = chc::Term::seq_concat(elem_sort, t, other);
                         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)
@@ -801,6 +810,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() {
@@ -811,6 +821,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/basic_block.rs b/src/analyze/basic_block.rs
index 4ed04196..a82505ab 100644
--- a/src/analyze/basic_block.rs
+++ b/src/analyze/basic_block.rs
@@ -544,8 +544,9 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
             Rvalue::Aggregate(kind, fields) => {
                 match *kind {
                     mir::AggregateKind::Array(mir_elem_ty) => {
-                        // Build Seq<T> = (Box<Array<Int,T>>, Box<Int>) from array literal elements,
-                        // pinning each element at its index via store folds.
+                        // Build Seq<T> = (Box<Array<Int,T>>, Box<Int>, Box<Int>) from array literal
+                        // elements, pinning each element at its index via store folds. The offset
+                        // of a freshly built array is 0.
                         //
                         // TODO: Stop embedding knowledge of `<[T; N] as Model>::Ty` in the analyzer
                         let mut builder = PlaceTypeBuilder::default();
@@ -561,12 +562,18 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
                             rty::ArrayType::new(rty::Type::int(), elem_ty).into(),
                             arr_term,
                         );
+                        let offset_pty =
+                            PlaceType::with_ty_and_term(rty::Type::int(), chc::Term::int(0));
                         let size = fields.len();
                         let size_pty = PlaceType::with_ty_and_term(
                             rty::Type::int(),
                             chc::Term::int(size as i64),
                         );
-                        PlaceType::tuple(vec![arr_pty.boxed(), size_pty.boxed()])
+                        PlaceType::tuple(vec![
+                            arr_pty.boxed(),
+                            offset_pty.boxed(),
+                            size_pty.boxed(),
+                        ])
                     }
                     mir::AggregateKind::Adt(did, variant_idx, args, _, _)
                         if self.tcx.def_kind(did) == DefKind::Enum =>
diff --git a/src/chc.rs b/src/chc.rs
index f98a3111..39f5e1d1 100644
--- a/src/chc.rs
+++ b/src/chc.rs
@@ -871,15 +871,19 @@ 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(seq_concat(s, t), i)
-        //   ↦ ite(i < len(s), select(array(s), i), select(array(t), i - len(s)))`
-        // where `s`/`t` are `(array, length)` tuples.
+        // `select(seq_concat(s, t), i)`
+        //   ↦ ite(i < offset(s) + length(s),
+        //         select(array(s), i),
+        //         select(array(t), offset(t) + i - (offset(s) + length(s))))`
+        // where `s`/`t` are `(array, offset, length)` tuples and `i` is an absolute index into
+        // the concatenated array (which reuses `s`'s offset).
         if let Term::SeqConcat(_, t) = self {
             let SeqConcatTerm { seq1, seq2 } = *t;
-            let len1 = seq1.clone().tuple_proj(1);
-            let cond = index.clone().lt(len1.clone());
+            let split = seq1.clone().tuple_proj(1).add(seq1.clone().tuple_proj(2));
+            let offset2 = seq2.clone().tuple_proj(1);
+            let cond = index.clone().lt(split.clone());
             let then_ = seq1.tuple_proj(0).select(index.clone());
-            let else_ = seq2.tuple_proj(0).select(index.sub(len1));
+            let else_ = seq2.tuple_proj(0).select(offset2.add(index.sub(split)));
             return Term::ite(cond, then_, else_);
         }
         Term::App(Function::SELECT, vec![self, index])
diff --git a/src/chc/format_context.rs b/src/chc/format_context.rs
index 86752f78..cf61ab06 100644
--- a/src/chc/format_context.rs
+++ b/src/chc/format_context.rs
@@ -283,13 +283,14 @@ impl FormatContext {
                 _ => None,
             })
             .collect();
-        // The `seq_concat` definitions operate on `(array, length)` sequence tuples, so
-        // make sure that tuple datatype is declared for every element sort we emit one for, even
-        // when no sequence value of that element sort otherwise appears in the system.
+        // The `seq_concat` definitions operate on `(array, offset, length)` sequence
+        // tuples, so make sure that tuple datatype is declared for every element sort we emit one
+        // for, even when no sequence value of that element sort otherwise appears in the system.
         for elem in &int_array_elem_sorts {
             sorts.insert(chc::Sort::tuple(vec![
                 chc::Sort::array(chc::Sort::int(), elem.clone()),
                 chc::Sort::int(),
+                chc::Sort::int(),
             ]));
         }
         let datatypes: Vec<_> = sorts
diff --git a/src/chc/smtlib2.rs b/src/chc/smtlib2.rs
index c95bf75a..aa33ccbe 100644
--- a/src/chc/smtlib2.rs
+++ b/src/chc/smtlib2.rs
@@ -641,25 +641,29 @@ impl<'a> std::fmt::Display for System<'a> {
         for elem in self.ctx.int_array_elem_sorts() {
             let name = self.ctx.seq_concat(elem);
             let elem_ty = self.ctx.fmt_sort(elem);
-            // The sequences are passed as `(array, length)` tuples; project their fields
-            // instead of taking the array and length as separate parameters.
+            // The sequences are passed as `(array, offset, length)` tuples; project their fields
+            // instead of taking the array and length as separate parameters. The concatenated
+            // array keeps `s`'s offset: `s`'s elements stay in place and `t`'s elements are
+            // appended right after them.
             let seq_fields = [
                 chc::Sort::array(chc::Sort::int(), elem.clone()),
                 chc::Sort::int(),
+                chc::Sort::int(),
             ];
             let seq_ty = self.ctx.fmt_sort(&chc::Sort::tuple(seq_fields.to_vec()));
             let ctor = self.ctx.tuple_ctor(&seq_fields);
             let array = self.ctx.tuple_proj(&seq_fields, 0);
-            let len = self.ctx.tuple_proj(&seq_fields, 1);
+            let off = self.ctx.tuple_proj(&seq_fields, 1);
+            let len = self.ctx.tuple_proj(&seq_fields, 2);
             writeln!(
                 f,
                 "(define-fun-rec {name} \
                   ((s {seq_ty}) (t {seq_ty})) \
                   (Array Int {elem_ty}) \
                   (ite (<= ({len} t) 0) ({array} s) \
-                       (store ({name} s ({ctor} ({array} t) (- ({len} t) 1))) \
-                              (+ ({len} s) (- ({len} t) 1)) \
-                              (select ({array} t) (- ({len} t) 1)))))\n",
+                       (store ({name} s ({ctor} ({array} t) ({off} t) (- ({len} t) 1))) \
+                              (+ ({off} s) ({len} s) (- ({len} t) 1)) \
+                              (select ({array} t) (+ ({off} t) (- ({len} t) 1))))))\n",
             )?;
         }
 
diff --git a/std.rs b/std.rs
index 4d6cd8b6..62d29442 100644
--- a/std.rs
+++ b/std.rs
@@ -190,6 +190,7 @@ mod thrust_models {
         #[thrust::def::seq_model]
         pub struct Seq<T: ?Sized> {
             pub array: Array<Int, T>,
+            pub offset: Int,
             pub length: Int,
         }
 
@@ -719,14 +720,14 @@ fn _extern_spec_i32_is_negative(x: i32) -> bool {
 
 #[thrust::extern_spec_fn]
 #[thrust_macros::requires(true)]
-#[thrust_macros::ensures(result.length == 0)]
+#[thrust_macros::ensures(result.offset == 0 && result.length == 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 { array: (*vec).array.store((*vec).length, elem), length: (*vec).length + 1 })]
+#[thrust_macros::ensures(!vec == thrust_models::model::Seq { array: (*vec).array.store((*vec).offset + (*vec).length, elem), offset: (*vec).offset, length: (*vec).length + 1 })]
 fn _extern_spec_vec_push<T>(vec: &mut Vec<T>, elem: T)
     where T: thrust_models::Model, T::Ty: PartialEq
 {
@@ -742,7 +743,7 @@ fn _extern_spec_vec_len<T>(vec: &Vec<T>) -> usize where T: thrust_models::Model,
 
 #[thrust::extern_spec_fn]
 #[thrust_macros::requires(index < (*vec).length)]
-#[thrust_macros::ensures(*result == (*vec).array[index])]
+#[thrust_macros::ensures(*result == (*vec).array[(*vec).offset + 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)
 }
@@ -750,9 +751,9 @@ fn _extern_spec_vec_index<T>(vec: &Vec<T>, index: usize) -> &T where T: thrust_m
 #[thrust::extern_spec_fn]
 #[thrust_macros::requires(index < (*vec).length)]
 #[thrust_macros::ensures(
-    *result == (*vec).array[index] &&
-    !result == (!vec).array[index] &&
-    !vec == thrust_models::model::Seq { array: (*vec).array.store(index, !result), length: (*vec).length }
+    *result == (*vec).array[(*vec).offset + index] &&
+    !result == (!vec).array[(!vec).offset + index] &&
+    !vec == thrust_models::model::Seq { array: (*vec).array.store((*vec).offset + index, !result), offset: (*vec).offset, length: (*vec).length }
 )]
 fn _extern_spec_vec_index_mut<T>(vec: &mut Vec<T>, index: usize) -> &mut T
     where T: thrust_models::Model, T::Ty: PartialEq
@@ -762,7 +763,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).length == 0)]
+#[thrust_macros::ensures(
+    (!vec).array == (*vec).array && (!vec).offset == (*vec).offset && (!vec).length == 0
+)]
 fn _extern_spec_vec_clear<T>(vec: &mut Vec<T>) where T: thrust_models::Model, T::Ty: PartialEq {
     Vec::clear(vec)
 }
@@ -770,11 +773,11 @@ 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).array == (*vec).array && (
+    (!vec).array == (*vec).array && (!vec).offset == (*vec).offset && (
         (
             (*vec).length > 0 &&
             (!vec).length == (*vec).length - 1 &&
-            result == Some((*vec).array[(*vec).length - 1])
+            result == Some((*vec).array[(*vec).offset + (*vec).length - 1])
         ) || (
             (*vec).length == 0 &&
             (!vec).length == 0 &&
@@ -798,7 +801,7 @@ fn _extern_spec_vec_is_empty<T>(vec: &Vec<T>) -> bool where T: thrust_models::Mo
 #[thrust_macros::ensures(
     (
         (*vec).length > len &&
-        !vec == thrust_models::model::Seq { array: (*vec).array, length: len }
+        !vec == thrust_models::model::Seq { array: (*vec).array, offset: (*vec).offset, length: len }
     ) || (
         (*vec).length <= len &&
         !vec == *vec
@@ -856,7 +859,7 @@ fn _extern_spec_slice_is_empty<T>(slice: &[T]) -> bool
 #[thrust::extern_spec_fn]
 #[thrust_macros::requires(true)]
 #[thrust_macros::ensures(
-    (index < (*slice).length && result == Some(&(*slice).array[index]))
+    (index < (*slice).length && result == Some(&(*slice).array[(*slice).offset + index]))
     || ((*slice).length <= index && result == None)
 )]
 fn _extern_spec_slice_get<T>(slice: &[T], index: usize) -> Option<&T>
@@ -870,11 +873,12 @@ fn _extern_spec_slice_get<T>(slice: &[T], index: usize) -> Option<&T>
 #[thrust_macros::ensures(
     (index < (*slice).length
         && result == Some(thrust_models::model::Mut::new(
-            (*slice).array[index],
-            (!slice).array[index],
+            (*slice).array[(*slice).offset + index],
+            (!slice).array[(*slice).offset + index],
         ))
         && !slice == thrust_models::model::Seq {
-            array: (*slice).array.store(index, (!slice).array[index]),
+            array: (*slice).array.store((*slice).offset + index, (!slice).array[(*slice).offset + index]),
+            offset: (*slice).offset,
             length: (*slice).length,
         }
     )
@@ -889,7 +893,7 @@ 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).length > 0 && result == Some(&(*slice).array[0]))
+    ((*slice).length > 0 && result == Some(&(*slice).array[(*slice).offset]))
     || ((*slice).length == 0 && result == None)
 )]
 fn _extern_spec_slice_first<T>(slice: &[T]) -> Option<&T>
@@ -903,11 +907,12 @@ fn _extern_spec_slice_first<T>(slice: &[T]) -> Option<&T>
 #[thrust_macros::ensures(
     ((*slice).length > 0
         && result == Some(thrust_models::model::Mut::new(
-            (*slice).array[0],
-            (!slice).array[0],
+            (*slice).array[(*slice).offset],
+            (!slice).array[(*slice).offset],
         ))
         && !slice == thrust_models::model::Seq {
-            array: (*slice).array.store(0, (!slice).array[0]),
+            array: (*slice).array.store((*slice).offset, (!slice).array[(*slice).offset]),
+            offset: (*slice).offset,
             length: (*slice).length,
         }
     )
@@ -922,7 +927,7 @@ 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).length > 0 && result == Some(&(*slice).array[(*slice).length - 1]))
+    ((*slice).length > 0 && result == Some(&(*slice).array[(*slice).offset + (*slice).length - 1]))
     || ((*slice).length == 0 && result == None)
 )]
 fn _extern_spec_slice_last<T>(slice: &[T]) -> Option<&T>
@@ -936,14 +941,15 @@ fn _extern_spec_slice_last<T>(slice: &[T]) -> Option<&T>
 #[thrust_macros::ensures(
     ((*slice).length > 0
         && result == Some(thrust_models::model::Mut::new(
-            (*slice).array[(*slice).length - 1],
-            (!slice).array[(*slice).length - 1],
+            (*slice).array[(*slice).offset + (*slice).length - 1],
+            (!slice).array[(*slice).offset + (*slice).length - 1],
         ))
         && !slice == thrust_models::model::Seq {
             array: (*slice).array.store(
-                (*slice).length - 1,
-                (!slice).array[(*slice).length - 1],
+                (*slice).offset + (*slice).length - 1,
+                (!slice).array[(*slice).offset + (*slice).length - 1],
             ),
+            offset: (*slice).offset,
             length: (*slice).length,
         }
     )
@@ -960,7 +966,7 @@ fn _extern_spec_slice_last_mut<T>(slice: &mut [T]) -> Option<&mut T>
 
 #[thrust::extern_spec_fn]
 #[thrust_macros::requires(index < (*slice).length)]
-#[thrust_macros::ensures(*result == (*slice).array[index])]
+#[thrust_macros::ensures(*result == (*slice).array[(*slice).offset + index])]
 fn _extern_spec_slice_index<T>(slice: &[T], index: usize) -> &T
     where T: thrust_models::Model, T::Ty: PartialEq
 {
@@ -970,10 +976,11 @@ fn _extern_spec_slice_index<T>(slice: &[T], index: usize) -> &T
 #[thrust::extern_spec_fn]
 #[thrust_macros::requires(index < (*slice).length)]
 #[thrust_macros::ensures(
-    *result == (*slice).array[index] &&
-    !result == (!slice).array[index] &&
+    *result == (*slice).array[(*slice).offset + index] &&
+    !result == (!slice).array[(!slice).offset + index] &&
     !slice == thrust_models::model::Seq {
-        array: (*slice).array.store(index, !result),
+        array: (*slice).array.store((*slice).offset + index, !result),
+        offset: (*slice).offset,
         length: (*slice).length,
     }
 )]
diff --git a/tests/ui/fail/seq_specs_vec_build.rs b/tests/ui/fail/seq_specs_vec_build.rs
index 097e9b02..4dd0c7f0 100644
--- a/tests/ui/fail/seq_specs_vec_build.rs
+++ b/tests/ui/fail/seq_specs_vec_build.rs
@@ -7,10 +7,10 @@ use thrust_models::model::Seq;
 #[thrust_macros::requires(true)]
 #[thrust_macros::ensures(
     result.length == Seq::empty().push(10).push(20).push(30).len()
-        && result.array[0] == Seq::empty().push(10).push(20).push(30)[0]
-        && result.array[1] == Seq::empty().push(10).push(20).push(30)[1]
+        && result.array[result.offset] == Seq::empty().push(10).push(20).push(30)[0]
+        && result.array[result.offset + 1] == Seq::empty().push(10).push(20).push(30)[1]
         // wrong: last element should be 30, not 99
-        && result.array[2] == Seq::empty().push(10).push(20).push(99)[2]
+        && result.array[result.offset + 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/slice_first_mut.rs b/tests/ui/fail/slice_first_mut.rs
index 7800f2c8..114bb4d6 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).length > 0 && (*result).array[0] == 10
+    (*result).length > 0 && (*result).array[(*result).offset] == 10
 )]
 fn slice() -> &'static mut [i32] {
     unimplemented!()
diff --git a/tests/ui/fail/slice_index.rs b/tests/ui/fail/slice_index.rs
index c5c937d3..f8053c89 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).length == 1 && (*result).array[0] == 10)]
+#[thrust_macros::ensures((*result).length == 1 && (*result).array[(*result).offset] == 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 95dc7064..e31f9c97 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).length > 1 && (*result).array[1] == 20
+    (*result).length > 1 && (*result).array[(*result).offset + 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 10bcedfb..51a8b436 100644
--- a/tests/ui/fail/slice_last_mut.rs
+++ b/tests/ui/fail/slice_last_mut.rs
@@ -5,7 +5,7 @@
 #[thrust_macros::requires(true)]
 #[thrust_macros::ensures(
     (*result).length > 0
-        && (*result).array[(*result).length - 1] == 30
+        && (*result).array[(*result).offset + (*result).length - 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 fb57d55e..7dd0a843 100644
--- a/tests/ui/fail/slice_methods.rs
+++ b/tests/ui/fail/slice_methods.rs
@@ -5,8 +5,8 @@
 #[thrust_macros::requires(true)]
 #[thrust_macros::ensures(
     (*result).length == 2
-        && (*result).array[0] == 10
-        && (*result).array[1] == 20
+        && (*result).array[(*result).offset] == 10
+        && (*result).array[(*result).offset + 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 a01f3ecb..c637bf67 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).length > 1 && (*result).array[1] == 20
+    (*result).length > 1 && (*result).array[(*result).offset + 1] == 20
 )]
 fn slice() -> &'static mut [i32] {
     unimplemented!()
diff --git a/tests/ui/pass/seq_specs_vec_build.rs b/tests/ui/pass/seq_specs_vec_build.rs
index 70f1d667..f301712e 100644
--- a/tests/ui/pass/seq_specs_vec_build.rs
+++ b/tests/ui/pass/seq_specs_vec_build.rs
@@ -7,9 +7,9 @@ use thrust_models::model::Seq;
 #[thrust_macros::requires(true)]
 #[thrust_macros::ensures(
     result.length == Seq::empty().push(10).push(20).push(30).len()
-        && result.array[0] == Seq::empty().push(10).push(20).push(30)[0]
-        && result.array[1] == Seq::empty().push(10).push(20).push(30)[1]
-        && result.array[2] == Seq::empty().push(10).push(20).push(30)[2]
+        && result.array[result.offset] == Seq::empty().push(10).push(20).push(30)[0]
+        && result.array[result.offset + 1] == Seq::empty().push(10).push(20).push(30)[1]
+        && result.array[result.offset + 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/slice_first_mut.rs b/tests/ui/pass/slice_first_mut.rs
index 24ea5d93..b4a3f545 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).length > 0 && (*result).array[0] == 10
+    (*result).length > 0 && (*result).array[(*result).offset] == 10
 )]
 fn slice() -> &'static mut [i32] {
     unimplemented!()
diff --git a/tests/ui/pass/slice_index.rs b/tests/ui/pass/slice_index.rs
index 1e044954..c7583513 100644
--- a/tests/ui/pass/slice_index.rs
+++ b/tests/ui/pass/slice_index.rs
@@ -5,8 +5,8 @@
 #[thrust_macros::requires(true)]
 #[thrust_macros::ensures(
     (*result).length == 2
-        && (*result).array[0] == 10
-        && (*result).array[1] == 20
+        && (*result).array[(*result).offset] == 10
+        && (*result).array[(*result).offset + 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 c84f1a5e..6fa265c4 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).length > 1 && (*result).array[1] == 20
+    (*result).length > 1 && (*result).array[(*result).offset + 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 92f94287..448985ce 100644
--- a/tests/ui/pass/slice_last_mut.rs
+++ b/tests/ui/pass/slice_last_mut.rs
@@ -5,7 +5,7 @@
 #[thrust_macros::requires(true)]
 #[thrust_macros::ensures(
     (*result).length > 0
-        && (*result).array[(*result).length - 1] == 30
+        && (*result).array[(*result).offset + (*result).length - 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 70671165..881cbef6 100644
--- a/tests/ui/pass/slice_methods.rs
+++ b/tests/ui/pass/slice_methods.rs
@@ -5,10 +5,10 @@
 #[thrust_macros::requires(true)]
 #[thrust_macros::ensures(
     (*result).length == 4
-        && (*result).array[0] == 10
-        && (*result).array[1] == 20
-        && (*result).array[2] == 30
-        && (*result).array[3] == 40
+        && (*result).array[(*result).offset] == 10
+        && (*result).array[(*result).offset + 1] == 20
+        && (*result).array[(*result).offset + 2] == 30
+        && (*result).array[(*result).offset + 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 b7ef7bed..a392d0c8 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).length > 1 && (*result).array[1] == 20
+    (*result).length > 1 && (*result).array[(*result).offset + 1] == 20
 )]
 fn slice() -> &'static mut [i32] {
     unimplemented!()