From 7a63664df22eb6b12e732d7789ac9e5627366f56 Mon Sep 17 00:00:00 2001
From: Mate Soos <mate.soos@ethereum.org>
Date: Wed, 6 Sep 2023 15:44:31 +0200
Subject: [PATCH 01/12] The SMT2 file ought to be printed while executing it

---
 src/EVM/Fetch.hs   |  4 ++--
 src/EVM/Solvers.hs | 23 +++++++++++++++++------
 src/EVM/SymExec.hs | 29 +++++++++++------------------
 test/test.hs       |  7 ++++---
 4 files changed, 34 insertions(+), 29 deletions(-)

diff --git a/src/EVM/Fetch.hs b/src/EVM/Fetch.hs
index 4f61a3560..431a14de8 100644
--- a/src/EVM/Fetch.hs
+++ b/src/EVM/Fetch.hs
@@ -238,13 +238,13 @@ type Fetcher s = Query s -> IO (EVM s ())
 -- will be pruned anyway.
 checkBranch :: SolverGroup -> Prop -> Prop -> IO BranchCondition
 checkBranch solvers branchcondition pathconditions = do
-  checkSat solvers (assertProps abstRefineDefault [(branchcondition .&& pathconditions)]) >>= \case
+  checkSat solvers (assertProps abstRefineDefault [(branchcondition .&& pathconditions)]) Nothing >>= \case
     -- the condition is unsatisfiable
     Unsat -> -- if pathconditions are consistent then the condition must be false
       pure $ Case False
     -- Sat means its possible for condition to hold
     Sat _ -> -- is its negation also possible?
-      checkSat solvers (assertProps abstRefineDefault [(pathconditions .&& (PNeg branchcondition))]) >>= \case
+      checkSat solvers (assertProps abstRefineDefault [(pathconditions .&& (PNeg branchcondition))]) Nothing >>= \case
         -- No. The condition must hold
         Unsat -> pure $ Case True
         -- Yes. Both branches possible
diff --git a/src/EVM/Solvers.hs b/src/EVM/Solvers.hs
index 310f1743f..e78c95b6e 100644
--- a/src/EVM/Solvers.hs
+++ b/src/EVM/Solvers.hs
@@ -15,7 +15,7 @@ import Control.Monad.State.Strict
 import Data.Char (isSpace)
 import Data.Map (Map)
 import Data.Map qualified as Map
-import Data.Maybe (fromMaybe)
+import Data.Maybe (fromMaybe, isJust, fromJust)
 import Data.Text qualified as TS
 import Data.Text.Lazy (Text)
 import Data.Text.Lazy qualified as T
@@ -57,6 +57,7 @@ newtype SolverGroup = SolverGroup (Chan Task)
 data Task = Task
   { script :: SMT2
   , resultChan :: Chan CheckSatResult
+  , debugFName :: Maybe String
   }
 
 -- | The result of a call to (check-sat)
@@ -79,15 +80,21 @@ isUnsat :: CheckSatResult -> Bool
 isUnsat Unsat = True
 isUnsat _ = False
 
-checkSat :: SolverGroup -> SMT2 -> IO CheckSatResult
-checkSat (SolverGroup taskQueue) script = do
+checkSat :: SolverGroup -> SMT2 -> Maybe String -> IO CheckSatResult
+checkSat (SolverGroup taskQueue) script debugFName = do
   -- prepare result channel
   resChan <- newChan
   -- send task to solver group
-  writeChan taskQueue (Task script resChan)
+  writeChan taskQueue (Task script resChan debugFName)
   -- collect result
   readChan resChan
 
+writeSMT2File :: SMT2 -> Maybe String -> String -> IO ()
+writeSMT2File smt2 fname abst =
+  when (isJust fname) $
+  do T.writeFile (fromJust fname <> "-" <> abst <> ".smt2")
+      ("; " <> formatSMT2 smt2 <> "\n\n(check-sat)")
+
 withSolvers :: Solver -> Natural -> Maybe Natural -> (SolverGroup -> IO a) -> IO a
 withSolvers solver count timeout cont = do
   -- spawn solvers
@@ -106,13 +113,15 @@ withSolvers solver count timeout cont = do
   killThread orchestrateId
   pure res
   where
+    orchestrate :: Chan Task -> Chan SolverInstance -> IO b
     orchestrate queue avail = do
       task <- readChan queue
       inst <- readChan avail
       _ <- forkIO $ runTask task inst avail
       orchestrate queue avail
 
-    runTask (Task (SMT2 cmds (RefinementEqs refineEqs) cexvars) r) inst availableInstances = do
+    runTask (Task smt2@(SMT2 cmds (RefinementEqs refineEqs) cexvars) r debugFName) inst availableInstances = do
+      writeSMT2File smt2 debugFName ("abstracted")
       -- reset solver and send all lines of provided script
       out <- sendScript inst (SMT2 ("(reset)" : cmds) mempty mempty)
       case out of
@@ -128,7 +137,9 @@ withSolvers solver count timeout cont = do
                 "unknown" -> pure Unknown
                 "sat" -> if null refineEqs then Sat <$> getModel inst cexvars
                          else do
-                              _ <- sendScript inst (SMT2 refineEqs mempty mempty)
+                              let refinedSMT2 = SMT2 refineEqs mempty mempty
+                              writeSMT2File refinedSMT2 debugFName ("refined")
+                              _ <- sendScript inst refinedSMT2
                               sat2 <- sendLine inst "(check-sat)"
                               case sat2 of
                                 "unsat" -> pure Unsat
diff --git a/src/EVM/SymExec.hs b/src/EVM/SymExec.hs
index 5a02a45d9..ea1c6aa01 100644
--- a/src/EVM/SymExec.hs
+++ b/src/EVM/SymExec.hs
@@ -24,8 +24,6 @@ import Data.Set qualified as Set
 import Data.Text (Text)
 import Data.Text qualified as T
 import Data.Text.IO qualified as T
-import Data.Text.Lazy qualified as TL
-import Data.Text.Lazy.IO qualified as TL
 import Data.Tree.Zipper qualified as Zipper
 import Data.Tuple (swap)
 import EVM (makeVm, abstractContract, initialContract, getCodeLocation, isValidJumpDest)
@@ -34,7 +32,7 @@ import EVM.Fetch qualified as Fetch
 import EVM.ABI
 import EVM.Expr qualified as Expr
 import EVM.Format (formatExpr, formatPartial)
-import EVM.SMT (SMTCex(..), SMT2(..), assertProps, formatSMT2)
+import EVM.SMT (SMTCex(..), SMT2(..), assertProps)
 import EVM.SMT qualified as SMT
 import EVM.Solvers
 import EVM.Stepper (Stepper)
@@ -512,7 +510,7 @@ reachable solvers e = do
         pure (fst tres <> fst fres, subexpr)
       leaf -> do
         let query = assertProps abstRefineDefault pcs
-        res <- checkSat solvers query
+        res <- checkSat solvers query Nothing
         case res of
           Sat _ -> pure ([query], Just leaf)
           Unsat -> pure ([query], Nothing)
@@ -578,18 +576,14 @@ verify solvers opts preState maybepost = do
         assumes = preState.constraints
         withQueries = canViolate <&> \leaf ->
           (assertProps opts.abstRefineConfig (PNeg (post preState leaf) : assumes <> extractProps leaf), leaf)
+        debugFName = if opts.debug then Just ("verify-query") else Nothing
       putStrLn $ "Checking for reachability of "
                    <> show (length withQueries)
                    <> " potential property violation(s)"
 
-      when opts.debug $ forM_ (zip [(1 :: Int)..] withQueries) $ \(idx, (q, leaf)) -> do
-        TL.writeFile
-          ("query-" <> show idx <> ".smt2")
-          ("; " <> (TL.pack $ show leaf) <> "\n\n" <> formatSMT2 q <> "\n\n(check-sat)")
-
       -- Dispatch the remaining branches to the solver to check for violations
       results <- flip mapConcurrently withQueries $ \(query, leaf) -> do
-        res <- checkSat solvers query
+        res <- checkSat solvers query debugFName
         pure (res, leaf)
       let cexs = filter (\(res, _) -> not . isUnsat $ res) results
       pure $ if Prelude.null cexs then (expr, [Qed ()]) else (expr, fmap toVRes cexs)
@@ -689,15 +683,14 @@ equivalenceCheck' solvers branchesA branchesB opts = do
     -- used or not
     check :: UnsatCache -> (Set Prop) -> Int -> IO (EquivResult, Bool)
     check knownUnsat props idx = do
-      let smt = assertProps opts.abstRefineConfig (Set.toList props)
-      -- if debug is on, write the query to a file
-      let filename = "equiv-query-" <> show idx <> ".smt2"
-      when opts.debug $ TL.writeFile filename (formatSMT2 smt <> "\n\n(check-sat)")
-
+      let
+        smt = assertProps opts.abstRefineConfig (Set.toList props)
+        debugFName = if opts.debug then Just "equiv-query"
+                                   else Nothing
       ku <- readTVarIO knownUnsat
       res <- if subsetAny props ku
              then pure (True, Unsat)
-             else (fmap ((False),) (checkSat solvers smt))
+             else (fmap ((False),) (checkSat solvers smt debugFName))
       case res of
         (_, Sat x) -> pure (Cex x, False)
         (quick, Unsat) ->
@@ -709,7 +702,7 @@ equivalenceCheck' solvers branchesA branchesB opts = do
               atomically $ readTVar knownUnsat >>= writeTVar knownUnsat . (props :)
               pure (Qed (), False)
         (_, EVM.Solvers.Unknown) -> pure (Timeout (), False)
-        (_, Error txt) -> internalError $ "solver returned: " <> (T.unpack txt) <> if opts.debug then "\n SMT file was: " <> filename <> "" else ""
+        (_, Error txt) -> internalError $ "solver returned: " <> (T.unpack txt)
 
     -- Allows us to run it in parallel. Note that this (seems to) run it
     -- from left-to-right, and with a max of K threads. This is in contrast to
@@ -790,7 +783,7 @@ produceModels solvers expr = do
   let flattened = flattenExpr expr
       withQueries = fmap (\e -> ((assertProps abstRefineDefault) . extractProps $ e, e)) flattened
   results <- flip mapConcurrently withQueries $ \(query, leaf) -> do
-    res <- checkSat solvers query
+    res <- checkSat solvers query Nothing
     pure (res, leaf)
   pure $ fmap swap $ filter (\(res, _) -> not . isUnsat $ res) results
 
diff --git a/test/test.hs b/test/test.hs
index e6c2cd279..4251bd139 100644
--- a/test/test.hs
+++ b/test/test.hs
@@ -1723,7 +1723,7 @@ tests = testGroup "hevm"
               }
             }
             |]
-        (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint16)" [AbiUIntType 16])) [] defaultVeriOpts
+        (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint16)" [AbiUIntType 16])) [] debugVeriOpts
         putStrLn "DIV by zero is zero"
       ,
       -- Somewhat tautological since we are asserting the precondition
@@ -1952,7 +1952,7 @@ tests = testGroup "hevm"
               }
              }
             |]
-          (_, [Cex (_, a), Cex (_, b)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
+          (_, [Cex (_, a), Cex (_, b)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] debugVeriOpts
           let ints = map (flip getVar "arg1") [a,b]
           assertBool "0 must be one of the Cex-es" $ isJust $ List.elemIndex 0 ints
           putStrLn "expected 2 counterexamples found, one Cex is the 0 value"
@@ -3046,7 +3046,8 @@ checkEquivBase mkprop l r = withSolvers Z3 1 (Just 1) $ \solvers -> do
        pure True
      else do
        let smt = assertPropsNoSimp abstRefineDefault [mkprop l r]
-       res <- checkSat solvers smt
+       let smt = assertProps abstRefineDefault [mkprop l r]
+       res <- checkSat solvers smt Nothing
        print res
        pure $ case res of
          Unsat -> True

From e96eef07dfb099790f47afcf0e8479eddc6c8638 Mon Sep 17 00:00:00 2001
From: dxo <hi@d-xo.org>
Date: Wed, 6 Sep 2023 19:00:05 +0200
Subject: [PATCH 02/12] fileCounter + ReaderT

---
 src/EVM/Solvers.hs | 16 +++++++++-------
 1 file changed, 9 insertions(+), 7 deletions(-)

diff --git a/src/EVM/Solvers.hs b/src/EVM/Solvers.hs
index e78c95b6e..70ec93ad6 100644
--- a/src/EVM/Solvers.hs
+++ b/src/EVM/Solvers.hs
@@ -12,8 +12,10 @@ import Control.Concurrent.Chan (Chan, newChan, writeChan, readChan)
 import Control.Concurrent (forkIO, killThread)
 import Control.Monad
 import Control.Monad.State.Strict
+import Control.Monad.Reader
 import Data.Char (isSpace)
 import Data.Map (Map)
+import Data.IORef
 import Data.Map qualified as Map
 import Data.Maybe (fromMaybe, isJust, fromJust)
 import Data.Text qualified as TS
@@ -103,7 +105,7 @@ withSolvers solver count timeout cont = do
   taskQueue <- newChan
   availableInstances <- newChan
   forM_ instances (writeChan availableInstances)
-  orchestrateId <- forkIO $ orchestrate taskQueue availableInstances
+  orchestrateId <- forkIO $ orchestrate taskQueue availableInstances 0
 
   -- run continuation with task queue
   res <- cont (SolverGroup taskQueue)
@@ -113,14 +115,14 @@ withSolvers solver count timeout cont = do
   killThread orchestrateId
   pure res
   where
-    orchestrate :: Chan Task -> Chan SolverInstance -> IO b
-    orchestrate queue avail = do
+    orchestrate :: Chan Task -> Chan SolverInstance -> Int -> IO b
+    orchestrate queue avail fileCounter = do
       task <- readChan queue
       inst <- readChan avail
-      _ <- forkIO $ runTask task inst avail
-      orchestrate queue avail
+      _ <- forkIO $ runTask task inst avail fileCounter
+      orchestrate queue avail (fileCounter + 1)
 
-    runTask (Task smt2@(SMT2 cmds (RefinementEqs refineEqs) cexvars) r debugFName) inst availableInstances = do
+    runTask (Task smt2@(SMT2 cmds (RefinementEqs refineEqs) cexvars) r debugFName) inst availableInstances fileCounter = do
       writeSMT2File smt2 debugFName ("abstracted")
       -- reset solver and send all lines of provided script
       out <- sendScript inst (SMT2 ("(reset)" : cmds) mempty mempty)
@@ -284,7 +286,7 @@ sendScript solver (SMT2 cmds _ _) = do
         "success" -> go cs
         e -> pure $ Left $ "Solver returned an error:\n" <> e <> "\nwhile sending the following line: " <> c
 
-checkCommand :: SolverInstance -> Text -> IO ()
+checkCommand :: SolverInstance -> Text -> ReaderT Text IO ()
 checkCommand inst cmd = do
   res <- sendCommand inst cmd
   case res of

From 2cd5d7869b362b1c96bcfbb7262a80e7b92bde1a Mon Sep 17 00:00:00 2001
From: Mate Soos <mate.soos@ethereum.org>
Date: Wed, 20 Sep 2023 16:19:48 +0200
Subject: [PATCH 03/12] Rebase fix

---
 test/test.hs | 1 -
 1 file changed, 1 deletion(-)

diff --git a/test/test.hs b/test/test.hs
index 4251bd139..1281fbcf3 100644
--- a/test/test.hs
+++ b/test/test.hs
@@ -3046,7 +3046,6 @@ checkEquivBase mkprop l r = withSolvers Z3 1 (Just 1) $ \solvers -> do
        pure True
      else do
        let smt = assertPropsNoSimp abstRefineDefault [mkprop l r]
-       let smt = assertProps abstRefineDefault [mkprop l r]
        res <- checkSat solvers smt Nothing
        print res
        pure $ case res of

From c63c57780ca46d3901f8a6dff8a5bb7158335c40 Mon Sep 17 00:00:00 2001
From: Mate Soos <mate.soos@ethereum.org>
Date: Wed, 20 Sep 2023 17:12:03 +0200
Subject: [PATCH 04/12] Almost clean  setup

---
 src/EVM/Fetch.hs   |  4 ++--
 src/EVM/Solvers.hs | 22 +++++++++++-----------
 src/EVM/SymExec.hs | 20 ++++++++------------
 test/test.hs       |  2 +-
 4 files changed, 22 insertions(+), 26 deletions(-)

diff --git a/src/EVM/Fetch.hs b/src/EVM/Fetch.hs
index 431a14de8..4f61a3560 100644
--- a/src/EVM/Fetch.hs
+++ b/src/EVM/Fetch.hs
@@ -238,13 +238,13 @@ type Fetcher s = Query s -> IO (EVM s ())
 -- will be pruned anyway.
 checkBranch :: SolverGroup -> Prop -> Prop -> IO BranchCondition
 checkBranch solvers branchcondition pathconditions = do
-  checkSat solvers (assertProps abstRefineDefault [(branchcondition .&& pathconditions)]) Nothing >>= \case
+  checkSat solvers (assertProps abstRefineDefault [(branchcondition .&& pathconditions)]) >>= \case
     -- the condition is unsatisfiable
     Unsat -> -- if pathconditions are consistent then the condition must be false
       pure $ Case False
     -- Sat means its possible for condition to hold
     Sat _ -> -- is its negation also possible?
-      checkSat solvers (assertProps abstRefineDefault [(pathconditions .&& (PNeg branchcondition))]) Nothing >>= \case
+      checkSat solvers (assertProps abstRefineDefault [(pathconditions .&& (PNeg branchcondition))]) >>= \case
         -- No. The condition must hold
         Unsat -> pure $ Case True
         -- Yes. Both branches possible
diff --git a/src/EVM/Solvers.hs b/src/EVM/Solvers.hs
index 70ec93ad6..617c3b7f1 100644
--- a/src/EVM/Solvers.hs
+++ b/src/EVM/Solvers.hs
@@ -12,10 +12,8 @@ import Control.Concurrent.Chan (Chan, newChan, writeChan, readChan)
 import Control.Concurrent (forkIO, killThread)
 import Control.Monad
 import Control.Monad.State.Strict
-import Control.Monad.Reader
 import Data.Char (isSpace)
 import Data.Map (Map)
-import Data.IORef
 import Data.Map qualified as Map
 import Data.Maybe (fromMaybe, isJust, fromJust)
 import Data.Text qualified as TS
@@ -25,6 +23,7 @@ import Data.Text.Lazy.IO qualified as T
 import Data.Text.Lazy.Builder
 import System.Process (createProcess, cleanupProcess, proc, ProcessHandle, std_in, std_out, std_err, StdStream(..))
 import Witch (into)
+import GHC.Stack (HasCallStack, prettyCallStack, callStack)
 
 import EVM.SMT
 import EVM.Types (W256, Expr(AbstractBuf), internalError)
@@ -82,19 +81,20 @@ isUnsat :: CheckSatResult -> Bool
 isUnsat Unsat = True
 isUnsat _ = False
 
-checkSat :: SolverGroup -> SMT2 -> Maybe String -> IO CheckSatResult
-checkSat (SolverGroup taskQueue) script debugFName = do
+checkSat :: HasCallStack => SolverGroup -> SMT2 -> IO CheckSatResult
+checkSat (SolverGroup taskQueue) script = do
   -- prepare result channel
   resChan <- newChan
   -- send task to solver group
-  writeChan taskQueue (Task script resChan debugFName)
+  let callingFunc = head . lines $ prettyCallStack callStack
+  writeChan taskQueue (Task script resChan (Just callingFunc))
   -- collect result
   readChan resChan
 
-writeSMT2File :: SMT2 -> Maybe String -> String -> IO ()
-writeSMT2File smt2 fname abst =
+writeSMT2File :: SMT2 -> Maybe String -> Int -> String -> IO ()
+writeSMT2File smt2 fname count abst =
   when (isJust fname) $
-  do T.writeFile (fromJust fname <> "-" <> abst <> ".smt2")
+  do T.writeFile (fromJust fname <> "-" <> (show count) <> "-" <> abst <> ".smt2")
       ("; " <> formatSMT2 smt2 <> "\n\n(check-sat)")
 
 withSolvers :: Solver -> Natural -> Maybe Natural -> (SolverGroup -> IO a) -> IO a
@@ -123,7 +123,7 @@ withSolvers solver count timeout cont = do
       orchestrate queue avail (fileCounter + 1)
 
     runTask (Task smt2@(SMT2 cmds (RefinementEqs refineEqs) cexvars) r debugFName) inst availableInstances fileCounter = do
-      writeSMT2File smt2 debugFName ("abstracted")
+      writeSMT2File smt2 debugFName fileCounter "abstracted"
       -- reset solver and send all lines of provided script
       out <- sendScript inst (SMT2 ("(reset)" : cmds) mempty mempty)
       case out of
@@ -140,7 +140,7 @@ withSolvers solver count timeout cont = do
                 "sat" -> if null refineEqs then Sat <$> getModel inst cexvars
                          else do
                               let refinedSMT2 = SMT2 refineEqs mempty mempty
-                              writeSMT2File refinedSMT2 debugFName ("refined")
+                              writeSMT2File refinedSMT2 debugFName fileCounter "refined"
                               _ <- sendScript inst refinedSMT2
                               sat2 <- sendLine inst "(check-sat)"
                               case sat2 of
@@ -286,7 +286,7 @@ sendScript solver (SMT2 cmds _ _) = do
         "success" -> go cs
         e -> pure $ Left $ "Solver returned an error:\n" <> e <> "\nwhile sending the following line: " <> c
 
-checkCommand :: SolverInstance -> Text -> ReaderT Text IO ()
+checkCommand :: SolverInstance -> Text -> IO ()
 checkCommand inst cmd = do
   res <- sendCommand inst cmd
   case res of
diff --git a/src/EVM/SymExec.hs b/src/EVM/SymExec.hs
index ea1c6aa01..d198a891a 100644
--- a/src/EVM/SymExec.hs
+++ b/src/EVM/SymExec.hs
@@ -510,7 +510,7 @@ reachable solvers e = do
         pure (fst tres <> fst fres, subexpr)
       leaf -> do
         let query = assertProps abstRefineDefault pcs
-        res <- checkSat solvers query Nothing
+        res <- checkSat solvers query
         case res of
           Sat _ -> pure ([query], Just leaf)
           Unsat -> pure ([query], Nothing)
@@ -576,14 +576,13 @@ verify solvers opts preState maybepost = do
         assumes = preState.constraints
         withQueries = canViolate <&> \leaf ->
           (assertProps opts.abstRefineConfig (PNeg (post preState leaf) : assumes <> extractProps leaf), leaf)
-        debugFName = if opts.debug then Just ("verify-query") else Nothing
       putStrLn $ "Checking for reachability of "
                    <> show (length withQueries)
                    <> " potential property violation(s)"
 
       -- Dispatch the remaining branches to the solver to check for violations
       results <- flip mapConcurrently withQueries $ \(query, leaf) -> do
-        res <- checkSat solvers query debugFName
+        res <- checkSat solvers query
         pure (res, leaf)
       let cexs = filter (\(res, _) -> not . isUnsat $ res) results
       pure $ if Prelude.null cexs then (expr, [Qed ()]) else (expr, fmap toVRes cexs)
@@ -681,16 +680,13 @@ equivalenceCheck' solvers branchesA branchesB opts = do
     -- the solver if we can determine unsatisfiability from the cache already
     -- the last element of the returned tuple indicates whether the cache was
     -- used or not
-    check :: UnsatCache -> (Set Prop) -> Int -> IO (EquivResult, Bool)
-    check knownUnsat props idx = do
-      let
-        smt = assertProps opts.abstRefineConfig (Set.toList props)
-        debugFName = if opts.debug then Just "equiv-query"
-                                   else Nothing
+    check :: UnsatCache -> (Set Prop) -> IO (EquivResult, Bool)
+    check knownUnsat props = do
+      let smt = assertProps opts.abstRefineConfig (Set.toList props)
       ku <- readTVarIO knownUnsat
       res <- if subsetAny props ku
              then pure (True, Unsat)
-             else (fmap ((False),) (checkSat solvers smt debugFName))
+             else (fmap ((False),) (checkSat solvers smt))
       case res of
         (_, Sat x) -> pure (Cex x, False)
         (quick, Unsat) ->
@@ -711,7 +707,7 @@ equivalenceCheck' solvers branchesA branchesB opts = do
     checkAll :: [(Set Prop)] -> UnsatCache -> Int -> IO [(EquivResult, Bool)]
     checkAll input cache numproc = do
        wrap <- pool numproc
-       parMapIO (wrap . (uncurry $ check cache)) $ zip input [1..]
+       parMapIO (wrap . (check cache)) input
 
 
     -- Takes two branches and returns a set of props that will need to be
@@ -783,7 +779,7 @@ produceModels solvers expr = do
   let flattened = flattenExpr expr
       withQueries = fmap (\e -> ((assertProps abstRefineDefault) . extractProps $ e, e)) flattened
   results <- flip mapConcurrently withQueries $ \(query, leaf) -> do
-    res <- checkSat solvers query Nothing
+    res <- checkSat solvers query
     pure (res, leaf)
   pure $ fmap swap $ filter (\(res, _) -> not . isUnsat $ res) results
 
diff --git a/test/test.hs b/test/test.hs
index 1281fbcf3..88b19c173 100644
--- a/test/test.hs
+++ b/test/test.hs
@@ -3046,7 +3046,7 @@ checkEquivBase mkprop l r = withSolvers Z3 1 (Just 1) $ \solvers -> do
        pure True
      else do
        let smt = assertPropsNoSimp abstRefineDefault [mkprop l r]
-       res <- checkSat solvers smt Nothing
+       res <- checkSat solvers smt
        print res
        pure $ case res of
          Unsat -> True

From 1dde6a1adb71d57f75c3e1639b59b8717b8895bc Mon Sep 17 00:00:00 2001
From: Mate Soos <mate.soos@ethereum.org>
Date: Thu, 21 Sep 2023 11:14:24 +0200
Subject: [PATCH 05/12] All queries are saved

---
 src/EVM/Solvers.hs | 22 +++++++++-------------
 1 file changed, 9 insertions(+), 13 deletions(-)

diff --git a/src/EVM/Solvers.hs b/src/EVM/Solvers.hs
index 617c3b7f1..845babb32 100644
--- a/src/EVM/Solvers.hs
+++ b/src/EVM/Solvers.hs
@@ -15,7 +15,7 @@ import Control.Monad.State.Strict
 import Data.Char (isSpace)
 import Data.Map (Map)
 import Data.Map qualified as Map
-import Data.Maybe (fromMaybe, isJust, fromJust)
+import Data.Maybe (fromMaybe)
 import Data.Text qualified as TS
 import Data.Text.Lazy (Text)
 import Data.Text.Lazy qualified as T
@@ -23,7 +23,6 @@ import Data.Text.Lazy.IO qualified as T
 import Data.Text.Lazy.Builder
 import System.Process (createProcess, cleanupProcess, proc, ProcessHandle, std_in, std_out, std_err, StdStream(..))
 import Witch (into)
-import GHC.Stack (HasCallStack, prettyCallStack, callStack)
 
 import EVM.SMT
 import EVM.Types (W256, Expr(AbstractBuf), internalError)
@@ -58,7 +57,6 @@ newtype SolverGroup = SolverGroup (Chan Task)
 data Task = Task
   { script :: SMT2
   , resultChan :: Chan CheckSatResult
-  , debugFName :: Maybe String
   }
 
 -- | The result of a call to (check-sat)
@@ -81,20 +79,18 @@ isUnsat :: CheckSatResult -> Bool
 isUnsat Unsat = True
 isUnsat _ = False
 
-checkSat :: HasCallStack => SolverGroup -> SMT2 -> IO CheckSatResult
+checkSat :: SolverGroup -> SMT2 -> IO CheckSatResult
 checkSat (SolverGroup taskQueue) script = do
   -- prepare result channel
   resChan <- newChan
   -- send task to solver group
-  let callingFunc = head . lines $ prettyCallStack callStack
-  writeChan taskQueue (Task script resChan (Just callingFunc))
+  writeChan taskQueue (Task script resChan)
   -- collect result
   readChan resChan
 
-writeSMT2File :: SMT2 -> Maybe String -> Int -> String -> IO ()
-writeSMT2File smt2 fname count abst =
-  when (isJust fname) $
-  do T.writeFile (fromJust fname <> "-" <> (show count) <> "-" <> abst <> ".smt2")
+writeSMT2File :: SMT2 -> Int -> String -> IO ()
+writeSMT2File smt2 count abst =
+  do T.writeFile ("query-" <> (show count) <> "-" <> abst <> ".smt2")
       ("; " <> formatSMT2 smt2 <> "\n\n(check-sat)")
 
 withSolvers :: Solver -> Natural -> Maybe Natural -> (SolverGroup -> IO a) -> IO a
@@ -122,8 +118,8 @@ withSolvers solver count timeout cont = do
       _ <- forkIO $ runTask task inst avail fileCounter
       orchestrate queue avail (fileCounter + 1)
 
-    runTask (Task smt2@(SMT2 cmds (RefinementEqs refineEqs) cexvars) r debugFName) inst availableInstances fileCounter = do
-      writeSMT2File smt2 debugFName fileCounter "abstracted"
+    runTask (Task smt2@(SMT2 cmds (RefinementEqs refineEqs) cexvars) r) inst availableInstances fileCounter = do
+      writeSMT2File smt2 fileCounter "abstracted"
       -- reset solver and send all lines of provided script
       out <- sendScript inst (SMT2 ("(reset)" : cmds) mempty mempty)
       case out of
@@ -140,7 +136,7 @@ withSolvers solver count timeout cont = do
                 "sat" -> if null refineEqs then Sat <$> getModel inst cexvars
                          else do
                               let refinedSMT2 = SMT2 refineEqs mempty mempty
-                              writeSMT2File refinedSMT2 debugFName fileCounter "refined"
+                              writeSMT2File refinedSMT2 fileCounter "refined"
                               _ <- sendScript inst refinedSMT2
                               sat2 <- sendLine inst "(check-sat)"
                               case sat2 of

From 8024cf4632424a7199d466aa4d866f6a1ad9625c Mon Sep 17 00:00:00 2001
From: Mate Soos <mate.soos@ethereum.org>
Date: Thu, 21 Sep 2023 11:48:11 +0200
Subject: [PATCH 06/12] Get both props and SMT2s

---
 src/EVM/SMT.hs     | 60 +++++++++++++++++++++++++++-------------------
 src/EVM/Solvers.hs | 13 +++++-----
 2 files changed, 42 insertions(+), 31 deletions(-)

diff --git a/src/EVM/SMT.hs b/src/EVM/SMT.hs
index b199031e2..8e49230df 100644
--- a/src/EVM/SMT.hs
+++ b/src/EVM/SMT.hs
@@ -103,8 +103,14 @@ data SMTCex = SMTCex
 
 
 -- | Used for abstraction-refinement of the SMT formula. Contains assertions that make our query fully precise. These will be added to the assertion stack if we get `sat` with the abstracted query.
-newtype RefinementEqs = RefinementEqs [Builder]
-  deriving (Eq, Show, Monoid, Semigroup)
+data RefinementEqs = RefinementEqs [Builder] [Prop]
+  deriving (Eq, Show)
+
+instance Semigroup RefinementEqs where
+  (RefinementEqs a b) <> (RefinementEqs a2 b2) = RefinementEqs (a <> a2) (b <> b2)
+
+instance Monoid RefinementEqs where
+  mempty = RefinementEqs mempty mempty
 
 flattenBufs :: SMTCex -> Maybe SMTCex
 flattenBufs cex = do
@@ -125,17 +131,20 @@ collapse model = case toBuf model of
 getVar :: SMTCex -> TS.Text -> W256
 getVar cex name = fromJust $ Map.lookup (Var name) cex.vars
 
-data SMT2 = SMT2 [Builder] RefinementEqs CexVars
+data SMT2 = SMT2 [Builder] RefinementEqs CexVars [Prop]
   deriving (Eq, Show)
 
 instance Semigroup SMT2 where
-  (SMT2 a (RefinementEqs b) c) <> (SMT2 a2 (RefinementEqs b2) c2) = SMT2 (a <> a2) (RefinementEqs (b <> b2)) (c <> c2)
+  (SMT2 a (RefinementEqs b refps) c d) <> (SMT2 a2 (RefinementEqs b2 refps2) c2 d2) = SMT2 (a <> a2) (RefinementEqs (b <> b2) (refps <> refps2)) (c <> c2) (d <> d2)
 
 instance Monoid SMT2 where
-  mempty = SMT2 mempty mempty mempty
+  mempty = SMT2 mempty mempty mempty mempty
 
 formatSMT2 :: SMT2 -> Text
-formatSMT2 (SMT2 ls _ _) = T.unlines (fmap toLazyText ls)
+formatSMT2 (SMT2 ls _ _ ps) = expr <> smt2
+ where
+ expr = T.pack $ "; " <> show ps
+ smt2 = T.unlines (fmap toLazyText ls)
 
 -- | Reads all intermediate variables from the builder state and produces SMT declaring them as constants
 declareIntermediates :: BufEnv -> StoreEnv -> SMT2
@@ -144,16 +153,16 @@ declareIntermediates bufs stores =
       encBs = Map.mapWithKey encodeBuf bufs
       sorted = List.sortBy compareFst $ Map.toList $ encSs <> encBs
       decls = fmap snd sorted
-      smt2 = (SMT2 [fromText "; intermediate buffers & stores"] mempty mempty):decls
-  in  foldr (<>) (SMT2[""] mempty mempty) smt2
+      smt2 = (SMT2 [fromText "; intermediate buffers & stores"] mempty mempty mempty):decls
+  in  foldr (<>) (SMT2[""] mempty mempty mempty) smt2
   where
     compareFst (l, _) (r, _) = compare l r
     encodeBuf n expr =
-      SMT2 ["(define-const buf" <> (fromString . show $ n) <> " Buf " <> exprToSMT expr <> ")\n"]  mempty mempty <> encodeBufLen n expr
+      SMT2 ["(define-const buf" <> (fromString . show $ n) <> " Buf " <> exprToSMT expr <> ")\n"]  mempty mempty mempty <> encodeBufLen n expr
     encodeBufLen n expr =
-      SMT2 ["(define-const buf" <> (fromString . show $ n) <>"_length" <> " (_ BitVec 256) " <> exprToSMT (bufLengthEnv bufs True expr) <> ")"] mempty mempty
+      SMT2 ["(define-const buf" <> (fromString . show $ n) <>"_length" <> " (_ BitVec 256) " <> exprToSMT (bufLengthEnv bufs True expr) <> ")"] mempty mempty mempty
     encodeStore n expr =
-      SMT2 ["(define-const store" <> (fromString . show $ n) <> " Storage " <> exprToSMT expr <> ")"] mempty mempty
+      SMT2 ["(define-const store" <> (fromString . show $ n) <> " Storage " <> exprToSMT expr <> ")"] mempty mempty mempty
 
 data AbstState = AbstState
   { words :: Map (Expr EWord) Int
@@ -190,7 +199,7 @@ abstractAwayProps abstRefineConfig ps = runState (mapM abstrAway ps) (AbstState
                   pure $ Var (TS.pack ("abst_" ++ show next))
 
 smt2Line :: Builder -> SMT2
-smt2Line txt = SMT2 [txt] mempty mempty
+smt2Line txt = SMT2 [txt] mempty mempty mempty
 
 assertProps :: AbstRefineConfig -> [Prop] -> SMT2
 assertProps conf ps = assertPropsNoSimp conf (Expr.simplifyProps ps)
@@ -221,9 +230,10 @@ assertPropsNoSimp abstRefineConfig ps =
   <> keccakAssumes
   <> readAssumes
   <> smt2Line ""
-  <> SMT2 (fmap (\p -> "(assert " <> p <> ")") encs) mempty mempty
-  <> SMT2 mempty (RefinementEqs $ fmap (\p -> "(assert " <> p <> ")") abstSMT) mempty
-  <> SMT2 mempty mempty mempty { storeReads = storageReads }
+  <> SMT2 (fmap (\p -> "(assert " <> p <> ")") encs) mempty mempty mempty
+  <> SMT2 mempty (RefinementEqs (fmap (\p -> "(assert " <> p <> ")") abstSMT) (psElimAbst <> abstProps)) mempty mempty
+  <> SMT2 mempty mempty mempty { storeReads = storageReads } mempty
+  <> SMT2 mempty mempty mempty ps
 
   where
     (psElim, bufs, stores) = eliminateProps ps
@@ -251,13 +261,13 @@ assertPropsNoSimp abstRefineConfig ps =
 
     keccakAssumes
       = smt2Line "; keccak assumptions"
-      <> SMT2 (fmap (\p -> "(assert " <> propToSMT p <> ")") (keccakAssumptions psElim bufVals storeVals)) mempty mempty
+      <> SMT2 (fmap (\p -> "(assert " <> propToSMT p <> ")") (keccakAssumptions psElim bufVals storeVals)) mempty mempty mempty
       <> smt2Line "; keccak computations"
-      <> SMT2 (fmap (\p -> "(assert " <> propToSMT p <> ")") (keccakCompute psElim bufVals storeVals)) mempty mempty
+      <> SMT2 (fmap (\p -> "(assert " <> propToSMT p <> ")") (keccakCompute psElim bufVals storeVals)) mempty mempty mempty
 
     readAssumes
       = smt2Line "; read assumptions"
-        <> SMT2 (fmap (\p -> "(assert " <> propToSMT p <> ")") (assertReads psElim bufs stores)) mempty mempty
+        <> SMT2 (fmap (\p -> "(assert " <> propToSMT p <> ")") (assertReads psElim bufs stores)) mempty mempty mempty
 
 referencedAbstractStores :: TraversableTerm a => a -> Set Builder
 referencedAbstractStores term = foldTerm go mempty term
@@ -395,7 +405,7 @@ discoverMaxReads props benv senv = bufMap
 
 -- | Returns an SMT2 object with all buffers referenced from the input props declared, and with the appropriate cex extraction metadata attached
 declareBufs :: [Prop] -> BufEnv -> StoreEnv -> SMT2
-declareBufs props bufEnv storeEnv = SMT2 ("; buffers" : fmap declareBuf allBufs <> ("; buffer lengths" : fmap declareLength allBufs)) mempty cexvars
+declareBufs props bufEnv storeEnv = SMT2 ("; buffers" : fmap declareBuf allBufs <> ("; buffer lengths" : fmap declareLength allBufs)) mempty cexvars mempty
   where
     cexvars = (mempty :: CexVars){ buffers = discoverMaxReads props bufEnv storeEnv }
     allBufs = fmap fromLazyText $ Map.keys cexvars.buffers
@@ -404,39 +414,39 @@ declareBufs props bufEnv storeEnv = SMT2 ("; buffers" : fmap declareBuf allBufs
 
 -- Given a list of variable names, create an SMT2 object with the variables declared
 declareVars :: [Builder] -> SMT2
-declareVars names = SMT2 (["; variables"] <> fmap declare names) mempty cexvars
+declareVars names = SMT2 (["; variables"] <> fmap declare names) mempty cexvars mempty
   where
     declare n = "(declare-const " <> n <> " (_ BitVec 256))"
     cexvars = (mempty :: CexVars){ calldata = fmap toLazyText names }
 
 -- Given a list of variable names, create an SMT2 object with the variables declared
 declareAddrs :: [Builder] -> SMT2
-declareAddrs names = SMT2 (["; symbolic addresseses"] <> fmap declare names) mempty cexvars
+declareAddrs names = SMT2 (["; symbolic addresseses"] <> fmap declare names) mempty cexvars mempty
   where
     declare n = "(declare-const " <> n <> " Addr)"
     cexvars = (mempty :: CexVars){ addrs = fmap toLazyText names }
 
 declareFrameContext :: [(Builder, [Prop])] -> SMT2
-declareFrameContext names = SMT2 (["; frame context"] <> concatMap declare names) mempty cexvars
+declareFrameContext names = SMT2 (["; frame context"] <> concatMap declare names) mempty cexvars mempty
   where
     declare (n,props) = [ "(declare-const " <> n <> " (_ BitVec 256))" ]
                         <> fmap (\p -> "(assert " <> propToSMT p <> ")") props
     cexvars = (mempty :: CexVars){ txContext = fmap (toLazyText . fst) names }
 
 declareAbstractStores :: [Builder] -> SMT2
-declareAbstractStores names = SMT2 (["; abstract base stores"] <> fmap declare names) mempty mempty
+declareAbstractStores names = SMT2 (["; abstract base stores"] <> fmap declare names) mempty mempty mempty
   where
     declare n = "(declare-const " <> n <> " Storage)"
 
 declareBlockContext :: [(Builder, [Prop])] -> SMT2
-declareBlockContext names = SMT2 (["; block context"] <> concatMap declare names) mempty cexvars
+declareBlockContext names = SMT2 (["; block context"] <> concatMap declare names) mempty cexvars mempty
   where
     declare (n, props) = [ "(declare-const " <> n <> " (_ BitVec 256))" ]
                          <> fmap (\p -> "(assert " <> propToSMT p <> ")") props
     cexvars = (mempty :: CexVars){ blockContext = fmap (toLazyText . fst) names }
 
 prelude :: SMT2
-prelude =  SMT2 src mempty mempty
+prelude =  SMT2 src mempty mempty mempty
   where
   src = fmap (fromLazyText . T.drop 2) . T.lines $ [i|
   ; logic
diff --git a/src/EVM/Solvers.hs b/src/EVM/Solvers.hs
index 845babb32..23dbd83b3 100644
--- a/src/EVM/Solvers.hs
+++ b/src/EVM/Solvers.hs
@@ -90,8 +90,9 @@ checkSat (SolverGroup taskQueue) script = do
 
 writeSMT2File :: SMT2 -> Int -> String -> IO ()
 writeSMT2File smt2 count abst =
-  do T.writeFile ("query-" <> (show count) <> "-" <> abst <> ".smt2")
-      ("; " <> formatSMT2 smt2 <> "\n\n(check-sat)")
+  do
+    let content = formatSMT2 smt2 <> "\n\n(check-sat)"
+    T.writeFile ("query-" <> (show count) <> "-" <> abst <> ".smt2") content
 
 withSolvers :: Solver -> Natural -> Maybe Natural -> (SolverGroup -> IO a) -> IO a
 withSolvers solver count timeout cont = do
@@ -118,10 +119,10 @@ withSolvers solver count timeout cont = do
       _ <- forkIO $ runTask task inst avail fileCounter
       orchestrate queue avail (fileCounter + 1)
 
-    runTask (Task smt2@(SMT2 cmds (RefinementEqs refineEqs) cexvars) r) inst availableInstances fileCounter = do
+    runTask (Task smt2@(SMT2 cmds (RefinementEqs refineEqs refps) cexvars ps) r) inst availableInstances fileCounter = do
       writeSMT2File smt2 fileCounter "abstracted"
       -- reset solver and send all lines of provided script
-      out <- sendScript inst (SMT2 ("(reset)" : cmds) mempty mempty)
+      out <- sendScript inst (SMT2 ("(reset)" : cmds) mempty mempty ps)
       case out of
         -- if we got an error then return it
         Left e -> writeChan r (Error ("error while writing SMT to solver: " <> T.toStrict e))
@@ -135,7 +136,7 @@ withSolvers solver count timeout cont = do
                 "unknown" -> pure Unknown
                 "sat" -> if null refineEqs then Sat <$> getModel inst cexvars
                          else do
-                              let refinedSMT2 = SMT2 refineEqs mempty mempty
+                              let refinedSMT2 = SMT2 refineEqs mempty mempty (ps <> refps)
                               writeSMT2File refinedSMT2 fileCounter "refined"
                               _ <- sendScript inst refinedSMT2
                               sat2 <- sendLine inst "(check-sat)"
@@ -271,7 +272,7 @@ stopSolver (SolverInstance _ stdin stdout stderr process) = cleanupProcess (Just
 
 -- | Sends a list of commands to the solver. Returns the first error, if there was one.
 sendScript :: SolverInstance -> SMT2 -> IO (Either Text ())
-sendScript solver (SMT2 cmds _ _) = do
+sendScript solver (SMT2 cmds _ _ _) = do
   let sexprs = splitSExpr $ fmap toLazyText cmds
   go sexprs
   where

From 8db6f533511e0a3df5f013acea78521a32c59019 Mon Sep 17 00:00:00 2001
From: Mate Soos <mate.soos@ethereum.org>
Date: Thu, 21 Sep 2023 14:00:27 +0200
Subject: [PATCH 07/12] Better printing of SMT2 queries

---
 src/EVM/Format.hs | 1 +
 src/EVM/SMT.hs    | 3 ++-
 2 files changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/EVM/Format.hs b/src/EVM/Format.hs
index 7b24a6fe9..c8b8db08c 100644
--- a/src/EVM/Format.hs
+++ b/src/EVM/Format.hs
@@ -5,6 +5,7 @@ module EVM.Format
   ( formatExpr
   , formatSomeExpr
   , formatPartial
+  , formatProp
   , contractNamePart
   , contractPathPart
   , showError
diff --git a/src/EVM/SMT.hs b/src/EVM/SMT.hs
index 8e49230df..4566116db 100644
--- a/src/EVM/SMT.hs
+++ b/src/EVM/SMT.hs
@@ -32,6 +32,7 @@ import Language.SMT2.Syntax (Symbol, SpecConstant(..), GeneralRes(..), Term(..),
 import Numeric (readHex, readBin)
 import Witch (into, unsafeInto)
 import Control.Monad.State
+import EVM.Format (formatProp)
 
 import EVM.CSE
 import EVM.Expr (writeByte, bufLengthEnv, containsNode, bufLength, minLength, inRange)
@@ -143,7 +144,7 @@ instance Monoid SMT2 where
 formatSMT2 :: SMT2 -> Text
 formatSMT2 (SMT2 ls _ _ ps) = expr <> smt2
  where
- expr = T.pack $ "; " <> show ps
+ expr = T.replace "\n" "\n;" $ T.pack . TS.unpack $  TS.unlines (fmap formatProp ps)
  smt2 = T.unlines (fmap toLazyText ls)
 
 -- | Reads all intermediate variables from the builder state and produces SMT declaring them as constants

From b4b1232addd572ec44a3116ac7c30007e1fb8029 Mon Sep 17 00:00:00 2001
From: Mate Soos <mate.soos@ethereum.org>
Date: Fri, 22 Sep 2023 14:24:14 +0200
Subject: [PATCH 08/12] Fixing generated SMT2

---
 src/EVM/SMT.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/EVM/SMT.hs b/src/EVM/SMT.hs
index 4566116db..2e5d46e7a 100644
--- a/src/EVM/SMT.hs
+++ b/src/EVM/SMT.hs
@@ -144,7 +144,7 @@ instance Monoid SMT2 where
 formatSMT2 :: SMT2 -> Text
 formatSMT2 (SMT2 ls _ _ ps) = expr <> smt2
  where
- expr = T.replace "\n" "\n;" $ T.pack . TS.unpack $  TS.unlines (fmap formatProp ps)
+ expr = T.concat [T.singleton ';', T.replace "\n" "\n;" $ T.pack . TS.unpack $  TS.unlines (fmap formatProp ps)]
  smt2 = T.unlines (fmap toLazyText ls)
 
 -- | Reads all intermediate variables from the builder state and produces SMT declaring them as constants

From 920cc2e1d05beee8b320f7dc34a6d4e96cae5c0c Mon Sep 17 00:00:00 2001
From: "Mate Soos @ Ethereum Foundation"
 <99662964+msooseth@users.noreply.github.com>
Date: Wed, 4 Oct 2023 12:33:35 +0200
Subject: [PATCH 09/12] Update test/test.hs

Co-authored-by: dxo  <6689924+d-xo@users.noreply.github.com>
---
 test/test.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test/test.hs b/test/test.hs
index 88b19c173..04a8686d8 100644
--- a/test/test.hs
+++ b/test/test.hs
@@ -1723,7 +1723,7 @@ tests = testGroup "hevm"
               }
             }
             |]
-        (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint16)" [AbiUIntType 16])) [] debugVeriOpts
+        (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint16)" [AbiUIntType 16])) [] defaultVeriOpts
         putStrLn "DIV by zero is zero"
       ,
       -- Somewhat tautological since we are asserting the precondition

From 353f20af6f75f556f5acaa6c58eb9ab98222315e Mon Sep 17 00:00:00 2001
From: "Mate Soos @ Ethereum Foundation"
 <99662964+msooseth@users.noreply.github.com>
Date: Wed, 4 Oct 2023 12:33:42 +0200
Subject: [PATCH 10/12] Update test/test.hs

Co-authored-by: dxo  <6689924+d-xo@users.noreply.github.com>
---
 test/test.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test/test.hs b/test/test.hs
index 04a8686d8..e6c2cd279 100644
--- a/test/test.hs
+++ b/test/test.hs
@@ -1952,7 +1952,7 @@ tests = testGroup "hevm"
               }
              }
             |]
-          (_, [Cex (_, a), Cex (_, b)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] debugVeriOpts
+          (_, [Cex (_, a), Cex (_, b)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
           let ints = map (flip getVar "arg1") [a,b]
           assertBool "0 must be one of the Cex-es" $ isJust $ List.elemIndex 0 ints
           putStrLn "expected 2 counterexamples found, one Cex is the 0 value"

From cf769b95faf77947ac36ebcba367b6b7a05e8147 Mon Sep 17 00:00:00 2001
From: Mate Soos <mate.soos@ethereum.org>
Date: Wed, 4 Oct 2023 13:29:28 +0200
Subject: [PATCH 11/12] Sendline change

---
 src/EVM/Solvers.hs | 47 ++++++++++++++++++++++++++--------------------
 1 file changed, 27 insertions(+), 20 deletions(-)

diff --git a/src/EVM/Solvers.hs b/src/EVM/Solvers.hs
index 23dbd83b3..fe69cfa26 100644
--- a/src/EVM/Solvers.hs
+++ b/src/EVM/Solvers.hs
@@ -21,8 +21,10 @@ import Data.Text.Lazy (Text)
 import Data.Text.Lazy qualified as T
 import Data.Text.Lazy.IO qualified as T
 import Data.Text.Lazy.Builder
+import Data.Maybe (fromJust, isJust)
 import System.Process (createProcess, cleanupProcess, proc, ProcessHandle, std_in, std_out, std_err, StdStream(..))
 import Witch (into)
+import System.IO (openFile, IOMode(..))
 
 import EVM.SMT
 import EVM.Types (W256, Expr(AbstractBuf), internalError)
@@ -120,15 +122,16 @@ withSolvers solver count timeout cont = do
       orchestrate queue avail (fileCounter + 1)
 
     runTask (Task smt2@(SMT2 cmds (RefinementEqs refineEqs refps) cexvars ps) r) inst availableInstances fileCounter = do
+      debugF <- openFile "filename" WriteMode
       writeSMT2File smt2 fileCounter "abstracted"
       -- reset solver and send all lines of provided script
-      out <- sendScript inst (SMT2 ("(reset)" : cmds) mempty mempty ps)
+      out <- sendScript inst (Just debugF) (SMT2 ("(reset)" : cmds) mempty mempty ps)
       case out of
         -- if we got an error then return it
         Left e -> writeChan r (Error ("error while writing SMT to solver: " <> T.toStrict e))
         -- otherwise call (check-sat), parse the result, and send it down the result channel
         Right () -> do
-          sat <- sendLine inst "(check-sat)"
+          sat <- sendLine inst (Just debugF) "(check-sat)"
           res <- do
               case sat of
                 "unsat" -> pure Unsat
@@ -138,8 +141,8 @@ withSolvers solver count timeout cont = do
                          else do
                               let refinedSMT2 = SMT2 refineEqs mempty mempty (ps <> refps)
                               writeSMT2File refinedSMT2 fileCounter "refined"
-                              _ <- sendScript inst refinedSMT2
-                              sat2 <- sendLine inst "(check-sat)"
+                              _ <- sendScript inst (Just debugF) refinedSMT2
+                              sat2 <- sendLine inst (Just debugF) "(check-sat)"
                               case sat2 of
                                 "unsat" -> pure Unsat
                                 "timeout" -> pure Unknown
@@ -263,7 +266,7 @@ spawnSolver solver timeout = do
     CVC5 -> pure solverInstance
     _ -> do
       _ <- sendLine' solverInstance $ "(set-option :timeout " <> mkTimeout timeout <> ")"
-      _ <- sendLine solverInstance "(set-option :print-success true)"
+      _ <- sendLine solverInstance Nothing "(set-option :print-success true)"
       pure solverInstance
 
 -- | Cleanly shutdown a running solver instnace
@@ -271,46 +274,50 @@ stopSolver :: SolverInstance -> IO ()
 stopSolver (SolverInstance _ stdin stdout stderr process) = cleanupProcess (Just stdin, Just stdout, Just stderr, process)
 
 -- | Sends a list of commands to the solver. Returns the first error, if there was one.
-sendScript :: SolverInstance -> SMT2 -> IO (Either Text ())
-sendScript solver (SMT2 cmds _ _ _) = do
+sendScript :: SolverInstance -> Maybe Handle -> SMT2 -> IO (Either Text ())
+sendScript solver debugF (SMT2 cmds _ _ _) = do
   let sexprs = splitSExpr $ fmap toLazyText cmds
   go sexprs
   where
     go [] = pure $ Right ()
     go (c:cs) = do
-      out <- sendCommand solver c
+      out <- sendCommand solver debugF c
       case out of
         "success" -> go cs
         e -> pure $ Left $ "Solver returned an error:\n" <> e <> "\nwhile sending the following line: " <> c
 
-checkCommand :: SolverInstance -> Text -> IO ()
-checkCommand inst cmd = do
-  res <- sendCommand inst cmd
+checkCommand :: SolverInstance -> Maybe Handle -> Text -> IO ()
+checkCommand inst debugF cmd = do
+  res <- sendCommand inst debugF cmd
   case res of
     "success" -> pure ()
     _ -> internalError $ "Unexpected solver output: " <> T.unpack res
 
 -- | Sends a single command to the solver, returns the first available line from the output buffer
-sendCommand :: SolverInstance -> Text -> IO Text
-sendCommand inst cmd = do
+sendCommand :: SolverInstance -> Maybe Handle -> Text -> IO Text
+sendCommand inst debugF cmd = do
   -- trim leading whitespace
   let cmd' = T.dropWhile isSpace cmd
   case T.unpack cmd' of
     "" -> pure "success"      -- ignore blank lines
     ';' : _ -> pure "success" -- ignore comments
-    _ -> sendLine inst cmd'
+    _ -> sendLine inst debugF cmd'
 
 -- | Sends a string to the solver and appends a newline, returns the first available line from the output buffer
-sendLine :: SolverInstance -> Text -> IO Text
-sendLine (SolverInstance _ stdin stdout _ _) cmd = do
-  T.hPutStr stdin (T.append cmd "\n")
+sendLine :: SolverInstance -> Maybe Handle -> Text -> IO Text
+sendLine (SolverInstance _ stdin stdout _ _) debugF cmd = do
+  let toWrite = (T.append cmd "\n")
+  T.hPutStr stdin toWrite
+  when (isJust debugF) $ T.hPutStr (fromJust debugF) toWrite
   hFlush stdin
   T.hGetLine stdout
 
 -- | Sends a string to the solver and appends a newline, doesn't return stdout
-sendLine' :: SolverInstance -> Text -> IO ()
-sendLine' (SolverInstance _ stdin _ _ _) cmd = do
-  T.hPutStr stdin (T.append cmd "\n")
+sendLine' :: SolverInstance -> Maybe Handle -> Text -> IO ()
+sendLine' (SolverInstance _ stdin _ _ _) debugF cmd = do
+  let toWrite = (T.append cmd "\n")
+  T.hPutStr stdin toWrite
+  when (isJust debugF) $ T.hPutStr (fromJust debugF) toWrite
   hFlush stdin
 
 -- | Returns a string representation of the model for the requested variable

From f751e8a791266c2a6d0286b2bc06e7a8fab23075 Mon Sep 17 00:00:00 2001
From: Mate Soos <mate.soos@ethereum.org>
Date: Wed, 4 Oct 2023 13:45:08 +0200
Subject: [PATCH 12/12] Revert "Sendline change"

This reverts commit cf769b95faf77947ac36ebcba367b6b7a05e8147.
---
 src/EVM/Solvers.hs | 47 ++++++++++++++++++++--------------------------
 1 file changed, 20 insertions(+), 27 deletions(-)

diff --git a/src/EVM/Solvers.hs b/src/EVM/Solvers.hs
index fe69cfa26..23dbd83b3 100644
--- a/src/EVM/Solvers.hs
+++ b/src/EVM/Solvers.hs
@@ -21,10 +21,8 @@ import Data.Text.Lazy (Text)
 import Data.Text.Lazy qualified as T
 import Data.Text.Lazy.IO qualified as T
 import Data.Text.Lazy.Builder
-import Data.Maybe (fromJust, isJust)
 import System.Process (createProcess, cleanupProcess, proc, ProcessHandle, std_in, std_out, std_err, StdStream(..))
 import Witch (into)
-import System.IO (openFile, IOMode(..))
 
 import EVM.SMT
 import EVM.Types (W256, Expr(AbstractBuf), internalError)
@@ -122,16 +120,15 @@ withSolvers solver count timeout cont = do
       orchestrate queue avail (fileCounter + 1)
 
     runTask (Task smt2@(SMT2 cmds (RefinementEqs refineEqs refps) cexvars ps) r) inst availableInstances fileCounter = do
-      debugF <- openFile "filename" WriteMode
       writeSMT2File smt2 fileCounter "abstracted"
       -- reset solver and send all lines of provided script
-      out <- sendScript inst (Just debugF) (SMT2 ("(reset)" : cmds) mempty mempty ps)
+      out <- sendScript inst (SMT2 ("(reset)" : cmds) mempty mempty ps)
       case out of
         -- if we got an error then return it
         Left e -> writeChan r (Error ("error while writing SMT to solver: " <> T.toStrict e))
         -- otherwise call (check-sat), parse the result, and send it down the result channel
         Right () -> do
-          sat <- sendLine inst (Just debugF) "(check-sat)"
+          sat <- sendLine inst "(check-sat)"
           res <- do
               case sat of
                 "unsat" -> pure Unsat
@@ -141,8 +138,8 @@ withSolvers solver count timeout cont = do
                          else do
                               let refinedSMT2 = SMT2 refineEqs mempty mempty (ps <> refps)
                               writeSMT2File refinedSMT2 fileCounter "refined"
-                              _ <- sendScript inst (Just debugF) refinedSMT2
-                              sat2 <- sendLine inst (Just debugF) "(check-sat)"
+                              _ <- sendScript inst refinedSMT2
+                              sat2 <- sendLine inst "(check-sat)"
                               case sat2 of
                                 "unsat" -> pure Unsat
                                 "timeout" -> pure Unknown
@@ -266,7 +263,7 @@ spawnSolver solver timeout = do
     CVC5 -> pure solverInstance
     _ -> do
       _ <- sendLine' solverInstance $ "(set-option :timeout " <> mkTimeout timeout <> ")"
-      _ <- sendLine solverInstance Nothing "(set-option :print-success true)"
+      _ <- sendLine solverInstance "(set-option :print-success true)"
       pure solverInstance
 
 -- | Cleanly shutdown a running solver instnace
@@ -274,50 +271,46 @@ stopSolver :: SolverInstance -> IO ()
 stopSolver (SolverInstance _ stdin stdout stderr process) = cleanupProcess (Just stdin, Just stdout, Just stderr, process)
 
 -- | Sends a list of commands to the solver. Returns the first error, if there was one.
-sendScript :: SolverInstance -> Maybe Handle -> SMT2 -> IO (Either Text ())
-sendScript solver debugF (SMT2 cmds _ _ _) = do
+sendScript :: SolverInstance -> SMT2 -> IO (Either Text ())
+sendScript solver (SMT2 cmds _ _ _) = do
   let sexprs = splitSExpr $ fmap toLazyText cmds
   go sexprs
   where
     go [] = pure $ Right ()
     go (c:cs) = do
-      out <- sendCommand solver debugF c
+      out <- sendCommand solver c
       case out of
         "success" -> go cs
         e -> pure $ Left $ "Solver returned an error:\n" <> e <> "\nwhile sending the following line: " <> c
 
-checkCommand :: SolverInstance -> Maybe Handle -> Text -> IO ()
-checkCommand inst debugF cmd = do
-  res <- sendCommand inst debugF cmd
+checkCommand :: SolverInstance -> Text -> IO ()
+checkCommand inst cmd = do
+  res <- sendCommand inst cmd
   case res of
     "success" -> pure ()
     _ -> internalError $ "Unexpected solver output: " <> T.unpack res
 
 -- | Sends a single command to the solver, returns the first available line from the output buffer
-sendCommand :: SolverInstance -> Maybe Handle -> Text -> IO Text
-sendCommand inst debugF cmd = do
+sendCommand :: SolverInstance -> Text -> IO Text
+sendCommand inst cmd = do
   -- trim leading whitespace
   let cmd' = T.dropWhile isSpace cmd
   case T.unpack cmd' of
     "" -> pure "success"      -- ignore blank lines
     ';' : _ -> pure "success" -- ignore comments
-    _ -> sendLine inst debugF cmd'
+    _ -> sendLine inst cmd'
 
 -- | Sends a string to the solver and appends a newline, returns the first available line from the output buffer
-sendLine :: SolverInstance -> Maybe Handle -> Text -> IO Text
-sendLine (SolverInstance _ stdin stdout _ _) debugF cmd = do
-  let toWrite = (T.append cmd "\n")
-  T.hPutStr stdin toWrite
-  when (isJust debugF) $ T.hPutStr (fromJust debugF) toWrite
+sendLine :: SolverInstance -> Text -> IO Text
+sendLine (SolverInstance _ stdin stdout _ _) cmd = do
+  T.hPutStr stdin (T.append cmd "\n")
   hFlush stdin
   T.hGetLine stdout
 
 -- | Sends a string to the solver and appends a newline, doesn't return stdout
-sendLine' :: SolverInstance -> Maybe Handle -> Text -> IO ()
-sendLine' (SolverInstance _ stdin _ _ _) debugF cmd = do
-  let toWrite = (T.append cmd "\n")
-  T.hPutStr stdin toWrite
-  when (isJust debugF) $ T.hPutStr (fromJust debugF) toWrite
+sendLine' :: SolverInstance -> Text -> IO ()
+sendLine' (SolverInstance _ stdin _ _ _) cmd = do
+  T.hPutStr stdin (T.append cmd "\n")
   hFlush stdin
 
 -- | Returns a string representation of the model for the requested variable