diff --git a/src/analyze/annot.rs b/src/analyze/annot.rs
index b246df43..57d50925 100644
--- a/src/analyze/annot.rs
+++ b/src/analyze/annot.rs
@@ -37,6 +37,14 @@ pub fn extern_spec_fn_path() -> [Symbol; 2] {
     [Symbol::intern("thrust"), Symbol::intern("extern_spec_fn")]
 }
 
+pub fn slice_len_path() -> [Symbol; 3] {
+    [
+        Symbol::intern("thrust"),
+        Symbol::intern("def"),
+        Symbol::intern("slice_len"),
+    ]
+}
+
 pub fn raw_command_path() -> [Symbol; 2] {
     [Symbol::intern("thrust"), Symbol::intern("raw_command")]
 }
@@ -177,6 +185,22 @@ pub fn seq_push_path() -> [Symbol; 3] {
     ]
 }
 
+pub fn seq_prepend_path() -> [Symbol; 3] {
+    [
+        Symbol::intern("thrust"),
+        Symbol::intern("def"),
+        Symbol::intern("seq_prepend"),
+    ]
+}
+
+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..48f9b145 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,47 @@ 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_prepend() {
+                        assert_eq!(args.len(), 1, "Seq::prepend 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 offset = t.clone().tuple_proj(1);
+                        let len = t.tuple_proj(2);
+                        let new_offset = offset.sub(chc::Term::int(1));
+                        let new_arr = arr.store(new_offset.clone(), v);
+                        let new_len = len.add(chc::Term::int(1));
+                        return FormulaOrTerm::Term(chc::Term::tuple(vec![
+                            new_arr, new_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 +725,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 +825,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 +836,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 6e5aecf2..1ecd17a4 100644
--- a/src/analyze/basic_block.rs
+++ b/src/analyze/basic_block.rs
@@ -1,13 +1,16 @@
 use std::borrow::Cow;
 use std::collections::HashMap;
 
-use rustc_hir::def::DefKind;
+use rustc_hir::def::{DefKind, Namespace};
+use rustc_hir::lang_items::LangItem;
 use rustc_index::IndexVec;
 use rustc_middle::mir::{
     self, BasicBlock, Body, Local, Operand, Rvalue, StatementKind, TerminatorKind,
 };
 use rustc_middle::ty::{self as mir_ty, TyCtxt};
 use rustc_span::def_id::{DefId, LocalDefId};
+use rustc_span::source_map::Spanned;
+use rustc_span::{sym, Symbol};
 
 use crate::analyze;
 use crate::chc;
@@ -24,6 +27,258 @@ mod drop_point;
 mod visitor;
 pub use drop_point::DropPoints;
 
+fn lang_item_method(tcx: TyCtxt<'_>, item: LangItem, name: Symbol) -> DefId {
+    let trait_id = tcx.lang_items().get(item).unwrap();
+    tcx.associated_items(trait_id)
+        .in_definition_order()
+        .find(|item| item.name() == name && item.namespace() == Namespace::ValueNS)
+        .unwrap()
+        .def_id
+}
+
+fn fn_operand<'tcx>(
+    tcx: TyCtxt<'tcx>,
+    def_id: DefId,
+    args: mir_ty::GenericArgsRef<'tcx>,
+    span: rustc_span::Span,
+) -> Operand<'tcx> {
+    Operand::Constant(Box::new(mir::ConstOperand {
+        span,
+        user_ty: None,
+        const_: mir::Const::Val(
+            mir::ConstValue::ZeroSized,
+            mir_ty::Ty::new_fn_def(tcx, def_id, args),
+        ),
+    }))
+}
+
+struct IndexedPlaceFinder<'a, 'tcx> {
+    body: &'a Body<'tcx>,
+    tcx: TyCtxt<'tcx>,
+    index: Local,
+    found: Option<(mir::Place<'tcx>, bool)>,
+}
+
+impl<'tcx> mir::visit::Visitor<'tcx> for IndexedPlaceFinder<'_, 'tcx> {
+    fn visit_place(
+        &mut self,
+        place: &mir::Place<'tcx>,
+        context: mir::visit::PlaceContext,
+        _location: mir::Location,
+    ) {
+        if self.found.is_some() {
+            return;
+        }
+        let Some(index_pos) = place
+            .projection
+            .iter()
+            .position(|elem| elem == mir::PlaceElem::Index(self.index))
+        else {
+            return;
+        };
+        let indexed = mir::Place {
+            local: place.local,
+            projection: self
+                .tcx
+                .mk_place_elems(&place.projection.as_slice()[..=index_pos]),
+        };
+        let base = mir::Place {
+            local: place.local,
+            projection: self
+                .tcx
+                .mk_place_elems(&place.projection.as_slice()[..index_pos]),
+        };
+        if matches!(
+            base.ty(&self.body.local_decls, self.tcx).ty.kind(),
+            mir_ty::TyKind::Slice(_)
+        ) {
+            self.found = Some((indexed, context.is_mutating_use()));
+        }
+    }
+}
+
+/// Reconstructs the trait call erased by MIR's first-class slice indexing operation.
+///
+/// A bounds check followed by `slice[index]` is changed into an `Index::index` or
+/// `IndexMut::index_mut` call whose returned reference replaces the indexed place. This keeps the
+/// analyzer independent of the model selected for slices: all semantics continue to come from the
+/// extern specs of those trait methods.
+pub fn lower_slice_indexing<'tcx>(tcx: TyCtxt<'tcx>, body: &mut Body<'tcx>) {
+    use mir::visit::Visitor as _;
+
+    for bb in body.basic_blocks.indices().collect::<Vec<_>>() {
+        let Some(terminator) = body.basic_blocks[bb].terminator.as_ref() else {
+            continue;
+        };
+        let TerminatorKind::Assert {
+            cond,
+            msg,
+            target,
+            unwind,
+            ..
+        } = &terminator.kind
+        else {
+            continue;
+        };
+        let mir::AssertMessage::BoundsCheck { len, index } = &**msg else {
+            continue;
+        };
+        let len = len.clone();
+        let index = index.clone();
+        let condition_local = cond
+            .place()
+            .filter(|place| place.projection.is_empty())
+            .map(|p| p.local);
+        let Some(index_place) = index.place() else {
+            continue;
+        };
+        if !index_place.projection.is_empty() {
+            continue;
+        }
+        let index_local = index_place.local;
+        let target = *target;
+        let unwind = *unwind;
+        let source_info = terminator.source_info;
+
+        let mut finder = IndexedPlaceFinder {
+            body,
+            tcx,
+            index: index_local,
+            found: None,
+        };
+        finder.visit_basic_block_data(target, &body.basic_blocks[target]);
+        let Some((indexed_place, mutable)) = finder.found else {
+            continue;
+        };
+
+        let mut base_projection = indexed_place.projection.as_slice().to_vec();
+        assert_eq!(
+            base_projection.pop(),
+            Some(mir::PlaceElem::Index(index_local))
+        );
+        assert_eq!(base_projection.pop(), Some(mir::PlaceElem::Deref));
+        let receiver = mir::Place {
+            local: indexed_place.local,
+            projection: tcx.mk_place_elems(&base_projection),
+        };
+        let receiver_ty = receiver.ty(&body.local_decls, tcx).ty;
+        let mir_ty::TyKind::Ref(_, slice_ty, receiver_mutability) = receiver_ty.kind() else {
+            continue;
+        };
+        let mir_ty::TyKind::Slice(elem_ty) = slice_ty.kind() else {
+            continue;
+        };
+        if mutable && !receiver_mutability.is_mut() {
+            continue;
+        }
+
+        let ref_mutability = if mutable {
+            mir_ty::Mutability::Mut
+        } else {
+            mir_ty::Mutability::Not
+        };
+        let region = mir_ty::Region::new_from_kind(tcx, mir_ty::RegionKind::ReErased);
+        let result_ty = mir_ty::Ty::new_ref(tcx, region, *elem_ty, ref_mutability);
+        let result_local = body
+            .local_decls
+            .push(mir::LocalDecl::new(result_ty, source_info.span).immutable());
+
+        let replacement = tcx.mk_place_deref(result_local.into());
+        let mut replacer =
+            analyze::ReplacePlacesVisitor::with_replacement(tcx, indexed_place, replacement);
+        let target_data = &mut body.basic_blocks.as_mut()[target];
+        for statement in &mut target_data.statements {
+            replacer.visit_statement(statement);
+        }
+        if let Some(terminator) = &mut target_data.terminator {
+            replacer.visit_terminator(terminator);
+        }
+
+        let (lang_item, method_name) = if mutable {
+            (LangItem::IndexMut, sym::index_mut)
+        } else {
+            (LangItem::Index, sym::index)
+        };
+        let method = lang_item_method(tcx, lang_item, method_name);
+        let args = tcx.mk_args(&[(*slice_ty).into(), tcx.types.usize.into()]);
+        let func = fn_operand(tcx, method, args, source_info.span);
+        let receiver = if !mutable && receiver_mutability.is_mut() {
+            let immut_receiver_ty =
+                mir_ty::Ty::new_ref(tcx, region, *slice_ty, mir_ty::Mutability::Not);
+            let immut_receiver = body
+                .local_decls
+                .push(mir::LocalDecl::new(immut_receiver_ty, source_info.span).immutable());
+            body.basic_blocks.as_mut()[bb]
+                .statements
+                .push(mir::Statement::new(
+                    source_info,
+                    StatementKind::Assign(Box::new((
+                        immut_receiver.into(),
+                        Rvalue::Ref(
+                            region,
+                            mir::BorrowKind::Shared,
+                            tcx.mk_place_deref(receiver),
+                        ),
+                    ))),
+                ));
+            Operand::Copy(immut_receiver.into())
+        } else if mutable {
+            Operand::Move(receiver)
+        } else {
+            Operand::Copy(receiver)
+        };
+        let call_args = vec![
+            Spanned {
+                node: receiver,
+                span: source_info.span,
+            },
+            Spanned {
+                node: index,
+                span: source_info.span,
+            },
+        ];
+
+        let mut lowered_locals: Vec<_> = condition_local.into_iter().collect();
+        if let Some(len_place) = len.place().filter(|place| place.projection.is_empty()) {
+            lowered_locals.push(len_place.local);
+            for statement in &body.basic_blocks[bb].statements {
+                let Some((lhs, Rvalue::UnaryOp(mir::UnOp::PtrMetadata, operand))) =
+                    statement.kind.as_assign()
+                else {
+                    continue;
+                };
+                if lhs.local == len_place.local {
+                    if let Some(raw_place) =
+                        operand.place().filter(|place| place.projection.is_empty())
+                    {
+                        lowered_locals.push(raw_place.local);
+                    }
+                }
+            }
+        }
+        for statement in &mut body.basic_blocks.as_mut()[bb].statements {
+            let Some((lhs, _)) = statement.kind.as_assign() else {
+                continue;
+            };
+            if lowered_locals.contains(&lhs.local) {
+                statement.kind = StatementKind::Nop;
+            }
+        }
+        body.basic_blocks.as_mut()[bb].terminator = Some(mir::Terminator {
+            source_info,
+            kind: TerminatorKind::Call {
+                func,
+                args: call_args.into_boxed_slice(),
+                destination: result_local.into(),
+                target: Some(target),
+                unwind,
+                call_source: mir::CallSource::Normal,
+                fn_span: source_info.span,
+            },
+        });
+    }
+}
+
 /// Whether a basic block needs a precondition of its own, rather than
 /// inheriting its predecessor's outgoing env state.
 ///
@@ -1012,6 +1267,47 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
         // definition
         assert!(lhs.projection.is_empty());
 
+        if let Rvalue::UnaryOp(mir::UnOp::PtrMetadata, operand) = rvalue {
+            let operand_mir_ty = operand.ty(&self.local_decls, self.tcx);
+            let mir_ty::TyKind::Ref(_, slice_ty, mutability) = operand_mir_ty.kind() else {
+                unimplemented!("PtrMetadata for {operand_mir_ty:?}")
+            };
+            let mir_ty::TyKind::Slice(elem_ty) = slice_ty.kind() else {
+                unimplemented!("PtrMetadata for {operand_mir_ty:?}")
+            };
+            let slice_len = self
+                .ctx
+                .def_ids()
+                .slice_len()
+                .expect("slice len extern spec was not registered");
+            let args = self.tcx.mk_args(&[(*elem_ty).into()]);
+            let func = fn_operand(self.tcx, slice_len, args, rustc_span::DUMMY_SP);
+            let operand = if mutability.is_mut() {
+                let place = operand
+                    .place()
+                    .expect("mutable slice metadata operand must be a place");
+                let region = mir_ty::Region::new_from_kind(self.tcx, mir_ty::RegionKind::ReErased);
+                let ty = mir_ty::Ty::new_ref(self.tcx, region, *slice_ty, mir_ty::Mutability::Not);
+                let local = self
+                    .local_decls
+                    .push(mir::LocalDecl::new(ty, rustc_span::DUMMY_SP).immutable());
+                let rty = self.immut_borrow_place(self.tcx.mk_place_deref(place));
+                self.bind_local(local, rty);
+                Operand::Copy(local.into())
+            } else {
+                operand.clone()
+            };
+            let decl = self.local_decls[lhs.local].clone();
+            let rty = self
+                .type_builder
+                .for_template(&mut self.ctx)
+                .with_scope(&self.env)
+                .build_refined(decl.ty);
+            self.type_call(func, [operand], &rty);
+            self.bind_local(lhs.local, rty);
+            return;
+        }
+
         if let Rvalue::Ref(_, mir::BorrowKind::Mut { .. }, referent) = rvalue {
             // mutable borrow
             let rty = self.mutable_borrow(stmt_idx, *referent);
diff --git a/src/analyze/crate_.rs b/src/analyze/crate_.rs
index 74198f18..3f399bbc 100644
--- a/src/analyze/crate_.rs
+++ b/src/analyze/crate_.rs
@@ -70,6 +70,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
     #[tracing::instrument(skip(self), fields(def_id = %self.tcx.def_path_str(local_def_id)))]
     fn refine_fn_def(&mut self, local_def_id: LocalDefId) {
         let sig = self.ctx.fn_sig(local_def_id.to_def_id());
+        let def_ids = self.ctx.def_ids();
 
         let mut analyzer = self.ctx.local_def_analyzer(local_def_id);
 
@@ -118,6 +119,14 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
         } else {
             local_def_id.to_def_id()
         };
+        if self
+            .tcx
+            .get_attrs_by_path(local_def_id.to_def_id(), &analyze::annot::slice_len_path())
+            .next()
+            .is_some()
+        {
+            def_ids.register_slice_len(target_def_id);
+        }
 
         use mir_ty::TypeVisitableExt as _;
         if sig.has_param() {
diff --git a/src/analyze/did_cache.rs b/src/analyze/did_cache.rs
index 4dbcf110..e59c1570 100644
--- a/src/analyze/did_cache.rs
+++ b/src/analyze/did_cache.rs
@@ -29,7 +29,10 @@ struct DefIds {
     seq_singleton: OnceCell<Option<DefId>>,
     seq_len: OnceCell<Option<DefId>>,
     seq_push: OnceCell<Option<DefId>>,
+    seq_prepend: OnceCell<Option<DefId>>,
+    seq_subsequence: OnceCell<Option<DefId>>,
     seq_concat: OnceCell<Option<DefId>>,
+    slice_len: OnceCell<DefId>,
 
     exists: OnceCell<Option<DefId>>,
     forall: OnceCell<Option<DefId>>,
@@ -221,6 +224,20 @@ impl<'tcx> DefIdCache<'tcx> {
             .get_or_init(|| self.annotated_def(&crate::analyze::annot::seq_push_path()))
     }
 
+    pub fn seq_prepend(&self) -> Option<DefId> {
+        *self
+            .def_ids
+            .seq_prepend
+            .get_or_init(|| self.annotated_def(&crate::analyze::annot::seq_prepend_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
@@ -228,6 +245,17 @@ impl<'tcx> DefIdCache<'tcx> {
             .get_or_init(|| self.annotated_def(&crate::analyze::annot::seq_concat_path()))
     }
 
+    pub fn register_slice_len(&self, def_id: DefId) {
+        self.def_ids
+            .slice_len
+            .set(def_id)
+            .expect("slice len DefId registered twice");
+    }
+
+    pub fn slice_len(&self) -> Option<DefId> {
+        self.def_ids.slice_len.get().copied()
+    }
+
     pub fn exists(&self) -> Option<DefId> {
         *self
             .def_ids
diff --git a/src/analyze/local_def.rs b/src/analyze/local_def.rs
index 3938e071..a8944f4e 100644
--- a/src/analyze/local_def.rs
+++ b/src/analyze/local_def.rs
@@ -1310,6 +1310,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
         let _guard = span.enter();
 
         self.unelaborate_derefs();
+        analyze::basic_block::lower_slice_indexing(self.tcx, &mut self.body);
         self.reassign_local_mutabilities();
         self.refine_basic_blocks();
         self.analyze_basic_blocks(expected);
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 9d1a883f..08514f69 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,20 @@ mod thrust_models {
                 unimplemented!()
             }
 
+            #[allow(dead_code)]
+            #[thrust::def::seq_prepend]
+            #[thrust::ignored]
+            pub fn prepend(self, _x: T) -> Self {
+                unimplemented!()
+            }
+
+            #[allow(dead_code)]
+            #[thrust::def::seq_subsequence]
+            #[thrust::ignored]
+            pub fn subsequence(self, _start: Int, _end: Int) -> Self {
+                unimplemented!()
+            }
+
             #[allow(dead_code)]
             #[thrust::def::seq_concat]
             #[thrust::ignored]
@@ -364,6 +378,10 @@ mod thrust_models {
         type Ty = model::Seq<<T as Model>::Ty>;
     }
 
+    impl<T> Model for [T] where T: Model {
+        type Ty = model::Seq<<T as Model>::Ty>;
+    }
+
     impl<T> Model for Option<T> where T: Model {
         type Ty = Option<<T as Model>::Ty>;
     }
@@ -707,14 +725,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
 {
@@ -723,24 +741,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
@@ -750,7 +768,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)
 }
@@ -758,14 +778,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
         )
     )
@@ -776,7 +796,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)
 }
@@ -785,10 +805,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
     )
 )]
@@ -796,6 +816,156 @@ fn _extern_spec_vec_truncate<T>(vec: &mut Vec<T>, len: usize) where T: thrust_mo
     Vec::truncate(vec, len)
 }
 
+#[thrust::extern_spec_fn]
+#[thrust::def::slice_len]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(result == slice.2)]
+fn _extern_spec_slice_len<T>(slice: &[T]) -> usize
+    where T: thrust_models::Model, T::Ty: PartialEq
+{
+    <[T]>::len(slice)
+}
+
+#[thrust::extern_spec_fn]
+#[thrust_macros::requires(true)]
+#[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
+{
+    <[T]>::is_empty(slice)
+}
+
+#[thrust::extern_spec_fn]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(
+    (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
+{
+    <[T]>::get(slice, index)
+}
+
+#[thrust::extern_spec_fn]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(
+    (index < (*slice).2
+        && result == Some(thrust_models::model::Mut::new(
+            (*slice).0[(*slice).1 + index],
+            (!slice).0[(*slice).1 + index],
+        ))
+        && !slice == thrust_models::model::Seq(
+            (*slice).0.store((*slice).1 + index, (!slice).0[(*slice).1 + index]),
+            (*slice).1,
+            (*slice).2,
+        )
+    )
+    || ((*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
+{
+    <[T]>::get_mut(slice, index)
+}
+
+#[thrust::extern_spec_fn]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(
+    (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
+{
+    <[T]>::first(slice)
+}
+
+#[thrust::extern_spec_fn]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(
+    ((*slice).2 > 0
+        && result == Some(thrust_models::model::Mut::new(
+            (*slice).0[(*slice).1],
+            (!slice).0[(*slice).1],
+        ))
+        && !slice == thrust_models::model::Seq(
+            (*slice).0.store((*slice).1, (!slice).0[(*slice).1]),
+            (*slice).1,
+            (*slice).2,
+        )
+    )
+    || ((*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
+{
+    <[T]>::first_mut(slice)
+}
+
+#[thrust::extern_spec_fn]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(
+    (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
+{
+    <[T]>::last(slice)
+}
+
+#[thrust::extern_spec_fn]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(
+    ((*slice).2 > 0
+        && result == Some(thrust_models::model::Mut::new(
+            (*slice).0[(*slice).1 + (*slice).2 - 1],
+            (!slice).0[(*slice).1 + (*slice).2 - 1],
+        ))
+        && !slice == thrust_models::model::Seq(
+            (*slice).0.store(
+                (*slice).1 + (*slice).2 - 1,
+                (!slice).0[(*slice).1 + (*slice).2 - 1],
+            ),
+            (*slice).1,
+            (*slice).2,
+        )
+    )
+    || ((*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
+{
+    <[T]>::last_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
+{
+    <[T] as std::ops::Index<usize>>::index(slice, index)
+}
+
+#[thrust::extern_spec_fn]
+#[thrust_macros::requires(index < (*slice).2)]
+#[thrust_macros::ensures(
+    *result == (*slice).0[(*slice).1 + index] &&
+    !result == (!slice).0[(!slice).1 + index] &&
+    !slice == thrust_models::model::Seq(
+        (*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
+    where T: thrust_models::Model, T::Ty: PartialEq
+{
+    <[T] as std::ops::IndexMut<usize>>::index_mut(slice, index)
+}
+
 // TODO: The following specs of some trait methods are too restrictive; we should allow for a
 //       per-impl spec once we can describe the spec of blanket impls.
 
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
new file mode 100644
index 00000000..31acda48
--- /dev/null
+++ b/tests/ui/fail/slice_first_mut.rs
@@ -0,0 +1,18 @@
+//@error-in-other-file: Unsat
+//@compile-flags: -C debug-assertions=off
+//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper
+
+#[thrust::trusted]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(
+    (*result).2 > 0 && (*result).0[(*result).1] == 10
+)]
+fn slice() -> &'static mut [i32] {
+    unimplemented!()
+}
+
+fn main() {
+    let slice = slice();
+    *slice.first_mut().unwrap() = 11;
+    assert!(*slice.first().unwrap() == 12);
+}
diff --git a/tests/ui/fail/slice_index.rs b/tests/ui/fail/slice_index.rs
new file mode 100644
index 00000000..92b2632e
--- /dev/null
+++ b/tests/ui/fail/slice_index.rs
@@ -0,0 +1,16 @@
+//@error-in-other-file: Unsat
+//@compile-flags: -C debug-assertions=off
+//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper
+
+#[thrust::trusted]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(result.2 == 1 && result.0[result.1] == 10)]
+fn slice() -> &'static [i32] {
+    unimplemented!()
+}
+
+fn main() {
+    let slice = slice();
+    assert!(slice.len() == 1);
+    let _ = slice[1];
+}
diff --git a/tests/ui/fail/slice_index_mut.rs b/tests/ui/fail/slice_index_mut.rs
new file mode 100644
index 00000000..25016b99
--- /dev/null
+++ b/tests/ui/fail/slice_index_mut.rs
@@ -0,0 +1,18 @@
+//@error-in-other-file: Unsat
+//@compile-flags: -C debug-assertions=off
+//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper
+
+#[thrust::trusted]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(
+    (*result).2 > 1 && (*result).0[(*result).1 + 1] == 20
+)]
+fn slice() -> &'static mut [i32] {
+    unimplemented!()
+}
+
+fn main() {
+    let slice = slice();
+    slice[1] = 21;
+    assert!(slice[1] == 22);
+}
diff --git a/tests/ui/fail/slice_index_mut_trait.rs b/tests/ui/fail/slice_index_mut_trait.rs
new file mode 100644
index 00000000..3ece123d
--- /dev/null
+++ b/tests/ui/fail/slice_index_mut_trait.rs
@@ -0,0 +1,18 @@
+//@error-in-other-file: Unsat
+//@compile-flags: -C debug-assertions=off
+//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper
+
+#[thrust::trusted]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(
+    (*result).2 > 2 && (*result).0[(*result).1 + 2] == 40
+)]
+fn slice() -> &'static mut [i32] {
+    unimplemented!()
+}
+
+fn main() {
+    let slice = slice();
+    *<[i32] as std::ops::IndexMut<usize>>::index_mut(slice, 2) = 41;
+    assert!(*<[i32] as std::ops::Index<usize>>::index(slice, 2) == 42);
+}
diff --git a/tests/ui/fail/slice_last_mut.rs b/tests/ui/fail/slice_last_mut.rs
new file mode 100644
index 00000000..1c1ebf24
--- /dev/null
+++ b/tests/ui/fail/slice_last_mut.rs
@@ -0,0 +1,19 @@
+//@error-in-other-file: Unsat
+//@compile-flags: -C debug-assertions=off
+//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper
+
+#[thrust::trusted]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(
+    (*result).2 > 0
+        && (*result).0[(*result).1 + (*result).2 - 1] == 30
+)]
+fn slice() -> &'static mut [i32] {
+    unimplemented!()
+}
+
+fn main() {
+    let slice = slice();
+    *slice.last_mut().unwrap() = 31;
+    assert!(*slice.last().unwrap() == 32);
+}
diff --git a/tests/ui/fail/slice_methods.rs b/tests/ui/fail/slice_methods.rs
new file mode 100644
index 00000000..b7ef45e0
--- /dev/null
+++ b/tests/ui/fail/slice_methods.rs
@@ -0,0 +1,19 @@
+//@error-in-other-file: Unsat
+//@compile-flags: -C debug-assertions=off
+//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper
+
+#[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 [i32] {
+    unimplemented!()
+}
+
+fn main() {
+    let slice = slice();
+    assert!(*slice.last().unwrap() == 10);
+}
diff --git a/tests/ui/fail/slice_methods_mut.rs b/tests/ui/fail/slice_methods_mut.rs
new file mode 100644
index 00000000..652dfd19
--- /dev/null
+++ b/tests/ui/fail/slice_methods_mut.rs
@@ -0,0 +1,18 @@
+//@error-in-other-file: Unsat
+//@compile-flags: -C debug-assertions=off
+//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper
+
+#[thrust::trusted]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(
+    (*result).2 > 1 && (*result).0[(*result).1 + 1] == 20
+)]
+fn slice() -> &'static mut [i32] {
+    unimplemented!()
+}
+
+fn main() {
+    let slice = slice();
+    *slice.get_mut(1).unwrap() = 21;
+    assert!(*slice.get(1).unwrap() == 22);
+}
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..b68c2163
--- /dev/null
+++ b/tests/ui/pass/seq_subsequence.rs
@@ -0,0 +1,22 @@
+//@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]))
+        && s.prepend(x).len() == s.len() + 1
+        && s.prepend(x)[0] == x
+        && ((0 < s.len()) ==> (s.prepend(x)[1] == s[0]))
+        && ((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, x: Int) {
+    let _ = (s, start, end, x);
+}
+
+fn main() {}
diff --git a/tests/ui/pass/slice_first_mut.rs b/tests/ui/pass/slice_first_mut.rs
new file mode 100644
index 00000000..d5666b67
--- /dev/null
+++ b/tests/ui/pass/slice_first_mut.rs
@@ -0,0 +1,18 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off
+//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper
+
+#[thrust::trusted]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(
+    (*result).2 > 0 && (*result).0[(*result).1] == 10
+)]
+fn slice() -> &'static mut [i32] {
+    unimplemented!()
+}
+
+fn main() {
+    let slice = slice();
+    *slice.first_mut().unwrap() = 11;
+    assert!(*slice.first().unwrap() == 11);
+}
diff --git a/tests/ui/pass/slice_index.rs b/tests/ui/pass/slice_index.rs
new file mode 100644
index 00000000..b8cb54e3
--- /dev/null
+++ b/tests/ui/pass/slice_index.rs
@@ -0,0 +1,21 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off
+//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper
+
+#[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 [i32] {
+    unimplemented!()
+}
+
+fn main() {
+    let slice = slice();
+    assert!(slice.len() == 2);
+    assert!(slice[0] == 10);
+    assert!(slice[1] == 20);
+}
diff --git a/tests/ui/pass/slice_index_mut.rs b/tests/ui/pass/slice_index_mut.rs
new file mode 100644
index 00000000..f806f237
--- /dev/null
+++ b/tests/ui/pass/slice_index_mut.rs
@@ -0,0 +1,19 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off
+//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper
+
+#[thrust::trusted]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(
+    (*result).2 > 1 && (*result).0[(*result).1 + 1] == 20
+)]
+fn slice() -> &'static mut [i32] {
+    unimplemented!()
+}
+
+fn main() {
+    let slice = slice();
+    assert!(slice.len() > 1);
+    slice[1] = 21;
+    assert!(slice[1] == 21);
+}
diff --git a/tests/ui/pass/slice_index_mut_trait.rs b/tests/ui/pass/slice_index_mut_trait.rs
new file mode 100644
index 00000000..daf6a40e
--- /dev/null
+++ b/tests/ui/pass/slice_index_mut_trait.rs
@@ -0,0 +1,18 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off
+//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper
+
+#[thrust::trusted]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(
+    (*result).2 > 2 && (*result).0[(*result).1 + 2] == 40
+)]
+fn slice() -> &'static mut [i32] {
+    unimplemented!()
+}
+
+fn main() {
+    let slice = slice();
+    *<[i32] as std::ops::IndexMut<usize>>::index_mut(slice, 2) = 41;
+    assert!(*<[i32] as std::ops::Index<usize>>::index(slice, 2) == 41);
+}
diff --git a/tests/ui/pass/slice_last_mut.rs b/tests/ui/pass/slice_last_mut.rs
new file mode 100644
index 00000000..1dfe7d31
--- /dev/null
+++ b/tests/ui/pass/slice_last_mut.rs
@@ -0,0 +1,19 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off
+//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper
+
+#[thrust::trusted]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(
+    (*result).2 > 0
+        && (*result).0[(*result).1 + (*result).2 - 1] == 30
+)]
+fn slice() -> &'static mut [i32] {
+    unimplemented!()
+}
+
+fn main() {
+    let slice = slice();
+    *slice.last_mut().unwrap() = 31;
+    assert!(*slice.last().unwrap() == 31);
+}
diff --git a/tests/ui/pass/slice_methods.rs b/tests/ui/pass/slice_methods.rs
new file mode 100644
index 00000000..d06260e3
--- /dev/null
+++ b/tests/ui/pass/slice_methods.rs
@@ -0,0 +1,26 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off
+//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper
+
+#[thrust::trusted]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(
+    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!()
+}
+
+fn main() {
+    let slice = slice();
+    assert!(!slice.is_empty());
+    assert!(*slice.first().unwrap() == 10);
+    assert!(*slice.get(1).unwrap() == 20);
+    assert!(*<[i32] as std::ops::Index<usize>>::index(slice, 2) == 30);
+    assert!(*slice.last().unwrap() == 40);
+    assert!(slice.get(4).is_none());
+}
diff --git a/tests/ui/pass/slice_methods_mut.rs b/tests/ui/pass/slice_methods_mut.rs
new file mode 100644
index 00000000..ea6197a4
--- /dev/null
+++ b/tests/ui/pass/slice_methods_mut.rs
@@ -0,0 +1,18 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off
+//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper
+
+#[thrust::trusted]
+#[thrust_macros::requires(true)]
+#[thrust_macros::ensures(
+    (*result).2 > 1 && (*result).0[(*result).1 + 1] == 20
+)]
+fn slice() -> &'static mut [i32] {
+    unimplemented!()
+}
+
+fn main() {
+    let slice = slice();
+    *slice.get_mut(1).unwrap() = 21;
+    assert!(*slice.get(1).unwrap() == 21);
+}