diff --git a/deps/crucible b/deps/crucible
index 6ca63440a0..319b6a625a 160000
--- a/deps/crucible
+++ b/deps/crucible
@@ -1 +1 @@
-Subproject commit 6ca63440a017dc6e99ea421ef60a1b879e70ec5a
+Subproject commit 319b6a625a805a51b062b69e16e3c316eec9af3f
diff --git a/deps/cryptol b/deps/cryptol
index 36bcfab5e9..c67a777689 160000
--- a/deps/cryptol
+++ b/deps/cryptol
@@ -1 +1 @@
-Subproject commit 36bcfab5e971f06db379a9e1c49bbd33f2d679aa
+Subproject commit c67a77768919584a5dcdd9b51d5d29bee2adf1a1
diff --git a/deps/macaw b/deps/macaw
index 3c2d237a59..6a83d23989 160000
--- a/deps/macaw
+++ b/deps/macaw
@@ -1 +1 @@
-Subproject commit 3c2d237a597e512b7116c080a4fe72fb3decfde3
+Subproject commit 6a83d23989a44eb7b57b411e7fb2c425d2d95565
diff --git a/deps/saw-core b/deps/saw-core
index c5da982c89..920a0148b5 160000
--- a/deps/saw-core
+++ b/deps/saw-core
@@ -1 +1 @@
-Subproject commit c5da982c893d8b897a9d9945b4fcdcf1108c3a44
+Subproject commit 920a0148b581c98a7d85abb1b449f36120544ce2
diff --git a/deps/what4 b/deps/what4
index b66527eda1..1e3c18073d 160000
--- a/deps/what4
+++ b/deps/what4
@@ -1 +1 @@
-Subproject commit b66527eda1274d4f9d539d8c2956d9fe215c4aa2
+Subproject commit 1e3c18073d0c7cb04b0244c47be46c340a9363ed
diff --git a/src/SAWScript/Crucible/JVM/ResolveSetupValue.hs b/src/SAWScript/Crucible/JVM/ResolveSetupValue.hs
index d640a3d669..de81b82141 100644
--- a/src/SAWScript/Crucible/JVM/ResolveSetupValue.hs
+++ b/src/SAWScript/Crucible/JVM/ResolveSetupValue.hs
@@ -103,7 +103,7 @@ typeOfSetupValue _cc env _nameEnv val =
     MS.SetupTerm tt ->
       case ttSchema tt of
         Cryptol.Forall [] [] ty ->
-          case toJVMType (Cryptol.evalValType Map.empty ty) of
+          case toJVMType (Cryptol.evalValType mempty ty) of
             Nothing -> fail "typeOfSetupValue: non-representable type"
             Just jty -> return jty
         s -> fail $ unlines [ "typeOfSetupValue: expected monomorphic term"
@@ -158,7 +158,7 @@ resolveTypedTerm ::
 resolveTypedTerm cc tm =
   case ttSchema tm of
     Cryptol.Forall [] [] ty ->
-      resolveSAWTerm cc (Cryptol.evalValType Map.empty ty) (ttTerm tm)
+      resolveSAWTerm cc (Cryptol.evalValType mempty ty) (ttTerm tm)
     _ -> fail "resolveSetupVal: expected monomorphic term"
 
 resolveSAWPred ::
diff --git a/src/SAWScript/Crucible/LLVM/Override.hs b/src/SAWScript/Crucible/LLVM/Override.hs
index 2f25fb77cb..7f8c8d7a6d 100644
--- a/src/SAWScript/Crucible/LLVM/Override.hs
+++ b/src/SAWScript/Crucible/LLVM/Override.hs
@@ -152,7 +152,7 @@ ppLLVMVal ::
 ppLLVMVal cc val = do
   sym <- Ov.getSymInterface
   mem <- readGlobal (Crucible.llvmMemVar (ccLLVMContext cc))
-  liftIO $ Crucible.ppLLVMValWithGlobals sym (Crucible.memImplGlobalMap mem) val
+  pure $ Crucible.ppLLVMValWithGlobals sym (Crucible.memImplSymbolMap mem) val
 
 -- | Resolve a 'SetupValue' into a 'LLVMVal' and pretty-print it
 ppSetupValueAsLLVMVal ::
@@ -336,7 +336,7 @@ ppArgs sym cc cs (Crucible.RegMap args) = do
   case Crucible.lookupGlobal (Crucible.llvmMemVar (ccLLVMContext cc)) (cc^.ccLLVMGlobals) of
     Nothing -> fail "Internal error: Couldn't find LLVM memory variable"
     Just mem -> do
-      traverse (Crucible.ppLLVMValWithGlobals sym (Crucible.memImplGlobalMap mem) . fst) =<<
+      map (Crucible.ppLLVMValWithGlobals sym (Crucible.memImplSymbolMap mem) . fst) <$>
         liftIO (zipWithM aux expectedArgTypes (assignmentToList args))
 
 -- | This function is responsible for implementing the \"override\" behavior
diff --git a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs
index bbd8440ec5..8e0225afad 100644
--- a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs
+++ b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs
@@ -182,7 +182,7 @@ typeOfSetupValue' cc env nameEnv val =
     SetupTerm tt ->
       case ttSchema tt of
         Cryptol.Forall [] [] ty ->
-          case toLLVMType dl (Cryptol.evalValType Map.empty ty) of
+          case toLLVMType dl (Cryptol.evalValType mempty ty) of
             Left err -> fail (toLLVMTypeErrToString err)
             Right memTy -> return memTy
         s -> fail $ unlines [ "typeOfSetupValue: expected monomorphic term"
@@ -345,7 +345,7 @@ resolveTypedTerm ::
 resolveTypedTerm cc tm =
   case ttSchema tm of
     Cryptol.Forall [] [] ty ->
-      resolveSAWTerm cc (Cryptol.evalValType Map.empty ty) (ttTerm tm)
+      resolveSAWTerm cc (Cryptol.evalValType mempty ty) (ttTerm tm)
     _ -> fail "resolveSetupVal: expected monomorphic term"
 
 resolveSAWPred ::
@@ -650,7 +650,7 @@ memArrayToSawCoreTerm crucible_context endianess typed_term = do
 
   case ttSchema typed_term of
     Cryptol.Forall [] [] cryptol_type -> do
-      let evaluated_type = (Cryptol.evalValType Map.empty cryptol_type)
+      let evaluated_type = Cryptol.evalValType mempty cryptol_type
       fresh_array_const <- scFreshGlobal saw_context "arr"
         =<< scArrayType saw_context offset_type_term byte_type_term
       execStateT