diff --git a/deps/cryptol b/deps/cryptol
index 0abde1e55e..538b6c4ff5 160000
--- a/deps/cryptol
+++ b/deps/cryptol
@@ -1 +1 @@
-Subproject commit 0abde1e55e4db85a054e8976c61531ca7d29137a
+Subproject commit 538b6c4ff5c8ae83ca27f320357d534c9ae69249
diff --git a/deps/saw-core b/deps/saw-core
index ed0d14aa85..78185d35a9 160000
--- a/deps/saw-core
+++ b/deps/saw-core
@@ -1 +1 @@
-Subproject commit ed0d14aa85818be4eb258832115ed77348ea8846
+Subproject commit 78185d35a936765a906e1181b3a5c13e28336bef
diff --git a/saw-remote-api/src/SAWServer/CryptolExpression.hs b/saw-remote-api/src/SAWServer/CryptolExpression.hs
index 6cff2c924b..6da82d66ee 100644
--- a/saw-remote-api/src/SAWServer/CryptolExpression.hs
+++ b/saw-remote-api/src/SAWServer/CryptolExpression.hs
@@ -24,7 +24,7 @@ import Data.Traversable (for)
 import Cryptol.Eval (EvalOpts(..))
 import Cryptol.ModuleSystem (ModuleRes, ModuleInput(..))
 import Cryptol.ModuleSystem.Base (genInferInput, getPrimMap, noPat, rename)
-import Cryptol.ModuleSystem.Env (ModuleEnv)
+import Cryptol.ModuleSystem.Env (ModuleEnv, meSolverConfig)
 import Cryptol.ModuleSystem.Interface (noIfaceParams)
 import Cryptol.ModuleSystem.Monad (ModuleM, interactive, runModuleM, setNameSeeds, setSupply, typeCheckWarnings, typeCheckingFailed)
 import qualified Cryptol.ModuleSystem.Renamer as MR
@@ -33,6 +33,7 @@ import qualified Cryptol.Parser as CP
 import Cryptol.Parser.Position (emptyRange, getLoc)
 import Cryptol.TypeCheck (tcExpr)
 import Cryptol.TypeCheck.Monad (InferOutput(..), inpVars, inpTSyns)
+import Cryptol.TypeCheck.Solver.SMT (withSolver)
 import Cryptol.Utils.Ident (interactiveName)
 import Cryptol.Utils.Logger (quietLogger)
 import Cryptol.Utils.PP
@@ -64,7 +65,9 @@ getTypedTermOfCExp fileReader sc cenv expr =
   do let ?fileReader = fileReader
      let env = eModuleEnv cenv
      let minp = ModuleInput True (pure defaultEvalOpts) B.readFile env
-     mres <- runModuleM minp $
+     mres <-
+       withSolver (meSolverConfig env) $ \s ->
+       runModuleM (minp s) $
        do npe <- interactive (noPat expr) -- eliminate patterns
 
           -- resolve names
diff --git a/src/SAWScript/AutoMatch.hs b/src/SAWScript/AutoMatch.hs
index 497070bb54..23b86b825e 100644
--- a/src/SAWScript/AutoMatch.hs
+++ b/src/SAWScript/AutoMatch.hs
@@ -435,7 +435,8 @@ processResults (TaggedSourceFile leftLang  leftFile) (TaggedSourceFile rightLang
 
       cryptolAbstractNamesSAW :: [SAWScript.LName] -> Cryptol.Expr Cryptol.PName -> Cryptol.Expr Cryptol.PName
       cryptolAbstractNamesSAW names expr =
-         Cryptol.EFun (for names $ Cryptol.PVar . cryptolLocate . SAWScript.getVal) expr
+         Cryptol.EFun Cryptol.emptyFunDesc
+         (for names $ Cryptol.PVar . cryptolLocate . SAWScript.getVal) expr
 
       cryptolApplyFunctionSAW :: SAWScript.LName -> [SAWScript.LName] -> Cryptol.Expr Cryptol.PName
       cryptolApplyFunctionSAW function args =
diff --git a/src/SAWScript/AutoMatch/Cryptol.hs b/src/SAWScript/AutoMatch/Cryptol.hs
index ef6e4f8bb0..a782ef8c86 100644
--- a/src/SAWScript/AutoMatch/Cryptol.hs
+++ b/src/SAWScript/AutoMatch/Cryptol.hs
@@ -22,6 +22,7 @@ import Cryptol.ModuleSystem.Name
 import Cryptol.Utils.Ident (unpackIdent)
 import Cryptol.Utils.Logger (quietLogger)
 import qualified Cryptol.TypeCheck.AST as AST
+import qualified Cryptol.TypeCheck.Solver.SMT as SMT
 import Cryptol.Utils.PP
 
 -- | Parse a Cryptol module into a list of declarations
@@ -31,7 +32,9 @@ getDeclsCryptol path = do
    let evalOpts = EvalOpts quietLogger defaultPPOpts
    modEnv <- M.initialModuleEnv
    let minp = M.ModuleInput True (pure evalOpts) BS.readFile modEnv
-   (result, warnings) <- M.loadModuleByPath path minp
+   (result, warnings) <-
+     SMT.withSolver (M.meSolverConfig modEnv) $ \s ->
+     M.loadModuleByPath path (minp s)
    return $ do
       forM_ warnings $ liftF . flip Warning () . pretty
       case result of