diff --git a/CHANGES.md b/CHANGES.md
index c30667bcc3..61b4130864 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -26,6 +26,13 @@
   command.) For more details on how each of these commands should be used,
   consult the "Bitfields" section of the SAW manual.
 
+* A new `llvm_cast_pointer` function has been added that allows users
+  to directly specify that a pointer should be treated as pointing to
+  a particular type. This mainly affects the results of subsequent
+  `llvm_field` and `llvm_elem` calls.  This is especially useful for
+  dealing with C `union` types, as the type information provided by
+  LLVM is imprecise in these cases.
+
 # Version 0.9
 
 ## New Features
diff --git a/crux-mir-comp/src/Mir/Compositional/Builder.hs b/crux-mir-comp/src/Mir/Compositional/Builder.hs
index cd9f70246f..cf37cc5d88 100644
--- a/crux-mir-comp/src/Mir/Compositional/Builder.hs
+++ b/crux-mir-comp/src/Mir/Compositional/Builder.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE EmptyCase #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE FlexibleInstances #-}
@@ -611,6 +612,7 @@ substMethodSpec sc sm ms = do
         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
+        MS.SetupCast v _ _ -> case v of {}
         MS.SetupGlobal _ _ -> return sv
         MS.SetupGlobalInitializer _ _ -> return sv
 
diff --git a/crux-mir-comp/src/Mir/Compositional/MethodSpec.hs b/crux-mir-comp/src/Mir/Compositional/MethodSpec.hs
index a68e5eb380..28404f136e 100644
--- a/crux-mir-comp/src/Mir/Compositional/MethodSpec.hs
+++ b/crux-mir-comp/src/Mir/Compositional/MethodSpec.hs
@@ -29,6 +29,7 @@ type instance MS.HasSetupStruct MIR = 'True
 type instance MS.HasSetupArray MIR = 'True
 type instance MS.HasSetupElem MIR = 'True
 type instance MS.HasSetupField MIR = 'True
+type instance MS.HasSetupCast MIR = 'False
 type instance MS.HasSetupGlobalInitializer MIR = 'False
 
 type instance MS.HasGhostState MIR = 'False
@@ -39,6 +40,8 @@ type instance MS.ExtType MIR = M.Ty
 type instance MS.MethodId MIR = DefId
 type instance MS.AllocSpec MIR = Some MirAllocSpec
 type instance MS.PointsTo MIR = MirPointsTo
+type instance MS.ResolvedState MIR = ()
+type instance MS.CastType MIR = ()
 
 type instance MS.Codebase MIR = CollectionState
 
diff --git a/doc/manual/manual.md b/doc/manual/manual.md
index fc50d60a4b..088742583b 100644
--- a/doc/manual/manual.md
+++ b/doc/manual/manual.md
@@ -2199,7 +2199,8 @@ pointer points to a value that does not agree with its static type.
 CrucibleSetup ()` works like `llvm_points_to` but omits type
 checking. Rather than omitting type checking across the board, we
 introduced this additional function to make it clear when a type
-reinterpretation is intentional.
+reinterpretation is intentional. As an alternative, one
+may instead use `llvm_cast_pointer` to line up the static types.
 
 ## Working with Compound Types
 
@@ -2213,7 +2214,7 @@ is the array index. For `struct` values, it is the field index.
 
 * `llvm_field : SetupValue -> String -> SetupValue` yields a pointer
 to a particular named `struct` field, if debugging information is
-available in the bitcode
+available in the bitcode.
 
 Either of these functions can be used with `llvm_points_to` to
 specify the value of a particular array element or `struct` field.
@@ -2240,6 +2241,22 @@ following command will create values of such types:
 
 * `llvm_packed_struct_value : [SetupValue] -> SetupValue`
 
+C programs will sometimes make use of pointer casting to implement
+various kinds of polymorphic behaviors, either via direct pointer
+casts, or by using `union` types to codify the pattern. To reason
+about such cases, the following operation is useful.
+
+* `llvm_cast_pointer : SetupValue -> LLVMType -> SetupValue`
+
+This function function casts the type of the input value (which must be a
+pointer) so that it points to values of the given type.  This mainly
+affects the results of subsequent `llvm_field` and `llvm_elem` calls,
+and any eventual `points_to` statements that the resulting pointer
+flows into.  This is especially useful for dealing with C `union`
+types, as the type information provided by LLVM is imprecise in these
+cases.
+
+
 In the experimental Java verification implementation, the following
 functions can be used to state the equivalent of a combination of
 `llvm_points_to` and either `llvm_elem` or `llvm_field`.
diff --git a/doc/manual/manual.pdf b/doc/manual/manual.pdf
index 0b42365742..6d4671cbde 100644
Binary files a/doc/manual/manual.pdf and b/doc/manual/manual.pdf differ
diff --git a/intTests/test_llvm_union/Makefile b/intTests/test_llvm_union/Makefile
new file mode 100644
index 0000000000..977e89a70a
--- /dev/null
+++ b/intTests/test_llvm_union/Makefile
@@ -0,0 +1,2 @@
+test.bc : test.c
+	clang -c -emit-llvm -g -o test.bc test.c
diff --git a/intTests/test_llvm_union/README b/intTests/test_llvm_union/README
new file mode 100644
index 0000000000..18269aad5c
--- /dev/null
+++ b/intTests/test_llvm_union/README
@@ -0,0 +1,4 @@
+This example is derived from an older union example
+from `examples/llvm/union`.  It is intended to demonstrate
+the use of the `llvm_pointer_cast` operation for selecting
+the branches of unions.
diff --git a/intTests/test_llvm_union/test.bc b/intTests/test_llvm_union/test.bc
new file mode 100644
index 0000000000..4f2e570553
Binary files /dev/null and b/intTests/test_llvm_union/test.bc differ
diff --git a/intTests/test_llvm_union/test.c b/intTests/test_llvm_union/test.c
new file mode 100644
index 0000000000..3a0d213e9d
--- /dev/null
+++ b/intTests/test_llvm_union/test.c
@@ -0,0 +1,35 @@
+#include <stdint.h>
+
+typedef enum { INC_1 , INC_2 } alg;
+
+typedef struct {
+  uint32_t x;
+} inc_1_st;
+
+typedef struct {
+  uint32_t x;
+  uint32_t y;
+} inc_2_st;
+
+typedef struct {
+  alg alg;
+  union {
+    inc_1_st inc_1_st;
+    inc_2_st inc_2_st;
+  } inc_st;
+} st;
+
+uint32_t inc(st *st) {
+  switch (st->alg) {
+  case INC_1:
+    st->inc_st.inc_1_st.x += 1;
+    break;
+  case INC_2:
+    st->inc_st.inc_2_st.x += 1;
+    st->inc_st.inc_2_st.y += 1;
+    break;
+  default:
+    return 1/0;
+  }
+  return 0;
+}
diff --git a/intTests/test_llvm_union/test.saw b/intTests/test_llvm_union/test.saw
new file mode 100644
index 0000000000..3d65c7a6f8
--- /dev/null
+++ b/intTests/test_llvm_union/test.saw
@@ -0,0 +1,52 @@
+m <- llvm_load_module "test.bc";
+
+let {{
+INC_1 = 0 : [32]
+INC_2 = 1 : [32]
+}};
+
+
+// The argument 'INC' specifies which 'alg' enum to test.
+let inc_spec INC = do {
+
+  stp <- llvm_alloc (llvm_alias "struct.st");
+  llvm_points_to (llvm_field stp "alg") (llvm_term {{ INC }});
+
+  if eval_bool {{ INC == INC_1 }} then
+    do {
+      let p = llvm_cast_pointer (llvm_field stp "inc_st") (llvm_alias "struct.inc_1_st");
+
+      x0 <- llvm_fresh_var "x0" (llvm_int 32);
+      llvm_points_to (llvm_field p "x") (llvm_term x0);
+
+      llvm_execute_func [stp];
+
+      llvm_points_to (llvm_field p "x") (llvm_term {{ x0 + 1 }});
+    }
+  else if eval_bool {{ INC == INC_2 }} then
+    do {
+      let p = llvm_cast_pointer (llvm_field stp "inc_st") (llvm_alias "struct.inc_2_st");
+
+      x0 <- llvm_fresh_var "x0" (llvm_int 32);
+      y0 <- llvm_fresh_var "y0" (llvm_int 32);
+
+      llvm_points_to (llvm_field p "x") (llvm_term x0);
+      llvm_points_to (llvm_field p "y") (llvm_term y0);
+
+      llvm_execute_func [stp];
+
+      llvm_points_to (llvm_field p "x") (llvm_term {{ x0 + 1 }});
+      llvm_points_to (llvm_field p "y") (llvm_term {{ y0 + 1 }});
+    }
+  else return (); // Unknown INC value
+
+  llvm_return (llvm_term {{ 0 : [32] }});
+};
+
+print "Verifying 'inc_1' using 'llvm_verify':";
+llvm_verify m "inc" [] true (inc_spec {{ INC_1 }}) abc;
+print "";
+
+print "Verifying 'inc_2' using 'llvm_verify':";
+llvm_verify m "inc" [] true (inc_spec {{ INC_2 }}) abc;
+print "";
diff --git a/intTests/test_llvm_union/test.sh b/intTests/test_llvm_union/test.sh
new file mode 100644
index 0000000000..0b864017cd
--- /dev/null
+++ b/intTests/test_llvm_union/test.sh
@@ -0,0 +1 @@
+$SAW test.saw
diff --git a/saw-remote-api/src/SAWServer.hs b/saw-remote-api/src/SAWServer.hs
index 66e1269579..cbc72e3845 100644
--- a/saw-remote-api/src/SAWServer.hs
+++ b/saw-remote-api/src/SAWServer.hs
@@ -87,13 +87,14 @@ instance Show SAWTask where
   show (JVMSetup n) = "(JVMSetup" ++ show n ++ ")"
 
 
-data CrucibleSetupVal e
+data CrucibleSetupVal ty e
   = NullValue
-  | ArrayValue [CrucibleSetupVal e]
-  | TupleValue [CrucibleSetupVal e]
+  | ArrayValue [CrucibleSetupVal ty e]
+  | TupleValue [CrucibleSetupVal ty e]
   -- | RecordValue [(String, CrucibleSetupVal e)]
-  | FieldLValue (CrucibleSetupVal e) String
-  | ElementLValue (CrucibleSetupVal e) Int
+  | FieldLValue (CrucibleSetupVal ty e) String
+  | CastLValue (CrucibleSetupVal ty e) ty
+  | ElementLValue (CrucibleSetupVal ty e) Int
   | GlobalInitializer String
   | GlobalLValue String
   | NamedValue ServerName
@@ -101,26 +102,25 @@ data CrucibleSetupVal e
   deriving stock (Foldable, Functor, Traversable)
 
 data SetupStep ty
-  = SetupReturn (CrucibleSetupVal CryptolAST) -- ^ The return value
+  = SetupReturn (CrucibleSetupVal ty CryptolAST) -- ^ The return value
   | SetupFresh ServerName Text ty -- ^ Server name to save in, debug name, fresh variable type
   | SetupAlloc ServerName ty Bool (Maybe Int) -- ^ Server name to save in, type of allocation, mutability, alignment
   | SetupGhostValue ServerName Text CryptolAST -- ^ Variable, term
-  | SetupPointsTo (CrucibleSetupVal CryptolAST)
-                  (CrucibleSetupVal CryptolAST)
+  | SetupPointsTo (CrucibleSetupVal ty CryptolAST)
+                  (CrucibleSetupVal ty CryptolAST)
                   (Maybe (CheckPointsToType ty))
                   (Maybe CryptolAST)
                   -- ^ The source, the target, the type to check the target,
                   --   and the condition that must hold in order for the source to point to the target
-  | SetupPointsToBitfield (CrucibleSetupVal CryptolAST)
+  | SetupPointsToBitfield (CrucibleSetupVal ty CryptolAST)
                           Text
-                          (CrucibleSetupVal CryptolAST)
+                          (CrucibleSetupVal ty CryptolAST)
                           -- ^ The source bitfield,
                           --   the name of the field within the bitfield,
                           --   and the target.
-  | SetupExecuteFunction [CrucibleSetupVal CryptolAST] -- ^ Function's arguments
+  | SetupExecuteFunction [CrucibleSetupVal ty CryptolAST] -- ^ Function's arguments
   | SetupPrecond CryptolAST -- ^ Function's precondition
   | SetupPostcond CryptolAST -- ^ Function's postcondition
-  deriving stock (Foldable, Functor, Traversable)
 
 instance Show (SetupStep ty) where
   show _ = "⟨SetupStep⟩" -- TODO
diff --git a/saw-remote-api/src/SAWServer/Data/Contract.hs b/saw-remote-api/src/SAWServer/Data/Contract.hs
index 6fc7aa3902..b1701c6855 100644
--- a/saw-remote-api/src/SAWServer/Data/Contract.hs
+++ b/saw-remote-api/src/SAWServer/Data/Contract.hs
@@ -35,15 +35,15 @@ data Contract ty cryptolExpr =
     , preAllocated  :: [Allocated ty]
     , preGhostValues  :: [GhostValue cryptolExpr]
     , prePointsTos  :: [PointsTo ty cryptolExpr]
-    , prePointsToBitfields :: [PointsToBitfield cryptolExpr]
-    , argumentVals  :: [CrucibleSetupVal cryptolExpr]
+    , prePointsToBitfields :: [PointsToBitfield ty cryptolExpr]
+    , argumentVals  :: [CrucibleSetupVal ty cryptolExpr]
     , postVars      :: [ContractVar ty]
     , postConds     :: [cryptolExpr]
     , postAllocated :: [Allocated ty]
     , postGhostValues :: [GhostValue cryptolExpr]
     , postPointsTos :: [PointsTo ty cryptolExpr]
-    , postPointsToBitfields :: [PointsToBitfield cryptolExpr]
-    , returnVal     :: Maybe (CrucibleSetupVal cryptolExpr)
+    , postPointsToBitfields :: [PointsToBitfield ty cryptolExpr]
+    , returnVal     :: Maybe (CrucibleSetupVal ty cryptolExpr)
     }
     deriving stock (Functor, Foldable, Traversable)
 
@@ -64,17 +64,17 @@ data Allocated ty =
 
 data PointsTo ty cryptolExpr =
   PointsTo
-    { pointer           :: CrucibleSetupVal cryptolExpr
-    , pointsTo          :: CrucibleSetupVal cryptolExpr
+    { pointer           :: CrucibleSetupVal ty cryptolExpr
+    , pointsTo          :: CrucibleSetupVal ty cryptolExpr
     , checkPointsToType :: Maybe (CheckPointsToType ty)
     , condition         :: Maybe cryptolExpr
     } deriving stock (Functor, Foldable, Traversable)
 
-data PointsToBitfield cryptolExpr =
+data PointsToBitfield ty cryptolExpr =
   PointsToBitfield
-    { bfPointer   :: CrucibleSetupVal cryptolExpr
+    { bfPointer   :: CrucibleSetupVal ty cryptolExpr
     , bfFieldName :: Text
-    , bfPointsTo  :: CrucibleSetupVal cryptolExpr
+    , bfPointsTo  :: CrucibleSetupVal ty cryptolExpr
     } deriving stock (Functor, Foldable, Traversable)
 
 data CheckAgainstTag
@@ -96,7 +96,7 @@ instance (FromJSON ty, FromJSON cryptolExpr) => FromJSON (PointsTo ty cryptolExp
                <*> o .:? "check points to type"
                <*> o .:? "condition"
 
-instance FromJSON cryptolExpr => FromJSON (PointsToBitfield cryptolExpr) where
+instance (FromJSON ty, FromJSON cryptolExpr) => FromJSON (PointsToBitfield ty cryptolExpr) where
   parseJSON =
     withObject "Points-to-bitfield relationship" $ \o ->
       PointsToBitfield <$> o .: "pointer"
diff --git a/saw-remote-api/src/SAWServer/Data/SetupValue.hs b/saw-remote-api/src/SAWServer/Data/SetupValue.hs
index 0e229eef93..18fb6836fd 100644
--- a/saw-remote-api/src/SAWServer/Data/SetupValue.hs
+++ b/saw-remote-api/src/SAWServer/Data/SetupValue.hs
@@ -15,6 +15,7 @@ data SetupValTag
   | TagArrayValue
   | TagTupleValue
   | TagFieldLValue
+  | TagCastLValue
   | TagElemLValue
   | TagGlobalInit
   | TagGlobalLValue
@@ -29,12 +30,13 @@ instance FromJSON SetupValTag where
       "array" -> pure TagArrayValue
       "tuple" -> pure TagTupleValue
       "field" -> pure TagFieldLValue
+      "cast"  -> pure TagCastLValue
       "element lvalue" -> pure TagElemLValue
       "global initializer" -> pure TagGlobalInit
       "global lvalue" -> pure TagGlobalLValue
       _ -> empty
 
-instance FromJSON cryptolExpr => FromJSON (CrucibleSetupVal cryptolExpr) where
+instance (FromJSON ty, FromJSON cryptolExpr) => FromJSON (CrucibleSetupVal ty cryptolExpr) where
   parseJSON v = fromObject v
     where
       fromObject = withObject "saved value or Cryptol expression" $ \o ->
@@ -46,6 +48,7 @@ instance FromJSON cryptolExpr => FromJSON (CrucibleSetupVal cryptolExpr) where
           TagArrayValue -> ArrayValue <$> o .: "elements"
           TagTupleValue -> TupleValue <$> o .: "elements"
           TagFieldLValue -> FieldLValue <$> o .: "base" <*> o .: "field"
+          TagCastLValue -> CastLValue <$> o .: "base" <*> o .: "type"
           TagElemLValue -> ElementLValue <$> o .: "base" <*> o .: "index"
           TagGlobalInit -> GlobalInitializer <$> o .: "name"
           TagGlobalLValue -> GlobalLValue <$> o .: "name"
diff --git a/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs b/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs
index dec9344cdf..d2e571e943 100644
--- a/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs
+++ b/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs
@@ -145,7 +145,7 @@ compileJVMContract fileReader bic cenv0 c =
            GlobalLValue name -> jvm_static_field_is name sv
            _ -> JVMSetupM $ fail "Invalid points-to statement."
 
-    setupPointsToBitfields :: PointsToBitfield (P.Expr P.PName) -> JVMSetupM ()
+    setupPointsToBitfields :: PointsToBitfield JavaType (P.Expr P.PName) -> JVMSetupM ()
     setupPointsToBitfields _ =
       JVMSetupM $ fail "Points-to-bitfield not supported in JVM API."
 
@@ -173,7 +173,7 @@ compileJVMContract fileReader bic cenv0 c =
 
     getSetupVal ::
       (Map ServerName ServerSetupVal, CryptolEnv) ->
-      CrucibleSetupVal (P.Expr P.PName) ->
+      CrucibleSetupVal JavaType (P.Expr P.PName) ->
       JVMSetupM (MS.SetupValue CJ.JVM)
     getSetupVal _ NullValue = JVMSetupM $ return (MS.SetupNull ())
     getSetupVal (env, _) (NamedValue n) =
@@ -186,6 +186,8 @@ compileJVMContract fileReader bic cenv0 c =
       JVMSetupM $ fail "Tuple setup values unsupported in JVM API."
     getSetupVal _ (FieldLValue _ _) =
       JVMSetupM $ fail "Field l-values unsupported in JVM API."
+    getSetupVal _ (CastLValue _ _) =
+      JVMSetupM $ fail "Cast l-values unsupported in JVM API."
     getSetupVal _ (ElementLValue _ _) =
       JVMSetupM $ fail "Element l-values unsupported in JVM API."
     getSetupVal _ (GlobalInitializer _) =
diff --git a/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs b/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs
index b0b27a30db..ab25b88d8d 100644
--- a/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs
+++ b/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs
@@ -138,7 +138,7 @@ compileLLVMContract fileReader bic ghostEnv cenv0 c =
 
     setupPointsToBitfield ::
       (Map ServerName ServerSetupVal, CryptolEnv) ->
-      PointsToBitfield (P.Expr P.PName) ->
+      PointsToBitfield JSONLLVMType (P.Expr P.PName) ->
       LLVMCrucibleSetupM ()
     setupPointsToBitfield env (PointsToBitfield p fieldName v) =
       do ptr <- getSetupVal env p
@@ -173,7 +173,7 @@ compileLLVMContract fileReader bic ghostEnv cenv0 c =
 
     getSetupVal ::
       (Map ServerName ServerSetupVal, CryptolEnv) ->
-      CrucibleSetupVal (P.Expr P.PName) ->
+      CrucibleSetupVal JSONLLVMType (P.Expr P.PName) ->
       LLVMCrucibleSetupM (CMS.AllLLVM MS.SetupValue)
     getSetupVal _ NullValue = LLVMCrucibleSetupM $ return CMS.anySetupNull
     getSetupVal env (ArrayValue elts) =
@@ -185,6 +185,9 @@ compileLLVMContract fileReader bic ghostEnv cenv0 c =
     getSetupVal env (FieldLValue base fld) =
       do base' <- getSetupVal env base
          LLVMCrucibleSetupM $ return $ CMS.anySetupField base' fld
+    getSetupVal env (CastLValue base ty) =
+      do base' <- getSetupVal env base
+         LLVMCrucibleSetupM $ return $ CMS.anySetupCast base' (llvmType ty)
     getSetupVal env (ElementLValue base idx) =
       do base' <- getSetupVal env base
          LLVMCrucibleSetupM $ return $ CMS.anySetupElem base' idx
diff --git a/src/SAWScript/Crucible/Common/MethodSpec.hs b/src/SAWScript/Crucible/Common/MethodSpec.hs
index 28358002a1..680fff2c48 100644
--- a/src/SAWScript/Crucible/Common/MethodSpec.hs
+++ b/src/SAWScript/Crucible/Common/MethodSpec.hs
@@ -67,6 +67,32 @@ data PrePost
   = PreState | PostState
   deriving (Eq, Ord, Show)
 
+--------------------------------------------------------------------------------
+-- *** Extension-specific information
+
+type family CrucibleContext ext :: Type
+
+-- | How to specify allocations in this syntax extension
+type family AllocSpec ext :: Type
+
+-- | The type of identifiers for types in this syntax extension
+type family TypeName ext :: Type
+
+-- | The type of types of the syntax extension we're dealing with
+type family ExtType ext :: Type
+
+-- | The types that can appear in casts
+type family CastType ext :: Type
+
+-- | The type of points-to assertions
+type family PointsTo ext :: Type
+
+-- | The type of global allocations
+type family AllocGlobal ext :: Type
+
+-- | The type of \"resolved\" state
+type family ResolvedState ext :: Type
+
 --------------------------------------------------------------------------------
 -- ** SetupValue
 
@@ -85,6 +111,7 @@ type family HasSetupArray ext :: Bool
 type family HasSetupElem ext :: Bool
 type family HasSetupField ext :: Bool
 type family HasSetupGlobal ext :: Bool
+type family HasSetupCast ext :: Bool
 type family HasSetupGlobalInitializer ext :: Bool
 
 -- | From the manual: \"The SetupValue type corresponds to values that can occur
@@ -99,6 +126,8 @@ data SetupValue ext where
   SetupArray  :: B (HasSetupArray ext) -> [SetupValue ext] -> SetupValue ext
   SetupElem   :: B (HasSetupElem ext) -> SetupValue ext -> Int -> SetupValue ext
   SetupField  :: B (HasSetupField ext) -> SetupValue ext -> String -> SetupValue ext
+  SetupCast   :: B (HasSetupCast ext) -> SetupValue ext -> CastType ext -> SetupValue ext
+
   -- | A pointer to a global variable
   SetupGlobal :: B (HasSetupGlobal ext) -> String -> SetupValue ext
   -- | This represents the value of a global's initializer.
@@ -114,8 +143,10 @@ type SetupValueHas (c :: Type -> Constraint) ext =
   , c (B (HasSetupArray ext))
   , c (B (HasSetupElem ext))
   , c (B (HasSetupField ext))
+  , c (B (HasSetupCast ext))
   , c (B (HasSetupGlobal ext))
   , c (B (HasSetupGlobalInitializer ext))
+  , c (CastType ext)
   )
 
 deriving instance (SetupValueHas Show ext) => Show (SetupValue ext)
@@ -128,7 +159,7 @@ deriving instance (SetupValueHas Show ext) => Show (SetupValue ext)
 --   are implementation details and won't be familiar to users.
 --   Consider using 'resolveSetupValue' and printing an 'LLVMVal'
 --   with @PP.pretty@ instead.
-ppSetupValue :: SetupValue ext -> PP.Doc ann
+ppSetupValue :: Show (CastType ext) => SetupValue ext -> PP.Doc ann
 ppSetupValue setupval = case setupval of
   SetupTerm tm   -> ppTypedTerm tm
   SetupVar i     -> ppAllocIndex i
@@ -139,6 +170,7 @@ ppSetupValue setupval = case setupval of
   SetupArray _ vs  -> PP.brackets (commaList (map ppSetupValue vs))
   SetupElem _ v i  -> PP.parens (ppSetupValue v) PP.<> PP.pretty ("." ++ show i)
   SetupField _ v f -> PP.parens (ppSetupValue v) PP.<> PP.pretty ("." ++ f)
+  SetupCast _ v tp -> PP.parens (ppSetupValue v) PP.<> PP.pretty (" AS " ++ show tp)
   SetupGlobal _ nm -> PP.pretty ("global(" ++ nm ++ ")")
   SetupGlobalInitializer _ nm -> PP.pretty ("global_initializer(" ++ nm ++ ")")
   where
@@ -243,87 +275,6 @@ type GhostGlobal = Crucible.GlobalVar GhostType
 --------------------------------------------------------------------------------
 -- ** Pre- and post-conditions
 
---------------------------------------------------------------------------------
--- *** ResolvedState
-
--- | A datatype to keep track of which parts of the simulator state -- have been initialized already. For each allocation unit or global,
--- we keep a list of element-paths that identify the initialized
--- sub-components.
-data ResolvedState =
-  ResolvedState
-    { _rsAllocs :: Map AllocIndex [[Either String Int]]
-    , _rsGlobals :: Map String [[Either String Int]]
-    }
-  deriving (Eq, Ord, Show)
-
-makeLenses ''ResolvedState
-
-emptyResolvedState :: ResolvedState
-emptyResolvedState = ResolvedState Map.empty Map.empty
-
--- | Record the initialization of the pointer represented by the given
--- SetupValue.
-markResolved ::
-  SetupValue ext ->
-  [Either String Int] {-^ path within this object (if any) -} ->
-  ResolvedState ->
-  ResolvedState
-markResolved val0 path0 rs = go path0 val0
-  where
-    go path val =
-      case val of
-        SetupVar n         -> rs & rsAllocs %~ Map.alter (ins path) n
-        SetupGlobal _ name -> rs & rsGlobals %~ Map.alter (ins path) name
-        SetupElem _ v idx  -> go (Right idx : path) v
-        SetupField _ v fld -> go (Left fld : path) v
-        _                  -> rs
-
-    ins path Nothing = Just [path]
-    ins path (Just paths) = Just (path : paths)
-
--- | Test whether the pointer represented by the given SetupValue has
--- been initialized already.
-testResolved ::
-  SetupValue ext ->
-  [Either String Int] {-^ path within this object (if any) -} ->
-  ResolvedState ->
-  Bool
-testResolved val0 path0 rs = go path0 val0
-  where
-    go path val =
-      case val of
-        SetupVar n         -> test path (Map.lookup n (_rsAllocs rs))
-        SetupGlobal _ c    -> test path (Map.lookup c (_rsGlobals rs))
-        SetupElem _ v idx  -> go (Right idx : path) v
-        SetupField _ v fld -> go (Left fld : path) v
-        _                  -> False
-
-    test _ Nothing = False
-    test path (Just paths) = any (overlap path) paths
-
-    overlap (x : xs) (y : ys) = x == y && overlap xs ys
-    overlap [] _ = True
-    overlap _ [] = True
-
---------------------------------------------------------------------------------
--- *** Extension-specific information
-
-type family CrucibleContext ext :: Type
-
--- | How to specify allocations in this syntax extension
-type family AllocSpec ext :: Type
-
--- | The type of identifiers for types in this syntax extension
-type family TypeName ext :: Type
-
--- | The type of types of the syntax extension we're dealing with
-type family ExtType ext :: Type
-
--- | The type of points-to assertions
-type family PointsTo ext :: Type
-
--- | The type of global allocations
-type family AllocGlobal ext :: Type
 
 --------------------------------------------------------------------------------
 -- *** StateSpec
diff --git a/src/SAWScript/Crucible/Common/Setup/Type.hs b/src/SAWScript/Crucible/Common/Setup/Type.hs
index 055ec60bd3..9f47a73062 100644
--- a/src/SAWScript/Crucible/Common/Setup/Type.hs
+++ b/src/SAWScript/Crucible/Common/Setup/Type.hs
@@ -55,7 +55,7 @@ data CrucibleSetupState ext =
   CrucibleSetupState
   { _csVarCounter      :: !MS.AllocIndex
   , _csPrePost         :: !MS.PrePost
-  , _csResolvedState   :: MS.ResolvedState
+  , _csResolvedState   :: MS.ResolvedState ext
   , _csMethodSpec      :: MS.CrucibleMethodSpecIR ext
   , _csCrucibleContext :: MS.CrucibleContext ext
   }
@@ -63,14 +63,15 @@ data CrucibleSetupState ext =
 makeLenses ''CrucibleSetupState
 
 makeCrucibleSetupState ::
+  MS.ResolvedState ext ->
   MS.CrucibleContext ext ->
   MS.CrucibleMethodSpecIR ext ->
   CrucibleSetupState ext
-makeCrucibleSetupState cc mspec =
+makeCrucibleSetupState rs cc mspec =
   CrucibleSetupState
     { _csVarCounter      = MS.AllocIndex 0
     , _csPrePost         = MS.PreState
-    , _csResolvedState   = MS.emptyResolvedState
+    , _csResolvedState   = rs
     , _csMethodSpec      = mspec
     , _csCrucibleContext = cc
     }
diff --git a/src/SAWScript/Crucible/JVM/MethodSpecIR.hs b/src/SAWScript/Crucible/JVM/MethodSpecIR.hs
index 5a86d8afeb..957452f383 100644
--- a/src/SAWScript/Crucible/JVM/MethodSpecIR.hs
+++ b/src/SAWScript/Crucible/JVM/MethodSpecIR.hs
@@ -58,6 +58,7 @@ type instance MS.HasSetupStruct CJ.JVM = 'False
 type instance MS.HasSetupArray CJ.JVM = 'False
 type instance MS.HasSetupElem CJ.JVM = 'False
 type instance MS.HasSetupField CJ.JVM = 'False
+type instance MS.HasSetupCast CJ.JVM = 'False
 type instance MS.HasSetupGlobalInitializer CJ.JVM = 'False
 
 type instance MS.HasGhostState CJ.JVM = 'False
@@ -67,6 +68,8 @@ type JIdent = String -- FIXME(huffman): what to put here?
 type instance MS.TypeName CJ.JVM = JIdent
 
 type instance MS.ExtType CJ.JVM = J.Type
+type instance MS.CastType CJ.JVM = ()
+type instance MS.ResolvedState CJ.JVM = ()
 
 --------------------------------------------------------------------------------
 -- *** JVMMethodId
@@ -222,7 +225,7 @@ initialCrucibleSetupState ::
   ProgramLoc ->
   Setup.CrucibleSetupState CJ.JVM
 initialCrucibleSetupState cc (cls, method) loc =
-  Setup.makeCrucibleSetupState cc $
+  Setup.makeCrucibleSetupState () cc $
     initialDefCrucibleMethodSpecIR
       (cc ^. jccCodebase)
       (J.className cls)
diff --git a/src/SAWScript/Crucible/JVM/Override.hs b/src/SAWScript/Crucible/JVM/Override.hs
index f03f7ee811..ce464d92aa 100644
--- a/src/SAWScript/Crucible/JVM/Override.hs
+++ b/src/SAWScript/Crucible/JVM/Override.hs
@@ -963,6 +963,7 @@ instantiateSetupValue sc s v =
     MS.SetupArray empty _             -> absurd empty
     MS.SetupElem empty _ _            -> absurd empty
     MS.SetupField empty _ _           -> absurd empty
+    MS.SetupCast empty _ _            -> absurd empty
     MS.SetupGlobalInitializer empty _ -> absurd empty
   where
     doTerm (TypedTerm schema t) = TypedTerm schema <$> scInstantiateExt sc s t
diff --git a/src/SAWScript/Crucible/JVM/ResolveSetupValue.hs b/src/SAWScript/Crucible/JVM/ResolveSetupValue.hs
index d9f6d243a8..ddf904b0a5 100644
--- a/src/SAWScript/Crucible/JVM/ResolveSetupValue.hs
+++ b/src/SAWScript/Crucible/JVM/ResolveSetupValue.hs
@@ -144,6 +144,7 @@ typeOfSetupValue _cc env _nameEnv val =
     MS.SetupArray empty _             -> absurd empty
     MS.SetupElem empty _ _            -> absurd empty
     MS.SetupField empty _ _           -> absurd empty
+    MS.SetupCast empty _ _            -> absurd empty
     MS.SetupGlobalInitializer empty _ -> absurd empty
 
 lookupAllocIndex :: Map AllocIndex a -> AllocIndex -> a
@@ -173,6 +174,7 @@ resolveSetupVal cc env _tyenv _nameEnv val =
     MS.SetupArray empty _             -> absurd empty
     MS.SetupElem empty _ _            -> absurd empty
     MS.SetupField empty _ _           -> absurd empty
+    MS.SetupCast empty _ _            -> absurd empty
     MS.SetupGlobalInitializer empty _ -> absurd empty
   where
     sym = cc^.jccSym
diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs
index 4dc5da2414..f31cfab88b 100644
--- a/src/SAWScript/Crucible/LLVM/Builtins.hs
+++ b/src/SAWScript/Crucible/LLVM/Builtins.hs
@@ -63,6 +63,7 @@ module SAWScript.Crucible.LLVM.Builtins
     , llvm_alloc_global
     , llvm_fresh_expanded_val
     , llvm_sizeof
+    , llvm_cast_pointer
 
     --
     -- These function are common to LLVM & JVM implementation (not for external use)
@@ -2102,6 +2103,9 @@ llvm_fresh_pointer lty =
      memTy <- memTypeForLLVMType loc lty
      constructFreshPointer (llvmTypeAlias lty) loc memTy
 
+llvm_cast_pointer :: AllLLVM SetupValue -> L.Type -> AllLLVM SetupValue
+llvm_cast_pointer ptr lty = mkAllLLVM (SetupCast () (getAllLLVM ptr) lty)
+
 constructFreshPointer ::
   Crucible.HasPtrWidth (Crucible.ArchWidth arch) =>
   Maybe Crucible.Ident ->
@@ -2236,7 +2240,7 @@ llvm_points_to_bitfield (getAllLLVM -> ptr) fieldName (getAllLLVM -> val) =
           -- have multiple llvm_points_to_bitfield statements on the same
           -- pointer provided that the field names are different, so we use
           -- the field name as the path.
-          let path = [Left fieldName]
+          let path = [ResolvedField fieldName]
           _ <- llvm_points_to_check_lhs_validity ptr loc path
 
           bfIndex <- resolveSetupBitfieldIndexOrFail cc env nameEnv ptr fieldName
@@ -2263,16 +2267,16 @@ llvm_points_to_bitfield (getAllLLVM -> ptr) fieldName (getAllLLVM -> val) =
 llvm_points_to_check_lhs_validity ::
   SetupValue (LLVM arch) {- ^ lhs pointer -} ->
   W4.ProgramLoc {- ^ the location in the program -} ->
-  [Either String Int] {- ^ the path from the pointer to the pointee -} ->
+  ResolvedPath {- ^ the path from the pointer to the pointee -} ->
   StateT (Setup.CrucibleSetupState (LLVM arch)) TopLevel Crucible.MemType
 llvm_points_to_check_lhs_validity ptr loc path =
   do cc <- getLLVMCrucibleContext
      let ?lc = ccTypeCtx cc
      st <- get
      let rs = st ^. Setup.csResolvedState
-     if st ^. Setup.csPrePost == PreState && MS.testResolved ptr path rs
+     if st ^. Setup.csPrePost == PreState && testResolved ptr path rs
        then throwCrucibleSetup loc "Multiple points-to preconditions on same pointer"
-       else Setup.csResolvedState %= MS.markResolved ptr path
+       else Setup.csResolvedState %= markResolved ptr path
      let env = MS.csAllocations (st ^. Setup.csMethodSpec)
          nameEnv = MS.csTypeNames (st ^. Setup.csMethodSpec)
      ptrTy <- typeOfSetupValue cc env nameEnv ptr
@@ -2317,9 +2321,9 @@ llvm_points_to_array_prefix (getAllLLVM -> ptr) arr sz =
        do let ?lc = ccTypeCtx cc
           st <- get
           let rs = st ^. Setup.csResolvedState
-          if st ^. Setup.csPrePost == PreState && MS.testResolved ptr [] rs
+          if st ^. Setup.csPrePost == PreState && testResolved ptr [] rs
             then throwCrucibleSetup loc "Multiple points-to preconditions on same pointer"
-            else Setup.csResolvedState %= MS.markResolved ptr []
+            else Setup.csResolvedState %= markResolved ptr []
           let env = MS.csAllocations (st ^. Setup.csMethodSpec)
               nameEnv = MS.csTypeNames (st ^. Setup.csMethodSpec)
           ptrTy <- typeOfSetupValue cc env nameEnv ptr
diff --git a/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs b/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs
index 1a76ba1aa6..f7a64dbf0c 100644
--- a/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs
+++ b/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs
@@ -94,6 +94,7 @@ module SAWScript.Crucible.LLVM.MethodSpecIR
   , getAllLLVM
   , anySetupTerm
   , anySetupArray
+  , anySetupCast
   , anySetupStruct
   , anySetupElem
   , anySetupField
@@ -105,11 +106,22 @@ module SAWScript.Crucible.LLVM.MethodSpecIR
   , pattern SomeLLVM
   , mkSomeLLVM
   , getSomeLLVM
+    -- * ResolvedState
+  , LLVMResolvedState
+  , ResolvedPath
+  , ResolvedPathItem(..)
+  , emptyResolvedState
+  , rsAllocs
+  , rsGlobals
+  , markResolved
+  , testResolved
   ) where
 
 import           Control.Lens
 import           Control.Monad (when)
 import           Data.Functor.Compose (Compose(..))
+import           Data.Map ( Map )
+import qualified Data.Map as Map
 import qualified Data.Text as Text
 import           Data.Type.Equality (TestEquality(..))
 import qualified Prettyprinter as PPL
@@ -160,6 +172,7 @@ type instance MS.HasSetupStruct (LLVM _) = 'True
 type instance MS.HasSetupArray (LLVM _) = 'True
 type instance MS.HasSetupElem (LLVM _) = 'True
 type instance MS.HasSetupField (LLVM _) = 'True
+type instance MS.HasSetupCast (LLVM _) = 'True
 type instance MS.HasSetupGlobal (LLVM _) = 'True
 type instance MS.HasSetupGlobalInitializer (LLVM _) = 'True
 
@@ -167,6 +180,7 @@ type instance MS.HasGhostState (LLVM _) = 'True
 
 type instance MS.TypeName (LLVM arch) = CL.Ident
 type instance MS.ExtType (LLVM arch) = CL.MemType
+type instance MS.CastType (LLVM arch) = L.Type
 
 --------------------------------------------------------------------------------
 -- *** LLVMMethodId
@@ -507,7 +521,7 @@ initialCrucibleSetupState ::
   Either SetupError (Setup.CrucibleSetupState (LLVM arch))
 initialCrucibleSetupState cc def loc parent = do
   ms <- initialDefCrucibleMethodSpecIR (cc ^. ccLLVMModule) def loc parent
-  return $ Setup.makeCrucibleSetupState cc ms
+  return $ Setup.makeCrucibleSetupState emptyResolvedState cc ms
 
 initialCrucibleSetupStateDecl ::
   (?lc :: CL.TypeContext) =>
@@ -518,7 +532,7 @@ initialCrucibleSetupStateDecl ::
   Either SetupError (Setup.CrucibleSetupState (LLVM arch))
 initialCrucibleSetupStateDecl cc dec loc parent = do
   ms <- initialDeclCrucibleMethodSpecIR (cc ^. ccLLVMModule) dec loc parent
-  return $ Setup.makeCrucibleSetupState cc ms
+  return $ Setup.makeCrucibleSetupState emptyResolvedState cc ms
 
 --------------------------------------------------------------------------------
 -- ** AllLLVM/SomeLLVM
@@ -562,6 +576,9 @@ anySetupStruct b vals = mkAllLLVM (MS.SetupStruct () b $ map (\a -> getAllLLVM a
 anySetupElem :: AllLLVM MS.SetupValue -> Int -> AllLLVM MS.SetupValue
 anySetupElem val idx = mkAllLLVM (MS.SetupElem () (getAllLLVM val) idx)
 
+anySetupCast :: AllLLVM MS.SetupValue -> L.Type -> AllLLVM MS.SetupValue
+anySetupCast val ty = mkAllLLVM (MS.SetupCast () (getAllLLVM val) ty)
+
 anySetupField :: AllLLVM MS.SetupValue -> String -> AllLLVM MS.SetupValue
 anySetupField val field = mkAllLLVM (MS.SetupField () (getAllLLVM val) field)
 
@@ -597,3 +614,89 @@ mkSomeLLVM x = Some (Compose x)
 
 getSomeLLVM :: forall t. (forall arch. t (LLVM arch)) -> AllLLVM t
 getSomeLLVM x = All (Compose x)
+
+--------------------------------------------------------------------------------
+-- *** ResolvedState
+
+type instance MS.ResolvedState (LLVM arch) = LLVMResolvedState
+
+data ResolvedPathItem
+  = ResolvedField String
+  | ResolvedElem Int
+  | ResolvedCast L.Type
+ deriving (Show, Eq, Ord)
+
+type ResolvedPath = [ResolvedPathItem]
+
+-- | A datatype to keep track of which parts of the simulator state
+-- have been initialized already. For each allocation unit or global,
+-- we keep a list of element-paths that identify the initialized
+-- sub-components.
+--
+-- Note that the data collected and maintained by this datatype
+-- represents a \"best-effort\" check that attempts to prevent
+-- the user from stating unsatisfiable method specifications.
+--
+-- It will not prevent all cases of overlapping points-to
+-- specifications, especially in the presence of pointer casts.
+-- A typical result of overlapping specifications will be
+-- successful (vacuous) verifications of functions resulting in
+-- overrides that cannot be used at call sites (as their
+-- preconditions are unsatisfiable).
+data LLVMResolvedState =
+  ResolvedState
+    { _rsAllocs :: Map MS.AllocIndex [ResolvedPath]
+    , _rsGlobals :: Map String [ResolvedPath]
+    }
+  deriving (Eq, Ord, Show)
+
+emptyResolvedState :: LLVMResolvedState
+emptyResolvedState = ResolvedState Map.empty Map.empty
+
+makeLenses ''LLVMResolvedState
+
+-- | Record the initialization of the pointer represented by the given
+-- SetupValue.
+markResolved ::
+  MS.SetupValue (LLVM arch) ->
+  ResolvedPath {-^ path within this object (if any) -} ->
+  LLVMResolvedState ->
+  LLVMResolvedState
+markResolved val0 path0 rs = go path0 val0
+  where
+    go path val =
+      case val of
+        MS.SetupVar n         -> rs & rsAllocs %~ Map.alter (ins path) n
+        MS.SetupGlobal _ name -> rs & rsGlobals %~ Map.alter (ins path) name
+        MS.SetupElem _ v idx  -> go (ResolvedElem idx : path) v
+        MS.SetupField _ v fld -> go (ResolvedField fld : path) v
+        MS.SetupCast _ v tp   -> go (ResolvedCast tp : path) v
+        _                     -> rs
+
+    ins path Nothing = Just [path]
+    ins path (Just paths) = Just (path : paths)
+
+-- | Test whether the pointer represented by the given SetupValue has
+-- been initialized already.
+testResolved ::
+  MS.SetupValue (LLVM arch) ->
+  ResolvedPath {-^ path within this object (if any) -} ->
+  LLVMResolvedState ->
+  Bool
+testResolved val0 path0 rs = go path0 val0
+  where
+    go path val =
+      case val of
+        MS.SetupVar n         -> test path (Map.lookup n (_rsAllocs rs))
+        MS.SetupGlobal _ c    -> test path (Map.lookup c (_rsGlobals rs))
+        MS.SetupElem _ v idx  -> go (ResolvedElem idx : path) v
+        MS.SetupField _ v fld -> go (ResolvedField fld : path) v
+        MS.SetupCast _ v tp   -> go (ResolvedCast tp : path) v
+        _                     -> False
+
+    test _ Nothing = False
+    test path (Just paths) = any (overlap path) paths
+
+    overlap (x : xs) (y : ys) = x == y && overlap xs ys
+    overlap [] _ = True
+    overlap _ [] = True
diff --git a/src/SAWScript/Crucible/LLVM/Override.hs b/src/SAWScript/Crucible/LLVM/Override.hs
index 70145e9b33..694f8bccc1 100644
--- a/src/SAWScript/Crucible/LLVM/Override.hs
+++ b/src/SAWScript/Crucible/LLVM/Override.hs
@@ -1022,6 +1022,7 @@ matchPointsTos opts sc cc spec prepost = go False []
         SetupArray _ xs            -> foldMap setupVars xs
         SetupElem _ x _            -> setupVars x
         SetupField _ x _           -> setupVars x
+        SetupCast _ x _            -> setupVars x
         SetupTerm _                -> Set.empty
         SetupNull _                -> Set.empty
         SetupGlobal _ _            -> Set.empty
@@ -2351,6 +2352,7 @@ instantiateSetupValue sc s v =
     SetupArray () vs         -> SetupArray ()    <$> mapM (instantiateSetupValue sc s) vs
     SetupElem{}              -> return v
     SetupField{}             -> return v
+    SetupCast{}              -> return v
     SetupNull{}              -> return v
     SetupGlobal{}            -> return v
     SetupGlobalInitializer{} -> return v
diff --git a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs
index 0c967cd120..db16fb3b00 100644
--- a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs
+++ b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs
@@ -109,6 +109,9 @@ resolveSetupValueInfo cc env nameEnv v =
       | Just alias <- Map.lookup i nameEnv
       -> L.Pointer (L.guessAliasInfo mdMap alias)
 
+    SetupCast () _ (L.Alias alias)
+      -> L.Pointer (L.guessAliasInfo mdMap alias)
+
     SetupField () a n ->
        fromMaybe L.Unknown $
        do L.Pointer (L.Structure xs) <- return (resolveSetupValueInfo cc env nameEnv a)
@@ -329,6 +332,21 @@ typeOfSetupValue' cc env nameEnv val =
                              , "instead got:"
                              , show (ppTypedTermType tp)
                              ]
+    SetupCast () v ltp ->
+      do memTy <- typeOfSetupValue cc env nameEnv v
+         case memTy of
+           Crucible.PtrType _symTy ->
+             case let ?lc = lc in Crucible.liftMemType (L.PtrTo ltp) of
+               Left err -> fail $ unlines [ "typeOfSetupValue: invalid type " ++ show ltp
+                                          , "Details:"
+                                          , err
+                                          ]
+               Right mt -> return mt
+
+           _ -> fail $ unwords $
+                  [ "typeOfSetupValue: tried to cast the type of a non-pointer value"
+                  , "actual type of value: " ++ show memTy
+                  ]
     SetupStruct () packed vs ->
       do memTys <- traverse (typeOfSetupValue cc env nameEnv) vs
          let si = Crucible.mkStructInfo dl packed memTys
@@ -458,6 +476,9 @@ resolveSetupVal cc mem env tyenv nameEnv val =
       | Just ptr <- Map.lookup i env -> return (Crucible.ptrToPtrVal ptr)
       | otherwise -> fail ("resolveSetupVal: Unresolved prestate variable:" ++ show i)
     SetupTerm tm -> resolveTypedTerm cc tm
+    -- NB, SetupCast values should always be pointers. Pointer casts have no
+    -- effect on the actual computed LLVMVal.
+    SetupCast () v _lty -> resolveSetupVal cc mem env tyenv nameEnv v
     SetupStruct () packed vs -> do
       vals <- mapM (resolveSetupVal cc mem env tyenv nameEnv) vs
       let tps = map Crucible.llvmValStorableType vals
diff --git a/src/SAWScript/Crucible/LLVM/X86.hs b/src/SAWScript/Crucible/LLVM/X86.hs
index 0db88b49a8..0d0a02c3be 100644
--- a/src/SAWScript/Crucible/LLVM/X86.hs
+++ b/src/SAWScript/Crucible/LLVM/X86.hs
@@ -570,7 +570,7 @@ buildMethodSpec lm nm loc checkSat setup =
     let initialMethodSpec = MS.makeCrucibleMethodSpecIR @LLVM
           methodId mtargs mtret programLoc lm
     view Setup.csMethodSpec <$> execStateT (runLLVMCrucibleSetupM setup)
-      (Setup.makeCrucibleSetupState cc initialMethodSpec)
+      (Setup.makeCrucibleSetupState emptyResolvedState cc initialMethodSpec)
 
 llvmTypeToMemType ::
   C.LLVM.TypeContext ->
diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs
index d948beef22..7df26f6d31 100644
--- a/src/SAWScript/Interpreter.hs
+++ b/src/SAWScript/Interpreter.hs
@@ -2617,6 +2617,14 @@ primitives = Map.fromList
     Current
     [ "Legacy alternative name for `llvm_return`." ]
 
+  , prim "llvm_cast_pointer" "SetupValue -> LLVMType -> SetupValue"
+    (pureVal llvm_cast_pointer)
+    Current
+    [ "Cast the type of the given setup value (which must be a pointer value)."
+    , "The resulting setup value will be a pointer to the same location, treated"
+    , "as a pointer to the provided type."
+    ]
+
   , prim "llvm_verify"
     "LLVMModule -> String -> [LLVMSpec] -> Bool -> LLVMSetup () -> ProofScript () -> TopLevel LLVMSpec"
     (pureVal llvm_verify)