diff --git a/copilot-verifier/src/Copilot/Verifier.hs b/copilot-verifier/src/Copilot/Verifier.hs
index 12f36d7..7cfae0e 100644
--- a/copilot-verifier/src/Copilot/Verifier.hs
+++ b/copilot-verifier/src/Copilot/Verifier.hs
@@ -105,7 +105,9 @@ import Crux.LLVM.Config (llvmCruxConfig, LLVMOptions(..))
 import Crux.LLVM.Compile (genBitCode)
 import Crux.LLVM.Simulate (setupSimCtxt, parseLLVM, explainFailure)
 import CruxLLVMMain
-  (withCruxLLVMLogging, cruxLLVMLoggingToSayWhat, processLLVMOptions)
+  ( CruxLLVMLogging, withCruxLLVMLogging
+  , cruxLLVMLoggingToSayWhat, processLLVMOptions
+  )
 
 import What4.Config
   (extendConfig)
@@ -141,7 +143,8 @@ verify csettings0 properties prefix spec =
           let csettings = csettings0{ cSettingsOutputDirectory = Just odir }
           let csrc = odir </> prefix ++ ".c"
           let cruxOpts1 = cruxOpts0{ outDir = odir, bldDir = odir, inputFiles = [csrc] }
-          let ?outputConfig = defaultOutputConfig cruxLogMessageToSayWhat (Just cruxOpts1)
+          ocfg <- defaultOutputConfig cruxLogMessageToSayWhat
+          let ?outputConfig = ocfg (Just cruxOpts1)
           cruxOpts2 <- withCruxLogMessage (postprocessOptions cruxOpts1)
           (cruxOpts3, llvmOpts2) <- processLLVMOptions (cruxOpts2, llvmOpts0{ optLevel = 0 })
           return (cruxOpts3, llvmOpts2, csettings, csrc)
@@ -149,13 +152,15 @@ verify csettings0 properties prefix spec =
      compileWith csettings prefix spec
      putStrLn ("Generated " ++ show csrc)
 
-     let ?outputConfig = defaultOutputConfig cruxLLVMLoggingToSayWhat (Just cruxOpts)
+     ocfg <- defaultOutputConfig cruxLLVMLoggingToSayWhat
+     let ?outputConfig = ocfg (Just cruxOpts)
      bcFile <- withCruxLLVMLogging (genBitCode cruxOpts llvmOpts)
      putStrLn ("Compiled " ++ prefix ++ " into " ++ bcFile)
 
      verifyBitcode csettings properties spec cruxOpts llvmOpts bcFile
 
 verifyBitcode ::
+  Logs CruxLLVMLogging =>
   CSettings ->
   [String] ->
   Spec ->
@@ -170,7 +175,6 @@ verifyBitcode csettings properties spec cruxOpts llvmOpts bcFile =
      startCaching sym
      bbMapRef <- newIORef mempty
      let ?recordLLVMAnnotation = \an bb -> modifyIORef bbMapRef (Map.insert an bb)
-     let ?outputConfig = defaultOutputConfig cruxLLVMLoggingToSayWhat (Just cruxOpts)
 
      let adapters = [z3Adapter] -- TODO? configurable
      extendConfig (solver_adapter_config_options z3Adapter) (getConfiguration sym)
@@ -181,8 +185,9 @@ verifyBitcode csettings properties spec cruxOpts llvmOpts bcFile =
                   { printHandle = view outputHandle ?outputConfig }
 
      llvmMod <- parseLLVM bcFile
-     Some trans <- let ?transOpts = transOpts llvmOpts
-                    in translateModule halloc memVar llvmMod
+     (Some trans, _warns) <-
+        let ?transOpts = transOpts llvmOpts
+         in translateModule halloc memVar llvmMod
 
      putStrLn ("Translated bitcode into Crucible")
 
diff --git a/deps/crucible b/deps/crucible
index 600231b..9b0fe15 160000
--- a/deps/crucible
+++ b/deps/crucible
@@ -1 +1 @@
-Subproject commit 600231b113abc361a1676d50fecc9fa94eb61bb3
+Subproject commit 9b0fe15eef44e994e859183b5a98b24356ba636b
diff --git a/deps/llvm-pretty b/deps/llvm-pretty
index 97fd46c..7ab7ac9 160000
--- a/deps/llvm-pretty
+++ b/deps/llvm-pretty
@@ -1 +1 @@
-Subproject commit 97fd46c51f59ba8aa836a00e04d59945b494a1d8
+Subproject commit 7ab7ac98eab93b6a84472fb040621adf0b150297
diff --git a/deps/llvm-pretty-bc-parser b/deps/llvm-pretty-bc-parser
index d1a6057..24dc69a 160000
--- a/deps/llvm-pretty-bc-parser
+++ b/deps/llvm-pretty-bc-parser
@@ -1 +1 @@
-Subproject commit d1a605738498e32e366d2d0e7020d442f5d757fb
+Subproject commit 24dc69a4e718193d65874d84466a7daecf8d8356
diff --git a/deps/what4 b/deps/what4
index 26a47b8..54ee2bb 160000
--- a/deps/what4
+++ b/deps/what4
@@ -1 +1 @@
-Subproject commit 26a47b8e11031ff94b59b2d075086aef592a87d5
+Subproject commit 54ee2bb4535ca939c1615111cd91398555bb600f