diff --git a/deps/crucible b/deps/crucible
index dcc7071b53..cf39f32633 160000
--- a/deps/crucible
+++ b/deps/crucible
@@ -1 +1 @@
-Subproject commit dcc7071b53e27957f12718443a1700a5bdc2487c
+Subproject commit cf39f32633c5848c658093ae0ea883339e4a3a0f
diff --git a/deps/macaw b/deps/macaw
index cd4dd31343..1bc6a358d8 160000
--- a/deps/macaw
+++ b/deps/macaw
@@ -1 +1 @@
-Subproject commit cd4dd3134305901981a3f1c730b61ae98c5d7fe2
+Subproject commit 1bc6a358d8abe7cc9ccd219a0a0d3387f808416c
diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs
index 4b0ae2d916..01e4235bda 100644
--- a/src/SAWScript/Crucible/LLVM/Builtins.hs
+++ b/src/SAWScript/Crucible/LLVM/Builtins.hs
@@ -511,12 +511,10 @@ verifyMethodSpec bic opts cc methodSpec lemmas checkSat tactic asp =
          Nothing   -> fail "internal error: LLVM Memory global not found"
          Just mem0 -> return mem0
      -- push a memory stack frame if starting from a breakpoint
-     let mem = if isJust (methodSpec^.csParentName)
-               then mem0
-                 { Crucible.memImplHeap = Crucible.pushStackFrameMem
-                   (Crucible.memImplHeap mem0)
-                 }
-               else mem0
+     let mem = case methodSpec^.csParentName of
+                 Just nm -> mem0 { Crucible.memImplHeap = Crucible.pushStackFrameMem (Text.pack nm)
+                                                             (Crucible.memImplHeap mem0) }
+                 Nothing -> mem0
      let globals1 = Crucible.llvmGlobals (ccLLVMContext cc) mem
 
      -- construct the initial state for verifications
@@ -897,7 +895,7 @@ ppGlobalPair cc gp =
       globals = gp ^. Crucible.gpGlobals in
   case Crucible.lookupGlobal mvar globals of
     Nothing -> text "LLVM Memory global variable not initialized"
-    Just mem -> Crucible.ppMem mem
+    Just mem -> Crucible.ppMem (Crucible.memImplHeap mem)
 
 
 --------------------------------------------------------------------------------
diff --git a/src/SAWScript/Crucible/LLVM/Override.hs b/src/SAWScript/Crucible/LLVM/Override.hs
index bcd1be4baa..10d3c62786 100644
--- a/src/SAWScript/Crucible/LLVM/Override.hs
+++ b/src/SAWScript/Crucible/LLVM/Override.hs
@@ -1442,7 +1442,8 @@ instantiateExtResolveSAWSymBV sc cc w tm = do
 -- is overwritten by a postcondition memory write is not invalidated.
 -- Return a map containing the overwritten memory allocations.
 invalidateMutableAllocs ::
-  (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) =>
+  (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch)
+  , Crucible.HasLLVMAnn Sym) =>
   Options ->
   SharedContext ->
   LLVMCrucibleContext arch ->
diff --git a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs
index b78939395e..bbd8440ec5 100644
--- a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs
+++ b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs
@@ -17,7 +17,6 @@ Stability   : provisional
 module SAWScript.Crucible.LLVM.ResolveSetupValue
   ( LLVMVal, LLVMPtr
   , resolveSetupVal
-  , typeOfLLVMVal
   , typeOfSetupValue
   , resolveTypedTerm
   , resolveSAWPred
@@ -33,7 +32,6 @@ import Control.Monad
 import qualified Control.Monad.Fail as Fail
 import Control.Monad.State
 import qualified Data.BitVector.Sized as BV
-import Data.Foldable (toList)
 import Data.Maybe (fromMaybe, listToMaybe, fromJust)
 import Data.IORef
 import           Data.Map (Map)
@@ -280,7 +278,7 @@ resolveSetupVal cc mem env tyenv nameEnv val = do
     SetupTerm tm -> resolveTypedTerm cc tm
     SetupStruct () packed vs -> do
       vals <- mapM (resolveSetupVal cc mem env tyenv nameEnv) vs
-      let tps = map (typeOfLLVMVal dl) vals
+      let tps = map Crucible.llvmValStorableType vals
       let t = Crucible.mkStructType (V.fromList (mkFields packed dl Crucible.noAlignment 0 tps))
       let flds = case Crucible.storageTypeF t of
                    Crucible.Struct v -> v
@@ -289,7 +287,7 @@ resolveSetupVal cc mem env tyenv nameEnv val = do
     SetupArray () [] -> fail "resolveSetupVal: invalid empty array"
     SetupArray () vs -> do
       vals <- V.mapM (resolveSetupVal cc mem env tyenv nameEnv) (V.fromList vs)
-      let tp = typeOfLLVMVal dl (V.head vals)
+      let tp = Crucible.llvmValStorableType (V.head vals)
       return $ Crucible.LLVMValArray tp vals
     SetupField () v n -> do
       i <- resolveSetupFieldIndexOrFail cc tyenv nameEnv v n
@@ -543,48 +541,19 @@ typeAlignment dl ty =
     Crucible.Array _sz ty'   -> typeAlignment dl ty'
     Crucible.Struct flds     -> V.foldl max Crucible.noAlignment (fmap (typeAlignment dl . (^. Crucible.fieldVal)) flds)
 
-typeOfLLVMVal :: Crucible.DataLayout -> LLVMVal -> Crucible.StorageType
-typeOfLLVMVal _dl val =
-  case val of
-    Crucible.LLVMValInt _bkl bv ->
-       Crucible.bitvectorType (Crucible.intWidthSize (fromIntegral (natValue (W4.bvWidth bv))))
-    Crucible.LLVMValFloat _ _   -> error "FIXME: typeOfLLVMVal LLVMValFloat"
-    Crucible.LLVMValStruct flds -> Crucible.mkStructType (fmap fieldType flds)
-    Crucible.LLVMValArray tp vs -> Crucible.arrayType (fromIntegral (V.length vs)) tp
-    Crucible.LLVMValZero tp     -> tp
-    Crucible.LLVMValUndef tp    -> tp
-  where
-    fieldType (f, _) = (f ^. Crucible.fieldVal, Crucible.fieldPad f)
 
 equalValsPred ::
   LLVMCrucibleContext wptr ->
   LLVMVal ->
   LLVMVal ->
   IO (W4.Pred Sym)
-equalValsPred cc v1 v2 = go (v1, v2)
-  where
-  go :: (LLVMVal, LLVMVal) -> IO (W4.Pred Sym)
-
-  go (Crucible.LLVMValInt blk1 off1, Crucible.LLVMValInt blk2 off2)
-       | Just Refl <- testEquality (W4.bvWidth off1) (W4.bvWidth off2)
-       = do blk_eq <- W4.natEq sym blk1 blk2
-            off_eq <- W4.bvEq sym off1 off2
-            W4.andPred sym blk_eq off_eq
-  --go (Crucible.LLVMValFloat xsz x, Crucible.LLVMValFloat ysz y) | xsz == ysz
-  --     = W4.floatEq sym x y -- TODO
-  go (Crucible.LLVMValStruct xs, Crucible.LLVMValStruct ys)
-       | V.length xs == V.length ys
-       = do cs <- mapM go (zip (map snd (toList xs)) (map snd (toList ys)))
-            foldM (W4.andPred sym) (W4.truePred sym) cs
-  go (Crucible.LLVMValArray _tpx xs, Crucible.LLVMValArray _tpy ys)
-       | V.length xs == V.length ys
-       = do cs <- mapM go (zip (toList xs) (toList ys))
-            foldM (W4.andPred sym) (W4.truePred sym) cs
-
-  go _ = return (W4.falsePred sym)
+equalValsPred cc v1 v2 =
+   fromMaybe (W4.falsePred sym) <$> Crucible.testEqual sym v1 v2
 
+  where
   sym = cc^.ccBackend
 
+
 memArrayToSawCoreTerm ::
   Crucible.HasPtrWidth (Crucible.ArchWidth arch) =>
   LLVMCrucibleContext arch ->
diff --git a/src/SAWScript/X86Spec.hs b/src/SAWScript/X86Spec.hs
index 6275ce313c..14b57f3d75 100644
--- a/src/SAWScript/X86Spec.hs
+++ b/src/SAWScript/X86Spec.hs
@@ -999,7 +999,8 @@ checkAlloc sym s (l := a) =
 -- If the region ID is concretely zero, it should be the case that the
 -- 'RegionIndex' map would translate it into a real 'LLVMPtr' since the only map
 -- entry (established in 'setupGlobals') is for 0.
-mkGlobalMap :: Map.Map RegionIndex (LLVMPtr Sym 64) -> GlobalMap Sym Crucible.Mem 64
+mkGlobalMap :: Crucible.HasLLVMAnn Sym =>
+  Map.Map RegionIndex (LLVMPtr Sym 64) -> GlobalMap Sym Crucible.Mem 64
 mkGlobalMap rmap sym mem region off =
   mapConcreteRegion <|> passThroughConcreteRegion <|> mapSymbolicRegion
   where
@@ -1259,6 +1260,7 @@ lookupCry x mp =
 
 
 adjustPtr ::
+  Crucible.HasLLVMAnn Sym =>
   Sym -> MemImpl Sym -> LLVMPtr Sym 64 -> Integer -> IO (LLVMPtr Sym 64)
 adjustPtr sym mem ptr amt
   | amt == 0  = return ptr