diff --git a/crucible-mir-comp/src/Mir/Compositional/Builder.hs b/crucible-mir-comp/src/Mir/Compositional/Builder.hs
index 2a041b829f..e4d64c9ee9 100644
--- a/crucible-mir-comp/src/Mir/Compositional/Builder.hs
+++ b/crucible-mir-comp/src/Mir/Compositional/Builder.hs
@@ -636,6 +636,7 @@ substMethodSpec sc sm ms = do
         MS.SetupTerm tt -> MS.SetupTerm <$> goTypedTerm tt
         MS.SetupNull _ -> return sv
         MS.SetupStruct b svs -> MS.SetupStruct b <$> mapM goSetupValue svs
+        MS.SetupTuple b svs -> MS.SetupTuple b <$> mapM goSetupValue svs
         MS.SetupArray b svs -> MS.SetupArray b <$> mapM goSetupValue svs
         MS.SetupElem b sv idx -> MS.SetupElem b <$> goSetupValue sv <*> pure idx
         MS.SetupField b sv name -> MS.SetupField b <$> goSetupValue sv <*> pure name
@@ -677,14 +678,14 @@ regToSetup bak p eval shp rv = go shp rv
 
     go :: forall tp. TypeShape tp -> RegValue sym tp ->
         BuilderT sym t (OverrideSim p sym MIR rtp args ret) (MS.SetupValue MIR)
-    go (UnitShape _) () = return $ MS.SetupStruct () []
+    go (UnitShape _) () = return $ MS.SetupTuple () []
     go (PrimShape _ btpr) expr = do
         -- Record all vars used in `expr`
         cache <- use msbVisitCache
         visitExprVars cache expr $ \var -> do
             msbPrePost p . seVars %= Set.insert (Some var)
         liftIO $ MS.SetupTerm <$> eval btpr expr
-    go (TupleShape _ _ flds) rvs = MS.SetupStruct () <$> goFields flds rvs
+    go (TupleShape _ _ flds) rvs = MS.SetupTuple () <$> goFields flds rvs
     go (ArrayShape _ elemTy shp) vec = do
         svs <- case vec of
             MirVector_Vector v -> mapM (go shp) (toList v)
diff --git a/crucible-mir-comp/src/Mir/Compositional/Override.hs b/crucible-mir-comp/src/Mir/Compositional/Override.hs
index c89164423e..c0f5154d74 100644
--- a/crucible-mir-comp/src/Mir/Compositional/Override.hs
+++ b/crucible-mir-comp/src/Mir/Compositional/Override.hs
@@ -356,7 +356,7 @@ matchArg sym sc eval allocSpecs md shp rv sv = go shp rv sv
   where
     go :: forall tp. TypeShape tp -> RegValue sym tp -> MS.SetupValue MIR ->
         MirOverrideMatcher sym ()
-    go (UnitShape _) () (MS.SetupStruct () []) = return ()
+    go (UnitShape _) () (MS.SetupTuple () []) = return ()
     go (PrimShape _ _btpr) expr (MS.SetupTerm tt) = do
         loc <- use MS.osLocation
         exprTerm <- liftIO $ eval expr
@@ -390,7 +390,7 @@ matchArg sym sc eval allocSpecs md shp rv sv = go shp rv sv
                         ("mismatch on " ++ show (W4.exprType expr) ++ ": expected " ++
                             show (W4.printSymExpr val))
                         ""
-    go (TupleShape _ _ flds) rvs (MS.SetupStruct () svs) = goFields flds rvs svs
+    go (TupleShape _ _ flds) rvs (MS.SetupTuple () svs) = goFields flds rvs svs
     go (ArrayShape _ _ shp) vec (MS.SetupArray _ svs) = case vec of
         MirVector_Vector v -> zipWithM_ (\x y -> go shp x y) (toList v) svs
         MirVector_PartialVector pv -> forM_ (zip (toList pv) svs) $ \(p, sv) -> do
@@ -510,7 +510,7 @@ setupToReg :: forall sym t st fs tp.
 setupToReg sym sc termSub regMap allocMap shp sv = go shp sv
   where
     go :: forall tp. TypeShape tp -> MS.SetupValue MIR -> IO (RegValue sym tp)
-    go (UnitShape _) (MS.SetupStruct _ []) = return ()
+    go (UnitShape _) (MS.SetupTuple _ []) = return ()
     go (PrimShape _ btpr) (MS.SetupTerm tt) = do
         term <- liftIO $ SAW.scInstantiateExt sc termSub $ SAW.ttTerm tt
         Some expr <- termToExpr sym sc regMap term
@@ -519,7 +519,7 @@ setupToReg sym sc termSub regMap allocMap shp sv = go shp sv
             Nothing -> error $ "setupToReg: expected " ++ show btpr ++ ", but got " ++
                 show (W4.exprType expr)
         return expr
-    go (TupleShape _ _ flds) (MS.SetupStruct _ svs) = goFields flds svs
+    go (TupleShape _ _ flds) (MS.SetupTuple _ svs) = goFields flds svs
     go (ArrayShape _ _ shp) (MS.SetupArray _ svs) = do
         rvs <- mapM (go shp) svs
         return $ MirVector_Vector $ V.fromList rvs
diff --git a/doc/manual/manual.md b/doc/manual/manual.md
index 02cec02a93..d15b7e17cd 100644
--- a/doc/manual/manual.md
+++ b/doc/manual/manual.md
@@ -2435,9 +2435,9 @@ The experimental MIR implementation also has a `mir_alloc` function, which
 behaves similarly to `llvm_alloc`. `mir_alloc` creates an immutable reference,
 but there is also a `mir_alloc_mut` function for creating a mutable reference:
 
-* `mir_alloc : MIRType -> MIRSetup SetupValue`
+* `mir_alloc : MIRType -> MIRSetup MIRValue`
 
-* `mir_alloc_mut : MIRType -> MIRSetup SetupValue`
+* `mir_alloc_mut : MIRType -> MIRSetup MIRValue`
 
 MIR tracks whether references are mutable or immutable at the type level, so it
 is important to use the right allocation command for a given reference type.
@@ -2538,7 +2538,7 @@ value.
 
 MIR verification has a single `mir_points_to` command:
 
-* `mir_points_to : SetupValue -> SetupValue -> MIRSetup ()`
+* `mir_points_to : MIRValue -> MIRValue -> MIRSetup ()`
 takes two `SetupValue` arguments, the first of which must be a reference,
 and states that the memory specified by that reference should contain the
 value given in the second argument (which may be any type of
@@ -2624,9 +2624,11 @@ specifies the name of an object field.
 In the experimental MIR verification implementation, the following functions
 construct compound values:
 
-* `mir_array_value : MIRType -> [SetupValue] -> SetupValue` constructs an array
+* `mir_array_value : MIRType -> [MIRValue] -> MIRValue` constructs an array
   of the given type whose elements consist of the given values. Supplying the
   element type is necessary to support length-0 arrays.
+* `mir_tuple_value : [MIRValue] -> MIRValue` construct a tuple with the given
+  list of values as elements.
 
 ### Bitfields
 
diff --git a/intTests/test_mir_verify_tuples/Makefile b/intTests/test_mir_verify_tuples/Makefile
new file mode 100644
index 0000000000..bc6297ae15
--- /dev/null
+++ b/intTests/test_mir_verify_tuples/Makefile
@@ -0,0 +1,13 @@
+all: test.linked-mir.json
+
+test.linked-mir.json: test.rs
+	saw-rustc $<
+	$(MAKE) remove-unused-build-artifacts
+
+.PHONY: remove-unused-build-artifacts
+remove-unused-build-artifacts:
+	rm -f test libtest.mir libtest.rlib
+
+.PHONY: clean
+clean: remove-unused-build-artifacts
+	rm -f test.linked-mir.json
diff --git a/intTests/test_mir_verify_tuples/test.linked-mir.json b/intTests/test_mir_verify_tuples/test.linked-mir.json
new file mode 100644
index 0000000000..34b9c9363c
--- /dev/null
+++ b/intTests/test_mir_verify_tuples/test.linked-mir.json
@@ -0,0 +1 @@
+{"fns":[{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::25602b11826e1882"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::u32"}},"pos":"test.rs:10:13: 10:16","rhs":{"kind":"Use","usevar":{"data":{"data":[{"kind":"Deref"},{"field":0,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::25602b11826e1882"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_3","ty":"ty::u32"}},"pos":"test.rs:11:13: 11:16","rhs":{"kind":"Use","usevar":{"data":{"data":[{"kind":"Deref"},{"field":1,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::25602b11826e1882"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::u32"}},"pos":"test.rs:12:11: 12:12","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_3","ty":"ty::u32"}},"kind":"Copy"}}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::u32"}},"kind":"Move"},{"data":{"rendered":{"kind":"uint","size":4,"val":"1"},"ty":"ty::u32"},"kind":"Constant"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},"bb1"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::f55acdef755f1aaa"},"kind":"Constant"},"kind":"Call","pos":"test.rs:12:11: 12:28"}},"blockid":"bb0"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[{"kind":"Deref"},{"field":0,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::25602b11826e1882"}},"pos":"test.rs:12:5: 12:28","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},"kind":"Move"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::u32"}},"pos":"test.rs:13:11: 13:12","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::u32"}},"kind":"Copy"}}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::u32"}},"kind":"Move"},{"data":{"rendered":{"kind":"uint","size":4,"val":"2"},"ty":"ty::u32"},"kind":"Constant"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::u32"}},"bb2"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::f55acdef755f1aaa"},"kind":"Constant"},"kind":"Call","pos":"test.rs:13:11: 13:28"}},"blockid":"bb1"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[{"kind":"Deref"},{"field":1,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::25602b11826e1882"}},"pos":"test.rs:13:5: 13:28","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::u32"}},"kind":"Move"}}}],"terminator":{"kind":"Return","pos":"test.rs:14:2: 14:2"}},"blockid":"bb2"}],"vars":[{"is_zst":true,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::e93222e871854c41"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_3","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::u32"}]},"name":"test/34c2a073::h","return_ty":"ty::Tuple::e93222e871854c41","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Tuple::f54c7b3282e27392"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"}},"pos":"test.rs:2:6: 2:9","rhs":{"kind":"Use","usevar":{"data":{"data":[{"field":1,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Tuple::f54c7b3282e27392"}},"kind":"Copy"}}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"}},"kind":"Move"},{"data":{"rendered":{"kind":"uint","size":4,"val":"1"},"ty":"ty::u32"},"kind":"Constant"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"}},"bb1"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::f55acdef755f1aaa"},"kind":"Constant"},"kind":"Call","pos":"test.rs:2:6: 2:25"}},"blockid":"bb0"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::u32"}},"pos":"test.rs:2:27: 2:30","rhs":{"kind":"Use","usevar":{"data":{"data":[{"field":0,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Tuple::f54c7b3282e27392"}},"kind":"Copy"}}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::u32"}},"kind":"Move"},{"data":{"rendered":{"kind":"uint","size":4,"val":"2"},"ty":"ty::u32"},"kind":"Constant"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},"bb2"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::f55acdef755f1aaa"},"kind":"Constant"},"kind":"Call","pos":"test.rs:2:27: 2:46"}},"blockid":"bb1"},{"block":{"data":[{"kind":"Deinit","pos":"test.rs:2:5: 2:47"},{"kind":"Assign","lhs":{"data":[{"field":0,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::f54c7b3282e27392"}},"pos":"test.rs:2:5: 2:47","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"}},"kind":"Move"}}},{"kind":"Assign","lhs":{"data":[{"field":1,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::f54c7b3282e27392"}},"pos":"test.rs:2:5: 2:47","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},"kind":"Move"}}}],"terminator":{"kind":"Return","pos":"test.rs:3:2: 3:2"}},"blockid":"bb2"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::f54c7b3282e27392"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::u32"}]},"name":"test/34c2a073::f","return_ty":"ty::Tuple::f54c7b3282e27392","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::22d6f3c23aaa2830"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"}},"pos":"test.rs:6:6: 6:9","rhs":{"kind":"Use","usevar":{"data":{"data":[{"kind":"Deref"},{"field":1,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::22d6f3c23aaa2830"}},"kind":"Copy"}}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"}},"kind":"Move"},{"data":{"rendered":{"kind":"uint","size":4,"val":"1"},"ty":"ty::u32"},"kind":"Constant"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"}},"bb1"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::f55acdef755f1aaa"},"kind":"Constant"},"kind":"Call","pos":"test.rs:6:6: 6:25"}},"blockid":"bb0"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::u32"}},"pos":"test.rs:6:27: 6:30","rhs":{"kind":"Use","usevar":{"data":{"data":[{"kind":"Deref"},{"field":0,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::22d6f3c23aaa2830"}},"kind":"Copy"}}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::u32"}},"kind":"Move"},{"data":{"rendered":{"kind":"uint","size":4,"val":"2"},"ty":"ty::u32"},"kind":"Constant"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},"bb2"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::f55acdef755f1aaa"},"kind":"Constant"},"kind":"Call","pos":"test.rs:6:27: 6:46"}},"blockid":"bb1"},{"block":{"data":[{"kind":"Deinit","pos":"test.rs:6:5: 6:47"},{"kind":"Assign","lhs":{"data":[{"field":0,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::f54c7b3282e27392"}},"pos":"test.rs:6:5: 6:47","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"}},"kind":"Move"}}},{"kind":"Assign","lhs":{"data":[{"field":1,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::f54c7b3282e27392"}},"pos":"test.rs:6:5: 6:47","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},"kind":"Move"}}}],"terminator":{"kind":"Return","pos":"test.rs:7:2: 7:2"}},"blockid":"bb2"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::f54c7b3282e27392"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::u32"}]},"name":"test/34c2a073::g","return_ty":"ty::Tuple::f54c7b3282e27392","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::u32"}],"body":{"blocks":[{"block":{"data":[{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1162:38: 1162:42 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1162:38: 1162:42 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u32"}},"kind":"Copy"}}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1162:44: 1162:47 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1162:44: 1162:47 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::u32"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1162:13: 1162:48 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101","rhs":{"L":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"}},"kind":"Move"},"R":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},"kind":"Move"},"kind":"BinaryOp","op":{"kind":"Add"}}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1162:47: 1162:48 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1162:47: 1162:48 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"}}],"terminator":{"kind":"Return","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1163:10: 1163:10 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}]},"name":"core/73237d41::num::{impl#9}::wrapping_add","return_ty":"ty::u32","spread_arg":null}],"adts":[],"statics":[],"vtables":[],"traits":[],"intrinsics":[{"inst":{"def_id":"test/34c2a073::h","kind":"Item","substs":[]},"name":"test/34c2a073::h"},{"inst":{"def_id":"test/34c2a073::f","kind":"Item","substs":[]},"name":"test/34c2a073::f"},{"inst":{"def_id":"test/34c2a073::g","kind":"Item","substs":[]},"name":"test/34c2a073::g"},{"inst":{"def_id":"core/73237d41::num::{impl#9}::wrapping_add","kind":"Item","substs":[]},"name":"core/73237d41::num::{impl#9}::wrapping_add"}],"tys":[{"name":"ty::u32","ty":{"kind":"Uint","uintkind":{"kind":"U32"}}},{"name":"ty::Tuple::f54c7b3282e27392","ty":{"kind":"Tuple","tys":["ty::u32","ty::u32"]}},{"name":"ty::Ref::25602b11826e1882","ty":{"kind":"Ref","mutability":{"kind":"Mut"},"ty":"ty::Tuple::f54c7b3282e27392"}},{"name":"ty::Tuple::e93222e871854c41","ty":{"kind":"Tuple","tys":[]}},{"name":"ty::FnDef::f55acdef755f1aaa","ty":{"defid":"core/73237d41::num::{impl#9}::wrapping_add","kind":"FnDef"}},{"name":"ty::Ref::22d6f3c23aaa2830","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::Tuple::f54c7b3282e27392"}}],"roots":["test/34c2a073::f","test/34c2a073::g","test/34c2a073::h"]}
\ No newline at end of file
diff --git a/intTests/test_mir_verify_tuples/test.rs b/intTests/test_mir_verify_tuples/test.rs
new file mode 100644
index 0000000000..85e0f888d2
--- /dev/null
+++ b/intTests/test_mir_verify_tuples/test.rs
@@ -0,0 +1,14 @@
+pub fn f(s: (u32, u32)) -> (u32, u32) {
+    (s.1.wrapping_add(1), s.0.wrapping_add(2))
+}
+
+pub fn g(s: &(u32, u32)) -> (u32, u32) {
+    (s.1.wrapping_add(1), s.0.wrapping_add(2))
+}
+
+pub fn h(s: &mut (u32, u32)) {
+    let x = s.0;
+    let y = s.1;
+    s.0 = y.wrapping_add(1);
+    s.1 = x.wrapping_add(2);
+}
diff --git a/intTests/test_mir_verify_tuples/test.saw b/intTests/test_mir_verify_tuples/test.saw
new file mode 100644
index 0000000000..fea2f8fe33
--- /dev/null
+++ b/intTests/test_mir_verify_tuples/test.saw
@@ -0,0 +1,44 @@
+enable_experimental;
+
+let f_spec = do {
+  x <- mir_fresh_var "x" mir_u32;
+  y <- mir_fresh_var "y" mir_u32;
+  let s = mir_tuple_value [mir_term x, mir_term y];
+
+  mir_execute_func [s];
+
+  let s' = mir_tuple_value [mir_term {{ y + 1 }}, mir_term {{ x + 2 }}];
+  mir_return s';
+};
+
+let g_spec = do {
+  s_ptr <- mir_alloc (mir_tuple [mir_u32, mir_u32]);
+  x <- mir_fresh_var "x" mir_u32;
+  y <- mir_fresh_var "y" mir_u32;
+  let s = mir_tuple_value [mir_term x, mir_term y];
+  mir_points_to s_ptr s;
+
+  mir_execute_func [s_ptr];
+
+  let s' = mir_tuple_value [mir_term {{ y + 1 }}, mir_term {{ x + 2 }}];
+  mir_return s';
+};
+
+let h_spec = do {
+  s_ptr <- mir_alloc_mut (mir_tuple [mir_u32, mir_u32]);
+  x <- mir_fresh_var "x" mir_u32;
+  y <- mir_fresh_var "y" mir_u32;
+  let s = mir_tuple_value [mir_term x, mir_term y];
+  mir_points_to s_ptr s;
+
+  mir_execute_func [s_ptr];
+
+  let s' = mir_tuple_value [mir_term {{ y + 1 }}, mir_term {{ x + 2 }}];
+  mir_points_to s_ptr s';
+};
+
+m <- mir_load_module "test.linked-mir.json";
+
+mir_verify m "test::f" [] false f_spec z3;
+mir_verify m "test::g" [] false g_spec z3;
+mir_verify m "test::h" [] false h_spec z3;
diff --git a/intTests/test_mir_verify_tuples/test.sh b/intTests/test_mir_verify_tuples/test.sh
new file mode 100755
index 0000000000..2315cc233c
--- /dev/null
+++ b/intTests/test_mir_verify_tuples/test.sh
@@ -0,0 +1,3 @@
+set -e
+
+$SAW test.saw
diff --git a/saw-remote-api/CHANGELOG.md b/saw-remote-api/CHANGELOG.md
index 90fc120547..56caf2597b 100644
--- a/saw-remote-api/CHANGELOG.md
+++ b/saw-remote-api/CHANGELOG.md
@@ -17,6 +17,9 @@
   LLVM verification, this field is optional. For MIR verification, this field
   is required if the `"elements"` value is empty and optional if the
   `"elements"` value is non-empty.
+* The old `"tuple"` `setup value` has been renamed to `"struct"`. This better
+  reflects its intended purpose of representing struct values. There is now a
+  new `"tuple"` `setup value` that is only used to represent MIR tuples.
 
 ## 1.0.0 -- 2023-06-26
 
diff --git a/saw-remote-api/python/CHANGELOG.md b/saw-remote-api/python/CHANGELOG.md
index 7aa8094779..8a4e41ef79 100644
--- a/saw-remote-api/python/CHANGELOG.md
+++ b/saw-remote-api/python/CHANGELOG.md
@@ -15,6 +15,8 @@
 * The `array()` function now takes an additional `element_type` argument, which
   defaults to `None`. If constructing a MIR array with no elements, then the
   `element_type` must be specified. Otherwise, this argument is optional.
+* Add a `tuple_value()` function for constructing MIR tuples. Using this
+  function with LLVM or JVM verification will raise an error.
 
 ## 1.0.1 -- YYYY-MM-DD
 
diff --git a/saw-remote-api/python/saw_client/crucible.py b/saw-remote-api/python/saw_client/crucible.py
index 04f1393969..eff2381868 100644
--- a/saw-remote-api/python/saw_client/crucible.py
+++ b/saw-remote-api/python/saw_client/crucible.py
@@ -144,6 +144,15 @@ def to_json(self) -> JSON:
 class StructVal(SetupVal):
     fields : List[SetupVal]
 
+    def __init__(self, fields : List[SetupVal]) -> None:
+        self.fields = fields
+
+    def to_json(self) -> JSON:
+        return {'setup value': 'struct', 'elements': [fld.to_json() for fld in self.fields]}
+
+class TupleVal(SetupVal):
+    fields : List[SetupVal]
+
     def __init__(self, fields : List[SetupVal]) -> None:
         self.fields = fields
 
@@ -727,3 +736,15 @@ def struct(*fields : SetupVal) -> SetupVal:
         if not isinstance(field, SetupVal):
             raise ValueError('struct expected a SetupVal, but got {field!r}')
     return StructVal(list(fields))
+
+def tuple_value(*fields : SetupVal) -> SetupVal:
+    """Returns a MIR tuple value with the given ``fields`` (i.e., a ``TupleVal``).
+    Using this function with LLVM or JVM verification will raise an error.
+
+    Unlike most other functions in saw_client.crucible, this has a ``_value``
+    suffix so as not to clash with the built-in ``tuple()`` function in Python.
+    """
+    for field in fields:
+        if not isinstance(field, SetupVal):
+            raise ValueError('tuple expected a SetupVal, but got {field!r}')
+    return TupleVal(list(fields))
diff --git a/saw-remote-api/python/tests/saw/test-files/mir_tuples.linked-mir.json b/saw-remote-api/python/tests/saw/test-files/mir_tuples.linked-mir.json
new file mode 100644
index 0000000000..5135f3cb32
--- /dev/null
+++ b/saw-remote-api/python/tests/saw/test-files/mir_tuples.linked-mir.json
@@ -0,0 +1 @@
+{"fns":[{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::25602b11826e1882"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::u32"}},"pos":"mir_tuples.rs:10:13: 10:16","rhs":{"kind":"Use","usevar":{"data":{"data":[{"kind":"Deref"},{"field":0,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::25602b11826e1882"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_3","ty":"ty::u32"}},"pos":"mir_tuples.rs:11:13: 11:16","rhs":{"kind":"Use","usevar":{"data":{"data":[{"kind":"Deref"},{"field":1,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::25602b11826e1882"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::u32"}},"pos":"mir_tuples.rs:12:11: 12:12","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_3","ty":"ty::u32"}},"kind":"Copy"}}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::u32"}},"kind":"Move"},{"data":{"rendered":{"kind":"uint","size":4,"val":"1"},"ty":"ty::u32"},"kind":"Constant"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},"bb1"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::f55acdef755f1aaa"},"kind":"Constant"},"kind":"Call","pos":"mir_tuples.rs:12:11: 12:28"}},"blockid":"bb0"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[{"kind":"Deref"},{"field":0,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::25602b11826e1882"}},"pos":"mir_tuples.rs:12:5: 12:28","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},"kind":"Move"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::u32"}},"pos":"mir_tuples.rs:13:11: 13:12","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::u32"}},"kind":"Copy"}}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::u32"}},"kind":"Move"},{"data":{"rendered":{"kind":"uint","size":4,"val":"2"},"ty":"ty::u32"},"kind":"Constant"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::u32"}},"bb2"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::f55acdef755f1aaa"},"kind":"Constant"},"kind":"Call","pos":"mir_tuples.rs:13:11: 13:28"}},"blockid":"bb1"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[{"kind":"Deref"},{"field":1,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::25602b11826e1882"}},"pos":"mir_tuples.rs:13:5: 13:28","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::u32"}},"kind":"Move"}}}],"terminator":{"kind":"Return","pos":"mir_tuples.rs:14:2: 14:2"}},"blockid":"bb2"}],"vars":[{"is_zst":true,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::e93222e871854c41"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_3","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::u32"}]},"name":"mir_tuples/93b69543::h","return_ty":"ty::Tuple::e93222e871854c41","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::22d6f3c23aaa2830"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"}},"pos":"mir_tuples.rs:6:6: 6:9","rhs":{"kind":"Use","usevar":{"data":{"data":[{"kind":"Deref"},{"field":1,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::22d6f3c23aaa2830"}},"kind":"Copy"}}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"}},"kind":"Move"},{"data":{"rendered":{"kind":"uint","size":4,"val":"1"},"ty":"ty::u32"},"kind":"Constant"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"}},"bb1"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::f55acdef755f1aaa"},"kind":"Constant"},"kind":"Call","pos":"mir_tuples.rs:6:6: 6:25"}},"blockid":"bb0"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::u32"}},"pos":"mir_tuples.rs:6:27: 6:30","rhs":{"kind":"Use","usevar":{"data":{"data":[{"kind":"Deref"},{"field":0,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::22d6f3c23aaa2830"}},"kind":"Copy"}}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::u32"}},"kind":"Move"},{"data":{"rendered":{"kind":"uint","size":4,"val":"2"},"ty":"ty::u32"},"kind":"Constant"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},"bb2"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::f55acdef755f1aaa"},"kind":"Constant"},"kind":"Call","pos":"mir_tuples.rs:6:27: 6:46"}},"blockid":"bb1"},{"block":{"data":[{"kind":"Deinit","pos":"mir_tuples.rs:6:5: 6:47"},{"kind":"Assign","lhs":{"data":[{"field":0,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::f54c7b3282e27392"}},"pos":"mir_tuples.rs:6:5: 6:47","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"}},"kind":"Move"}}},{"kind":"Assign","lhs":{"data":[{"field":1,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::f54c7b3282e27392"}},"pos":"mir_tuples.rs:6:5: 6:47","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},"kind":"Move"}}}],"terminator":{"kind":"Return","pos":"mir_tuples.rs:7:2: 7:2"}},"blockid":"bb2"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::f54c7b3282e27392"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::u32"}]},"name":"mir_tuples/93b69543::g","return_ty":"ty::Tuple::f54c7b3282e27392","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Tuple::f54c7b3282e27392"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"}},"pos":"mir_tuples.rs:2:6: 2:9","rhs":{"kind":"Use","usevar":{"data":{"data":[{"field":1,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Tuple::f54c7b3282e27392"}},"kind":"Copy"}}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"}},"kind":"Move"},{"data":{"rendered":{"kind":"uint","size":4,"val":"1"},"ty":"ty::u32"},"kind":"Constant"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"}},"bb1"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::f55acdef755f1aaa"},"kind":"Constant"},"kind":"Call","pos":"mir_tuples.rs:2:6: 2:25"}},"blockid":"bb0"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::u32"}},"pos":"mir_tuples.rs:2:27: 2:30","rhs":{"kind":"Use","usevar":{"data":{"data":[{"field":0,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Tuple::f54c7b3282e27392"}},"kind":"Copy"}}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::u32"}},"kind":"Move"},{"data":{"rendered":{"kind":"uint","size":4,"val":"2"},"ty":"ty::u32"},"kind":"Constant"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},"bb2"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::f55acdef755f1aaa"},"kind":"Constant"},"kind":"Call","pos":"mir_tuples.rs:2:27: 2:46"}},"blockid":"bb1"},{"block":{"data":[{"kind":"Deinit","pos":"mir_tuples.rs:2:5: 2:47"},{"kind":"Assign","lhs":{"data":[{"field":0,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::f54c7b3282e27392"}},"pos":"mir_tuples.rs:2:5: 2:47","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"}},"kind":"Move"}}},{"kind":"Assign","lhs":{"data":[{"field":1,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::f54c7b3282e27392"}},"pos":"mir_tuples.rs:2:5: 2:47","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},"kind":"Move"}}}],"terminator":{"kind":"Return","pos":"mir_tuples.rs:3:2: 3:2"}},"blockid":"bb2"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::f54c7b3282e27392"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::u32"}]},"name":"mir_tuples/93b69543::f","return_ty":"ty::Tuple::f54c7b3282e27392","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::u32"}],"body":{"blocks":[{"block":{"data":[{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1162:38: 1162:42 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1162:38: 1162:42 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u32"}},"kind":"Copy"}}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1162:44: 1162:47 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1162:44: 1162:47 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::u32"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1162:13: 1162:48 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101","rhs":{"L":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"}},"kind":"Move"},"R":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},"kind":"Move"},"kind":"BinaryOp","op":{"kind":"Add"}}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1162:47: 1162:48 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1162:47: 1162:48 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"}}],"terminator":{"kind":"Return","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1163:10: 1163:10 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}]},"name":"core/73237d41::num::{impl#9}::wrapping_add","return_ty":"ty::u32","spread_arg":null}],"adts":[],"statics":[],"vtables":[],"traits":[],"intrinsics":[{"inst":{"def_id":"mir_tuples/93b69543::h","kind":"Item","substs":[]},"name":"mir_tuples/93b69543::h"},{"inst":{"def_id":"mir_tuples/93b69543::g","kind":"Item","substs":[]},"name":"mir_tuples/93b69543::g"},{"inst":{"def_id":"mir_tuples/93b69543::f","kind":"Item","substs":[]},"name":"mir_tuples/93b69543::f"},{"inst":{"def_id":"core/73237d41::num::{impl#9}::wrapping_add","kind":"Item","substs":[]},"name":"core/73237d41::num::{impl#9}::wrapping_add"}],"tys":[{"name":"ty::u32","ty":{"kind":"Uint","uintkind":{"kind":"U32"}}},{"name":"ty::Tuple::f54c7b3282e27392","ty":{"kind":"Tuple","tys":["ty::u32","ty::u32"]}},{"name":"ty::Ref::25602b11826e1882","ty":{"kind":"Ref","mutability":{"kind":"Mut"},"ty":"ty::Tuple::f54c7b3282e27392"}},{"name":"ty::Tuple::e93222e871854c41","ty":{"kind":"Tuple","tys":[]}},{"name":"ty::FnDef::f55acdef755f1aaa","ty":{"defid":"core/73237d41::num::{impl#9}::wrapping_add","kind":"FnDef"}},{"name":"ty::Ref::22d6f3c23aaa2830","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::Tuple::f54c7b3282e27392"}}],"roots":["mir_tuples/93b69543::f","mir_tuples/93b69543::g","mir_tuples/93b69543::h"]}
\ No newline at end of file
diff --git a/saw-remote-api/python/tests/saw/test-files/mir_tuples.rs b/saw-remote-api/python/tests/saw/test-files/mir_tuples.rs
new file mode 100644
index 0000000000..85e0f888d2
--- /dev/null
+++ b/saw-remote-api/python/tests/saw/test-files/mir_tuples.rs
@@ -0,0 +1,14 @@
+pub fn f(s: (u32, u32)) -> (u32, u32) {
+    (s.1.wrapping_add(1), s.0.wrapping_add(2))
+}
+
+pub fn g(s: &(u32, u32)) -> (u32, u32) {
+    (s.1.wrapping_add(1), s.0.wrapping_add(2))
+}
+
+pub fn h(s: &mut (u32, u32)) {
+    let x = s.0;
+    let y = s.1;
+    s.0 = y.wrapping_add(1);
+    s.1 = x.wrapping_add(2);
+}
diff --git a/saw-remote-api/python/tests/saw/test_mir_tuples.py b/saw-remote-api/python/tests/saw/test_mir_tuples.py
new file mode 100644
index 0000000000..0f6c2c6134
--- /dev/null
+++ b/saw-remote-api/python/tests/saw/test_mir_tuples.py
@@ -0,0 +1,66 @@
+import unittest
+from pathlib import Path
+
+from saw_client import *
+from saw_client.crucible import cry_f, tuple_value
+from saw_client.mir import Contract, tuple_ty, u32, void
+
+
+class FContract(Contract):
+    def specification(self) -> None:
+        x = self.fresh_var(u32, "x")
+        y = self.fresh_var(u32, "y")
+        s = tuple_value(x, y)
+
+        self.execute_func(s)
+
+        s_ = tuple_value(cry_f('{y} + 1'), cry_f('{x} + 2'))
+        self.returns(s_)
+
+
+class GContract(Contract):
+    def specification(self) -> None:
+        x = self.fresh_var(u32, "x")
+        y = self.fresh_var(u32, "y")
+        s = tuple_value(x, y)
+        s_ptr = self.alloc(tuple_ty(u32, u32), points_to = s, read_only = True)
+
+        self.execute_func(s_ptr)
+
+        s_ = tuple_value(cry_f('{y} + 1'), cry_f('{x} + 2'))
+        self.returns(s_)
+
+
+class HContract(Contract):
+    def specification(self) -> None:
+        x = self.fresh_var(u32, "x")
+        y = self.fresh_var(u32, "y")
+        s = tuple_value(x, y)
+        s_ptr = self.alloc(tuple_ty(u32, u32), points_to = s)
+
+        self.execute_func(s_ptr)
+
+        s_ = tuple_value(cry_f('{y} + 1'), cry_f('{x} + 2'))
+        self.points_to(s_ptr, s_)
+        self.returns(void)
+
+
+class MIRStructsTest(unittest.TestCase):
+    def test_mir_points_to(self):
+        connect(reset_server=True)
+        if __name__ == "__main__": view(LogResults())
+        json_name = str(Path('tests', 'saw', 'test-files', 'mir_tuples.linked-mir.json'))
+        mod = mir_load_module(json_name)
+
+        f_result = mir_verify(mod, 'mir_tuples::f', FContract())
+        self.assertIs(f_result.is_success(), True)
+
+        g_result = mir_verify(mod, 'mir_tuples::g', GContract())
+        self.assertIs(g_result.is_success(), True)
+
+        h_result = mir_verify(mod, 'mir_tuples::h', HContract())
+        self.assertIs(h_result.is_success(), True)
+
+
+if __name__ == "__main__":
+    unittest.main()
diff --git a/saw-remote-api/src/SAWServer.hs b/saw-remote-api/src/SAWServer.hs
index a3200fb6de..67f0a6363d 100644
--- a/saw-remote-api/src/SAWServer.hs
+++ b/saw-remote-api/src/SAWServer.hs
@@ -107,6 +107,7 @@ instance Show SAWTask where
 data CrucibleSetupVal ty e
   = NullValue
   | ArrayValue (Maybe ty) [CrucibleSetupVal ty e]
+  | StructValue [CrucibleSetupVal ty e]
   | TupleValue [CrucibleSetupVal ty e]
   -- | RecordValue [(String, CrucibleSetupVal e)]
   | FieldLValue (CrucibleSetupVal ty e) String
diff --git a/saw-remote-api/src/SAWServer/Data/SetupValue.hs b/saw-remote-api/src/SAWServer/Data/SetupValue.hs
index c924fda107..0a3b0e6020 100644
--- a/saw-remote-api/src/SAWServer/Data/SetupValue.hs
+++ b/saw-remote-api/src/SAWServer/Data/SetupValue.hs
@@ -13,6 +13,7 @@ data SetupValTag
   | TagNullValue
   | TagCryptol
   | TagArrayValue
+  | TagStructValue
   | TagTupleValue
   | TagFieldLValue
   | TagCastLValue
@@ -29,6 +30,7 @@ instance FromJSON SetupValTag where
       "null" -> pure TagNullValue
       "Cryptol" -> pure TagCryptol
       "array" -> pure TagArrayValue
+      "struct" -> pure TagStructValue
       "tuple" -> pure TagTupleValue
       "field" -> pure TagFieldLValue
       "cast"  -> pure TagCastLValue
@@ -48,6 +50,7 @@ instance (FromJSON ty, FromJSON cryptolExpr) => FromJSON (CrucibleSetupVal ty cr
           TagNullValue -> pure NullValue
           TagCryptol -> CryptolExpr <$> o .: "expression"
           TagArrayValue -> ArrayValue <$> o .:? "element type" <*> o .: "elements"
+          TagStructValue -> StructValue <$> o .: "elements"
           TagTupleValue -> TupleValue <$> o .: "elements"
           TagFieldLValue -> FieldLValue <$> o .: "base" <*> o .: "field"
           TagCastLValue -> CastLValue <$> o .: "base" <*> o .: "type"
diff --git a/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs b/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs
index 925655df86..17b6313d4f 100644
--- a/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs
+++ b/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs
@@ -182,6 +182,8 @@ compileJVMContract fileReader bic cenv0 c =
       MS.SetupTerm <$> getTypedTerm cenv expr
     getSetupVal _ (ArrayValue _ _) =
       JVMSetupM $ fail "Array setup values unsupported in JVM API."
+    getSetupVal _ (StructValue _) =
+      JVMSetupM $ fail "Struct setup values unsupported in JVM API."
     getSetupVal _ (TupleValue _) =
       JVMSetupM $ fail "Tuple setup values unsupported in JVM API."
     getSetupVal _ (FieldLValue _ _) =
diff --git a/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs b/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs
index 4de73bf090..b0e4591b3c 100644
--- a/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs
+++ b/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs
@@ -179,9 +179,11 @@ compileLLVMContract fileReader bic ghostEnv cenv0 c =
     getSetupVal env (ArrayValue _ elts) =
       do elts' <- mapM (getSetupVal env) elts
          LLVMCrucibleSetupM $ return $ CMS.anySetupArray elts'
-    getSetupVal env (TupleValue elts) =
+    getSetupVal env (StructValue elts) =
       do elts' <- mapM (getSetupVal env) elts
          LLVMCrucibleSetupM $ return $ CMS.anySetupStruct False elts'
+    getSetupVal _ (TupleValue _) =
+      LLVMCrucibleSetupM $ fail "Tuple setup values unsupported in the LLVM API."
     getSetupVal env (FieldLValue base fld) =
       do base' <- getSetupVal env base
          LLVMCrucibleSetupM $ return $ CMS.anySetupField base' fld
diff --git a/saw-remote-api/src/SAWServer/MIRCrucibleSetup.hs b/saw-remote-api/src/SAWServer/MIRCrucibleSetup.hs
index 6c762033d1..682e484503 100644
--- a/saw-remote-api/src/SAWServer/MIRCrucibleSetup.hs
+++ b/saw-remote-api/src/SAWServer/MIRCrucibleSetup.hs
@@ -180,8 +180,11 @@ compileMIRContract fileReader bic cenv0 c =
                       Just eltTy -> pure $ mirType eltTy
                       Nothing -> MIRSetupM $ typeOfSetupValue cc allocEnv nameEnv elt'
              return $ MS.SetupArray ty' (elt':eltss')
-    getSetupVal _ (TupleValue _) =
-      MIRSetupM $ fail "Tuple setup values unsupported in the MIR API."
+    getSetupVal _ (StructValue _) =
+      MIRSetupM $ fail "Struct setup values unsupported in the MIR API."
+    getSetupVal env (TupleValue elems) = do
+      elems' <- mapM (getSetupVal env) elems
+      pure $ MS.SetupTuple () elems'
     getSetupVal _ (FieldLValue _ _) =
       MIRSetupM $ fail "Field l-values unsupported in the MIR API."
     getSetupVal _ (CastLValue _ _) =
diff --git a/src/SAWScript/Crucible/Common/MethodSpec.hs b/src/SAWScript/Crucible/Common/MethodSpec.hs
index 3df49ee9af..c9edcf7885 100644
--- a/src/SAWScript/Crucible/Common/MethodSpec.hs
+++ b/src/SAWScript/Crucible/Common/MethodSpec.hs
@@ -40,6 +40,7 @@ module SAWScript.Crucible.Common.MethodSpec
 
   , XSetupNull
   , XSetupStruct
+  , XSetupTuple
   , XSetupArray
   , XSetupElem
   , XSetupField
@@ -194,6 +195,14 @@ ppSetupValue setupval = case setupval of
         absurd empty
       (MIRExt, ()) ->
         ppSetupStructDefault vs
+  SetupTuple x vs ->
+    case (ext, x) of
+      (LLVMExt, empty) ->
+        absurd empty
+      (JVMExt, empty) ->
+        absurd empty
+      (MIRExt, ()) ->
+        PP.parens (commaList (map ppSetupValue vs))
   SetupArray _ vs  -> PP.brackets (commaList (map ppSetupValue vs))
   SetupElem _ v i  -> PP.parens (ppSetupValue v) PP.<> PP.pretty ("." ++ show i)
   SetupField _ v f -> PP.parens (ppSetupValue v) PP.<> PP.pretty ("." ++ f)
diff --git a/src/SAWScript/Crucible/Common/Setup/Value.hs b/src/SAWScript/Crucible/Common/Setup/Value.hs
index 12b69dfe14..b96b9b2ad8 100644
--- a/src/SAWScript/Crucible/Common/Setup/Value.hs
+++ b/src/SAWScript/Crucible/Common/Setup/Value.hs
@@ -38,6 +38,7 @@ module SAWScript.Crucible.Common.Setup.Value
 
   , XSetupNull
   , XSetupStruct
+  , XSetupTuple
   , XSetupArray
   , XSetupElem
   , XSetupField
@@ -121,6 +122,7 @@ type family ResolvedState ext :: Type
 
 type family XSetupNull ext
 type family XSetupStruct ext
+type family XSetupTuple ext
 type family XSetupArray ext
 type family XSetupElem ext
 type family XSetupField ext
@@ -137,6 +139,7 @@ data SetupValue ext where
   SetupTerm   :: TypedTerm -> SetupValue ext
   SetupNull   :: XSetupNull ext -> SetupValue ext
   SetupStruct :: XSetupStruct ext -> [SetupValue ext] -> SetupValue ext
+  SetupTuple  :: XSetupTuple ext -> [SetupValue ext] -> SetupValue ext
   SetupArray  :: XSetupArray ext -> [SetupValue ext] -> SetupValue ext
   SetupElem   :: XSetupElem ext -> SetupValue ext -> Int -> SetupValue ext
   SetupField  :: XSetupField ext -> SetupValue ext -> String -> SetupValue ext
@@ -157,6 +160,7 @@ data SetupValue ext where
 type SetupValueHas (c :: Type -> Constraint) ext =
   ( c (XSetupNull ext)
   , c (XSetupStruct ext)
+  , c (XSetupTuple ext)
   , c (XSetupArray ext)
   , c (XSetupElem ext)
   , c (XSetupField ext)
diff --git a/src/SAWScript/Crucible/JVM/Override.hs b/src/SAWScript/Crucible/JVM/Override.hs
index 41c316a317..5ba395b742 100644
--- a/src/SAWScript/Crucible/JVM/Override.hs
+++ b/src/SAWScript/Crucible/JVM/Override.hs
@@ -575,6 +575,7 @@ matchArg opts sc cc cs prepost md actual@(RVal ref) expectedTy setupval =
          addAssert p md (Crucible.SimError (cs ^. MS.csLoc) (Crucible.AssertFailureSimError ("null-equality " ++ MS.stateCond prepost) ""))
 
     MS.SetupGlobal empty _ -> absurd empty
+    MS.SetupTuple  empty _ -> absurd empty
 
     _ -> failure (cs ^. MS.csLoc) =<<
            mkStructuralMismatch opts cc sc cs actual setupval expectedTy
@@ -965,6 +966,7 @@ instantiateSetupValue sc s v =
     MS.SetupNull ()                   -> return v
     MS.SetupGlobal empty _            -> absurd empty
     MS.SetupStruct empty _            -> absurd empty
+    MS.SetupTuple empty _             -> absurd empty
     MS.SetupArray empty _             -> absurd empty
     MS.SetupElem empty _ _            -> absurd empty
     MS.SetupField empty _ _           -> absurd empty
diff --git a/src/SAWScript/Crucible/JVM/ResolveSetupValue.hs b/src/SAWScript/Crucible/JVM/ResolveSetupValue.hs
index 685cb42a98..6a3863685e 100644
--- a/src/SAWScript/Crucible/JVM/ResolveSetupValue.hs
+++ b/src/SAWScript/Crucible/JVM/ResolveSetupValue.hs
@@ -140,6 +140,7 @@ typeOfSetupValue _cc env _nameEnv val =
       return (J.ClassType (J.mkClassName "java/lang/Object"))
     MS.SetupGlobal empty _            -> absurd empty
     MS.SetupStruct empty _            -> absurd empty
+    MS.SetupTuple empty _             -> absurd empty
     MS.SetupArray empty _             -> absurd empty
     MS.SetupElem empty _ _            -> absurd empty
     MS.SetupField empty _ _           -> absurd empty
@@ -171,6 +172,7 @@ resolveSetupVal cc env _tyenv _nameEnv val =
       return (RVal (W4.maybePartExpr sym Nothing))
     MS.SetupGlobal empty _            -> absurd empty
     MS.SetupStruct empty _            -> absurd empty
+    MS.SetupTuple empty _             -> absurd empty
     MS.SetupArray empty _             -> absurd empty
     MS.SetupElem empty _ _            -> absurd empty
     MS.SetupField empty _ _           -> absurd empty
diff --git a/src/SAWScript/Crucible/JVM/Setup/Value.hs b/src/SAWScript/Crucible/JVM/Setup/Value.hs
index 04711a02e6..edf3c80581 100644
--- a/src/SAWScript/Crucible/JVM/Setup/Value.hs
+++ b/src/SAWScript/Crucible/JVM/Setup/Value.hs
@@ -78,6 +78,7 @@ import qualified SAWScript.Crucible.Common.Setup.Value as MS
 type instance MS.XSetupNull CJ.JVM = ()
 type instance MS.XSetupGlobal CJ.JVM = Void
 type instance MS.XSetupStruct CJ.JVM = Void
+type instance MS.XSetupTuple CJ.JVM = Void
 type instance MS.XSetupArray CJ.JVM = Void
 type instance MS.XSetupElem CJ.JVM = Void
 type instance MS.XSetupField CJ.JVM = Void
diff --git a/src/SAWScript/Crucible/LLVM/Override.hs b/src/SAWScript/Crucible/LLVM/Override.hs
index 3e4c838e6a..f9b258952e 100644
--- a/src/SAWScript/Crucible/LLVM/Override.hs
+++ b/src/SAWScript/Crucible/LLVM/Override.hs
@@ -80,6 +80,7 @@ import           Data.Set (Set)
 import qualified Data.Set as Set
 import           Data.Text (Text, pack)
 import qualified Data.Vector as V
+import           Data.Void (absurd)
 import           GHC.Generics (Generic)
 import           Numeric.Natural
 import qualified Prettyprinter as PP
@@ -1117,6 +1118,7 @@ matchPointsTos opts sc cc spec prepost = go False []
       case v of
         SetupVar i                 -> Set.singleton i
         SetupStruct _ xs           -> foldMap setupVars xs
+        SetupTuple empty _         -> absurd empty
         SetupArray _ xs            -> foldMap setupVars xs
         SetupElem _ x _            -> setupVars x
         SetupField _ x _           -> setupVars x
@@ -1298,6 +1300,9 @@ matchArg opts sc cc cs prepost md actual expectedTy expected =
                               (V.toList (Crucible.fiType <$> Crucible.siFields fields))
                               zs ]
 
+    (_, _, SetupTuple empty _) ->
+      absurd empty
+
     (Crucible.LLVMValInt blk off, _, SetupElem () v i) | Crucible.isPointerMemType expectedTy ->
       do let tyenv = MS.csAllocations cs
              nameEnv = MS.csTypeNames cs
@@ -2480,6 +2485,7 @@ instantiateSetupValue sc s v =
     SetupNull{}              -> return v
     SetupGlobal{}            -> return v
     SetupGlobalInitializer{} -> return v
+    SetupTuple empty _       -> absurd empty
   where
     doTerm (TypedTerm schema t) = TypedTerm schema <$> scInstantiateExt sc s t
 
diff --git a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs
index 59877cfa87..c021372a03 100644
--- a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs
+++ b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs
@@ -41,6 +41,7 @@ import Control.Monad.Except
 import Control.Monad.State
 import qualified Data.BitVector.Sized as BV
 import Data.Maybe (fromMaybe, fromJust)
+import Data.Void (absurd)
 
 import qualified Data.Dwarf as Dwarf
 import           Data.Map (Map)
@@ -450,6 +451,9 @@ typeOfSetupValue cc env nameEnv val =
          let si = Crucible.mkStructInfo dl packed memTys
          return (Crucible.StructType si)
 
+    SetupTuple empty _ ->
+      absurd empty
+
     SetupArray () [] -> throwError "typeOfSetupValue: invalid empty llvm_array_value"
     SetupArray () (v : vs) ->
       do memTy <- typeOfSetupValue cc env nameEnv v
@@ -626,6 +630,8 @@ resolveSetupVal cc mem env tyenv nameEnv val =
                    Crucible.Struct v -> v
                    _ -> error "impossible"
       return $ Crucible.LLVMValStruct (V.zip flds (V.fromList vals))
+    SetupTuple empty _ ->
+      absurd empty
     SetupArray () [] -> fail "resolveSetupVal: invalid empty array"
     SetupArray () vs -> do
       vals <- V.mapM (resolveSetupVal cc mem env tyenv nameEnv) (V.fromList vs)
diff --git a/src/SAWScript/Crucible/LLVM/Setup/Value.hs b/src/SAWScript/Crucible/LLVM/Setup/Value.hs
index 9416b96a7b..de4b0ff143 100644
--- a/src/SAWScript/Crucible/LLVM/Setup/Value.hs
+++ b/src/SAWScript/Crucible/LLVM/Setup/Value.hs
@@ -85,6 +85,7 @@ import           Data.Map ( Map )
 import qualified Data.Map as Map
 import qualified Data.Text as Text
 import           Data.Type.Equality (TestEquality(..))
+import           Data.Void (Void)
 import qualified Prettyprinter as PPL
 import qualified Text.LLVM.AST as L
 import qualified Text.LLVM.PP as L
@@ -119,6 +120,7 @@ data LLVM (arch :: CL.LLVMArch)
 type instance Setup.XSetupNull (LLVM _) = ()
 -- 'True' if this is an LLVM packed struct, 'False' otherwise.
 type instance Setup.XSetupStruct (LLVM _) = Bool
+type instance Setup.XSetupTuple (LLVM _) = Void
 type instance Setup.XSetupArray (LLVM _) = ()
 type instance Setup.XSetupElem (LLVM _) = ()
 type instance Setup.XSetupField (LLVM _) = ()
diff --git a/src/SAWScript/Crucible/MIR/Override.hs b/src/SAWScript/Crucible/MIR/Override.hs
index f0fc0fba28..c41e6955ac 100644
--- a/src/SAWScript/Crucible/MIR/Override.hs
+++ b/src/SAWScript/Crucible/MIR/Override.hs
@@ -182,6 +182,7 @@ instantiateSetupValue sc s v =
     MS.SetupNull empty                -> absurd empty
     MS.SetupGlobal empty _            -> absurd empty
     MS.SetupStruct _ _                -> return v
+    MS.SetupTuple x vs                -> MS.SetupTuple x <$> mapM (instantiateSetupValue sc s) vs
     MS.SetupArray elemTy vs           -> MS.SetupArray elemTy <$> mapM (instantiateSetupValue sc s) vs
     MS.SetupElem _ _ _                -> return v
     MS.SetupField _ _ _               -> return v
@@ -324,6 +325,21 @@ matchArg opts sc cc cs prepost md actual expectedTy expected =
              [ matchArg opts sc cc cs prepost md (MIRVal elemShp x) y z
              | (x, z) <- zip (V.toList xs'') zs ]
 
+    -- match the fields of a tuple point-wise
+    (MIRVal (TupleShape _ _ xsFldShps) xs, Mir.TyTuple ys, MS.SetupTuple () zs) ->
+      sequence_
+        [ case xFldShp of
+            ReqField shp ->
+              matchArg opts sc cc cs prepost md (MIRVal shp x) y z
+            OptField shp -> do
+              x' <- liftIO $ readMaybeType sym "field" (shapeType shp) x
+              matchArg opts sc cc cs prepost md (MIRVal shp x') y z
+        | (Some (Functor.Pair xFldShp (Crucible.RV x)), y, z) <-
+            zip3 (FC.toListFC Some (Ctx.zipWith Functor.Pair xsFldShps xs))
+                 ys
+                 zs
+        ]
+
     (_, _, MS.SetupNull empty)                -> absurd empty
     (_, _, MS.SetupGlobal empty _)            -> absurd empty
     (_, _, MS.SetupCast empty _)              -> absurd empty
diff --git a/src/SAWScript/Crucible/MIR/ResolveSetupValue.hs b/src/SAWScript/Crucible/MIR/ResolveSetupValue.hs
index 5ddf1b6a21..960e33b994 100644
--- a/src/SAWScript/Crucible/MIR/ResolveSetupValue.hs
+++ b/src/SAWScript/Crucible/MIR/ResolveSetupValue.hs
@@ -105,7 +105,7 @@ typeOfSetupValue ::
   Map AllocIndex Text ->
   SetupValue ->
   m Mir.Ty
-typeOfSetupValue _mcc env _nameEnv val =
+typeOfSetupValue mcc env nameEnv val =
   case val of
     MS.SetupVar i ->
       case Map.lookup i env of
@@ -122,6 +122,9 @@ typeOfSetupValue _mcc env _nameEnv val =
         tp -> X.throwM (MIRInvalidTypedTerm tp)
     MS.SetupArray elemTy vs ->
       pure $ Mir.TyArray elemTy (length vs)
+    MS.SetupTuple () vals -> do
+      tys <- traverse (typeOfSetupValue mcc env nameEnv) vals
+      pure $ Mir.TyTuple tys
 
     MS.SetupNull empty                -> absurd empty
     MS.SetupGlobal empty _            -> absurd empty
@@ -162,6 +165,17 @@ resolveSetupVal mcc env tyenv nameEnv val =
     MS.SetupNull empty                -> absurd empty
     MS.SetupGlobal empty _            -> absurd empty
     MS.SetupStruct _ _                -> panic "resolveSetupValue" ["structs not yet implemented"]
+    MS.SetupTuple () flds -> do
+      flds' <- traverse (resolveSetupVal mcc env tyenv nameEnv) flds
+      let fldMirTys = map (\(MIRVal shp _) -> shapeMirTy shp) flds'
+      Some fldAssn <-
+        pure $ Ctx.fromList $
+        map (\(MIRVal shp v) ->
+              Some $ Functor.Pair (OptField shp) (RV (W4.justPartExpr sym v)))
+            flds'
+      let (fldShpAssn, valAssn) = Ctx.unzip fldAssn
+      let tupleShp = TupleShape (Mir.TyTuple fldMirTys) fldMirTys fldShpAssn
+      pure $ MIRVal tupleShp valAssn
     MS.SetupArray elemTy vs -> do
       vals <- V.mapM (resolveSetupVal mcc env tyenv nameEnv) (V.fromList vs)
 
@@ -186,6 +200,7 @@ resolveSetupVal mcc env tyenv nameEnv val =
     MS.SetupUnion empty _ _           -> absurd empty
     MS.SetupGlobalInitializer empty _ -> absurd empty
   where
+    sym = mcc ^. mccSym
     col = mcc ^. mccRustModule . Mir.rmCS . Mir.collection
 
 resolveTypedTerm ::
diff --git a/src/SAWScript/Crucible/MIR/Setup/Value.hs b/src/SAWScript/Crucible/MIR/Setup/Value.hs
index 211d82d2f2..91ee03ccab 100644
--- a/src/SAWScript/Crucible/MIR/Setup/Value.hs
+++ b/src/SAWScript/Crucible/MIR/Setup/Value.hs
@@ -61,6 +61,7 @@ import qualified SAWScript.Crucible.Common.Setup.Value as MS
 type instance MS.XSetupNull MIR = Void
 type instance MS.XSetupGlobal MIR = Void
 type instance MS.XSetupStruct MIR = ()
+type instance MS.XSetupTuple MIR = ()
 -- The 'M.Ty' represents the type of array elements.
 type instance MS.XSetupArray MIR = M.Ty
 type instance MS.XSetupElem MIR = ()
diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs
index d0869a1bc5..13738e8b87 100644
--- a/src/SAWScript/Interpreter.hs
+++ b/src/SAWScript/Interpreter.hs
@@ -3954,6 +3954,13 @@ primitives = Map.fromList
     Experimental
     [ "Construct a `MIRValue` from a `Term`." ]
 
+  , prim "mir_tuple_value" "[MIRValue] -> MIRValue"
+    (pureVal (CMS.SetupTuple () :: [CMS.SetupValue MIR] -> CMS.SetupValue MIR))
+    Experimental
+    [ "Create a SetupValue representing a MIR tuple with the given list of"
+    , "values as elements."
+    ]
+
   , prim "mir_verify"
     "MIRModule -> String -> [MIRSpec] -> Bool -> MIRSetup () -> ProofScript () -> TopLevel MIRSpec"
     (pureVal mir_verify)