diff --git a/deps/cryptol b/deps/cryptol
index be24bfe260..49d60aae2a 160000
--- a/deps/cryptol
+++ b/deps/cryptol
@@ -1 +1 @@
-Subproject commit be24bfe26058b3ad94bed2fda1065e0f801a7e9c
+Subproject commit 49d60aae2afdb37219bb5e05533b286ceb900485
diff --git a/deps/saw-core b/deps/saw-core
index 0d1051dc78..06162031ec 160000
--- a/deps/saw-core
+++ b/deps/saw-core
@@ -1 +1 @@
-Subproject commit 0d1051dc78200ada20ce6ffa27d00a603d464950
+Subproject commit 06162031ecc1cc5d21eff62418480740c851f053
diff --git a/saw-remote-api/src/SAWServer/CryptolExpression.hs b/saw-remote-api/src/SAWServer/CryptolExpression.hs
index e9d25d23a3..c966cc6316 100644
--- a/saw-remote-api/src/SAWServer/CryptolExpression.hs
+++ b/saw-remote-api/src/SAWServer/CryptolExpression.hs
@@ -9,7 +9,7 @@ import qualified Data.Map as Map
 import Data.Maybe (fromMaybe)
 
 import Cryptol.Eval (EvalOpts(..), defaultPPOpts)
-import Cryptol.ModuleSystem (ModuleRes)
+import Cryptol.ModuleSystem (ModuleRes, ModuleInput(..))
 import Cryptol.ModuleSystem.Base (genInferInput, getPrimMap, noPat, rename)
 import Cryptol.ModuleSystem.Env (ModuleEnv)
 import Cryptol.ModuleSystem.Interface (noIfaceParams)
@@ -47,7 +47,8 @@ getTypedTermOfCExp ::
 getTypedTermOfCExp fileReader sc cenv expr =
   do let ?fileReader = fileReader
      let env = eModuleEnv cenv
-     mres <- runModuleM (defaultEvalOpts, B.readFile, env) $
+     let minp = ModuleInput True defaultEvalOpts B.readFile env
+     mres <- runModuleM minp $
        do npe <- interactive (noPat expr) -- eliminate patterns
 
           -- resolve names
diff --git a/saw/SAWScript/REPL/Monad.hs b/saw/SAWScript/REPL/Monad.hs
index c5b615185d..3e7f425a23 100644
--- a/saw/SAWScript/REPL/Monad.hs
+++ b/saw/SAWScript/REPL/Monad.hs
@@ -47,7 +47,7 @@ module SAWScript.REPL.Monad (
   , getSAWScriptNames
   ) where
 
-import Cryptol.Eval (EvalError)
+import Cryptol.Eval (EvalError, EvalErrorEx(..))
 import qualified Cryptol.ModuleSystem as M
 import qualified Cryptol.ModuleSystem.NamingEnv as MN
 import Cryptol.ModuleSystem.NamingEnv (NamingEnv)
@@ -235,8 +235,8 @@ rethrowEvalError m = run `X.catch` rethrow
     a <- m
     return $! a
 
-  rethrow :: EvalError -> IO a
-  rethrow exn = X.throwIO (EvalError exn)
+  rethrow :: EvalErrorEx -> IO a
+  rethrow (EvalErrorEx _ exn) = X.throwIO (EvalError exn)
 
 
 
diff --git a/src/SAWScript/AutoMatch/Cryptol.hs b/src/SAWScript/AutoMatch/Cryptol.hs
index 7088fd2aaf..8b5e242817 100644
--- a/src/SAWScript/AutoMatch/Cryptol.hs
+++ b/src/SAWScript/AutoMatch/Cryptol.hs
@@ -30,7 +30,8 @@ getDeclsCryptol :: FilePath -> IO (Interaction (Maybe [Decl]))
 getDeclsCryptol path = do
    let evalOpts = EvalOpts quietLogger defaultPPOpts
    modEnv <- M.initialModuleEnv
-   (result, warnings) <- M.loadModuleByPath path (evalOpts, BS.readFile, modEnv)
+   let minp = M.ModuleInput True evalOpts BS.readFile modEnv
+   (result, warnings) <- M.loadModuleByPath path minp
    return $ do
       forM_ warnings $ liftF . flip Warning () . pretty
       case result of
diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs
index a033dbca68..35bc972d16 100644
--- a/src/SAWScript/Builtins.hs
+++ b/src/SAWScript/Builtins.hs
@@ -1328,7 +1328,7 @@ eval_int t = do
     C.Forall [] [] (isInteger -> True) -> return ()
     _ -> fail "eval_int: argument is not a finite bitvector"
   v <- io $ rethrowEvalError $ SV.evaluateTypedTerm sc t'
-  io $ C.runEval (C.bvVal <$> C.fromVWord C.Concrete "eval_int" v)
+  io $ C.runEval mempty (C.bvVal <$> C.fromVWord C.Concrete "eval_int" v)
 
 -- Predicate on Cryptol types true of integer types, i.e. types
 -- @[n]Bit@ for *finite* @n@.
diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs
index 57d693b363..a5197a70f0 100644
--- a/src/SAWScript/Interpreter.hs
+++ b/src/SAWScript/Interpreter.hs
@@ -585,7 +585,7 @@ print_value (VTerm t) = do
                               , V.useBase = ppOptsBase opts
                               }
   evaled_t <- io $ evaluateTypedTerm sc t'
-  doc <- io $ V.runEval (V.ppValue V.Concrete opts' evaled_t)
+  doc <- io $ V.runEval mempty (V.ppValue V.Concrete opts' evaled_t)
   sawOpts <- getOptions
   io (rethrowEvalError $ printOutLn sawOpts Info $ show $ doc)
 
diff --git a/src/SAWScript/JavaBuiltins.hs b/src/SAWScript/JavaBuiltins.hs
index d763b5b226..4ff7cd93a9 100644
--- a/src/SAWScript/JavaBuiltins.hs
+++ b/src/SAWScript/JavaBuiltins.hs
@@ -308,7 +308,7 @@ showCexResults vpopts sc opts ms vs exts vals = do
   printOutLn vpopts Info $ "When verifying " ++ specName ms ++ ":"
   printOutLn vpopts Info $ "Proof of " ++ vsVCName vs ++ " failed."
   printOutLn vpopts Info $ "Counterexample:"
-  let showVal v = show <$> (Cryptol.runEval
+  let showVal v = show <$> (Cryptol.runEval mempty
                     (Cryptol.ppValue Cryptol.Concrete (cryptolPPOpts opts) (exportFirstOrderValue v)))
   mapM_ (\(n, v) -> do vdoc <- showVal v
                        printOutLn vpopts Info ("  " ++ n ++ ": " ++ vdoc)) vals
diff --git a/src/SAWScript/VerificationCheck.hs b/src/SAWScript/VerificationCheck.hs
index 542a043b67..58fc679308 100644
--- a/src/SAWScript/VerificationCheck.hs
+++ b/src/SAWScript/VerificationCheck.hs
@@ -61,8 +61,8 @@ vcCounterexample sc opts (EqualityCheck nm impNode specNode) evalFn =
          sv = exportValueWithSchema sschema sn
          opts' = SV.cryptolPPOpts opts
      -- Grr. Different pretty-printers.
-     lv_doc <- CV.runEval (CV.ppValue CV.Concrete opts' lv)
-     sv_doc <- CV.runEval (CV.ppValue CV.Concrete opts' sv)
+     lv_doc <- CV.runEval mempty (CV.ppValue CV.Concrete opts' lv)
+     sv_doc <- CV.runEval mempty (CV.ppValue CV.Concrete opts' sv)
 
      return $
        vcat