diff --git a/crucible-mir-comp/src/Mir/Compositional/Builder.hs b/crucible-mir-comp/src/Mir/Compositional/Builder.hs
index 0e77b644b7..9743a2af2f 100644
--- a/crucible-mir-comp/src/Mir/Compositional/Builder.hs
+++ b/crucible-mir-comp/src/Mir/Compositional/Builder.hs
@@ -629,6 +629,7 @@ substMethodSpec sc sm ms = do
         MS.SetupStruct b svs -> MS.SetupStruct b <$> mapM goSetupValue svs
         MS.SetupTuple b svs -> MS.SetupTuple b <$> mapM goSetupValue svs
         MS.SetupSlice slice -> MS.SetupSlice <$> goSetupSlice slice
+        MS.SetupEnum enum_ -> MS.SetupEnum <$> goSetupEnum enum_
         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
@@ -644,6 +645,11 @@ substMethodSpec sc sm ms = do
     goSetupCondition (MS.SetupCond_Ghost b loc gg tt) =
         MS.SetupCond_Ghost b loc gg <$> goTypedTerm tt
 
+    goSetupEnum (MirSetupEnumVariant adt variantNm svs) =
+      MirSetupEnumVariant adt variantNm <$> mapM goSetupValue svs
+    goSetupEnum sv@(MirSetupEnumSymbolic _) =
+      return sv
+
     goSetupSlice (MirSetupSliceRaw ref len) =
       MirSetupSliceRaw <$> goSetupValue ref <*> goSetupValue len
     goSetupSlice (MirSetupSlice arr) =
@@ -742,6 +748,8 @@ regToSetup bak p eval shp rv = go shp rv
         refSV <- go refShp refRV
         lenSV <- go lenShp lenRV
         pure $ MS.SetupSlice $ MirSetupSliceRaw refSV lenSV
+    go (EnumShape _ _ _ _) _ =
+      error "Enums not currently supported in overrides"
     go (FnPtrShape _ _ _) _ =
         error "Function pointers not currently supported in overrides"
 
diff --git a/crucible-mir-comp/src/Mir/Compositional/Clobber.hs b/crucible-mir-comp/src/Mir/Compositional/Clobber.hs
index f9bebc062d..64301bdf93 100644
--- a/crucible-mir-comp/src/Mir/Compositional/Clobber.hs
+++ b/crucible-mir-comp/src/Mir/Compositional/Clobber.hs
@@ -62,6 +62,8 @@ clobberSymbolic sym loc nameStr shp rv = go shp rv
         ", but got Any wrapping " ++ show tpr
       where shpTpr = StructRepr $ fmapFC fieldShapeType flds
     go (TransparentShape _ shp) rv = go shp rv
+    go (EnumShape _ _ _ _) _rv =
+      error "Enums not currently supported in overrides"
     go (FnPtrShape _ _ _) _rv =
         error "Function pointers not currently supported in overrides"
     go (RefShape _ _ _ _) _rv = error "clobberSymbolic: RefShape NYI"
@@ -120,6 +122,8 @@ clobberImmutSymbolic sym loc nameStr shp rv = go shp rv
         ref' <- go refShp ref
         len' <- go lenShp len
         pure $ Ctx.Empty Ctx.:> RV ref' Ctx.:> RV len'
+    go (EnumShape _ _ _ _) _rv =
+      error "Enums not currently supported in overrides"
     go (FnPtrShape _ _ _) _rv =
         error "Function pointers not currently supported in overrides"
 
diff --git a/crucible-mir-comp/src/Mir/Compositional/Override.hs b/crucible-mir-comp/src/Mir/Compositional/Override.hs
index da5d4ce55e..a9231015b0 100644
--- a/crucible-mir-comp/src/Mir/Compositional/Override.hs
+++ b/crucible-mir-comp/src/Mir/Compositional/Override.hs
@@ -544,6 +544,8 @@ setupToReg sym sc termSub regMap allocMap shp sv = go shp sv
         refRV <- go refShp refSV
         lenRV <- go lenShp lenSV
         pure $ Ctx.Empty Ctx.:> RV refRV Ctx.:> RV lenRV
+    go (EnumShape _ _ _ _) _ =
+      error "Enums not currently supported in overrides"
     go (FnPtrShape _ _ _) _ =
         error "Function pointers not currently supported in overrides"
     go shp sv = error $ "setupToReg: type error: bad SetupValue for " ++ show (shapeType shp) ++
diff --git a/crux-mir-comp/src/Mir/Cryptol.hs b/crux-mir-comp/src/Mir/Cryptol.hs
index 08bf240b29..37ebe45463 100644
--- a/crux-mir-comp/src/Mir/Cryptol.hs
+++ b/crux-mir-comp/src/Mir/Cryptol.hs
@@ -337,6 +337,8 @@ munge sym shp rv = do
                 AnyValue tpr <$> goFields flds rvs
             | otherwise = error $  "munge: StructShape AnyValue with NYI TypeRepr " ++ show tpr
         go (TransparentShape _ shp) rv = go shp rv
+        go (EnumShape _ _ _ _) _ =
+            error "Enums not currently supported in overrides"
         go (FnPtrShape _ _ _) _ =
             error "Function pointers not currently supported in overrides"
         -- TODO: RefShape
diff --git a/doc/manual/manual.md b/doc/manual/manual.md
index 9fb91a2d73..f1a83ac958 100644
--- a/doc/manual/manual.md
+++ b/doc/manual/manual.md
@@ -2117,12 +2117,9 @@ mir_verify :
 
 ### Running a MIR-based verification
 
-`mir_verify` requires `enable_experimental` in order to be used.  Moreover,
-some parts of `mir_verify` are not currently implemented, so it is possible
-that using `mir_verify` on some programs will fail. Features that are not yet
-implemented include the following:
-
-* The ability to construct MIR `enum` values in specifications
+(Note: API functions involving MIR verification require `enable_experimental`
+in order to be used. As such, some parts of this API may change before being
+finalized.)
 
 The `String` supplied as an argument to `mir_verify` is expected to be a
 function _identifier_. An identifier is expected adhere to one of the following
@@ -2926,6 +2923,14 @@ construct compound values:
 * `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_enum_value : MIRAdt -> String -> [MIRValue] -> MIRValue` constructs an
+  enum using a particular enum variant. The `MIRAdt` arguments determines what
+  enum type to create, the `String` value determines the name of the variant to
+  use, and the `[MIRValue]` list are the values to use as elements in the
+  variant.
+
+  See the "Finding MIR alegraic data types" section for more information on how
+  to compute a `MIRAdt` value to pass to `mir_enum_value`.
 * `mir_slice_value : MIRValue -> MIRValue`: see the "MIR slices" section below.
 * `mir_slice_range_value : MIRValue -> Int -> Int -> MIRValue`: see the
   "MIR slices" section below.
@@ -3102,9 +3107,46 @@ s_8_16  <- mir_find_adt m "example::S" [mir_u8,  mir_u16];
 s_32_64 <- mir_find_adt m "example::S" [mir_u32, mir_u64];
 ~~~~
 
-The `mir_adt` command (for constructing a struct type) and `mir_struct_value`
-(for constructing a struct value) commands in turn take a `MIRAdt` as an
-argument.
+The `mir_adt` command (for constructing a struct type), `mir_struct_value` (for
+constructing a struct value), and `mir_enum_value` (for constructing an enum
+value) commands in turn take a `MIRAdt` as an argument.
+
+In addition to taking a `MIRAdt` as an argument, `mir_enum_variant` also takes
+a `String` representing the name of the variant to construct. The variant name
+should be a short name such as `"None"` or `"Some"`, and not a full identifier
+such as `"core::option::None"` or `"core::option::Some"`. This is because the
+`MIRAdt` already contains the full identifiers for all of an enum's variants,
+so SAW will use this information to look up a variant's identifier from a short
+name. Here is an example of using `mir_enum_value` in practice:
+
+~~~~ .rs
+pub fn n() -> Option<u32> {
+    None
+}
+
+pub fn s(x: u32) -> Option<u32> {
+    Some(x)
+}
+~~~~
+~~~~
+m <- mir_load_module "example.linked-mir.json";
+
+option_u32 <- mir_find_adt m "core::option::Option" [mir_u32];
+
+let n_spec = do {
+  mir_execute_func [];
+
+  mir_return (mir_enum_value option_u32 "None" []);
+};
+
+let s_spec = do {
+  x <- mir_fresh_var "x" mir_u32;
+
+  mir_execute_func [mir_term x];
+
+  mir_return (mir_enum_value option_u32 "Some" [mir_term x]);
+};
+~~~~
 
 ### Bitfields
 
diff --git a/doc/manual/manual.pdf b/doc/manual/manual.pdf
index 80e0c8ad8c..9784c50890 100644
Binary files a/doc/manual/manual.pdf and b/doc/manual/manual.pdf differ
diff --git a/intTests/test_mir_verify_enums/Makefile b/intTests/test_mir_verify_enums/Makefile
new file mode 100644
index 0000000000..bc6297ae15
--- /dev/null
+++ b/intTests/test_mir_verify_enums/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_enums/test.linked-mir.json b/intTests/test_mir_verify_enums/test.linked-mir.json
new file mode 100644
index 0000000000..0b503737b6
--- /dev/null
+++ b/intTests/test_mir_verify_enums/test.linked-mir.json
@@ -0,0 +1 @@
+{"fns":[{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[{"kind":"Deinit","pos":"test.rs:17:5: 17:9"},{"kind":"SetDiscriminant","lvalue":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::3fa7c2d95c7fce06"}},"pos":"test.rs:17:5: 17:9","variant_index":0}],"terminator":{"kind":"Return","pos":"test.rs:18:2: 18:2"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::3fa7c2d95c7fce06"}]},"name":"test/f696fd3c::h_none","return_ty":"ty::Adt::3fa7c2d95c7fce06","spread_arg":null},{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[{"kind":"Deinit","pos":"test.rs:30:5: 30:11"},{"kind":"SetDiscriminant","lvalue":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::7746688b48f54a60"}},"pos":"test.rs:30:5: 30:11","variant_index":0}],"terminator":{"kind":"Return","pos":"test.rs:31:2: 31:2"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::7746688b48f54a60"}]},"name":"test/f696fd3c::i42","return_ty":"ty::Adt::7746688b48f54a60","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::bool"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::bool"}},"pos":"test.rs:9:8: 9:9","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::bool"}},"kind":"Copy"}}}],"terminator":{"discr":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::bool"}},"kind":"Move"},"discr_span":"test.rs:9:8: 9:9 !test.rs:9:8: 9:9","kind":"SwitchInt","pos":"test.rs:9:8: 9:9 !test.rs:9:8: 9:9","switch_ty":"ty::bool","targets":["bb2","bb1"],"values":["0"]}},"blockid":"bb0"},{"block":{"data":[{"kind":"Deinit","pos":"test.rs:10:11: 10:15"},{"kind":"SetDiscriminant","lvalue":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::Adt::3fa7c2d95c7fce06"}},"pos":"test.rs:10:11: 10:15","variant_index":0}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::Adt::3fa7c2d95c7fce06"}},"kind":"Move"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"bb3"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::935b79106a1ed847"},"kind":"Constant"},"kind":"Call","pos":"test.rs:10:9: 10:16"}},"blockid":"bb1"},{"block":{"data":[{"kind":"Deinit","pos":"test.rs:12:11: 12:19"},{"kind":"Assign","lhs":{"data":[{"kind":"Downcast","variant":1},{"field":0,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::Adt::3fa7c2d95c7fce06"}},"pos":"test.rs:12:11: 12:19","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"uint","size":4,"val":"42"},"ty":"ty::u32"},"kind":"Constant"}}},{"kind":"SetDiscriminant","lvalue":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::Adt::3fa7c2d95c7fce06"}},"pos":"test.rs:12:11: 12:19","variant_index":1}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::Adt::3fa7c2d95c7fce06"}},"kind":"Move"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"bb3"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::935b79106a1ed847"},"kind":"Constant"},"kind":"Call","pos":"test.rs:12:9: 12:20"}},"blockid":"bb2"},{"block":{"data":[],"terminator":{"kind":"Return","pos":"test.rs:14:2: 14:2"}},"blockid":"bb3"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::bool"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::Adt::3fa7c2d95c7fce06"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::Adt::3fa7c2d95c7fce06"}]},"name":"test/f696fd3c::g","return_ty":"ty::u32","spread_arg":null},{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[{"kind":"Deinit","pos":"test.rs:34:5: 34:11"},{"kind":"SetDiscriminant","lvalue":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::7746688b48f54a60"}},"pos":"test.rs:34:5: 34:11","variant_index":1}],"terminator":{"kind":"Return","pos":"test.rs:35:2: 35:2"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::7746688b48f54a60"}]},"name":"test/f696fd3c::i43","return_ty":"ty::Adt::7746688b48f54a60","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Adt::3fa7c2d95c7fce06"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::isize"}},"pos":"test.rs:2:11: 2:12","rhs":{"kind":"Discriminant","ty":"ty::isize","val":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Adt::3fa7c2d95c7fce06"}}}}],"terminator":{"discr":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::isize"}},"kind":"Move"},"discr_span":"test.rs:3:9: 3:16","kind":"SwitchInt","pos":"test.rs:2:5: 2:12","switch_ty":"ty::isize","targets":["bb1","bb3","bb2"],"values":["0","1"]}},"blockid":"bb0"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"pos":"test.rs:4:17: 4:19","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"uint","size":4,"val":"27"},"ty":"ty::u32"},"kind":"Constant"}}}],"terminator":{"kind":"Goto","pos":"test.rs:4:17: 4:19","target":"bb4"}},"blockid":"bb1"},{"block":{"data":[],"terminator":{"kind":"Unreachable","pos":"test.rs:2:11: 2:12"}},"blockid":"bb2"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_3","ty":"ty::u32"}},"pos":"test.rs:3:14: 3:15","rhs":{"kind":"Use","usevar":{"data":{"data":[{"kind":"Downcast","variant":1},{"field":0,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Adt::3fa7c2d95c7fce06"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"pos":"test.rs:3:20: 3:21","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_3","ty":"ty::u32"}},"kind":"Copy"}}}],"terminator":{"kind":"Goto","pos":"test.rs:3:20: 3:21","target":"bb4"}},"blockid":"bb3"},{"block":{"data":[],"terminator":{"kind":"Return","pos":"test.rs:6:2: 6:2"}},"blockid":"bb4"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::isize"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_3","ty":"ty::u32"}]},"name":"test/f696fd3c::f","return_ty":"ty::u32","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u32"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"}},"pos":"test.rs:21:10: 21:11","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u32"}},"kind":"Copy"}}},{"kind":"Deinit","pos":"test.rs:21:5: 21:12"},{"kind":"Assign","lhs":{"data":[{"kind":"Downcast","variant":1},{"field":0,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::3fa7c2d95c7fce06"}},"pos":"test.rs:21:5: 21:12","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"}},"kind":"Move"}}},{"kind":"SetDiscriminant","lvalue":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::3fa7c2d95c7fce06"}},"pos":"test.rs:21:5: 21:12","variant_index":1}],"terminator":{"kind":"Return","pos":"test.rs:22:2: 22:2"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::3fa7c2d95c7fce06"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"}]},"name":"test/f696fd3c::h_some","return_ty":"ty::Adt::3fa7c2d95c7fce06","spread_arg":null},{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::isize"}},"pos":"test.rs:25:11: 25:13","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"isize","size":8,"val":"42"},"ty":"ty::isize"},"kind":"Constant"}}}],"terminator":{"kind":"Return","pos":"test.rs:25:11: 25:13"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::isize"}]},"name":"test/f696fd3c::I::I42::{constant#0}","return_ty":"ty::isize","spread_arg":null}],"adts":[{"kind":{"discr_ty":"ty::isize","kind":"Enum"},"name":"core/73237d41::option::Option::_adtc5e93708b8ca6e2a[0]","orig_def_id":"core/73237d41::option::Option","orig_substs":["ty::u32"],"repr_transparent":false,"size":8,"variants":[{"ctor_kind":{"kind":"Const"},"discr":{"index":0,"kind":"Relative"},"discr_value":"0","fields":[],"inhabited":true,"name":"core/73237d41::option::Option::None"},{"ctor_kind":{"kind":"Fn"},"discr":{"index":1,"kind":"Relative"},"discr_value":"1","fields":[{"name":"core/73237d41::option::Option::Some::0","ty":"ty::u32"}],"inhabited":true,"name":"core/73237d41::option::Option::Some"}]},{"kind":{"discr_ty":"ty::isize","kind":"Enum"},"name":"test/f696fd3c::I::_adtb7803c2264daf0ec[0]","orig_def_id":"test/f696fd3c::I","orig_substs":[],"repr_transparent":false,"size":1,"variants":[{"ctor_kind":{"kind":"Const"},"discr":{"kind":"Explicit","name":"test/f696fd3c::I::I42::{constant#0}"},"discr_value":"42","fields":[],"inhabited":true,"name":"test/f696fd3c::I::I42"},{"ctor_kind":{"kind":"Const"},"discr":{"index":1,"kind":"Relative"},"discr_value":"43","fields":[],"inhabited":true,"name":"test/f696fd3c::I::I43"}]}],"statics":[],"vtables":[],"traits":[],"intrinsics":[{"inst":{"def_id":"test/f696fd3c::h_none","kind":"Item","substs":[]},"name":"test/f696fd3c::h_none"},{"inst":{"def_id":"test/f696fd3c::i42","kind":"Item","substs":[]},"name":"test/f696fd3c::i42"},{"inst":{"def_id":"test/f696fd3c::g","kind":"Item","substs":[]},"name":"test/f696fd3c::g"},{"inst":{"def_id":"test/f696fd3c::i43","kind":"Item","substs":[]},"name":"test/f696fd3c::i43"},{"inst":{"def_id":"test/f696fd3c::f","kind":"Item","substs":[]},"name":"test/f696fd3c::f"},{"inst":{"def_id":"test/f696fd3c::h_some","kind":"Item","substs":[]},"name":"test/f696fd3c::h_some"},{"inst":{"def_id":"test/f696fd3c::I::I42::{constant#0}","kind":"Item","substs":[]},"name":"test/f696fd3c::I::I42::{constant#0}"}],"tys":[{"name":"ty::u32","ty":{"kind":"Uint","uintkind":{"kind":"U32"}}},{"name":"ty::Adt::3fa7c2d95c7fce06","ty":{"kind":"Adt","name":"core/73237d41::option::Option::_adtc5e93708b8ca6e2a[0]","orig_def_id":"core/73237d41::option::Option","substs":["ty::u32"]}},{"name":"ty::Adt::7746688b48f54a60","ty":{"kind":"Adt","name":"test/f696fd3c::I::_adtb7803c2264daf0ec[0]","orig_def_id":"test/f696fd3c::I","substs":[]}},{"name":"ty::bool","ty":{"kind":"Bool"}},{"name":"ty::FnDef::935b79106a1ed847","ty":{"defid":"test/f696fd3c::f","kind":"FnDef"}},{"name":"ty::isize","ty":{"intkind":{"kind":"Isize"},"kind":"Int"}}],"roots":["test/f696fd3c::f","test/f696fd3c::g","test/f696fd3c::h_none","test/f696fd3c::h_some","test/f696fd3c::i42","test/f696fd3c::i43"]}
\ No newline at end of file
diff --git a/intTests/test_mir_verify_enums/test.rs b/intTests/test_mir_verify_enums/test.rs
new file mode 100644
index 0000000000..e4f25f1e2c
--- /dev/null
+++ b/intTests/test_mir_verify_enums/test.rs
@@ -0,0 +1,35 @@
+pub fn f(x: Option<u32>) -> u32 {
+    match x {
+        Some(x) => x,
+        None => 27,
+    }
+}
+
+pub fn g(b: bool) -> u32 {
+    if b {
+        f(None)
+    } else {
+        f(Some(42))
+    }
+}
+
+pub fn h_none() -> Option<u32> {
+    None
+}
+
+pub fn h_some(x: u32) -> Option<u32> {
+    Some(x)
+}
+
+pub enum I {
+    I42 = 42,
+    I43,
+}
+
+pub fn i42() -> I {
+    I::I42
+}
+
+pub fn i43() -> I {
+    I::I43
+}
diff --git a/intTests/test_mir_verify_enums/test.saw b/intTests/test_mir_verify_enums/test.saw
new file mode 100644
index 0000000000..aa5b84def5
--- /dev/null
+++ b/intTests/test_mir_verify_enums/test.saw
@@ -0,0 +1,78 @@
+enable_experimental;
+
+m <- mir_load_module "test.linked-mir.json";
+
+let option_u32_adt = mir_find_adt m "core::option::Option" [mir_u32];
+let i_adt = mir_find_adt m "test::I" [];
+
+let f_none_spec = do {
+  let x = mir_enum_value option_u32_adt "None" [];
+
+  mir_execute_func [x];
+
+  mir_return (mir_term {{ 27 : [32] }});
+};
+
+let f_some_spec = do {
+  let ret = mir_term {{ 42 : [32] }};
+  let x = mir_enum_value option_u32_adt "Some" [ret];
+
+  mir_execute_func [x];
+
+  mir_return ret;
+};
+
+let g_spec = do {
+  b <- mir_fresh_var "b" mir_bool;
+
+  mir_execute_func [mir_term b];
+
+  mir_return (mir_term {{ if b then 27 else 42 : [32] }});
+};
+
+let h_none_spec = do {
+  mir_execute_func [];
+
+  mir_return (mir_enum_value option_u32_adt "None" []);
+};
+
+let h_some_spec = do {
+  x <- mir_fresh_var "x" mir_u32;
+
+  mir_execute_func [mir_term x];
+
+  mir_return (mir_enum_value option_u32_adt "Some" [mir_term x]);
+};
+
+let i42_spec = do {
+  mir_execute_func [];
+
+  mir_return (mir_enum_value i_adt "I42" []);
+};
+
+let i43_spec = do {
+  mir_execute_func [];
+
+  mir_return (mir_enum_value i_adt "I43" []);
+};
+
+// `mir_enum_value` should error if it cannot find a variant name.
+let i43_bad_spec = do {
+  mir_execute_func [];
+
+  mir_return (mir_enum_value i_adt "I44" []);
+};
+
+f_none_ov <- mir_verify m "test::f" [] false f_none_spec z3;
+f_some_ov <- mir_verify m "test::f" [] false f_some_spec z3;
+
+mir_verify m "test::g" [f_none_ov, f_some_ov] false g_spec z3;
+
+mir_verify m "test::h_none" [] false h_none_spec z3;
+mir_verify m "test::h_some" [] false h_some_spec z3;
+
+mir_verify m "test::i42" [] false i42_spec z3;
+mir_verify m "test::i43" [] false i43_spec z3;
+fails (
+  mir_verify m "test::i43" [] false i43_bad_spec z3
+);
diff --git a/intTests/test_mir_verify_enums/test.sh b/intTests/test_mir_verify_enums/test.sh
new file mode 100755
index 0000000000..2315cc233c
--- /dev/null
+++ b/intTests/test_mir_verify_enums/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 1316e3e6ba..33b2dc02c2 100644
--- a/saw-remote-api/CHANGELOG.md
+++ b/saw-remote-api/CHANGELOG.md
@@ -35,6 +35,7 @@
 * Add `"slice"` and `"slice range"` `setup value`s representing slices in MIR
   verification. Attempting to use these in LLVM or JVM verification will raise
   an error.
+* Add `"enum"` `setup value`s representing enums in MIR verification.
 
 ## 1.0.0 -- 2023-06-26
 
diff --git a/saw-remote-api/python/CHANGELOG.md b/saw-remote-api/python/CHANGELOG.md
index 4892e5c863..947e644e3f 100644
--- a/saw-remote-api/python/CHANGELOG.md
+++ b/saw-remote-api/python/CHANGELOG.md
@@ -38,6 +38,7 @@
   variable. This function is currently only supported with LLVM and MIR
   verification, and using this function with JVM verification will raise an
   error.
+* Add an `enum()` function for constructing MIR enum values.
 
 ## 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 984d79cc62..93f9827310 100644
--- a/saw-remote-api/python/saw_client/crucible.py
+++ b/saw-remote-api/python/saw_client/crucible.py
@@ -154,6 +154,22 @@ def to_json(self) -> JSON:
                 'elements': [fld.to_json() for fld in self.fields],
                 'MIR ADT server name': self.mir_adt.server_name if self.mir_adt is not None else None}
 
+class EnumVal(SetupVal):
+    adt : MIRAdt
+    variant_name : str
+    fields : List[SetupVal]
+
+    def __init__(self, adt : MIRAdt, variant_name : str, fields : List[SetupVal]) -> None:
+        self.adt = adt
+        self.variant_name = variant_name
+        self.fields = fields
+
+    def to_json(self) -> JSON:
+        return {'setup value': 'enum',
+                'MIR ADT server name': self.adt.server_name,
+                'variant name': self.variant_name,
+                'elements': [fld.to_json() for fld in self.fields]}
+
 class TupleVal(SetupVal):
     fields : List[SetupVal]
 
@@ -766,6 +782,19 @@ def elem(base: SetupVal, index: int) -> SetupVal:
         raise ValueError('elem expected an int, but got {index!r}')
     return ElemVal(base, index)
 
+def enum(adt : MIRAdt, variant_name : str, *fields : SetupVal) -> SetupVal:
+    """Returns a MIR enum value (i.e., an ``EnumVal``) whose type corresponds to
+    the given ``adt``, whose variant corresponds to the given ``variant_name``,
+    and whose field values correspond to the given ``fields``.
+
+    At present, this is only supported with MIR verification. Using this
+    function with LLVM or JVM verification will raise an error.
+    """
+    for field in fields:
+        if not isinstance(field, SetupVal):
+            raise ValueError('enum expected a SetupVal, but got {field!r}')
+    return EnumVal(adt, variant_name, list(fields))
+
 def field(base : SetupVal, field_name : str) -> SetupVal:
     """Returns the value of struct ``base``'s field ``field_name`` (i.e., a ``FieldVal``).
 
diff --git a/saw-remote-api/python/tests/saw/test-files/mir_enums.linked-mir.json b/saw-remote-api/python/tests/saw/test-files/mir_enums.linked-mir.json
new file mode 100644
index 0000000000..d2a9e3e66c
--- /dev/null
+++ b/saw-remote-api/python/tests/saw/test-files/mir_enums.linked-mir.json
@@ -0,0 +1 @@
+{"fns":[{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::bool"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::bool"}},"pos":"mir_enums.rs:9:8: 9:9","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::bool"}},"kind":"Copy"}}}],"terminator":{"discr":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::bool"}},"kind":"Move"},"discr_span":"mir_enums.rs:9:8: 9:9 !mir_enums.rs:9:8: 9:9","kind":"SwitchInt","pos":"mir_enums.rs:9:8: 9:9 !mir_enums.rs:9:8: 9:9","switch_ty":"ty::bool","targets":["bb2","bb1"],"values":["0"]}},"blockid":"bb0"},{"block":{"data":[{"kind":"Deinit","pos":"mir_enums.rs:10:11: 10:15"},{"kind":"SetDiscriminant","lvalue":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::Adt::3fa7c2d95c7fce06"}},"pos":"mir_enums.rs:10:11: 10:15","variant_index":0}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::Adt::3fa7c2d95c7fce06"}},"kind":"Move"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"bb3"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::be69c9ad94113883"},"kind":"Constant"},"kind":"Call","pos":"mir_enums.rs:10:9: 10:16"}},"blockid":"bb1"},{"block":{"data":[{"kind":"Deinit","pos":"mir_enums.rs:12:11: 12:19"},{"kind":"Assign","lhs":{"data":[{"kind":"Downcast","variant":1},{"field":0,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::Adt::3fa7c2d95c7fce06"}},"pos":"mir_enums.rs:12:11: 12:19","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"uint","size":4,"val":"42"},"ty":"ty::u32"},"kind":"Constant"}}},{"kind":"SetDiscriminant","lvalue":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::Adt::3fa7c2d95c7fce06"}},"pos":"mir_enums.rs:12:11: 12:19","variant_index":1}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::Adt::3fa7c2d95c7fce06"}},"kind":"Move"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"bb3"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::be69c9ad94113883"},"kind":"Constant"},"kind":"Call","pos":"mir_enums.rs:12:9: 12:20"}},"blockid":"bb2"},{"block":{"data":[],"terminator":{"kind":"Return","pos":"mir_enums.rs:14:2: 14:2"}},"blockid":"bb3"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::bool"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::Adt::3fa7c2d95c7fce06"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::Adt::3fa7c2d95c7fce06"}]},"name":"mir_enums/284a9f79::g","return_ty":"ty::u32","spread_arg":null},{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[{"kind":"Deinit","pos":"mir_enums.rs:34:5: 34:11"},{"kind":"SetDiscriminant","lvalue":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::d1797ca6daa8927f"}},"pos":"mir_enums.rs:34:5: 34:11","variant_index":1}],"terminator":{"kind":"Return","pos":"mir_enums.rs:35:2: 35:2"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::d1797ca6daa8927f"}]},"name":"mir_enums/284a9f79::i43","return_ty":"ty::Adt::d1797ca6daa8927f","spread_arg":null},{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[{"kind":"Deinit","pos":"mir_enums.rs:17:5: 17:9"},{"kind":"SetDiscriminant","lvalue":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::3fa7c2d95c7fce06"}},"pos":"mir_enums.rs:17:5: 17:9","variant_index":0}],"terminator":{"kind":"Return","pos":"mir_enums.rs:18:2: 18:2"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::3fa7c2d95c7fce06"}]},"name":"mir_enums/284a9f79::h_none","return_ty":"ty::Adt::3fa7c2d95c7fce06","spread_arg":null},{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[{"kind":"Deinit","pos":"mir_enums.rs:30:5: 30:11"},{"kind":"SetDiscriminant","lvalue":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::d1797ca6daa8927f"}},"pos":"mir_enums.rs:30:5: 30:11","variant_index":0}],"terminator":{"kind":"Return","pos":"mir_enums.rs:31:2: 31:2"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::d1797ca6daa8927f"}]},"name":"mir_enums/284a9f79::i42","return_ty":"ty::Adt::d1797ca6daa8927f","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u32"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"}},"pos":"mir_enums.rs:21:10: 21:11","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u32"}},"kind":"Copy"}}},{"kind":"Deinit","pos":"mir_enums.rs:21:5: 21:12"},{"kind":"Assign","lhs":{"data":[{"kind":"Downcast","variant":1},{"field":0,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::3fa7c2d95c7fce06"}},"pos":"mir_enums.rs:21:5: 21:12","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"}},"kind":"Move"}}},{"kind":"SetDiscriminant","lvalue":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::3fa7c2d95c7fce06"}},"pos":"mir_enums.rs:21:5: 21:12","variant_index":1}],"terminator":{"kind":"Return","pos":"mir_enums.rs:22:2: 22:2"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::3fa7c2d95c7fce06"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"}]},"name":"mir_enums/284a9f79::h_some","return_ty":"ty::Adt::3fa7c2d95c7fce06","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Adt::3fa7c2d95c7fce06"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::isize"}},"pos":"mir_enums.rs:2:11: 2:12","rhs":{"kind":"Discriminant","ty":"ty::isize","val":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Adt::3fa7c2d95c7fce06"}}}}],"terminator":{"discr":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::isize"}},"kind":"Move"},"discr_span":"mir_enums.rs:3:9: 3:16","kind":"SwitchInt","pos":"mir_enums.rs:2:5: 2:12","switch_ty":"ty::isize","targets":["bb1","bb3","bb2"],"values":["0","1"]}},"blockid":"bb0"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"pos":"mir_enums.rs:4:17: 4:19","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"uint","size":4,"val":"27"},"ty":"ty::u32"},"kind":"Constant"}}}],"terminator":{"kind":"Goto","pos":"mir_enums.rs:4:17: 4:19","target":"bb4"}},"blockid":"bb1"},{"block":{"data":[],"terminator":{"kind":"Unreachable","pos":"mir_enums.rs:2:11: 2:12"}},"blockid":"bb2"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_3","ty":"ty::u32"}},"pos":"mir_enums.rs:3:14: 3:15","rhs":{"kind":"Use","usevar":{"data":{"data":[{"kind":"Downcast","variant":1},{"field":0,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Adt::3fa7c2d95c7fce06"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"pos":"mir_enums.rs:3:20: 3:21","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_3","ty":"ty::u32"}},"kind":"Copy"}}}],"terminator":{"kind":"Goto","pos":"mir_enums.rs:3:20: 3:21","target":"bb4"}},"blockid":"bb3"},{"block":{"data":[],"terminator":{"kind":"Return","pos":"mir_enums.rs:6:2: 6:2"}},"blockid":"bb4"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::isize"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_3","ty":"ty::u32"}]},"name":"mir_enums/284a9f79::f","return_ty":"ty::u32","spread_arg":null},{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::isize"}},"pos":"mir_enums.rs:25:11: 25:13","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"isize","size":8,"val":"42"},"ty":"ty::isize"},"kind":"Constant"}}}],"terminator":{"kind":"Return","pos":"mir_enums.rs:25:11: 25:13"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::isize"}]},"name":"mir_enums/284a9f79::I::I42::{constant#0}","return_ty":"ty::isize","spread_arg":null}],"adts":[{"kind":{"discr_ty":"ty::isize","kind":"Enum"},"name":"mir_enums/284a9f79::I::_adtb7803c2264daf0ec[0]","orig_def_id":"mir_enums/284a9f79::I","orig_substs":[],"repr_transparent":false,"size":1,"variants":[{"ctor_kind":{"kind":"Const"},"discr":{"kind":"Explicit","name":"mir_enums/284a9f79::I::I42::{constant#0}"},"discr_value":"42","fields":[],"inhabited":true,"name":"mir_enums/284a9f79::I::I42"},{"ctor_kind":{"kind":"Const"},"discr":{"index":1,"kind":"Relative"},"discr_value":"43","fields":[],"inhabited":true,"name":"mir_enums/284a9f79::I::I43"}]},{"kind":{"discr_ty":"ty::isize","kind":"Enum"},"name":"core/73237d41::option::Option::_adtc5e93708b8ca6e2a[0]","orig_def_id":"core/73237d41::option::Option","orig_substs":["ty::u32"],"repr_transparent":false,"size":8,"variants":[{"ctor_kind":{"kind":"Const"},"discr":{"index":0,"kind":"Relative"},"discr_value":"0","fields":[],"inhabited":true,"name":"core/73237d41::option::Option::None"},{"ctor_kind":{"kind":"Fn"},"discr":{"index":1,"kind":"Relative"},"discr_value":"1","fields":[{"name":"core/73237d41::option::Option::Some::0","ty":"ty::u32"}],"inhabited":true,"name":"core/73237d41::option::Option::Some"}]}],"statics":[],"vtables":[],"traits":[],"intrinsics":[{"inst":{"def_id":"mir_enums/284a9f79::g","kind":"Item","substs":[]},"name":"mir_enums/284a9f79::g"},{"inst":{"def_id":"mir_enums/284a9f79::i43","kind":"Item","substs":[]},"name":"mir_enums/284a9f79::i43"},{"inst":{"def_id":"mir_enums/284a9f79::h_none","kind":"Item","substs":[]},"name":"mir_enums/284a9f79::h_none"},{"inst":{"def_id":"mir_enums/284a9f79::i42","kind":"Item","substs":[]},"name":"mir_enums/284a9f79::i42"},{"inst":{"def_id":"mir_enums/284a9f79::h_some","kind":"Item","substs":[]},"name":"mir_enums/284a9f79::h_some"},{"inst":{"def_id":"mir_enums/284a9f79::f","kind":"Item","substs":[]},"name":"mir_enums/284a9f79::f"},{"inst":{"def_id":"mir_enums/284a9f79::I::I42::{constant#0}","kind":"Item","substs":[]},"name":"mir_enums/284a9f79::I::I42::{constant#0}"}],"tys":[{"name":"ty::bool","ty":{"kind":"Bool"}},{"name":"ty::u32","ty":{"kind":"Uint","uintkind":{"kind":"U32"}}},{"name":"ty::Adt::3fa7c2d95c7fce06","ty":{"kind":"Adt","name":"core/73237d41::option::Option::_adtc5e93708b8ca6e2a[0]","orig_def_id":"core/73237d41::option::Option","substs":["ty::u32"]}},{"name":"ty::FnDef::be69c9ad94113883","ty":{"defid":"mir_enums/284a9f79::f","kind":"FnDef"}},{"name":"ty::Adt::d1797ca6daa8927f","ty":{"kind":"Adt","name":"mir_enums/284a9f79::I::_adtb7803c2264daf0ec[0]","orig_def_id":"mir_enums/284a9f79::I","substs":[]}},{"name":"ty::isize","ty":{"intkind":{"kind":"Isize"},"kind":"Int"}}],"roots":["mir_enums/284a9f79::f","mir_enums/284a9f79::g","mir_enums/284a9f79::h_none","mir_enums/284a9f79::h_some","mir_enums/284a9f79::i42","mir_enums/284a9f79::i43"]}
\ No newline at end of file
diff --git a/saw-remote-api/python/tests/saw/test-files/mir_enums.rs b/saw-remote-api/python/tests/saw/test-files/mir_enums.rs
new file mode 100644
index 0000000000..e4f25f1e2c
--- /dev/null
+++ b/saw-remote-api/python/tests/saw/test-files/mir_enums.rs
@@ -0,0 +1,35 @@
+pub fn f(x: Option<u32>) -> u32 {
+    match x {
+        Some(x) => x,
+        None => 27,
+    }
+}
+
+pub fn g(b: bool) -> u32 {
+    if b {
+        f(None)
+    } else {
+        f(Some(42))
+    }
+}
+
+pub fn h_none() -> Option<u32> {
+    None
+}
+
+pub fn h_some(x: u32) -> Option<u32> {
+    Some(x)
+}
+
+pub enum I {
+    I42 = 42,
+    I43,
+}
+
+pub fn i42() -> I {
+    I::I42
+}
+
+pub fn i43() -> I {
+    I::I43
+}
diff --git a/saw-remote-api/python/tests/saw/test_mir_enums.py b/saw-remote-api/python/tests/saw/test_mir_enums.py
new file mode 100644
index 0000000000..490832140c
--- /dev/null
+++ b/saw-remote-api/python/tests/saw/test_mir_enums.py
@@ -0,0 +1,136 @@
+import unittest
+from pathlib import Path
+
+from saw_client import *
+from saw_client.crucible import cry_f, enum
+from saw_client.mir import Contract, MIRAdt, adt_ty, bool_ty, u32
+
+
+class FNoneContract(Contract):
+    adt: MIRAdt
+
+    def __init__(self, adt: MIRAdt):
+        super().__init__()
+        self.adt = adt
+
+    def specification(self) -> None:
+        x = enum(self.adt, 'None')
+
+        self.execute_func(x)
+
+        self.returns_f('27 : [32]')
+
+
+class FSomeContract(Contract):
+    adt: MIRAdt
+
+    def __init__(self, adt: MIRAdt):
+        super().__init__()
+        self.adt = adt
+
+    def specification(self) -> None:
+        ret = cry_f('42 : [32]')
+        x = enum(self.adt, 'Some', ret)
+
+        self.execute_func(x)
+
+        self.returns(ret)
+
+
+class GContract(Contract):
+    def specification(self) -> None:
+        b = self.fresh_var(bool_ty, 'b')
+
+        self.execute_func(b)
+
+        self.returns_f('if {b} then 27 else 42 : [32]')
+
+
+class HNoneContract(Contract):
+    adt: MIRAdt
+
+    def __init__(self, adt: MIRAdt):
+        super().__init__()
+        self.adt = adt
+
+    def specification(self) -> None:
+        self.execute_func()
+
+        self.returns(enum(self.adt, 'None'))
+
+
+class HSomeContract(Contract):
+    adt: MIRAdt
+
+    def __init__(self, adt: MIRAdt):
+        super().__init__()
+        self.adt = adt
+
+    def specification(self) -> None:
+        x = self.fresh_var(u32, 'x')
+
+        self.execute_func(x)
+
+        self.returns(enum(self.adt, 'Some', x))
+
+
+class I42Contract(Contract):
+    adt: MIRAdt
+
+    def __init__(self, adt: MIRAdt):
+        super().__init__()
+        self.adt = adt
+
+    def specification(self) -> None:
+        self.execute_func()
+
+        self.returns(enum(self.adt, 'I42'))
+
+
+class I43Contract(Contract):
+    adt: MIRAdt
+
+    def __init__(self, adt: MIRAdt):
+        super().__init__()
+        self.adt = adt
+
+    def specification(self) -> None:
+        self.execute_func()
+
+        self.returns(enum(self.adt, 'I43'))
+
+
+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_enums.linked-mir.json'))
+        mod = mir_load_module(json_name)
+
+        option_adt = mir_find_adt(mod, 'core::option::Option', u32)
+        i_adt = mir_find_adt(mod, "mir_enums::I")
+
+        f_none_ov = mir_verify(mod, 'mir_enums::f', FNoneContract(option_adt))
+        self.assertIs(f_none_ov.is_success(), True)
+
+        f_some_ov = mir_verify(mod, 'mir_enums::f', FSomeContract(option_adt))
+        self.assertIs(f_some_ov.is_success(), True)
+
+        g_result = mir_verify(mod, 'mir_enums::g', GContract(), lemmas=[f_none_ov, f_some_ov])
+        self.assertIs(g_result.is_success(), True)
+
+        h_none_result = mir_verify(mod, 'mir_enums::h_none', HNoneContract(option_adt))
+        self.assertIs(h_none_result.is_success(), True)
+
+        h_some_result = mir_verify(mod, 'mir_enums::h_some', HSomeContract(option_adt))
+        self.assertIs(h_some_result.is_success(), True)
+
+        i42_result = mir_verify(mod, 'mir_enums::i42', I42Contract(i_adt))
+        self.assertIs(i42_result.is_success(), True)
+
+        i43_result = mir_verify(mod, 'mir_enums::i43', I43Contract(i_adt))
+        self.assertIs(i43_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 d7b2f2942b..76a5600590 100644
--- a/saw-remote-api/src/SAWServer.hs
+++ b/saw-remote-api/src/SAWServer.hs
@@ -112,6 +112,7 @@ data CrucibleSetupVal ty e
     -- ^ The @'Maybe' 'ServerName'@ value represents a possible MIR
     -- ADT. This should always be 'Just' with MIR verification and
     -- 'Nothing' with LLVM or JVM verification.
+  | EnumValue ServerName String [CrucibleSetupVal ty e]
   | TupleValue [CrucibleSetupVal ty e]
   | SliceValue (CrucibleSetupVal ty e)
   | SliceRangeValue (CrucibleSetupVal ty e) Int Int
diff --git a/saw-remote-api/src/SAWServer/Data/SetupValue.hs b/saw-remote-api/src/SAWServer/Data/SetupValue.hs
index 13ae0bedbd..04cc3f0a25 100644
--- a/saw-remote-api/src/SAWServer/Data/SetupValue.hs
+++ b/saw-remote-api/src/SAWServer/Data/SetupValue.hs
@@ -14,6 +14,7 @@ data SetupValTag
   | TagCryptol
   | TagArrayValue
   | TagStructValue
+  | TagEnumValue
   | TagTupleValue
   | TagSliceValue
   | TagSliceRangeValue
@@ -34,6 +35,7 @@ instance FromJSON SetupValTag where
       "Cryptol" -> pure TagCryptol
       "array" -> pure TagArrayValue
       "struct" -> pure TagStructValue
+      "enum" -> pure TagEnumValue
       "tuple" -> pure TagTupleValue
       "slice" -> pure TagSliceValue
       "slice range" -> pure TagSliceRangeValue
@@ -57,6 +59,7 @@ instance (FromJSON ty, FromJSON cryptolExpr) => FromJSON (CrucibleSetupVal ty cr
           TagCryptol -> CryptolExpr <$> o .: "expression"
           TagArrayValue -> ArrayValue <$> o .:? "element type" <*> o .: "elements"
           TagStructValue -> StructValue <$> o .:? "MIR ADT server name" <*> o .: "elements"
+          TagEnumValue -> EnumValue <$> o .: "MIR ADT server name" <*> o .: "variant name" <*> o .: "elements"
           TagTupleValue -> TupleValue <$> o .: "elements"
           TagSliceValue -> SliceValue <$> o .: "base"
           TagSliceRangeValue -> SliceRangeValue <$> o .: "base" <*> o .: "start" <*> o .: "end"
diff --git a/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs b/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs
index c601974f4a..b6e94c2fc4 100644
--- a/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs
+++ b/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs
@@ -184,6 +184,8 @@ compileJVMContract fileReader bic cenv0 c =
       JVMSetupM $ fail "Array setup values unsupported in JVM API."
     getSetupVal _ (StructValue _ _) =
       JVMSetupM $ fail "Struct setup values unsupported in JVM API."
+    getSetupVal _ (EnumValue _ _ _) =
+      JVMSetupM $ fail "Enum setup values unsupported in JVM API."
     getSetupVal _ (TupleValue _) =
       JVMSetupM $ fail "Tuple setup values unsupported in JVM API."
     getSetupVal _ (SliceValue _) =
diff --git a/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs b/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs
index 6b05fe1d65..c091d0f029 100644
--- a/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs
+++ b/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs
@@ -190,6 +190,8 @@ compileLLVMContract fileReader bic ghostEnv cenv0 c =
       LLVMCrucibleSetupM $ fail "Tuple setup values unsupported in the LLVM API."
     getSetupVal _ (SliceValue _) =
       LLVMCrucibleSetupM $ fail "Slice setup values unsupported in the LLVM API."
+    getSetupVal _ (EnumValue _ _ _) =
+      LLVMCrucibleSetupM $ fail "Enum setup values unsupported in the LLVM API."
     getSetupVal _ (SliceRangeValue _ _ _) =
       LLVMCrucibleSetupM $ fail "Slice range setup values unsupported in the LLVM API."
     getSetupVal env (FieldLValue base fld) =
diff --git a/saw-remote-api/src/SAWServer/MIRCrucibleSetup.hs b/saw-remote-api/src/SAWServer/MIRCrucibleSetup.hs
index a1ce2f07d3..62e31fce5e 100644
--- a/saw-remote-api/src/SAWServer/MIRCrucibleSetup.hs
+++ b/saw-remote-api/src/SAWServer/MIRCrucibleSetup.hs
@@ -19,6 +19,7 @@ import Data.Map (Map)
 import qualified Data.Map as Map
 
 import Mir.Intrinsics (MIR)
+import qualified Mir.Mir as Mir
 
 import qualified Cryptol.Parser.AST as P
 import Cryptol.Utils.Ident (mkIdent)
@@ -30,6 +31,7 @@ import SAWScript.Crucible.MIR.Builtins
       mir_alloc_mut,
       mir_fresh_expanded_value,
       mir_fresh_var,
+      mir_enum_value,
       mir_execute_func,
       mir_load_module,
       mir_points_to,
@@ -188,14 +190,14 @@ compileMIRContract fileReader bic cenv0 sawenv c =
              return $ MS.SetupArray ty' (elt':eltss')
     getSetupVal _ (StructValue Nothing _) =
       MIRSetupM $ fail "MIR struct without a corresponding ADT."
-    getSetupVal env (StructValue (Just adtServerName) elts) =
-      -- First, we look up the MIR ADT from its ServerName. If we find it,
-      -- proceed to handle the struct field types. Otherwise, raise an error.
-      case getMIRAdtEither sawenv adtServerName of
-        Left ex -> throw ex
-        Right adt -> do
-          elts' <- mapM (getSetupVal env) elts
-          pure $ MS.SetupStruct adt elts'
+    getSetupVal env (StructValue (Just adtServerName) elts) = do
+      adt <- getMirAdt adtServerName
+      elts' <- mapM (getSetupVal env) elts
+      pure $ MS.SetupStruct adt elts'
+    getSetupVal env (EnumValue adtServerName variantName elts) = do
+      adt <- getMirAdt adtServerName
+      elts' <- mapM (getSetupVal env) elts
+      MIRSetupM $ mir_enum_value adt variantName elts'
     getSetupVal env (TupleValue elems) = do
       elems' <- mapM (getSetupVal env) elems
       pure $ MS.SetupTuple () elems'
@@ -221,6 +223,10 @@ compileMIRContract fileReader bic cenv0 sawenv c =
     getSetupVal _ (ElementLValue _ _) =
       MIRSetupM $ fail "Element l-values unsupported in the MIR API."
 
+    getMirAdt :: ServerName -> MIRSetupM Mir.Adt
+    getMirAdt adtServerName =
+      either throw pure $ getMIRAdtEither sawenv adtServerName
+
 data MIRLoadModuleParams
   = MIRLoadModuleParams ServerName FilePath
 
diff --git a/saw-script.cabal b/saw-script.cabal
index 2b52c55716..7804376543 100644
--- a/saw-script.cabal
+++ b/saw-script.cabal
@@ -54,6 +54,7 @@ library
     , haskeline
     , heapster-saw
     , hobbits >= 1.3.1
+    , indexed-traversable
     , galois-dwarf >= 0.2.2
     , IfElse
     , jvm-parser
diff --git a/src/SAWScript/Crucible/Common/MethodSpec.hs b/src/SAWScript/Crucible/Common/MethodSpec.hs
index e8ce39d657..e198622d5e 100644
--- a/src/SAWScript/Crucible/Common/MethodSpec.hs
+++ b/src/SAWScript/Crucible/Common/MethodSpec.hs
@@ -142,7 +142,8 @@ import           Verifier.SAW.SharedTerm as SAWVerifier
 import           SAWScript.Crucible.Common.Setup.Value
 import           SAWScript.Crucible.LLVM.Setup.Value (LLVM)
 import           SAWScript.Crucible.JVM.Setup.Value ()
-import           SAWScript.Crucible.MIR.Setup.Value (MirSetupSlice(..))
+import           SAWScript.Crucible.MIR.Setup.Value
+  (MirSetupEnum(..), MirSetupSlice(..))
 import           SAWScript.Options
 import           SAWScript.Prover.SolverStats
 import           SAWScript.Utils (bullets)
@@ -196,6 +197,14 @@ ppSetupValue setupval = case setupval of
         absurd empty
       (MIRExt, _defId) ->
         ppSetupStructDefault vs
+  SetupEnum x ->
+    case (ext, x) of
+      (LLVMExt, empty) ->
+        absurd empty
+      (JVMExt, empty) ->
+        absurd empty
+      (MIRExt, enum_) ->
+        ppMirSetupEnum enum_
   SetupTuple x vs ->
     case (ext, x) of
       (LLVMExt, empty) ->
@@ -242,12 +251,18 @@ ppSetupValue setupval = case setupval of
       | packed    = PP.angles (ppSetupStructDefault vs)
       | otherwise = ppSetupStructDefault vs
 
-    ppSetupStructDefault :: [SetupValue ext] -> PP.Doc ann
+    ppSetupStructDefault :: forall ext'. IsExt ext' => [SetupValue ext'] -> PP.Doc ann
     ppSetupStructDefault vs = PP.braces (commaList (map ppSetupValue vs))
 
     ppSetupTuple :: [SetupValue MIR] -> PP.Doc ann
     ppSetupTuple vs = PP.parens (commaList (map ppSetupValue vs))
 
+    ppMirSetupEnum :: MirSetupEnum -> PP.Doc ann
+    ppMirSetupEnum (MirSetupEnumVariant _defId variantName _discr _varIdx fields) =
+      PP.pretty variantName PP.<+> ppSetupStructDefault fields
+    ppMirSetupEnum (MirSetupEnumSymbolic _defId) =
+      PP.pretty "<symbolic enum>"
+
     ppMirSetupSlice :: MirSetupSlice -> PP.Doc ann
     ppMirSetupSlice (MirSetupSliceRaw ref len) =
       PP.pretty "SliceRaw" <> ppSetupTuple [ref, len]
diff --git a/src/SAWScript/Crucible/Common/Setup/Value.hs b/src/SAWScript/Crucible/Common/Setup/Value.hs
index 505acce1c9..fca67f5fd3 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
+  , XSetupEnum
   , XSetupTuple
   , XSetupSlice
   , XSetupArray
@@ -123,6 +124,7 @@ type family ResolvedState ext :: Type
 
 type family XSetupNull ext
 type family XSetupStruct ext
+type family XSetupEnum ext
 type family XSetupTuple ext
 type family XSetupSlice ext
 type family XSetupArray ext
@@ -153,6 +155,9 @@ data SetupValue ext where
   -- | A slice value. At the moment, this is only ever used for MIR
   -- verification.
   SetupSlice :: XSetupSlice ext -> SetupValue ext
+  -- | An enumeration value. At the moment, this is only ever used for MIR
+  -- verification.
+  SetupEnum :: XSetupEnum ext -> SetupValue ext
 
   -- | A pointer to a global variable
   SetupGlobal :: XSetupGlobal ext -> String -> SetupValue ext
@@ -168,6 +173,7 @@ data SetupValue ext where
 type SetupValueHas (c :: Type -> Constraint) ext =
   ( c (XSetupNull ext)
   , c (XSetupStruct ext)
+  , c (XSetupEnum ext)
   , c (XSetupTuple ext)
   , c (XSetupSlice ext)
   , c (XSetupArray ext)
diff --git a/src/SAWScript/Crucible/JVM/Override.hs b/src/SAWScript/Crucible/JVM/Override.hs
index 258249647c..fb0ff1e0ef 100644
--- a/src/SAWScript/Crucible/JVM/Override.hs
+++ b/src/SAWScript/Crucible/JVM/Override.hs
@@ -560,6 +560,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.SetupEnum   empty   -> absurd empty
     MS.SetupTuple  empty _ -> absurd empty
     MS.SetupSlice  empty   -> absurd empty
 
@@ -952,6 +953,7 @@ instantiateSetupValue sc s v =
     MS.SetupNull ()                   -> return v
     MS.SetupGlobal empty _            -> absurd empty
     MS.SetupStruct empty _            -> absurd empty
+    MS.SetupEnum empty                -> absurd empty
     MS.SetupTuple empty _             -> absurd empty
     MS.SetupSlice empty               -> absurd empty
     MS.SetupArray empty _             -> absurd empty
diff --git a/src/SAWScript/Crucible/JVM/ResolveSetupValue.hs b/src/SAWScript/Crucible/JVM/ResolveSetupValue.hs
index 9364b7716c..98f38a0d14 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.SetupEnum empty                -> absurd empty
     MS.SetupTuple empty _             -> absurd empty
     MS.SetupSlice empty               -> absurd empty
     MS.SetupArray empty _             -> absurd empty
@@ -173,6 +174,7 @@ resolveSetupVal cc env _tyenv _nameEnv val =
       return (RVal (W4.maybePartExpr sym Nothing))
     MS.SetupGlobal empty _            -> absurd empty
     MS.SetupStruct empty _            -> absurd empty
+    MS.SetupEnum empty                -> absurd empty
     MS.SetupTuple empty _             -> absurd empty
     MS.SetupSlice empty               -> absurd empty
     MS.SetupArray empty _             -> absurd empty
diff --git a/src/SAWScript/Crucible/JVM/Setup/Value.hs b/src/SAWScript/Crucible/JVM/Setup/Value.hs
index 8286704750..ba50ba6dee 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.XSetupEnum CJ.JVM = Void
 type instance MS.XSetupTuple CJ.JVM = Void
 type instance MS.XSetupSlice CJ.JVM = Void
 type instance MS.XSetupArray CJ.JVM = Void
diff --git a/src/SAWScript/Crucible/LLVM/Override.hs b/src/SAWScript/Crucible/LLVM/Override.hs
index f28768f11b..8718a712a7 100644
--- a/src/SAWScript/Crucible/LLVM/Override.hs
+++ b/src/SAWScript/Crucible/LLVM/Override.hs
@@ -1010,6 +1010,7 @@ matchPointsTos opts sc cc spec prepost = go False []
       case v of
         SetupVar i                 -> Set.singleton i
         SetupStruct _ xs           -> foldMap setupVars xs
+        SetupEnum  empty           -> absurd empty
         SetupTuple empty _         -> absurd empty
         SetupSlice empty           -> absurd empty
         SetupArray _ xs            -> foldMap setupVars xs
@@ -1193,6 +1194,8 @@ matchArg opts sc cc cs prepost md actual expectedTy expected =
                               (V.toList (Crucible.fiType <$> Crucible.siFields fields))
                               zs ]
 
+    (_, _, SetupEnum empty) ->
+      absurd empty
     (_, _, SetupTuple empty _) ->
       absurd empty
     (_, _, SetupSlice empty) ->
@@ -2380,6 +2383,7 @@ instantiateSetupValue sc s v =
     SetupNull{}              -> return v
     SetupGlobal{}            -> return v
     SetupGlobalInitializer{} -> return v
+    SetupEnum  empty         -> absurd empty
     SetupTuple empty _       -> absurd empty
     SetupSlice empty         -> absurd empty
   where
diff --git a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs
index 84b29b9784..b5fd1bdbf6 100644
--- a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs
+++ b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs
@@ -451,6 +451,8 @@ typeOfSetupValue cc env nameEnv val =
          let si = Crucible.mkStructInfo dl packed memTys
          return (Crucible.StructType si)
 
+    SetupEnum empty ->
+      absurd empty
     SetupTuple empty _ ->
       absurd empty
     SetupSlice empty ->
@@ -632,6 +634,8 @@ resolveSetupVal cc mem env tyenv nameEnv val =
                    Crucible.Struct v -> v
                    _ -> error "impossible"
       return $ Crucible.LLVMValStruct (V.zip flds (V.fromList vals))
+    SetupEnum empty ->
+      absurd empty
     SetupTuple empty _ ->
       absurd empty
     SetupSlice empty ->
diff --git a/src/SAWScript/Crucible/LLVM/Setup/Value.hs b/src/SAWScript/Crucible/LLVM/Setup/Value.hs
index ac5baba510..55b2abc27c 100644
--- a/src/SAWScript/Crucible/LLVM/Setup/Value.hs
+++ b/src/SAWScript/Crucible/LLVM/Setup/Value.hs
@@ -120,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.XSetupEnum (LLVM _) = Void
 type instance Setup.XSetupTuple (LLVM _) = Void
 type instance Setup.XSetupSlice (LLVM _) = Void
 type instance Setup.XSetupArray (LLVM _) = ()
diff --git a/src/SAWScript/Crucible/MIR/Builtins.hs b/src/SAWScript/Crucible/MIR/Builtins.hs
index 341e6dac0c..deb53ff676 100644
--- a/src/SAWScript/Crucible/MIR/Builtins.hs
+++ b/src/SAWScript/Crucible/MIR/Builtins.hs
@@ -25,6 +25,8 @@ module SAWScript.Crucible.MIR.Builtins
   , mir_return
   , mir_unsafe_assume_spec
   , mir_verify
+    -- ** MIR enums
+  , mir_enum_value
     -- ** MIR slices
   , mir_slice_value
   , mir_slice_range_value
@@ -63,8 +65,9 @@ import Control.Monad.State (MonadState(..), StateT(..), execStateT, gets)
 import Control.Monad.Trans.Class (MonadTrans(..))
 import qualified Data.ByteString.Lazy as BSL
 import Data.Foldable (for_)
+import qualified Data.Foldable.WithIndex as FWI
 import Data.IORef
-import qualified Data.List as List (find)
+import qualified Data.List.Extra as List (find, unsnoc)
 import qualified Data.List.NonEmpty as NE
 import Data.List.NonEmpty (NonEmpty(..))
 import qualified Data.Map as Map
@@ -328,6 +331,23 @@ constructExpandedSetupValue cc sc = go
                   adt_not_found_panic "StructShape" adtName
             _ ->
               non_adt_type_panic "StructShape" ty
+        EnumShape ty _ _ _ ->
+          case ty of
+            Mir.TyAdt adtName _ _ ->
+              case col ^. Mir.adts . at adtName of
+                Just adt@(Mir.Adt _ kind _ _ _ _ _) ->
+                  case kind of
+                    Mir.Enum _ ->
+                      pure $ MS.SetupEnum $ MirSetupEnumSymbolic adt
+                    _ ->
+                      panic "constructExpandedSetupValue"
+                            [ "Expected enum, encountered " ++
+                              show kind
+                            ]
+                Nothing ->
+                  adt_not_found_panic "EnumShape" adtName
+            _ ->
+              non_adt_type_panic "EnumShape" ty
         TransparentShape ty shp' ->
           case ty of
             Mir.TyAdt adtName _ _ -> do
@@ -338,7 +358,7 @@ constructExpandedSetupValue cc sc = go
                       val <- go pfx shp'
                       pure $ MS.SetupStruct adt [val]
                     Mir.Enum{} ->
-                      fail "`repr(transparent)` enums not currently supported"
+                      pure $ MS.SetupEnum $ MirSetupEnumSymbolic adt
                     Mir.Union ->
                       panic "constructExpandedSetupValue"
                             [ "Unexpected `repr(transparent)` union:"
@@ -587,6 +607,58 @@ mir_verify rm nm lemmas checkSat setup tactic =
      ps <- io (MS.mkProvedSpec MS.SpecProved methodSpec stats vcstats lemmaSet diff)
      returnProof ps
 
+-----
+-- MIR enums
+-----
+
+-- | Construct a specific enum variant. This does a light amount of validity
+-- checking, which is the only reason that this function is monadic.
+mir_enum_value ::
+  X.MonadThrow m =>
+  Mir.Adt ->
+  String ->
+  [MS.SetupValue MIR] ->
+  m (MS.SetupValue MIR)
+mir_enum_value adt variantNm vs =
+  -- MIRSetupM $
+  case adt of
+    Mir.Adt adtNm (Mir.Enum _) variants _ _ _ _ -> do
+      (variantIdx, variant) <-
+        case FWI.ifind (\_ v -> variantDefIdMatches (v ^. Mir.vname)) variants of
+          Just iv ->
+            pure iv
+          Nothing ->
+            X.throwM $ MIREnumValueVariantNotFound adtNm variantNm
+      discr <-
+        case variant ^. Mir.discrval of
+          Just discr -> pure discr
+          Nothing ->
+            panic "mir_enum_value"
+                  [ "discrval not set for variant:"
+                  , show (variant ^. Mir.vname)
+                  ]
+      pure $ MS.SetupEnum $ MirSetupEnumVariant adt variant discr variantIdx vs
+    Mir.Adt adtNm Mir.Struct _ _ _ _ _ ->
+      X.throwM $ MIREnumValueNonEnum adtNm "struct"
+    Mir.Adt adtNm Mir.Union _ _ _ _ _ ->
+      X.throwM $ MIREnumValueNonEnum adtNm "union"
+  where
+    variantNmText :: Text
+    variantNmText = Text.pack variantNm
+
+    -- Check if the user-supplied String argument matches the name of the given
+    -- variant's DefId. For instance, the variant might be named
+    -- @core::option[0]::Option[0]::Some[0]@, but the user will simply write
+    -- @Some@, so this function decomposes the DefId to retrieve the @Some@
+    -- portion.
+    variantDefIdMatches :: Mir.DefId -> Bool
+    variantDefIdMatches variantDefId
+      | Just (_, (variantNmText', _idx)) <- List.unsnoc (variantDefId ^. Mir.didPath)
+      = variantNmText == variantNmText'
+
+      | otherwise
+      = False
+
 -----
 -- MIR slices
 -----
@@ -1363,6 +1435,8 @@ data MIRSetupError
   | MIRArgNumberWrong Int Int -- number expected, number found
   | MIRReturnUnexpected Mir.Ty -- found
   | MIRReturnTypeMismatch Mir.Ty Mir.Ty -- expected, found
+  | MIREnumValueVariantNotFound Mir.DefId String
+  | MIREnumValueNonEnum Mir.DefId String -- The String is either \"struct\" or \"union\"
 
 instance X.Exception MIRSetupError where
   toException = topLevelExceptionToException
@@ -1400,3 +1474,13 @@ instance Show MIRSetupError where
         , "Expected type: " ++ show (PP.pretty expected)
         , "Given type:    " ++ show (PP.pretty found)
         ]
+      MIREnumValueVariantNotFound adtNm variantNm ->
+        unlines
+        [ "mir_enum_value: Could not find a variant named `" ++ variantNm ++ "`"
+        , "in the enum " ++ show adtNm
+        ]
+      MIREnumValueNonEnum adtNm what ->
+        unlines
+        [ "mir_enum_value: Expected enum, received " ++ what
+        , show adtNm
+        ]
diff --git a/src/SAWScript/Crucible/MIR/MethodSpecIR.hs b/src/SAWScript/Crucible/MIR/MethodSpecIR.hs
index b66b3cc02a..ea4480c1e4 100644
--- a/src/SAWScript/Crucible/MIR/MethodSpecIR.hs
+++ b/src/SAWScript/Crucible/MIR/MethodSpecIR.hs
@@ -47,6 +47,9 @@ module SAWScript.Crucible.MIR.MethodSpecIR
     -- * @MIRMethodSpec@
   , MIRMethodSpec
 
+    -- * @MirSetupEnum@
+  , MirSetupEnum(..)
+
     -- * @MirSetupSlice@
   , MirSetupSlice(..)
 
diff --git a/src/SAWScript/Crucible/MIR/Override.hs b/src/SAWScript/Crucible/MIR/Override.hs
index bea3d78edf..980dc5a3fa 100644
--- a/src/SAWScript/Crucible/MIR/Override.hs
+++ b/src/SAWScript/Crucible/MIR/Override.hs
@@ -67,6 +67,7 @@ import qualified Mir.TransTy as Mir
 import qualified What4.Expr as W4
 import qualified What4.Interface as W4
 import qualified What4.LabeledPred as W4
+import qualified What4.Partial as W4
 import qualified What4.ProgramLoc as W4
 
 import Verifier.SAW.Prelude (scEq)
@@ -905,6 +906,7 @@ instantiateSetupValue sc s v =
     MS.SetupTerm tt                   -> MS.SetupTerm <$> doTerm tt
     MS.SetupArray elemTy vs           -> MS.SetupArray elemTy <$> mapM (instantiateSetupValue sc s) vs
     MS.SetupStruct did vs             -> MS.SetupStruct did <$> mapM (instantiateSetupValue sc s) vs
+    MS.SetupEnum enum_                -> MS.SetupEnum <$> instantiateSetupEnum enum_
     MS.SetupTuple x vs                -> MS.SetupTuple x <$> mapM (instantiateSetupValue sc s) vs
     MS.SetupSlice slice               -> MS.SetupSlice <$> instantiateSetupSlice slice
     MS.SetupNull empty                -> absurd empty
@@ -917,6 +919,13 @@ instantiateSetupValue sc s v =
   where
     doTerm (TypedTerm schema t) = TypedTerm schema <$> scInstantiateExt sc s t
 
+    instantiateSetupEnum :: MirSetupEnum -> IO MirSetupEnum
+    instantiateSetupEnum (MirSetupEnumVariant adt variant discr variantIdx vs) =
+      MirSetupEnumVariant adt variant discr variantIdx <$>
+      mapM (instantiateSetupValue sc s) vs
+    instantiateSetupEnum v'@(MirSetupEnumSymbolic _adt) =
+      return v'
+
     instantiateSetupSlice :: MirSetupSlice -> IO MirSetupSlice
     instantiateSetupSlice (MirSetupSliceRaw ref len) =
       MirSetupSliceRaw
@@ -1032,6 +1041,7 @@ learnSetupCondition _opts _ _ _ _ (MS.SetupCond_Ghost empty _ _ _) = absurd empt
 
 -- | Match the value of a function argument with a symbolic 'SetupValue'.
 matchArg ::
+  forall w.
   Options          {- ^ saw script print out opts -} ->
   SharedContext      {- ^ context for constructing SAW terms    -} ->
   MIRCrucibleContext    {- ^ context for interacting with Crucible -} ->
@@ -1082,40 +1092,77 @@ matchArg opts sc cc cs prepost md actual expectedTy expected =
     (MIRVal (StructShape _ _ xsFldShps) (Crucible.AnyValue tpr@(Crucible.StructRepr _) xs),
      Mir.TyAdt _ _ _,
      MS.SetupStruct adt zs)
-      | Ctx.sizeInt (Ctx.size xs) == length zs
-      , let xsTpr = Crucible.StructRepr (FC.fmapFC fieldShapeType xsFldShps)
+      | let xsTpr = Crucible.StructRepr (FC.fmapFC fieldShapeType xsFldShps)
       , Just Refl <- W4.testEquality tpr xsTpr ->
         case adt of
-          Mir.Adt _ Mir.Struct [v] _ _ _ _ ->
-            let ys = v ^.. Mir.vfields . each . Mir.fty in
-            sequence_
-              [ case xFldShp of
-                  ReqField shp ->
-                    matchArg opts sc cc cs prepost md (MIRVal shp x) y z
-                  OptField shp -> do
-                    let x' = 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 ]
-          Mir.Adt _ ak _ _ _ _ _ ->
-            panic "matchArg" ["AdtKind " ++ show ak ++ " not yet implemented"]
+          Mir.Adt nm Mir.Struct variants _ _ _ _ -> do
+            variant <-
+              case variants of
+                [variant] ->
+                  pure variant
+                _ ->
+                  panic "matchArg"
+                        [ "Encountered struct Adt with " ++
+                          show (length variants) ++
+                          " variants:"
+                        , show nm
+                        ]
+            let ys = variant ^.. Mir.vfields . each . Mir.fty
+            matchFields sym xsFldShps xs ys zs
+          Mir.Adt nm (Mir.Enum _) _ _ _ _ _ ->
+            panic "matchArg"
+                  [ "Expected struct type, received enum:"
+                  , show nm
+                  ]
+          Mir.Adt nm Mir.Union _ _ _ _ _ ->
+            panic "matchArg"
+                  [ "Expected struct type, received union:"
+                  , show nm
+                  ]
+
+    (MIRVal (EnumShape _ variantShps _ discrShp)
+            (Crucible.AnyValue
+              (Mir.RustEnumRepr discrTpr variantCtx)
+              (Ctx.Empty
+                Ctx.:> Crucible.RV actualDiscr
+                Ctx.:> Crucible.RV variantAssn)),
+     _,
+     MS.SetupEnum enum_)
+      | Just Refl <- W4.testEquality (shapeType discrShp) discrTpr
+      , Just Refl <- W4.testEquality (FC.fmapFC variantShapeType variantShps) variantCtx ->
+        case enum_ of
+          -- match the fields of a particular enum variant point-wise
+          MirSetupEnumVariant adt variant discr variantIdxInt zs -> do
+            Some variantIdx <- pure $
+              variantIntIndex (adt ^. Mir.adtname) variantIdxInt (Ctx.size variantAssn)
+            VariantShape _ xsFldShps <- pure $ variantShps Ctx.! variantIdx
+            let Crucible.VB expectedVariant = variantAssn Ctx.! variantIdx
+            let ys = variant ^.. Mir.vfields . each . Mir.fty
+
+            -- Ensure that the discriminant values match.
+            IsBVShape _ discrW <- pure $ testDiscriminantIsBV discrShp
+            expectedDiscr <- liftIO $
+              W4.bvLit sym discrW $ BV.mkBV discrW discr
+            discrEq <- liftIO $
+              W4.bvEq sym expectedDiscr actualDiscr
+            addAssert discrEq md =<< notEq
+
+            -- Ensure that the variant is defined, i.e., that the predicate in
+            -- the underlying PartialExpr holds.
+            (xsPred, xs) <-
+              case expectedVariant of
+                W4.PE xsPred xs -> pure (xsPred, xs)
+                W4.Unassigned -> fail_
+            addAssert xsPred md =<< notEq
+
+            -- Finally, ensure that the fields match point-wise.
+            matchFields sym xsFldShps xs ys zs
+          MirSetupEnumSymbolic{} ->
+            error "TODO RGS: Symbolic enums"
 
     -- 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
-              let x' = 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
-        ]
+      matchFields sym xsFldShps xs ys zs
 
     -- Match the parts of a slice point-wise
     (MIRVal (SliceShape _ actualElemTy actualMutbl actualElemTpr)
@@ -1190,8 +1237,36 @@ matchArg opts sc cc cs prepost md actual expectedTy expected =
     nameEnv  = MS.csTypeNames cs
 
     loc   = MS.conditionLoc md
+
+    fail_ :: OverrideMatcher MIR w a
     fail_ = failure loc =<<
               mkStructuralMismatch opts cc sc cs actual expected expectedTy
+
+    -- Match the fields (point-wise) in a tuple, a struct, or enum variant.
+    matchFields ::
+      Sym ->
+      Ctx.Assignment FieldShape ctx ->
+      Ctx.Assignment (Crucible.RegValue' Sym) ctx ->
+      [Mir.Ty] ->
+      [SetupValue] ->
+      OverrideMatcher MIR w ()
+    matchFields sym xsFldShps xs ys zs = do
+      -- As a sanity check, first ensure that the number of fields matches
+      -- what is expected.
+      unless (Ctx.sizeInt (Ctx.size xs) == length zs) fail_
+      -- Then match the fields point-wise.
+      sequence_
+        [ case xFldShp of
+            ReqField shp ->
+              matchArg opts sc cc cs prepost md (MIRVal shp x) y z
+            OptField shp -> do
+              let x' = 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 ]
+
     notEq = notEqual prepost opts loc cc sc cs expected actual
 
     iTypes :: Crucible.IntrinsicTypes Sym
@@ -1251,6 +1326,7 @@ matchPointsTos opts sc cc spec prepost = go False []
       case v of
         MS.SetupVar i                     -> Set.singleton i
         MS.SetupStruct _ xs               -> foldMap setupVars xs
+        MS.SetupEnum enum_                -> setupEnum enum_
         MS.SetupTuple _ xs                -> foldMap setupVars xs
         MS.SetupSlice slice               -> setupSlice slice
         MS.SetupArray _ xs                -> foldMap setupVars xs
@@ -1263,6 +1339,13 @@ matchPointsTos opts sc cc spec prepost = go False []
         MS.SetupUnion empty _ _           -> absurd empty
         MS.SetupNull empty                -> absurd empty
 
+    -- Compute the set of variable identifiers in a 'MirSetupEnum'
+    setupEnum :: MirSetupEnum -> Set AllocIndex
+    setupEnum (MirSetupEnumVariant _ _ _ _ xs) =
+      foldMap setupVars xs
+    setupEnum (MirSetupEnumSymbolic _) =
+      Set.empty
+
     -- Compute the set of variable identifiers in a 'MirSetupSlice'
     setupSlice :: MirSetupSlice -> Set AllocIndex
     setupSlice (MirSetupSliceRaw ref len) =
diff --git a/src/SAWScript/Crucible/MIR/ResolveSetupValue.hs b/src/SAWScript/Crucible/MIR/ResolveSetupValue.hs
index 1426e62f02..2993253f5e 100644
--- a/src/SAWScript/Crucible/MIR/ResolveSetupValue.hs
+++ b/src/SAWScript/Crucible/MIR/ResolveSetupValue.hs
@@ -29,10 +29,15 @@ module SAWScript.Crucible.MIR.ResolveSetupValue
   , mirAdtToTy
   , findDefId
   , findDefIdEither
+    -- * Static items
   , findStatic
   , findStaticInitializer
   , findStaticVar
   , staticRefMux
+    -- * Enum discriminants
+  , testDiscriminantIsBV
+  , variantIntIndex
+    -- * Types of errors
   , MIRTypeOfError(..)
   ) where
 
@@ -45,6 +50,7 @@ import qualified Data.BitVector.Sized as BV
 import qualified Data.Foldable as F
 import qualified Data.Functor.Product as Functor
 import           Data.Kind (Type)
+import qualified Data.List.Extra as List (firstJust)
 import           Data.List.NonEmpty (NonEmpty(..))
 import           Data.Map (Map)
 import qualified Data.Map as Map
@@ -67,7 +73,9 @@ import qualified Cryptol.TypeCheck.AST as Cryptol (Type, Schema(..))
 import qualified Cryptol.Utils.PP as Cryptol (pp)
 import Lang.Crucible.Backend (IsSymInterface)
 import Lang.Crucible.Simulator
-  ( AnyValue(..), GlobalVar(..), RegValue, RegValue'(..), SymGlobalState )
+  ( AnyValue(..), GlobalVar(..), RegValue, RegValue'(..), SymGlobalState
+  , VariantBranch(..), injectVariant
+  )
 import Lang.Crucible.Types (MaybeType, TypeRepr(..))
 import qualified Mir.DefId as Mir
 import qualified Mir.FancyMuxTree as Mir
@@ -115,7 +123,7 @@ ppMIRVal sym (MIRVal shp val) =
     PrimShape _ _ ->
       W4.printSymExpr val
     TupleShape _ _ fldShp ->
-      PP.parens $ prettyStructOrTuple fldShp val
+      PP.parens $ prettyAdtOrTuple fldShp val
     ArrayShape _ _ shp' ->
       case val of
         Mir.MirVector_Vector vec ->
@@ -130,10 +138,22 @@ ppMIRVal sym (MIRVal shp val) =
     StructShape _ _ fldShp
       |  AnyValue (StructRepr fldTpr) fldVals <- val
       ,  Just Refl <- W4.testEquality (FC.fmapFC fieldShapeType fldShp) fldTpr
-      -> PP.braces $ prettyStructOrTuple fldShp fldVals
+      -> PP.braces $ prettyAdtOrTuple fldShp fldVals
 
       | otherwise
       -> error "Malformed MIRVal struct"
+    EnumShape _ variantShps _ _
+      |  AnyValue (Mir.RustEnumRepr _ variantCtx)
+                  (Ctx.Empty Ctx.:> RV _ Ctx.:> RV variants) <- val
+      ,  Just Refl <- W4.testEquality (FC.fmapFC variantShapeType variantShps) variantCtx
+      -> case firstConcreteVariant variantShps variants of
+           Just (Some (Functor.Pair fldShps fldVals)) ->
+             PP.braces $ prettyAdtOrTuple fldShps fldVals
+           Nothing ->
+             "<symbolic enum>"
+
+      |  otherwise
+      -> error "Malformed MIRVal enum"
     TransparentShape _ shp' ->
       ppMIRVal sym $ MIRVal shp' val
     RefShape _ _ _ _  ->
@@ -147,12 +167,35 @@ ppMIRVal sym (MIRVal shp val) =
     commaList []     = PP.emptyDoc
     commaList (x:xs) = x PP.<> PP.hcat (map (\y -> PP.comma PP.<+> y) xs)
 
-    prettyStructOrTuple ::
+    -- Return Just the first VariantBranch whose predicate is concretely equal
+    -- to True. If none of the VariantBranches satisfy this property, then
+    -- return Nothing.
+    firstConcreteVariant ::
+      Ctx.Assignment VariantShape ctx ->
+      Ctx.Assignment (VariantBranch Sym) ctx ->
+      Maybe (Some (Functor.Product
+        (Ctx.Assignment FieldShape)
+        (Ctx.Assignment (RegValue' Sym))))
+    firstConcreteVariant variantShapes variantBranches =
+      List.firstJust
+        (\(Some (Functor.Pair (VariantShape _ fldShps) (VB branch))) ->
+          case branch of
+            W4.PE fldPred fldVals
+              |  W4.asConstantPred fldPred == Just True
+              -> Just $ Some $ Functor.Pair fldShps fldVals
+              |  otherwise
+              -> Nothing
+            W4.Unassigned ->
+              Nothing) $
+      FC.toListFC Some $
+      Ctx.zipWith Functor.Pair variantShapes variantBranches
+
+    prettyAdtOrTuple ::
       forall ctx.
       Ctx.Assignment FieldShape ctx ->
       Ctx.Assignment (RegValue' Sym) ctx ->
       PP.Doc ann
-    prettyStructOrTuple fldShp fldVals =
+    prettyAdtOrTuple fldShp fldVals =
       commaList $
       map (\(Some (Functor.Pair shp' (RV v))) -> prettyField shp' v) $
       FC.toListFC Some $
@@ -245,6 +288,12 @@ typeOfSetupValue mcc env nameEnv val =
       pure $ Mir.TyArray elemTy (length vs)
     MS.SetupStruct adt _ ->
       pure $ mirAdtToTy adt
+    MS.SetupEnum enum_ ->
+      case enum_ of
+        MirSetupEnumVariant adt _ _ _ _ ->
+          pure $ mirAdtToTy adt
+        MirSetupEnumSymbolic adt ->
+          pure $ mirAdtToTy adt
     MS.SetupTuple () vals -> do
       tys <- traverse (typeOfSetupValue mcc env nameEnv) vals
       pure $ Mir.TyTuple tys
@@ -312,48 +361,133 @@ resolveSetupVal mcc env tyenv nameEnv val =
     MS.SetupStruct adt flds ->
       case adt of
         _ | adt ^. Mir.adtReprTransparent,
-            [fld] <- flds -> do
-          MIRVal shp fld' <- resolveSetupVal mcc env tyenv nameEnv fld
-          pure $ MIRVal (TransparentShape (mirAdtToTy adt) shp) fld'
-        Mir.Adt nm Mir.Struct [variant] _ _ _ _ -> do
+            [fld] <- flds ->
+          resolveTransparentSetupVal adt fld
+        Mir.Adt nm Mir.Struct variants _ _ _ _ -> do
+          -- First, retrieve the struct variant.
+          variant <-
+            case variants of
+              [variant] ->
+                pure variant
+              _ ->
+                panic "resolveSetupVal"
+                      [ "Encountered struct Adt with " ++
+                        show (length variants) ++
+                        " variants:"
+                      , show nm
+                      ]
+
+          -- Next, resolve the field values and check that they have the
+          -- expected types.
           flds' <- traverse (resolveSetupVal mcc env tyenv nameEnv) flds
           let expectedFlds = variant ^. Mir.vfields
-          let expectedFldsNum = length expectedFlds
           let actualFldTys = map (\(MIRVal shp _) -> shapeMirTy shp) flds'
-          let actualFldsNum = length actualFldTys
-          unless (expectedFldsNum == actualFldsNum) $
-            fail $ unlines
-              [ "Mismatch in number of struct fields"
-              , "Struct name: " ++ show nm
-              , "Expected number of fields: " ++ show expectedFldsNum
-              , "Actual number of fields:   " ++ show actualFldsNum
-              ]
-          zipWithM_
-            (\expectedFld actualFldTy ->
-              let expectedFldTy = expectedFld ^. Mir.fty in
-              let expectedFldName = expectedFld ^. Mir.fName in
-              unless (checkCompatibleTys expectedFldTy actualFldTy) $
-                fail $ unlines
-                  [ "Struct field type mismatch"
-                  , "Field name: " ++ show expectedFldName
-                  , "Expected type: " ++ show (PP.pretty expectedFldTy)
-                  , "Given type:    " ++ show (PP.pretty actualFldTy)
-                  ])
-            expectedFlds
-            actualFldTys
-          Some fldAssn <-
-            pure $ Ctx.fromList $
-            map (\(MIRVal shp v) ->
-                  if Mir.canInitialize col (shapeMirTy shp)
-                  then Some $ Functor.Pair (ReqField shp) (RV v)
-                  else Some $ Functor.Pair (OptField shp) (RV (W4.justPartExpr sym v)))
-                flds'
+          checkFields nm "Struct" "struct fields" expectedFlds actualFldTys
+
+          -- Finally, construct a MIRVal of the appropriate shape.
+          Some fldAssn <- pure $ variantFieldsToAssn sym flds'
           let (fldShpAssn, valAssn) = Ctx.unzip fldAssn
           let structShp = StructShape (mirAdtToTy adt) actualFldTys fldShpAssn
           let structTpr = StructRepr (FC.fmapFC fieldShapeType fldShpAssn)
           pure $ MIRVal structShp (AnyValue structTpr valAssn)
-        Mir.Adt _ ak _ _ _ _ _ ->
-          panic "resolveSetupVal" ["AdtKind " ++ show ak ++ " not yet implemented"]
+        Mir.Adt nm (Mir.Enum _) _ _ _ _ _ ->
+          panic "resolveSetupVal"
+                [ "Expected struct type, received enum:"
+                , show nm
+                ]
+        Mir.Adt nm Mir.Union _ _ _ _ _ ->
+          panic "resolveSetupVal"
+                [ "Expected struct type, received union:"
+                , show nm
+                ]
+    MS.SetupEnum enum_ ->
+      case enum_ of
+        MirSetupEnumVariant adt variant discr variantIdxInt flds ->
+          case adt of
+            _ | adt ^. Mir.adtReprTransparent,
+                [fld] <- flds -> do
+              resolveTransparentSetupVal adt fld
+            Mir.Adt nm (Mir.Enum discrTp) variants _ _ _ _ -> do
+              -- Resolve the field values and check that they have the expected
+              -- types.
+              flds' <- traverse (resolveSetupVal mcc env tyenv nameEnv) flds
+              let expectedFlds = variant ^. Mir.vfields
+              let actualFldTys = map (\(MIRVal shp _) -> shapeMirTy shp) flds'
+              checkFields
+                nm
+                "Enum"
+                ("fields in enum variant " ++ show (variant ^. Mir.vname))
+                expectedFlds
+                actualFldTys
+
+              -- Ensure that the discriminant has an integral type and build
+              -- a symbolic bitvector from it.
+              Some discrTpr <- pure $ Mir.tyToRepr col discrTp
+              let discrShp = tyToShapeEq col discrTp discrTpr
+              IsBVShape _ discrW <- pure $ testDiscriminantIsBV discrShp
+              discrVal <- W4.bvLit sym discrW $ BV.mkBV discrW discr
+
+              -- Construct an EnumShape and RustEnumRepr. This requires mapping
+              -- over /all/ variants, not just the particular variant that we
+              -- are building.
+              Some variantShps <-
+                pure $ Ctx.fromList $
+                map (\variantTys ->
+                      case Ctx.fromList $
+                           map
+                             (\ty ->
+                               case tyToShape col ty of
+                                 Some shp ->
+                                   if Mir.canInitialize col ty
+                                   then Some $ ReqField shp
+                                   else Some $ OptField shp)
+                             variantTys of
+                        Some fldAssn -> Some $ VariantShape variantTys fldAssn)
+                    (map (\v -> v ^.. Mir.vfields . each . Mir.fty) variants)
+              let enumShp = EnumShape (mirAdtToTy adt) variantShps discrTp discrShp
+              let variantTprs = FC.fmapFC variantShapeType variantShps
+              let enumTpr = Mir.RustEnumRepr
+                              discrTpr
+                              variantTprs
+
+              -- Construct the VariantShape of the particular variant that we
+              -- are building.
+              Some variantIdx <- pure $
+                variantIntIndex nm variantIdxInt (Ctx.size variantShps)
+              VariantShape _ expectedFldAssn <- pure $ variantShps Ctx.! variantIdx
+
+              -- Check that the actual field values match the expected types.
+              Some actualFldValAssn <- pure $ variantFieldsToAssn sym flds'
+              let (actualFldAssn, actualValAssn) =
+                    Ctx.unzip actualFldValAssn
+              Refl <-
+                case W4.testEquality expectedFldAssn actualFldAssn of
+                  Just r -> pure r
+                  Nothing ->
+                    panic "resolveSetupVal"
+                          [ "Enum field shape mismatch"
+                          , "Expected: " ++ show expectedFldAssn
+                          , "Actual: " ++ show actualFldAssn
+                          ]
+
+              -- Finally, construct a MIRVal.
+              let enumVal =
+                    Ctx.empty
+                      Ctx.:> RV discrVal
+                      Ctx.:> RV (injectVariant sym variantTprs variantIdx actualValAssn)
+              pure $ MIRVal enumShp (AnyValue enumTpr enumVal)
+            Mir.Adt nm Mir.Struct _ _ _ _ _ ->
+              panic "resolveSetupVal"
+                    [ "Expected enum type, received struct:"
+                    , show nm
+                    ]
+            Mir.Adt nm Mir.Union _ _ _ _ _ ->
+              panic "resolveSetupVal"
+                    [ "Expected enum type, received union:"
+                    , show nm
+                    ]
+        MirSetupEnumSymbolic _adt ->
+          error "TODO RGS: Symbolic enums"
     MS.SetupTuple () flds -> do
       flds' <- traverse (resolveSetupVal mcc env tyenv nameEnv) flds
       let fldMirTys = map (\(MIRVal shp _) -> shapeMirTy shp) flds'
@@ -427,6 +561,41 @@ resolveSetupVal mcc env tyenv nameEnv val =
     usizeBvLit :: Sym -> Int -> IO (W4.SymBV Sym Mir.SizeBits)
     usizeBvLit sym = W4.bvLit sym W4.knownNat . BV.mkBV W4.knownNat . toInteger
 
+    -- Perform a light amount of typechecking on the fields in a struct or enum
+    -- variant. This ensures that the variant receives the expected number of
+    -- types and that the types of each field match.
+    checkFields ::
+      Mir.DefId {- The struct or enum name. (Only used for error messages.) -} ->
+      String {- "Struct" or "Enum". (Only used for error messages.) -} ->
+      String {- What type of fields are we checking?
+                (Only used for error messages.) -} ->
+      [Mir.Field] {- The expected fields. -} ->
+      [Mir.Ty] {- The actual field types. -} ->
+      IO ()
+    checkFields adtNm what fieldDiscr expectedFlds actualFldTys = do
+      let expectedFldsNum = length expectedFlds
+      let actualFldsNum = length actualFldTys
+      unless (expectedFldsNum == actualFldsNum) $
+        fail $ unlines
+          [ "Mismatch in number of " ++ fieldDiscr
+          , what ++ " name: " ++ show adtNm
+          , "Expected number of fields: " ++ show expectedFldsNum
+          , "Actual number of fields:   " ++ show actualFldsNum
+          ]
+      zipWithM_
+        (\expectedFld actualFldTy ->
+          let expectedFldTy = expectedFld ^. Mir.fty in
+          let expectedFldName = expectedFld ^. Mir.fName in
+          unless (checkCompatibleTys expectedFldTy actualFldTy) $
+            fail $ unlines
+              [ what ++ " field type mismatch"
+              , "Field name: " ++ show expectedFldName
+              , "Expected type: " ++ show (PP.pretty expectedFldTy)
+              , "Given type:    " ++ show (PP.pretty actualFldTy)
+              ])
+        expectedFlds
+        actualFldTys
+
     -- Resolve parts of a slice that are shared in common between
     -- 'MirSetupSlice' and 'MirSetupSliceRange'.
     resolveSetupSliceFromArray ::
@@ -445,6 +614,26 @@ resolveSetupVal mcc env tyenv nameEnv val =
           pure $ SetupSliceFromArray elemTpr sliceShp refVal len
         _ -> X.throwM $ MIRSliceNonArrayReference $ shapeMirTy arrRefShp
 
+    -- Resolve a transparent struct or enum value.
+    resolveTransparentSetupVal :: Mir.Adt -> SetupValue -> IO MIRVal
+    resolveTransparentSetupVal adt fld = do
+      MIRVal shp fld' <- resolveSetupVal mcc env tyenv nameEnv fld
+      pure $ MIRVal (TransparentShape (mirAdtToTy adt) shp) fld'
+
+    -- Given the list of fields in a struct or enum variant, construct an
+    -- Assignment, consisting of each field's type and value.
+    variantFieldsToAssn ::
+      Sym ->
+      [MIRVal] ->
+      Some (Ctx.Assignment (Functor.Product FieldShape (RegValue' Sym)))
+    variantFieldsToAssn sym flds =
+      Ctx.fromList $
+      map (\(MIRVal shp v) ->
+            if Mir.canInitialize col (shapeMirTy shp)
+            then Some $ Functor.Pair (ReqField shp) (RV v)
+            else Some $ Functor.Pair (OptField shp) (RV (W4.justPartExpr sym v)))
+          flds
+
 -- | An intermediate data structure that is only used by
 -- 'resolveSetupSliceFromArray'.
 data SetupSliceFromArray where
@@ -697,6 +886,21 @@ equalValsPred cc mv1 mv2 =
           goFldAssn fldShp fldAssn1 fldAssn2
         (_, _) ->
           pure $ W4.falsePred sym
+    goTy (EnumShape _ variantShp _ discrShp) any1 any2 =
+      case (any1, any2) of
+        (AnyValue (Mir.RustEnumRepr discrTpr1 variantCtx1)
+                  (Ctx.Empty Ctx.:> RV discr1 Ctx.:> RV variant1),
+         AnyValue (Mir.RustEnumRepr discrTpr2 variantCtx2)
+                  (Ctx.Empty Ctx.:> RV discr2 Ctx.:> RV variant2)) -> do
+           Refl <- testEquality discrTpr1 discrTpr2
+           Refl <- testEquality (shapeType discrShp) discrTpr1
+           Refl <- testEquality variantCtx1 variantCtx2
+           Refl <- testEquality (FC.fmapFC variantShapeType variantShp) variantCtx1
+           discrPred <- goTy discrShp discr1 discr2
+           variantPred <- goVariantAssn variantShp variant1 variant2
+           liftIO $ W4.andPred sym discrPred variantPred
+        (_, _) ->
+          pure $ W4.falsePred sym
     goTy (TransparentShape _ shp) v1 v2 =
       goTy shp v1 v2
     goTy (RefShape _ _ _ _) ref1 ref2 =
@@ -749,6 +953,34 @@ equalValsPred cc mv1 mv2 =
         (W4.truePred sym)
         (Ctx.zipWith Functor.Pair fldAssn1 fldAssn2)
 
+    goVariantAssn :: Ctx.Assignment VariantShape ctx
+                  -> Ctx.Assignment (VariantBranch Sym) ctx
+                  -> Ctx.Assignment (VariantBranch Sym) ctx
+                  -> MaybeT IO (W4.Pred Sym)
+    goVariantAssn variantShp vbAssn1 vbAssn2 =
+      FCI.ifoldrMFC
+        (\idx (Functor.Pair (VB var1) (VB var2)) z -> do
+          VariantShape _ fldShp <- pure $ variantShp Ctx.! idx
+          varPred <- goVariantFlds fldShp var1 var2
+          liftIO $ W4.andPred sym varPred z)
+        (W4.truePred sym)
+        (Ctx.zipWith Functor.Pair vbAssn1 vbAssn2)
+
+    goVariantFlds :: Ctx.Assignment FieldShape ctx
+                  -> W4.PartExpr (W4.Pred Sym) (Ctx.Assignment (RegValue' Sym) ctx)
+                  -> W4.PartExpr (W4.Pred Sym) (Ctx.Assignment (RegValue' Sym) ctx)
+                  -> MaybeT IO (W4.Pred Sym)
+    goVariantFlds fldShp (W4.PE p1 fldAssn1) (W4.PE p2 fldAssn2) = do
+      pPred <- liftIO $ W4.eqPred sym p1 p2
+      fldPred <- goFldAssn fldShp fldAssn1 fldAssn2
+      liftIO $ W4.andPred sym pPred fldPred
+    goVariantFlds _ W4.Unassigned W4.Unassigned =
+      pure $ W4.truePred sym
+    goVariantFlds _ (W4.PE{}) W4.Unassigned =
+      pure $ W4.falsePred sym
+    goVariantFlds _ W4.Unassigned (W4.PE{}) =
+      pure $ W4.falsePred sym
+
     goFld :: FieldShape tp
           -> RegValue Sym tp
           -> RegValue Sym tp
@@ -1163,3 +1395,35 @@ staticTyRef static =
   Mir.TyRef
     (static ^. Mir.sTy)
     (staticMutability static)
+
+-- | An enum's discriminant should have an integral type such as @isize@ or
+-- @i8@, which this function checks. If this is not the case, this function will
+-- panic.
+testDiscriminantIsBV :: TypeShape shp -> IsBVShape shp
+testDiscriminantIsBV discrShp =
+  case testBVShape discrShp of
+    Just ibvs -> ibvs
+    Nothing ->
+      panic "testDiscriminantIsBV"
+            [ "Unexpected non-integral discriminant type:"
+            , show $ PP.pretty $ shapeMirTy discrShp
+            ]
+
+-- | Compute the index of a variant as an 'Ctx.Index'. If the index is out of
+-- range, this function will panic.
+variantIntIndex ::
+  Mir.DefId {-^ The enum identifier. (Only used for error messages.) -} ->
+  Int {-^ The index of the variant as an 'Int'. -} ->
+  Ctx.Size ctx {-^ The number of variants as a 'Ctx.Size'. -} ->
+  Some (Ctx.Index ctx)
+variantIntIndex adtNm variantIdx variantsSize =
+  case Ctx.intIndex variantIdx variantsSize of
+    Just someIdx ->
+      someIdx
+    Nothing ->
+      panic "variantIntIndex"
+            [ "Enum variant index out of range"
+            , "Enum: " ++ show adtNm
+            , "Index: " ++ show variantIdx
+            , "Number of variants: " ++ show variantsSize
+            ]
diff --git a/src/SAWScript/Crucible/MIR/Setup/Value.hs b/src/SAWScript/Crucible/MIR/Setup/Value.hs
index f764de1f17..ecb2062fba 100644
--- a/src/SAWScript/Crucible/MIR/Setup/Value.hs
+++ b/src/SAWScript/Crucible/MIR/Setup/Value.hs
@@ -47,6 +47,9 @@ module SAWScript.Crucible.MIR.Setup.Value
   , mpMirType
   , mpRef
 
+    -- * @MirSetupEnum@
+  , MirSetupEnum(..)
+
     -- * @MirSetupSlice@
   , MirSetupSlice(..)
   ) where
@@ -71,6 +74,7 @@ import qualified SAWScript.Crucible.Common.Setup.Value as MS
 type instance MS.XSetupNull MIR = Void
 type instance MS.XSetupGlobal MIR = ()
 type instance MS.XSetupStruct MIR = M.Adt
+type instance MS.XSetupEnum MIR = MirSetupEnum
 type instance MS.XSetupTuple MIR = ()
 type instance MS.XSetupSlice MIR = MirSetupSlice
 -- The 'M.Ty' represents the type of array elements.
@@ -140,6 +144,52 @@ data MirPointer sym tp = MirPointer
     , _mpRef :: MirReferenceMux sym tp
     }
 
+-- | A enum-related MIR 'SetupValue'.
+data MirSetupEnum
+  = MirSetupEnumVariant M.Adt M.Variant Integer Int [MS.SetupValue MIR]
+    -- ^ A specific variant of an enum, where:
+    --
+    -- * The 'M.Adt' represents the enum type.
+    --
+    -- * The 'M.Variant' represents the variant.
+    --
+    -- * The 'Integer' is the discriminant value for the variant.
+    --
+    -- * The 'Int' is the index of the variant within the list of all the enum's
+    --   variants. In most circumstances, this index will be the same as the
+    --   discriminant value, but the index can be different if a variant uses an
+    --   explicit value. For instance, in this example:
+    --
+    --   @
+    --   enum A {
+    --       A0,
+    --       A1,
+    --   }
+    --
+    --   enum B {
+    --       B0 = 42,
+    --       B1,
+    --   }
+    --   @
+    --
+    --   The indexes for @A0@ and @B0@ are both @0@, and the indexes for @A1@
+    --   and @B1@ are both @1@. The discriminant values are different, however.
+    --   The discriminants for @A0@ and @A1@ are @0@ and @1@, respectively,
+    --   while the discriminants for @B0@ and @B1@ are @42@ and @43@,
+    --   respectively.
+    --
+    -- * The list of 'MS.SetupValue's are the values of the variant's fields.
+    --
+    -- Note that the discriminant value and index are accessible within the
+    -- 'M.Variant', but retrieving the information is somewhat involved. (See
+    -- the implementation of @mir_enum_variant@.) For this reason, we store
+    -- this information separately in 'MirSetupEnumVariant' to make it easier
+    -- to look up later.
+  | MirSetupEnumSymbolic M.Adt
+    -- ^ A symbolic enum value, where the 'M.Adt' represents the enum type.
+    -- This is only used in the implementation of @mir_fresh_expanded_value@.
+  deriving Show
+
 -- | A slice-related MIR 'SetupValue'.
 data MirSetupSlice
   = MirSetupSliceRaw (MS.SetupValue MIR) (MS.SetupValue MIR)
diff --git a/src/SAWScript/Crucible/MIR/TypeShape.hs b/src/SAWScript/Crucible/MIR/TypeShape.hs
index f24d372ea8..b20ffffc97 100644
--- a/src/SAWScript/Crucible/MIR/TypeShape.hs
+++ b/src/SAWScript/Crucible/MIR/TypeShape.hs
@@ -6,18 +6,23 @@
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeOperators #-}
 
 -- | The 'TypeShape' data type and related utilities.
 module SAWScript.Crucible.MIR.TypeShape
   ( TypeShape(..)
   , FieldShape(..)
+  , VariantShape(..)
   , tyToShape
   , tyToShapeEq
   , shapeType
   , fieldShapeType
+  , variantShapeType
   , shapeMirTy
   , fieldShapeMirTy
   , shapeToTerm
+  , IsBVShape(..)
+  , testBVShape
   , IsRefShape(..)
   , testRefShape
   , sliceShapeParts
@@ -95,6 +100,19 @@ data TypeShape (tp :: CrucibleType) where
                -> TypeRepr tp
                -- ^ The Crucible representation of @T@.
                -> TypeShape (MirSlice tp)
+    -- | A shape for an enum type. Like 'StructShape', this is indexed by
+    -- 'AnyType', so code that matches on 'EnumShape' may need to further match
+    -- on the 'VariantShape's in order to bring additional type information into
+    -- scope.
+    EnumShape :: M.Ty
+              -- ^ The overall enum type.
+              -> Assignment VariantShape ctx
+              -- ^ The shapes of the enum type's variants.
+              -> M.Ty
+              -- ^ The discriminant type.
+              -> TypeShape discrTp
+              -- ^ The shape of the discriminant type.
+              -> TypeShape AnyType
     -- | Note that 'FnPtrShape' contains only 'TypeRepr's for the argument and
     -- result types, not 'TypeShape's, as none of our operations need to recurse
     -- inside them.
@@ -121,6 +139,27 @@ instance PP.Pretty (FieldShape tp) where
 deriving instance Show (FieldShape tp)
 instance ShowF FieldShape
 
+-- | The 'TypeShape' of an enum variant, which consists of some numer of field
+-- types.
+--
+-- This is indexed by a 'StructType', but that is simply an artifact of the
+-- particular way that @crucible-mir@ encodes enum types. Despite the use of
+-- 'StructType' as a type index, we only use 'VariantShape' for enums, not
+-- structs.
+data VariantShape (tp :: CrucibleType) where
+    VariantShape :: [M.Ty]
+                 -- ^ The types of the variant's fields.
+                 -> Assignment FieldShape ctx
+                 -- ^ The shapes of the variant's field types.
+                 -> VariantShape (StructType ctx)
+
+-- TODO: Improve?
+instance PP.Pretty (VariantShape tp) where
+  pretty = PP.viaShow
+
+deriving instance Show (VariantShape tp)
+instance ShowF VariantShape
+
 -- | Return the `TypeShape` of `ty`.
 --
 -- It is guaranteed that the `tp :: CrucibleType` index of the resulting
@@ -142,8 +181,16 @@ tyToShape col = go
         M.TyAdt nm _ _ -> case Map.lookup nm (col ^. M.adts) of
             Just adt | Just ty' <- reprTransparentFieldTy col adt ->
                 mapSome (TransparentShape ty) $ go ty'
-            Just (M.Adt _ M.Struct [v] _ _ _ _) -> goStruct ty (v ^.. M.vfields . each . M.fty)
-            Just (M.Adt _ ak _ _ _ _ _) -> error $ "tyToShape: AdtKind " ++ show ak ++ " NYI"
+            Just (M.Adt _ kind vs _ _ _ _) ->
+              case kind of
+                M.Struct
+                  |  [v] <- vs
+                  -> goStruct ty (variantFieldTys v)
+                  |  otherwise
+                  -> error $ "tyToShape: Unexpected struct with multiple variants: "
+                          ++ show (PP.pretty vs)
+                M.Enum discrTy -> goEnum ty discrTy vs
+                M.Union -> error "tyToShape: Union types NYI"
             Nothing -> error $ "tyToShape: bad adt: " ++ show ty
         M.TyRef ty' mutbl -> goRef ty ty' mutbl
         M.TyRawPtr ty' mutbl -> goRef ty ty' mutbl
@@ -167,7 +214,36 @@ tyToShape col = go
         loop (ty':tys') flds | Some fld <- go ty' = loop tys' (flds :> OptField fld)
 
     goStruct :: M.Ty -> [M.Ty] -> Some TypeShape
-    goStruct ty tys | Some flds <- loop tys Empty = Some $ StructShape ty tys flds
+    goStruct ty tys | Some flds <- goFields tys = Some $ StructShape ty tys flds
+
+    -- The first Ty is the overall enum type, and the second Ty is the
+    -- discriminant type.
+    goEnum :: M.Ty -> M.Ty -> [M.Variant] -> Some TypeShape
+    goEnum ty discrTy vs
+        | Some discrShp <- go discrTy
+        , Some variants <- loop vs Empty
+        = Some $ EnumShape ty variants discrTy discrShp
+      where
+        loop ::
+          forall ctx.
+          [M.Variant] ->
+          Assignment VariantShape ctx ->
+          Some (Assignment VariantShape)
+        loop [] variants = Some variants
+        loop (v':vs') variants
+          | Some variant <- goVariant v'
+          = loop vs' (variants :> variant)
+
+    -- Process a single Variant in an enum type.
+    goVariant :: M.Variant -> Some VariantShape
+    goVariant v
+        | Some flds <- goFields tys
+        = Some $ VariantShape tys flds
+      where
+        tys = variantFieldTys v
+
+    goFields :: [M.Ty] -> Some (Assignment FieldShape)
+    goFields tys = loop tys Empty
       where
         loop :: forall ctx. [M.Ty] -> Assignment FieldShape ctx -> Some (Assignment FieldShape)
         loop [] flds = Some flds
@@ -195,6 +271,11 @@ tyToShape col = go
         tyToReprCont col ret $ \retr ->
            Some (FnPtrShape ty argsr retr)
 
+    -- Retrieve the field types in a variant. This used for both struct and enum
+    -- variants.
+    variantFieldTys :: M.Variant -> [M.Ty]
+    variantFieldTys v = v ^.. M.vfields . each . M.fty
+
 -- | Given a `Ty` and the result of `tyToRepr ty`, produce a `TypeShape` with
 -- the same index `tp`.  Raises an `error` if the `TypeRepr` doesn't match
 -- `tyToRepr ty`.
@@ -215,6 +296,7 @@ shapeType = go
     go (TupleShape _ _ flds) = StructRepr $ fmapFC fieldShapeType flds
     go (ArrayShape _ _ shp) = MirVectorRepr $ shapeType shp
     go (StructShape _ _ _flds) = AnyRepr
+    go (EnumShape _ _ _ _variants) = AnyRepr
     go (TransparentShape _ shp) = go shp
     go (RefShape _ _ _ tpr) = MirReferenceRepr tpr
     go (SliceShape _ _ _ tpr) = MirSliceRepr tpr
@@ -224,12 +306,17 @@ fieldShapeType :: FieldShape tp -> TypeRepr tp
 fieldShapeType (ReqField shp) = shapeType shp
 fieldShapeType (OptField shp) = MaybeRepr $ shapeType shp
 
+variantShapeType :: VariantShape tp -> TypeRepr tp
+variantShapeType (VariantShape _ flds) =
+  StructRepr $ fmapFC fieldShapeType flds
+
 shapeMirTy :: TypeShape tp -> M.Ty
 shapeMirTy (UnitShape ty) = ty
 shapeMirTy (PrimShape ty _) = ty
 shapeMirTy (TupleShape ty _ _) = ty
 shapeMirTy (ArrayShape ty _ _) = ty
 shapeMirTy (StructShape ty _ _) = ty
+shapeMirTy (EnumShape ty _ _ _) = ty
 shapeMirTy (TransparentShape ty _) = ty
 shapeMirTy (RefShape ty _ _ _) = ty
 shapeMirTy (SliceShape ty _ _ _) = ty
@@ -263,6 +350,24 @@ shapeToTerm sc = go
     goField (OptField shp) = go shp
     goField (ReqField shp) = go shp
 
+-- | A witness that a 'TypeShape' is equal to a 'PrimShape' that characterizes
+-- a bitvector.
+data IsBVShape (tp :: CrucibleType) where
+  IsBVShape :: (1 <= w)
+            => M.Ty
+            -> NatRepr w
+            -> IsBVShape (BVType w)
+
+-- | Check that a 'TypeShape' is equal to a 'PrimShape' that characterizes a
+-- bitvector. If so, return 'Just' a witness of that equality. Otherwise, return
+-- 'Nothing'.
+testBVShape :: TypeShape tp -> Maybe (IsBVShape tp)
+testBVShape shp =
+  case shp of
+    PrimShape ty (BaseBVRepr w)
+      -> Just $ IsBVShape ty w
+    _ -> Nothing
+
 -- | A witness that a 'TypeShape' is equal to a 'RefShape'.
 data IsRefShape (tp :: CrucibleType) where
   IsRefShape :: M.Ty
@@ -313,6 +418,13 @@ instance TestEquality TypeShape where
         , (TypeApp (ConType [t|CtxRepr|]) AnyType, [|testEquality|])
         ])
 
+instance TestEquality VariantShape where
+  testEquality =
+    $(structuralTypeEquality
+        [t|VariantShape|]
+        [ (TypeApp (TypeApp (ConType [t|Assignment|]) AnyType) AnyType, [|testEquality|])
+        ])
+
 instance TestEquality FieldShape where
   testEquality =
     $(structuralTypeEquality
diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs
index 9f4830e4a0..dae3eb1ca9 100644
--- a/src/SAWScript/Interpreter.hs
+++ b/src/SAWScript/Interpreter.hs
@@ -3917,6 +3917,15 @@ primitives = Map.fromList
     , "it appears (i.e., before or after `mir_execute_func`)."
     ]
 
+  , prim "mir_enum_value" "MIRAdt -> String -> [MIRValue] -> MIRValue"
+    (funVal3 mir_enum_value)
+    Experimental
+    [ "Create a MIRValue representing a variant of a MIR enum with the given"
+    , "list of values as elements. The MIRAdt argument determines what enum"
+    , "type to create; use `mir_find_adt` to retrieve a MIRAdt value. The"
+    , "String argument represents the variant name."
+    ]
+
   , prim "mir_execute_func" "[MIRValue] -> MIRSetup ()"
     (pureVal mir_execute_func)
     Experimental