diff --git a/.github/ci.sh b/.github/ci.sh
index fbb961e785..2b865a8cc3 100755
--- a/.github/ci.sh
+++ b/.github/ci.sh
@@ -163,10 +163,7 @@ install_system_deps() {
 }
 
 test_dist() {
-  (cd intTests &&
-    env &&
-    LOUD=true ./runtests.sh &&
-    sh -c "! grep '<failure>' results.xml")
+  VERBOSE=y cabal v2-test integration_tests
 }
 
 build_cryptol() {
diff --git a/.gitignore b/.gitignore
index 4b312cbf5e..bba708807a 100644
--- a/.gitignore
+++ b/.gitignore
@@ -20,3 +20,11 @@ cabal.project.freeze
 *~
 *#
 .#*
+intTests/test_intro_examples/*.cnf
+intTests/test_llvm_x86_0[1234]/test
+intTests/test_llvm_x86_0[1234]/test.o
+intTests/test_llvm_x86_0[1234]/test.bc
+intTests/test*/*.out
+intTests/test_crucible_jvm/Stat.class
+intTests/test_profiling/prof
+intTests/test_smtlib/*.smt2
diff --git a/deps/saw-core b/deps/saw-core
index f7b6b74c93..ead69c0d0d 160000
--- a/deps/saw-core
+++ b/deps/saw-core
@@ -1 +1 @@
-Subproject commit f7b6b74c93b8463ad074913e9175b086c1fbc6ef
+Subproject commit ead69c0d0d4f2c1be463dbc89a744ed6c3a87a14
diff --git a/intTests/IntegrationTest.hs b/intTests/IntegrationTest.hs
new file mode 100644
index 0000000000..a87cd6855e
--- /dev/null
+++ b/intTests/IntegrationTest.hs
@@ -0,0 +1,221 @@
+{-# LANGUAGE LambdaCase #-}
+
+module Main where
+
+import Control.Monad ( filterM, foldM, join, unless )
+import Control.Monad.IO.Class (liftIO)
+import Data.List ( isPrefixOf, intercalate, sort )
+import Data.Maybe ( fromMaybe )
+import System.Directory ( getCurrentDirectory, findExecutable, listDirectory
+                        , doesDirectoryExist )
+import System.Environment ( lookupEnv )
+import System.Exit ( ExitCode(ExitSuccess), exitFailure )
+import System.FilePath ( (</>), pathSeparator, searchPathSeparator
+                       , takeDirectory, takeFileName, isAbsolute )
+import System.FilePath.Find ( always, find, extension, (==?) )
+import System.IO ( hPutStrLn, stderr )
+import System.Process ( readCreateProcessWithExitCode
+                      , shell, CreateProcess(..) )
+import Test.Tasty
+    ( defaultMain, localOption, testGroup, mkTimeout, TestTree )
+import Test.Tasty.HUnit ( testCase, (@=?), assertBool )
+import Test.Tasty.ExpectedFailure ( ignoreTest )
+
+
+-- | Reads from DISABLED_TESTS env var or disabled_tests.txt file
+-- (preference is given to the former) and returns the list of tests.
+-- Shell-style comments are removed, and test names are assumed to be
+-- a single word without whitespace.  The input can separate testnames
+-- with any type of whitespace (space, tab, newline).
+--
+-- Returns the list of disabled test names.
+getDisabledTestList :: FilePath -> IO [String]
+getDisabledTestList testdir = do
+  let dtfile = testdir </> "disabled_tests.txt"
+  dset <- lookupEnv "DISABLED_TESTS" >>= \case
+    Just d -> return d
+    Nothing -> readFile dtfile
+  let removeComment = takeWhile ((/=) '#')
+      stripWhitespace = words
+      processInput = join . map (stripWhitespace . removeComment) . lines
+  return $ processInput dset
+
+
+-- | Gets the list of tests (subdirectories) to run given the base
+-- directory and the list of disabled tests
+getTestList :: FilePath -> [String] -> IO [String]
+getTestList testdir disabled = do
+  f <- listDirectory testdir
+  let isTest = filter (isPrefixOf "test")
+      notDisabled = filter (not . flip elem disabled)
+      inTestdir = fmap (testdir </>)
+  filterM doesDirectoryExist $ inTestdir $ notDisabled $ isTest $ sort f
+
+
+-- ----------------------------------------------------------------------=
+-- * Environment variable handling.
+--
+-- Start with an initial set of variables and an asociated value (or
+-- set of values with a separator), then override/update with any
+-- environment variables set.
+
+data EnvVarSpec = EV String String
+                  -- ^ single string value
+                | EVp String Char [String]
+                  -- ^ accumulative path with separator
+
+updEnvVars :: String -> String -> [EnvVarSpec] -> [EnvVarSpec]
+updEnvVars n v [] = [EV n v | v /= ""]
+updEnvVars n v (EV  n'   v' : evs) | n == n' = EV  n (if v == "" then v' else v) : evs
+updEnvVars n v (EVp n' s v' : evs) | n == n' = EVp n s (v' <> [v]) : evs
+updEnvVars n v (ev : evs) = ev : updEnvVars n v evs
+
+envVarAssocList :: [EnvVarSpec] -> [(String, String)]
+envVarAssocList = map envVarAssoc
+  where
+    envVarAssoc (EV  n v)    = (n, v)
+    envVarAssoc (EVp n s vs) = (n, intercalate [s] vs)
+
+-- ----------------------------------------------------------------------
+-- * Test Parameters
+--
+--  Determine all Environment Variables that should be set for the
+--  tests, using the internal defaults plus overrides from the current
+--  environment:
+--     - SAW = saw invocation command (with jars specification)
+--     - JAVA = path to java runtime
+--     - HOME = directory to act as home when running tests
+--     - PATH = PATH searchlist, supplemented with discovered elements
+--     - JAVA_HOME = path to java installation
+--     - TESTBASE = path to intTests directory
+--     - SAW_JDK_JAR = path to rt.jar
+--
+--  These environment variables may already be set to supply default
+--  locations for these components.
+--
+--  Also determine the list of JAR files to pass to the various tests:
+--     - The rt.jar runtime library from the JAVA installation
+--     - Any jars supplied with the jvm-verifier
+--     - Any jars supplied by saw
+--
+-- Note that even if SAW is specified in the environment, this test runner will
+-- augment those definitions with the discovered jar files and target path
+-- specifications.
+
+
+-- | Returns the environment variable assocList to use for running
+-- each individual test
+testParams :: FilePath -> (String -> IO ()) -> IO [(String, String)]
+testParams intTestBase verbose = do
+  here <- getCurrentDirectory
+  let absTestBase = if isAbsolute intTestBase then intTestBase
+                    else here </> intTestBase
+
+  -- try to determine where the saw binary is in case there are other
+  -- executables there (e.g. z3, etc.)
+  sawExe <- findExecutable "saw" >>= \case
+              Just e -> return e
+              _ -> return "" -- may be supplied via env var
+
+  verbose $ "Found saw: " <> sawExe
+  let eVars0 = [ EV  "HOME"     absTestBase
+               , EVp "PATH"     searchPathSeparator [takeDirectory sawExe]
+               , EV  "TESTBASE" absTestBase
+               , EV  "DIRSEP"   [pathSeparator]
+               , EV  "CPSEP"    [searchPathSeparator]
+
+               -- The eval is used to protect the evaluation of the
+               -- single-quoted arguments supplied below when run in a
+               -- bash test.sh script.
+               , EVp "SAW"      ' ' ["eval", "saw"]
+               ]
+      addEnvVar evs e = do v <- lookupEnv e
+                           return $ updEnvVars e (fromMaybe "" v) evs
+  -- override eVars0 with any environment variables set in this process
+  e1 <- foldM addEnvVar eVars0 [ "SAW", "PATH", "JAVAC", "JAVA_HOME", "SAW_JDK_JAR" ]
+
+  -- Create a pathlist of jars for invoking saw
+  let jarsDir = absTestBase </> "jars"
+
+  let findJarsIn p = doesDirectoryExist p >>= \case
+        True -> find always (extension ==? ".jar") p
+        False -> return []
+
+  verbose $ "Finding JARs in " <> jarsDir
+  jars <- intercalate [searchPathSeparator] <$> findJarsIn jarsDir
+
+  -- Set the SAW env var for the testing scripts to invoke saw with the JAR
+  -- list, again allowing ENV override.
+  let e3 = updEnvVars "SAW" (unwords [ "-j", "'" <> jars <> "'" ]) e1
+
+  return $ envVarAssocList e3
+
+
+-- ----------------------------------------------------------------------
+
+-- | Generate a HUnit test for each test, executed by running the
+-- test.sh file in that test directory.  The first argument is the set
+-- of environment variables to set when running the tests and the
+-- second is the list of disabled tests.
+genTests :: [(String,String)] -> [String] -> [String] -> [TestTree]
+genTests envvars disabled = map mkTest
+  where
+    preTest n = if takeFileName n `elem` disabled then ignoreTest else id
+    mkTest n = preTest n $ testCase (takeFileName n) $ do
+      let cmd = (shell "bash test.sh") { cwd = Just n, env = Just envvars }
+      (r,o,e) <- liftIO $ readCreateProcessWithExitCode cmd ""
+      if r == ExitSuccess
+        then return ()
+        else putStrLn o >> hPutStrLn stderr e
+      r @=? ExitSuccess
+
+
+-- | Several of the tests use definitions from the cryptol-specs
+-- repository, which should be present in deps/cryptol-specs.
+-- Verify the existence of that repository if any of the tools here
+-- need it.
+check_cryptol_specs :: String -> [String] -> [String] -> TestTree
+check_cryptol_specs testPath disabled tests = testCase "cryptol-specs Available" $
+  let need_cryptol_spec = any (\t -> let tp = (testPath </> t)
+                                     in tp `elem` tests && not (t `elem` disabled))
+                          [ "test0001", "test0002"
+                          , "test0006", "test0006_w4"
+                          , "test0035_aes_consistent"
+                          , "test_w4"
+                          , "test_examples"
+                          ]
+      cspec_dir = takeDirectory testPath </> "deps" </> "cryptol-specs"
+  in if need_cryptol_spec
+     then do have_cs <- liftIO $ doesDirectoryExist $ cspec_dir </> "Primitive"
+             unless (have_cs) $ liftIO $ do
+               hPutStrLn stderr "Tests require cryptol-specs as a checked-out subrepo:"
+               hPutStrLn stderr "  $ git submodule update --init deps/cryptol-specs"
+             assertBool "Missing cryptol-specs" have_cs
+     else return ()
+
+
+main :: IO ()
+main = do
+  let base = "intTests"
+  -- Run tests with VERBOSE=y environment variable for extra output.
+  verbose <- lookupEnv "VERBOSE" >>= \case
+    Just "y" -> return $ putStrLn
+    _ -> return $ const (return ())
+  found <- doesDirectoryExist base
+  unless found $ do
+    curwd <- getCurrentDirectory
+    hPutStrLn stderr $ "FAILURE: cannot find test directory " <> base <> " from " <> curwd
+    exitFailure
+  dset <- getDisabledTestList base
+  verbose $ "Disabled tests: " <> show dset
+  testdirs' <- getTestList base [] -- no filtering here; they will be ignoreTest'd by genTests
+  testdirs <- fromMaybe testdirs' .
+              (fmap (\et -> let path_ets = fmap (base </>) $ words et in
+                              filter (flip elem path_ets) testdirs')) <$>
+              lookupEnv "ENABLED_TESTS"
+  envVars <- testParams base verbose
+  verbose $ "ENV: " <> show envVars
+  defaultMain $
+    localOption (mkTimeout $ 500 * 1000 * 1000) $  -- 500 second timeout in usecs
+    testGroup "intTests" $
+    check_cryptol_specs base dset testdirs : (genTests envVars dset) testdirs
diff --git a/intTests/README b/intTests/README
deleted file mode 100644
index e596c00cd6..0000000000
--- a/intTests/README
+++ /dev/null
@@ -1,53 +0,0 @@
-===============================
-Integration tests for SAWScript
-===============================
-
-Running tests
-=============
-
-To run all default tests:
-    ./runtests.sh
-
-The default tests are those with directory names of the form "test*"
-which are not listed in the file defined by the environment variable
-"DISABLED_TESTS". The default value of "DISABLED_TESTS" is
-"disabled_tests.txt". Non-default tests can always be run manually, as
-in the next example.
-
-To run a subset of tests, provide the directory names you wish to run:
-    ./runtests.sh test0001 test0029
-
-Output from test runs will be placed in the logs/ directory.
-
-The "runtests.sh" script finds the generated executables
-(e.g. `saw`) using `stack path --local-install-root`. A different directory
-can be specified by defining the "BIN" environment variable.
-
-By default tests are run with a timeout of 5 minutes. The default
-timeout can be overridden by defining the timeout in seconds in the
-TEST_TIMEOUT environment variable. For example, to run the default
-tests with a timeout of 30 minutes:
-
-  (TEST_TIMEOUT=1800; ./runtests.sh)
-
-Creating tests
-==============
-
-A test is defined by a directory which contains a shell script called
-"test.sh"; the test succeeds when the shell script does. When run by
-"runtests.sh", these "test.sh" scripts are interpreted by "sh", which
-varies with platform -- in particular, it's not Bash on Debian based
-systems. So, keep your "test.sh" simple, or change how "runtests.sh"
-works.
-
-Tests generally consist of a SAW script that is expected to succeed
-together with the artifacts that are needed. The "runtests.sh" script
-defines environment variables "JAVA" and "SAW", pointing to the
-corresponding executables, and with appropriate Java classpaths
-included. It's a good idea to include a README in each test directory.
-
-If the test directory name starts with "test", and the directory name
-is not included in the file specified by the environment variable
-"DISABLED_TESTS", then the test is run by default. Only default tests
-are run on the build slaves. When disabling a test by default, explain
-why in that test's README.
diff --git a/intTests/README.md b/intTests/README.md
new file mode 100644
index 0000000000..79dcff99b3
--- /dev/null
+++ b/intTests/README.md
@@ -0,0 +1,46 @@
+Integration tests for SAWScript
+===============================
+
+Running tests
+-------------
+
+The integration tests are exposed as [cabal test suite](../saw-script.cabal)
+`integration_tests`. The default tests can be run with:
+
+```
+cabal test --enable-tests integration_tests
+```
+
+For each `test_*` directory that is not listed in the `DISABLED_TESTS`
+environment variable or the `disabled_tests.txt` if the environment variable
+isn't set, invoke the `test.sh` in that directory with some supporting
+environment variables set. The `test.sh` should complete with a return code of 0
+on no error or non-zero on error.
+
+If the `DISABLED_TESTS` environment variable is set, the `disabled_tests.txt`
+file is ignored. Both may specify tests separated by spaces and/or newlines, and
+the `#` character starts a comment to the end of the current line.
+
+The `ENABLED_TESTS` environment variable, if set, overrides the set of
+discovered tests to include only those in the `ENABLED_TESTS` list. This
+environment variable is commonly used during development to run specific tests
+(which `cabal test` does not easily support).
+
+Creating tests
+--------------
+
+A test is defined by a directory which contains a shell script called "test.sh";
+the test succeeds when the shell script does. When run as part of the suite,
+these "test.sh" scripts are interpreted by `bash`.
+
+Tests generally consist of a SAW script that is expected to succeed together
+with the artifacts that are needed. The test suite defines the environment
+variable "SAW", pointing to the corresponding executable, and with appropriate
+Java classpaths included. It's a good idea to include a README in each test
+directory.
+
+If the test directory name starts with "test", and the directory name is not
+included in the `disabled_tests.txt` file or `DISABLED_TESTS` environment
+variable, then the test is run by default. Only default tests are run on the
+build slaves. When disabling a test by default, explain why in that test's
+README.
diff --git a/intTests/runtests.sh b/intTests/runtests.sh
deleted file mode 100755
index 0ad0e4ec9c..0000000000
--- a/intTests/runtests.sh
+++ /dev/null
@@ -1,151 +0,0 @@
-#!/usr/bin/env bash
-
-################################################################
-# Setup environment.
-
-trap "finish" SIGINT
-
-finish() {
-  echo "tests passed: ${PASSED_TESTS} / ${NUM_TESTS}"
-  if [ "${PASSED_TESTS}" == "${NUM_TESTS}" ]; then
-    echo "all tests passed"
-    exit 0
-  else
-    if [ "${FAILED_TESTS}" != 0 ]; then
-      echo "${FAILED_TEST_DETAILS}"
-    fi
-    if [ -z "$DONE" ]; then
-      echo "interrupted: $i"
-    fi
-    exit 1
-  fi
-}
-
-if [ -z "$TESTBASE" ]; then
-  TESTBASE=$(pwd)
-  export TESTBASE
-fi
-
-if [ "${OS}" == "Windows_NT" ]; then
-  export CPSEP=";"
-  export DIRSEP="\\"
-else
-  export CPSEP=":"
-  export DIRSEP="/"
-fi
-
-# Build the class path. On Windows, Java requires Windows-style paths
-# here, even in Cygwin.
-CP=""
-# Add our bundled .jars to the class path.
-for i in "$TESTBASE"/jars/*.jar; do
-  if [ "$OS" == "Windows_NT" ]; then
-    i=$(cygpath -w "$i")
-  fi
-  if [ -z "$CP" ]; then
-    CP=$i
-  else
-    CP=$CP$CPSEP$i
-  fi
-done
-export CP
-
-# We need the 'eval's here to interpret the single quotes protecting
-# the spaces and semi-colons in the Windows class path.
-export SAW="eval saw -j '$CP'"
-
-# Figure out what tests to run
-if [[ -z "$*" ]]; then
-  if [ -z "$DISABLED_TESTS" ]; then
-    # File listing tests disabled by default.
-    DISABLED_TESTS=disabled_tests.txt
-  fi
-  # Collect tests not listed in the disabled tests.
-  TESTS=""
-  for t in test*; do
-    if ! grep -q "^$t\$" $DISABLED_TESTS; then
-      TESTS="$TESTS $t"
-    fi
-  done
-else
-  # Default disabled tests are ignored when specific tests are
-  # specified on the command line.
-  TESTS=$*
-fi
-
-if [ -z "${TEST_TIMEOUT}" ]; then
-  TEST_TIMEOUT=500
-fi
-
-if [ -z "${XML_FILE}" ]; then
-  XML_FILE="results.xml"
-fi
-XML_TEMP="${XML_FILE}.tmp"
-
-################################################################
-# Run tests.
-
-mkdir -p logs
-rm -f logs/*
-
-NUM_TESTS=$(echo "$TESTS" | wc -w)
-PASSED_TESTS=0
-FAILED_TESTS=0
-FAILED_TEST_DETAILS="failed:"
-export TIMEFORMAT="%R"
-TOTAL_TIME=0
-
-for i in $TESTS; do
-  # Some nasty bash hacking here to catpure the amount of time taken by the test
-  # See http://mywiki.wooledge.org/BashFAQ/032
-  START_TIME=$SECONDS
-  if [ "${OS}" == "Windows_NT" ]; then
-    # ulimit is useless on cygwin :-(  Use the 'timeout' utility instead
-    ( cd "$i" || exit 1; (/usr/bin/timeout -k 15 ${TEST_TIMEOUT} sh -vx test.sh > "../logs/$i.log" 2>&1) 2>&1 )
-    RES=$?
-  else
-    ( ulimit -t ${TEST_TIMEOUT}; cd "$i" || exit 1; (sh -vx test.sh > "../logs/$i.log" 2>&1) 2>&1 )
-    RES=$?
-  fi
-  END_TIME=$SECONDS
-  TEST_TIME=$((END_TIME - START_TIME))
-
-  if [ $((TEST_TIME >= TEST_TIMEOUT)) == 1 ]; then
-    TIMED_OUT=" TIMEOUT"
-  else
-    TIMED_OUT=""
-  fi
-
-  TOTAL_TIME=$((TOTAL_TIME + TEST_TIME))
-
-  if [ $RES == 0 ]; then
-    PASSED_TESTS=$(( PASSED_TESTS + 1 ))
-    echo "$i: OK (${TEST_TIME}s)"
-    echo "  <testcase name=\"${i}\" time=\"${TEST_TIME}\" />" >> ${XML_TEMP}
-  else
-    FAILED_TESTS=$(( FAILED_TESTS + 1 ))
-    echo "$i: FAIL (${TEST_TIME}s${TIMED_OUT})"
-    if [ -n "$LOUD" ]; then cat "logs/$i.log"; fi
-    FAILED_TEST_DETAILS+=" $i"
-    {
-      echo "  <testcase name=\"${i}\" time=\"${TEST_TIME}\"><failure><![CDATA["
-      sed -e 's/]]>/] ]>/' "logs/$i.log"
-      echo "]]></failure></testcase>"
-    } >> ${XML_TEMP}
-  fi
-done
-
-DONE=1
-
-echo "<?xml version='1.0'?>" > $XML_FILE
-{
-  echo "<testsuites errors=\"${FAILED_TESTS}\" tests=\"${NUM_TESTS}\" time=\"${TOTAL_TIME}\">"
-  echo " <testsuite name=\"SAWScript Integration Tests\">"
-  cat $XML_TEMP
-  echo " </testsuite>"
-  echo "</testsuites>"
-} >> $XML_FILE
-
-rm $XML_TEMP
-
-finish;
diff --git a/intTests/test_crucible_jvm/Makefile b/intTests/test_crucible_jvm/Makefile
index 332398c5a2..830af663d9 100644
--- a/intTests/test_crucible_jvm/Makefile
+++ b/intTests/test_crucible_jvm/Makefile
@@ -1,4 +1,5 @@
 SAW?=../../bin/saw
+JAVAC?=javac
 SAWS=$(wildcard *.saw)
 OUTS=$(SAWS:.saw=.out)
 
@@ -10,7 +11,7 @@ run: all ${OUTS}
 	clang -emit-llvm -c $< -o $@
 
 %.class: %.java
-	javac -g $<
+	${JAVAC} -g $<
 
 %.out: %.saw
 	${SAW} $< 2>&1 | tee $@
diff --git a/saw-remote-api/python/README.md b/saw-remote-api/python/README.md
index 2722590bcc..268403adb3 100644
--- a/saw-remote-api/python/README.md
+++ b/saw-remote-api/python/README.md
@@ -28,7 +28,7 @@ cd saw-remote-api/python
    E.g., here is how the docker image of the server might be used:
 ```
 $ docker run --name=saw-remote-api -d \
-  -v $PWD/tests/saw/test-files:/home/saw/tests/test-files \
+  -v $PWD/tests/saw/test-files:/home/saw/tests/saw/test-files \
   -p 8080:8080 \
   galoisinc/saw-remote-api:nightly
 $ export SAW_SERVER_URL="http://localhost:8080/"
diff --git a/saw-remote-api/src/SAWServer/CryptolExpression.hs b/saw-remote-api/src/SAWServer/CryptolExpression.hs
index 5af4d95c19..b52b8e5f57 100644
--- a/saw-remote-api/src/SAWServer/CryptolExpression.hs
+++ b/saw-remote-api/src/SAWServer/CryptolExpression.hs
@@ -6,8 +6,10 @@ module SAWServer.CryptolExpression
  ( getCryptolExpr
  , getTypedTerm
  , getTypedTermOfCExp
+ , CryptolModuleException(..)
  ) where
 
+import Control.Exception (Exception)
 import Control.Lens ( view )
 import Control.Monad.IO.Class ( MonadIO(liftIO) )
 import qualified Data.ByteString as B
@@ -15,7 +17,7 @@ import qualified Data.Map as Map
 import Data.Maybe (fromMaybe)
 
 import Cryptol.Eval (EvalOpts(..))
-import Cryptol.ModuleSystem (ModuleRes, ModuleInput(..))
+import Cryptol.ModuleSystem (ModuleError, ModuleInput(..), ModuleRes, ModuleWarning)
 import Cryptol.ModuleSystem.Base (genInferInput, getPrimMap, noPat, rename)
 import Cryptol.ModuleSystem.Env (ModuleEnv, meSolverConfig)
 import Cryptol.ModuleSystem.Interface (noIfaceParams)
@@ -108,3 +110,10 @@ runInferOutput out =
     InferFailed nm warns errs ->
       do typeCheckWarnings nm warns
          typeCheckingFailed nm errs
+
+data CryptolModuleException = CryptolModuleException
+  { cmeError    :: ModuleError
+  , cmeWarnings :: [ModuleWarning]
+  } deriving Show
+
+instance Exception CryptolModuleException
diff --git a/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs b/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs
index e3e20389fe..629a989b9c 100644
--- a/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs
+++ b/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs
@@ -13,6 +13,7 @@ module SAWServer.JVMCrucibleSetup
   , compileJVMContract
   ) where
 
+import Control.Exception (throw)
 import Control.Lens ( view )
 import Control.Monad.IO.Class ( MonadIO(liftIO) )
 import Control.Monad.State
@@ -66,7 +67,7 @@ import SAWServer.Data.Contract
                argumentVals, postVars, postConds, postAllocated, postPointsTos,
                returnVal) )
 import SAWServer.Data.SetupValue ()
-import SAWServer.CryptolExpression (getTypedTermOfCExp)
+import SAWServer.CryptolExpression (CryptolModuleException(..), getTypedTermOfCExp)
 import SAWServer.Exceptions ( notAtTopLevel )
 import SAWServer.OK ( OK, ok )
 import SAWServer.TopLevel ( tl )
@@ -178,24 +179,20 @@ interpretJVMSetup fileReader bic cenv0 ss = evalStateT (traverse_ go ss) (mempty
         Val x -> return x -- TODO add cases for the server values that
                           -- are not coming from the setup monad
                           -- (e.g. surrounding context)
-    getSetupVal (_, cenv) (CryptolExpr expr) = JVMSetupM $
-      do res <- liftIO $ getTypedTermOfCExp fileReader (biSharedContext bic) cenv expr
-         -- TODO: add warnings (snd res)
-         case fst res of
-           Right (t, _) -> return (MS.SetupTerm t)
-           Left err -> error $ "Cryptol error: " ++ show err -- TODO: report properly
+    getSetupVal env (CryptolExpr expr) =
+      do t <- getTypedTerm env expr
+         return (MS.SetupTerm t)
     getSetupVal _ _sv = error $ "unrecognized setup value" -- ++ show sv
 
     getTypedTerm ::
       (Map ServerName ServerSetupVal, CryptolEnv) ->
       P.Expr P.PName ->
       JVMSetupM TypedTerm
-    getTypedTerm (_, cenv) expr = JVMSetupM $
-      do res <- liftIO $ getTypedTermOfCExp fileReader (biSharedContext bic) cenv expr
-         -- TODO: add warnings (snd res)
-         case fst res of
-           Right (t, _) -> return t
-           Left err -> error $ "Cryptol error: " ++ show err -- TODO: report properly
+    getTypedTerm (_, cenv) expr = JVMSetupM $ liftIO $
+      do (res, warnings) <- getTypedTermOfCExp fileReader (biSharedContext bic) cenv expr
+         case res of
+           Right (t, _) -> return t -- TODO: Report warnings
+           Left err -> throw $ CryptolModuleException err warnings
 
     resolve env name =
        case Map.lookup name env of
diff --git a/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs b/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs
index 37ad666367..b66bb8ac83 100644
--- a/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs
+++ b/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs
@@ -18,6 +18,7 @@ module SAWServer.LLVMCrucibleSetup
   , compileLLVMContract
   ) where
 
+import Control.Exception (throw)
 import Control.Lens ( view )
 import Control.Monad.State
     ( evalStateT,
@@ -71,7 +72,7 @@ import SAWServer.Data.Contract
     ( PointsTo(..), Allocated(..), ContractVar(..), Contract(..) )
 import SAWServer.Data.LLVMType (JSONLLVMType, llvmType)
 import SAWServer.Data.SetupValue ()
-import SAWServer.CryptolExpression (getTypedTermOfCExp)
+import SAWServer.CryptolExpression (CryptolModuleException(..), getTypedTermOfCExp)
 import SAWServer.Exceptions ( notAtTopLevel, cantLoadLLVMModule )
 import SAWServer.OK ( OK, ok )
 import SAWServer.TrackFile ( trackFile )
@@ -181,23 +182,19 @@ interpretLLVMSetup fileReader bic cenv0 ss =
         Val x -> return x -- TODO add cases for the named server values that
                           -- are not coming from the setup monad
                           -- (e.g. surrounding context)
-    getSetupVal (_, cenv) (CryptolExpr expr) = LLVMCrucibleSetupM $
-      do res <- liftIO $ getTypedTermOfCExp fileReader (biSharedContext bic) cenv expr
-         -- TODO: add warnings (snd res)
-         case fst res of
-           Right (t, _) -> return (CMS.anySetupTerm t)
-           Left err -> error $ "Cryptol error: " ++ show err -- TODO: report properly
+    getSetupVal env (CryptolExpr expr) =
+      do t <- getTypedTerm env expr
+         return (CMS.anySetupTerm t)
 
     getTypedTerm ::
       (Map ServerName ServerSetupVal, CryptolEnv) ->
       P.Expr P.PName ->
       LLVMCrucibleSetupM TypedTerm
-    getTypedTerm (_, cenv) expr = LLVMCrucibleSetupM $
-      do res <- liftIO $ getTypedTermOfCExp fileReader (biSharedContext bic) cenv expr
-         -- TODO: add warnings (snd res)
-         case fst res of
-           Right (t, _) -> return t
-           Left err -> error $ "Cryptol error: " ++ show err -- TODO: report properly
+    getTypedTerm (_, cenv) expr = LLVMCrucibleSetupM $ liftIO $
+      do (res, warnings) <- getTypedTermOfCExp fileReader (biSharedContext bic) cenv expr
+         case res of
+           Right (t, _) -> return t -- TODO: report warnings
+           Left err -> throw $ CryptolModuleException err warnings
 
     resolve env name =
        case Map.lookup name env of
diff --git a/saw-remote-api/src/SAWServer/TopLevel.hs b/saw-remote-api/src/SAWServer/TopLevel.hs
index 8121edd6f7..4d314abd29 100644
--- a/saw-remote-api/src/SAWServer/TopLevel.hs
+++ b/saw-remote-api/src/SAWServer/TopLevel.hs
@@ -2,14 +2,17 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 module SAWServer.TopLevel (tl) where
 
-import Control.Exception ( try, SomeException )
+import Control.Exception ( try, SomeException(..) )
 import Control.Lens ( view, set )
 import Control.Monad.State ( MonadIO(liftIO) )
+import Data.Typeable (cast)
 
 import SAWScript.Value ( TopLevel, runTopLevel )
 
 import qualified Argo
+import CryptolServer.Exceptions (cryptolError)
 import SAWServer ( SAWState, sawTopLevelRO, sawTopLevelRW )
+import SAWServer.CryptolExpression (CryptolModuleException(..))
 import SAWServer.Exceptions ( verificationException )
 
 tl :: TopLevel a -> Argo.Command SAWState a
@@ -19,8 +22,11 @@ tl act =
          rw = view sawTopLevelRW st
      liftIO (try (runTopLevel act ro rw)) >>=
        \case
-         Left (e :: SomeException) ->
-           Argo.raise (verificationException e)
+         Left e@(SomeException e')
+           |  Just (CryptolModuleException err warnings) <- cast e'
+           -> Argo.raise (cryptolError err warnings)
+           |  otherwise
+           -> Argo.raise (verificationException e)
          Right (res, rw') ->
            do Argo.modifyState $ set sawTopLevelRW rw'
               return res
diff --git a/saw-script.cabal b/saw-script.cabal
index d64a5a1f0a..21d8b02bde 100644
--- a/saw-script.cabal
+++ b/saw-script.cabal
@@ -224,3 +224,23 @@ executable saw
   else
     build-depends: aig
     GHC-options: -O2 -Wall -Werror -fno-ignore-asserts -fno-spec-constr-count
+
+test-suite integration_tests
+  type: exitcode-stdio-1.0
+  hs-source-dirs: intTests
+
+  ghc-options: -Wall
+  default-language: Haskell2010
+
+  main-is: IntegrationTest.hs
+
+  build-depends: base
+               , directory
+               , filemanip
+               , filepath
+               , process
+               , tasty
+               , tasty-hunit
+               , tasty-expected-failure
+
+  build-tool-depends: saw-script:saw
diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs
index a08d69ba09..0b40944f0f 100644
--- a/src/SAWScript/Builtins.hs
+++ b/src/SAWScript/Builtins.hs
@@ -9,6 +9,7 @@ Stability   : provisional
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE DeriveDataTypeable #-}
 {-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE Rank2Types #-}
 {-# LANGUAGE ScopedTypeVariables #-}
@@ -32,16 +33,14 @@ import qualified Control.Exception as Ex
 import qualified Data.ByteString as StrictBS
 import qualified Data.ByteString.Lazy as BS
 import qualified Data.ByteString.Lazy.UTF8 as B
-import Data.Char (isSpace)
 import qualified Data.IntMap as IntMap
 import Data.List (isPrefixOf, isInfixOf)
 import qualified Data.Map as Map
 import Data.Set (Set)
 import qualified Data.Set as Set
-import Data.Maybe
 import Data.Time.Clock
 import Data.Typeable
-import Data.Text (Text)
+
 import qualified Data.Text as Text
 import System.Directory
 import qualified System.Environment
@@ -60,39 +59,28 @@ import Verifier.SAW.Grammar (parseSAWTerm)
 import Verifier.SAW.ExternalFormat
 import Verifier.SAW.FiniteValue
   ( FiniteType(..), readFiniteValue
-  , FirstOrderValue(..), asFiniteType
+  , FirstOrderValue(..)
   , toFirstOrderValue, scFirstOrderValue
   )
-import Verifier.SAW.Prelude
+import Verifier.SAW.SATQuery
 import Verifier.SAW.SCTypeCheck hiding (TypedTerm)
 import qualified Verifier.SAW.SCTypeCheck as TC (TypedTerm(..))
 import Verifier.SAW.SharedTerm
 import Verifier.SAW.TypedTerm
 import qualified Verifier.SAW.Simulator.Concrete as Concrete
 import Verifier.SAW.Prim (rethrowEvalError)
-import Verifier.SAW.Recognizer
 import Verifier.SAW.Rewriter
-import Verifier.SAW.Testing.Random (scRunTestsTFIO, scTestableType)
+import Verifier.SAW.Testing.Random (prepareSATQuery, runManyTests)
 import Verifier.SAW.TypedAST
 
 import SAWScript.Position
 
--- crucible-jvm
-import Lang.JVM.ProcessUtils
-
 -- cryptol-saw-core
 import qualified Verifier.SAW.CryptolEnv as CEnv
 
--- saw-core-aig
-import qualified Verifier.SAW.Simulator.BitBlast as BBSim
-
 -- saw-core-sbv
 import qualified Verifier.SAW.Simulator.SBV as SBVSim
 
--- saw-core-what4
-import qualified Verifier.SAW.Simulator.What4 as W4Sim
-import qualified Verifier.SAW.Simulator.What4.ReturnTrip as W4Sim
-
 -- sbv
 import qualified Data.SBV.Dynamic as SBV
 
@@ -114,7 +102,6 @@ import qualified Cryptol.Eval.Value as C (fromVBit, fromVWord)
 import qualified Cryptol.Eval.Concrete as C (Concrete(..), bvVal)
 import qualified Cryptol.Utils.Ident as C (mkIdent, packModName)
 import qualified Cryptol.Utils.RecordMap as C (recordFromFields)
-import Cryptol.Utils.PP (pretty)
 
 import qualified SAWScript.SBVParser as SBV
 import SAWScript.ImportAIG
@@ -126,7 +113,7 @@ import SAWScript.TopLevel
 import qualified SAWScript.Value as SV
 import SAWScript.Value (ProofScript, printOutLnTop, AIGNetwork)
 
-import SAWScript.Prover.Util(checkBooleanSchema,liftCexBB)
+import SAWScript.Prover.Util(checkBooleanSchema)
 import SAWScript.Prover.SolverStats
 import qualified SAWScript.Prover.SBV as Prover
 import qualified SAWScript.Prover.RME as Prover
@@ -135,7 +122,6 @@ import qualified SAWScript.Prover.What4 as Prover
 import qualified SAWScript.Prover.Exporter as Prover
 import qualified SAWScript.Prover.MRSolver as Prover
 import SAWScript.VerificationSummary
-import SAWScript.Crucible.Common as Common
 
 showPrim :: SV.Value -> TopLevel String
 showPrim v = do
@@ -341,81 +327,47 @@ readCore path = do
   sc <- getSharedContext
   io (mkTypedTerm sc =<< scReadExternal sc =<< readFile path)
 
-withFirstGoal :: (ProofGoal -> TopLevel (a, SolverStats, Maybe ProofGoal)) -> ProofScript a
-withFirstGoal f =
-  StateT $ \(ProofState goals concl stats timeout) ->
-  case goals of
-    [] -> fail "ProofScript failed: no subgoal"
-    g : gs -> do
-      (x, stats', mg') <- f g
-      case mg' of
-        Nothing -> return (x, ProofState gs concl (stats <> stats') timeout)
-        Just g' -> return (x, ProofState (g' : gs) concl (stats <> stats') timeout)
-
 quickcheckGoal :: SharedContext -> Integer -> ProofScript SV.SatResult
 quickcheckGoal sc n = do
   opts <- Control.Monad.State.lift getOptions
-  withFirstGoal $ \goal -> io $ do
+  withFirstGoal $ tacticSolve $ \goal -> io $ do
     printOutLn opts Warn $ "WARNING: using quickcheck to prove goal..."
     hFlush stdout
-    tm0 <- propToPredicate sc (goalProp goal)
-    tm <- scAbstractExts sc (getAllExts tm0) tm0
-    ty <- scTypeOf sc tm
-    maybeInputs <- scTestableType sc ty
-    let stats = solverStats "quickcheck" (scSharedSize tm)
-    case maybeInputs of
-      Just inputs -> do
-        result <- scRunTestsTFIO sc n tm inputs
-        case result of
-          Nothing -> do
-            printOutLn opts Info $ "checked " ++ show n ++ " cases."
-            return (SV.Unsat stats, stats, Nothing)
-          -- TODO: use reasonable names here
-          Just cex -> return (SV.SatMulti stats (zip (repeat "_") (map toFirstOrderValue cex)), stats, Just goal)
-      Nothing -> fail $ "quickcheck:\n" ++
-        "term has non-testable type:\n" ++
-        showTerm ty ++ ", for term: " ++ showTerm tm
+    satq <- propToSATQuery sc mempty (goalProp goal)
+    testGen <- prepareSATQuery sc satq
+    let stats = solverStats "quickcheck" (propSize (goalProp goal))
+    runManyTests testGen n >>= \case
+       Nothing ->
+         do printOutLn opts Info $ "checked " ++ show n ++ " cases."
+            return (SV.Unsat stats, stats, Just (QuickcheckEvidence n (goalProp goal)))
+       Just cex ->
+         let cex' = [ (Text.unpack (toShortName (ecName ec)), v) | (ec,v) <- cex ]
+          in return (SV.SatMulti stats cex', stats, Nothing)
 
 assumeValid :: ProofScript SV.ProofResult
 assumeValid =
-  withFirstGoal $ \goal ->
+  withFirstGoal $ tacticSolve $ \goal ->
   do printOutLnTop Warn $ "WARNING: assuming goal " ++ goalName goal ++ " is valid"
-     let stats = solverStats "ADMITTED" (scSharedSize (unProp (goalProp goal)))
-     return (SV.Valid stats, stats, Nothing)
+     let stats = solverStats "ADMITTED" (propSize (goalProp goal))
+     return (SV.Valid stats, stats, Just (Admitted (goalProp goal)))
 
 assumeUnsat :: ProofScript SV.SatResult
 assumeUnsat =
-  withFirstGoal $ \goal ->
+  withFirstGoal $ tacticSolve $ \goal ->
   do printOutLnTop Warn $ "WARNING: assuming goal " ++ goalName goal ++ " is unsat"
-     let stats = solverStats "ADMITTED" (scSharedSize (unProp (goalProp goal)))
-     return (SV.Unsat stats, stats, Nothing)
+     let stats = solverStats "ADMITTED" (propSize (goalProp goal))
+     return (SV.Unsat stats, stats, Just (Admitted (goalProp goal)))
 
 trivial :: ProofScript SV.SatResult
 trivial =
-  withFirstGoal $ \goal ->
-  do checkTrue (unProp (goalProp goal))
-     return (SV.Unsat mempty, mempty, Nothing)
-  where
-    checkTrue :: Term -> TopLevel ()
-    checkTrue (asPiList -> (_, asEqTrue -> Just (asBool -> Just True))) = return ()
-    checkTrue _ = fail "trivial: not a trivial goal"
+  do sc <- lift getSharedContext
+     withFirstGoal (tacticTrivial sc)
+     pure (SV.Unsat mempty)
 
 split_goal :: ProofScript ()
 split_goal =
-  StateT $ \(ProofState goals concl stats timeout) ->
-  case goals of
-    [] -> fail "ProofScript failed: no subgoal"
-    (ProofGoal num ty name (Prop prop)) : gs ->
-      let (vars, body) = asPiList prop in
-      case (isGlobalDef "Prelude.and" <@> return <@> return) =<< asEqTrue body of
-        Nothing -> fail "split_goal: goal not of form 'Prelude.and _ _'"
-        Just (_ :*: p1 :*: p2) ->
-          do sc <- getSharedContext
-             t1 <- io $ scPiList sc vars =<< scEqTrue sc p1
-             t2 <- io $ scPiList sc vars =<< scEqTrue sc p2
-             let g1 = ProofGoal num (ty ++ ".left") name (Prop t1)
-             let g2 = ProofGoal num (ty ++ ".right") name (Prop t2)
-             return ((), ProofState (g1 : g2 : gs) concl stats timeout)
+  do sc <- lift getSharedContext
+     withFirstGoal (tacticSplit sc)
 
 getTopLevelPPOpts :: TopLevel PPOpts
 getTopLevelPPOpts = do
@@ -441,41 +393,40 @@ print_term_depth d t =
 
 print_goal :: ProofScript ()
 print_goal =
-  withFirstGoal $ \goal ->
+  withFirstGoal $ tacticId $ \goal ->
   do opts <- getTopLevelPPOpts
      sc <- getSharedContext
-     output <- liftIO $ scShowTerm sc opts (unProp (goalProp goal))
+     output <- liftIO (scShowTerm sc opts =<< propToTerm sc (goalProp goal))
      printOutLnTop Info ("Goal " ++ goalName goal ++ " (goal number " ++ (show $ goalNum goal) ++ "):")
      printOutLnTop Info output
-     return ((), mempty, Just goal)
 
 print_goal_depth :: Int -> ProofScript ()
 print_goal_depth n =
-  withFirstGoal $ \goal ->
+  withFirstGoal $ tacticId $ \goal ->
   do opts <- getTopLevelPPOpts
      sc <- getSharedContext
      let opts' = opts { ppMaxDepth = Just n }
-     output <- liftIO $ scShowTerm sc opts' (unProp (goalProp goal))
+     output <- liftIO (scShowTerm sc opts' =<< propToTerm sc (goalProp goal))
      printOutLnTop Info ("Goal " ++ goalName goal ++ ":")
      printOutLnTop Info output
-     return ((), mempty, Just goal)
 
 printGoalConsts :: ProofScript ()
 printGoalConsts =
-  withFirstGoal $ \goal ->
-  do mapM_ (printOutLnTop Info) $
+  withFirstGoal $ tacticId $ \goal ->
+  do sc <- getSharedContext
+     tm <- io (propToTerm sc (goalProp goal))
+     mapM_ (printOutLnTop Info) $
        [ show nm
-       | (_,(nm,_,_)) <- Map.toList (getConstantSet (unProp (goalProp goal)))
+       | (_,(nm,_,_)) <- Map.toList (getConstantSet tm)
        ]
-     return ((), mempty, Just goal)
 
 printGoalSize :: ProofScript ()
 printGoalSize =
-  withFirstGoal $ \goal ->
-  do let Prop t = goalProp goal
+  withFirstGoal $ tacticId $ \goal ->
+  do sc <- getSharedContext
+     t  <- io (propToTerm sc (goalProp goal))
      printOutLnTop Info $ "Goal shared size: " ++ show (scSharedSize t)
      printOutLnTop Info $ "Goal unshared size: " ++ show (scTreeSize t)
-     return ((), mempty, Just goal)
 
 resolveNames :: [String] -> TopLevel (Set VarIndex)
 resolveNames nms =
@@ -517,130 +468,53 @@ resolveName sc nm =
 
 unfoldGoal :: [String] -> ProofScript ()
 unfoldGoal unints =
-  withFirstGoal $ \goal ->
+  withFirstGoal $ tacticChange $ \goal ->
   do sc <- getSharedContext
-     unints' <- mapM (resolveName sc) unints
-     let Prop trm = goalProp goal
-     trm' <- io $ scUnfoldConstants sc unints' trm
-     return ((), mempty, Just (goal { goalProp = Prop trm' }))
+     unints' <- resolveNames unints
+     prop' <- io (unfoldProp sc unints' (goalProp goal))
+     return (prop', UnfoldEvidence unints')
 
 simplifyGoal :: Simpset -> ProofScript ()
 simplifyGoal ss =
-  withFirstGoal $ \goal ->
+  withFirstGoal $ tacticChange $ \goal ->
   do sc <- getSharedContext
-     let Prop trm = goalProp goal
-     trm' <- io $ rewriteSharedTerm sc ss trm
-     return ((), mempty, Just (goal { goalProp = Prop trm' }))
+     prop' <- io (simplifyProp sc ss (goalProp goal))
+     return (prop', RewriteEvidence ss)
 
 goal_eval :: [String] -> ProofScript ()
 goal_eval unints =
-  withFirstGoal $ \goal ->
+  withFirstGoal $ tacticChange $ \goal ->
   do sc <- getSharedContext
      unintSet <- resolveNames unints
-
-     -- replace all pi-bound quantified variables with new free variables
-     let (args, body) = asPiList (unProp (goalProp goal))
-     body' <-
-       case asEqTrue body of
-         Just t -> pure t
-         Nothing -> fail "goal_eval: expected EqTrue"
-     ecs <- liftIO $ traverse (\(nm, ty) -> scFreshEC sc (Text.unpack nm) ty) args
-     vars <- liftIO $ traverse (scExtCns sc) ecs
-     t0 <- liftIO $ instantiateVarList sc 0 (reverse vars) body'
-
-     sym <- liftIO $ Common.newSAWCoreBackend sc
-     st <- liftIO $ Common.sawCoreState sym
-     (_names, (_mlabels, p)) <- liftIO $ W4Sim.w4Eval sym st sc Map.empty unintSet t0
-     t1 <- liftIO $ W4Sim.toSC sym st p
-
-     t2 <- liftIO $ scEqTrue sc t1
-     -- turn the free variables we generated back into pi-bound variables
-     t3 <- liftIO $ scGeneralizeExts sc ecs t2
-     return ((), mempty, Just (goal { goalProp = Prop t3 }))
+     prop' <- io (evalProp sc unintSet (goalProp goal))
+     return (prop', EvalEvidence unintSet)
 
 beta_reduce_goal :: ProofScript ()
 beta_reduce_goal =
-  withFirstGoal $ \goal ->
+  withFirstGoal $ tacticChange $ \goal ->
   do sc <- getSharedContext
-     let Prop trm = goalProp goal
-     trm' <- io $ betaNormalize sc trm
-     return ((), mempty, Just (goal { goalProp = Prop trm' }))
+     prop' <- io (betaReduceProp sc (goalProp goal))
+     return (prop', id)
 
 goal_apply :: Theorem -> ProofScript ()
-goal_apply (Theorem (Prop rule) _stats) =
-  StateT $ \(ProofState goals concl stats timeout) ->
-  case goals of
-    [] -> fail "goal_apply failed: no subgoal"
-    goal : goals' ->
-      do sc <- getSharedContext
-         let applyFirst [] = fail "goal_apply failed: no match"
-             applyFirst ((ruleArgs, ruleConcl) : rest) =
-               do result <- io $ scMatch sc ruleConcl (unProp (goalProp goal))
-                  case result of
-                    Nothing -> applyFirst rest
-                    Just inst ->
-                      do let inst' = [ Map.lookup i inst | i <- take (length ruleArgs) [0..] ]
-                         dummy <- io $ scUnitType sc
-                         let mkNewGoals (Nothing : mts) ((_, prop) : args) =
-                               do c0 <- instantiateVarList sc 0 (map (fromMaybe dummy) mts) prop
-                                  cs <- mkNewGoals mts args
-                                  return (Prop c0 : cs)
-                             mkNewGoals (Just _ : mts) (_ : args) =
-                               mkNewGoals mts args
-                             mkNewGoals _ _ = return []
-                         newgoalterms <- io $ mkNewGoals inst' (reverse ruleArgs)
-                         let newgoals = reverse [ goal { goalProp = t } | t <- newgoalterms ]
-                         return ((), ProofState (newgoals ++ goals') concl stats timeout)
-         applyFirst (asPiLists rule)
-  where
-    asPiLists :: Term -> [([(Text, Term)], Term)]
-    asPiLists t =
-      case asPi t of
-        Nothing -> [([], t)]
-        Just (nm, tp, body) ->
-          [ ((nm, tp) : args, concl) | (args, concl) <- asPiLists body ] ++ [([], t)]
+goal_apply thm =
+  do sc <- lift getSharedContext
+     withFirstGoal (tacticApply sc thm)
 
 goal_assume :: ProofScript Theorem
 goal_assume =
-  StateT $ \(ProofState goals concl stats timeout) ->
-  case goals of
-    [] -> fail "goal_assume failed: no subgoal"
-    goal : goals' ->
-      case asPi (unProp (goalProp goal)) of
-        Nothing -> fail "goal_assume failed: not a pi type"
-        Just (_nm, tp, body)
-          | looseVars body /= emptyBitSet -> fail "goal_assume failed: dependent pi type"
-          | otherwise ->
-            let goal' = goal { goalProp = Prop body } in
-            return (Theorem (Prop tp) mempty, ProofState (goal' : goals') concl stats timeout)
+  do sc <- lift getSharedContext
+     withFirstGoal (tacticAssume sc)
 
 goal_intro :: String -> ProofScript TypedTerm
 goal_intro s =
-  StateT $ \(ProofState goals concl stats timeout) ->
-  case goals of
-    [] -> fail "goal_intro failed: no subgoal"
-    goal : goals' ->
-      case asPi (unProp (goalProp goal)) of
-        Nothing -> fail "goal_intro failed: not a pi type"
-        Just (nm, tp, body) ->
-          do let name = if null s then Text.unpack nm else s
-             sc <- SV.getSharedContext
-             x <- io $ scFreshGlobal sc name tp
-             tt <- io $ mkTypedTerm sc x
-             body' <- io $ instantiateVar sc 0 x body
-             let goal' = goal { goalProp = Prop body' }
-             return (tt, ProofState (goal' : goals') concl stats timeout)
+  do sc <- lift getSharedContext
+     withFirstGoal (tacticIntro sc s)
 
 goal_insert :: Theorem -> ProofScript ()
-goal_insert (Theorem (Prop t) _stats) =
-  StateT $ \(ProofState goals concl stats timeout) ->
-  case goals of
-    [] -> fail "goal_insert failed: no subgoal"
-    goal : goals' ->
-      do sc <- SV.getSharedContext
-         body' <- io $ scFun sc t (unProp (goalProp goal))
-         let goal' = goal { goalProp = Prop body' }
-         return ((), ProofState (goal' : goals') concl stats timeout)
+goal_insert thm =
+  do sc <- lift getSharedContext
+     withFirstGoal (tacticCut sc thm)
 
 goal_num_when :: Int -> ProofScript () -> ProofScript ()
 goal_num_when n script =
@@ -669,64 +543,15 @@ proveABC = do
   SV.AIGProxy proxy <- lift SV.getProxy
   wrapProver (Prover.proveABC proxy)
 
-parseDimacsSolution :: [Int]    -- ^ The list of CNF variables to return
-                    -> [String] -- ^ The value lines from the solver
-                    -> [Bool]
-parseDimacsSolution vars ls = map lkup vars
-  where
-    vs :: [Int]
-    vs = concatMap (filter (/= 0) . mapMaybe readMaybe . tail . words) ls
-    varToPair n | n < 0 = (-n, False)
-                | otherwise = (n, True)
-    assgnMap = Map.fromList (map varToPair vs)
-    lkup v = Map.findWithDefault False v assgnMap
-
 satExternal :: Bool -> String -> [String] -> ProofScript SV.SatResult
-satExternal doCNF execName args = withFirstGoal $ \g -> do
-  sc <- SV.getSharedContext
-  SV.AIGProxy proxy <- SV.getProxy
-  io $ do
-  t <- propToPredicate sc (goalProp g)
-  let cnfName = goalType g ++ show (goalNum g) ++ ".cnf"
-  (path, fh) <- openTempFile "." cnfName
-  hClose fh -- Yuck. TODO: allow writeCNF et al. to work on handles.
-  let args' = map replaceFileName args
-      replaceFileName "%f" = path
-      replaceFileName a = a
-  BBSim.withBitBlastedPred proxy sc mempty t $ \be l0 shapes -> do
-  -- negate formula to turn it into an existentially-quantified SAT query
-  let l = AIG.not l0
-  variables <- (if doCNF then AIG.writeCNF else writeAIGWithMapping) be l path
-  (_ec, out, err) <- readProcessWithExitCode execName args' ""
-  removeFile path
-  unless (null err) $
-    print $ unlines ["Standard error from SAT solver:", err]
-  let ls = lines out
-      sls = filter ("s " `isPrefixOf`) ls
-      vls = filter ("v " `isPrefixOf`) ls
-  ft <- Prop <$> (scEqTrue sc =<< scApplyPrelude_False sc)
-  let stats = solverStats ("external SAT:" ++ execName) (scSharedSize t)
-  case (sls, vls) of
-    (["s SATISFIABLE"], _) -> do
-      let bs = parseDimacsSolution variables vls
-      let r = liftCexBB (map snd shapes) bs
-          argNames = map fst shapes
-      case r of
-        Left msg -> fail $ "Can't parse counterexample: " ++ msg
-        Right vs
-          | length argNames == length vs -> do
-            let r' = SV.SatMulti stats (zip argNames (map toFirstOrderValue vs))
-            return (r', stats, Just (g { goalProp = ft }))
-          | otherwise -> fail $ unwords ["external SAT results do not match expected arguments", show argNames, show vs]
-    (["s UNSATISFIABLE"], []) ->
-      return (SV.Unsat stats, stats, Nothing)
-    _ -> fail $ "Unexpected result from SAT solver:\n" ++ out
-
-writeAIGWithMapping :: AIG.IsAIG l g => g s -> l s -> FilePath -> IO [Int]
-writeAIGWithMapping be l path = do
-  nins <- AIG.inputCount be
-  AIG.writeAiger path (AIG.Network be [l])
-  return [1..nins]
+satExternal doCNF execName args =
+  withFirstGoal $ tacticSolve $ \g ->
+    do SV.AIGProxy proxy <- SV.getProxy
+       sc <- SV.getSharedContext
+       (mb, stats) <- Prover.abcSatExternal proxy sc doCNF execName args g
+       case mb of
+         Nothing -> return (SV.Unsat stats, stats, Just (SolverEvidence stats (goalProp g)))
+         Just a  -> return (SV.SatMulti stats a, stats, Nothing)
 
 writeAIGPrim :: FilePath -> Term -> TopLevel ()
 writeAIGPrim f t = do
@@ -774,17 +599,12 @@ applyProverToGoal :: (SharedContext
                       -> Prop -> IO (Maybe [(String, FirstOrderValue)], SolverStats))
                      -> SharedContext
                      -> ProofGoal
-                     -> TopLevel (SV.SatResult, SolverStats, Maybe ProofGoal)
+                     -> TopLevel (SV.SatResult, SolverStats, Maybe Evidence)
 applyProverToGoal f sc g = do
   (mb, stats) <- io $ f sc (goalProp g)
-
-  let nope r = do ft <- io $ scEqTrue sc =<< scApplyPrelude_False sc
-                  return (r, stats, Just g { goalProp = Prop ft })
-
   case mb of
-    Nothing -> return (SV.Unsat stats, stats, Nothing)
-    Just a  -> nope (SV.SatMulti stats a)
-
+    Nothing -> return (SV.Unsat stats, stats, Just (SolverEvidence stats (goalProp g)))
+    Just a  -> return (SV.SatMulti stats a, stats, Nothing)
 
 
 wrapProver ::
@@ -793,8 +613,7 @@ wrapProver ::
   ProofScript SV.SatResult
 wrapProver f = do
   sc <- lift $ SV.getSharedContext
-  withFirstGoal (applyProverToGoal f sc)
-
+  withFirstGoal $ tacticSolve $ applyProverToGoal f sc
 
 wrapW4Prover ::
   ( Set VarIndex -> SharedContext -> Bool ->
@@ -817,7 +636,7 @@ wrapW4ProveExporter f unints path ext = do
   hashConsing <- lift $ gets SV.rwWhat4HashConsing
   sc <- lift $ SV.getSharedContext
   unintSet <- lift $ resolveNames unints
-  withFirstGoal $ \g -> do
+  withFirstGoal $ tacticSolve $ \g -> do
     let file = path ++ "." ++ goalType g ++ show (goalNum g) ++ ext
     applyProverToGoal (\s -> f unintSet s hashConsing file) sc g
 
@@ -896,110 +715,67 @@ offline_w4_unint_yices :: [String] -> String -> ProofScript SV.SatResult
 offline_w4_unint_yices unints path =
      wrapW4ProveExporter Prover.proveExportWhat4_yices unints path ".smt2"
 
-proveWithExporter ::
-  (SharedContext -> FilePath -> Prop -> TopLevel ()) ->
+proveWithSATExporter ::
+  (SharedContext -> FilePath -> SATQuery -> TopLevel a) ->
+  Set VarIndex ->
+  String ->
+  String ->
+  String ->
+  ProofScript SV.SatResult
+proveWithSATExporter exporter unintSet path sep ext =
+  withFirstGoal $ tacticSolve $ \g ->
+  do let file = path ++ sep ++ goalType g ++ show (goalNum g) ++ ext
+     stats <- Prover.proveWithSATExporter exporter unintSet file (goalProp g)
+     return (SV.Unsat stats, stats, Just (SolverEvidence stats (goalProp g)))
+
+proveWithPropExporter ::
+  (SharedContext -> FilePath -> Prop -> TopLevel a) ->
+  String ->
   String ->
   String ->
   ProofScript SV.SatResult
-proveWithExporter exporter path ext =
-  withFirstGoal $ \g ->
-  do let file = path ++ "." ++ goalType g ++ show (goalNum g) ++ ext
-     stats <- Prover.proveWithExporter exporter file (goalProp g)
-     return (SV.Unsat stats, stats, Nothing)
+proveWithPropExporter exporter path sep ext =
+  withFirstGoal $ tacticSolve $ \g ->
+  do let file = path ++ sep ++ goalType g ++ show (goalNum g) ++ ext
+     stats <- Prover.proveWithPropExporter exporter file (goalProp g)
+     return (SV.Unsat stats, stats, Just (SolverEvidence stats (goalProp g)))
 
 offline_aig :: FilePath -> ProofScript SV.SatResult
 offline_aig path = do
   SV.AIGProxy proxy <- lift $ SV.getProxy
-  proveWithExporter (Prover.adaptExporter (Prover.writeAIG proxy)) path ".aig"
+  proveWithSATExporter (Prover.writeAIG_SAT proxy) mempty path "." ".aig"
 
 offline_cnf :: FilePath -> ProofScript SV.SatResult
 offline_cnf path = do
   SV.AIGProxy proxy <- lift $ SV.getProxy
-  proveWithExporter (Prover.adaptExporter (Prover.writeCNF proxy)) path ".cnf"
+  proveWithSATExporter (Prover.writeCNF proxy) mempty path "." ".cnf"
 
 offline_coq :: FilePath -> ProofScript SV.SatResult
-offline_coq path = proveWithExporter (const (Prover.writeCoqProp "goal" [] [])) path ".v"
+offline_coq path = proveWithPropExporter (const (Prover.writeCoqProp "goal" [] [])) path "_" ".v"
 
 offline_extcore :: FilePath -> ProofScript SV.SatResult
-offline_extcore path = proveWithExporter (const Prover.writeCoreProp) path ".extcore"
+offline_extcore path = proveWithPropExporter (const Prover.writeCoreProp) path "." ".extcore"
 
 offline_smtlib2 :: FilePath -> ProofScript SV.SatResult
-offline_smtlib2 path = proveWithExporter Prover.writeSMTLib2 path ".smt2"
+offline_smtlib2 path = proveWithSATExporter Prover.writeSMTLib2 mempty path "." ".smt2"
 
 w4_offline_smtlib2 :: FilePath -> ProofScript SV.SatResult
-w4_offline_smtlib2 path = proveWithExporter Prover.writeSMTLib2What4 path ".smt2"
+w4_offline_smtlib2 path = proveWithSATExporter Prover.writeSMTLib2What4 mempty path "." ".smt2"
 
 offline_unint_smtlib2 :: [String] -> FilePath -> ProofScript SV.SatResult
 offline_unint_smtlib2 unints path =
   do unintSet <- lift $ resolveNames unints
-     proveWithExporter (Prover.writeUnintSMTLib2 unintSet) path ".smt2"
+     proveWithSATExporter Prover.writeSMTLib2 unintSet path "." ".smt2"
 
 offline_verilog :: FilePath -> ProofScript SV.SatResult
 offline_verilog path =
-  proveWithExporter (Prover.adaptExporter Prover.write_verilog) path ".v"
-
-parseAigerCex :: String -> IO [Bool]
-parseAigerCex text =
-  case lines text of
-    [_, cex] ->
-      case words cex of
-        [bits, _] -> mapM bitToBool bits
-        _ -> fail $ "invalid counterexample line: " ++ cex
-    _ -> fail $ "invalid counterexample text: " ++ text
-  where
-    bitToBool '0' = return False
-    bitToBool '1' = return True
-    bitToBool c   = fail ("invalid bit: " ++ [c])
+  proveWithSATExporter Prover.writeVerilogSAT mempty path "." ".v"
 
 w4_abc_verilog :: ProofScript SV.SatResult
-w4_abc_verilog = wrapW4Prover w4AbcVerilog []
-
-w4AbcVerilog ::
-  Set VarIndex ->
-  SharedContext ->
-  Bool ->
-  Prop ->
-  IO (Maybe [(String, FirstOrderValue)], SolverStats)
-w4AbcVerilog _unints sc _hashcons g =
-       -- Create temporary files
-    do let tpl = "abc_verilog.v"
-           tplCex = "abc_verilog.cex"
-       tmp <- emptySystemTempFile tpl
-       tmpCex <- emptySystemTempFile tplCex
-
-       -- Get goal into the right form
-       let (goalArgs, concl) = asPiList (unProp g)
-       p <- case asEqTrue concl of
-              Just p -> return p
-              Nothing -> fail "adaptExporter: expected EqTrue"
-       t <- scLambdaList sc goalArgs =<< scNot sc p
-       Prover.writeVerilog sc tmp t
-
-       -- Run ABC and remove temporaries
-       let execName = "abc"
-           args = ["-q", "%read " ++ tmp ++"; %blast; &sweep -C 5000; &syn4; &cec -m; write_aiger_cex " ++ tmpCex]
-       (_out, _err) <- readProcessExitIfFailure execName args
-       cexText <- readFile tmpCex
-       removeFile tmp
-       removeFile tmpCex
-
-       -- Parse and report results
-       let stats = solverStats "abc_verilog" (scSharedSize (unProp g))
-       res <- if all isSpace cexText
-              then return Nothing
-              else do bits <- reverse <$> parseAigerCex cexText
-                      let goalArgs' = reverse goalArgs
-                          argTys = map snd goalArgs'
-                          argNms = map (Text.unpack . fst) goalArgs'
-                      finiteArgTys <- traverse (asFiniteType sc) argTys
-                      case liftCexBB finiteArgTys bits of
-                        Left parseErr -> fail parseErr
-                        Right vs -> return $ Just model
-                          where model = zip argNms (map toFirstOrderValue vs)
-       return (res, stats)
+w4_abc_verilog = wrapW4Prover Prover.w4AbcVerilog []
 
 set_timeout :: Integer -> ProofScript ()
-set_timeout to = modify (\ps -> ps { psTimeout = Just to })
+set_timeout to = modify (setProofTimeout to)
 
 -- | Translate a @Term@ representing a theorem for input to the
 -- given validity-checking script and attempt to prove it.
@@ -1008,21 +784,24 @@ provePrim :: ProofScript SV.SatResult
 provePrim script t = do
   io $ checkBooleanSchema (ttSchema t)
   sc <- getSharedContext
-  goal <- io $ makeProofGoal sc Universal 0 "prove" "prove" (ttTerm t)
+  prop <- io $ predicateToProp sc Universal (ttTerm t)
+  let goal = ProofGoal 0 "prove" "prove" prop
   (r, pstate) <- runStateT script (startProof goal)
-  case finishProof pstate of
-    (_stats, Just _)  -> return ()
-    (_stats, Nothing) -> printOutLnTop Info $ "prove: " ++ show (length (psGoals pstate)) ++ " unsolved subgoal(s)"
+  io (finishProof sc pstate) >>= \case
+    (_stats, Just _) -> return ()
+    (_stats, Nothing) ->
+      printOutLnTop Info $ "prove: " ++ show (length (psGoals pstate)) ++ " unsolved subgoal(s)"
   return (SV.flipSatResult r)
 
 provePrintPrim :: ProofScript SV.SatResult
                -> TypedTerm -> TopLevel Theorem
 provePrintPrim script t = do
   sc <- getSharedContext
-  goal <- io $ makeProofGoal sc Universal 0 "prove" "prove" (ttTerm t)
+  prop <- io $ predicateToProp sc Universal (ttTerm t)
+  let goal = ProofGoal 0 "prove" "prove" prop
   (r, pstate) <- runStateT script (startProof goal)
   opts <- rwPPOpts <$> getTopLevelRW
-  case finishProof pstate of
+  io (finishProof sc pstate) >>= \case
     (_,Just thm) -> do
       printOutLnTop Debug $ "Valid: " ++ show (ppTerm (SV.sawPPOpts opts) $ ttTerm t)
       SV.returnProof thm
@@ -1034,7 +813,8 @@ satPrim :: ProofScript SV.SatResult -> TypedTerm
 satPrim script t =
   do io $ checkBooleanSchema (ttSchema t)
      sc <- getSharedContext
-     goal <- io $ makeProofGoal sc Existential 0 "sat" "sat" (ttTerm t)
+     prop <- io $ predicateToProp sc Existential (ttTerm t)
+     let goal = ProofGoal 0 "sat" "sat" prop
      evalStateT script (startProof goal)
 
 satPrintPrim :: ProofScript SV.SatResult
@@ -1047,21 +827,18 @@ satPrintPrim script t = do
 -- | Quick check (random test) a term and print the result. The
 -- 'Integer' parameter is the number of random tests to run.
 quickCheckPrintPrim :: Options -> SharedContext -> Integer -> TypedTerm -> IO ()
-quickCheckPrintPrim opts sc numTests tt = do
-  let tm = ttTerm tt
-  ty <- scTypeOf sc tm
-  maybeInputs <- scTestableType sc ty
-  case maybeInputs of
-    Just inputs -> do
-      result <- scRunTestsTFIO sc numTests tm inputs
-      case result of
+quickCheckPrintPrim opts sc numTests tt =
+  do let tm = ttTerm tt
+     prop <- predicateToProp sc Universal tm
+     satq <- propToSATQuery sc mempty prop
+     testGen <- prepareSATQuery sc satq
+     runManyTests testGen numTests >>= \case
         Nothing -> printOutLn opts Info $ "All " ++ show numTests ++ " tests passed!"
-        Just counterExample -> printOutLn opts OnlyCounterExamples $
-          "----------Counterexample----------\n" ++
-          showList counterExample ""
-    Nothing -> fail $ "quickCheckPrintPrim:\n" ++
-      "term has non-testable type:\n" ++
-      pretty (ttSchema tt)
+        Just cex ->
+          do let cex' = [ (Text.unpack (toShortName (ecName ec)), v) | (ec,v) <- cex ]
+             printOutLn opts OnlyCounterExamples $
+               "----------Counterexample----------\n" ++
+               showList cex' ""
 
 cryptolSimpset :: TopLevel Simpset
 cryptolSimpset =
@@ -1124,10 +901,11 @@ beta_reduce_term (TypedTerm schema t) = do
   return (TypedTerm schema t')
 
 addsimp :: Theorem -> Simpset -> TopLevel Simpset
-addsimp (Theorem (Prop t) _stats) ss =
-  case ruleOfProp t of
-    Nothing -> fail "addsimp: theorem not an equation"
-    Just rule -> pure (addRule rule ss)
+addsimp thm ss =
+  do sc <- getSharedContext
+     io (propToRewriteRule sc (thmProp thm)) >>= \case
+       Nothing -> fail "addsimp: theorem not an equation"
+       Just rule -> pure (addRule rule ss)
 
 addsimp' :: Term -> Simpset -> TopLevel Simpset
 addsimp' t ss =
@@ -1157,12 +935,14 @@ check_term t = do
 
 check_goal :: ProofScript ()
 check_goal =
-  StateT $ \(ProofState goals concl stats timeout) ->
-  case goals of
+  StateT $ \pfst ->
+  case psGoals pfst of
     [] -> fail "ProofScript failed: no subgoal"
-    (ProofGoal _num _ty _name (Prop prop)) : _ ->
-      do check_term prop
-         return ((), ProofState goals concl stats timeout)
+    g : _ ->
+      do sc <- getSharedContext
+         tm <- io (propToTerm sc (goalProp g))
+         check_term tm
+         return ((), pfst)
 
 fixPos :: Pos
 fixPos = PosInternal "FIXME"
@@ -1211,9 +991,14 @@ cexEvalFn sc args tm = do
   args' <- mapM (scFirstOrderValue sc . snd) args
   let is = map ecVarIndex exts
       argMap = Map.fromList (zip is args')
+
+  -- TODO, instead of instantiating and then evaluating, we should
+  -- evaluate in the context of an EC map instead.  argMap is almost
+  -- what we need, but the values syould be @Concrete.CValue@ instead.
+
   tm' <- scInstantiateExt sc argMap tm
   modmap <- scGetModuleMap sc
-  return $ Concrete.evalSharedTerm modmap mempty tm'
+  return $ Concrete.evalSharedTerm modmap mempty mempty tm'
 
 toValueCase :: (SV.FromValue b) =>
                (b -> SV.Value -> SV.Value -> TopLevel SV.Value)
@@ -1448,26 +1233,30 @@ parse_core input = do
 
 prove_core :: ProofScript SV.SatResult -> String -> TopLevel Theorem
 prove_core script input =
-  do t <- parseCore input
-     (r', pstate) <- runStateT script (startProof (ProofGoal 0 "prove" "prove" (Prop t)))
+  do sc <- getSharedContext
+     t <- parseCore input
+     p <- io (termToProp sc t)
+     (r', pstate) <- runStateT script (startProof (ProofGoal 0 "prove" "prove" p))
      let r = SV.flipSatResult r'
      opts <- rwPPOpts <$> getTopLevelRW
-     case finishProof pstate of
+     io (finishProof sc pstate) >>= \case
        (_,Just thm) -> SV.returnProof thm
        (_,Nothing)  -> fail $ "prove_core: " ++ show (length (psGoals pstate)) ++ " unsolved subgoal(s)\n"
                          ++ SV.showsProofResult opts r ""
 
 core_axiom :: String -> TopLevel Theorem
 core_axiom input =
-  do t <- parseCore input
-     SV.returnProof (Theorem (Prop t) mempty)
+  do sc <- getSharedContext
+     t <- parseCore input
+     p <- io (termToProp sc t)
+     SV.returnProof (admitTheorem p)
 
 core_thm :: String -> TopLevel Theorem
 core_thm input =
   do t <- parseCore input
      sc <- getSharedContext
-     ty <- io $ scTypeOf sc t
-     SV.returnProof (Theorem (Prop ty) mempty) -- TODO: this is proved, not assumed
+     thm <- io (proofByTerm sc t)
+     SV.returnProof thm
 
 get_opt :: Int -> TopLevel String
 get_opt n = do
diff --git a/src/SAWScript/Crucible/JVM/Builtins.hs b/src/SAWScript/Crucible/JVM/Builtins.hs
index 6575e7129f..a119fa1457 100644
--- a/src/SAWScript/Crucible/JVM/Builtins.hs
+++ b/src/SAWScript/Crucible/JVM/Builtins.hs
@@ -268,9 +268,9 @@ verifyObligations cc mspec tactic assumes asserts =
      let nm = mspec ^. csMethodName
      stats <- forM (zip [(0::Int)..] asserts) $ \(n, (msg, assert)) -> do
        goal   <- io $ scImplies sc assume assert
-       goal'  <- io $ scEqTrue sc goal
+       goal'  <- io $ predicateToProp sc Universal goal
        let goalname = concat [nm, " (", takeWhile (/= '\n') msg, ")"]
-           proofgoal = ProofGoal n "vc" goalname (Prop goal')
+           proofgoal = ProofGoal n "vc" goalname goal'
        r      <- evalStateT tactic (startProof proofgoal)
        case r of
          Unsat stats -> return stats
diff --git a/src/SAWScript/Crucible/JVM/ResolveSetupValue.hs b/src/SAWScript/Crucible/JVM/ResolveSetupValue.hs
index e5a5b48f46..da2d85894c 100644
--- a/src/SAWScript/Crucible/JVM/ResolveSetupValue.hs
+++ b/src/SAWScript/Crucible/JVM/ResolveSetupValue.hs
@@ -43,10 +43,12 @@ import qualified What4.BaseTypes as W4
 import qualified What4.Interface as W4
 import qualified What4.ProgramLoc as W4
 
-import Verifier.SAW.Rewriter
 import Verifier.SAW.SharedTerm
 import Verifier.SAW.TypedTerm
 
+import qualified Verifier.SAW.Prim as Prim
+import qualified Verifier.SAW.Simulator.Concrete as Concrete
+
 import Verifier.SAW.Simulator.What4.ReturnTrip
 
 -- crucible
@@ -59,10 +61,6 @@ import qualified What4.Partial as W4
 -- crucible-jvm
 import qualified Lang.Crucible.JVM as CJ
 
--- sbv
-import qualified Verifier.SAW.Simulator.SBV as SBV (sbvSolveBasic, toWord, toBool)
-import qualified Data.SBV.Dynamic as SBV (svAsInteger, svAsBool)
-
 -- jvm-parser
 import qualified Language.JVM.Parser as J
 
@@ -70,7 +68,6 @@ import SAWScript.Crucible.Common
 import SAWScript.Crucible.Common.MethodSpec (AllocIndex(..))
 
 import SAWScript.Panic
-import SAWScript.Prover.Rewrite
 import SAWScript.Crucible.JVM.MethodSpecIR
 import qualified SAWScript.Crucible.Common.MethodSpec as MS
 
@@ -241,7 +238,6 @@ resolveSAWTerm cc tp tm =
   where
     sym = cc^.jccBackend
 
--- TODO: Instead of evaluating in SBV backend, just evaluate in W4 backend directly.
 resolveBitvectorTerm ::
   forall w.
   (1 W4.<= w) =>
@@ -252,35 +248,31 @@ resolveBitvectorTerm ::
 resolveBitvectorTerm sym w tm =
   do st <- sawCoreState sym
      let sc = saw_ctx st
-     --ss <- basic_ss sc
-     --tm' <- rewriteSharedTerm sc ss tm
-     let tm' = tm
-     mx <- case getAllExts tm' of
+     mx <- case getAllExts tm of
+             -- concretely evaluate if it is a closed term
              [] ->
-               do -- Evaluate in SBV to test whether 'tm' is a concrete value
-                  sbv <- SBV.toWord =<< SBV.sbvSolveBasic sc Map.empty mempty tm'
-                  return (SBV.svAsInteger sbv)
+               do modmap <- scGetModuleMap sc
+                  let v = Concrete.evalSharedTerm modmap mempty mempty tm
+                  pure (Just (Prim.unsigned (Concrete.toWord v)))
              _ -> return Nothing
      case mx of
        Just x  -> W4.bvLit sym w (BV.mkBV w x)
-       Nothing -> bindSAWTerm sym st (W4.BaseBVRepr w) tm'
+       Nothing -> bindSAWTerm sym st (W4.BaseBVRepr w) tm
 
--- TODO: Instead of evaluating in SBV backend, just evaluate in W4 backend directly.
 resolveBoolTerm :: Sym -> Term -> IO (W4.Pred Sym)
 resolveBoolTerm sym tm =
   do st <- sawCoreState sym
      let sc = saw_ctx st
-     ss <- basic_ss sc
-     tm' <- rewriteSharedTerm sc ss tm
-     mx <- case getAllExts tm' of
+     mx <- case getAllExts tm of
+             -- concretely evaluate if it is a closed term
              [] ->
-               do -- Evaluate in SBV to test whether 'tm' is a concrete value
-                  sbv <- SBV.toBool <$> SBV.sbvSolveBasic sc Map.empty mempty tm'
-                  return (SBV.svAsBool sbv)
+               do modmap <- scGetModuleMap sc
+                  let v = Concrete.evalSharedTerm modmap mempty mempty tm
+                  pure (Just (Concrete.toBool v))
              _ -> return Nothing
      case mx of
        Just x  -> return (W4.backendPred sym x)
-       Nothing -> bindSAWTerm sym st W4.BaseBoolRepr tm'
+       Nothing -> bindSAWTerm sym st W4.BaseBoolRepr tm
 
 toJVMType :: Cryptol.TValue -> Maybe J.Type
 toJVMType tp =
diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs
index 551efc2d9a..ab9f9b5c61 100644
--- a/src/SAWScript/Crucible/LLVM/Builtins.hs
+++ b/src/SAWScript/Crucible/LLVM/Builtins.hs
@@ -598,9 +598,9 @@ verifyObligations cc mspec tactic assumes asserts =
      stats <-
        forM (zip [(0::Int)..] asserts) $ \(n, (msg, assert)) ->
        do goal   <- io $ scImplies sc assume assert
-          goal'  <- io $ scEqTrue sc goal
+          goal'  <- io $ predicateToProp sc Universal goal
           let goalname = concat [nm, " (", takeWhile (/= '\n') msg, ")"]
-              proofgoal = ProofGoal n "vc" goalname (Prop goal')
+              proofgoal = ProofGoal n "vc" goalname goal'
           r <- evalStateT tactic (startProof proofgoal)
           case r of
             Unsat stats -> return stats
@@ -751,7 +751,7 @@ assumptionsContainContradiction ::
   TopLevel Bool
 assumptionsContainContradiction cc tactic assumptions =
   do
-     proofGoal <- io $
+     pgl <- io $
       do
          let sym = cc^.ccBackend
          st <- Common.sawCoreState sym
@@ -760,9 +760,9 @@ assumptionsContainContradiction cc tactic assumptions =
          assume <- scAndList sc (toListOf (folded . Crucible.labeledPred) assumptions)
          -- implies falsehood
          goal  <- scImplies sc assume =<< toSC sym st (W4.falsePred sym)
-         goal' <- scEqTrue sc goal
-         return $ ProofGoal 0 "vc" "vacuousness check" (Prop goal')
-     evalStateT tactic (startProof proofGoal) >>= \case
+         goal' <- predicateToProp sc Universal goal
+         return $ ProofGoal 0 "vc" "vacuousness check" goal'
+     evalStateT tactic (startProof pgl) >>= \case
        Unsat _stats -> return True
        SatMulti _stats _vals -> return False
 
diff --git a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs
index 8e79d3a1a5..57797468f5 100644
--- a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs
+++ b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs
@@ -60,14 +60,14 @@ import qualified SAWScript.Crucible.LLVM.CrucibleLLVM as Crucible
 
 import Verifier.SAW.Rewriter
 import Verifier.SAW.SharedTerm
+import qualified Verifier.SAW.Prim as Prim
+import qualified Verifier.SAW.Simulator.Concrete as Concrete
+
 import Verifier.SAW.Cryptol (importType, emptyEnv)
 import Verifier.SAW.TypedTerm
 import Verifier.SAW.Simulator.What4.ReturnTrip
 import Text.LLVM.DebugUtils as L
 
-import qualified Verifier.SAW.Simulator.SBV as SBV
-import qualified Data.SBV.Dynamic as SBV
-
 import           SAWScript.Crucible.Common (Sym, sawCoreState)
 import           SAWScript.Crucible.Common.MethodSpec (AllocIndex(..), SetupValue(..))
 
@@ -374,10 +374,10 @@ resolveSAWPred cc tm = do
      let ss = cc^.ccBasicSS
      tm' <- rewriteSharedTerm sc ss tm
      mx <- case getAllExts tm' of
-             [] -> do
-               -- Evaluate in SBV to test whether 'tm' is a concrete value
-               sbv <- SBV.toBool <$> SBV.sbvSolveBasic sc Map.empty mempty tm'
-               return (SBV.svAsBool sbv)
+             -- concretely evaluate if it is a closed term
+             [] -> do modmap <- scGetModuleMap sc
+                      let v = Concrete.evalSharedTerm modmap mempty mempty tm
+                      pure (Just (Concrete.toBool v))
              _ -> return Nothing
      case mx of
        Just x  -> return $ W4.backendPred sym x
@@ -393,17 +393,15 @@ resolveSAWSymBV cc w tm =
   do let sym = cc^.ccBackend
      st <- sawCoreState sym
      let sc = saw_ctx st
-     let ss = cc^.ccBasicSS
-     tm' <- rewriteSharedTerm sc ss tm
-     mx <- case getAllExts tm' of
-             [] -> do
-               -- Evaluate in SBV to test whether 'tm' is a concrete value
-               sbv <- SBV.toWord =<< SBV.sbvSolveBasic sc Map.empty mempty tm'
-               return (SBV.svAsInteger sbv)
+     mx <- case getAllExts tm of
+             -- concretely evaluate if it is a closed term
+             [] -> do modmap <- scGetModuleMap sc
+                      let v = Concrete.evalSharedTerm modmap mempty mempty tm
+                      pure (Just (Prim.unsigned (Concrete.toWord v)))
              _ -> return Nothing
      case mx of
        Just x  -> W4.bvLit sym w (BV.mkBV w x)
-       Nothing -> bindSAWTerm sym st (W4.BaseBVRepr w) tm'
+       Nothing -> bindSAWTerm sym st (W4.BaseBVRepr w) tm
 
 resolveSAWTerm ::
   Crucible.HasPtrWidth (Crucible.ArchWidth arch) =>
diff --git a/src/SAWScript/Proof.hs b/src/SAWScript/Proof.hs
index 1193e2da8c..4901cf72a8 100644
--- a/src/SAWScript/Proof.hs
+++ b/src/SAWScript/Proof.hs
@@ -5,24 +5,396 @@ License     : BSD3
 Maintainer  : huffman
 Stability   : provisional
 -}
-module SAWScript.Proof where
 
+{-# LANGUAGE BlockArguments #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE ViewPatterns #-}
+
+module SAWScript.Proof
+  ( Prop
+  , splitProp
+  , unfoldProp
+  , simplifyProp
+  , evalProp
+  , betaReduceProp
+  , falseProp
+  , termToProp
+  , propToTerm
+  , propToRewriteRule
+  , propIsTrivial
+  , propSize
+  , prettyProp
+  , ppProp
+  , propToSATQuery
+
+  , Theorem
+  , thmProp
+  , thmStats
+  , thmEvidence
+
+  , admitTheorem
+  , solverTheorem
+  , proofByTerm
+  , constructTheorem
+  , validateTheorem
+
+  , Evidence(..)
+  , checkEvidence
+
+  , Tactic
+  , withFirstGoal
+  , tacticIntro
+  , tacticCut
+  , tacticAssume
+  , tacticApply
+  , tacticSplit
+  , tacticTrivial
+  , tacticId
+  , tacticChange
+  , tacticSolve
+
+  , Quantification(..)
+  , predicateToProp
+
+  , ProofState
+  , psTimeout
+  , psGoals
+  , setProofTimeout
+  , ProofGoal(..)
+  , startProof
+  , finishProof
+
+  , predicateToSATQuery
+  ) where
+
+import qualified Control.Monad.Fail as F
+import           Control.Monad.State
+import           Data.Maybe (fromMaybe)
+import qualified Data.Map as Map
+import           Data.Set (Set)
+import qualified Data.Set as Set
+import           Data.Text (Text)
+import qualified Data.Text as Text
+
+import Verifier.SAW.Prelude (scApplyPrelude_False)
 import Verifier.SAW.Recognizer
+import Verifier.SAW.Rewriter
+import Verifier.SAW.SATQuery
 import Verifier.SAW.SharedTerm
+import Verifier.SAW.TypedAST
+import Verifier.SAW.TypedTerm
+import Verifier.SAW.Term.Pretty (SawDoc)
+import Verifier.SAW.SCTypeCheck (scTypeCheckError)
+
+import Verifier.SAW.Simulator.Concrete (evalSharedTerm)
+import Verifier.SAW.Simulator.Value (asFirstOrderTypeValue)
+
 import SAWScript.Prover.SolverStats
+import SAWScript.Crucible.Common as Common
+import qualified Verifier.SAW.Simulator.What4 as W4Sim
+import qualified Verifier.SAW.Simulator.What4.ReturnTrip as W4Sim
 
 -- | A proposition is a saw-core type (i.e. a term of type @sort n@
 -- for some @n@). In particular, this includes any pi type whose
 -- result type is a proposition. The argument of a pi type represents
 -- a universally quantified variable.
-newtype Prop = Prop { unProp :: Term }
+newtype Prop = Prop Term
+  -- INVARIANT: The type of the given term is a sort
+
+unProp :: Prop -> Term
+unProp (Prop tm) = tm
+
+-- | Turn a saw-core term into a proposition under the type-as-propositions
+--   regime.  The given term must be a type, which means that its own type
+--   is a sort.
+termToProp :: SharedContext -> Term -> IO Prop
+termToProp sc tm =
+   do ty <- scWhnf sc =<< scTypeOf sc tm
+      case asSort ty of
+        Nothing -> fail $ unlines [ "termToProp: Term is not a proposition", showTerm tm ]
+        Just _s -> return (Prop tm)
+
+-- | Return the saw-core term that represents this proposition.
+propToTerm :: SharedContext -> Prop -> IO Term
+propToTerm _sc (Prop tm) = pure tm
+
+-- | Attempt to interpret a proposition as a rewrite rule.
+propToRewriteRule :: SharedContext -> Prop -> IO (Maybe (RewriteRule))
+propToRewriteRule _sc (Prop tm) =
+  case ruleOfProp tm of
+    Nothing -> pure Nothing
+    Just r  -> pure (Just r)
+
+-- | Attempt to split a conjunctive proposition into two propositions,
+--   such that a proof of both return propositions is equivalent to
+--   a proof of the original.
+splitProp :: SharedContext -> Prop -> IO (Maybe (Prop, Prop))
+splitProp sc (Prop p) =
+  do let (vars, body) = asPiList p
+     case (isGlobalDef "Prelude.and" <@> return <@> return) =<< asEqTrue body of
+       Nothing -> pure Nothing
+       Just (_ :*: p1 :*: p2) ->
+         do t1 <- scPiList sc vars =<< scEqTrue sc p1
+            t2 <- scPiList sc vars =<< scEqTrue sc p2
+            return (Just (Prop t1,Prop t2))
+
+-- | Unfold all the constants appearing in the proposition
+--   whose VarIndex is found in the given set.
+unfoldProp :: SharedContext -> Set VarIndex -> Prop -> IO Prop
+unfoldProp sc unints (Prop tm) =
+  do tm' <- scUnfoldConstantSet sc True unints tm
+     return (Prop tm')
+
+-- | Rewrite the proposition using the provided Simpset
+simplifyProp :: SharedContext -> Simpset -> Prop -> IO Prop
+simplifyProp sc ss (Prop tm) =
+  do tm' <- rewriteSharedTerm sc ss tm
+     return (Prop tm')
+
+-- | Evaluate the given proposition by round-tripping
+--   through the What4 formula representation.  This will
+--   perform a variety of simplifications and rewrites.
+evalProp :: SharedContext -> Set VarIndex -> Prop -> IO Prop
+evalProp sc unints (Prop p) =
+  do let (args, body) = asPiList p
+
+     body' <-
+       case asEqTrue body of
+         Just t -> pure t
+         Nothing -> fail "goal_eval: expected EqTrue"
+
+     ecs <- traverse (\(nm, ty) -> scFreshEC sc (Text.unpack nm) ty) args
+     vars <- traverse (scExtCns sc) ecs
+     t0 <- instantiateVarList sc 0 (reverse vars) body'
+
+     sym <- Common.newSAWCoreBackend sc
+     st <- Common.sawCoreState sym
+     (_names, (_mlabels, p')) <- W4Sim.w4Eval sym st sc mempty unints t0
+     t1 <- W4Sim.toSC sym st p'
+
+     t2 <- scEqTrue sc t1
+     -- turn the free variables we generated back into pi-bound variables
+     t3 <- scGeneralizeExts sc ecs t2
+     return (Prop t3)
+
+-- | Perform beta normalization on the given proposition.
+betaReduceProp :: SharedContext -> Prop -> IO Prop
+betaReduceProp sc (Prop tm) =
+  do tm' <- betaNormalize sc tm
+     return (Prop tm')
+
+-- | Return the contant false proposition.
+falseProp :: SharedContext -> IO Prop
+falseProp sc = Prop <$> (scEqTrue sc =<< scApplyPrelude_False sc)
+
+-- | Compute the shared-term size of the proposition.
+propSize :: Prop -> Integer
+propSize (Prop tm) = scSharedSize tm
+
+-- | Test if the given proposition is trivially true.  This holds
+--   just when the proposition is a (possibly empty) sequence of
+--   Pi-types followed by an @EqTrue@ proposition for a
+--   concretely-true boolean value.
+propIsTrivial :: Prop -> Bool
+propIsTrivial (Prop tm) = checkTrue tm
+  where
+    checkTrue :: Term -> Bool
+    checkTrue (asPiList -> (_, asEqTrue -> Just (asBool -> Just True))) = True
+    checkTrue _ = False
+
+-- | Pretty print the given proposition as a string.
+prettyProp :: PPOpts -> Prop -> String
+prettyProp opts (Prop tm) = scPrettyTerm opts tm
+
+-- | Pretty print the given proposition as a @SawDoc@.
+ppProp :: PPOpts -> Prop -> SawDoc
+ppProp opts (Prop tm) = ppTerm opts tm
 
 -- | A theorem is a proposition which has been wrapped in a
--- constructor indicating that it has already been proved.
+--   constructor indicating that it has already been proved,
+--   and contains @Evidence@ for its truth.
 data Theorem =
   Theorem
-  { thmProp :: Prop
-  , thmStats :: SolverStats
+  { _thmProp :: Prop
+  , _thmStats :: SolverStats
+  , _thmEvidence :: Evidence
+  } -- INVARIANT: the provided evidence is valid for the included proposition
+
+  | LocalAssumption Prop
+      -- This constructor is used to construct "hypothetical" theorems that
+      -- are intended to be used in local scopes when proving implications.
+
+-- | Check that the purported theorem is valid.
+--
+--   This checks that the given theorem object does not correspond
+--   to a local assumption that has been leaked from its scope,
+--   and validates that the included evidence actually supports
+--   the proposition.  Note, however, this validation procedure
+--   does not totally guarantee the theorem is true, as it does
+--   not rerun any solver-provided proofs, and it accepts admitted
+--   propositions and quickchecked propositions as valid.
+validateTheorem :: SharedContext -> Theorem -> IO ()
+
+validateTheorem _sc (LocalAssumption p) =
+   fail $ unlines
+     [ "Illegal use of unbound local hypothesis"
+     , showTerm (unProp p)
+     ]
+
+validateTheorem sc Theorem{ _thmProp = p, _thmEvidence = e } =
+   checkEvidence sc e p
+
+-- | This datatype records evidence for the truth of a proposition.
+data Evidence
+  = -- | The given term provides a direct programs-as-proofs witness
+    --   for the truth of its type (qua proposition).
+    ProofTerm Term
+
+    -- | This type of evidence refers to a local assumption that
+    --   must have been introduced by a surrounding @AssumeEvidence@
+    --   constructor.
+  | LocalAssumptionEvidence Prop
+
+    -- | This type of evidence is produced when the given proposition
+    --   has been dispatched to a solver which has indicated that it
+    --   was able to prove the proposition.  The included @SolverStats@
+    --   give some details about the solver run.
+  | SolverEvidence SolverStats Prop
+
+    -- | This type of evidence is produced when the given proposition
+    --   has been randomly tested against input vectors in the style
+    --   of quickcheck.  The included number is the number of successfully
+    --   passed test vectors.
+  | QuickcheckEvidence Integer Prop
+
+    -- | This type of evidence is produced when the given proposition
+    --   has been explicitly assumed without other evidence at the
+    --   user's direction.
+  | Admitted Prop
+
+    -- | This type of evidence is produced when a given proposition is trivially
+    --   true.
+  | TrivialEvidence
+
+    -- | This type of evidence is produced when a proposition can be deconstructed
+    --   along a conjunction into two subgoals, each of which is supported by
+    --   the included evidence.
+  | SplitEvidence Evidence Evidence
+
+    -- | This type of evidence is produced when a previously-proved theorem is
+    --   applied via backward reasoning to prove a goal.  Some of the hypotheses
+    --   of the theorem may be discharged via the included list of evidence, and
+    --   then the proposition must match the conclusion of the theorem.
+  | ApplyEvidence Theorem [Evidence]
+
+    -- | This type of evidence is used to prove an implication.  The included
+    --   proposition must match the hypothesis of the goal, and the included
+    --   evidence must match the conclusion of the goal.  The proposition is
+    --   allowed to appear inside the evidence as a local assumption.
+  | AssumeEvidence Prop Evidence
+
+    -- | This type of evidence is used to prove a universally-quantified statement.
+  | ForallEvidence (ExtCns Term) Evidence
+
+    -- | This type of evidence is used to weaken a goal by adding a hypothesis,
+    --   where the hypothesis is proved by the given theorem.
+  | CutEvidence Theorem Evidence
+
+    -- | This type of evidence is used to modify a goal to prove via rewriting.
+    --   The goal to prove is rewritten by the given simpset; then the provided
+    --   evidence is used to check the modified goal.
+  | RewriteEvidence Simpset Evidence
+
+    -- | This type of evidence is used to modify a goal to prove via unfolding
+    --   constant definitions.  The goal to prove is modified by unfolding
+    --   constants identified via the given set of @VarIndex@; then the provided
+    --   evidence is used to check the modified goal.
+  | UnfoldEvidence (Set VarIndex) Evidence
+
+    -- | This type of evidence is used to modify a goal to prove via evaluation
+    --   into the the What4 formula representation. During evaluation, the
+    --   constants identified by the given set of @VarIndex@ are held
+    --   uninterpreted (i.e., will not be unfolded).  Then, the provided
+    --   evidence is use to check the modified goal.
+  | EvalEvidence (Set VarIndex) Evidence
+
+-- | The the proposition proved by a given theorem.
+thmProp :: Theorem -> Prop
+thmProp (LocalAssumption p) = p
+thmProp Theorem{ _thmProp = p } = p
+
+-- | Retrieve any solver stats from the proved theorem.
+thmStats :: Theorem -> SolverStats
+thmStats (LocalAssumption _) = mempty
+thmStats Theorem{ _thmStats = stats } = stats
+
+-- | Retrive the evidence associated with this theorem.
+thmEvidence :: Theorem -> Evidence
+thmEvidence (LocalAssumption p) = LocalAssumptionEvidence p
+thmEvidence Theorem{ _thmEvidence = e } = e
+
+impossibleEvidence :: [Evidence] -> IO Evidence
+impossibleEvidence _ = fail "impossibleEvidence: attempted to check an impossible proof!"
+
+splitEvidence :: [Evidence] -> IO Evidence
+splitEvidence [e1,e2] = pure (SplitEvidence e1 e2)
+splitEvidence _ = fail "splitEvidence: expected two evidence values"
+
+assumeEvidence :: Prop -> [Evidence] -> IO Evidence
+assumeEvidence p [e] = pure (AssumeEvidence p e)
+assumeEvidence _ _ = fail "assumeEvidence: expected one evidence value"
+
+forallEvidence :: ExtCns Term -> [Evidence] -> IO Evidence
+forallEvidence x [e] = pure (ForallEvidence x e)
+forallEvidence _ _ = fail "forallEvidence: expected one evidence value"
+
+cutEvidence :: Theorem -> [Evidence] -> IO Evidence
+cutEvidence thm [e] = pure (CutEvidence thm e)
+cutEvidence _ _ = fail "cutEvidence: expected one evidence value"
+
+-- | Construct a theorem directly via a proof term.
+proofByTerm :: SharedContext -> Term -> IO Theorem
+proofByTerm sc prf =
+  do ty <- scTypeOf sc prf
+     p  <- termToProp sc ty
+     return
+       Theorem
+       { _thmProp      = p
+       , _thmStats     = mempty
+       , _thmEvidence  = ProofTerm prf
+       }
+
+-- | Construct a theorem directly from a proposition and evidence
+--   for that proposition.  The evidence will be validated to
+--   check that it supports the given proposition; if not, an
+--   error will be raised.
+constructTheorem :: SharedContext -> Prop -> Evidence -> IO Theorem
+constructTheorem sc p e =
+  do checkEvidence sc e p
+     return
+       Theorem
+       { _thmProp  = p
+       , _thmStats = mempty
+       , _thmEvidence = e
+       }
+
+-- | Admit the given theorem without evidence.
+admitTheorem :: Prop -> Theorem
+admitTheorem p =
+  Theorem
+  { _thmProp      = p
+  , _thmStats     = solverStats "ADMITTED" (propSize p)
+  , _thmEvidence  = Admitted p
+  }
+
+-- | Construct a theorem that an external solver has proved.
+solverTheorem :: Prop -> SolverStats -> Theorem
+solverTheorem p stats =
+  Theorem
+  { _thmProp      = p
+  , _thmStats     = stats
+  , _thmEvidence  = SolverEvidence stats p
   }
 
 -- | A @ProofGoal@ contains a proposition to be proved, along with
@@ -35,77 +407,476 @@ data ProofGoal =
   , goalProp :: Prop
   }
 
+
 data Quantification = Existential | Universal
   deriving Eq
 
--- | Construct a 'ProofGoal' from a term of type @Bool@, or a function
--- of any arity with a boolean result type. Any function arguments are
--- treated as quantified variables. If the 'Quantification' argument
--- is 'Existential', then the predicate is negated and turned into a
--- universally-quantified goal.
-makeProofGoal ::
-  SharedContext ->
-  Quantification ->
-  Int    {- goal number    -} ->
-  String {- goal type      -} ->
-  String {- goal name      -} ->
-  Term   {- goal predicate -} ->
-  IO ProofGoal
-makeProofGoal sc quant gnum gtype gname t =
-  do t' <- predicateToProp sc quant [] t
-     return (ProofGoal gnum gtype gname t')
-
 -- | Convert a term with a function type of any arity into a pi type.
 -- Negate the term if the result type is @Bool@ and the quantification
 -- is 'Existential'.
-predicateToProp :: SharedContext -> Quantification -> [Term] -> Term -> IO Prop
-predicateToProp sc quant env t =
-  case asLambda t of
-    Just (x, ty, body) ->
-      do Prop body' <- predicateToProp sc quant (ty : env) body
-         Prop <$> scPi sc x ty body'
-    Nothing ->
-      do (argTs, resT) <- asPiList <$> scTypeOf' sc env t
-         let toPi [] t0 =
-               case asBoolType resT of
-                 Nothing -> return t0 -- TODO: check quantification
-                 Just () ->
-                   case quant of
-                     Universal -> scEqTrue sc t0
-                     Existential -> scEqTrue sc =<< scNot sc t0
-             toPi ((x, xT) : tys) t0 =
-               do t1 <- incVars sc 0 1 t0
-                  t2 <- scApply sc t1 =<< scLocalVar sc 0
-                  t3 <- toPi tys t2
-                  scPi sc x xT t3
-         Prop <$> toPi argTs t
-
--- | Turn a pi type with an @EqTrue@ result into a lambda term with a
--- boolean result type. This function exists to interface the new
--- pi-type proof goals with older proof tactic implementations that
--- expect the old lambda-term representation.
-propToPredicate :: SharedContext -> Prop -> IO Term
-propToPredicate sc (Prop goal) =
-  do let (args, t1) = asPiList goal
-     case asEqTrue t1 of
-       Just t2 -> scLambdaList sc args t2
-       Nothing -> fail $ "propToPredicate: expected EqTrue, actual " ++ show t1
+predicateToProp :: SharedContext -> Quantification -> Term -> IO Prop
+predicateToProp sc quant = loop []
+  where
+  loop env t =
+    case asLambda t of
+      Just (x, ty, body) ->
+        do Prop body' <- loop (ty : env) body
+           Prop <$> scPi sc x ty body'
+      Nothing ->
+        do (argTs, resT) <- asPiList <$> scTypeOf' sc env t
+           let toPi [] t0 =
+                 case asBoolType resT of
+                   Nothing -> return t0 -- TODO: check quantification  TODO2: should this just be an error?
+                   Just () ->
+                     case quant of
+                       Universal -> scEqTrue sc t0
+                       Existential -> scEqTrue sc =<< scNot sc t0
+               toPi ((x, xT) : tys) t0 =
+                 do t1 <- incVars sc 0 1 t0
+                    t2 <- scApply sc t1 =<< scLocalVar sc 0
+                    t3 <- toPi tys t2
+                    scPi sc x xT t3
+           Prop <$> toPi argTs t
+
 
 -- | A ProofState represents a sequent, where the collection of goals
 -- implies the conclusion.
 data ProofState =
   ProofState
-  { psGoals :: [ProofGoal]
-  , psConcl :: ProofGoal
-  , psStats :: SolverStats
-  , psTimeout :: Maybe Integer
+  { _psGoals :: [ProofGoal]
+  , _psConcl :: Prop
+  , _psStats :: SolverStats
+  , _psTimeout :: Maybe Integer
+  , _psEvidence :: [Evidence] -> IO Evidence
   }
 
+psTimeout :: ProofState -> Maybe Integer
+psTimeout = _psTimeout
+
+psGoals :: ProofState -> [ProofGoal]
+psGoals = _psGoals
+
+-- | Verify that the given evidence in fact supports
+--   the given proposition.
+checkEvidence :: SharedContext -> Evidence -> Prop -> IO ()
+checkEvidence sc = check mempty
+  where
+    checkApply _hyps (Prop p) [] = return p
+    checkApply hyps (Prop p) (e:es)
+      | Just (_lnm, tp, body) <- asPi p
+      , looseVars body == emptyBitSet
+      = do check hyps e =<< termToProp sc tp
+           checkApply hyps (Prop body) es
+      | otherwise = fail $ unlines
+           [ "Apply evidence mismatch: non-function or dependent function"
+           , showTerm p
+           ]
+
+    checkTheorem :: Set Term -> Theorem -> IO ()
+    checkTheorem hyps (LocalAssumption p) =
+       unless (Set.member (unProp p) hyps) $ fail $ unlines
+          [ "Attempt to reference a local hypothesis that is not in scope"
+          , showTerm (unProp p)
+          ]
+    checkTheorem _hyps Theorem{} = return ()
+
+    check :: Set Term -> Evidence -> Prop -> IO ()
+    check hyps e p@(Prop ptm) = case e of
+      ProofTerm tm ->
+        do ty <- scTypeCheckError sc tm
+           ok <- scConvertible sc False ptm ty
+           unless ok $ fail $ unlines
+               [ "Proof term does not prove the required proposition"
+               , showTerm ptm
+               , showTerm tm
+               ]
+
+      LocalAssumptionEvidence (Prop l) ->
+        unless (Set.member l hyps) $ fail $ unlines
+             [ "Illegal use of local hypothesis"
+             , showTerm l
+             ]
+
+      SolverEvidence _stats (Prop p') ->
+        do ok <- scConvertible sc False ptm p'
+           unless ok $ fail $ unlines
+               [ "Solver proof does not prove the required proposition"
+               , showTerm ptm
+               , showTerm p'
+               ]
+
+      Admitted (Prop p') ->
+        do ok <- scConvertible sc False ptm p'
+           unless ok $ fail $ unlines
+               [ "Admitted proof does not match the required proposition"
+               , showTerm ptm
+               , showTerm p'
+               ]
+
+      QuickcheckEvidence _n (Prop p') ->
+        do ok <- scConvertible sc False ptm p'
+           unless ok $ fail $ unlines
+               [ "Quickcheck evidence does not match the required proposition"
+               , showTerm ptm
+               , showTerm p'
+               ]
+
+      TrivialEvidence ->
+        unless (propIsTrivial p) $ fail $ unlines
+            [ "Proposition is not trivial"
+            , showTerm ptm
+            ]
+
+      SplitEvidence e1 e2 ->
+        splitProp sc p >>= \case
+          Nothing -> fail $ unlines
+                       [ "Split evidence does not apply to non-conjunction prop"
+                       , showTerm ptm
+                       ]
+          Just (p1,p2) ->
+            do check hyps e1 p1
+               check hyps e2 p2
+
+      ApplyEvidence thm es ->
+        do checkTheorem hyps thm
+           p' <- checkApply hyps (thmProp thm) es
+           ok <- scConvertible sc False ptm p'
+           unless ok $ fail $ unlines
+               [ "Apply evidence does not match the required proposition"
+               , showTerm ptm
+               , showTerm p'
+               ]
+
+      CutEvidence thm e' ->
+        do checkTheorem hyps thm
+           p' <- scFun sc (unProp (thmProp thm)) ptm
+           check hyps e' (Prop p')
+
+      UnfoldEvidence vars e' ->
+        do p' <- unfoldProp sc vars p
+           check hyps e' p'
+
+      RewriteEvidence ss e' ->
+        do p' <- simplifyProp sc ss p
+           check hyps e' p'
+
+      EvalEvidence vars e' ->
+        do p' <- evalProp sc vars p
+           check hyps e' p'
+
+      AssumeEvidence (Prop p') e' ->
+        case asPi ptm of
+          Nothing -> fail $ unlines ["Assume evidence expected function prop", showTerm ptm]
+          Just (_lnm, ty, body) ->
+            do ok <- scConvertible sc False ty p'
+               unless ok $ fail $ unlines
+                   [ "Assume evidence types do not match"
+                   , showTerm ty
+                   , showTerm p'
+                   ]
+               unless (looseVars body == emptyBitSet) $ fail $ unlines
+                   [ "Assume evidence cannot be used on a dependent proposition"
+                   , showTerm ptm
+                   ]
+               check (Set.insert p' hyps) e' (Prop body)
+
+      ForallEvidence x e' ->
+        case asPi ptm of
+          Nothing -> fail $ unlines ["Assume evidence expected function prop", showTerm ptm]
+          Just (_lnm, ty, body) ->
+            do let ty' = ecType x
+               ok <- scConvertible sc False ty ty'
+               unless ok $ fail $ unlines
+                 ["Forall evidence types do not match"
+                 , showTerm ty'
+                 , showTerm ty
+                 ]
+               x' <- scExtCns sc x
+               body' <- instantiateVar sc 0 x' body
+               check hyps e' (Prop body')
+
+passthroughEvidence :: [Evidence] -> IO Evidence
+passthroughEvidence [e] = pure e
+passthroughEvidence _   = fail "passthroughEvidence: incorrect arity"
+
+updateEvidence :: (Evidence -> Evidence) -> [Evidence] -> IO Evidence
+updateEvidence f [e] = pure (f e)
+updateEvidence _ _ = fail "updateEvidence: incorrect arity"
+
+leafEvidence :: Evidence -> [Evidence] -> IO Evidence
+leafEvidence e [] = pure e
+leafEvidence _ _  = fail "leafEvidence: incorrect arity"
+
+setProofTimeout :: Integer -> ProofState -> ProofState
+setProofTimeout to ps = ps { _psTimeout = Just to }
+
+-- | Initialize a proof state with a single goal to prove.
 startProof :: ProofGoal -> ProofState
-startProof g = ProofState [g] g mempty Nothing
+startProof g = ProofState [g] (goalProp g) mempty Nothing passthroughEvidence
 
-finishProof :: ProofState -> (SolverStats, Maybe Theorem)
-finishProof (ProofState gs concl stats _) =
+-- | Attempt to complete a proof by checking that all subgoals have been discharged,
+--   and validate the computed evidence to ensure that it supports the original
+--   proposition.  If successful, return the completed @Theorem@ and a summary
+--   of solver resources used in the proof.
+finishProof :: SharedContext -> ProofState -> IO (SolverStats, Maybe Theorem)
+finishProof sc (ProofState gs concl stats _ checkEv) =
   case gs of
-    []    -> (stats, Just (Theorem (goalProp concl) stats))
-    _ : _ -> (stats, Nothing)
+    [] ->
+      do e <- checkEv []
+         checkEvidence sc e concl
+         let thm = Theorem
+                   { _thmProp = concl
+                   , _thmStats = stats
+                   , _thmEvidence = e
+                   }
+         pure (stats, Just thm)
+    _ : _ ->
+         pure (stats, Nothing)
+
+-- | A @Tactic@ is a computation that examines, simplifies
+--   and/or solves a proof goal.  Given a goal, it does some
+--   work and returns 0 or more subgoals which, if they are all proved,
+--   imply the original goal.  Moreover, it returns a way to compute
+--   evidence for the original goal when given evidence for the generated
+--   subgoal.  An important special case is a tactic that returns 0 subgoals,
+--   and therefore completely solves the goal.
+newtype Tactic m a = Tactic
+    { runTactic :: ProofGoal -> m (a, SolverStats, [ProofGoal], [Evidence] -> IO Evidence) }
+
+-- | Choose the first subgoal in the current proof state and apply the given
+--   proof tactic.
+withFirstGoal :: F.MonadFail m => Tactic m a -> StateT ProofState m a
+withFirstGoal f =
+  StateT $ \(ProofState goals concl stats timeout evidenceCont) ->
+  case goals of
+    [] -> fail "ProofScript failed: no subgoal"
+    g : gs -> do
+      (x, stats', gs', buildTacticEvidence) <- runTactic f g
+      let evidenceCont' es =
+              do let (es1, es2) = splitAt (length gs') es
+                 e <- buildTacticEvidence es1
+                 evidenceCont (e:es2)
+      return (x, ProofState (gs' <> gs) concl (stats <> stats') timeout evidenceCont')
+
+predicateToSATQuery :: SharedContext -> Set VarIndex -> Term -> IO SATQuery
+predicateToSATQuery sc unintSet tm0 =
+    do mmap <- scGetModuleMap sc
+       (initVars, abstractVars) <- filterFirstOrderVars mmap mempty mempty (getAllExts tm0)
+       (finalVars, tm') <- processTerm mmap initVars tm0
+       return SATQuery
+              { satVariables = finalVars
+              , satUninterp  = Set.union unintSet abstractVars
+              , satAsserts   = [tm']
+              }
+  where
+    evalFOT mmap t =
+      asFirstOrderTypeValue (evalSharedTerm mmap mempty mempty t)
+
+    filterFirstOrderVars _ fovars absvars [] = pure (fovars, absvars)
+    filterFirstOrderVars mmap fovars absvars (e:es) =
+      case evalFOT mmap (ecType e) of
+        Nothing  -> filterFirstOrderVars mmap fovars (Set.insert (ecVarIndex e) absvars) es
+        Just fot -> filterFirstOrderVars mmap (Map.insert e fot fovars) absvars es
+
+    processTerm mmap vars tm =
+      case asLambda tm of
+        Just (lnm,tp,body) ->
+          case evalFOT mmap tp of
+            Nothing -> fail ("predicateToSATQuery: expected first order type: " ++ showTerm tp)
+            Just fot ->
+              do ec  <- scFreshEC sc (Text.unpack lnm) tp
+                 etm <- scExtCns sc ec
+                 body' <- instantiateVar sc 0 etm body
+                 processTerm mmap (Map.insert ec fot vars) body'
+
+          -- TODO: check that the type is a boolean
+        Nothing ->
+          do ty <- scTypeOf sc tm
+             ok <- scConvertible sc True ty =<< scBoolType sc
+             unless ok $ fail $ unlines
+               [ "predicateToSATQuery: expected boolean result but got:"
+               , showTerm ty
+               , showTerm tm0
+               ]
+             return (vars, tm)
+
+-- | Given a proposition, compute a SAT query which will prove the proposition
+--   iff the SAT query is unsatisfiable.
+propToSATQuery :: SharedContext -> Set VarIndex -> Prop -> IO SATQuery
+propToSATQuery sc unintSet prop =
+    do mmap <- scGetModuleMap sc
+       tm <- propToTerm sc prop
+       (initVars, abstractVars) <- filterFirstOrderVars mmap mempty mempty (getAllExts tm)
+       (finalVars, asserts)     <- processTerm mmap initVars [] tm
+       return SATQuery
+              { satVariables = finalVars
+              , satUninterp  = Set.union unintSet abstractVars
+              , satAsserts   = asserts
+              }
+
+  where
+    evalFOT mmap t =
+      asFirstOrderTypeValue (evalSharedTerm mmap mempty mempty t)
+
+    filterFirstOrderVars _ fovars absvars [] = pure (fovars, absvars)
+    filterFirstOrderVars mmap fovars absvars (e:es) =
+      case evalFOT mmap (ecType e) of
+         Nothing  -> filterFirstOrderVars mmap fovars (Set.insert (ecVarIndex e) absvars) es
+         Just fot -> filterFirstOrderVars mmap (Map.insert e fot fovars) absvars es
+
+    processTerm mmap vars xs tm =
+      case asPi tm of
+        Just (lnm, tp, body)
+          | Just x <- asEqTrue tp
+          , looseVars body == emptyBitSet ->
+              do processTerm mmap vars (x:xs) body
+
+            -- TODO? Allow universal hypotheses...
+
+          | otherwise ->
+              case evalFOT mmap tp of
+                Nothing -> fail ("propToSATQuery: expected first order type: " ++ showTerm tp)
+                Just fot ->
+                  do ec  <- scFreshEC sc (Text.unpack lnm) tp
+                     etm <- scExtCns sc ec
+                     body' <- instantiateVar sc 0 etm body
+                     processTerm mmap (Map.insert ec fot vars) xs body'
+
+        Nothing ->
+          case asEqTrue tm of
+            Nothing  -> fail $ "propToSATQuery: expected EqTrue, actual " ++ showTerm tm
+            Just tmBool ->
+              do tmNeg <- scNot sc tmBool
+                 return (vars, reverse (tmNeg:xs))
+
+-- | Given a goal to prove, attempt to apply the given proposition, producing
+--   new subgoals for any necessary hypotheses of the proposition.  Returns
+--   @Nothing@ if the given proposition does not apply to the goal.
+goalApply :: SharedContext -> Prop-> ProofGoal -> IO (Maybe [ProofGoal])
+goalApply sc rule goal = applyFirst (asPiLists (unProp rule))
+  where
+
+    applyFirst [] = pure Nothing
+    applyFirst ((ruleArgs, ruleConcl) : rest) =
+      do result <- scMatch sc ruleConcl (unProp (goalProp goal))
+         case result of
+           Nothing -> applyFirst rest
+           Just inst ->
+             do let inst' = [ Map.lookup i inst | i <- take (length ruleArgs) [0..] ]
+                dummy <- scUnitType sc
+                let mkNewGoals (Nothing : mts) ((_, prop) : args) =
+                      do c0 <- instantiateVarList sc 0 (map (fromMaybe dummy) mts) prop
+                         cs <- mkNewGoals mts args
+                         return (Prop c0 : cs)
+                    mkNewGoals (Just _ : mts) (_ : args) =
+                      mkNewGoals mts args
+                    mkNewGoals _ _ = return []
+                newgoalterms <- mkNewGoals inst' (reverse ruleArgs)
+                -- TODO, change the "ty" field to list the hypotheses?
+                let newgoals = reverse [ goal { goalProp = t } | t <- newgoalterms ]
+                return (Just newgoals)
+
+    asPiLists :: Term -> [([(Text, Term)], Term)]
+    asPiLists t =
+      case asPi t of
+        Nothing -> [([], t)]
+        Just (nm, tp, body) ->
+          [ ((nm, tp) : args, concl) | (args, concl) <- asPiLists body ] ++ [([], t)]
+
+
+-- | Attempt to prove a universally quantified goal by introducing a fresh variable
+--   for the binder.  Return the generated fresh term.
+tacticIntro :: (F.MonadFail m, MonadIO m) =>
+  SharedContext ->
+  String {- ^ Name to give to the variable.  If empty, will be chosen automatically from the goal. -} ->
+  Tactic m TypedTerm
+tacticIntro sc usernm = Tactic \goal ->
+  case asPi (unProp (goalProp goal)) of
+    Just (nm, tp, body) ->
+      do let name = if null usernm then Text.unpack nm else usernm
+         xv <- liftIO $ scFreshEC sc name tp
+         x  <- liftIO $ scExtCns sc xv
+         tt <- liftIO $ mkTypedTerm sc x
+         body' <- liftIO $ instantiateVar sc 0 x body
+         let goal' = goal { goalProp = Prop body' }
+         return (tt, mempty, [goal'], forallEvidence xv)
+
+    _ -> fail "intro tactic failed: not a function"
+
+-- | Attempt to prove an implication goal by introducing a local assumption for
+--   hypothesis.  Return a @Theorem@ representing this local assumption.
+--   This hypothesis should only be used for proving subgoals arising
+--   from this call to @tacticAssume@ or evidence verification will later fail.
+tacticAssume :: (F.MonadFail m, MonadIO m) => SharedContext -> Tactic m Theorem
+tacticAssume _sc = Tactic \goal ->
+  case asPi (unProp (goalProp goal)) of
+    Just (_nm, tp, body)
+      | looseVars body == emptyBitSet ->
+          do let goal' = goal{ goalProp = Prop body }
+             let p     = Prop tp
+             let thm'  = LocalAssumption p
+             return (thm', mempty, [goal'], assumeEvidence p)
+
+    _ -> fail "assume tactic failed: not a function, or a dependent function"
+
+-- | Attempt to prove a goal by weakening it with a new hypothesis, which is
+--   justified by the given theorem.
+tacticCut :: (F.MonadFail m, MonadIO m) => SharedContext -> Theorem -> Tactic m ()
+tacticCut sc thm = Tactic \goal ->
+  do body' <- liftIO (scFun sc (unProp (thmProp thm)) (unProp (goalProp goal)))
+     let goal' = goal{ goalProp = Prop body' }
+     return ((), mempty, [goal'], cutEvidence thm)
+
+-- | Attempt to prove a goal by applying the given theorem.  Any hypotheses of
+--   the theorem will generate additional subgoals.
+tacticApply :: (F.MonadFail m, MonadIO m) => SharedContext -> Theorem -> Tactic m ()
+tacticApply sc thm = Tactic \goal ->
+  liftIO (goalApply sc (thmProp thm) goal) >>= \case
+    Nothing -> fail "apply tactic failed: no match"
+    Just newgoals ->
+      return ((), mempty, newgoals, pure . ApplyEvidence thm)
+
+-- | Attempt to simplify a goal by splitting it along conjunctions.  If successful,
+--   two subgoals will be produced, representing the two conjuncts to be proved.
+tacticSplit :: (F.MonadFail m, MonadIO m) => SharedContext -> Tactic m ()
+tacticSplit sc = Tactic \(ProofGoal num ty name prop) ->
+  liftIO (splitProp sc prop) >>= \case
+    Nothing -> fail "split tactic failed: goal not a conjunction"
+    Just (p1,p2) ->
+      do let g1 = ProofGoal num (ty ++ ".left")  name p1
+         let g2 = ProofGoal num (ty ++ ".right") name p2
+         return ((), mempty, [g1,g2], splitEvidence)
+
+-- | Attempt to solve a goal by recognizing it as a trivially true proposition.
+tacticTrivial :: (F.MonadFail m, MonadIO m) => SharedContext -> Tactic m ()
+tacticTrivial _sc = Tactic \goal ->
+  if (propIsTrivial (goalProp goal)) then
+    return ((), mempty, [], leafEvidence TrivialEvidence)
+  else
+    fail "trivial tactic: not a trivial goal"
+
+-- | Examine the given proof goal and potentially do some work with it,
+--   but do not alter the proof state.
+tacticId :: Monad m => (ProofGoal -> m ()) -> Tactic m ()
+tacticId f = Tactic \gl ->
+  do f gl
+     return ((), mempty, [gl], passthroughEvidence)
+
+-- | Attempt to solve the given goal, usually via an automatic solver.
+--   If the goal is discharged, return evidence for the goal.  Otherwise,
+--   the goal will be considered unsolvable.
+tacticSolve :: Monad m => (ProofGoal -> m (a, SolverStats, Maybe Evidence)) -> Tactic m a
+tacticSolve f = Tactic \gl ->
+  do (a, stats, me) <- f gl
+     case me of
+       Nothing -> return (a, stats, [gl], impossibleEvidence)
+       Just e  -> return (a, stats, [], leafEvidence e)
+
+-- | Attempt to simplify a proof goal via computation, rewriting or similar.
+--   The tactic should return a new proposition to prove and a method for
+--   transferring evidence for the modified proposition into a evidence for
+--   the original goal.
+tacticChange :: Monad m => (ProofGoal -> m (Prop, Evidence -> Evidence)) -> Tactic m ()
+tacticChange f = Tactic \gl ->
+  do (p, ef) <- f gl
+     return ((), mempty, [ gl{ goalProp = p } ], updateEvidence ef)
diff --git a/src/SAWScript/Prover/ABC.hs b/src/SAWScript/Prover/ABC.hs
index 932bee7285..f124205903 100644
--- a/src/SAWScript/Prover/ABC.hs
+++ b/src/SAWScript/Prover/ABC.hs
@@ -1,16 +1,40 @@
-module SAWScript.Prover.ABC (proveABC) where
+module SAWScript.Prover.ABC
+  ( proveABC
+  , w4AbcVerilog
+  , abcSatExternal
+  ) where
 
+import Control.Monad (unless)
+import Control.Monad.IO.Class
+import Data.Char (isSpace)
+import Data.List (isPrefixOf)
+import qualified Data.Map as Map
+import Data.Maybe
+import           Data.Set (Set)
+import qualified Data.Text as Text
+import Text.Read (readMaybe)
+
+import System.Directory
+import System.IO
+import System.IO.Temp (emptySystemTempFile)
+import System.Process (readProcessWithExitCode)
 
 import qualified Data.AIG as AIG
 
-import           Verifier.SAW.SharedTerm
 import           Verifier.SAW.FiniteValue
+import           Verifier.SAW.Name
+import           Verifier.SAW.SharedTerm
 import qualified Verifier.SAW.Simulator.BitBlast as BBSim
 
-import SAWScript.Proof(Prop, propToPredicate)
+import SAWScript.Proof(Prop, propToSATQuery, propSize, goalProp, ProofGoal, goalType, goalNum)
 import SAWScript.Prover.SolverStats (SolverStats, solverStats)
-import SAWScript.Prover.Util
-         (liftCexBB, bindAllExts)
+import qualified SAWScript.Prover.Exporter as Exporter
+import SAWScript.Prover.Util (liftCexBB)
+
+-- crucible-jvm
+-- TODO, very weird import
+import Lang.JVM.ProcessUtils (readProcessExitIfFailure)
+
 
 -- | Bit-blast a proposition and check its validity using ABC.
 proveABC ::
@@ -20,14 +44,13 @@ proveABC ::
   Prop ->
   IO (Maybe [(String, FirstOrderValue)], SolverStats)
 proveABC proxy sc goal =
-  do t0 <- propToPredicate sc goal
-     t <- bindAllExts sc t0
-     BBSim.withBitBlastedPred proxy sc mempty t $
-      \be lit0 shapes ->
-         do let lit = AIG.not lit0
-            satRes <- getModel (map fst shapes) (map snd shapes) =<< AIG.checkSat be lit
-            let stats = solverStats "ABC" (scSharedSize t0)
-            return (satRes, stats)
+  do satq <- propToSATQuery sc mempty goal
+     BBSim.withBitBlastedSATQuery proxy sc mempty satq $ \be lit shapes ->
+       do let (ecs,fts) = unzip shapes
+          let nms = map (Text.unpack . toShortName . ecName) ecs
+          res <- getModel nms fts =<< AIG.checkSat be lit
+          let stats = solverStats "ABC" (propSize goal)
+          return (res, stats)
 
 
 getModel ::
@@ -54,3 +77,115 @@ getModel argNames shapes satRes =
 
     AIG.SatUnknown -> fail "Unknown result from ABC"
 
+
+w4AbcVerilog :: MonadIO m =>
+  Set VarIndex ->
+  SharedContext ->
+  Bool ->
+  Prop ->
+  m (Maybe [(String, FirstOrderValue)], SolverStats)
+w4AbcVerilog unints sc _hashcons goal = liftIO $
+       -- Create temporary files
+    do let tpl = "abc_verilog.v"
+           tplCex = "abc_verilog.cex"
+       tmp <- emptySystemTempFile tpl
+       tmpCex <- emptySystemTempFile tplCex
+
+       satq <- propToSATQuery sc unints goal
+       (argNames, argTys) <- Exporter.writeVerilogSAT sc tmp satq
+
+       -- Run ABC and remove temporaries
+       let execName = "abc"
+           args = ["-q", "%read " ++ tmp ++"; %blast; &sweep -C 5000; &syn4; &cec -m; write_aiger_cex " ++ tmpCex]
+       (_out, _err) <- readProcessExitIfFailure execName args
+       cexText <- readFile tmpCex
+       removeFile tmp
+       removeFile tmpCex
+
+       -- Parse and report results
+       let stats = solverStats "abc_verilog" (propSize goal)
+       res <- if all isSpace cexText
+              then return Nothing
+                      -- NB: reverse bits to get bit-order convention right
+              else do bits <- reverse <$> parseAigerCex cexText
+                      case liftCexBB (reverse argTys) bits of
+                        Left parseErr -> fail parseErr
+                        Right vs -> return $ Just model
+                          where model = zip argNames (map toFirstOrderValue (reverse vs))
+       return (res, stats)
+
+parseAigerCex :: String -> IO [Bool]
+parseAigerCex text =
+  case lines text of
+    [_, cex] ->
+      case words cex of
+        [bits, _] -> mapM bitToBool bits
+        _ -> fail $ "invalid counterexample line: " ++ cex
+    _ -> fail $ "invalid counterexample text: " ++ text
+  where
+    bitToBool '0' = return False
+    bitToBool '1' = return True
+    bitToBool c   = fail ("invalid bit: " ++ [c])
+
+
+abcSatExternal :: MonadIO m =>
+  (AIG.IsAIG l g) =>
+  AIG.Proxy l g ->
+  SharedContext ->
+  Bool ->
+  String ->
+  [String] ->
+  ProofGoal ->
+  m (Maybe [(String,FirstOrderValue)], SolverStats)
+abcSatExternal proxy sc doCNF execName args g = liftIO $
+  do satq <- propToSATQuery sc mempty (goalProp g)
+     let cnfName = goalType g ++ show (goalNum g) ++ ".cnf"
+     (path, fh) <- openTempFile "." cnfName
+     hClose fh -- Yuck. TODO: allow writeCNF et al. to work on handles.
+
+     let args' = map replaceFileName args
+         replaceFileName "%f" = path
+         replaceFileName a = a
+
+     BBSim.withBitBlastedSATQuery proxy sc mempty satq $ \be l shapes -> do
+       variables <- (if doCNF then AIG.writeCNF else writeAIGWithMapping) be l path
+       (_ec, out, err) <- readProcessWithExitCode execName args' ""
+       removeFile path
+       unless (null err) $
+         print $ unlines ["Standard error from SAT solver:", err]
+       let ls = lines out
+           sls = filter ("s " `isPrefixOf`) ls
+           vls = filter ("v " `isPrefixOf`) ls
+       let stats = solverStats ("external SAT:" ++ execName) (propSize (goalProp g))
+       case (sls, vls) of
+         (["s SATISFIABLE"], _) -> do
+           let bs = parseDimacsSolution variables vls
+           let r = liftCexBB (map snd shapes) bs
+               argNames = map (Text.unpack . toShortName . ecName . fst) shapes
+           case r of
+             Left msg -> fail $ "Can't parse counterexample: " ++ msg
+             Right vs
+               | length argNames == length vs -> do
+                 return (Just (zip argNames (map toFirstOrderValue vs)), stats)
+               | otherwise -> fail $ unwords ["external SAT results do not match expected arguments", show argNames, show vs]
+         (["s UNSATISFIABLE"], []) ->
+           return (Nothing, stats)
+         _ -> fail $ "Unexpected result from SAT solver:\n" ++ out
+
+parseDimacsSolution :: [Int]    -- ^ The list of CNF variables to return
+                    -> [String] -- ^ The value lines from the solver
+                    -> [Bool]
+parseDimacsSolution vars ls = map lkup vars
+  where
+    vs :: [Int]
+    vs = concatMap (filter (/= 0) . mapMaybe readMaybe . tail . words) ls
+    varToPair n | n < 0 = (-n, False)
+                | otherwise = (n, True)
+    assgnMap = Map.fromList (map varToPair vs)
+    lkup v = Map.findWithDefault False v assgnMap
+
+writeAIGWithMapping :: AIG.IsAIG l g => g s -> l s -> FilePath -> IO [Int]
+writeAIGWithMapping be l path = do
+  nins <- AIG.inputCount be
+  AIG.writeAiger path (AIG.Network be [l])
+  return [1..nins]
diff --git a/src/SAWScript/Prover/Exporter.hs b/src/SAWScript/Prover/Exporter.hs
index 0dc93cddf2..89927d9b90 100644
--- a/src/SAWScript/Prover/Exporter.hs
+++ b/src/SAWScript/Prover/Exporter.hs
@@ -6,11 +6,12 @@
 {-# Language FlexibleContexts #-}
 {-# Language TypeApplications #-}
 module SAWScript.Prover.Exporter
-  ( proveWithExporter
-  , adaptExporter
+  ( proveWithSATExporter
+  , proveWithPropExporter
 
     -- * External formats
   , writeAIG
+  , writeAIG_SAT
   , writeSAIG
   , writeSAIGInferLatches
   , writeAIGComputedLatches
@@ -20,8 +21,6 @@ module SAWScript.Prover.Exporter
   , writeSMTLib2What4
   , write_smtlib2
   , write_smtlib2_w4
-  , writeUnintSMTLib2
-  , writeUnintSMTLib2What4
   , writeCoqCryptolPrimitivesForSAWCore
   , writeCoqCryptolModule
   , writeCoqSAWCorePrelude
@@ -29,6 +28,7 @@ module SAWScript.Prover.Exporter
   , writeCoqProp
   , writeCore
   , writeVerilog
+  , writeVerilogSAT
   , write_verilog
   , writeCoreProp
 
@@ -39,7 +39,7 @@ module SAWScript.Prover.Exporter
 import Data.Foldable(toList)
 
 import Control.Monad.Except (runExceptT, throwError)
-import Control.Monad.IO.Class (liftIO)
+import Control.Monad.IO.Class (liftIO, MonadIO)
 import qualified Data.AIG as AIG
 import qualified Data.ByteString as BS
 import Data.Parameterized.Nonce (globalNonceGenerator)
@@ -57,7 +57,8 @@ import Verifier.SAW.ExternalFormat(scWriteExternal)
 import Verifier.SAW.FiniteValue
 import Verifier.SAW.Module (emptyModule, moduleDecls)
 import Verifier.SAW.Prelude (preludeModule)
-import Verifier.SAW.Recognizer (asPi, asPiList, asEqTrue)
+import Verifier.SAW.Recognizer (asPi)
+import Verifier.SAW.SATQuery
 import Verifier.SAW.SharedTerm as SC
 import qualified Verifier.SAW.Translation.Coq as Coq
 import Verifier.SAW.TypedAST (mkModuleName)
@@ -65,54 +66,58 @@ import Verifier.SAW.TypedTerm
 import qualified Verifier.SAW.Simulator.BitBlast as BBSim
 import qualified Verifier.SAW.Simulator.Value as Sim
 import qualified Verifier.SAW.Simulator.What4 as W4Sim
+import qualified Verifier.SAW.Simulator.SBV as SBV
+import qualified Verifier.SAW.Simulator.What4 as W
 
 import qualified Verifier.SAW.UntypedAST as Un
 
 import SAWScript.Crucible.Common
-import SAWScript.Proof (Prop(..), predicateToProp, Quantification(..), propToPredicate)
+import SAWScript.Proof (Prop, propSize, propToTerm, predicateToSATQuery, propToSATQuery)
 import SAWScript.Prover.SolverStats
 import SAWScript.Prover.Util
 import SAWScript.Prover.What4
-import SAWScript.Prover.SBV (prepNegatedSBV)
 import SAWScript.Value
 
-import qualified What4.Interface as W4
 import qualified What4.Expr.Builder as W4
 import What4.Protocol.SMTLib2 (writeDefaultSMT2)
 import What4.Protocol.VerilogWriter (exprVerilog)
 import What4.Solver.Adapter
 import qualified What4.SWord as W4Sim
 
-proveWithExporter ::
-  (SharedContext -> FilePath -> Prop -> TopLevel ()) ->
+proveWithSATExporter ::
+  (SharedContext -> FilePath -> SATQuery -> TopLevel a) ->
+  Set VarIndex ->
   String ->
   Prop ->
   TopLevel SolverStats
-proveWithExporter exporter path goal =
+proveWithSATExporter exporter unintSet path goal =
   do sc <- getSharedContext
-     exporter sc path goal
-     let stats = solverStats ("offline: "++ path) (scSharedSize (unProp goal))
+     satq <- io $ propToSATQuery sc unintSet goal
+     _ <- exporter sc path satq
+     let stats = solverStats ("offline: "++ path) (propSize goal)
      return stats
 
--- | Converts an old-style exporter (which expects to take a predicate
--- as an argument) into a new-style one (which takes a pi-type proposition).
-adaptExporter ::
-  (SharedContext -> FilePath -> Term -> TopLevel ()) ->
-  (SharedContext -> FilePath -> Prop -> TopLevel ())
-adaptExporter exporter sc path (Prop goal) =
-  do let (args, concl) = asPiList goal
-     p <-
-       case asEqTrue concl of
-         Just p -> return p
-         Nothing -> throwTopLevel "adaptExporter: expected EqTrue"
-     p' <- io $ scNot sc p -- is this right?
-     t <- io $ scLambdaList sc args p'
-     exporter sc path t
+
+proveWithPropExporter ::
+  (SharedContext -> FilePath -> Prop -> TopLevel a) ->
+  String ->
+  Prop ->
+  TopLevel SolverStats
+proveWithPropExporter exporter path goal =
+  do sc <- getSharedContext
+     _ <- exporter sc path goal
+     let stats = solverStats ("offline: "++ path) (propSize goal)
+     return stats
 
 --------------------------------------------------------------------------------
 
--- | Write a @Term@ representing a theorem or an arbitrary
--- function to an AIG file.
+writeAIG_SAT :: (AIG.IsAIG l g) => AIG.Proxy l g -> SharedContext -> FilePath -> SATQuery -> TopLevel ()
+writeAIG_SAT proxy sc f satq = io $
+  do t  <- satQueryAsTerm sc satq
+     BBSim.withBitBlastedPred proxy sc mempty t $ \g l _vars -> do
+       AIG.writeAiger f (AIG.Network g [l])
+
+-- | Write a @Term@ representing a an arbitrary function to an AIG file.
 writeAIG :: (AIG.IsAIG l g) => AIG.Proxy l g -> SharedContext -> FilePath -> Term -> TopLevel ()
 writeAIG proxy sc f t = do
   io $ do
@@ -174,31 +179,18 @@ writeAIGComputedLatches ::
 writeAIGComputedLatches proxy sc file term numLatches =
   writeSAIG proxy sc file term numLatches
 
-writeCNF :: (AIG.IsAIG l g) => AIG.Proxy l g -> SharedContext -> FilePath -> Term -> TopLevel ()
-writeCNF proxy sc f t = do
-  AIG.Network be ls <- io $ bitblastPrim proxy sc t
-  case ls of
-    [l] -> do
-      _ <- io $ AIG.writeCNF be l f
-      return ()
-    _ -> throwTopLevel "writeCNF: non-boolean term"
+writeCNF :: (AIG.IsAIG l g) => AIG.Proxy l g -> SharedContext -> FilePath -> SATQuery -> TopLevel ()
+writeCNF proxy sc f satq = io $
+  do t  <- satQueryAsTerm sc satq
+     _ <- BBSim.withBitBlastedPred proxy sc mempty t $ \g l _vars -> AIG.writeCNF g l f
+     return ()
 
 write_cnf :: SharedContext -> FilePath -> TypedTerm -> TopLevel ()
 write_cnf sc f (TypedTerm schema t) = do
   liftIO $ checkBooleanSchema schema
   AIGProxy proxy <- getProxy
-  writeCNF proxy sc f t
-
--- | Write a proposition to an SMT-Lib version 2 file. Because @Prop@ is
--- assumed to have universally quantified variables, it will be negated.
-writeSMTLib2 :: SharedContext -> FilePath -> Prop -> TopLevel ()
-writeSMTLib2 sc f t = writeUnintSMTLib2 mempty sc f t
-
--- | Write a proposition to an SMT-Lib version 2 file. Because @Prop@ is
--- assumed to have universally quantified variables, it will be negated.
--- This version uses What4 instead of SBV.
-writeSMTLib2What4 :: SharedContext -> FilePath -> Prop -> TopLevel ()
-writeSMTLib2What4 sc f t = writeUnintSMTLib2What4 mempty sc f t
+  satq <- io (predicateToSATQuery sc mempty t)
+  writeCNF proxy sc f satq
 
 -- | Write a @Term@ representing a predicate (i.e. a monomorphic
 -- function returning a boolean) to an SMT-Lib version 2 file. The goal
@@ -207,8 +199,8 @@ writeSMTLib2What4 sc f t = writeUnintSMTLib2What4 mempty sc f t
 write_smtlib2 :: SharedContext -> FilePath -> TypedTerm -> TopLevel ()
 write_smtlib2 sc f (TypedTerm schema t) = do
   io $ checkBooleanSchema schema
-  p <- io $ predicateToProp sc Existential [] t
-  writeSMTLib2 sc f p
+  satq <- io $ predicateToSATQuery sc mempty t
+  writeSMTLib2 sc f satq
 
 -- | Write a @Term@ representing a predicate (i.e. a monomorphic
 -- function returning a boolean) to an SMT-Lib version 2 file. The goal
@@ -217,29 +209,23 @@ write_smtlib2 sc f (TypedTerm schema t) = do
 write_smtlib2_w4 :: SharedContext -> FilePath -> TypedTerm -> TopLevel ()
 write_smtlib2_w4 sc f (TypedTerm schema t) = do
   io $ checkBooleanSchema schema
-  p <- io $ predicateToProp sc Existential [] t
-  writeUnintSMTLib2What4 mempty sc f p
-
--- | Write a proposition to an SMT-Lib version 2 file, treating some
--- constants as uninterpreted. Because @Prop@ is assumed to have
--- universally quantified variables, it will be negated.
-writeUnintSMTLib2 :: Set VarIndex -> SharedContext -> FilePath -> Prop -> TopLevel ()
-writeUnintSMTLib2 unintSet sc f p = io $
-  do (_, _, l) <- prepNegatedSBV sc unintSet p
+  satq <- io $ predicateToSATQuery sc mempty t
+  writeSMTLib2What4 sc f satq
+
+-- | Write a SAT query to an SMT-Lib version 2 file.
+writeSMTLib2 :: SharedContext -> FilePath -> SATQuery -> TopLevel ()
+writeSMTLib2 sc f satq = io $
+  do (_, _, l) <- SBV.sbvSATQuery sc mempty satq
      let isSat = True -- l is encoded as an existential formula
      txt <- SBV.generateSMTBenchmark isSat l
      writeFile f txt
 
--- | Write a proposition to an SMT-Lib version 2 file, treating some
--- constants as uninterpreted. Because @Prop@ is assumed to have
--- universally quantified variables, it will be negated. This version
--- uses What4 instead of SBV.
-writeUnintSMTLib2What4 :: Set VarIndex -> SharedContext -> FilePath -> Prop -> TopLevel ()
-writeUnintSMTLib2What4 unints sc f goal = io $
+-- | Write a SAT query an SMT-Lib version 2 file.
+-- This version uses What4 instead of SBV.
+writeSMTLib2What4 :: SharedContext -> FilePath -> SATQuery -> TopLevel ()
+writeSMTLib2What4 sc f satq = io $
   do sym <- W4.newExprBuilder W4.FloatRealRepr St globalNonceGenerator
-     term <- propToPredicate sc goal
-     (_, _, (_,lit0)) <- prepWhat4 sym sc unints term
-     lit <- W4.notPred sym lit0 -- for symmetry with `prepNegatedSBV` above
+     (_argNames, _argTys, _labels, lit) <- W.w4Solve sym sc satq
      withFile f WriteMode $ \h ->
        writeDefaultSMT2 () "Offline SMTLib2" defaultWriteSMTLIB2Features sym h [lit]
 
@@ -249,6 +235,25 @@ writeCore path t = io $ writeFile path (scWriteExternal t)
 write_verilog :: SharedContext -> FilePath -> Term -> TopLevel ()
 write_verilog sc path t = io $ writeVerilog sc path t
 
+writeVerilogSAT :: MonadIO m => SharedContext -> FilePath -> SATQuery -> m ([String],[FiniteType])
+writeVerilogSAT sc path satq = liftIO $
+  do sym <- newSAWCoreBackend sc
+     (argNames, argTys, _lbls, bval) <- W.w4Solve sym sc satq
+     let f fot = case toFiniteType fot of
+                   Nothing -> fail $ "writeVerilogSAT: Unsupported argument type " ++ show fot
+                   Just ft -> return ft
+     argTys' <- traverse f argTys
+
+     edoc <- runExceptT $ exprVerilog sym bval "f"
+     case edoc of
+       Left err -> fail $ "Failed to translate to Verilog: " ++ err
+       Right doc -> do
+         h <- openFile path WriteMode
+         hPutDoc h doc
+         hPutStrLn h ""
+         hClose h
+     return (argNames, argTys')
+
 writeVerilog :: SharedContext -> FilePath -> Term -> IO ()
 writeVerilog sc path t = do
   sym <- newSAWCoreBackend sc
@@ -268,7 +273,10 @@ writeVerilog sc path t = do
       hClose h
 
 writeCoreProp :: FilePath -> Prop -> TopLevel ()
-writeCoreProp path (Prop t) = io $ writeFile path (scWriteExternal t)
+writeCoreProp path t =
+  do sc <- getSharedContext
+     tm <- io (propToTerm sc t)
+     io $ writeFile path (scWriteExternal tm)
 
 coqTranslationConfiguration ::
   [(String, String)] ->
@@ -303,8 +311,10 @@ writeCoqProp ::
   FilePath ->
   Prop ->
   TopLevel ()
-writeCoqProp name notations skips path (Prop t) =
-  writeCoqTerm name notations skips path t
+writeCoqProp name notations skips path t =
+  do sc <- getSharedContext
+     tm <- io (propToTerm sc t)
+     writeCoqTerm name notations skips path tm
 
 writeCoqCryptolModule ::
   FilePath ->
diff --git a/src/SAWScript/Prover/MRSolver.hs b/src/SAWScript/Prover/MRSolver.hs
index 6519559bf3..db4d3254d2 100644
--- a/src/SAWScript/Prover/MRSolver.hs
+++ b/src/SAWScript/Prover/MRSolver.hs
@@ -21,7 +21,7 @@ import Verifier.SAW.Term.Functor
 import Verifier.SAW.SharedTerm
 import Verifier.SAW.Recognizer
 
-import SAWScript.Proof (Prop(..))
+import SAWScript.Proof (predicateToProp, Quantification(..))
 import qualified SAWScript.Prover.SBV as SBV
 
 import Prelude
@@ -280,8 +280,9 @@ mrProvable bool_prop =
      timeout <- mrSMTTimeout <$> get
      path_prop <- mrPathCondition <$> get
      bool_prop' <- liftSC2 scImplies path_prop bool_prop
-     prop <- liftSC1 scEqTrue bool_prop'
-     (smt_res, _) <- liftSC1 (SBV.proveUnintSBV smt_conf mempty timeout) (Prop prop)
+     sc <- mrSC <$> get
+     prop <- liftIO (predicateToProp sc Universal bool_prop')
+     (smt_res, _) <- liftSC1 (SBV.proveUnintSBV smt_conf mempty timeout) prop
      case smt_res of
        Just _ -> return False
        Nothing -> return True
diff --git a/src/SAWScript/Prover/RME.hs b/src/SAWScript/Prover/RME.hs
index 220c0f26a5..cd9aea4e04 100644
--- a/src/SAWScript/Prover/RME.hs
+++ b/src/SAWScript/Prover/RME.hs
@@ -5,13 +5,13 @@ import qualified Data.Text as Text
 
 import qualified Data.RME as RME
 
+import Verifier.SAW.Name
 import Verifier.SAW.SharedTerm
 import Verifier.SAW.FiniteValue
 
 import qualified Verifier.SAW.Simulator.RME as RME
-import Verifier.SAW.Recognizer(asPiList)
 
-import SAWScript.Proof(Prop, propToPredicate)
+import SAWScript.Proof(Prop, propToSATQuery, propSize)
 import SAWScript.Prover.SolverStats
 import SAWScript.Prover.Util
 
@@ -21,25 +21,20 @@ proveRME ::
   Prop          {- ^ A proposition to be proved -} ->
   IO (Maybe [(String, FirstOrderValue)], SolverStats)
 proveRME sc goal =
-  do t0 <- propToPredicate sc goal
-     t <- bindAllExts sc t0
-     tp <- scWhnf sc =<< scTypeOf sc t
-     let (args, _) = asPiList tp
-         argNames = map (Text.unpack . fst) args
-     RME.withBitBlastedPred sc Map.empty t $ \lit0 shapes ->
-       let lit = RME.compl lit0
-           stats = solverStats "RME" (scSharedSize t0)
+  do satq <- propToSATQuery sc mempty goal
+     RME.withBitBlastedSATQuery sc Map.empty satq $ \lit shapes ->
+       let stats = solverStats "RME" (propSize goal)
        in case RME.sat lit of
             Nothing -> return (Nothing, stats)
             Just cex -> do
               let m = Map.fromList cex
-              let n = sum (map sizeFiniteType shapes)
+              let n = sum (map (sizeFiniteType . snd) shapes)
               let bs = map (maybe False id . flip Map.lookup m) $ take n [0..]
-              let r = liftCexBB shapes bs
+              let r = liftCexBB (map snd shapes) bs
               case r of
                 Left err -> fail $ "Can't parse counterexample: " ++ err
                 Right vs
-                  | length argNames == length vs -> do
-                    let model = zip argNames (map toFirstOrderValue vs)
+                  | length shapes == length vs -> do
+                    let model = zip (map (Text.unpack . toShortName . ecName . fst) shapes) (map toFirstOrderValue vs)
                     return (Just model, stats)
-                  | otherwise -> fail $ unwords ["RME SAT results do not match expected arguments", show argNames, show vs]
+                  | otherwise -> fail $ unwords ["RME SAT results do not match expected arguments", show shapes, show vs]
diff --git a/src/SAWScript/Prover/SBV.hs b/src/SAWScript/Prover/SBV.hs
index e063090203..2205896afd 100644
--- a/src/SAWScript/Prover/SBV.hs
+++ b/src/SAWScript/Prover/SBV.hs
@@ -8,11 +8,8 @@ module SAWScript.Prover.SBV
 import System.Directory
 
 import           Data.Maybe
-import           Data.Map ( Map )
-import qualified Data.Map as Map
 import           Data.Set ( Set )
 import qualified Data.Text as Text
-import qualified Data.Vector as V
 import           Control.Monad
 
 import qualified Data.SBV.Dynamic as SBV
@@ -22,12 +19,10 @@ import qualified Verifier.SAW.Simulator.SBV as SBVSim
 
 import Verifier.SAW.SharedTerm
 import Verifier.SAW.FiniteValue
-import Verifier.SAW.Recognizer(asPi, asPiList)
 
-import SAWScript.Proof(Prop, propToPredicate)
+import SAWScript.Proof(Prop, propSize, propToSATQuery)
 import SAWScript.Prover.SolverStats
 
-
 -- | Bit-blast a proposition and check its validity using SBV.
 -- Constants with names in @unints@ are kept as uninterpreted
 -- functions.
@@ -39,7 +34,7 @@ proveUnintSBV ::
   Prop          {- ^ A proposition to be proved -} ->
   IO (Maybe [(String, FirstOrderValue)], SolverStats)
     -- ^ (example/counter-example, solver statistics)
-proveUnintSBV conf unintSet timeout sc term =
+proveUnintSBV conf unintSet timeout sc goal =
   do p <- findExecutable . SBV.executable $ SBV.solver conf
      unless (isJust p) . fail $ mconcat
        [ "Unable to locate the executable \""
@@ -48,93 +43,39 @@ proveUnintSBV conf unintSet timeout sc term =
        , show . SBV.name $ SBV.solver conf
        ]
 
-     (t', mlabels, lit) <- prepNegatedSBV sc unintSet term
+     (labels, argNames, lit) <- prepNegatedSBV sc unintSet goal
 
-     tp <- scWhnf sc =<< scTypeOf sc t'
-     let (args, _) = asPiList tp
-         (labels, argNames) = unzip [ (l, n) | (Just l, n) <- zip mlabels (map fst args) ]
+     let script = maybe (return ()) SBV.setTimeOut timeout >> lit
 
-         script = do
-           maybe (return ()) SBV.setTimeOut timeout
-           lit
      SBV.SatResult r <- SBV.satWith conf script
 
      let stats = solverStats ("SBV->" ++ show (SBV.name (SBV.solver conf)))
-                             (scSharedSize t')
+                             (propSize goal)
      case r of
+       SBV.Unsatisfiable {} -> return (Nothing, stats)
 
        SBV.Satisfiable {} ->
          do let dict = SBV.getModelDictionary r
-                r'   = getLabels labels dict (map Text.unpack argNames)
+                r'   = SBVSim.getLabels labels dict (map Text.unpack argNames)
             return (r', stats)
 
        SBV.SatExtField {} -> fail "Prover returned model in extension field"
 
-       SBV.Unsatisfiable {} -> return (Nothing, stats)
-
        SBV.Unknown {} -> fail "Prover returned Unknown"
 
        SBV.ProofError _ ls _ -> fail . unlines $ "Prover returned error: " : ls
 
+
 -- | Convert a saw-core proposition to a logically-negated SBV
 -- symbolic boolean formula with existentially quantified variables.
 -- The returned formula is suitable for checking satisfiability. The
 -- specified function names are left uninterpreted.
+
 prepNegatedSBV ::
   SharedContext ->
   Set VarIndex {- ^ Uninterpreted function names -} ->
   Prop     {- ^ Proposition to prove -} ->
-  IO (Term, [Maybe SBVSim.Labeler], SBV.Symbolic SBV.SVal)
+  IO ([SBVSim.Labeler], [Text.Text], SBV.Symbolic SBV.SVal)
 prepNegatedSBV sc unintSet goal =
-  do t0 <- propToPredicate sc goal
-     -- Abstract over all non-function ExtCns variables
-     let nonFun e = fmap ((== Nothing) . asPi) (scWhnf sc (ecType e))
-     exts <- filterM nonFun (getAllExts t0)
-
-     t' <- scAbstractExts sc exts t0
-
-     (labels, lit) <- SBVSim.sbvSolve sc mempty unintSet t'
-     let lit' = liftM SBV.svNot lit
-     return (t', labels, lit')
-
-
-
-
-getLabels ::
-  [SBVSim.Labeler] ->
-  Map String SBV.CV ->
-  [String] -> Maybe [(String,FirstOrderValue)]
-
-getLabels ls d argNames
-  | length argNames == length xs = Just (zip argNames xs)
-  | otherwise = error $ unwords
-                [ "SBV SAT results do not match expected arguments "
-                , show argNames, show xs]
-
-  where
-  xs = fmap getLabel ls
-
-  getLabel (SBVSim.BoolLabel s)    = FOVBit (SBV.cvToBool (d Map.! s))
-  getLabel (SBVSim.IntegerLabel s) = FOVInt (cvToInteger (d Map.! s))
-
-  getLabel (SBVSim.WordLabel s)    = FOVWord (cvKind cv) (cvToInteger cv)
-    where cv = d Map.! s
-
-  getLabel (SBVSim.VecLabel ns)
-    | V.null ns = error "getLabel of empty vector"
-    | otherwise = fovVec t vs
-    where vs = map getLabel (V.toList ns)
-          t  = firstOrderTypeOf (head vs)
-
-  getLabel (SBVSim.TupleLabel ns) = FOVTuple $ map getLabel (V.toList ns)
-  getLabel (SBVSim.RecLabel ns) = FOVRec $ fmap getLabel ns
-
-  cvKind cv =
-    case SBV.kindOf cv of
-      SBV.KBounded _ k -> fromIntegral k
-      _                -> error "cvKind"
-
-  cvToInteger cv =
-    case SBV.cvVal cv of
-      SBV.CInteger i -> i
-      _               -> error "cvToInteger"
+  do satq <- propToSATQuery sc unintSet goal
+     SBVSim.sbvSATQuery sc mempty satq
diff --git a/src/SAWScript/Prover/What4.hs b/src/SAWScript/Prover/What4.hs
index 6a12955cdd..aea7999a7d 100644
--- a/src/SAWScript/Prover/What4.hs
+++ b/src/SAWScript/Prover/What4.hs
@@ -9,15 +9,11 @@ module SAWScript.Prover.What4 where
 import System.IO
 
 import           Data.Set (Set)
-import           Control.Monad(filterM)
-import           Data.Maybe (catMaybes)
 
 import Verifier.SAW.SharedTerm
 import Verifier.SAW.FiniteValue
 
-import Verifier.SAW.Recognizer(asPi)
-
-import           SAWScript.Proof(Prop, propToPredicate)
+import           SAWScript.Proof(Prop, propToSATQuery, propSize)
 import           SAWScript.Prover.SolverStats
 
 import Data.Parameterized.Nonce
@@ -119,26 +115,24 @@ setupWhat4_solver :: forall st t ff.
   SharedContext      {- ^ Context for working with terms -} ->
   Prop               {- ^ A proposition to be proved/checked. -} ->
   IO ( [String]
-     , [Maybe (W.Labeler (B.ExprBuilder t st ff))]
+     , [W.Labeler (B.ExprBuilder t st ff)]
      , Pred (B.ExprBuilder t st ff)
      , SolverStats)
 setupWhat4_solver solver sym unintSet sc goal =
   do
-     -- convert goal to lambda term
-     term <- propToPredicate sc goal
      -- symbolically evaluate
-     (t', argNames, (bvs,lit0)) <- prepWhat4 sym sc unintSet term
-
-     lit <- notPred sym lit0
+     satq <- propToSATQuery sc unintSet goal
+     (argNames, _argTys, bvs, lit) <- W.w4Solve sym sc satq
 
      extendConfig (solver_adapter_config_options solver)
                   (getConfiguration sym)
 
      let stats = solverStats ("W4 ->" ++ solver_adapter_name solver)
-                             (scSharedSize t')
+                             (propSize goal)
 
      return (argNames, bvs, lit, stats)
 
+
 -- | Check the validity of a proposition using What4.
 proveWhat4_solver :: forall st t ff.
   SolverAdapter st   {- ^ Which solver to use -} ->
@@ -162,34 +156,19 @@ proveWhat4_solver solver sym unintSet sc goal =
          Sat (gndEvalFcn,_) -> do
            mvals <- mapM (getValues @(B.ExprBuilder t st ff) gndEvalFcn)
                          (zip bvs argNames)
-           return (Just (catMaybes mvals), stats) where
+           return (Just mvals, stats) where
 
          Unsat _ -> return (Nothing, stats)
 
          Unknown -> fail "Prover returned Unknown"
 
 
-prepWhat4 ::
-  forall sym. (IsSymExprBuilder sym) =>
-  sym -> SharedContext -> Set VarIndex -> Term ->
-  IO (Term, [String], ([Maybe (W.Labeler sym)], Pred sym))
-prepWhat4 sym sc unintSet t0 = do
-  -- Abstract over all non-function ExtCns variables
-  let nonFun e = fmap ((== Nothing) . asPi) (scWhnf sc (ecType e))
-  exts <- filterM nonFun (getAllExts t0)
-
-  t' <- scAbstractExts sc exts t0
-
-  (argNames, lit) <- W.w4Solve sym sc mempty unintSet t'
-  return (t', argNames, lit)
-
 
 getValues :: forall sym gt. (SymExpr sym ~ B.Expr gt) => GroundEvalFn gt ->
-  (Maybe (W.Labeler sym), String) -> IO (Maybe (String, FirstOrderValue))
-getValues _ (Nothing, _) = return Nothing
-getValues f (Just labeler, orig) = do
+  (W.Labeler sym, String) -> IO (String, FirstOrderValue)
+getValues f (labeler, orig) = do
   fov <- W.getLabelValues f labeler
-  return $ Just (orig,fov)
+  return (orig, fov)
 
 
 -- | For debugging
diff --git a/src/SAWScript/Value.hs b/src/SAWScript/Value.hs
index 2598c73f91..2379ec13f3 100644
--- a/src/SAWScript/Value.hs
+++ b/src/SAWScript/Value.hs
@@ -280,9 +280,9 @@ showsPrecValue opts p v =
     VTopLevel {} -> showString "<<TopLevel>>"
     VSimpset ss -> showString (showSimpset opts ss)
     VProofScript {} -> showString "<<proof script>>"
-    VTheorem (Theorem (Prop t) _stats) ->
+    VTheorem thm ->
       showString "Theorem " .
-      showParen True (showString (SAWCorePP.scPrettyTerm opts' t))
+      showParen True (showString (prettyProp opts' (thmProp thm)))
     VLLVMCrucibleSetup{} -> showString "<<Crucible Setup>>"
     VLLVMCrucibleSetupValue{} -> showString "<<Crucible SetupValue>>"
     VLLVMCrucibleMethodSpec{} -> showString "<<Crucible MethodSpec>>"
@@ -334,7 +334,7 @@ tupleLookupValue _ _ = error "tupleLookupValue"
 
 evaluate :: SharedContext -> Term -> IO Concrete.CValue
 evaluate sc t =
-  (\modmap -> Concrete.evalSharedTerm modmap mempty t) <$>
+  (\modmap -> Concrete.evalSharedTerm modmap mempty mempty t) <$>
   scGetModuleMap sc
 
 evaluateTypedTerm :: SharedContext -> TypedTerm -> IO C.Value
diff --git a/src/SAWScript/VerificationSummary.hs b/src/SAWScript/VerificationSummary.hs
index 9a3995ebcd..56f96411ee 100644
--- a/src/SAWScript/VerificationSummary.hs
+++ b/src/SAWScript/VerificationSummary.hs
@@ -50,7 +50,7 @@ vsVerifSolvers vs =
 
 vsTheoremSolvers :: VerificationSummary -> Set.Set String
 vsTheoremSolvers = Set.unions . map getSolvers . vsTheorems
-  where getSolvers (Theorem _ ss) = solverStatsSolvers ss
+  where getSolvers thm = solverStatsSolvers (thmStats thm)
 
 vsAllSolvers :: VerificationSummary -> Set.Set String
 vsAllSolvers vs = Set.union (vsVerifSolvers vs) (vsTheoremSolvers vs)
@@ -73,7 +73,7 @@ thmToJSON thm = object [
     ("type" .= ("property" :: String))
     , ("loc" .= ("unknown" :: String)) -- TODO: Theorem has no attached location information
     , ("status" .= (statusString $ thmStats thm))
-    , ("term" .= (show $ PP.ppTerm PP.defaultPPOpts $ unProp $ thmProp thm))
+    , ("term" .= (show $ ppProp PP.defaultPPOpts $ thmProp thm))
   ]
 
 statusString :: SolverStats -> String
@@ -134,7 +134,7 @@ prettyVerificationSummary vs@(VerificationSummary jspecs lspecs thms) =
         vsep [ if Set.null (solverStatsSolvers (thmStats t))
                then "Axiom:"
                else "Theorem:"
-             , code (indent 2 (PP.ppTerm PP.defaultPPOpts (unProp (thmProp t))))
+             , code (indent 2 (ppProp PP.defaultPPOpts (thmProp t)))
              , ""
              ]
       prettySolvers ss =
diff --git a/src/SAWScript/X86.hs b/src/SAWScript/X86.hs
index 432e6263de..2400bf4086 100644
--- a/src/SAWScript/X86.hs
+++ b/src/SAWScript/X86.hs
@@ -540,7 +540,7 @@ data Goal = Goal
 
 -- | The proposition that needs proving (i.e., assumptions imply conclusion)
 gGoal :: SharedContext -> Goal -> IO Prop
-gGoal sc g0 = predicateToProp sc Universal [] =<< go (gAssumes g)
+gGoal sc g0 = predicateToProp sc Universal =<< go (gAssumes g)
   where
   g = g0 { gAssumes = mapMaybe skip (gAssumes g0) }