diff --git a/doc/manual/manual.md b/doc/manual/manual.md
index 1d0de3c9da..186e641c10 100644
--- a/doc/manual/manual.md
+++ b/doc/manual/manual.md
@@ -2648,6 +2648,19 @@ construct compound values:
 * `mir_tuple_value : [MIRValue] -> MIRValue` construct a tuple with the given
   list of values as elements.
 
+To specify a compound value in which each element or field is symbolic, it
+would be possible, but tedious, to use a large number of `mir_fresh_var`
+invocations in conjunction with the commands above. However, the following
+function can simplify the common case where you want every element or field to
+have a fresh value:
+
+* `mir_fresh_expanded_value : String -> MIRType -> MIRSetup MIRValue`
+
+The `String` argument denotes a prefix to use when generating the names of
+fresh symbolic variables. The `MIRType` can be any type, with the exception of
+reference types (or compound types that contain references as elements or
+fields), which are not currently supported.
+
 ### Finding MIR alegraic data types
 
 We collectively refer to MIR `struct`s and `enum`s together as _algebraic data
diff --git a/doc/manual/manual.pdf b/doc/manual/manual.pdf
index de9ccf68b8..48e70824f2 100644
Binary files a/doc/manual/manual.pdf and b/doc/manual/manual.pdf differ
diff --git a/intTests/test_mir_fresh_expanded_value/Makefile b/intTests/test_mir_fresh_expanded_value/Makefile
new file mode 100644
index 0000000000..bc6297ae15
--- /dev/null
+++ b/intTests/test_mir_fresh_expanded_value/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_fresh_expanded_value/test.linked-mir.json b/intTests/test_mir_fresh_expanded_value/test.linked-mir.json
new file mode 100644
index 0000000000..f202b4695a
--- /dev/null
+++ b/intTests/test_mir_fresh_expanded_value/test.linked-mir.json
@@ -0,0 +1 @@
+{"fns":[{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Adt::01bd9e2f4f30865e"}],"body":{"blocks":[{"block":{"data":[],"terminator":{"kind":"Return","pos":"test.rs:6:20: 6:20"}},"blockid":"bb0"}],"vars":[{"is_zst":true,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::e93222e871854c41"}]},"name":"test/8e312bae::f","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":[],"terminator":{"kind":"Return","pos":"test.rs:10:28: 10:28"}},"blockid":"bb0"}],"vars":[{"is_zst":true,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::e93222e871854c41"}]},"name":"test/8e312bae::h","return_ty":"ty::Tuple::e93222e871854c41","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Array::cef0e4ed0a308aa2"}],"body":{"blocks":[{"block":{"data":[],"terminator":{"kind":"Return","pos":"test.rs:8:26: 8:26"}},"blockid":"bb0"}],"vars":[{"is_zst":true,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::e93222e871854c41"}]},"name":"test/8e312bae::g","return_ty":"ty::Tuple::e93222e871854c41","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Adt::480389e29db14a3a"}],"body":{"blocks":[{"block":{"data":[],"terminator":{"kind":"Return","pos":"test.rs:17:20: 17:20"}},"blockid":"bb0"}],"vars":[{"is_zst":true,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::e93222e871854c41"}]},"name":"test/8e312bae::i","return_ty":"ty::Tuple::e93222e871854c41","spread_arg":null}],"adts":[{"kind":{"kind":"Struct"},"name":"test/8e312bae::S2::_adtb7803c2264daf0ec[0]","orig_def_id":"test/8e312bae::S2","orig_substs":[],"repr_transparent":false,"size":16,"variants":[{"ctor_kind":null,"discr":{"index":0,"kind":"Relative"},"discr_value":null,"fields":[{"name":"test/8e312bae::S2::z","ty":"ty::u32"},{"name":"test/8e312bae::S2::w","ty":"ty::Ref::e028c0f25e8b6323"}],"inhabited":true,"name":"test/8e312bae::S2"}]},{"kind":{"kind":"Struct"},"name":"test/8e312bae::S1::_adtb7803c2264daf0ec[0]","orig_def_id":"test/8e312bae::S1","orig_substs":[],"repr_transparent":false,"size":8,"variants":[{"ctor_kind":null,"discr":{"index":0,"kind":"Relative"},"discr_value":null,"fields":[{"name":"test/8e312bae::S1::x","ty":"ty::u32"},{"name":"test/8e312bae::S1::y","ty":"ty::u32"}],"inhabited":true,"name":"test/8e312bae::S1"}]}],"statics":[],"vtables":[],"traits":[],"intrinsics":[{"inst":{"def_id":"test/8e312bae::f","kind":"Item","substs":[]},"name":"test/8e312bae::f"},{"inst":{"def_id":"test/8e312bae::h","kind":"Item","substs":[]},"name":"test/8e312bae::h"},{"inst":{"def_id":"test/8e312bae::g","kind":"Item","substs":[]},"name":"test/8e312bae::g"},{"inst":{"def_id":"test/8e312bae::i","kind":"Item","substs":[]},"name":"test/8e312bae::i"}],"tys":[{"name":"ty::Adt::01bd9e2f4f30865e","ty":{"kind":"Adt","name":"test/8e312bae::S1::_adtb7803c2264daf0ec[0]","orig_def_id":"test/8e312bae::S1","substs":[]}},{"name":"ty::Tuple::e93222e871854c41","ty":{"kind":"Tuple","tys":[]}},{"name":"ty::u32","ty":{"kind":"Uint","uintkind":{"kind":"U32"}}},{"name":"ty::Tuple::f54c7b3282e27392","ty":{"kind":"Tuple","tys":["ty::u32","ty::u32"]}},{"name":"ty::usize","ty":{"kind":"Uint","uintkind":{"kind":"Usize"}}},{"name":"ty::Array::cef0e4ed0a308aa2","ty":{"kind":"Array","size":{"rendered":{"kind":"usize","size":8,"val":"2"},"ty":"ty::usize"},"ty":"ty::u32"}},{"name":"ty::Adt::480389e29db14a3a","ty":{"kind":"Adt","name":"test/8e312bae::S2::_adtb7803c2264daf0ec[0]","orig_def_id":"test/8e312bae::S2","substs":[]}},{"name":"ty::Ref::e028c0f25e8b6323","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::u32"}}],"roots":["test/8e312bae::f","test/8e312bae::g","test/8e312bae::h","test/8e312bae::i"]}
\ No newline at end of file
diff --git a/intTests/test_mir_fresh_expanded_value/test.rs b/intTests/test_mir_fresh_expanded_value/test.rs
new file mode 100644
index 0000000000..6e9c26ba47
--- /dev/null
+++ b/intTests/test_mir_fresh_expanded_value/test.rs
@@ -0,0 +1,17 @@
+pub struct S1 {
+    pub x: u32,
+    pub y: u32,
+}
+
+pub fn f(_s: S1) {}
+
+pub fn g(_a: [u32; 2]) {}
+
+pub fn h(_t: (u32, u32)) {}
+
+pub struct S2 {
+    pub z: u32,
+    pub w: &'static u32,
+}
+
+pub fn i(_s: S2) {}
diff --git a/intTests/test_mir_fresh_expanded_value/test.saw b/intTests/test_mir_fresh_expanded_value/test.saw
new file mode 100644
index 0000000000..3a580cf679
--- /dev/null
+++ b/intTests/test_mir_fresh_expanded_value/test.saw
@@ -0,0 +1,36 @@
+enable_experimental;
+
+m <- mir_load_module "test.linked-mir.json";
+let s1_adt = mir_find_adt m "test::S1" [];
+let s2_adt = mir_find_adt m "test::S2" [];
+
+let f_spec = do {
+  s <- mir_fresh_expanded_value "s" (mir_adt s1_adt);
+
+  mir_execute_func [s];
+};
+
+let g_spec = do {
+  a <- mir_fresh_expanded_value "a" (mir_array 2 mir_u32);
+
+  mir_execute_func [a];
+};
+
+let h_spec = do {
+  t <- mir_fresh_expanded_value "t" (mir_tuple [mir_u32, mir_u32]);
+
+  mir_execute_func [t];
+};
+
+let i_spec = do {
+  s <- mir_fresh_expanded_value "s" (mir_adt s2_adt);
+
+  mir_execute_func [s];
+};
+
+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;
+fails (
+  mir_verify m "test::i" [] false i_spec z3
+);
diff --git a/intTests/test_mir_fresh_expanded_value/test.sh b/intTests/test_mir_fresh_expanded_value/test.sh
new file mode 100755
index 0000000000..2315cc233c
--- /dev/null
+++ b/intTests/test_mir_fresh_expanded_value/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 a7e3531764..214a3e7a45 100644
--- a/saw-remote-api/CHANGELOG.md
+++ b/saw-remote-api/CHANGELOG.md
@@ -25,6 +25,11 @@
 * The API for `"struct"` `setup value`s now has a `"MIR ADT"` field. For
   MIR verification, this field is required. For LLVM and JVM verification,
   this field must be `null`, or else an error will be raised.
+* Add a `"fresh expanded"` `setup value` that denotes a value entirely
+  populated by fresh symbolic variables. For compound types such as structs or
+  arrays, this will explicitly set each field or element to contain a fresh
+  symbolic variable. This is currently only supported with LLVM and MIR
+  verification, and using this with JVM verification will raise an error.
 
 ## 1.0.0 -- 2023-06-26
 
diff --git a/saw-remote-api/python/CHANGELOG.md b/saw-remote-api/python/CHANGELOG.md
index 6a25dcc327..09c0a4b3d0 100644
--- a/saw-remote-api/python/CHANGELOG.md
+++ b/saw-remote-api/python/CHANGELOG.md
@@ -29,6 +29,12 @@
 * Add a `proclaim_f` function. This behaves like the `proclaim` function, except
   that it takes a `cry_f`-style format string as an argument. That is,
   `proclaim_f(...)` is equivalent to `proclaim(cry_f(...))`.
+* Add a `fresh_expanded` function that creates a value entirely populated by
+  fresh symbolic variables. For compound types such as structs or arrays, this
+  will explicitly set each field or element to contain a fresh symbolic
+  variable. This function is currently only supported with LLVM and MIR
+  verification, and using this function with 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 d6ad9c1944..f89a18ccb4 100644
--- a/saw-remote-api/python/saw_client/crucible.py
+++ b/saw-remote-api/python/saw_client/crucible.py
@@ -187,6 +187,19 @@ def to_json(self) -> JSON:
         return {'setup value': 'field',
                 'base': self.base.to_json(), 'field': self.field_name}
 
+class FreshExpandedVal(SetupVal):
+    prefix: str
+    ty: Union['LLVMType', 'JVMType', 'MIRType']
+
+    def __init__(self, prefix : str, ty : Union['LLVMType', 'JVMType', 'MIRType']) -> None:
+        self.prefix = prefix
+        self.ty = ty
+
+    def to_json(self) -> JSON:
+        return {'setup value': 'fresh expanded',
+                'prefix': self.prefix,
+                'type': self.ty.to_json()}
+
 class GlobalInitializerVal(SetupVal):
     name : str
 
@@ -737,6 +750,18 @@ def field(base : SetupVal, field_name : str) -> SetupVal:
         raise ValueError('field expected a str, but got {field_name!r}')
     return FieldVal(base, field_name)
 
+def fresh_expanded(prefix: str, ty: Union['LLVMType', 'JVMType', 'MIRType']) -> SetupVal:
+    """Returns a value entirely populated with fresh symbolic variables (i.e.,
+    a ``FreshExpandedVal``). If ``ty`` is a compound type such as a struct or an
+    array, this will explicitly set each field or element to contain a fresh
+    symbolic variable. The ``prefix`` argument is used as a prefix in each of
+    the symbolic variables.
+
+    At present, this is only supported with LLVM and MIR verification. Using
+    this function with JVM verification will raise an error.
+    """
+    return FreshExpandedVal(prefix, ty)
+
 def global_initializer(name: str) -> SetupVal:
     """Returns the initializer value of a named global ``name`` (i.e., a ``GlobalInitializerVal``)."""
     if not isinstance(name, str):
diff --git a/saw-remote-api/python/tests/saw/test-files/mir_fresh_expanded_value.linked-mir.json b/saw-remote-api/python/tests/saw/test-files/mir_fresh_expanded_value.linked-mir.json
new file mode 100644
index 0000000000..16dbaae122
--- /dev/null
+++ b/saw-remote-api/python/tests/saw/test-files/mir_fresh_expanded_value.linked-mir.json
@@ -0,0 +1 @@
+{"fns":[{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Adt::280e5deae5669c6d"}],"body":{"blocks":[{"block":{"data":[],"terminator":{"kind":"Return","pos":"mir_fresh_expanded_value.rs:6:20: 6:20"}},"blockid":"bb0"}],"vars":[{"is_zst":true,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::e93222e871854c41"}]},"name":"mir_fresh_expanded_value/90f4371e::f","return_ty":"ty::Tuple::e93222e871854c41","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Array::cef0e4ed0a308aa2"}],"body":{"blocks":[{"block":{"data":[],"terminator":{"kind":"Return","pos":"mir_fresh_expanded_value.rs:8:26: 8:26"}},"blockid":"bb0"}],"vars":[{"is_zst":true,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::e93222e871854c41"}]},"name":"mir_fresh_expanded_value/90f4371e::g","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":[],"terminator":{"kind":"Return","pos":"mir_fresh_expanded_value.rs:10:28: 10:28"}},"blockid":"bb0"}],"vars":[{"is_zst":true,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::e93222e871854c41"}]},"name":"mir_fresh_expanded_value/90f4371e::h","return_ty":"ty::Tuple::e93222e871854c41","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Adt::9419786252d2b491"}],"body":{"blocks":[{"block":{"data":[],"terminator":{"kind":"Return","pos":"mir_fresh_expanded_value.rs:17:20: 17:20"}},"blockid":"bb0"}],"vars":[{"is_zst":true,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::e93222e871854c41"}]},"name":"mir_fresh_expanded_value/90f4371e::i","return_ty":"ty::Tuple::e93222e871854c41","spread_arg":null}],"adts":[{"kind":{"kind":"Struct"},"name":"mir_fresh_expanded_value/90f4371e::S1::_adtb7803c2264daf0ec[0]","orig_def_id":"mir_fresh_expanded_value/90f4371e::S1","orig_substs":[],"repr_transparent":false,"size":8,"variants":[{"ctor_kind":null,"discr":{"index":0,"kind":"Relative"},"discr_value":null,"fields":[{"name":"mir_fresh_expanded_value/90f4371e::S1::x","ty":"ty::u32"},{"name":"mir_fresh_expanded_value/90f4371e::S1::y","ty":"ty::u32"}],"inhabited":true,"name":"mir_fresh_expanded_value/90f4371e::S1"}]},{"kind":{"kind":"Struct"},"name":"mir_fresh_expanded_value/90f4371e::S2::_adtb7803c2264daf0ec[0]","orig_def_id":"mir_fresh_expanded_value/90f4371e::S2","orig_substs":[],"repr_transparent":false,"size":16,"variants":[{"ctor_kind":null,"discr":{"index":0,"kind":"Relative"},"discr_value":null,"fields":[{"name":"mir_fresh_expanded_value/90f4371e::S2::z","ty":"ty::u32"},{"name":"mir_fresh_expanded_value/90f4371e::S2::w","ty":"ty::Ref::e028c0f25e8b6323"}],"inhabited":true,"name":"mir_fresh_expanded_value/90f4371e::S2"}]}],"statics":[],"vtables":[],"traits":[],"intrinsics":[{"inst":{"def_id":"mir_fresh_expanded_value/90f4371e::f","kind":"Item","substs":[]},"name":"mir_fresh_expanded_value/90f4371e::f"},{"inst":{"def_id":"mir_fresh_expanded_value/90f4371e::g","kind":"Item","substs":[]},"name":"mir_fresh_expanded_value/90f4371e::g"},{"inst":{"def_id":"mir_fresh_expanded_value/90f4371e::h","kind":"Item","substs":[]},"name":"mir_fresh_expanded_value/90f4371e::h"},{"inst":{"def_id":"mir_fresh_expanded_value/90f4371e::i","kind":"Item","substs":[]},"name":"mir_fresh_expanded_value/90f4371e::i"}],"tys":[{"name":"ty::Adt::280e5deae5669c6d","ty":{"kind":"Adt","name":"mir_fresh_expanded_value/90f4371e::S1::_adtb7803c2264daf0ec[0]","orig_def_id":"mir_fresh_expanded_value/90f4371e::S1","substs":[]}},{"name":"ty::Tuple::e93222e871854c41","ty":{"kind":"Tuple","tys":[]}},{"name":"ty::u32","ty":{"kind":"Uint","uintkind":{"kind":"U32"}}},{"name":"ty::usize","ty":{"kind":"Uint","uintkind":{"kind":"Usize"}}},{"name":"ty::Array::cef0e4ed0a308aa2","ty":{"kind":"Array","size":{"rendered":{"kind":"usize","size":8,"val":"2"},"ty":"ty::usize"},"ty":"ty::u32"}},{"name":"ty::Tuple::f54c7b3282e27392","ty":{"kind":"Tuple","tys":["ty::u32","ty::u32"]}},{"name":"ty::Adt::9419786252d2b491","ty":{"kind":"Adt","name":"mir_fresh_expanded_value/90f4371e::S2::_adtb7803c2264daf0ec[0]","orig_def_id":"mir_fresh_expanded_value/90f4371e::S2","substs":[]}},{"name":"ty::Ref::e028c0f25e8b6323","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::u32"}}],"roots":["mir_fresh_expanded_value/90f4371e::f","mir_fresh_expanded_value/90f4371e::g","mir_fresh_expanded_value/90f4371e::h","mir_fresh_expanded_value/90f4371e::i"]}
\ No newline at end of file
diff --git a/saw-remote-api/python/tests/saw/test-files/mir_fresh_expanded_value.rs b/saw-remote-api/python/tests/saw/test-files/mir_fresh_expanded_value.rs
new file mode 100644
index 0000000000..6e9c26ba47
--- /dev/null
+++ b/saw-remote-api/python/tests/saw/test-files/mir_fresh_expanded_value.rs
@@ -0,0 +1,17 @@
+pub struct S1 {
+    pub x: u32,
+    pub y: u32,
+}
+
+pub fn f(_s: S1) {}
+
+pub fn g(_a: [u32; 2]) {}
+
+pub fn h(_t: (u32, u32)) {}
+
+pub struct S2 {
+    pub z: u32,
+    pub w: &'static u32,
+}
+
+pub fn i(_s: S2) {}
diff --git a/saw-remote-api/python/tests/saw/test_mir_fresh_expanded_value.py b/saw-remote-api/python/tests/saw/test_mir_fresh_expanded_value.py
new file mode 100644
index 0000000000..1c8bfd586f
--- /dev/null
+++ b/saw-remote-api/python/tests/saw/test_mir_fresh_expanded_value.py
@@ -0,0 +1,61 @@
+import unittest
+from pathlib import Path
+
+from saw_client import *
+from saw_client.crucible import fresh_expanded
+from saw_client.mir import Contract, MIRAdt, adt_ty, array_ty, tuple_ty, u32, void
+
+
+class FContract(Contract):
+    adt: MIRAdt
+
+    def __init__(self, adt: MIRAdt):
+        super().__init__()
+        self.adt = adt
+
+    def specification(self) -> None:
+        s = fresh_expanded('s', adt_ty(self.adt))
+
+        self.execute_func(s)
+
+        self.returns(void)
+
+
+class GContract(Contract):
+    def specification(self) -> None:
+        a = fresh_expanded('a', array_ty(2, u32))
+
+        self.execute_func(a)
+
+        self.returns(void)
+
+
+class HContract(Contract):
+    def specification(self) -> None:
+        t = fresh_expanded('t', tuple_ty(u32, u32))
+
+        self.execute_func(t)
+
+        self.returns(void)
+
+
+class MIRFreshExpandedValueTest(unittest.TestCase):
+    def test_mir_fresh_expanded_value(self):
+        connect(reset_server=True)
+        if __name__ == "__main__": view(LogResults())
+        json_name = str(Path('tests', 'saw', 'test-files', 'mir_fresh_expanded_value.linked-mir.json'))
+        mod = mir_load_module(json_name)
+
+        s1_adt = mir_find_adt(mod, 'mir_fresh_expanded_value::S1')
+        f_result = mir_verify(mod, 'mir_fresh_expanded_value::f', FContract(s1_adt))
+        self.assertIs(f_result.is_success(), True)
+
+        g_result = mir_verify(mod, 'mir_fresh_expanded_value::g', GContract())
+        self.assertIs(g_result.is_success(), True)
+
+        h_result = mir_verify(mod, 'mir_fresh_expanded_value::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 4523612af0..9a2e16d381 100644
--- a/saw-remote-api/src/SAWServer.hs
+++ b/saw-remote-api/src/SAWServer.hs
@@ -122,6 +122,7 @@ data CrucibleSetupVal ty e
   | GlobalLValue String
   | NamedValue ServerName
   | CryptolExpr e
+  | FreshExpandedValue Text ty
   deriving stock (Foldable, Functor, Traversable)
 
 data SetupStep ty
diff --git a/saw-remote-api/src/SAWServer/Data/SetupValue.hs b/saw-remote-api/src/SAWServer/Data/SetupValue.hs
index 22a329943f..4b30db129b 100644
--- a/saw-remote-api/src/SAWServer/Data/SetupValue.hs
+++ b/saw-remote-api/src/SAWServer/Data/SetupValue.hs
@@ -21,6 +21,7 @@ data SetupValTag
   | TagElemLValue
   | TagGlobalInit
   | TagGlobalLValue
+  | TagFreshExpandedValue
 
 instance FromJSON SetupValTag where
   parseJSON =
@@ -38,6 +39,7 @@ instance FromJSON SetupValTag where
       "element lvalue" -> pure TagElemLValue
       "global initializer" -> pure TagGlobalInit
       "global lvalue" -> pure TagGlobalLValue
+      "fresh expanded" -> pure TagFreshExpandedValue
       _ -> empty
 
 instance (FromJSON ty, FromJSON cryptolExpr) => FromJSON (CrucibleSetupVal ty cryptolExpr) where
@@ -58,3 +60,4 @@ instance (FromJSON ty, FromJSON cryptolExpr) => FromJSON (CrucibleSetupVal ty cr
           TagElemLValue -> ElementLValue <$> o .: "base" <*> o .: "index"
           TagGlobalInit -> GlobalInitializer <$> o .: "name"
           TagGlobalLValue -> GlobalLValue <$> o .: "name"
+          TagFreshExpandedValue -> FreshExpandedValue <$> o .: "prefix" <*> o .: "type"
diff --git a/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs b/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs
index 7f051c5fe0..b9b0bd34a7 100644
--- a/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs
+++ b/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs
@@ -198,6 +198,8 @@ compileJVMContract fileReader bic cenv0 c =
       JVMSetupM $ fail "Global initializers unsupported in JVM API."
     getSetupVal _ (GlobalLValue _) =
       JVMSetupM $ fail "Global l-values unsupported in JVM API."
+    getSetupVal _ (FreshExpandedValue _ _) =
+      JVMSetupM $ fail "Fresh expanded values unsupported in JVM API."
 
 data JVMLoadClassParams
   = JVMLoadClassParams ServerName String
diff --git a/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs b/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs
index 0b9a70066b..7d3799c937 100644
--- a/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs
+++ b/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs
@@ -38,6 +38,7 @@ import SAWScript.Crucible.LLVM.Builtins
     , llvm_alloc_readonly
     , llvm_alloc_readonly_aligned
     , llvm_execute_func
+    , llvm_fresh_expanded_val
     , llvm_fresh_var
     , llvm_points_to_internal
     , llvm_points_to_bitfield
@@ -207,6 +208,9 @@ compileLLVMContract fileReader bic ghostEnv cenv0 c =
       resolve env n >>= \case Val x -> return x
     getSetupVal (_, cenv) (CryptolExpr expr) =
       CMS.anySetupTerm <$> getTypedTerm cenv expr
+    getSetupVal _ (FreshExpandedValue _ ty) =
+      let ty' = llvmType ty in
+      llvm_fresh_expanded_val ty'
 
 data LLVMLoadModuleParams
   = LLVMLoadModuleParams ServerName FilePath
diff --git a/saw-remote-api/src/SAWServer/MIRCrucibleSetup.hs b/saw-remote-api/src/SAWServer/MIRCrucibleSetup.hs
index e2b5942741..d6494e64ac 100644
--- a/saw-remote-api/src/SAWServer/MIRCrucibleSetup.hs
+++ b/saw-remote-api/src/SAWServer/MIRCrucibleSetup.hs
@@ -28,6 +28,7 @@ import SAWScript.Crucible.Common.Setup.Builtins (CheckPointsToType(..))
 import SAWScript.Crucible.MIR.Builtins
     ( mir_alloc,
       mir_alloc_mut,
+      mir_fresh_expanded_value,
       mir_fresh_var,
       mir_execute_func,
       mir_load_module,
@@ -200,6 +201,9 @@ compileMIRContract fileReader bic cenv0 sawenv c =
       pure $ MS.SetupGlobalInitializer () name
     getSetupVal _ (GlobalLValue name) =
       pure $ MS.SetupGlobal () name
+    getSetupVal _ (FreshExpandedValue pfx ty) =
+      let ty' = mirType sawenv ty in
+      mir_fresh_expanded_value pfx ty'
     getSetupVal _ (FieldLValue _ _) =
       MIRSetupM $ fail "Field l-values unsupported in the MIR API."
     getSetupVal _ (CastLValue _ _) =
diff --git a/src/SAWScript/Crucible/MIR/Builtins.hs b/src/SAWScript/Crucible/MIR/Builtins.hs
index 3c4f0774f6..863444e9f9 100644
--- a/src/SAWScript/Crucible/MIR/Builtins.hs
+++ b/src/SAWScript/Crucible/MIR/Builtins.hs
@@ -15,6 +15,7 @@ module SAWScript.Crucible.MIR.Builtins
   , mir_assert
   , mir_execute_func
   , mir_find_adt
+  , mir_fresh_expanded_value
   , mir_fresh_var
   , mir_load_module
   , mir_points_to
@@ -67,6 +68,7 @@ import qualified Data.Parameterized.Context as Ctx
 import qualified Data.Parameterized.Map as MapF
 import Data.Parameterized.NatRepr (knownNat, natValue)
 import Data.Parameterized.Some (Some(..))
+import qualified Data.Parameterized.TraversableFC.WithIndex as FCI
 import qualified Data.Set as Set
 import qualified Data.Text as Text
 import Data.Text (Text)
@@ -201,6 +203,103 @@ mir_find_adt rm origName substs = do
   origDid <- findDefId crateDisambigs (Text.pack origName)
   findAdt col origDid (Mir.Substs substs)
 
+-- | Create a MIR value entirely populated with fresh symbolic variables.
+-- For compound types such as structs and arrays, this will explicitly set
+-- each field or element to contain a fresh symbolic variable. The Text
+-- argument is used as a prefix in each of the symbolic variables.
+mir_fresh_expanded_value ::
+  Text                 {- ^ Prefix to use in each symbolic variable -} ->
+  Mir.Ty               {- ^ value type -} ->
+  MIRSetupM SetupValue {- ^ elaborated setup value -}
+mir_fresh_expanded_value pfx ty =
+  MIRSetupM $
+  do sc <- lift $ lift getSharedContext
+     cc <- getMIRCrucibleContext
+     let col = cc ^. mccRustModule . Mir.rmCS . Mir.collection
+     Some shp <- pure $ tyToShape col ty
+     constructExpandedSetupValue cc sc pfx shp
+
+-- | See 'mir_fresh_expanded_val'.
+--
+-- This is the recursively-called worker function.
+constructExpandedSetupValue ::
+  MIRCrucibleContext ->
+  SharedContext ->
+  Text ->
+  TypeShape tp ->
+  CrucibleSetup MIR SetupValue
+constructExpandedSetupValue cc sc = go
+  where
+    col = cc ^. mccRustModule . Mir.rmCS . Mir.collection
+
+    go :: forall tp.
+          Text ->
+          TypeShape tp ->
+          CrucibleSetup MIR SetupValue
+    go pfx shp =
+      case shp of
+        UnitShape _ ->
+          pure $ MS.SetupTuple () []
+        PrimShape ty _ ->
+          case cryptolTypeOfActual ty of
+            Nothing ->
+              X.throwM $ MIRFreshExpandedValueUnsupportedType ty
+            Just cty -> do
+              fv <- Setup.freshVariable sc pfx cty
+              pure $ MS.SetupTerm fv
+        TupleShape _ _ fldShps -> do
+          flds <- goFlds pfx fldShps
+          pure $ MS.SetupTuple () flds
+        ArrayShape ty elemTy elemShp ->
+          case ty of
+            Mir.TyArray _ n -> do
+              elems <-
+                traverse
+                  (\i -> go (pfx <> "." <> Text.pack (show i)) elemShp)
+                  [0..n-1]
+              pure $ MS.SetupArray elemTy elems
+            _ ->
+              panic "constructExpandedSetupValue"
+                    [ "ArrayShape with non-TyArray type:"
+                    , show (PP.pretty ty)
+                    ]
+        StructShape ty _ fldShps ->
+          case ty of
+            Mir.TyAdt adtName _ _ -> do
+              case col ^. Mir.adts . at adtName of
+                Just adt -> do
+                  flds <- goFlds pfx fldShps
+                  pure $ MS.SetupStruct adt flds
+                Nothing ->
+                  panic "constructExpandedSetupValue"
+                        [ "Could not find ADT in StructShape:"
+                        , show adtName
+                        ]
+            _ ->
+              panic "constructExpandedSetupValue"
+                    [ "StructShape with non-TyAdt type:"
+                    , show (PP.pretty ty)
+                    ]
+        TransparentShape _ shp' ->
+          go pfx shp'
+        RefShape ty _ _ _ ->
+          X.throwM $ MIRFreshExpandedValueUnsupportedType ty
+        FnPtrShape ty _ _ ->
+          X.throwM $ MIRFreshExpandedValueUnsupportedType ty
+
+    goFlds :: forall ctx.
+              Text ->
+              Ctx.Assignment FieldShape ctx ->
+              CrucibleSetup MIR [SetupValue]
+    goFlds pfx fldShps = sequenceA $
+      FCI.itoListFC
+        (\idx fldShp ->
+          let pfx' = pfx <> "." <> Text.pack (show idx) in
+          case fldShp of
+            ReqField shp' -> go pfx' shp'
+            OptField shp' -> go pfx' shp')
+        fldShps
+
 -- | Generate a fresh variable term. The name will be used when
 -- pretty-printing the variable in debug output.
 mir_fresh_var ::
@@ -1204,6 +1303,7 @@ withImplicitParams opts k =
 
 data MIRSetupError
   = MIRFreshVarInvalidType Mir.Ty
+  | MIRFreshExpandedValueUnsupportedType Mir.Ty
   | MIRArgTypeMismatch Int Mir.Ty Mir.Ty -- argument position, expected, found
   | MIRArgNumberWrong Int Int -- number expected, number found
   | MIRReturnUnexpected Mir.Ty -- found
@@ -1218,6 +1318,9 @@ instance Show MIRSetupError where
     case err of
       MIRFreshVarInvalidType jty ->
         "mir_fresh_var: Invalid type: " ++ show jty
+      MIRFreshExpandedValueUnsupportedType ty ->
+        "mir_fresh_expanded_value: " ++ show (PP.pretty ty) ++
+        " not supported"
       MIRArgTypeMismatch i expected found ->
         unlines
         [ "mir_execute_func: Argument type mismatch"
diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs
index 980aec8d95..7ec8c4ec4f 100644
--- a/src/SAWScript/Interpreter.hs
+++ b/src/SAWScript/Interpreter.hs
@@ -3923,6 +3923,15 @@ primitives = Map.fromList
     , "be found in the MIRModule, this will raise an error."
     ]
 
+  , prim "mir_fresh_expanded_value" "String -> MIRType -> MIRSetup MIRValue"
+    (pureVal mir_fresh_expanded_value)
+    Experimental
+    [ "Create a MIR value entirely populated with fresh symbolic variables."
+    , "For compound types such as structs and arrays, this will explicitly set"
+    , "each field or element to contain a fresh symbolic variable. The String"
+    , "argument is used as a prefix in each of the symbolic variables."
+    ]
+
   , prim "mir_fresh_var" "String -> MIRType -> MIRSetup Term"
     (pureVal mir_fresh_var)
     Experimental