diff --git a/deps/asl-translator b/deps/asl-translator
index d0bac677..a71409d4 160000
--- a/deps/asl-translator
+++ b/deps/asl-translator
@@ -1 +1 @@
-Subproject commit d0bac677e038a54f47af0467e68c4aab95a32d64
+Subproject commit a71409d4168fe7db912e85c9c53af550751a6adf
diff --git a/deps/crucible b/deps/crucible
index 5cb47b4f..996db66c 160000
--- a/deps/crucible
+++ b/deps/crucible
@@ -1 +1 @@
-Subproject commit 5cb47b4f77299b54b0ead3f93f25dc24447c80f3
+Subproject commit 996db66ca35950439282fc5724278dc5490ecd55
diff --git a/deps/dismantle b/deps/dismantle
index 1f61d725..21c5d44d 160000
--- a/deps/dismantle
+++ b/deps/dismantle
@@ -1 +1 @@
-Subproject commit 1f61d7259228bbfb51053e7c990fac6d9228e154
+Subproject commit 21c5d44d2fdfe5bfbed6278668ddd433668218a9
diff --git a/deps/semmc b/deps/semmc
index 990ce7ab..08ff6f46 160000
--- a/deps/semmc
+++ b/deps/semmc
@@ -1 +1 @@
-Subproject commit 990ce7ab63dd67cf0f23876d5d4d93da507ec11e
+Subproject commit 08ff6f46c68b0166784779744860d11d9c919f1f
diff --git a/deps/what4 b/deps/what4
index f9a8f950..b66527ed 160000
--- a/deps/what4
+++ b/deps/what4
@@ -1 +1 @@
-Subproject commit f9a8f950e7c66f0f04312ce3983a42f3facd576e
+Subproject commit b66527eda1274d4f9d539d8c2956d9fe215c4aa2
diff --git a/refinement/src/Data/Macaw/Refinement/SymbolicExecution.hs b/refinement/src/Data/Macaw/Refinement/SymbolicExecution.hs
index e1389108..6ec9e875 100644
--- a/refinement/src/Data/Macaw/Refinement/SymbolicExecution.hs
+++ b/refinement/src/Data/Macaw/Refinement/SymbolicExecution.hs
@@ -508,6 +508,7 @@ initializeMemory :: forall arch sym m proxy
                   . ( MS.SymArchConstraints arch
                     , 16 <= M.ArchAddrWidth arch
                     , CB.IsSymInterface sym
+                    , LLVM.HasLLVMAnn sym
                     , MonadIO m
                     )
                  => proxy arch
diff --git a/refinement/tests/RefinementTests.hs b/refinement/tests/RefinementTests.hs
index b22c3d8e..813141f0 100644
--- a/refinement/tests/RefinementTests.hs
+++ b/refinement/tests/RefinementTests.hs
@@ -284,10 +284,10 @@ mkSymbolicTest testinp = do
               CCC.SomeCFG cfg <- MS.mkFunCFG archFns halloc funcName (posFn proxy) dfi
               regs <- MS.macawAssignToCrucM (mkReg archFns sym) (MS.crucGenRegAssignment archFns)
               -- FIXME: We probably need to pull endianness from somewhere else
-              (initMem, memPtrTbl) <- MSM.newGlobalMemory proxy sym CLD.LittleEndian MSM.ConcreteMutable mem
-              let globalMap = MSM.mapRegionPointers memPtrTbl
               bbMapRef <- newIORef mempty
               let ?badBehaviorMap = bbMapRef
+              (initMem, memPtrTbl) <- MSM.newGlobalMemory proxy sym CLD.LittleEndian MSM.ConcreteMutable mem
+              let globalMap = MSM.mapRegionPointers memPtrTbl
               let lookupFn = MS.LookupFunctionHandle $ \_s _mem _regs ->
                     error "Could not find function handle"
               let validityCheck _ _ _ _ = return Nothing
diff --git a/symbolic/src/Data/Macaw/Symbolic/Memory.hs b/symbolic/src/Data/Macaw/Symbolic/Memory.hs
index 07578d55..7e2896fe 100644
--- a/symbolic/src/Data/Macaw/Symbolic/Memory.hs
+++ b/symbolic/src/Data/Macaw/Symbolic/Memory.hs
@@ -196,6 +196,7 @@ newGlobalMemory :: ( 16 <= MC.ArchAddrWidth arch
                    , KnownNat (MC.ArchAddrWidth arch)
                    , CB.IsSymInterface sym
                    , Ord (WI.SymExpr sym WI.BaseNatType)
+                   , CL.HasLLVMAnn sym
                    , MonadIO m
                    )
                 => proxy arch
@@ -479,6 +480,7 @@ mkGlobalPointerValidityPred mpt = \sym puse mcond ptr -> do
 mapRegionPointers :: ( MC.MemWidth w
                      , 16 <= w
                      , CB.IsSymInterface sym
+                     , CL.HasLLVMAnn sym
                      )
                   => MemPtrTable sym w
                   -> MS.GlobalMap sym CL.Mem w
diff --git a/x86_symbolic/tests/Main.hs b/x86_symbolic/tests/Main.hs
index f6ac59a1..b03045a3 100644
--- a/x86_symbolic/tests/Main.hs
+++ b/x86_symbolic/tests/Main.hs
@@ -117,12 +117,12 @@ main = do
 
   symFuns <- MX.newSymFuns sym
 
-  (initMem, memPtrTbl) <-  MSM.newGlobalMemory (Proxy @MX.X86_64) sym LittleEndian MSM.ConcreteMutable mem
-  let globalMap = MSM.mapRegionPointers memPtrTbl
-
   bbMapRef <- newIORef mempty
   let ?badBehaviorMap = bbMapRef
 
+  (initMem, memPtrTbl) <-  MSM.newGlobalMemory (Proxy @MX.X86_64) sym LittleEndian MSM.ConcreteMutable mem
+  let globalMap = MSM.mapRegionPointers memPtrTbl
+
   let lookupFn :: MS.LookupFunctionHandle sym MX.X86_64
       lookupFn = MS.LookupFunctionHandle $ \_s _mem _regs -> do
         fail "Could not find function handle."