From ee8d927a5117487dfd8d2ee62d4cb2f79fa91db5 Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Mon, 26 Apr 2021 04:58:04 -0700
Subject: [PATCH] Update cryptol and saw-core, and adapt to "persist-solver2"
 PRs.

This patch includes the following submodule PRs:
- GaloisInc/cryptol#1128 "persist-solver2"
- GaloisInc/saw-core#197 "persist-solver2"
---
 deps/cryptol                       | 2 +-
 deps/saw-core                      | 2 +-
 src/SAWScript/AutoMatch/Cryptol.hs | 4 +++-
 src/SAWScript/Builtins.hs          | 4 ++--
 src/SAWScript/Interpreter.hs       | 3 +--
 5 files changed, 8 insertions(+), 7 deletions(-)

diff --git a/deps/cryptol b/deps/cryptol
index 8ed946ea75..b4e0a7fbe3 160000
--- a/deps/cryptol
+++ b/deps/cryptol
@@ -1 +1 @@
-Subproject commit 8ed946ea75646f732e46c6917dd4e95a4d4e964e
+Subproject commit b4e0a7fbe3bd5ea450efc46cfdf0992cc857219b
diff --git a/deps/saw-core b/deps/saw-core
index 12a8f95cc6..1c05dc0d9a 160000
--- a/deps/saw-core
+++ b/deps/saw-core
@@ -1 +1 @@
-Subproject commit 12a8f95cc6eeac9d472fe6cc74f87e288ca97887
+Subproject commit 1c05dc0d9a1482ebe62c6959a804cfb96520c76e
diff --git a/src/SAWScript/AutoMatch/Cryptol.hs b/src/SAWScript/AutoMatch/Cryptol.hs
index a782ef8c86..97de1ef35a 100644
--- a/src/SAWScript/AutoMatch/Cryptol.hs
+++ b/src/SAWScript/AutoMatch/Cryptol.hs
@@ -16,6 +16,8 @@ import Data.List hiding (sort)
 import Data.Maybe
 import Data.Ord
 
+import Verifier.SAW.CryptolEnv (meSolverConfig)
+
 import Cryptol.Eval (EvalOpts(..))
 import qualified Cryptol.ModuleSystem as M
 import Cryptol.ModuleSystem.Name
@@ -33,7 +35,7 @@ getDeclsCryptol path = do
    modEnv <- M.initialModuleEnv
    let minp = M.ModuleInput True (pure evalOpts) BS.readFile modEnv
    (result, warnings) <-
-     SMT.withSolver (M.meSolverConfig modEnv) $ \s ->
+     SMT.withSolver (meSolverConfig modEnv) $ \s ->
      M.loadModuleByPath path (minp s)
    return $ do
       forM_ warnings $ liftF . flip Warning () . pretty
diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs
index bf191a09ba..1e500fdde6 100644
--- a/src/SAWScript/Builtins.hs
+++ b/src/SAWScript/Builtins.hs
@@ -89,7 +89,7 @@ import qualified Data.SBV.Dynamic as SBV
 import qualified Data.AIG as AIG
 
 -- cryptol
-import qualified Cryptol.ModuleSystem.Env as C (meSolverConfig, meSearchPath)
+import qualified Cryptol.ModuleSystem.Env as C (meSearchPath)
 import qualified Cryptol.TypeCheck as C (SolverConfig)
 import qualified Cryptol.TypeCheck.AST as C
 import qualified Cryptol.TypeCheck.PP as C (ppWithNames, pp, text, (<+>))
@@ -1148,7 +1148,7 @@ eval_int :: TypedTerm -> TopLevel Integer
 eval_int t = do
   sc <- getSharedContext
   cenv <- fmap rwCryptol getTopLevelRW
-  let cfg = C.meSolverConfig (CEnv.eModuleEnv cenv)
+  let cfg = CEnv.meSolverConfig (CEnv.eModuleEnv cenv)
   unless (null (getAllExts (ttTerm t))) $
     fail "term contains symbolic variables"
   opts <- getOptions
diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs
index 88ff31e39c..16ff9f73db 100644
--- a/src/SAWScript/Interpreter.hs
+++ b/src/SAWScript/Interpreter.hs
@@ -88,7 +88,6 @@ import           SAWScript.Crucible.LLVM.Skeleton.Builtins
 import qualified SAWScript.Crucible.LLVM.MethodSpecIR as CIR
 
 -- Cryptol
-import Cryptol.ModuleSystem.Env (meSolverConfig)
 import qualified Cryptol.Eval as V (PPOpts(..))
 import qualified Cryptol.Backend.Monad as V (runEval)
 import qualified Cryptol.Eval.Value as V (defaultPPOpts, ppValue)
@@ -609,7 +608,7 @@ print_value (VString s) = printOutLnTop Info s
 print_value (VTerm t) = do
   sc <- getSharedContext
   cenv <- fmap rwCryptol getTopLevelRW
-  let cfg = meSolverConfig (CEnv.eModuleEnv cenv)
+  let cfg = CEnv.meSolverConfig (CEnv.eModuleEnv cenv)
   unless (null (getAllExts (ttTerm t))) $
     fail "term contains symbolic variables"
   sawopts <- getOptions