diff --git a/.gitignore b/.gitignore
index f78b32318..c7e1881ed 100644
--- a/.gitignore
+++ b/.gitignore
@@ -10,3 +10,8 @@ dist/
 dist-newstyle/
 .configured
 cabal.project.local*
+
+# debug files
+*.smt2
+*.prop
+*.expr
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 423f7ff0f..9af608471 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -52,6 +52,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - CopySlice+WriteWord+ConcreteBuf now truncates ConcreteBuf in special cases
 - Better simplification of Eq IR elements
 - Run a toplevel constant folding reasoning system on branch conditions
+- Global config via a monad, which should allow for more refactoring
 - `evalProp` is renamed to `simplifyProp` for consistency
 - Mem explosion in `writeWord` function was possible in case `offset` was close to 2^256. Fixed.
 - BufLength was not simplified via bufLength function. Fixed.
diff --git a/bench/bench.hs b/bench/bench.hs
index 7b66d1eff..d5a02a9e1 100644
--- a/bench/bench.hs
+++ b/bench/bench.hs
@@ -2,6 +2,7 @@ module Main where
 
 import GHC.Natural
 import Control.Monad
+import Control.Monad.IO.Unlift
 import Data.Maybe
 import System.Environment (getEnv)
 
@@ -19,6 +20,7 @@ import qualified Data.ByteString.Lazy as LazyByteString
 import EVM.SymExec
 import EVM.Solidity
 import EVM.Solvers
+import EVM.Effects
 import EVM.Format (hexByteString)
 import qualified EVM.Stepper as Stepper
 import qualified EVM.Fetch as Fetch
@@ -67,16 +69,18 @@ blockchainTests ts = bench "blockchain-tests" $ nfIO $ do
       if n `elem` ignored
       then pure True
       else do
-        res <- runBCTest c
+        res <- runApp $ runBCTest c
         pure $ acc && res
     ) True cases
 
 -- | executes a single test case and returns a boolean value representing its success
-runBCTest :: BCTests.Case -> IO Bool
+runBCTest :: App m => BCTests.Case -> m Bool
 runBCTest x =
  do
-  vm0 <- BCTests.vmForCase x
+  vm0 <- liftIO $ BCTests.vmForCase x
   result <- Stepper.interpret (Fetch.zero 0 Nothing) vm0 Stepper.runFully
+  writeTrace vm0
+
   maybeReason <- BCTests.checkExpectation False x result
   pure $ isNothing maybeReason
 
@@ -84,7 +88,7 @@ runBCTest x =
 --- Helpers ----------------------------------------------------------------------------------------
 
 
-findPanics :: Solver -> Natural -> Integer -> ByteString -> IO ()
+findPanics :: App m => Solver -> Natural -> Integer -> ByteString -> m ()
 findPanics solver count iters c = do
   _ <- withSolvers solver count Nothing $ \s -> do
     let opts = defaultVeriOpts
@@ -92,7 +96,7 @@ findPanics solver count iters c = do
           , askSmtIters = iters + 1
           }
     checkAssert s allPanicCodes c Nothing [] opts
-  putStrLn "done"
+  liftIO $ putStrLn "done"
 
 
 -- constructs a benchmark suite that checks the given bytecode for reachable
@@ -103,8 +107,8 @@ mkbench :: IO ByteString -> String -> Integer -> [Natural] -> Benchmark
 mkbench c name iters counts = localOption WallTime $ env c (bgroup name . bmarks)
   where
     bmarks c' = concat $ [
-       [ bench ("cvc5-" <> show i) $ nfIO $ findPanics CVC5 i iters c'
-       , bench ("z3-" <> show i) $ nfIO $ findPanics Z3 i iters c'
+       [ bench ("cvc5-" <> show i) $ nfIO $ runApp $ findPanics CVC5 i iters c'
+       , bench ("z3-" <> show i) $ nfIO $ runApp $ findPanics Z3 i iters c'
        ]
        | i <- counts
      ]
diff --git a/cli/cli.hs b/cli/cli.hs
index 847519a6f..56e31e58f 100644
--- a/cli/cli.hs
+++ b/cli/cli.hs
@@ -8,6 +8,7 @@ module Main where
 
 import Control.Monad (when, forM_, unless)
 import Control.Monad.ST (RealWorld, stToIO)
+import Control.Monad.IO.Unlift
 import Data.ByteString (ByteString)
 import Data.DoubleWord (Word256)
 import Data.List (intersperse)
@@ -22,7 +23,6 @@ import Optics.Core ((&), set)
 import Witch (unsafeInto)
 import Options.Generic as Options
 import Paths_hevm qualified as Paths
-import System.IO (stderr)
 import System.Directory (withCurrentDirectory, getCurrentDirectory, doesDirectoryExist)
 import System.FilePath ((</>))
 import System.Exit (exitFailure, exitWith, ExitCode(..))
@@ -35,14 +35,15 @@ import EVM.Concrete qualified as Concrete
 import GitHash
 import EVM.FeeSchedule (feeSchedule)
 import EVM.Fetch qualified as Fetch
-import EVM.Format (hexByteString, strip0x, showTraceTree, formatExpr)
+import EVM.Format (hexByteString, strip0x, formatExpr)
 import EVM.Solidity
 import EVM.Solvers
 import EVM.Stepper qualified
 import EVM.SymExec
 import EVM.Transaction qualified
-import EVM.Types hiding (word)
+import EVM.Types hiding (word, Env)
 import EVM.UnitTest
+import EVM.Effects
 
 -- This record defines the program's command-line options
 -- automatically via the `optparse-generic` package.
@@ -85,6 +86,8 @@ data Command w
       , maxIterations :: w ::: Maybe Integer      <?> "Number of times we may revisit a particular branching point"
       , solver        :: w ::: Maybe Text         <?> "Used SMT solver: z3 (default) or cvc5"
       , smtdebug      :: w ::: Bool               <?> "Print smt queries sent to the solver"
+      , debug         :: w ::: Bool               <?> "Debug printing of internal behaviour"
+      , trace         :: w ::: Bool               <?> "Dump trace"
       , assertions    :: w ::: Maybe [Word256]    <?> "Comma separated list of solc panic codes to check for (default: user defined assertion violations only)"
       , askSmtIterations :: w ::: Integer         <!> "1" <?> "Number of times we may revisit a particular branching point before we consult the smt solver to check reachability (default: 1)"
       , numSolvers    :: w ::: Maybe Natural      <?> "Number of solver instances to use (default: number of cpu cores)"
@@ -103,6 +106,8 @@ data Command w
       , solver        :: w ::: Maybe Text       <?> "Used SMT solver: z3 (default) or cvc5"
       , smtoutput     :: w ::: Bool             <?> "Print verbose smt output"
       , smtdebug      :: w ::: Bool             <?> "Print smt queries sent to the solver"
+      , debug         :: w ::: Bool             <?> "Debug printing of internal behaviour"
+      , trace         :: w ::: Bool             <?> "Dump trace"
       , askSmtIterations :: w ::: Integer       <!> "1" <?> "Number of times we may revisit a particular branching point before we consult the smt solver to check reachability (default: 1)"
       , loopDetectionHeuristic :: w ::: LoopHeuristic <!> "StackBased" <?> "Which heuristic should be used to determine if we are in a loop: StackBased (default) or Naive"
       , abstractArithmetic    :: w ::: Bool             <?> "Use abstraction-refinement for complicated arithmetic functions such as MulMod. This runs the solver first with abstraction turned on, and if it returns a potential counterexample, the counterexample is refined to make sure it is a counterexample for the actual (not the abstracted) problem"
@@ -128,6 +133,7 @@ data Command w
       , maxcodesize :: w ::: Maybe W256        <?> "Block: max code size"
       , prevRandao  :: w ::: Maybe W256        <?> "Block: prevRandao"
       , chainid     :: w ::: Maybe W256        <?> "Env: chainId"
+      , debug       :: w ::: Bool              <?> "Debug printing of internal behaviour"
       , trace       :: w ::: Bool              <?> "Dump trace"
       , rpc         :: w ::: Maybe URL         <?> "Fetch state from a remote node"
       , block       :: w ::: Maybe W256        <?> "Block state is be fetched from"
@@ -144,6 +150,8 @@ data Command w
       , match         :: w ::: Maybe String             <?> "Test case filter - only run methods matching regex"
       , solver        :: w ::: Maybe Text               <?> "Used SMT solver: z3 (default) or cvc5"
       , smtdebug      :: w ::: Bool                     <?> "Print smt queries sent to the solver"
+      , debug         :: w ::: Bool                     <?> "Debug printing of internal behaviour"
+      , trace         :: w ::: Bool                     <?> "Dump trace"
       , ffi           :: w ::: Bool                     <?> "Allow the usage of the hevm.ffi() cheatcode (WARNING: this allows test authors to execute arbitrary code on your machine)"
       , smttimeout    :: w ::: Maybe Natural            <?> "Timeout given to SMT solver in seconds (default: 300)"
       , maxIterations :: w ::: Maybe Integer            <?> "Number of times we may revisit a particular branching point"
@@ -186,54 +194,58 @@ getFullVersion = showVersion Paths.version <> " [" <> gitVersion <> "]"
 main :: IO ()
 main = do
   cmd <- Options.unwrapRecord "hevm -- Ethereum evaluator"
+  let env = Env { config = defaultConfig
+    { dumpQueries = cmd.smtdebug
+    , debug = cmd.debug
+    , abstRefineMem = cmd.abstractMemory
+    , abstRefineArith = cmd.abstractArithmetic
+    , dumpTrace = cmd.trace
+    } }
   case cmd of
     Version {} ->putStrLn getFullVersion
     Symbolic {} -> do
       root <- getRoot cmd
-      withCurrentDirectory root $ assert cmd
-    Equivalence {} -> equivalence cmd
-    Exec {} ->
-      launchExec cmd
+      withCurrentDirectory root $ runEnv env $ assert cmd
+    Equivalence {} -> runEnv env $ equivalence cmd
+    Exec {} -> runEnv env $ launchExec cmd
     Test {} -> do
       root <- getRoot cmd
       withCurrentDirectory root $ do
         cores <- unsafeInto <$> getNumProcessors
         solver <- getSolver cmd
-        withSolvers solver cores cmd.smttimeout $ \solvers -> do
-          buildOut <- readBuildOutput root (getProjectType cmd)
+        runEnv env $ withSolvers solver cores cmd.smttimeout $ \solvers -> do
+          buildOut <- liftIO $ readBuildOutput root (getProjectType cmd)
           case buildOut of
-            Left e -> do
+            Left e -> liftIO $ do
               putStrLn $ "Error: " <> e
               exitFailure
             Right out -> do
               -- TODO: which functions here actually require a BuildOutput, and which can take it as a Maybe?
-              testOpts <- unitTestOptions cmd solvers (Just out)
+              testOpts <- liftIO $ unitTestOptions cmd solvers (Just out)
               res <- unitTest testOpts out.contracts
-              unless res exitFailure
+              liftIO $ unless res exitFailure
 
-equivalence :: Command Options.Unwrapped -> IO ()
+equivalence :: App m => Command Options.Unwrapped -> m ()
 equivalence cmd = do
   let bytecodeA = hexByteString "--code" . strip0x $ cmd.codeA
       bytecodeB = hexByteString "--code" . strip0x $ cmd.codeB
       veriOpts = VeriOpts { simp = True
-                          , debug = False
                           , maxIter = cmd.maxIterations
                           , askSmtIters = cmd.askSmtIterations
                           , loopHeuristic = cmd.loopDetectionHeuristic
-                          , abstRefineConfig = AbstRefineConfig cmd.abstractArithmetic cmd.abstractMemory
                           , rpcInfo = Nothing
                           }
-  calldata <- buildCalldata cmd
-  solver <- getSolver cmd
+  calldata <- liftIO $ buildCalldata cmd
+  solver <- liftIO $ getSolver cmd
   withSolvers solver 3 Nothing $ \s -> do
     res <- equivalenceCheck s bytecodeA bytecodeB veriOpts calldata
     case any isCex res of
-      False -> do
+      False -> liftIO $ do
         putStrLn "No discrepancies found"
         when (any isTimeout res) $ do
           putStrLn "But timeout(s) occurred"
           exitFailure
-      True -> do
+      True -> liftIO $ do
         let cexs = mapMaybe getCex res
         T.putStrLn . T.unlines $
           [ "Not equivalent. The following inputs result in differing behaviours:"
@@ -289,29 +301,27 @@ buildCalldata cmd = case (cmd.calldata, cmd.sig) of
 
 
 -- If function signatures are known, they should always be given for best results.
-assert :: Command Options.Unwrapped -> IO ()
+assert :: App m => Command Options.Unwrapped -> m ()
 assert cmd = do
   let block'  = maybe Fetch.Latest Fetch.BlockNumber cmd.block
       rpcinfo = (,) block' <$> cmd.rpc
-  calldata <- buildCalldata cmd
-  preState <- symvmFromCommand cmd calldata
+  calldata <- liftIO $ buildCalldata cmd
+  preState <- liftIO $ symvmFromCommand cmd calldata
   let errCodes = fromMaybe defaultPanicCodes cmd.assertions
-  cores <- unsafeInto <$> getNumProcessors
+  cores <- liftIO $ unsafeInto <$> getNumProcessors
   let solverCount = fromMaybe cores cmd.numSolvers
-  solver <- getSolver cmd
+  solver <- liftIO $ getSolver cmd
   withSolvers solver solverCount cmd.smttimeout $ \solvers -> do
     let opts = VeriOpts { simp = True
-                        , debug = cmd.smtdebug
                         , maxIter = cmd.maxIterations
                         , askSmtIters = cmd.askSmtIterations
                         , loopHeuristic = cmd.loopDetectionHeuristic
-                        , abstRefineConfig = AbstRefineConfig cmd.abstractArithmetic cmd.abstractMemory
                         , rpcInfo = rpcinfo
     }
     (expr, res) <- verify solvers opts preState (Just $ checkAssertions errCodes)
     case res of
       [Qed _] -> do
-        putStrLn "\nQED: No reachable property violations discovered\n"
+        liftIO $ putStrLn "\nQED: No reachable property violations discovered\n"
         showExtras solvers cmd calldata expr
       _ -> do
         let cexs = snd <$> mapMaybe getCex res
@@ -330,25 +340,26 @@ assert cmd = do
                  , "Could not determine reachability of the following end states:"
                  , ""
                  ] <> fmap (formatExpr) timeouts
-        T.putStrLn $ T.unlines (counterexamples <> unknowns)
+        liftIO $ T.putStrLn $ T.unlines (counterexamples <> unknowns)
         showExtras solvers cmd calldata expr
-        exitFailure
+        liftIO $ exitFailure
 
-showExtras :: SolverGroup -> Command Options.Unwrapped -> (Expr Buf, [Prop]) -> Expr End -> IO ()
+showExtras :: App m => SolverGroup -> Command Options.Unwrapped -> (Expr Buf, [Prop]) -> Expr End -> m ()
 showExtras solvers cmd calldata expr = do
-  when cmd.showTree $ do
+  when cmd.showTree $ liftIO $ do
     putStrLn "=== Expression ===\n"
     T.putStrLn $ formatExpr expr
     putStrLn ""
   when cmd.showReachableTree $ do
     reached <- reachable solvers expr
-    putStrLn "=== Reachable Expression ===\n"
-    T.putStrLn (formatExpr . snd $ reached)
-    putStrLn ""
+    liftIO $ do
+      putStrLn "=== Reachable Expression ===\n"
+      T.putStrLn (formatExpr . snd $ reached)
+      putStrLn ""
   when cmd.getModels $ do
-    putStrLn $ "=== Models for " <> show (Expr.numBranches expr) <> " branches ===\n"
+    liftIO $ putStrLn $ "=== Models for " <> show (Expr.numBranches expr) <> " branches ===\n"
     ms <- produceModels solvers expr
-    forM_ ms (showModel (fst calldata))
+    liftIO $ forM_ ms (showModel (fst calldata))
 
 isTestOrLib :: Text -> Bool
 isTestOrLib file = T.isSuffixOf ".t.sol" file || areAnyPrefixOf ["src/test/", "src/tests/", "lib/"] file
@@ -356,10 +367,10 @@ isTestOrLib file = T.isSuffixOf ".t.sol" file || areAnyPrefixOf ["src/test/", "s
 areAnyPrefixOf :: [Text] -> Text -> Bool
 areAnyPrefixOf prefixes t = any (flip T.isPrefixOf t) prefixes
 
-launchExec :: Command Options.Unwrapped -> IO ()
+launchExec :: App m => Command Options.Unwrapped -> m ()
 launchExec cmd = do
-  dapp <- getSrcInfo cmd
-  vm <- vmFromCommand cmd
+  dapp <- liftIO $ getSrcInfo cmd
+  vm <- liftIO $ vmFromCommand cmd
   let
     block = maybe Fetch.Latest Fetch.BlockNumber cmd.block
     rpcinfo = (,) block <$> cmd.rpc
@@ -367,21 +378,21 @@ launchExec cmd = do
   -- TODO: we shouldn't need solvers to execute this code
   withSolvers Z3 0 Nothing $ \solvers -> do
     vm' <- EVM.Stepper.interpret (Fetch.oracle solvers rpcinfo) vm EVM.Stepper.runFully
-    when cmd.trace $ T.hPutStr stderr (showTraceTree dapp vm')
+    writeTraceDapp dapp vm'
     case vm'.result of
-      Just (VMFailure (Revert msg)) -> do
+      Just (VMFailure (Revert msg)) -> liftIO $ do
         let res = case msg of
                     ConcreteBuf bs -> bs
                     _ -> "<symbolic>"
         putStrLn $ "Revert: " <> (show $ ByteStringS res)
         exitWith (ExitFailure 2)
-      Just (VMFailure err) -> do
+      Just (VMFailure err) -> liftIO $ do
         putStrLn $ "Error: " <> show err
         exitWith (ExitFailure 2)
-      Just (Unfinished p) -> do
+      Just (Unfinished p) -> liftIO $ do
         putStrLn $ "Could not continue execution: " <> show p
         exitWith (ExitFailure 2)
-      Just (VMSuccess buf) -> do
+      Just (VMSuccess buf) -> liftIO $ do
         let msg = case buf of
               ConcreteBuf msg' -> msg'
               _ -> "<symbolic>"
@@ -585,7 +596,6 @@ unitTestOptions cmd solvers buildOutput = do
          Nothing  -> Nothing
     , maxIter = cmd.maxIterations
     , askSmtIters = cmd.askSmtIterations
-    , smtDebug = cmd.smtdebug
     , smtTimeout = cmd.smttimeout
     , solver = cmd.solver
     , verbose = cmd.verbose
diff --git a/hevm.cabal b/hevm.cabal
index ffd4fe7fa..79b58f745 100644
--- a/hevm.cabal
+++ b/hevm.cabal
@@ -99,6 +99,7 @@ library
     EVM.Types,
     EVM.UnitTest,
     EVM.Sign,
+    EVM.Effects,
   other-modules:
     Paths_hevm
   autogen-modules:
@@ -168,7 +169,8 @@ library
     stm                               >= 2.5.0 && < 2.6.0,
     spawn                             >= 0.3 && < 0.4,
     filepattern                       >= 0.1.2 && < 0.2,
-    witch                             >= 1.1 && < 1.3
+    witch                             >= 1.1 && < 1.3,
+    unliftio-core                     >= 0.2.1.0
   if !os(windows)
     build-depends:
       brick                           >= 1.4 && < 2.0,
@@ -224,7 +226,8 @@ executable hevm
     spawn,
     optics-core,
     githash                       >= 0.1.6 && < 0.2,
-    witch
+    witch,
+    unliftio-core
   if os(windows)
     buildable: False
 
@@ -277,7 +280,9 @@ common test-base
     operational,
     optics-core,
     optics-extra,
-    witch
+    witch,
+    unliftio-core,
+    exceptions
 
 library test-utils
   import:
@@ -370,4 +375,5 @@ benchmark bench
     filemanip,
     filepath,
     containers,
-    mtl
+    mtl,
+    unliftio-core
diff --git a/src/EVM/Effects.hs b/src/EVM/Effects.hs
new file mode 100644
index 000000000..2428f8700
--- /dev/null
+++ b/src/EVM/Effects.hs
@@ -0,0 +1,99 @@
+{-|
+Module      : Effects
+Description : Domain specific effects
+
+This module contains custom app specific mtl style effects for hevm
+These are written in the style of the ReaderT over IO pattern [1].
+Right now we only have a single `ReadConfig` effect, but over time hope to
+migrate most usages of IO into custom effects here.
+
+This framework would allow us to have multiple interpretations for effects
+(e.g. a pure version for tests), but for now we interpret everything in IO
+only.
+
+[1]: https://www.fpcomplete.com/blog/readert-design-pattern/
+-}
+
+{-# Language RankNTypes #-}
+{-# Language FlexibleInstances #-}
+{-# Language KindSignatures #-}
+{-# Language DataKinds #-}
+{-# Language GADTs #-}
+{-# Language DerivingStrategies #-}
+{-# Language DuplicateRecordFields #-}
+{-# Language NoFieldSelectors #-}
+{-# Language ConstraintKinds #-}
+
+module EVM.Effects where
+
+import Control.Monad.Reader
+import Control.Monad.IO.Unlift
+import EVM.Dapp (DappInfo)
+import EVM.Types (VM(..))
+import Control.Monad.ST (RealWorld)
+import Data.Text.IO qualified as T
+import EVM.Format (showTraceTree)
+import EVM (traceForest)
+
+-- Abstract Effects --------------------------------------------------------------------------------
+-- Here we define the abstract interface for the effects that we wish to model
+
+-- Global config
+class Monad m => ReadConfig m where
+  readConfig ::  m Config
+
+data Config = Config
+  { dumpQueries     :: Bool
+  , dumpExprs       :: Bool
+  , dumpEndStates   :: Bool
+  , debug           :: Bool
+  , abstRefineArith :: Bool
+  , abstRefineMem   :: Bool
+  , dumpTrace       :: Bool
+  }
+  deriving (Show, Eq)
+
+defaultConfig :: Config
+defaultConfig = Config
+  { dumpQueries = False
+  , dumpExprs = False
+  , dumpEndStates = False
+  , debug = False
+  , abstRefineArith = False
+  , abstRefineMem   = False
+  , dumpTrace = False
+  }
+
+writeTraceDapp :: App m => DappInfo -> VM RealWorld -> m ()
+writeTraceDapp dapp vm = do
+  conf <- readConfig
+  liftIO $ when conf.dumpTrace $ T.writeFile "VM.trace" (showTraceTree dapp vm)
+
+writeTrace :: App m => VM RealWorld -> m ()
+writeTrace vm = do
+  conf <- readConfig
+  liftIO $ when conf.dumpTrace $ writeFile "VM.trace" (show $ traceForest vm)
+
+-- IO Interpretation -------------------------------------------------------------------------------
+
+newtype Env = Env
+  { config :: Config
+  }
+
+defaultEnv :: Env
+defaultEnv = Env { config = defaultConfig }
+
+instance Monad m => ReadConfig (ReaderT Env m) where
+  readConfig = do
+    e <- ask
+    pure e.config
+
+runEnv :: Env -> ReaderT Env m a -> m a
+runEnv e a = runReaderT a e
+
+-- Helpful Aliases ---------------------------------------------------------------------------------
+
+type App m = (MonadUnliftIO m, ReadConfig m)
+
+runApp :: ReaderT Env m a -> m a
+runApp = runEnv defaultEnv
diff --git a/src/EVM/Fetch.hs b/src/EVM/Fetch.hs
index 4f61a3560..a3acc2ff7 100644
--- a/src/EVM/Fetch.hs
+++ b/src/EVM/Fetch.hs
@@ -27,6 +27,8 @@ import Network.Wreq.Session (Session)
 import Network.Wreq.Session qualified as Session
 import Numeric.Natural (Natural)
 import System.Process
+import Control.Monad.IO.Class
+import EVM.Effects
 
 -- | Abstract representation of an RPC fetch request
 data RpcQuery a where
@@ -182,23 +184,23 @@ fetchChainIdFrom url = do
   sess <- Session.newAPISession
   fetchQuery Latest (fetchWithSession url sess) QueryChainId
 
-http :: Natural -> Maybe Natural -> BlockNumber -> Text -> Fetcher s
+http :: Natural -> Maybe Natural -> BlockNumber -> Text -> Fetcher m s
 http smtjobs smttimeout n url q =
   withSolvers Z3 smtjobs smttimeout $ \s ->
     oracle s (Just (n, url)) q
 
-zero :: Natural -> Maybe Natural -> Fetcher s
+zero :: Natural -> Maybe Natural -> Fetcher m s
 zero smtjobs smttimeout q =
   withSolvers Z3 smtjobs smttimeout $ \s ->
     oracle s Nothing q
 
 -- smtsolving + (http or zero)
-oracle :: SolverGroup -> RpcInfo -> Fetcher s
+oracle :: SolverGroup -> RpcInfo -> Fetcher m s
 oracle solvers info q = do
   case q of
     PleaseDoFFI vals continue -> case vals of
        cmd : args -> do
-          (_, stdout', _) <- readProcessWithExitCode cmd args ""
+          (_, stdout', _) <- liftIO $ readProcessWithExitCode cmd args ""
           pure . continue . encodeAbiValue $
             AbiTuple (RegularVector.fromList [ AbiBytesDynamic . hexText . pack $ stdout'])
        _ -> internalError (show vals)
@@ -215,7 +217,7 @@ oracle solvers info q = do
             AbstractBase -> unknownContract (LitAddr addr)
             EmptyBase -> emptyContract
           in pure $ Just c
-        Just (n, url) -> fetchContractFrom n url addr
+        Just (n, url) -> liftIO $ fetchContractFrom n url addr
       case contract of
         Just x -> pure $ continue x
         Nothing -> internalError $ "oracle error: " ++ show q
@@ -224,27 +226,28 @@ oracle solvers info q = do
       case info of
         Nothing -> pure (continue 0)
         Just (n, url) ->
-         fetchSlotFrom n url addr slot >>= \case
+         liftIO $ fetchSlotFrom n url addr slot >>= \case
            Just x  -> pure (continue x)
            Nothing ->
              internalError $ "oracle error: " ++ show q
 
-type Fetcher s = Query s -> IO (EVM s ())
+type Fetcher m s = App m => Query s -> m (EVM s ())
 
 -- | Checks which branches are satisfiable, checking the pathconditions for consistency
 -- if the third argument is true.
 -- When in debug mode, we do not want to be able to navigate to dead paths,
 -- but for normal execution paths with inconsistent pathconditions
 -- will be pruned anyway.
-checkBranch :: SolverGroup -> Prop -> Prop -> IO BranchCondition
+checkBranch :: App m => SolverGroup -> Prop -> Prop -> m BranchCondition
 checkBranch solvers branchcondition pathconditions = do
-  checkSat solvers (assertProps abstRefineDefault [(branchcondition .&& pathconditions)]) >>= \case
+  conf <- readConfig
+  liftIO $ checkSat solvers (assertProps conf [(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))]) >>= \case
+    Sat _ -> do -- is its negation also possible?
+      checkSat solvers (assertProps conf [(pathconditions .&& (PNeg branchcondition))]) >>= \case
         -- No. The condition must hold
         Unsat -> pure $ Case True
         -- Yes. Both branches possible
diff --git a/src/EVM/Format.hs b/src/EVM/Format.hs
index 7a0b9c1c4..b5561bed4 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 b199031e2..ea223a963 100644
--- a/src/EVM/SMT.hs
+++ b/src/EVM/SMT.hs
@@ -31,7 +31,8 @@ import Language.SMT2.Parser (getValueRes, parseCommentFreeFileMsg)
 import Language.SMT2.Syntax (Symbol, SpecConstant(..), GeneralRes(..), Term(..), QualIdentifier(..), Identifier(..), Sort(..), Index(..), VarBinding(..))
 import Numeric (readHex, readBin)
 import Witch (into, unsafeInto)
-import Control.Monad.State
+import Control.Monad.State (State, runState, get, put)
+import EVM.Format (formatProp)
 
 import EVM.CSE
 import EVM.Expr (writeByte, bufLengthEnv, containsNode, bufLength, minLength, inRange)
@@ -39,6 +40,7 @@ import EVM.Expr qualified as Expr
 import EVM.Keccak (keccakAssumptions, keccakCompute)
 import EVM.Traversals
 import EVM.Types
+import EVM.Effects
 
 
 -- ** Encoding ** ----------------------------------------------------------------------------------
@@ -103,8 +105,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 +133,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.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
 declareIntermediates :: BufEnv -> StoreEnv -> SMT2
@@ -144,16 +155,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
@@ -161,21 +172,21 @@ data AbstState = AbstState
   }
   deriving (Show)
 
-abstractAwayProps :: AbstRefineConfig -> [Prop] -> ([Prop], AbstState)
-abstractAwayProps abstRefineConfig ps = runState (mapM abstrAway ps) (AbstState mempty 0)
+abstractAwayProps :: Config -> [Prop] -> ([Prop], AbstState)
+abstractAwayProps conf ps = runState (mapM abstrAway ps) (AbstState mempty 0)
   where
     abstrAway :: Prop -> State AbstState Prop
     abstrAway prop = mapPropM go prop
     go :: Expr a -> State AbstState (Expr a)
     go x = case x of
-        e@(Mod{})       | abstRefineConfig.arith  -> abstrExpr e
-        e@(SMod{})      | abstRefineConfig.arith  -> abstrExpr e
-        e@(MulMod{})    | abstRefineConfig.arith  -> abstrExpr e
-        e@(AddMod{})    | abstRefineConfig.arith  -> abstrExpr e
-        e@(Mul{})       | abstRefineConfig.arith  -> abstrExpr e
-        e@(Div{})       | abstRefineConfig.arith  -> abstrExpr e
-        e@(SDiv {})     | abstRefineConfig.arith  -> abstrExpr e
-        e@(ReadWord {}) | abstRefineConfig.mem -> abstrExpr e
+        e@(Mod{})       | conf.abstRefineArith  -> abstrExpr e
+        e@(SMod{})      | conf.abstRefineArith  -> abstrExpr e
+        e@(MulMod{})    | conf.abstRefineArith  -> abstrExpr e
+        e@(AddMod{})    | conf.abstRefineArith  -> abstrExpr e
+        e@(Mul{})       | conf.abstRefineArith  -> abstrExpr e
+        e@(Div{})       | conf.abstRefineArith  -> abstrExpr e
+        e@(SDiv {})     | conf.abstRefineArith  -> abstrExpr e
+        e@(ReadWord {}) | conf.abstRefineMem -> abstrExpr e
         e -> pure e
         where
             abstrExpr e = do
@@ -190,16 +201,17 @@ 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 :: Config -> [Prop] -> SMT2
+-- first simplify to rewrite sload/sstore combos, then concretize&simplify
 assertProps conf ps = assertPropsNoSimp conf (Expr.simplifyProps ps)
 
 -- Note: we need a version that does NOT call simplify or simplifyProps,
 -- because we make use of it to verify the correctness of our simplification
 -- passes through property-based testing.
-assertPropsNoSimp :: AbstRefineConfig -> [Prop] -> SMT2
-assertPropsNoSimp abstRefineConfig ps =
+assertPropsNoSimp :: Config -> [Prop] -> SMT2
+assertPropsNoSimp config ps =
   let encs = map propToSMT psElimAbst
       abstSMT = map propToSMT abstProps
       intermediates = declareIntermediates bufs stores in
@@ -221,14 +233,15 @@ 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
-    (psElimAbst, abst@(AbstState abstExprToInt _)) = if abstRefineConfig.arith || abstRefineConfig.mem
-      then abstractAwayProps abstRefineConfig psElim
+    (psElimAbst, abst@(AbstState abstExprToInt _)) = if config.abstRefineArith || config.abstRefineMem
+      then abstractAwayProps config psElim
       else (psElim, AbstState mempty 0)
 
     abstProps = map toProp (Map.toList abstExprToInt)
@@ -251,13 +264,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 +408,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 +417,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/Solidity.hs b/src/EVM/Solidity.hs
index 0e06a357b..9e6d2161b 100644
--- a/src/EVM/Solidity.hs
+++ b/src/EVM/Solidity.hs
@@ -48,6 +48,7 @@ import Optics.Operators.Unsafe
 
 import Control.Applicative
 import Control.Monad
+import Control.Monad.IO.Unlift
 import Data.Aeson hiding (json)
 import Data.Aeson.Types
 import Data.Aeson.Optics
@@ -366,14 +367,18 @@ yulRuntime contractName src = do
       bytecode = c ^?! key "evm" ^?! key "deployedBytecode" ^?! key "object" % _String
   pure $ (toCode contractName) <$> (Just bytecode)
 
-solidity :: Text -> Text -> IO (Maybe ByteString)
-solidity contract src = do
+solidity
+  :: (MonadUnliftIO m)
+  => Text -> Text -> m (Maybe ByteString)
+solidity contract src = liftIO $ do
   json <- solc Solidity src
   let (Contracts sol, _, _) = fromJust $ readStdJSON json
   pure $ Map.lookup ("hevm.sol:" <> contract) sol <&> (.creationCode)
 
-solcRuntime :: Text -> Text -> IO (Maybe ByteString)
-solcRuntime contract src = do
+solcRuntime
+  :: (MonadUnliftIO m)
+  => Text -> Text -> m (Maybe ByteString)
+solcRuntime contract src = liftIO $ do
   json <- solc Solidity src
   case readStdJSON json of
     Just (Contracts sol, _, _) -> pure $ Map.lookup ("hevm.sol:" <> contract) sol <&> (.runtimeCode)
diff --git a/src/EVM/Solvers.hs b/src/EVM/Solvers.hs
index 310f1743f..57b2daae2 100644
--- a/src/EVM/Solvers.hs
+++ b/src/EVM/Solvers.hs
@@ -12,6 +12,7 @@ import Control.Concurrent.Chan (Chan, newChan, writeChan, readChan)
 import Control.Concurrent (forkIO, killThread)
 import Control.Monad
 import Control.Monad.State.Strict
+import Control.Monad.IO.Unlift
 import Data.Char (isSpace)
 import Data.Map (Map)
 import Data.Map qualified as Map
@@ -23,6 +24,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 EVM.Effects
 
 import EVM.SMT
 import EVM.Types (W256, Expr(AbstractBuf), internalError)
@@ -88,59 +90,74 @@ checkSat (SolverGroup taskQueue) script = do
   -- collect result
   readChan resChan
 
-withSolvers :: Solver -> Natural -> Maybe Natural -> (SolverGroup -> IO a) -> IO a
+writeSMT2File :: SMT2 -> Int -> String -> IO ()
+writeSMT2File smt2 count abst =
+  do
+    let content = formatSMT2 smt2 <> "\n\n(check-sat)"
+    T.writeFile ("query-" <> (show count) <> "-" <> abst <> ".smt2") content
+
+withSolvers :: App m => Solver -> Natural -> Maybe Natural -> (SolverGroup -> m a) -> m a
 withSolvers solver count timeout cont = do
-  -- spawn solvers
-  instances <- mapM (const $ spawnSolver solver timeout) [1..count]
-  -- spawn orchestration thread
-  taskQueue <- newChan
-  availableInstances <- newChan
-  forM_ instances (writeChan availableInstances)
-  orchestrateId <- forkIO $ orchestrate taskQueue availableInstances
-
-  -- run continuation with task queue
-  res <- cont (SolverGroup taskQueue)
-
-  -- cleanup and return results
-  mapM_ stopSolver instances
-  killThread orchestrateId
-  pure res
+    -- spawn solvers
+    instances <- mapM (const $ liftIO $ spawnSolver solver timeout) [1..count]
+    -- spawn orchestration thread
+    taskQueue <- liftIO newChan
+    availableInstances <- liftIO newChan
+    liftIO $ forM_ instances (writeChan availableInstances)
+    orchestrate' <- toIO $ orchestrate taskQueue availableInstances 0
+    orchestrateId <- liftIO $ forkIO orchestrate'
+
+    -- run continuation with task queue
+    res <- cont (SolverGroup taskQueue)
+
+    -- cleanup and return results
+    liftIO $ mapM_ (stopSolver) instances
+    liftIO $ killThread orchestrateId
+    pure res
   where
-    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
-      -- reset solver and send all lines of provided script
-      out <- sendScript inst (SMT2 ("(reset)" : cmds) mempty mempty)
-      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)"
-          res <- do
-              case sat of
-                "unsat" -> pure Unsat
-                "timeout" -> pure Unknown
-                "unknown" -> pure Unknown
-                "sat" -> if null refineEqs then Sat <$> getModel inst cexvars
-                         else do
-                              _ <- sendScript inst (SMT2 refineEqs mempty mempty)
-                              sat2 <- sendLine inst "(check-sat)"
-                              case sat2 of
-                                "unsat" -> pure Unsat
-                                "timeout" -> pure Unknown
-                                "unknown" -> pure Unknown
-                                "sat" -> Sat <$> getModel inst cexvars
-                                _ -> pure . Error $ T.toStrict $ "Unable to parse solver output: " <> sat2
-                _ -> pure . Error $ T.toStrict $ "Unable to parse solver output: " <> sat
-          writeChan r res
-
-      -- put the instance back in the list of available instances
-      writeChan availableInstances inst
+    orchestrate :: App m => Chan Task -> Chan SolverInstance -> Int -> m b
+    orchestrate queue avail fileCounter = do
+      task <- liftIO $ readChan queue
+      inst <- liftIO $ readChan avail
+      runTask' <- toIO $ runTask task inst avail fileCounter
+      _ <- liftIO $ forkIO runTask'
+      orchestrate queue avail (fileCounter + 1)
+
+    runTask :: (MonadIO m, ReadConfig m) => Task -> SolverInstance -> Chan SolverInstance -> Int -> m ()
+    runTask (Task smt2@(SMT2 cmds (RefinementEqs refineEqs refps) cexvars ps) r) inst availableInstances fileCounter = do
+      conf <- readConfig
+      liftIO $ do
+        when (conf.dumpQueries) $ writeSMT2File smt2 fileCounter "abstracted"
+        -- reset solver and send all lines of provided script
+        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 "(check-sat)"
+            res <- do
+                case sat of
+                  "unsat" -> pure Unsat
+                  "timeout" -> pure Unknown
+                  "unknown" -> pure Unknown
+                  "sat" -> if null refineEqs then Sat <$> getModel inst cexvars
+                           else do
+                                let refinedSMT2 = SMT2 refineEqs mempty mempty (ps <> refps)
+                                writeSMT2File refinedSMT2 fileCounter "refined"
+                                _ <- sendScript inst refinedSMT2
+                                sat2 <- sendLine inst "(check-sat)"
+                                case sat2 of
+                                  "unsat" -> pure Unsat
+                                  "timeout" -> pure Unknown
+                                  "unknown" -> pure Unknown
+                                  "sat" -> Sat <$> getModel inst cexvars
+                                  _ -> pure . Error $ T.toStrict $ "Unable to parse solver output: " <> sat2
+                  _ -> pure . Error $ T.toStrict $ "Unable to parse solver output: " <> sat
+            writeChan r res
+
+        -- put the instance back in the list of available instances
+        writeChan availableInstances inst
 
 getModel :: SolverInstance -> CexVars -> IO SMTCex
 getModel inst cexvars = do
@@ -262,7 +279,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
diff --git a/src/EVM/Stepper.hs b/src/EVM/Stepper.hs
index c305f632b..591d50ec9 100644
--- a/src/EVM/Stepper.hs
+++ b/src/EVM/Stepper.hs
@@ -1,4 +1,7 @@
 {-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+
 
 module EVM.Stepper
   ( Action (..)
@@ -31,6 +34,8 @@ import EVM.Exec qualified
 import EVM.Fetch qualified as Fetch
 import EVM.Types
 import Control.Monad.ST (stToIO, RealWorld)
+import Control.Monad.IO.Class
+import EVM.Effects
 
 -- | The instruction type of the operational monad
 data Action s a where
@@ -104,30 +109,30 @@ runFully = do
 enter :: Text -> Stepper s ()
 enter t = evm (EVM.pushTrace (EntryTrace t))
 
-interpret :: Fetch.Fetcher RealWorld -> VM RealWorld -> Stepper RealWorld a -> IO a
+interpret :: forall m a . (App m) => Fetch.Fetcher m RealWorld -> VM RealWorld -> Stepper RealWorld a -> m a
 interpret fetcher vm = eval . view
   where
-    eval :: ProgramView (Action RealWorld) a -> IO a
+    eval :: ProgramView (Action RealWorld) a -> m a
     eval (Return x) = pure x
     eval (action :>>= k) =
       case action of
         Exec -> do
-          (r, vm') <- stToIO $ runStateT EVM.Exec.exec vm
+          (r, vm') <- liftIO $ stToIO $ runStateT EVM.Exec.exec vm
           interpret fetcher vm' (k r)
         Wait (PleaseAskSMT (Lit c) _ continue) -> do
-          (r, vm') <- stToIO $ runStateT (continue (Case (c > 0))) vm
+          (r, vm') <- liftIO $ stToIO $ runStateT (continue (Case (c > 0))) vm
           interpret fetcher vm' (k r)
         Wait (PleaseAskSMT c _ _) ->
           error $ "cannot handle symbolic branch conditions in this interpreter: " <> show c
         Wait q -> do
           m <- fetcher q
-          vm' <- stToIO $ execStateT m vm
+          vm' <- liftIO $ stToIO $ execStateT m vm
           interpret fetcher vm' (k ())
         Ask _ ->
           internalError "cannot make choices with this interpreter"
         IOAct m -> do
-          r <- m
+          r <- liftIO $ m
           interpret fetcher vm (k r)
         EVM m -> do
-          (r, vm') <- stToIO $ runStateT m vm
+          (r, vm') <- liftIO $ stToIO $ runStateT m vm
           interpret fetcher vm' (k r)
diff --git a/src/EVM/SymExec.hs b/src/EVM/SymExec.hs
index bf72308e2..906ed1cde 100644
--- a/src/EVM/SymExec.hs
+++ b/src/EVM/SymExec.hs
@@ -1,5 +1,6 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 
 module EVM.SymExec where
 
@@ -24,8 +25,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 +33,7 @@ import EVM.Fetch qualified as Fetch
 import EVM.ABI
 import EVM.Expr qualified as Expr
 import EVM.Format (formatExpr, formatPartial, showVal, bsToHex)
-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)
@@ -48,6 +47,8 @@ import GHC.Generics (Generic)
 import Optics.Core
 import Options.Generic (ParseField, ParseFields, ParseRecord)
 import Witch (into, unsafeInto)
+import EVM.Effects
+import Control.Monad.IO.Unlift
 
 data LoopHeuristic
   = Naive
@@ -73,11 +74,9 @@ isQed _ = False
 
 data VeriOpts = VeriOpts
   { simp :: Bool
-  , debug :: Bool
   , maxIter :: Maybe Integer
   , askSmtIters :: Integer
   , loopHeuristic :: LoopHeuristic
-  , abstRefineConfig :: AbstRefineConfig
   , rpcInfo :: Fetch.RpcInfo
   }
   deriving (Eq, Show)
@@ -85,23 +84,15 @@ data VeriOpts = VeriOpts
 defaultVeriOpts :: VeriOpts
 defaultVeriOpts = VeriOpts
   { simp = True
-  , debug = False
   , maxIter = Nothing
   , askSmtIters = 1
   , loopHeuristic = StackBased
-  , abstRefineConfig = abstRefineDefault
   , rpcInfo = Nothing
   }
 
 rpcVeriOpts :: (Fetch.BlockNumber, Text) -> VeriOpts
 rpcVeriOpts info = defaultVeriOpts { rpcInfo = Just info }
 
-debugVeriOpts :: VeriOpts
-debugVeriOpts = defaultVeriOpts { debug = True }
-
-debugAbstVeriOpts :: VeriOpts
-debugAbstVeriOpts = defaultVeriOpts { abstRefineConfig = AbstRefineConfig True True }
-
 extractCex :: VerifyResult -> Maybe (Expr End, SMTCex)
 extractCex (Cex c) = Just c
 extractCex _ = Nothing
@@ -241,45 +232,44 @@ loadSymVM x callvalue cd create =
 -- | Interpreter which explores all paths at branching points. Returns an
 -- 'Expr End' representing the possible executions.
 interpret
-  :: Fetch.Fetcher RealWorld
+  :: forall m . App m
+  =>  Fetch.Fetcher m RealWorld
   -> Maybe Integer -- max iterations
   -> Integer -- ask smt iterations
   -> LoopHeuristic
   -> VM RealWorld
   -> Stepper RealWorld (Expr End)
-  -> IO (Expr End)
+  -> m (Expr End)
 interpret fetcher maxIter askSmtIters heuristic vm =
   eval . Operational.view
   where
   eval
     :: Operational.ProgramView (Stepper.Action RealWorld) (Expr End)
-    -> IO (Expr End)
+    -> m (Expr End)
 
   eval (Operational.Return x) = pure x
 
   eval (action Operational.:>>= k) =
     case action of
       Stepper.Exec -> do
-        (r, vm') <- stToIO $ runStateT exec vm
+        (r, vm') <- liftIO $ stToIO $ runStateT exec vm
         interpret fetcher maxIter askSmtIters heuristic vm' (k r)
       Stepper.IOAct q -> do
-        r <- q
+        r <- liftIO q
         interpret fetcher maxIter askSmtIters heuristic vm (k r)
       Stepper.Ask (PleaseChoosePath cond continue) -> do
-        (a, b) <- concurrently
-          (do
-            (ra, vma) <- stToIO $ runStateT (continue True) vm { result = Nothing }
-            interpret fetcher maxIter askSmtIters heuristic vma (k ra)
-          )
-          (do
-            (rb, vmb) <- stToIO $ runStateT (continue False) vm { result = Nothing }
-            interpret fetcher maxIter askSmtIters heuristic vmb (k rb)
-          )
+        evalLeft <- toIO $ do
+          (ra, vma) <- liftIO $ stToIO $ runStateT (continue True) vm { result = Nothing }
+          interpret fetcher maxIter askSmtIters heuristic vma (k ra)
+        evalRight <- toIO $ do
+          (rb, vmb) <- liftIO $ stToIO $ runStateT (continue False) vm { result = Nothing }
+          interpret fetcher maxIter askSmtIters heuristic vmb (k rb)
+        (a, b) <- liftIO $ concurrently evalLeft evalRight
         pure $ ITE cond a b
       Stepper.Wait q -> do
         let performQuery = do
-              m <- liftIO (fetcher q)
-              (r, vm') <- stToIO $ runStateT m vm
+              m <- fetcher q
+              (r, vm') <- liftIO$ stToIO $ runStateT m vm
               interpret fetcher maxIter askSmtIters heuristic vm' (k r)
 
         case q of
@@ -297,7 +287,7 @@ interpret fetcher maxIter askSmtIters heuristic vm =
                     pure $ Partial vm.keccakEqs (Traces (Zipper.toForest vm.traces) vm.env.contracts) $ MaxIterationsReached vm.state.pc vm.state.contract
                   -- No. keep executing
                   _ -> do
-                    (r, vm') <- stToIO $ runStateT (continue (Case (c > 0))) vm
+                    (r, vm') <- liftIO $ stToIO $ runStateT (continue (Case (c > 0))) vm
                     interpret fetcher maxIter askSmtIters heuristic vm' (k r)
 
               -- the condition is symbolic
@@ -308,7 +298,7 @@ interpret fetcher maxIter askSmtIters heuristic vm =
                   (Just True, _, Just n) -> do
                     -- continue execution down the opposite branch than the one that
                     -- got us to this point and return a partial leaf for the other side
-                    (r, vm') <- stToIO $ runStateT (continue (Case $ not n)) vm
+                    (r, vm') <- liftIO $ stToIO $ runStateT (continue (Case $ not n)) vm
                     a <- interpret fetcher maxIter askSmtIters heuristic vm' (k r)
                     pure $ ITE cond a (Partial vm.keccakEqs (Traces (Zipper.toForest vm.traces) vm.env.contracts) (MaxIterationsReached vm.state.pc vm.state.contract))
                   -- we're in a loop and askSmtIters has been reached
@@ -318,14 +308,14 @@ interpret fetcher maxIter askSmtIters heuristic vm =
                   _ -> do
                     (r, vm') <- case simpProps of
                       -- if we can statically determine unsatisfiability then we skip exploring the jump
-                      [PBool False] -> stToIO $ runStateT (continue (Case False)) vm
+                      [PBool False] -> liftIO $ stToIO $ runStateT (continue (Case False)) vm
                       -- otherwise we explore both branches
-                      _ -> stToIO $ runStateT (continue EVM.Types.Unknown) vm
+                      _ -> liftIO $ stToIO $ runStateT (continue EVM.Types.Unknown) vm
                     interpret fetcher maxIter askSmtIters heuristic vm' (k r)
           _ -> performQuery
 
       Stepper.EVM m -> do
-        (r, vm') <- stToIO $ runStateT m vm
+        (r, vm') <- liftIO $ stToIO $ runStateT m vm
         interpret fetcher maxIter askSmtIters heuristic vm' (k r)
 
 maxIterationsReached :: VM s -> Maybe Integer -> Maybe Bool
@@ -366,25 +356,27 @@ type Precondition s = VM s -> Prop
 type Postcondition s = VM s -> Expr End -> Prop
 
 checkAssert
-  :: SolverGroup
+  :: App m
+  => SolverGroup
   -> [Word256]
   -> ByteString
   -> Maybe Sig
   -> [String]
   -> VeriOpts
-  -> IO (Expr End, [VerifyResult])
+  -> m (Expr End, [VerifyResult])
 checkAssert solvers errs c signature' concreteArgs opts =
   verifyContract solvers c signature' concreteArgs opts Nothing (Just $ checkAssertions errs)
 
 getExpr
-  :: SolverGroup
+  :: App m
+  => SolverGroup
   -> ByteString
   -> Maybe Sig
   -> [String]
   -> VeriOpts
-  -> IO (Expr End)
+  -> m (Expr End)
 getExpr solvers c signature' concreteArgs opts = do
-      preState <- stToIO $ abstractVM (mkCalldata signature' concreteArgs) c Nothing False
+      preState <- liftIO $ stToIO $ abstractVM (mkCalldata signature' concreteArgs) c Nothing False
       exprInter <- interpret (Fetch.oracle solvers opts.rpcInfo) opts.maxIter opts.askSmtIters opts.loopHeuristic preState runExpr
       if opts.simp then (pure $ Expr.simplify exprInter) else pure exprInter
 
@@ -439,16 +431,17 @@ mkCalldata (Just (Sig name types)) args =
   symCalldata name types args (AbstractBuf "txdata")
 
 verifyContract
-  :: SolverGroup
+  :: App m
+  => SolverGroup
   -> ByteString
   -> Maybe Sig
   -> [String]
   -> VeriOpts
   -> Maybe (Precondition RealWorld)
   -> Maybe (Postcondition RealWorld)
-  -> IO (Expr End, [VerifyResult])
+  -> m (Expr End, [VerifyResult])
 verifyContract solvers theCode signature' concreteArgs opts maybepre maybepost = do
-  preState <- stToIO $ abstractVM (mkCalldata signature' concreteArgs) theCode maybepre False
+  preState <- liftIO $ stToIO $ abstractVM (mkCalldata signature' concreteArgs) theCode maybepre False
   verify solvers opts preState maybepost
 
 -- | Stepper that parses the result of Stepper.runFully into an Expr End
@@ -488,9 +481,10 @@ flattenExpr = go []
 -- the incremental nature of the task at hand. Introducing support for
 -- incremental queries might let us go even faster here.
 -- TODO: handle errors properly
-reachable :: SolverGroup -> Expr End -> IO ([SMT2], Expr End)
+reachable :: App m => SolverGroup -> Expr End -> m ([SMT2], Expr End)
 reachable solvers e = do
-  res <- go [] e
+  conf <- readConfig
+  res <- liftIO $ go conf [] e
   pure $ second (fromMaybe (internalError "no reachable paths found")) res
   where
     {-
@@ -499,12 +493,12 @@ reachable solvers e = do
        If reachable return the expr wrapped in a Just. If not return Nothing.
        When walking back up the tree drop unreachable subbranches.
     -}
-    go :: [Prop] -> Expr End -> IO ([SMT2], Maybe (Expr End))
-    go pcs = \case
+    go :: Config -> [Prop] -> Expr End -> IO ([SMT2], Maybe (Expr End))
+    go conf pcs = \case
       ITE c t f -> do
         (tres, fres) <- concurrently
-          (go (PEq (Lit 1) c : pcs) t)
-          (go (PEq (Lit 0) c : pcs) f)
+          (go conf (PEq (Lit 1) c : pcs) t)
+          (go conf (PEq (Lit 0) c : pcs) f)
         let subexpr = case (snd tres, snd fres) of
               (Just t', Just f') -> Just $ ITE c t' f'
               (Just t', Nothing) -> Just t'
@@ -512,7 +506,7 @@ reachable solvers e = do
               (Nothing, Nothing) -> Nothing
         pure (fst tres <> fst fres, subexpr)
       leaf -> do
-        let query = assertProps abstRefineDefault pcs
+        let query = assertProps conf pcs
         res <- checkSat solvers query
         case res of
           Sat _ -> pure ([query], Just leaf)
@@ -543,57 +537,54 @@ getPartials = mapMaybe go
 -- | Symbolically execute the VM and check all endstates against the
 -- postcondition, if available.
 verify
-  :: SolverGroup
+  :: App m
+  => SolverGroup
   -> VeriOpts
   -> VM RealWorld
   -> Maybe (Postcondition RealWorld)
-  -> IO (Expr End, [VerifyResult])
+  -> m (Expr End, [VerifyResult])
 verify solvers opts preState maybepost = do
-  putStrLn "Exploring contract"
+  liftIO $ putStrLn "Exploring contract"
 
   exprInter <- interpret (Fetch.oracle solvers opts.rpcInfo) opts.maxIter opts.askSmtIters opts.loopHeuristic preState runExpr
-  when opts.debug $ T.writeFile "unsimplified.expr" (formatExpr exprInter)
-
-  putStrLn "Simplifying expression"
-  let expr = if opts.simp then (Expr.simplify exprInter) else exprInter
-  when opts.debug $ T.writeFile "simplified.expr" (formatExpr expr)
-
-  putStrLn $ "Explored contract (" <> show (Expr.numBranches expr) <> " branches)"
-
-  let flattened = flattenExpr expr
-  when (any isPartial flattened) $ do
-    T.putStrLn ""
-    T.putStrLn "WARNING: hevm was only able to partially explore the given contract due to the following issues:"
-    T.putStrLn ""
-    T.putStrLn . T.unlines . fmap (indent 2 . ("- " <>)) . fmap formatPartial . getPartials $ flattened
-
-  case maybepost of
-    Nothing -> pure (expr, [Qed ()])
-    Just post -> do
-      let
-        -- Filter out any leaves that can be statically shown to be safe
-        canViolate = flip filter flattened $
-          \leaf -> case Expr.simplifyProp (post preState leaf) of
-            PBool True -> False
-            _ -> True
-        assumes = preState.constraints
-        withQueries = canViolate <&> \leaf ->
-          (assertProps opts.abstRefineConfig (PNeg (post preState leaf) : assumes <> extractProps leaf), leaf)
-      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
-        pure (res, leaf)
-      let cexs = filter (\(res, _) -> not . isUnsat $ res) results
-      pure $ if Prelude.null cexs then (expr, [Qed ()]) else (expr, fmap toVRes cexs)
+  conf <- readConfig
+  when conf.dumpExprs $ liftIO $ T.writeFile "unsimplified.expr" (formatExpr exprInter)
+  liftIO $ do
+    putStrLn "Simplifying expression"
+    let expr = if opts.simp then (Expr.simplify exprInter) else exprInter
+    when conf.dumpExprs $ T.writeFile "simplified.expr" (formatExpr expr)
+
+    putStrLn $ "Explored contract (" <> show (Expr.numBranches expr) <> " branches)"
+
+    let flattened = flattenExpr expr
+    when (any isPartial flattened) $ do
+      T.putStrLn ""
+      T.putStrLn "WARNING: hevm was only able to partially explore the given contract due to the following issues:"
+      T.putStrLn ""
+      T.putStrLn . T.unlines . fmap (indent 2 . ("- " <>)) . fmap formatPartial . getPartials $ flattened
+
+    case maybepost of
+      Nothing -> pure (expr, [Qed ()])
+      Just post -> liftIO $ do
+        let
+          -- Filter out any leaves that can be statically shown to be safe
+          canViolate = flip filter flattened $
+            \leaf -> case Expr.simplifyProp (post preState leaf) of
+              PBool True -> False
+              _ -> True
+          assumes = preState.constraints
+          withQueries = canViolate <&> \leaf ->
+            (assertProps conf (PNeg (post preState leaf) : assumes <> extractProps leaf), leaf)
+        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
+          pure (res, leaf)
+        let cexs = filter (\(res, _) -> not . isUnsat $ res) results
+        pure $ if Prelude.null cexs then (expr, [Qed ()]) else (expr, fmap toVRes cexs)
   where
     toVRes :: (CheckSatResult, Expr End) -> VerifyResult
     toVRes (res, leaf) = case res of
@@ -623,54 +614,62 @@ type UnsatCache = TVar [Set Prop]
 -- equivalence break, and since we run this check for every pair of end states,
 -- the check is exhaustive.
 equivalenceCheck
-  :: SolverGroup -> ByteString -> ByteString -> VeriOpts -> (Expr Buf, [Prop])
-  -> IO [EquivResult]
+  :: forall m . App m
+  => SolverGroup
+  -> ByteString
+  -> ByteString
+  -> VeriOpts
+  -> (Expr Buf, [Prop])
+  -> m [EquivResult]
 equivalenceCheck solvers bytecodeA bytecodeB opts calldata = do
   case bytecodeA == bytecodeB of
-    True -> do
+    True -> liftIO $ do
       putStrLn "bytecodeA and bytecodeB are identical"
       pure [Qed ()]
     False -> do
       branchesA <- getBranches bytecodeA
       branchesB <- getBranches bytecodeB
-      equivalenceCheck' solvers branchesA branchesB opts
+      equivalenceCheck' solvers branchesA branchesB
   where
     -- decompiles the given bytecode into a list of branches
-    getBranches :: ByteString -> IO [Expr End]
+    getBranches :: ByteString -> m [Expr End]
     getBranches bs = do
       let bytecode = if BS.null bs then BS.pack [0] else bs
-      prestate <- stToIO $ abstractVM calldata bytecode Nothing False
+      prestate <- liftIO $ stToIO $ abstractVM calldata bytecode Nothing False
       expr <- interpret (Fetch.oracle solvers Nothing) opts.maxIter opts.askSmtIters opts.loopHeuristic prestate runExpr
       let simpl = if opts.simp then (Expr.simplify expr) else expr
       pure $ flattenExpr simpl
 
 
-equivalenceCheck' :: SolverGroup -> [Expr End] -> [Expr End] -> VeriOpts -> IO [EquivResult]
-equivalenceCheck' solvers branchesA branchesB opts = do
-      when (any isPartial branchesA || any isPartial branchesB) $ do
+equivalenceCheck'
+  :: forall m . App m
+  => SolverGroup -> [Expr End] -> [Expr End] -> m [EquivResult]
+equivalenceCheck' solvers branchesA branchesB = do
+      when (any isPartial branchesA || any isPartial branchesB) $ liftIO $ do
         putStrLn ""
         putStrLn "WARNING: hevm was only able to partially explore the given contract due to the following issues:"
         putStrLn ""
         T.putStrLn . T.unlines . fmap (indent 2 . ("- " <>)) . fmap formatPartial . nubOrd $ ((getPartials branchesA) <> (getPartials branchesB))
 
       let allPairs = [(a,b) | a <- branchesA, b <- branchesB]
-      putStrLn $ "Found " <> show (length allPairs) <> " total pairs of endstates"
+      liftIO $ putStrLn $ "Found " <> show (length allPairs) <> " total pairs of endstates"
 
-      when opts.debug $
+      conf <- readConfig
+      when conf.dumpEndStates $ liftIO $
         putStrLn $ "endstates in bytecodeA: " <> show (length branchesA)
                    <> "\nendstates in bytecodeB: " <> show (length branchesB)
 
       let differingEndStates = sortBySize (mapMaybe (uncurry distinct) allPairs)
-      putStrLn $ "Asking the SMT solver for " <> (show $ length differingEndStates) <> " pairs"
-      when opts.debug $ forM_ (zip differingEndStates [(1::Integer)..]) (\(x, i) ->
-        T.writeFile ("prop-checked-" <> show i) (T.pack $ show x))
+      liftIO $ putStrLn $ "Asking the SMT solver for " <> (show $ length differingEndStates) <> " pairs"
+      when conf.dumpEndStates $ forM_ (zip differingEndStates [(1::Integer)..]) (\(x, i) ->
+        liftIO $ T.writeFile ("prop-checked-" <> show i <> ".prop") (T.pack $ show x))
 
-      knownUnsat <- newTVarIO []
-      procs <- getNumProcessors
+      knownUnsat <- liftIO $ newTVarIO []
+      procs <- liftIO getNumProcessors
       results <- checkAll differingEndStates knownUnsat procs
 
       let useful = foldr (\(_, b) n -> if b then n+1 else n) (0::Integer) results
-      putStrLn $ "Reuse of previous queries was Useful in " <> (show useful) <> " cases"
+      liftIO $ putStrLn $ "Reuse of previous queries was Useful in " <> (show useful) <> " cases"
       case all isQed . fmap fst $ results of
         True -> pure [Qed ()]
         False -> pure $ filter (/= Qed ()) . fmap fst $ results
@@ -688,13 +687,9 @@ 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)
-      -- 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)")
-
+    check :: Config -> UnsatCache -> (Set Prop) -> IO (EquivResult, Bool)
+    check conf knownUnsat props = do
+      let smt = assertProps conf (Set.toList props)
       ku <- readTVarIO knownUnsat
       res <- if subsetAny props ku
              then pure (True, Unsat)
@@ -710,16 +705,17 @@ 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
     -- mapConcurrently which would spawn as many threads as there are jobs, and
     -- run them in a random order. We ordered them correctly, though so that'd be bad
-    checkAll :: [(Set Prop)] -> UnsatCache -> Int -> IO [(EquivResult, Bool)]
+    checkAll :: App m => [(Set Prop)] -> UnsatCache -> Int -> m [(EquivResult, Bool)]
     checkAll input cache numproc = do
-       wrap <- pool numproc
-       parMapIO (wrap . (uncurry $ check cache)) $ zip input [1..]
+       conf <- readConfig
+       wrap <- liftIO $ pool numproc
+       liftIO $ parMapIO (wrap . (check conf cache)) input
 
 
     -- Takes two branches and returns a set of props that will need to be
@@ -786,11 +782,12 @@ equivalenceCheck' solvers branchesA branchesB opts = do
 both' :: (a -> b) -> (a, a) -> (b, b)
 both' f (x, y) = (f x, f y)
 
-produceModels :: SolverGroup -> Expr End -> IO [(Expr End, CheckSatResult)]
+produceModels :: App m => SolverGroup -> Expr End -> m [(Expr End, CheckSatResult)]
 produceModels solvers expr = do
   let flattened = flattenExpr expr
-      withQueries = fmap (\e -> ((assertProps abstRefineDefault) . extractProps $ e, e)) flattened
-  results <- flip mapConcurrently withQueries $ \(query, leaf) -> do
+      withQueries conf = fmap (\e -> ((assertProps conf) . extractProps $ e, e)) flattened
+  conf <- readConfig
+  results <- liftIO $ (flip mapConcurrently) (withQueries conf) $ \(query, leaf) -> do
     res <- checkSat solvers query
     pure (res, leaf)
   pure $ fmap swap $ filter (\(res, _) -> not . isUnsat $ res) results
diff --git a/src/EVM/Types.hs b/src/EVM/Types.hs
index b5d0d4902..13296066e 100644
--- a/src/EVM/Types.hs
+++ b/src/EVM/Types.hs
@@ -621,15 +621,6 @@ data RuntimeConfig = RuntimeConfig
   }
   deriving (Show)
 
-abstRefineDefault :: AbstRefineConfig
-abstRefineDefault = AbstRefineConfig False False
-
-data AbstRefineConfig = AbstRefineConfig
-  { arith :: Bool
-  , mem   :: Bool
-  }
-  deriving (Show, Eq)
-
 -- | An entry in the VM's "call/create stack"
 data Frame s = Frame
   { context :: FrameContext
diff --git a/src/EVM/UnitTest.hs b/src/EVM/UnitTest.hs
index 477aab5ce..4267f5c99 100644
--- a/src/EVM/UnitTest.hs
+++ b/src/EVM/UnitTest.hs
@@ -43,6 +43,7 @@ import Data.Word (Word64)
 import GHC.Natural
 import System.IO (hFlush, stdout)
 import Witch (unsafeInto, into)
+import EVM.Effects
 
 data UnitTestOptions s = UnitTestOptions
   { rpcInfo     :: Fetch.RpcInfo
@@ -50,7 +51,6 @@ data UnitTestOptions s = UnitTestOptions
   , verbose     :: Maybe Int
   , maxIter     :: Maybe Integer
   , askSmtIters :: Integer
-  , smtDebug    :: Bool
   , smtTimeout  :: Maybe Natural
   , solver      :: Maybe Text
   , match       :: Text
@@ -96,14 +96,13 @@ type ABIMethod = Text
 -- | Generate VeriOpts from UnitTestOptions
 makeVeriOpts :: UnitTestOptions s -> VeriOpts
 makeVeriOpts opts =
-   defaultVeriOpts { debug = opts.smtDebug
-                   , maxIter = opts.maxIter
+   defaultVeriOpts { maxIter = opts.maxIter
                    , askSmtIters = opts.askSmtIters
                    , rpcInfo = opts.rpcInfo
                    }
 
 -- | Top level CLI endpoint for hevm test
-unitTest :: UnitTestOptions RealWorld -> Contracts -> IO Bool
+unitTest :: App m => UnitTestOptions RealWorld -> Contracts -> m Bool
 unitTest opts (Contracts cs) = do
   let unitTests = findUnitTests opts.match $ Map.elems cs
   results <- concatMapM (runUnitTestContract opts cs) unitTests
@@ -143,15 +142,16 @@ initializeUnitTest opts theContract = do
     _ -> popTrace
 
 runUnitTestContract
-  :: UnitTestOptions RealWorld
+  :: App m
+  => UnitTestOptions RealWorld
   -> Map Text SolcContract
   -> (Text, [Sig])
-  -> IO [Bool]
+  -> m [Bool]
 runUnitTestContract
   opts@(UnitTestOptions {..}) contractMap (name, testSigs) = do
 
   -- Print a header
-  putStrLn $ "Running " ++ show (length testSigs) ++ " tests for " ++ unpack name
+  liftIO $ putStrLn $ "Running " ++ show (length testSigs) ++ " tests for " ++ unpack name
 
   -- Look for the wanted contract by name from the Solidity info
   case Map.lookup name contractMap of
@@ -161,12 +161,13 @@ runUnitTestContract
 
     Just theContract -> do
       -- Construct the initial VM and begin the contract's constructor
-      vm0 <- stToIO $ initialUnitTestVm opts theContract
+      vm0 <- liftIO $ stToIO $ initialUnitTestVm opts theContract
       vm1 <- Stepper.interpret (Fetch.oracle solvers rpcInfo) vm0 $ do
         Stepper.enter name
         initializeUnitTest opts theContract
         Stepper.evm get
 
+      writeTraceDapp dapp vm1
       case vm1.result of
         Just (VMFailure _) -> liftIO $ do
           Text.putStrLn "\x1b[31m[BAIL]\x1b[0m setUp() "
@@ -179,22 +180,23 @@ runUnitTestContract
           -- Run all the test cases and print their status
           details <- forM testSigs $ \s -> do
             (result, detail) <- symRun opts vm1 s
-            Text.putStrLn result
+            liftIO $ Text.putStrLn result
             pure detail
 
           let running = rights details
               bailing = lefts details
 
-          tick "\n"
-          tick (Text.unlines (filter (not . Text.null) running))
-          tick (Text.unlines bailing)
+          liftIO $ do
+            tick "\n"
+            tick (Text.unlines (filter (not . Text.null) running))
+            tick (Text.unlines bailing)
 
           pure $ fmap isRight details
         _ -> internalError "setUp() did not end with a result"
 
 
 -- | Define the thread spawner for symbolic tests
-symRun :: UnitTestOptions RealWorld -> VM RealWorld -> Sig -> IO (Text, Either Text Text)
+symRun :: App m => UnitTestOptions RealWorld -> VM RealWorld -> Sig -> m (Text, Either Text Text)
 symRun opts@UnitTestOptions{..} vm (Sig testName types) = do
     let cd = symCalldata testName types [] (AbstractBuf "txdata")
         shouldFail = "proveFail" `isPrefixOf` testName
@@ -226,6 +228,7 @@ symRun opts@UnitTestOptions{..} vm (Sig testName types) = do
         pushTrace (EntryTrace testName)
         makeTxCall testParams cd
         get
+    writeTraceDapp dapp vm'
 
     -- check postconditions against vm
     (e, results) <- verify solvers (makeVeriOpts opts) vm' (Just postcondition)
diff --git a/test/BlockchainTests.hs b/test/BlockchainTests.hs
index 1d75ef993..5606ec2f9 100644
--- a/test/BlockchainTests.hs
+++ b/test/BlockchainTests.hs
@@ -1,9 +1,13 @@
 module Main where
 
-import EVM.Test.BlockchainTests
+import EVM.Test.BlockchainTests qualified  as BlockchainTests
 import Test.Tasty
+import EVM.Effects
+
+testEnv :: Env
+testEnv = Env { config = defaultConfig }
 
 main :: IO ()
 main = do
-  tests <- prepareTests
+  tests <- runEnv testEnv BlockchainTests.prepareTests
   defaultMain tests
diff --git a/test/EVM/Test/BlockchainTests.hs b/test/EVM/Test/BlockchainTests.hs
index 5415d2350..0b4971a96 100644
--- a/test/EVM/Test/BlockchainTests.hs
+++ b/test/EVM/Test/BlockchainTests.hs
@@ -7,7 +7,7 @@ import EVM.Fetch qualified
 import EVM.Format (hexText)
 import EVM.Stepper qualified
 import EVM.Transaction
-import EVM.Types hiding (Block, Case)
+import EVM.Types hiding (Block, Case, Env)
 import EVM.Test.Tracing (interpretWithTrace, VMTrace, compareTraces, EVMToolTraceOutput(..))
 
 import Optics.Core
@@ -15,6 +15,8 @@ import Control.Arrow ((***), (&&&))
 import Control.Monad
 import Control.Monad.ST (RealWorld, stToIO)
 import Control.Monad.State.Strict
+import Control.Monad.IO.Unlift
+import EVM.Effects
 import Data.Aeson ((.:), (.:?), FromJSON (..))
 import Data.Aeson qualified as JSON
 import Data.Aeson.Types qualified as JSON
@@ -62,38 +64,48 @@ data BlockchainCase = BlockchainCase
   , network :: String
   } deriving Show
 
+
+testEnv :: Env
+testEnv = Env { config = defaultConfig }
+
 main :: IO ()
 main = do
-  tests <- prepareTests
+  tests <- runEnv testEnv prepareTests
   defaultMain tests
 
-prepareTests :: IO TestTree
+prepareTests :: App m => m TestTree
 prepareTests = do
-  repo <- getEnv "HEVM_ETHEREUM_TESTS_REPO"
+  repo <- liftIO $ getEnv "HEVM_ETHEREUM_TESTS_REPO"
   let testsDir = "BlockchainTests/GeneralStateTests"
   let dir = repo </> testsDir
-  jsonFiles <- Find.find Find.always (Find.extension Find.==? ".json") dir
-  putStrLn "Loading and parsing json files from ethereum-tests..."
-  isCI <- isJust <$> lookupEnv "CI"
+  jsonFiles <- liftIO $ Find.find Find.always (Find.extension Find.==? ".json") dir
+  liftIO $ putStrLn "Loading and parsing json files from ethereum-tests..."
+  isCI <- liftIO $ isJust <$> lookupEnv "CI"
   let problematicTests = if isCI then commonProblematicTests <> ciProblematicTests else commonProblematicTests
   let ignoredFiles = if isCI then ciIgnoredFiles else []
   groups <- mapM (\f -> testGroup (makeRelative repo f) <$> (if any (`isInfixOf` f) ignoredFiles then pure [] else testsFromFile f problematicTests)) jsonFiles
-  putStrLn "Loaded."
+  liftIO $ putStrLn "Loaded."
   pure $ testGroup "ethereum-tests" groups
 
-testsFromFile :: String -> Map String (TestTree -> TestTree) -> IO [TestTree]
+testsFromFile
+  :: forall m . App m
+  => String -> Map String (TestTree -> TestTree) -> m [TestTree]
 testsFromFile file problematicTests = do
-  parsed <- parseBCSuite <$> LazyByteString.readFile file
+  parsed <- parseBCSuite <$> (liftIO $ LazyByteString.readFile file)
   case parsed of
    Left "No cases to check." -> pure [] -- error "no-cases ok"
    Left _err -> pure [] -- error _err
-   Right allTests -> pure $
-     (\(name, x) -> testCase' name $ runVMTest True (name, x)) <$> Map.toList allTests
+   Right allTests -> mapM runTest (Map.toList allTests)
   where
-  testCase' name assertion =
-    case Map.lookup name problematicTests of
-      Just f -> f (testCase name assertion)
-      Nothing -> testCase name assertion
+    runTest :: (String , Case) -> m TestTree
+    runTest (name, x) = do
+      exec <- toIO $ runVMTest True (name, x)
+      pure $ testCase' name exec
+    testCase' :: String -> Assertion -> TestTree
+    testCase' name assertion =
+      case Map.lookup name problematicTests of
+        Just f -> f (testCase name (liftIO assertion))
+        Nothing -> testCase name (liftIO assertion)
 
 -- CI has issues with some heaver tests, disable in bulk
 ciIgnoredFiles :: [String]
@@ -126,24 +138,34 @@ ciProblematicTests = Map.fromList
   , ("loopExp_d9g0v0_Shanghai", ignoreTest)
   ]
 
-runVMTest :: Bool -> (String, Case) -> IO ()
+runVMTest
+  :: App m
+  => Bool -> (String, Case) -> m ()
 runVMTest diffmode (_name, x) = do
-  vm0 <- vmForCase x
+  vm0 <- liftIO $ vmForCase x
   result <- EVM.Stepper.interpret (EVM.Fetch.zero 0 (Just 0)) vm0 EVM.Stepper.runFully
+  writeTrace result
   maybeReason <- checkExpectation diffmode x result
-  forM_ maybeReason assertFailure
+  liftIO $ forM_ maybeReason assertFailure
+
 
 -- | Run a vm test and output a geth style per opcode trace
-traceVMTest :: String -> String -> IO [VMTrace]
+traceVMTest
+  :: App m
+  => String -> String -> m [VMTrace]
 traceVMTest file test = do
-  repo <- getEnv "HEVM_ETHEREUM_TESTS_REPO"
-  Right allTests <- parseBCSuite <$> LazyByteString.readFile (repo </> file)
-  let x = case filter (\(name, _) -> name == test) $ Map.toList allTests of
+  repo <- liftIO $ getEnv "HEVM_ETHEREUM_TESTS_REPO"
+  allTests <- parseBCSuite <$> (liftIO $ LazyByteString.readFile (repo </> file))
+  let x = case filter (\(name, _) -> name == test) $ Map.toList (getRight allTests) of
         [(_, x')] -> x'
         _ -> internalError "test not found"
-  vm0 <- vmForCase x
+  vm0 <- liftIO $ vmForCase x
   (_, (_, ts)) <- runStateT (interpretWithTrace (EVM.Fetch.zero 0 (Just 0)) EVM.Stepper.runFully) (vm0, [])
   pure ts
+    where
+      getRight :: Either a b -> b
+      getRight (Right a) = a
+      getRight (Left _) = error "Not allowed"
 
 -- | Read a geth trace from disk
 readTrace :: FilePath -> IO (Either String EVMToolTraceOutput)
@@ -151,11 +173,14 @@ readTrace = JSON.eitherDecodeFileStrict
 
 -- | given a path to a test file, a test case from within that file, and a trace from geth from running that test, compare the traces and show where we differ
 -- This would need a few tweaks to geth to make this really usable (i.e. evm statetest show allow running a single test from within the test file).
-traceVsGeth :: String -> String -> FilePath -> IO ()
+traceVsGeth
+  :: App m
+  => String -> String -> FilePath -> m ()
 traceVsGeth file test gethTrace = do
   hevm <- traceVMTest file test
-  EVMToolTraceOutput ts _ <- fromJust <$> (JSON.decodeFileStrict gethTrace :: IO (Maybe EVMToolTraceOutput))
-  _ <- compareTraces hevm ts
+  decodedContents <- liftIO (JSON.decodeFileStrict gethTrace :: IO (Maybe EVMToolTraceOutput))
+  let EVMToolTraceOutput ts _ = fromJust decodedContents
+  _ <- liftIO $ compareTraces hevm ts
   pure ()
 
 splitEithers :: (Filterable f) => f (Either a b) -> (f a, f b)
@@ -200,13 +225,15 @@ checkStateFail diff x vm (okMoney, okNonce, okData, okCode) = do
     printContracts actual
   pure (unwords reason)
 
-checkExpectation :: Bool -> Case -> VM RealWorld -> IO (Maybe String)
+checkExpectation
+  :: App m
+  => Bool -> Case -> VM RealWorld -> m (Maybe String)
 checkExpectation diff x vm = do
   let expectation = x.testExpectation
       (okState, b2, b3, b4, b5) = checkExpectedContracts vm expectation
   if okState then
     pure Nothing
-  else
+  else liftIO $
     Just <$> checkStateFail diff x vm (b2, b3, b4, b5)
 
 -- quotient account state by nullness
diff --git a/test/EVM/Test/Tracing.hs b/test/EVM/Test/Tracing.hs
index 996345826..f378f6d0f 100644
--- a/test/EVM/Test/Tracing.hs
+++ b/test/EVM/Test/Tracing.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 
 {-|
 Module      : Tracing
@@ -14,8 +15,9 @@ module EVM.Test.Tracing where
 import Control.Monad (when)
 import Control.Monad.Operational qualified as Operational
 import Control.Monad.ST (RealWorld, ST, stToIO)
-import Control.Monad.State.Strict (StateT(..), liftIO)
+import Control.Monad.State.Strict (StateT(..))
 import Control.Monad.State.Strict qualified as State
+import Control.Monad.Reader (ReaderT)
 import Data.Aeson ((.:), (.:?))
 import Data.Aeson qualified as JSON
 import Data.ByteString (ByteString)
@@ -36,7 +38,7 @@ import Test.QuickCheck (elements)
 import Test.QuickCheck.Instances.Text()
 import Test.QuickCheck.Instances.Natural()
 import Test.QuickCheck.Instances.ByteString()
-import Test.Tasty (testGroup, TestTree)
+import Test.Tasty (testGroup, TestTree, TestName)
 import Test.Tasty.HUnit (assertEqual, testCase)
 import Test.Tasty.QuickCheck hiding (Failure, Success)
 import Witch (into, unsafeInto)
@@ -59,7 +61,9 @@ import EVM.Stepper qualified as Stepper
 import EVM.SymExec
 import EVM.Traversals (mapExpr)
 import EVM.Transaction qualified
-import EVM.Types
+import EVM.Types hiding (Env)
+import EVM.Effects
+import Control.Monad.IO.Unlift
 
 data VMTrace =
   VMTrace
@@ -295,7 +299,9 @@ evmSetup contr txData gaslimitExec = (txn, evmEnv, contrAlloc, fromAddress, toAd
     fromAddress = fromJust $ deriveAddr sk
     toAddress = 0x8A8eAFb1cf62BfBeb1741769DAE1a9dd47996192
 
-getHEVMRet :: OpContract -> ByteString -> Int -> IO (Either (EvmError, [VMTrace]) (Expr 'End, [VMTrace], VMTraceResult))
+getHEVMRet
+  :: App m
+  => OpContract -> ByteString -> Int -> m (Either (EvmError, [VMTrace]) (Expr 'End, [VMTrace], VMTraceResult))
 getHEVMRet contr txData gaslimitExec = do
   let (txn, evmEnv, contrAlloc, fromAddress, toAddress, _) = evmSetup contr txData gaslimitExec
   runCodeWithTrace Nothing evmEnv contrAlloc txn (LitAddr fromAddress) (LitAddr toAddress)
@@ -413,13 +419,15 @@ symbolify vm = vm { state = vm.state { calldata = AbstractBuf "calldata" } }
 
 -- | Takes a runtime code and calls it with the provided calldata
 --   Uses evmtool's alloc and transaction to set up the VM correctly
-runCodeWithTrace :: Fetch.RpcInfo -> EVMToolEnv -> EVMToolAlloc -> EVM.Transaction.Transaction -> Expr EAddr -> Expr EAddr -> IO (Either (EvmError, [VMTrace]) ((Expr 'End, [VMTrace], VMTraceResult)))
+runCodeWithTrace
+  :: App m
+  => Fetch.RpcInfo -> EVMToolEnv -> EVMToolAlloc -> EVM.Transaction.Transaction
+  -> Expr EAddr -> Expr EAddr -> m (Either (EvmError, [VMTrace]) ((Expr 'End, [VMTrace], VMTraceResult)))
 runCodeWithTrace rpcinfo evmEnv alloc txn fromAddr toAddress = withSolvers Z3 0 Nothing $ \solvers -> do
   let calldata' = ConcreteBuf txn.txdata
       code' = alloc.code
-      buildExpr :: SolverGroup -> VM RealWorld -> IO (Expr End)
       buildExpr s vm = interpret (Fetch.oracle s Nothing) Nothing 1 Naive vm runExpr
-  origVM <- stToIO $ vmForRuntimeCode code' calldata' evmEnv alloc txn fromAddr toAddress
+  origVM <- liftIO $ stToIO $ vmForRuntimeCode code' calldata' evmEnv alloc txn fromAddr toAddress
 
   expr <- buildExpr solvers $ symbolify origVM
   (res, (vm, trace)) <- runStateT (interpretWithTrace (Fetch.oracle solvers rpcinfo) Stepper.execFully) (origVM, [])
@@ -460,9 +468,9 @@ vmForRuntimeCode runtimecode calldata' evmToolEnv alloc txn fromAddr toAddress =
              (Just (initialContract (RuntimeCode (ConcreteRuntimeCode BS.empty))))
        <&> set (#state % #calldata) calldata'
 
-runCode :: Fetch.RpcInfo -> ByteString -> Expr Buf -> IO (Maybe (Expr Buf))
+runCode :: App m => Fetch.RpcInfo -> ByteString -> Expr Buf -> m (Maybe (Expr Buf))
 runCode rpcinfo code' calldata' = withSolvers Z3 0 Nothing $ \solvers -> do
-  origVM <- stToIO $ vmForRuntimeCode
+  origVM <- liftIO $ stToIO $ vmForRuntimeCode
               code'
               calldata'
               emptyEvmToolEnv
@@ -530,12 +538,12 @@ vmres vm =
 
 type TraceState s = (VM s, [VMTrace])
 
-execWithTrace :: StateT (TraceState RealWorld) IO (VMResult RealWorld)
+execWithTrace :: App m => StateT (TraceState RealWorld) m (VMResult RealWorld)
 execWithTrace = do
   _ <- runWithTrace
   fromJust <$> use (_1 % #result)
 
-runWithTrace :: StateT (TraceState RealWorld) IO (VM RealWorld)
+runWithTrace :: App m => StateT (TraceState RealWorld) m (VM RealWorld)
 runWithTrace = do
   -- This is just like `exec` except for every instruction evaluated,
   -- we also increment a counter indexed by the current code location.
@@ -556,20 +564,18 @@ runWithTrace = do
     Just _ -> pure vm0
 
 interpretWithTrace
-  :: Fetch.Fetcher RealWorld
+  :: forall m a . App m
+  => Fetch.Fetcher m RealWorld
   -> Stepper.Stepper RealWorld a
-  -> StateT (TraceState RealWorld) IO a
+  -> StateT (TraceState RealWorld) m a
 interpretWithTrace fetcher =
   eval . Operational.view
-
   where
     eval
-      :: Operational.ProgramView (Stepper.Action RealWorld) a
-      -> StateT (TraceState RealWorld) IO a
-
-    eval (Operational.Return x) =
-      pure x
-
+      :: App m
+      => Operational.ProgramView (Stepper.Action RealWorld) a
+      -> StateT (TraceState RealWorld) m a
+    eval (Operational.Return x) = pure x
     eval (action Operational.:>>= k) =
       case action of
         Stepper.Exec ->
@@ -578,7 +584,7 @@ interpretWithTrace fetcher =
           PleaseAskSMT (Lit x) _ continue ->
             interpretWithTrace fetcher (Stepper.evm (continue (Case (x > 0))) >>= k)
           _ -> do
-            m <- liftIO (fetcher q)
+            m <- State.lift $ fetcher q
             vm <- use _1
             vm' <- liftIO $ stToIO $ State.execStateT m vm
             assign _1 vm'
@@ -820,29 +826,38 @@ getOp vm =
   in if xs == BS.empty then 0
                        else BS.head xs
 
+testEnv :: Env
+testEnv = Env { config = defaultConfig }
+
+test :: TestName -> ReaderT Env IO () -> TestTree
+test a b = testCase a $ runEnv testEnv b
+
+prop:: Testable prop => ReaderT Env IO prop -> Property
+prop a = ioProperty $ runEnv testEnv a
+
 tests :: TestTree
 tests = testGroup "contract-quickcheck-run"
-    [ testProperty "random-contract-concrete-call" $ \(contr :: OpContract, GasLimitInt gasLimit, TxDataRaw txDataRaw) -> ioProperty $ do
+    [ testProperty "random-contract-concrete-call" $ \(contr :: OpContract, GasLimitInt gasLimit, TxDataRaw txDataRaw) -> prop $ do
         let txData = BS.pack $ toEnum <$> txDataRaw
         -- TODO: By removing external calls, we fuzz less
         --       It should work also when we external calls. Removing for now.
-        contrFixed <- fixContractJumps $ removeExtcalls contr
+        contrFixed <- liftIO $ fixContractJumps $ removeExtcalls contr
         checkTraceAndOutputs contrFixed gasLimit txData
-      , testCase "calldata-wraparound" $ do
+      , test "calldata-wraparound" $ do
         let contract = OpContract $ concat
               [ [OpPush (Lit 0xff),OpPush (Lit 31),OpMstore8] -- value, offs
               , [OpPush (Lit 0x3),OpPush (Lit 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff),OpPush (Lit 0x0),OpCalldatacopy] -- size, offs, destOffs
               , [OpPush (Lit 0x20),OpPush (Lit 0),OpReturn] -- datasize, offs
               ]
         checkTraceAndOutputs contract 40000 (BS.pack [1, 2, 3, 4, 5])
-      , testCase "calldata-wraparound2" $ do
+      , test "calldata-wraparound2" $ do
         let contract = OpContract $ concat
               [ [OpPush (Lit 0xff),OpPush (Lit 0),OpMstore8] -- value, offs
               , [OpPush (Lit 0x10),OpPush (Lit 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff),OpPush (Lit 0x0),OpCalldatacopy] -- size, offs, destOffs
               , [OpPush (Lit 0x20),OpPush (Lit 0),OpReturn] -- datasize, offs
               ]
         checkTraceAndOutputs contract 40000 (BS.pack [1, 2, 3, 4, 5])
-      , testCase "calldata-overwrite-with-0-if-oversized" $ do
+      , test "calldata-overwrite-with-0-if-oversized" $ do
         -- supposed to copy 1...6 and then 0s, overwriting the 0xff with 0
         let contract = OpContract $ concat
               [ [OpPush (Lit 0xff),OpPush (Lit 1),OpMstore8] -- value, offs
@@ -850,14 +865,14 @@ tests = testGroup "contract-quickcheck-run"
               , [OpPush (Lit 10),OpPush (Lit 0x0),OpReturn] -- datasize, offset
               ]
         checkTraceAndOutputs contract 40000 (BS.pack [1, 2, 3, 4, 5, 6])
-      , testCase "calldata-overwrite-correct-size" $ do
+      , test "calldata-overwrite-correct-size" $ do
         let contract = OpContract $ concat
               [ [OpPush (Lit 0xff),OpPush (Lit 8),OpMstore8] -- value, offs
               , [OpPush (Lit 10),OpPush (Lit 0),OpPush (Lit 0), OpCalldatacopy] -- size, offs, destOffs
               , [OpPush (Lit 10),OpPush (Lit 0x0),OpReturn] -- datasize, offset
               ]
         checkTraceAndOutputs contract 40000 (BS.pack [1, 2, 3, 4, 5, 6])
-      , testCase "calldata-offset-copy" $ do
+      , test "calldata-offset-copy" $ do
         let contract = OpContract $ concat
               [ [OpPush (Lit 0xff),OpPush (Lit 8),OpMstore8] -- value, offs
               , [OpPush (Lit 0xff),OpPush (Lit 1),OpMstore8] -- value, offs
@@ -867,13 +882,13 @@ tests = testGroup "contract-quickcheck-run"
         checkTraceAndOutputs contract 40000 (BS.pack [1, 2, 3, 4, 5, 6])
     ]
 
-checkTraceAndOutputs :: OpContract -> Int -> ByteString -> IO ()
+checkTraceAndOutputs :: App m => OpContract -> Int -> ByteString -> m ()
 checkTraceAndOutputs contract gasLimit txData = do
-  evmtoolResult <- getEVMToolRet contract txData gasLimit
+  evmtoolResult <- liftIO $ getEVMToolRet contract txData gasLimit
   hevmRun <- getHEVMRet contract txData gasLimit
-  (Just evmtoolTraceOutput) <- getTraceOutput evmtoolResult
+  evmtoolTraceOutput <- fmap fromJust $ liftIO $ getTraceOutput evmtoolResult
   case hevmRun of
-    (Right (expr, hevmTrace, hevmTraceResult)) -> do
+    (Right (expr, hevmTrace, hevmTraceResult)) -> liftIO $ do
       let
         concretize :: Expr a -> Expr Buf -> Expr a
         concretize a c = mapExpr go a
@@ -893,7 +908,7 @@ checkTraceAndOutputs contract gasLimit txData = do
       -- putStrLn $ "evmtool trace: " <> show (evmtoolTraceOutput.trace)
       assertEqual "Traces and gas must match" traceOK True
       let resultOK = evmtoolTraceOutput.output.output == hevmTraceResult.out
-      if resultOK then do
+      if resultOK then liftIO $ do
         putStrLn $ "HEVM & evmtool's outputs match: '" <> (bsToHex $ bssToBs evmtoolTraceOutput.output.output) <> "'"
         if isNothing simplConcrExprRetval || (fromJust simplConcrExprRetval) == (bssToBs hevmTraceResult.out)
            then do
@@ -916,18 +931,19 @@ checkTraceAndOutputs contract gasLimit txData = do
         putStrLn $ "HEVM result len: " <> (show (BS.length $ bssToBs hevmTraceResult.out))
         putStrLn $ "evm result  len: " <> (show (BS.length $ bssToBs evmtoolTraceOutput.output.output))
       assertEqual "Contract exec successful. HEVM & evmtool's outputs must match" resultOK True
-    Left (evmerr, hevmTrace) -> do
+    Left (evmerr, hevmTrace) -> liftIO $ do
       putStrLn $ "HEVM contract exec issue: " <> (show evmerr)
       -- putStrLn $ "evmtool result was: " <> show (fromJust evmtoolResult)
       -- putStrLn $ "output by evmtool is: '" <> bsToHex evmtoolTraceOutput.toOutput.output <> "'"
       traceOK <- compareTraces hevmTrace (evmtoolTraceOutput.trace)
       assertEqual "Traces and gas must match" traceOK True
-  System.Directory.removeFile "txs.json"
-  System.Directory.removeFile "alloc-out.json"
-  System.Directory.removeFile "alloc.json"
-  System.Directory.removeFile "result.json"
-  System.Directory.removeFile "env.json"
-  deleteTraceOutputFiles evmtoolResult
+  liftIO $ do
+    System.Directory.removeFile "txs.json"
+    System.Directory.removeFile "alloc-out.json"
+    System.Directory.removeFile "alloc.json"
+    System.Directory.removeFile "result.json"
+    System.Directory.removeFile "env.json"
+    deleteTraceOutputFiles evmtoolResult
 
 -- GasLimitInt
 newtype GasLimitInt = GasLimitInt (Int)
diff --git a/test/EVM/Test/Utils.hs b/test/EVM/Test/Utils.hs
index ce079f253..6374db06b 100644
--- a/test/EVM/Test/Utils.hs
+++ b/test/EVM/Test/Utils.hs
@@ -20,18 +20,25 @@ import EVM.Solidity
 import EVM.Solvers
 import EVM.UnitTest
 import Control.Monad.ST (RealWorld)
+import Control.Monad.IO.Unlift
+import Control.Monad.Catch (MonadMask)
+import EVM.Effects
 
-runSolidityTestCustom :: FilePath -> Text -> Maybe Natural -> Maybe Integer -> Bool -> RpcInfo -> ProjectType -> IO Bool
+runSolidityTestCustom
+  :: (MonadMask m, App m)
+  => FilePath -> Text -> Maybe Natural -> Maybe Integer -> Bool -> RpcInfo -> ProjectType -> m Bool
 runSolidityTestCustom testFile match timeout maxIter ffiAllowed rpcinfo projectType = do
   withSystemTempDirectory "dapp-test" $ \root -> do
-    compile projectType root testFile >>= \case
+    (liftIO $ compile projectType root testFile) >>= \case
       Left e -> error e
       Right bo@(BuildOutput contracts _) -> do
         withSolvers Z3 1 timeout $ \solvers -> do
-          opts <- testOpts solvers root (Just bo) match maxIter ffiAllowed rpcinfo
+          opts <- liftIO $ testOpts solvers root (Just bo) match maxIter ffiAllowed rpcinfo
           unitTest opts contracts
 
-runSolidityTest :: FilePath -> Text -> IO Bool
+runSolidityTest
+  :: (MonadMask m, App m)
+  => FilePath -> Text -> m Bool
 runSolidityTest testFile match = runSolidityTestCustom testFile match Nothing Nothing True Nothing Foundry
 
 testOpts :: SolverGroup -> FilePath -> Maybe BuildOutput -> Text -> Maybe Integer -> Bool -> RpcInfo -> IO (UnitTestOptions RealWorld)
@@ -45,7 +52,6 @@ testOpts solvers root buildOutput match maxIter allowFFI rpcinfo = do
     , rpcInfo = rpcinfo
     , maxIter = maxIter
     , askSmtIters = 1
-    , smtDebug = False
     , smtTimeout = Nothing
     , solver = Nothing
     , verbose = Just 1
diff --git a/test/rpc.hs b/test/rpc.hs
index 1aefb453a..1d8d4fb2f 100644
--- a/test/rpc.hs
+++ b/test/rpc.hs
@@ -20,8 +20,17 @@ import EVM.Stepper qualified as Stepper
 import EVM.SymExec
 import EVM.Test.Utils
 import EVM.Solidity (ProjectType(..))
-import EVM.Types hiding (BlockNumber)
+import EVM.Types hiding (BlockNumber, Env)
 import Control.Monad.ST (stToIO, RealWorld)
+import Control.Monad.Reader (ReaderT)
+import Control.Monad.IO.Unlift
+import EVM.Effects
+
+rpcEnv :: Env
+rpcEnv = Env { config = defaultConfig }
+
+test :: TestName -> ReaderT Env IO () -> TestTree
+test a b = testCase a $ runEnv rpcEnv b
 
 main :: IO ()
 main = defaultMain tests
@@ -60,18 +69,19 @@ tests = testGroup "rpc"
     ]
   , testGroup "execution with remote state"
     -- execute against remote state from a ds-test harness
-    [ testCase "dapp-test" $ do
+    [ test "dapp-test" $ do
         let testFile = "test/contracts/pass/rpc.sol"
-        runSolidityTestCustom testFile ".*" Nothing Nothing False testRpcInfo Foundry >>= assertEqual "test result" True
+        res <- runSolidityTestCustom testFile ".*" Nothing Nothing False testRpcInfo Foundry
+        liftIO $ assertEqual "test result" True res
 
     -- concretely exec "transfer" on WETH9 using remote rpc
     -- https://etherscan.io/token/0xc02aaa39b223fe8d0a0e5c4f27ead9083c756cc2#code
-    , testCase "weth-conc" $ do
+    , test "weth-conc" $ do
         let
           blockNum = 16198552
           wad = 0x999999999999999999
           calldata' = ConcreteBuf $ abiMethod "transfer(address,uint256)" (AbiTuple (V.fromList [AbiAddress (Addr 0xdead), AbiUInt 256 wad]))
-        vm <- weth9VM blockNum (calldata', [])
+        vm <- liftIO $ weth9VM blockNum (calldata', [])
         postVm <- withSolvers Z3 1 Nothing $ \solvers ->
           Stepper.interpret (oracle solvers (Just (BlockNumber blockNum, testRpc))) vm Stepper.runFully
         let
@@ -83,21 +93,22 @@ tests = testGroup "rpc"
           msg = case postVm.result of
             Just (VMSuccess m) -> m
             _ -> internalError "VMSuccess expected"
-        assertEqual "should succeed" msg (ConcreteBuf $ word256Bytes 0x1)
-        assertEqual "should revert" receiverBal (W256 $ 2595433725034301 + wad)
+        liftIO $ do
+          assertEqual "should succeed" msg (ConcreteBuf $ word256Bytes 0x1)
+          assertEqual "should revert" receiverBal (W256 $ 2595433725034301 + wad)
 
     -- symbolically exec "transfer" on WETH9 using remote rpc
     -- https://etherscan.io/token/0xc02aaa39b223fe8d0a0e5c4f27ead9083c756cc2#code
-    , testCase "weth-sym" $ do
+    , test "weth-sym" $ do
         let
           blockNum = 16198552
           calldata' = symCalldata "transfer(address,uint256)" [AbiAddressType, AbiUIntType 256] ["0xdead"] (AbstractBuf "txdata")
           postc _ (Failure _ _ (Revert _)) = PBool False
           postc _ _ = PBool True
-        vm <- weth9VM blockNum calldata'
+        vm <- liftIO $ weth9VM blockNum calldata'
         (_, [Cex (_, model)]) <- withSolvers Z3 1 Nothing $ \solvers ->
           verify solvers (rpcVeriOpts (BlockNumber blockNum, testRpc)) vm (Just postc)
-        assertBool "model should exceed caller balance" (getVar model "arg2" >= 695836005599316055372648)
+        liftIO $ assertBool "model should exceed caller balance" (getVar model "arg2" >= 695836005599316055372648)
     ]
   ]
 
diff --git a/test/test.hs b/test/test.hs
index 100169799..826b6f766 100644
--- a/test/test.hs
+++ b/test/test.hs
@@ -9,6 +9,8 @@ import GHC.TypeLits
 import Data.Proxy
 import Control.Monad.ST (RealWorld, stToIO)
 import Control.Monad.State.Strict
+import Control.Monad.IO.Unlift
+import Control.Monad.Reader (ReaderT)
 import Data.Bits hiding (And, Xor)
 import Data.ByteString (ByteString)
 import Data.ByteString qualified as BS
@@ -63,7 +65,36 @@ import EVM.SymExec
 import EVM.Test.Tracing qualified as Tracing
 import EVM.Test.Utils
 import EVM.Traversals
-import EVM.Types
+import EVM.Types hiding (Env)
+import EVM.Effects
+
+testEnv :: Env
+testEnv = Env { config = defaultConfig {
+  dumpQueries = False
+  , dumpExprs = False
+  , dumpEndStates = False
+  , debug = False
+  , abstRefineArith = False
+  , abstRefineMem   = False
+  , dumpTrace = False
+  } }
+
+putStrLnM :: (MonadUnliftIO m) => String -> m ()
+putStrLnM a = liftIO $ putStrLn a
+
+assertEqualM :: (App m, Eq a, Show a, HasCallStack) => String -> a -> a -> m ()
+assertEqualM a b c = liftIO $ assertEqual a b c
+
+assertBoolM
+  :: (MonadUnliftIO m, HasCallStack)
+  => String -> Bool -> m ()
+assertBoolM a b = liftIO $ assertBool a b
+
+test :: TestName -> ReaderT Env IO () -> TestTree
+test a b = testCase a $ runEnv testEnv b
+
+prop :: Testable prop => ReaderT Env IO prop -> Property
+prop a = ioProperty $ runEnv testEnv a
 
 main :: IO ()
 main = defaultMain tests
@@ -77,7 +108,7 @@ tests :: TestTree
 tests = testGroup "hevm"
   [ Tracing.tests
   , testGroup "simplify-storage"
-    [ testCase "simplify-storage-array-only-static" $ do
+    [ test "simplify-storage-array-only-static" $ do
        Just c <- solcRuntime "MyContract"
         [i|
         contract MyContract {
@@ -91,13 +122,13 @@ tests = testGroup "hevm"
           }
         }
         |]
-       expr <- withSolvers Z3 1 Nothing $ \s -> getExpr s c (Just (Sig "transfer(uint256,uint256,uint256)" [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) [] debugVeriOpts
-       assertEqual "Expression is not clean." (badStoresInExpr expr) False
+       expr <- withSolvers Z3 1 Nothing $ \s -> getExpr s c (Just (Sig "transfer(uint256,uint256,uint256)" [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
+       assertEqualM "Expression is not clean." (badStoresInExpr expr) False
     -- This case is somewhat artificial. We can't simplify this using only
     -- static rewrite rules, because acct is totally abstract and acct + 1
     -- could overflow back to zero. we may be able to do better if we have some
     -- smt assisted simplification that can take branch conditions into account.
-    , expectFail $ testCase "simplify-storage-array-symbolic-index" $ do
+    , expectFail $ test "simplify-storage-array-symbolic-index" $ do
        Just c <- solcRuntime "MyContract"
         [i|
         contract MyContract {
@@ -111,10 +142,10 @@ tests = testGroup "hevm"
           }
         }
         |]
-       expr <- withSolvers Z3 1 Nothing $ \s -> getExpr s c (Just (Sig "transfer(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] debugVeriOpts
+       expr <- withSolvers Z3 1 Nothing $ \s -> getExpr s c (Just (Sig "transfer(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
        -- T.writeFile "symbolic-index.expr" $ formatExpr expr
-       assertEqual "Expression is not clean." (badStoresInExpr expr) False
-    , expectFail $ testCase "simplify-storage-array-of-struct-symbolic-index" $ do
+       assertEqualM "Expression is not clean." (badStoresInExpr expr) False
+    , expectFail $ test "simplify-storage-array-of-struct-symbolic-index" $ do
        Just c <- solcRuntime "MyContract"
         [i|
         contract MyContract {
@@ -132,9 +163,9 @@ tests = testGroup "hevm"
           }
         }
         |]
-       expr <- withSolvers Z3 1 Nothing $ \s -> getExpr s c (Just (Sig "transfer(uint256,uint256,uint256)" [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) [] debugVeriOpts
-       assertEqual "Expression is not clean." (badStoresInExpr expr) False
-    , testCase "simplify-storage-array-loop-nonstruct" $ do
+       expr <- withSolvers Z3 1 Nothing $ \s -> getExpr s c (Just (Sig "transfer(uint256,uint256,uint256)" [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
+       assertEqualM "Expression is not clean." (badStoresInExpr expr) False
+    , test "simplify-storage-array-loop-nonstruct" $ do
        Just c <- solcRuntime "MyContract"
         [i|
         contract MyContract {
@@ -147,9 +178,9 @@ tests = testGroup "hevm"
           }
         }
         |]
-       expr <- withSolvers Z3 1 Nothing $ \s -> getExpr s c (Just (Sig "transfer(uint256)" [AbiUIntType 256])) [] (debugVeriOpts { maxIter = Just 5 })
-       assertEqual "Expression is not clean." (badStoresInExpr expr) False
-    , testCase "simplify-storage-array-loop-struct" $ do
+       expr <- withSolvers Z3 1 Nothing $ \s -> getExpr s c (Just (Sig "transfer(uint256)" [AbiUIntType 256])) [] (defaultVeriOpts { maxIter = Just 5 })
+       assertEqualM "Expression is not clean." (badStoresInExpr expr) False
+    , test "simplify-storage-array-loop-struct" $ do
        Just c <- solcRuntime "MyContract"
         [i|
         contract MyContract {
@@ -167,9 +198,9 @@ tests = testGroup "hevm"
           }
         }
         |]
-       expr <- withSolvers Z3 1 Nothing $ \s -> getExpr s c (Just (Sig "transfer(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] (debugVeriOpts { maxIter = Just 5 })
-       assertEqual "Expression is not clean." (badStoresInExpr expr) False
-    , testCase "simplify-storage-map-only-static" $ do
+       expr <- withSolvers Z3 1 Nothing $ \s -> getExpr s c (Just (Sig "transfer(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] (defaultVeriOpts { maxIter = Just 5 })
+       assertEqualM "Expression is not clean." (badStoresInExpr expr) False
+    , test "simplify-storage-map-only-static" $ do
        Just c <- solcRuntime "MyContract"
         [i|
         contract MyContract {
@@ -183,9 +214,9 @@ tests = testGroup "hevm"
           }
         }
         |]
-       expr <- withSolvers Z3 1 Nothing $ \s -> getExpr s c (Just (Sig "transfer(uint256,uint256,uint256)" [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) [] debugVeriOpts
-       assertEqual "Expression is not clean." (badStoresInExpr expr) False
-    , testCase "simplify-storage-map-only-2" $ do
+       expr <- withSolvers Z3 1 Nothing $ \s -> getExpr s c (Just (Sig "transfer(uint256,uint256,uint256)" [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
+       assertEqualM "Expression is not clean." (badStoresInExpr expr) False
+    , test "simplify-storage-map-only-2" $ do
        Just c <- solcRuntime "MyContract"
         [i|
         contract MyContract {
@@ -199,10 +230,10 @@ tests = testGroup "hevm"
           }
         }
         |]
-       expr <- withSolvers Z3 1 Nothing $ \s -> getExpr s c (Just (Sig "transfer(uint256,uint256,uint256)" [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) [] debugVeriOpts
-       -- putStrLn $ T.unpack $ formatExpr expr
-       assertEqual "Expression is not clean." (badStoresInExpr expr) False
-    , testCase "simplify-storage-map-with-struct" $ do
+       expr <- withSolvers Z3 1 Nothing $ \s -> getExpr s c (Just (Sig "transfer(uint256,uint256,uint256)" [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
+       -- putStrLnM $ T.unpack $ formatExpr expr
+       assertEqualM "Expression is not clean." (badStoresInExpr expr) False
+    , test "simplify-storage-map-with-struct" $ do
        Just c <- solcRuntime "MyContract"
         [i|
         contract MyContract {
@@ -220,9 +251,9 @@ tests = testGroup "hevm"
           }
         }
         |]
-       expr <- withSolvers Z3 1 Nothing $ \s -> getExpr s c (Just (Sig "transfer(uint256,uint256,uint256)" [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) [] debugVeriOpts
-       assertEqual "Expression is not clean." (badStoresInExpr expr) False
-    , testCase "simplify-storage-map-and-array" $ do
+       expr <- withSolvers Z3 1 Nothing $ \s -> getExpr s c (Just (Sig "transfer(uint256,uint256,uint256)" [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
+       assertEqualM "Expression is not clean." (badStoresInExpr expr) False
+    , test "simplify-storage-map-and-array" $ do
        Just c <- solcRuntime "MyContract"
         [i|
         contract MyContract {
@@ -242,59 +273,59 @@ tests = testGroup "hevm"
           }
         }
        |]
-       expr <- withSolvers Z3 1 Nothing $ \s -> getExpr s c (Just (Sig "transfer(uint256,uint256,uint256)" [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) [] debugVeriOpts
-       -- putStrLn $ T.unpack $ formatExpr expr
-       assertEqual "Expression is not clean." (badStoresInExpr expr) False
+       expr <- withSolvers Z3 1 Nothing $ \s -> getExpr s c (Just (Sig "transfer(uint256,uint256,uint256)" [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
+       -- putStrLnM $ T.unpack $ formatExpr expr
+       assertEqualM "Expression is not clean." (badStoresInExpr expr) False
     ]
   , testGroup "StorageTests"
-    [ testCase "read-from-sstore" $ assertEqual ""
+    [ test "read-from-sstore" $ assertEqualM ""
         (Lit 0xab)
         (Expr.readStorage' (Lit 0x0) (SStore (Lit 0x0) (Lit 0xab) (AbstractStore (LitAddr 0x0))))
-    , testCase "read-from-concrete" $ assertEqual ""
+    , test "read-from-concrete" $ assertEqualM ""
         (Lit 0xab)
         (Expr.readStorage' (Lit 0x0) (ConcreteStore $ Map.fromList [(0x0, 0xab)]))
-    , testCase "read-past-write" $ assertEqual ""
+    , test "read-past-write" $ assertEqualM ""
         (Lit 0xab)
         (Expr.readStorage' (Lit 0x0) (SStore (Lit 0x1) (Var "b") (ConcreteStore $ Map.fromList [(0x0, 0xab)])))
-    , testCase "accessStorage uses fetchedStorage" $ do
+    , test "accessStorage uses fetchedStorage" $ do
         let dummyContract =
               (initialContract (RuntimeCode (ConcreteRuntimeCode mempty)))
                 { external = True }
-        vm <- stToIO $ vmForEthrunCreation ""
+        vm <- liftIO $ stToIO $ vmForEthrunCreation ""
             -- perform the initial access
-        vm1 <- stToIO $ execStateT (EVM.accessStorage (LitAddr 0) (Lit 0) (pure . pure ())) vm
+        vm1 <- liftIO $ stToIO $ execStateT (EVM.accessStorage (LitAddr 0) (Lit 0) (pure . pure ())) vm
         -- it should fetch the contract first
         vm2 <- case vm1.result of
                 Just (HandleEffect (Query (PleaseFetchContract _addr _ continue))) ->
-                  stToIO $ execStateT (continue dummyContract) vm1
+                  liftIO $ stToIO $ execStateT (continue dummyContract) vm1
                 _ -> internalError "unexpected result"
             -- then it should fetch the slow
         vm3 <- case vm2.result of
                     Just (HandleEffect (Query (PleaseFetchSlot _addr _slot continue))) ->
-                      stToIO $ execStateT (continue 1337) vm2
+                      liftIO $ stToIO $ execStateT (continue 1337) vm2
                     _ -> internalError "unexpected result"
             -- perform the same access as for vm1
-        vm4 <- stToIO $ execStateT (EVM.accessStorage (LitAddr 0) (Lit 0) (pure . pure ())) vm3
+        vm4 <- liftIO $ stToIO $ execStateT (EVM.accessStorage (LitAddr 0) (Lit 0) (pure . pure ())) vm3
 
         -- there won't be query now as accessStorage uses fetch cache
-        assertBool (show vm4.result) (isNothing vm4.result)
+        assertBoolM (show vm4.result) (isNothing vm4.result)
     ]
   , testGroup "SimplifierUnitTests"
     -- common overflow cases that the simplifier was getting wrong
-    [ testCase "bufLength-simp" $ do
+    [ test "writeWord-overflow" $ do
+        let e = ReadByte (Lit 0x0) (WriteWord (Lit 0xfffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffd) (Lit 0x0) (ConcreteBuf "\255\255\255\255"))
+        b <- checkEquiv e (Expr.simplify e)
+        assertBoolM "Simplifier failed" b
+    , test "bufLength-simp" $ do
       let
         a = BufLength (ConcreteBuf "ab")
         simp = Expr.simplify a
-      assertEqual "Must be simplified down to a Lit" simp (Lit 2)
-    , testCase "writeWord-overflow" $ do
-        let e = ReadByte (Lit 0x0) (WriteWord (Lit 0xfffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffd) (Lit 0x0) (ConcreteBuf "\255\255\255\255"))
-        b <- checkEquiv e (Expr.simplify e)
-        assertBool "Simplifier failed" b
-    , testCase "CopySlice-overflow" $ do
+      assertEqualM "Must be simplified down to a Lit" simp (Lit 2)
+    , test "CopySlice-overflow" $ do
         let e = ReadWord (Lit 0x0) (CopySlice (Lit 0x0) (Lit 0xfffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffc) (Lit 0x6) (ConcreteBuf "\255\255\255\255\255\255") (ConcreteBuf ""))
         b <- checkEquiv e (Expr.simplify e)
-        assertBool "Simplifier failed" b
-    , testCase "stripWrites-overflow" $ do
+        assertBoolM "Simplifier failed" b
+    , test "stripWrites-overflow" $ do
         -- below eventually boils down to
         -- unsafeInto (0xf0000000000000000000000000000000000000000000000000000000000000+1) :: Int
         -- which failed before
@@ -302,66 +333,66 @@ tests = testGroup "hevm"
           a = ReadByte (Lit 0xf0000000000000000000000000000000000000000000000000000000000000) (WriteByte (And (SHA256 (ConcreteBuf "")) (Lit 0x1)) (LitByte 0) (ConcreteBuf ""))
           b = Expr.simplify a
         ret <- checkEquiv a b
-        assertBool "must be equivalent" ret
+        assertBoolM "must be equivalent" ret
     ]
   -- These tests fuzz the simplifier by generating a random expression,
   -- applying some simplification rules, and then using the smt encoding to
   -- check that the simplified version is semantically equivalent to the
   -- unsimplified one
   , adjustOption (\(Test.Tasty.QuickCheck.QuickCheckTests n) -> Test.Tasty.QuickCheck.QuickCheckTests (min n 50)) $ testGroup "SimplifierTests"
-    [ testProperty  "buffer-simplification" $ \(expr :: Expr Buf) -> ioProperty $ do
+    [ testProperty  "buffer-simplification" $ \(expr :: Expr Buf) -> prop $ do
         let simplified = Expr.simplify expr
         checkEquiv expr simplified
-    , testProperty "store-simplification" $ \(expr :: Expr Storage) -> ioProperty $ do
+    , testProperty "store-simplification" $ \(expr :: Expr Storage) -> prop $ do
         let simplified = Expr.simplify expr
         checkEquiv expr simplified
-    , testProperty "byte-simplification" $ \(expr :: Expr Byte) -> ioProperty $ do
+    , testProperty "byte-simplification" $ \(expr :: Expr Byte) -> prop $ do
         let simplified = Expr.simplify expr
         checkEquiv expr simplified
-    , testProperty "word-simplification" $ \(ZeroDepthWord expr) -> ioProperty $ do
+    , testProperty "word-simplification" $ \(ZeroDepthWord expr) -> prop $ do
         let simplified = Expr.simplify expr
         checkEquiv expr simplified
-    , testProperty "readStorage-equivalance" $ \(store, slot) -> ioProperty $ do
+    , testProperty "readStorage-equivalance" $ \(store, slot) -> prop $ do
         let simplified = Expr.readStorage' slot store
             full = SLoad slot store
         checkEquiv simplified full
-    , testProperty "writeStorage-equivalance" $ \(val, GenWriteStorageExpr (slot, store)) -> ioProperty $ do
+    , testProperty "writeStorage-equivalance" $ \(val, GenWriteStorageExpr (slot, store)) -> prop $ do
         let simplified = Expr.writeStorage slot val store
             full = SStore slot val store
         checkEquiv simplified full
-    , testProperty "readWord-equivalance" $ \(buf, idx) -> ioProperty $ do
+    , testProperty "readWord-equivalance" $ \(buf, idx) -> prop $ do
         let simplified = Expr.readWord idx buf
             full = ReadWord idx buf
         checkEquiv simplified full
-    , testProperty "writeWord-equivalance" $ \(idx, val, WriteWordBuf buf) -> ioProperty $ do
+    , testProperty "writeWord-equivalance" $ \(idx, val, WriteWordBuf buf) -> prop $ do
         let simplified = Expr.writeWord idx val buf
             full = WriteWord idx val buf
         checkEquiv simplified full
-    , testProperty "arith-simplification" $ \(_ :: Int) -> ioProperty $ do
-        expr <- generate . sized $ genWordArith 15
+    , testProperty "arith-simplification" $ \(_ :: Int) -> prop $ do
+        expr <- liftIO $ generate . sized $ genWordArith 15
         let simplified = Expr.simplify expr
         checkEquiv expr simplified
-    , testProperty "readByte-equivalance" $ \(buf, idx) -> ioProperty $ do
+    , testProperty "readByte-equivalance" $ \(buf, idx) -> prop $ do
         let simplified = Expr.readByte idx buf
             full = ReadByte idx buf
         checkEquiv simplified full
     -- we currently only simplify concrete writes over concrete buffers so that's what we test here
-    , testProperty "writeByte-equivalance" $ \(LitOnly val, LitOnly buf, GenWriteByteIdx idx) -> ioProperty $ do
+    , testProperty "writeByte-equivalance" $ \(LitOnly val, LitOnly buf, GenWriteByteIdx idx) -> prop $ do
         let simplified = Expr.writeByte idx val buf
             full = WriteByte idx val buf
         checkEquiv simplified full
-    , testProperty "copySlice-equivalance" $ \(srcOff, GenCopySliceBuf src, GenCopySliceBuf dst, LitWord @300 size) -> ioProperty $ do
+    , testProperty "copySlice-equivalance" $ \(srcOff, GenCopySliceBuf src, GenCopySliceBuf dst, LitWord @300 size) -> prop $ do
         -- we bias buffers to be concrete more often than not
-        dstOff <- generate (maybeBoundedLit 100_000)
+        dstOff <- liftIO $ generate (maybeBoundedLit 100_000)
         let simplified = Expr.copySlice srcOff dstOff size src dst
             full = CopySlice srcOff dstOff size src dst
         checkEquiv simplified full
-    , testProperty "indexWord-equivalence" $ \(src, LitWord @50 idx) -> ioProperty $ do
+    , testProperty "indexWord-equivalence" $ \(src, LitWord @50 idx) -> prop $ do
         let simplified = Expr.indexWord idx src
             full = IndexWord idx src
         checkEquiv simplified full
-    , testProperty "indexWord-mask-equivalence" $ \(src :: Expr EWord, LitWord @35 idx) -> ioProperty $ do
-        mask <- generate $ do
+    , testProperty "indexWord-mask-equivalence" $ \(src :: Expr EWord, LitWord @35 idx) -> prop $ do
+        mask <- liftIO $ generate $ do
           pow <- arbitrary :: Gen Int
           frequency
            [ (1, pure $ Lit $ (shiftL 1 (pow `mod` 256)) - 1)        -- potentially non byte aligned
@@ -372,7 +403,7 @@ tests = testGroup "hevm"
           simplified = Expr.indexWord idx input
           full = IndexWord idx input
         checkEquiv simplified full
-    , testProperty "toList-equivalance" $ \buf -> ioProperty $ do
+    , testProperty "toList-equivalance" $ \buf -> prop $ do
         let
           -- transforms the input buffer to give it a known length
           fixLength :: Expr Buf -> Gen (Expr Buf)
@@ -393,161 +424,159 @@ tests = testGroup "hevm"
                 -- we use 100_000 as an upper bound for indices to keep tests reasonably fast here
                 pure $ Lit (w `mod` 100_000)
 
-        input <- generate $ fixLength buf
+        input <- liftIO $ generate $ fixLength buf
         case Expr.toList input of
           Nothing -> do
-            putStrLn "skip"
+            putStrLnM "skip"
             pure True -- ignore cases where the buf cannot be represented as a list
           Just asList -> do
             let asBuf = Expr.fromList asList
             checkEquiv asBuf input
-    , testProperty "simplifyProp-equivalence-lit" $ \(LitProp p) -> ioProperty $ do
+    , testProperty "simplifyProp-equivalence-lit" $ \(LitProp p) -> prop $ do
         let simplified = Expr.simplifyProps [p]
         case simplified of
           [] -> checkEquivProp (PBool True) p
           [val@(PBool _)] -> checkEquivProp val p
-          _ -> assertFailure "must evaluate down to a literal bool"
-    , testProperty "simplifyProp-equivalence-sym" $ \(p) -> ioProperty $ do
+          _ -> liftIO $ assertFailure "must evaluate down to a literal bool"
+    , testProperty "simplifyProp-equivalence-sym" $ \(p) -> prop $ do
         let simplified = Expr.simplifyProp p
         checkEquivProp simplified p
-    , testProperty "simpProp-equivalence-sym" $ \(ps :: [Prop]) -> ioProperty $ do
+    , testProperty "simpProp-equivalence-sym" $ \(ps :: [Prop]) -> prop $ do
         let simplified = pand (Expr.simplifyProps ps)
         checkEquivProp simplified (pand ps)
-    , testProperty "simpProp-equivalence-sym" $ \(LitProp p) -> ioProperty $ do
+    , testProperty "simpProp-equivalence-sym" $ \(LitProp p) -> prop $ do
         let simplified = pand (Expr.simplifyProps [p])
         checkEquivProp simplified p
     -- This would need to be a fuzz test I think. The SMT encoding of Keccak is not precise
     -- enough for this to succeed
-    , ignoreTest $ testProperty "storage-slot-simp-property" $ \(StorageExp s) -> ioProperty $ do
-        T.writeFile "unsimplified.expr" $ formatExpr s
+    , ignoreTest $ testProperty "storage-slot-simp-property" $ \(StorageExp s) -> prop $ do
         let simplified = Expr.simplify s
-        T.writeFile "simplified.expr" $ formatExpr simplified
         checkEquiv simplified s
     ]
   , testGroup "simpProp-concrete-tests" [
-      testCase "simpProp-concrete-trues" $ do
+      test "simpProp-concrete-trues" $ do
         let
           t = [PBool True, PBool True]
           simplified = Expr.simplifyProps t
-        assertEqual "Must be equal" [] simplified
-    , testCase "simpProp-concrete-false1" $ do
+        assertEqualM "Must be equal" [] simplified
+    , test "simpProp-concrete-false1" $ do
         let
           t = [PBool True, PBool False]
           simplified = Expr.simplifyProps t
-        assertEqual "Must be equal" [PBool False] simplified
-    , testCase "simpProp-concrete-false2" $ do
+        assertEqualM "Must be equal" [PBool False] simplified
+    , test "simpProp-concrete-false2" $ do
         let
           t = [PBool False, PBool False]
           simplified = Expr.simplifyProps t
-        assertEqual "Must be equal" [PBool False] simplified
-    , testCase "simpProp-concrete-or-1" $ do
+        assertEqualM "Must be equal" [PBool False] simplified
+    , test "simpProp-concrete-or-1" $ do
         let
           -- a = 5 && (a=4 || a=3)  -> False
           t = [PEq (Lit 5) (Var "a"), POr (PEq (Var "a") (Lit 4)) (PEq (Var "a") (Lit 3))]
           simplified = Expr.simplifyProps t
-        assertEqual "Must be equal" [PBool False] simplified
-    , ignoreTest $ testCase "simpProp-concrete-or-2" $ do
+        assertEqualM "Must be equal" [PBool False] simplified
+    , ignoreTest $ test "simpProp-concrete-or-2" $ do
         let
           -- Currently does not work, because we don't do simplification inside
           --   POr/PAnd using canBeSat
           -- a = 5 && (a=4 || a=5)  -> a=5
           t = [PEq (Lit 5) (Var "a"), POr (PEq (Var "a") (Lit 4)) (PEq (Var "a") (Lit 5))]
           simplified = Expr.simplifyProps t
-        assertEqual "Must be equal" [] simplified
-    , testCase "simpProp-concrete-and-1" $ do
+        assertEqualM "Must be equal" [] simplified
+    , test "simpProp-concrete-and-1" $ do
         let
           -- a = 5 && (a=4 && a=3)  -> False
           t = [PEq (Lit 5) (Var "a"), PAnd (PEq (Var "a") (Lit 4)) (PEq (Var "a") (Lit 3))]
           simplified = Expr.simplifyProps t
-        assertEqual "Must be equal" [PBool False] simplified
-    , testCase "simpProp-concrete-or-of-or" $ do
+        assertEqualM "Must be equal" [PBool False] simplified
+    , test "simpProp-concrete-or-of-or" $ do
         let
           -- a = 5 && ((a=4 || a=6) || a=3)  -> False
           t = [PEq (Lit 5) (Var "a"), POr (POr (PEq (Var "a") (Lit 4)) (PEq (Var "a") (Lit 6))) (PEq (Var "a") (Lit 3))]
           simplified = Expr.simplifyProps t
-        assertEqual "Must be equal" [PBool False] simplified
-    , testCase "simpProp-concrete-or-eq-rem" $ do
+        assertEqualM "Must be equal" [PBool False] simplified
+    , test "simpProp-concrete-or-eq-rem" $ do
         let
           -- a = 5 && ((a=4 || a=6) || a=3)  -> False
           t = [PEq (Lit 5) (Var "a"), POr (POr (PEq (Var "a") (Lit 4)) (PEq (Var "a") (Lit 6))) (PEq (Var "a") (Lit 3))]
           simplified = Expr.simplifyProps t
-        assertEqual "Must be equal" [PBool False] simplified
-    , testCase "simpProp-inner-expr-simp" $ do
+        assertEqualM "Must be equal" [PBool False] simplified
+    , test "simpProp-inner-expr-simp" $ do
         let
           -- 5+1 = 6
           t = [PEq (Add (Lit 5) (Lit 1)) (Var "a")]
           simplified = Expr.simplifyProps t
-        assertEqual "Must be equal" [PEq (Lit 6) (Var "a")] simplified
-    , testCase "simpProp-inner-expr-simp-with-canBeSat" $ do
+        assertEqualM "Must be equal" [PEq (Lit 6) (Var "a")] simplified
+    , test "simpProp-inner-expr-simp-with-canBeSat" $ do
         let
           -- 5+1 = 6, 6 != 7
           t = [PAnd (PEq (Add (Lit 5) (Lit 1)) (Var "a")) (PEq (Var "a") (Lit 7))]
           simplified = Expr.simplifyProps t
-        assertEqual "Must be equal" [PBool False] simplified
+        assertEqualM "Must be equal" [PBool False] simplified
   ]
   , testGroup "MemoryTests"
-    [ testCase "read-write-same-byte"  $ assertEqual ""
+    [ test "read-write-same-byte"  $ assertEqualM ""
         (LitByte 0x12)
         (Expr.readByte (Lit 0x20) (WriteByte (Lit 0x20) (LitByte 0x12) mempty))
-    , testCase "read-write-same-word"  $ assertEqual ""
+    , test "read-write-same-word"  $ assertEqualM ""
         (Lit 0x12)
         (Expr.readWord (Lit 0x20) (WriteWord (Lit 0x20) (Lit 0x12) mempty))
-    , testCase "read-byte-write-word"  $ assertEqual ""
+    , test "read-byte-write-word"  $ assertEqualM ""
         -- reading at byte 31 a word that's been written should return LSB
         (LitByte 0x12)
         (Expr.readByte (Lit 0x1f) (WriteWord (Lit 0x0) (Lit 0x12) mempty))
-    , testCase "read-byte-write-word2"  $ assertEqual ""
+    , test "read-byte-write-word2"  $ assertEqualM ""
         -- Same as above, but offset not 0
         (LitByte 0x12)
         (Expr.readByte (Lit 0x20) (WriteWord (Lit 0x1) (Lit 0x12) mempty))
-    ,testCase "read-write-with-offset"  $ assertEqual ""
+    ,test "read-write-with-offset"  $ assertEqualM ""
         -- 0x3F = 63 decimal, 0x20 = 32. 0x12 = 18
         --    We write 128bits (32 Bytes), representing 18 at offset 32.
         --    Hence, when reading out the 63rd byte, we should read out the LSB 8 bits
         --           which is 0x12
         (LitByte 0x12)
         (Expr.readByte (Lit 0x3F) (WriteWord (Lit 0x20) (Lit 0x12) mempty))
-    ,testCase "read-write-with-offset2"  $ assertEqual ""
+    ,test "read-write-with-offset2"  $ assertEqualM ""
         --  0x20 = 32, 0x3D = 61
         --  we write 128 bits (32 Bytes) representing 0x10012, at offset 32.
         --  we then read out a byte at offset 61.
         --  So, at 63 we'd read 0x12, at 62 we'd read 0x00, at 61 we should read 0x1
         (LitByte 0x1)
         (Expr.readByte (Lit 0x3D) (WriteWord (Lit 0x20) (Lit 0x10012) mempty))
-    , testCase "read-write-with-extension-to-zero" $ assertEqual ""
+    , test "read-write-with-extension-to-zero" $ assertEqualM ""
         -- write word and read it at the same place (i.e. 0 offset)
         (Lit 0x12)
         (Expr.readWord (Lit 0x0) (WriteWord (Lit 0x0) (Lit 0x12) mempty))
-    , testCase "read-write-with-extension-to-zero-with-offset" $ assertEqual ""
+    , test "read-write-with-extension-to-zero-with-offset" $ assertEqualM ""
         -- write word and read it at the same offset of 4
         (Lit 0x12)
         (Expr.readWord (Lit 0x4) (WriteWord (Lit 0x4) (Lit 0x12) mempty))
-    , testCase "read-write-with-extension-to-zero-with-offset2" $ assertEqual ""
+    , test "read-write-with-extension-to-zero-with-offset2" $ assertEqualM ""
         -- write word and read it at the same offset of 16
         (Lit 0x12)
         (Expr.readWord (Lit 0x20) (WriteWord (Lit 0x20) (Lit 0x12) mempty))
-    , testCase "read-word-copySlice-overlap" $ assertEqual ""
+    , test "read-word-copySlice-overlap" $ assertEqualM ""
         -- we should not recurse into a copySlice if the read index + 32 overlaps the sliced region
         (ReadWord (Lit 40) (CopySlice (Lit 0) (Lit 30) (Lit 12) (WriteWord (Lit 10) (Lit 0x64) (AbstractBuf "hi")) (AbstractBuf "hi")))
         (Expr.readWord (Lit 40) (CopySlice (Lit 0) (Lit 30) (Lit 12) (WriteWord (Lit 10) (Lit 0x64) (AbstractBuf "hi")) (AbstractBuf "hi")))
-    , testCase "indexword-MSB" $ assertEqual ""
+    , test "indexword-MSB" $ assertEqualM ""
         -- 31st is the LSB byte (of 32)
         (LitByte 0x78)
         (Expr.indexWord (Lit 31) (Lit 0x12345678))
-    , testCase "indexword-LSB" $ assertEqual ""
+    , test "indexword-LSB" $ assertEqualM ""
         -- 0th is the MSB byte (of 32), Lit 0xff22bb... is exactly 32 Bytes.
         (LitByte 0xff)
         (Expr.indexWord (Lit 0) (Lit 0xff22bb4455667788990011223344556677889900112233445566778899001122))
-    , testCase "indexword-LSB2" $ assertEqual ""
+    , test "indexword-LSB2" $ assertEqualM ""
         -- same as above, but with offset 2
         (LitByte 0xbb)
         (Expr.indexWord (Lit 2) (Lit 0xff22bb4455667788990011223344556677889900112233445566778899001122))
-    , testCase "encodeConcreteStore-overwrite" $
-      assertEqual ""
+    , test "encodeConcreteStore-overwrite" $
+      assertEqualM ""
         "(store (store ((as const Storage) #x0000000000000000000000000000000000000000000000000000000000000000) (_ bv1 256) (_ bv2 256)) (_ bv3 256) (_ bv4 256))"
         (EVM.SMT.encodeConcreteStore $
           Map.fromList [(W256 1, W256 2), (W256 3, W256 4)])
-    , testCase "indexword-oob-sym" $ assertEqual ""
+    , test "indexword-oob-sym" $ assertEqualM ""
         -- indexWord should return 0 for oob access
         (LitByte 0x0)
         (Expr.indexWord (Lit 100) (JoinBytes
@@ -555,7 +584,7 @@ tests = testGroup "hevm"
           (LitByte 0) (LitByte 0) (LitByte 0) (LitByte 0) (LitByte 0) (LitByte 0) (LitByte 0) (LitByte 0)
           (LitByte 0) (LitByte 0) (LitByte 0) (LitByte 0) (LitByte 0) (LitByte 0) (LitByte 0) (LitByte 0)
           (LitByte 0) (LitByte 0) (LitByte 0) (LitByte 0) (LitByte 0) (LitByte 0) (LitByte 0) (LitByte 0)))
-    , testCase "stripbytes-concrete-bug" $ assertEqual ""
+    , test "stripbytes-concrete-bug" $ assertEqualM ""
         (Expr.simplifyReads (ReadByte (Lit 0) (ConcreteBuf "5")))
         (LitByte 53)
     ]
@@ -566,43 +595,42 @@ tests = testGroup "hevm"
           _ -> False
     ]
   , testGroup "Solidity-Expressions"
-    [ testCase "Trivial" $
+    [ test "Trivial" $
         SolidityCall "x = 3;" []
           ===> AbiUInt 256 3
-
-    , testCase "Arithmetic" $ do
+    , test "Arithmetic" $ do
         SolidityCall "x = a + 1;"
           [AbiUInt 256 1] ===> AbiUInt 256 2
         SolidityCall "unchecked { x = a - 1; }"
           [AbiUInt 8 0] ===> AbiUInt 8 255
 
-    , testCase "keccak256()" $
+    , test "keccak256()" $
         SolidityCall "x = uint(keccak256(abi.encodePacked(a)));"
           [AbiString ""] ===> AbiUInt 256 0xc5d2460186f7233c927e7db2dcc703c0e500b653ca82273b7bfad8045d85a470
 
     , testProperty "abi encoding vs. solidity" $ withMaxSuccess 20 $ forAll (arbitrary >>= genAbiValue) $
-      \y -> ioProperty $ do
+      \y -> prop $ do
           Just encoded <- runStatements [i| x = abi.encode(a);|]
             [y] AbiBytesDynamicType
           let solidityEncoded = case decodeAbiValue (AbiTupleType $ V.fromList [AbiBytesDynamicType]) (BS.fromStrict encoded) of
                 AbiTuple (V.toList -> [e]) -> e
                 _ -> internalError "AbiTuple expected"
           let hevmEncoded = encodeAbiValue (AbiTuple $ V.fromList [y])
-          assertEqual "abi encoding mismatch" solidityEncoded (AbiBytesDynamic hevmEncoded)
+          assertEqualM "abi encoding mismatch" solidityEncoded (AbiBytesDynamic hevmEncoded)
 
     , testProperty "abi encoding vs. solidity (2 args)" $ withMaxSuccess 20 $ forAll (arbitrary >>= bothM genAbiValue) $
-      \(x', y') -> ioProperty $ do
+      \(x', y') -> prop $ do
           Just encoded <- runStatements [i| x = abi.encode(a, b);|]
             [x', y'] AbiBytesDynamicType
           let solidityEncoded = case decodeAbiValue (AbiTupleType $ V.fromList [AbiBytesDynamicType]) (BS.fromStrict encoded) of
                 AbiTuple (V.toList -> [e]) -> e
                 _ -> internalError "AbiTuple expected"
           let hevmEncoded = encodeAbiValue (AbiTuple $ V.fromList [x',y'])
-          assertEqual "abi encoding mismatch" solidityEncoded (AbiBytesDynamic hevmEncoded)
+          assertEqualM "abi encoding mismatch" solidityEncoded (AbiBytesDynamic hevmEncoded)
 
     -- we need a separate test for this because the type of a function is "function() external" in solidity but just "function" in the abi:
     , testProperty "abi encoding vs. solidity (function pointer)" $ withMaxSuccess 20 $ forAll (genAbiValue AbiFunctionType) $
-      \y -> ioProperty $ do
+      \y -> prop $ do
           Just encoded <- runFunction [i|
               function foo(function() external a) public pure returns (bytes memory x) {
                 x = abi.encode(a);
@@ -612,37 +640,37 @@ tests = testGroup "hevm"
                 AbiTuple (V.toList -> [e]) -> e
                 _ -> internalError "AbiTuple expected"
           let hevmEncoded = encodeAbiValue (AbiTuple $ V.fromList [y])
-          assertEqual "abi encoding mismatch" solidityEncoded (AbiBytesDynamic hevmEncoded)
+          assertEqualM "abi encoding mismatch" solidityEncoded (AbiBytesDynamic hevmEncoded)
     ]
 
   , testGroup "Precompiled contracts"
       [ testGroup "Example (reverse)"
-          [ testCase "success" $
-              assertEqual "example contract reverses"
+          [ test "success" $
+              assertEqualM "example contract reverses"
                 (execute 0xdeadbeef "foobar" 6) (Just "raboof")
-          , testCase "failure" $
-              assertEqual "example contract fails on length mismatch"
+          , test "failure" $
+              assertEqualM "example contract fails on length mismatch"
                 (execute 0xdeadbeef "foobar" 5) Nothing
           ]
 
       , testGroup "ECRECOVER"
-          [ testCase "success" $ do
+          [ test "success" $ do
               let
                 r = hex "c84e55cee2032ea541a32bf6749e10c8b9344c92061724c4e751600f886f4732"
                 s = hex "1542b6457e91098682138856165381453b3d0acae2470286fd8c8a09914b1b5d"
                 v = hex "000000000000000000000000000000000000000000000000000000000000001c"
                 h = hex "513954cf30af6638cb8f626bd3f8c39183c26784ce826084d9d267868a18fb31"
                 a = hex "0000000000000000000000002d5e56d45c63150d937f2182538a0f18510cb11f"
-              assertEqual "successful recovery"
+              assertEqualM "successful recovery"
                 (Just a)
                 (execute 1 (h <> v <> r <> s) 32)
-          , testCase "fail on made up values" $ do
+          , test "fail on made up values" $ do
               let
                 r = hex "c84e55cee2032ea541a32bf6749e10c8b9344c92061724c4e751600f886f4731"
                 s = hex "1542b6457e91098682138856165381453b3d0acae2470286fd8c8a09914b1b5d"
                 v = hex "000000000000000000000000000000000000000000000000000000000000001c"
                 h = hex "513954cf30af6638cb8f626bd3f8c39183c26784ce826084d9d267868a18fb31"
-              assertEqual "fail because bit flip"
+              assertEqualM "fail because bit flip"
                 Nothing
                 (execute 1 (h <> v <> r <> s) 32)
           ]
@@ -663,19 +691,19 @@ tests = testGroup "hevm"
     ]
 
   , testGroup "Unresolved link detection"
-    [ testCase "holes detected" $ do
+    [ test "holes detected" $ do
         let code' = "608060405234801561001057600080fd5b5060405161040f38038061040f83398181016040528101906100329190610172565b73__$f3cbc3eb14e5bd0705af404abcf6f741ec$__63ab5c1ffe826040518263ffffffff1660e01b81526004016100699190610217565b60206040518083038186803b15801561008157600080fd5b505af4158015610095573d6000803e3d6000fd5b505050506040513d601f19601f820116820180604052508101906100b99190610145565b50506103c2565b60006100d36100ce84610271565b61024c565b9050828152602081018484840111156100ef576100ee610362565b5b6100fa8482856102ca565b509392505050565b600081519050610111816103ab565b92915050565b600082601f83011261012c5761012b61035d565b5b815161013c8482602086016100c0565b91505092915050565b60006020828403121561015b5761015a61036c565b5b600061016984828501610102565b91505092915050565b6000602082840312156101885761018761036c565b5b600082015167ffffffffffffffff8111156101a6576101a5610367565b5b6101b284828501610117565b91505092915050565b60006101c6826102a2565b6101d081856102ad565b93506101e08185602086016102ca565b6101e981610371565b840191505092915050565b60006102016003836102ad565b915061020c82610382565b602082019050919050565b6000604082019050818103600083015261023181846101bb565b90508181036020830152610244816101f4565b905092915050565b6000610256610267565b905061026282826102fd565b919050565b6000604051905090565b600067ffffffffffffffff82111561028c5761028b61032e565b5b61029582610371565b9050602081019050919050565b600081519050919050565b600082825260208201905092915050565b60008115159050919050565b60005b838110156102e85780820151818401526020810190506102cd565b838111156102f7576000848401525b50505050565b61030682610371565b810181811067ffffffffffffffff821117156103255761032461032e565b5b80604052505050565b7f4e487b7100000000000000000000000000000000000000000000000000000000600052604160045260246000fd5b600080fd5b600080fd5b600080fd5b600080fd5b6000601f19601f8301169050919050565b7f6261720000000000000000000000000000000000000000000000000000000000600082015250565b6103b4816102be565b81146103bf57600080fd5b50565b603f806103d06000396000f3fe6080604052600080fdfea26469706673582212207d03b26e43dc3d116b0021ddc9817bde3762a3b14315351f11fc4be384fd14a664736f6c63430008060033"
-        assertBool "linker hole not detected" (containsLinkerHole code'),
-      testCase "no false positives" $ do
+        assertBoolM "linker hole not detected" (containsLinkerHole code'),
+      test "no false positives" $ do
         let code' = "0x608060405234801561001057600080fd5b50600436106100365760003560e01c806317bf8bac1461003b578063acffee6b1461005d575b600080fd5b610043610067565b604051808215151515815260200191505060405180910390f35b610065610073565b005b60008060015414905090565b6000809054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1663f8a8fd6d6040518163ffffffff1660e01b815260040160206040518083038186803b1580156100da57600080fd5b505afa1580156100ee573d6000803e3d6000fd5b505050506040513d602081101561010457600080fd5b810190808051906020019092919050505060018190555056fea265627a7a723158205d775f914dcb471365a430b5f5b2cfe819e615cbbb5b2f1ccc7da1fd802e43c364736f6c634300050b0032"
-        assertBool "false positive" (not . containsLinkerHole $ code')
+        assertBoolM "false positive" (not . containsLinkerHole $ code')
     ]
 
   , testGroup "metadata stripper"
-    [ testCase "it strips the metadata for solc => 0.6" $ do
+    [ test "it strips the metadata for solc => 0.6" $ do
         let code' = hexText "0x608060405234801561001057600080fd5b50600436106100365760003560e01c806317bf8bac1461003b578063acffee6b1461005d575b600080fd5b610043610067565b604051808215151515815260200191505060405180910390f35b610065610073565b005b60008060015414905090565b6000809054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1663f8a8fd6d6040518163ffffffff1660e01b815260040160206040518083038186803b1580156100da57600080fd5b505afa1580156100ee573d6000803e3d6000fd5b505050506040513d602081101561010457600080fd5b810190808051906020019092919050505060018190555056fea265627a7a723158205d775f914dcb471365a430b5f5b2cfe819e615cbbb5b2f1ccc7da1fd802e43c364736f6c634300050b0032"
             stripped = stripBytecodeMetadata code'
-        assertEqual "failed to strip metadata" (show (ByteStringS stripped)) "0x608060405234801561001057600080fd5b50600436106100365760003560e01c806317bf8bac1461003b578063acffee6b1461005d575b600080fd5b610043610067565b604051808215151515815260200191505060405180910390f35b610065610073565b005b60008060015414905090565b6000809054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1663f8a8fd6d6040518163ffffffff1660e01b815260040160206040518083038186803b1580156100da57600080fd5b505afa1580156100ee573d6000803e3d6000fd5b505050506040513d602081101561010457600080fd5b810190808051906020019092919050505060018190555056fe"
+        assertEqualM "failed to strip metadata" (show (ByteStringS stripped)) "0x608060405234801561001057600080fd5b50600436106100365760003560e01c806317bf8bac1461003b578063acffee6b1461005d575b600080fd5b610043610067565b604051808215151515815260200191505060405180910390f35b610065610073565b005b60008060015414905090565b6000809054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1663f8a8fd6d6040518163ffffffff1660e01b815260040160206040518083038186803b1580156100da57600080fd5b505afa1580156100ee573d6000803e3d6000fd5b505050506040513d602081101561010457600080fd5b810190808051906020019092919050505060018190555056fe"
     ,
       testCase "it strips the metadata and constructor args" $ do
         let srccode =
@@ -704,7 +732,7 @@ tests = testGroup "hevm"
     ]
  , testGroup "Panic code tests via symbolic execution"
   [
-     testCase "assert-fail" $ do
+     test "assert-fail" $ do
        Just c <- solcRuntime "MyContract"
            [i|
            contract MyContract {
@@ -714,10 +742,10 @@ tests = testGroup "hevm"
             }
            |]
        (_, [Cex (_, ctr)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x01] c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
-       assertEqual "Must be 0" 0 $ getVar ctr "arg1"
-       putStrLn  $ "expected counterexample found, and it's correct: " <> (show $ getVar ctr "arg1")
+       assertEqualM "Must be 0" 0 $ getVar ctr "arg1"
+       putStrLnM  $ "expected counterexample found, and it's correct: " <> (show $ getVar ctr "arg1")
      ,
-     testCase "safeAdd-fail" $ do
+     test "safeAdd-fail" $ do
         Just c <- solcRuntime "MyContract"
             [i|
             contract MyContract {
@@ -731,10 +759,10 @@ tests = testGroup "hevm"
         let y = getVar ctr "arg2"
 
         let maxUint = 2 ^ (256 :: Integer) :: Integer
-        assertBool "Overflow must occur" (toInteger x + toInteger y >= maxUint)
-        putStrLn "expected counterexample found"
+        assertBoolM "Overflow must occur" (toInteger x + toInteger y >= maxUint)
+        putStrLnM "expected counterexample found"
      ,
-     testCase "div-by-zero-fail" $ do
+     test "div-by-zero-fail" $ do
         Just c <- solcRuntime "MyContract"
             [i|
             contract MyContract {
@@ -744,10 +772,10 @@ tests = testGroup "hevm"
              }
             |]
         (_, [Cex (_, ctr)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x12] c (Just (Sig "fun(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
-        assertEqual "Division by 0 needs b=0" (getVar ctr "arg2") 0
-        putStrLn "expected counterexample found"
+        assertEqualM "Division by 0 needs b=0" (getVar ctr "arg2") 0
+        putStrLnM "expected counterexample found"
      ,
-      testCase "unused-args-fail" $ do
+      test "unused-args-fail" $ do
          Just c <- solcRuntime "C"
              [i|
              contract C {
@@ -757,9 +785,9 @@ tests = testGroup "hevm"
              }
              |]
          (_, [Cex _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x1] c Nothing [] defaultVeriOpts
-         putStrLn "expected counterexample found"
+         putStrLnM "expected counterexample found"
       ,
-     testCase "enum-conversion-fail" $ do
+     test "enum-conversion-fail" $ do
         Just c <- solcRuntime "MyContract"
             [i|
             contract MyContract {
@@ -770,13 +798,13 @@ tests = testGroup "hevm"
              }
             |]
         (_, [Cex (_, ctr)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x21] c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
-        assertBool "Enum is only defined for 0 and 1" $ (getVar ctr "arg1") > 1
-        putStrLn "expected counterexample found"
+        assertBoolM "Enum is only defined for 0 and 1" $ (getVar ctr "arg1") > 1
+        putStrLnM "expected counterexample found"
      ,
      -- TODO 0x22 is missing: "0x22: If you access a storage byte array that is incorrectly encoded."
      -- TODO below should NOT fail
      -- TODO this has a loop that depends on a symbolic value and currently causes interpret to loop
-     ignoreTest $ testCase "pop-empty-array" $ do
+     ignoreTest $ test "pop-empty-array" $ do
         Just c <- solcRuntime "MyContract"
             [i|
             contract MyContract {
@@ -791,11 +819,12 @@ tests = testGroup "hevm"
              }
             |]
         a <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x31] c (Just (Sig "fun(uint8)" [AbiUIntType 8])) [] defaultVeriOpts
-        print $ length a
-        print $ show a
-        putStrLn "expected counterexample found"
+        liftIO $ do
+          print $ length a
+          print $ show a
+          putStrLnM "expected counterexample found"
      ,
-     testCase "access-out-of-bounds-array" $ do
+     test "access-out-of-bounds-array" $ do
         Just c <- solcRuntime "MyContract"
             [i|
             contract MyContract {
@@ -808,11 +837,11 @@ tests = testGroup "hevm"
              }
             |]
         (_, [Cex (_, _)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x32] c (Just (Sig "fun(uint8)" [AbiUIntType 8])) [] defaultVeriOpts
-        -- assertBool "Access must be beyond element 2" $ (getVar ctr "arg1") > 1
-        putStrLn "expected counterexample found"
+        -- assertBoolM "Access must be beyond element 2" $ (getVar ctr "arg1") > 1
+        putStrLnM "expected counterexample found"
       ,
       -- Note: we catch the assertion here, even though we are only able to explore partially
-      testCase "alloc-too-much" $ do
+      test "alloc-too-much" $ do
         Just c <- solcRuntime "MyContract"
             [i|
             contract MyContract {
@@ -823,9 +852,9 @@ tests = testGroup "hevm"
             |]
         (_, [Cex _]) <- withSolvers Z3 1 Nothing $ \s ->
           checkAssert s [0x41] c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
-        putStrLn "expected counterexample found"
+        putStrLnM "expected counterexample found"
       ,
-      testCase "vm.deal unknown address" $ do
+      test "vm.deal unknown address" $ do
         Just c <- solcRuntime "C"
           [i|
             interface Vm {
@@ -841,9 +870,9 @@ tests = testGroup "hevm"
             }
           |]
         Right e <- reachableUserAsserts c (Just $ Sig "f(address,uint256)" [AbiAddressType, AbiUIntType 256])
-        assertBool "The expression is not partial" $ Expr.containsNode isPartial e
+        assertBoolM "The expression is not partial" $ Expr.containsNode isPartial e
       ,
-      testCase "vm.prank underflow" $ do
+      test "vm.prank underflow" $ do
         Just c <- solcRuntime "C"
             [i|
               interface Vm {
@@ -867,9 +896,9 @@ tests = testGroup "hevm"
               }
             |]
         r <- allBranchesFail c Nothing
-        assertBool "all branches must fail" (isRight r)
+        assertBoolM "all branches must fail" (isRight r)
       ,
-      testCase "call ffi when disabled" $ do
+      test "call ffi when disabled" $ do
         Just c <- solcRuntime "C"
             [i|
               interface Vm {
@@ -889,11 +918,11 @@ tests = testGroup "hevm"
               }
             |]
         Right e <- reachableUserAsserts c Nothing
-        T.putStrLn $ formatExpr e
-        assertBool "The expression is not partial" $ Expr.containsNode isPartial e
+        liftIO $ T.putStrLn $ formatExpr e
+        assertBoolM "The expression is not partial" $ Expr.containsNode isPartial e
       ,
       -- TODO: we can't deal with symbolic jump conditions
-      expectFail $ testCase "call-zero-inited-var-thats-a-function" $ do
+      expectFail $ test "call-zero-inited-var-thats-a-function" $ do
         Just c <- solcRuntime "MyContract"
             [i|
             contract MyContract {
@@ -912,12 +941,12 @@ tests = testGroup "hevm"
         (_, [Cex (_, cex)]) <- withSolvers Z3 1 Nothing $
           \s -> checkAssert s [0x51] c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
         let a = fromJust $ Map.lookup (Var "arg1") cex.vars
-        assertEqual "unexpected cex value" a 44
-        putStrLn "expected counterexample found"
+        assertEqualM "unexpected cex value" a 44
+        putStrLnM "expected counterexample found"
   ]
   , testGroup "Symbolic-Constructor-Args"
     -- this produced some hard to debug failures. keeping it around since it seemed to exercise the contract creation code in interesting ways...
-    [ testCase "multiple-symbolic-constructor-calls" $ do
+    [ test "multiple-symbolic-constructor-calls" $ do
         Just initCode <- solidity "C"
           [i|
             contract A {
@@ -939,10 +968,10 @@ tests = testGroup "hevm"
           |]
         withSolvers Z3 1 Nothing $ \s -> do
           let calldata = (WriteWord (Lit 0x0) (Var "u") (ConcreteBuf ""), [])
-          initVM <- stToIO $ abstractVM calldata initCode Nothing True
+          initVM <- liftIO $ stToIO $ abstractVM calldata initCode Nothing True
           expr <- Expr.simplify <$> interpret (Fetch.oracle s Nothing) Nothing 1 StackBased initVM runExpr
-          assertBool "unexptected partial execution" (not $ Expr.containsNode isPartial expr)
-    , testCase "mixed-concrete-symbolic-args" $ do
+          assertBoolM "unexptected partial execution" (not $ Expr.containsNode isPartial expr)
+    , test "mixed-concrete-symbolic-args" $ do
         Just c <- solcRuntime "C"
           [i|
             contract B {
@@ -964,8 +993,8 @@ tests = testGroup "hevm"
             }
           |]
         Right expr <- reachableUserAsserts c (Just $ Sig "foo(uint256)" [AbiUIntType 256])
-        assertBool "unexptected partial execution" (not $ Expr.containsNode isPartial expr)
-    , testCase "jump-into-symbolic-region" $ do
+        assertBoolM "unexptected partial execution" (not $ Expr.containsNode isPartial expr)
+    , test "jump-into-symbolic-region" $ do
         let
           -- our initCode just jumps directly to the end
           code = BS.pack . mapMaybe maybeLitByte $ V.toList $ assemble
@@ -993,17 +1022,17 @@ tests = testGroup "hevm"
               , OpCreate
               ])
         withSolvers Z3 1 Nothing $ \s -> do
-          vm <- stToIO $ loadSymVM runtimecode (Lit 0) initCode False
+          vm <- liftIO $ stToIO $ loadSymVM runtimecode (Lit 0) initCode False
           expr <- Expr.simplify <$> interpret (Fetch.oracle s Nothing) Nothing 1 StackBased vm runExpr
           case expr of
-            Partial _ _ (JumpIntoSymbolicCode _ _) -> assertBool "" True
-            _ -> assertBool "did not encounter expected partial node" False
+            Partial _ _ (JumpIntoSymbolicCode _ _) -> assertBoolM "" True
+            _ -> assertBoolM "did not encounter expected partial node" False
     ]
   , testGroup "Dapp-Tests"
-    [ testCase "Trivial-Pass" $ do
+    [ test "Trivial-Pass" $ do
         let testFile = "test/contracts/pass/trivial.sol"
-        runSolidityTest testFile ".*" >>= assertEqual "test result" True
-    , testCase "DappTools" $ do
+        runSolidityTest testFile ".*" >>= assertEqualM "test result" True
+    , test "DappTools" $ do
         -- quick smokecheck to make sure that we can parse dapptools style build outputs
         let cases =
               [ ("test/contracts/pass/trivial.sol", ".*", True)
@@ -1014,44 +1043,44 @@ tests = testGroup "hevm"
         results <- forM cases $ \(testFile, match, expected) -> do
           actual <- runSolidityTestCustom testFile match Nothing Nothing False Nothing DappTools
           pure (actual == expected)
-        assertBool "test result" (and results)
-    , testCase "Trivial-Fail" $ do
+        assertBoolM "test result" (and results)
+    , test "Trivial-Fail" $ do
         let testFile = "test/contracts/fail/trivial.sol"
-        runSolidityTest testFile "prove_false" >>= assertEqual "test result" False
-    , testCase "Abstract" $ do
+        runSolidityTest testFile "prove_false" >>= assertEqualM "test result" False
+    , test "Abstract" $ do
         let testFile = "test/contracts/pass/abstract.sol"
-        runSolidityTest testFile ".*" >>= assertEqual "test result" True
-    , testCase "Constantinople" $ do
+        runSolidityTest testFile ".*" >>= assertEqualM "test result" True
+    , test "Constantinople" $ do
         let testFile = "test/contracts/pass/constantinople.sol"
-        runSolidityTest testFile ".*" >>= assertEqual "test result" True
-    , testCase "Prove-Tests-Pass" $ do
+        runSolidityTest testFile ".*" >>= assertEqualM "test result" True
+    , test "Prove-Tests-Pass" $ do
         let testFile = "test/contracts/pass/dsProvePass.sol"
-        runSolidityTest testFile ".*" >>= assertEqual "test result" True
-    , testCase "prefix-check-for-dapp" $ do
+        runSolidityTest testFile ".*" >>= assertEqualM "test result" True
+    , test "prefix-check-for-dapp" $ do
         let testFile = "test/contracts/fail/check-prefix.sol"
-        runSolidityTest testFile "check_trivial" >>= assertEqual "test result" False
-    , testCase "Prove-Tests-Fail" $ do
+        runSolidityTest testFile "check_trivial" >>= assertEqualM "test result" False
+    , test "Prove-Tests-Fail" $ do
         let testFile = "test/contracts/fail/dsProveFail.sol"
-        runSolidityTest testFile "prove_trivial" >>= assertEqual "test result" False
-        runSolidityTest testFile "prove_trivial_dstest" >>= assertEqual "test result" False
-        runSolidityTest testFile "prove_add" >>= assertEqual "test result" False
-        runSolidityTestCustom testFile "prove_smtTimeout" (Just 1) Nothing False Nothing Foundry >>= assertEqual "test result" False
-        runSolidityTest testFile "prove_multi" >>= assertEqual "test result" False
+        runSolidityTest testFile "prove_trivial" >>= assertEqualM "test result" False
+        runSolidityTest testFile "prove_trivial_dstest" >>= assertEqualM "test result" False
+        runSolidityTest testFile "prove_add" >>= assertEqualM "test result" False
+        runSolidityTestCustom testFile "prove_smtTimeout" (Just 1) Nothing False Nothing Foundry >>= assertEqualM "test result" False
+        runSolidityTest testFile "prove_multi" >>= assertEqualM "test result" False
         -- TODO: implement overflow checking optimizations and enable, currently this runs forever
-        --runSolidityTest testFile "prove_distributivity" >>= assertEqual "test result" False
-    , testCase "Loop-Tests" $ do
+        --runSolidityTest testFile "prove_distributivity" >>= assertEqualM "test result" False
+    , test "Loop-Tests" $ do
         let testFile = "test/contracts/pass/loops.sol"
-        runSolidityTestCustom testFile "prove_loop" Nothing (Just 10) False Nothing Foundry >>= assertEqual "test result" True
-        runSolidityTestCustom testFile "prove_loop" Nothing (Just 100) False Nothing Foundry >>= assertEqual "test result" False
-    , testCase "Cheat-Codes-Pass" $ do
+        runSolidityTestCustom testFile "prove_loop" Nothing (Just 10) False Nothing Foundry >>= assertEqualM "test result" True
+        runSolidityTestCustom testFile "prove_loop" Nothing (Just 100) False Nothing Foundry >>= assertEqualM "test result" False
+    , test "Cheat-Codes-Pass" $ do
         let testFile = "test/contracts/pass/cheatCodes.sol"
-        runSolidityTest testFile ".*" >>= assertEqual "test result" True
-    , testCase "Unwind" $ do
+        runSolidityTest testFile ".*" >>= assertEqualM "test result" True
+    , test "Unwind" $ do
         let testFile = "test/contracts/pass/unwind.sol"
-        runSolidityTest testFile ".*" >>= assertEqual "test result" True
+        runSolidityTest testFile ".*" >>= assertEqualM "test result" True
     ]
   , testGroup "max-iterations"
-    [ testCase "concrete-loops-reached" $ do
+    [ test "concrete-loops-reached" $ do
         Just c <- solcRuntime "C"
             [i|
             contract C {
@@ -1066,8 +1095,8 @@ tests = testGroup "hevm"
             opts = defaultVeriOpts{ maxIter = Just 3 }
         (e, [Qed _]) <- withSolvers Z3 1 Nothing $
           \s -> checkAssert s defaultPanicCodes c sig [] opts
-        assertBool "The expression is not partial" $ isPartial e
-    , testCase "concrete-loops-not-reached" $ do
+        assertBoolM "The expression is not partial" $ isPartial e
+    , test "concrete-loops-not-reached" $ do
         Just c <- solcRuntime "C"
             [i|
             contract C {
@@ -1083,8 +1112,8 @@ tests = testGroup "hevm"
             opts = defaultVeriOpts{ maxIter = Just 6 }
         (e, [Qed _]) <- withSolvers Z3 1 Nothing $
           \s -> checkAssert s defaultPanicCodes c sig [] opts
-        assertBool "The expression is partial" $ not $ isPartial e
-    , testCase "symbolic-loops-reached" $ do
+        assertBoolM "The expression is partial" $ not $ isPartial e
+    , test "symbolic-loops-reached" $ do
         Just c <- solcRuntime "C"
             [i|
             contract C {
@@ -1097,8 +1126,8 @@ tests = testGroup "hevm"
             |]
         (e, [Qed _]) <- withSolvers Z3 1 Nothing $
           \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] (defaultVeriOpts{ maxIter = Just 5 })
-        assertBool "The expression is not partial" $ Expr.containsNode isPartial e
-    , testCase "inconsistent-paths" $ do
+        assertBoolM "The expression is not partial" $ Expr.containsNode isPartial e
+    , test "inconsistent-paths" $ do
         Just c <- solcRuntime "C"
             [i|
             contract C {
@@ -1117,8 +1146,8 @@ tests = testGroup "hevm"
             opts = defaultVeriOpts{ maxIter = Just 10, askSmtIters = 5 }
         (e, [Qed _]) <- withSolvers Z3 1 Nothing $
           \s -> checkAssert s defaultPanicCodes c sig [] opts
-        assertBool "The expression is not partial" $ Expr.containsNode isPartial e
-    , testCase "symbolic-loops-not-reached" $ do
+        assertBoolM "The expression is not partial" $ Expr.containsNode isPartial e
+    , test "symbolic-loops-not-reached" $ do
         Just c <- solcRuntime "C"
             [i|
             contract C {
@@ -1136,10 +1165,10 @@ tests = testGroup "hevm"
             opts = defaultVeriOpts{ maxIter = Just 5, askSmtIters = 1 }
         (e, [Qed _]) <- withSolvers Z3 1 Nothing $
           \s -> checkAssert s defaultPanicCodes c sig [] opts
-        assertBool "The expression is partial" $ not (Expr.containsNode isPartial e)
+        assertBoolM "The expression is partial" $ not (Expr.containsNode isPartial e)
     ]
   , testGroup "Symbolic Addresses"
-    [ testCase "symbolic-address-create" $ do
+    [ test "symbolic-address-create" $ do
         let src = [i|
                   contract A {
                     constructor() payable {}
@@ -1164,11 +1193,11 @@ tests = testGroup "hevm"
             let code = case ca.code of
                   RuntimeCode (ConcreteRuntimeCode c') -> c'
                   _ -> internalError "expected concrete code"
-            assertEqual "balance mismatch" (Var "arg1") ca.balance
-            assertEqual "code mismatch" (stripBytecodeMetadata a) (stripBytecodeMetadata code)
-            assertEqual "nonce mismatch" (Just 1) ca.nonce
-          _ -> assertBool "too many success nodes!" False
-    , testCase "symbolic-balance-call" $ do
+            assertEqualM "balance mismatch" (Var "arg1") ca.balance
+            assertEqualM "code mismatch" (stripBytecodeMetadata a) (stripBytecodeMetadata code)
+            assertEqualM "nonce mismatch" (Just 1) ca.nonce
+          _ -> assertBoolM "too many success nodes!" False
+    , test "symbolic-balance-call" $ do
         let src = [i|
                   contract A {
                     function f() public payable returns (uint) {
@@ -1186,9 +1215,9 @@ tests = testGroup "hevm"
                   |]
         Just c <- solcRuntime "C" src
         res <- reachableUserAsserts c Nothing
-        assertBool "unexpected cex" (isRight res)
+        assertBoolM "unexpected cex" (isRight res)
     -- TODO: implement missing aliasing rules
-    , expectFail $ testCase "deployed-contract-addresses-cannot-alias" $ do
+    , expectFail $ test "deployed-contract-addresses-cannot-alias" $ do
         Just c <- solcRuntime "C"
           [i|
             contract A {}
@@ -1200,8 +1229,8 @@ tests = testGroup "hevm"
             }
           |]
         res <- reachableUserAsserts c Nothing
-        assertBool "should not be able to alias" (isRight res)
-    , testCase "addresses-in-args-can-alias-anything" $ do
+        assertBoolM "should not be able to alias" (isRight res)
+    , test "addresses-in-args-can-alias-anything" $ do
         let addrs :: [Text]
             addrs = ["address(this)", "tx.origin", "block.coinbase", "msg.sender"]
             sig = Just $ Sig "f(address)" [AbiAddressType]
@@ -1218,12 +1247,13 @@ tests = testGroup "hevm"
           Left [cex] <- reachableUserAsserts c sig
           pure cex.addrs
 
-        let check as a = (Map.lookup (SymAddr "arg1") as) @?= (Map.lookup a as)
-        check self (SymAddr "entrypoint")
-        check origin (SymAddr "origin")
-        check coinbase (SymAddr "coinbase")
-        check caller (SymAddr "caller")
-    , testCase "addresses-in-args-can-alias-themselves" $ do
+        liftIO $ do
+          let check as a = (Map.lookup (SymAddr "arg1") as) @?= (Map.lookup a as)
+          check self (SymAddr "entrypoint")
+          check origin (SymAddr "origin")
+          check coinbase (SymAddr "coinbase")
+          check caller (SymAddr "caller")
+    , test "addresses-in-args-can-alias-themselves" $ do
         Just c <- solcRuntime "C"
           [i|
             contract C {
@@ -1236,9 +1266,9 @@ tests = testGroup "hevm"
         Left [cex] <- reachableUserAsserts c sig
         let arg1 = fromJust $ Map.lookup (SymAddr "arg1") cex.addrs
             arg2 = fromJust $ Map.lookup (SymAddr "arg1") cex.addrs
-        assertEqual "should match" arg1 arg2
+        assertEqualM "should match" arg1 arg2
     -- TODO: fails due to missing aliasing rules
-    , expectFail $ testCase "tx.origin cannot alias deployed contracts" $ do
+    , expectFail $ test "tx.origin cannot alias deployed contracts" $ do
         Just c <- solcRuntime "C"
           [i|
             contract A {}
@@ -1250,8 +1280,8 @@ tests = testGroup "hevm"
             }
           |]
         cexs <- reachableUserAsserts c Nothing
-        assertBool "unexpected cex" (isRight cexs)
-    , testCase "tx.origin can alias everything else" $ do
+        assertBoolM "unexpected cex" (isRight cexs)
+    , test "tx.origin can alias everything else" $ do
         let addrs = ["address(this)", "block.coinbase", "msg.sender", "arg"] :: [Text]
             sig = Just $ Sig "f(address)" [AbiAddressType]
             checkVs vs = [i|
@@ -1267,12 +1297,13 @@ tests = testGroup "hevm"
           Left [cex] <- reachableUserAsserts c sig
           pure cex.addrs
 
-        let check as a = (Map.lookup (SymAddr "origin") as) @?= (Map.lookup a as)
-        check self (SymAddr "entrypoint")
-        check coinbase (SymAddr "coinbase")
-        check caller (SymAddr "caller")
-        check arg (SymAddr "arg1")
-    , testCase "coinbase can alias anything" $ do
+        liftIO $ do
+          let check as a = (Map.lookup (SymAddr "origin") as) @?= (Map.lookup a as)
+          check self (SymAddr "entrypoint")
+          check coinbase (SymAddr "coinbase")
+          check caller (SymAddr "caller")
+          check arg (SymAddr "arg1")
+    , test "coinbase can alias anything" $ do
         let addrs = ["address(this)", "tx.origin", "msg.sender", "a", "arg"] :: [Text]
             sig = Just $ Sig "f(address)" [AbiAddressType]
             checkVs vs = [i|
@@ -1290,13 +1321,14 @@ tests = testGroup "hevm"
           Left [cex] <- reachableUserAsserts c sig
           pure cex.addrs
 
-        let check as a' = (Map.lookup (SymAddr "coinbase") as) @?= (Map.lookup a' as)
-        check self (SymAddr "entrypoint")
-        check origin (SymAddr "origin")
-        check caller (SymAddr "caller")
-        check a (SymAddr "freshSymAddr1")
-        check arg (SymAddr "arg1")
-    , testCase "caller can alias anything" $ do
+        liftIO $ do
+          let check as a' = (Map.lookup (SymAddr "coinbase") as) @?= (Map.lookup a' as)
+          check self (SymAddr "entrypoint")
+          check origin (SymAddr "origin")
+          check caller (SymAddr "caller")
+          check a (SymAddr "freshSymAddr1")
+          check arg (SymAddr "arg1")
+    , test "caller can alias anything" $ do
         let addrs = ["address(this)", "tx.origin", "block.coinbase", "a", "arg"] :: [Text]
             sig = Just $ Sig "f(address)" [AbiAddressType]
             checkVs vs = [i|
@@ -1314,13 +1346,14 @@ tests = testGroup "hevm"
           Left [cex] <- reachableUserAsserts c sig
           pure cex.addrs
 
-        let check as a' = (Map.lookup (SymAddr "caller") as) @?= (Map.lookup a' as)
-        check self (SymAddr "entrypoint")
-        check origin (SymAddr "origin")
-        check coinbase (SymAddr "coinbase")
-        check a (SymAddr "freshSymAddr1")
-        check arg (SymAddr "arg1")
-    , testCase "vm.load fails for a potentially aliased address" $ do
+        liftIO $ do
+          let check as a' = (Map.lookup (SymAddr "caller") as) @?= (Map.lookup a' as)
+          check self (SymAddr "entrypoint")
+          check origin (SymAddr "origin")
+          check coinbase (SymAddr "coinbase")
+          check a (SymAddr "freshSymAddr1")
+          check arg (SymAddr "arg1")
+    , test "vm.load fails for a potentially aliased address" $ do
         Just c <- solcRuntime "C"
           [i|
             interface Vm {
@@ -1336,7 +1369,7 @@ tests = testGroup "hevm"
         (_, [Cex _]) <- withSolvers Z3 1 Nothing $ \s ->
           verifyContract s c Nothing [] defaultVeriOpts Nothing (Just $ checkBadCheatCode "load(address,bytes32)")
         pure ()
-    , testCase "vm.store fails for a potentially aliased address" $ do
+    , test "vm.store fails for a potentially aliased address" $ do
         Just c <- solcRuntime "C"
           [i|
             interface Vm {
@@ -1353,7 +1386,7 @@ tests = testGroup "hevm"
           verifyContract s c Nothing [] defaultVeriOpts Nothing (Just $ checkBadCheatCode "store(address,bytes32,bytes32)")
         pure ()
     -- TODO: make this work properly
-    , testCase "transfering-eth-does-not-dealias" $ do
+    , test "transfering-eth-does-not-dealias" $ do
         Just c <- solcRuntime "C"
           [i|
             // we can't do calls to unknown code yet so we use selfdestruct
@@ -1383,8 +1416,8 @@ tests = testGroup "hevm"
           |]
         Right e <- reachableUserAsserts c Nothing
         -- TODO: this should work one day
-        assertBool "should be partial" (Expr.containsNode isPartial e)
-    , testCase "addresses-in-context-are-symbolic" $ do
+        assertBoolM "should be partial" (Expr.containsNode isPartial e)
+    , test "addresses-in-context-are-symbolic" $ do
         Just a <- solcRuntime "A"
           [i|
             contract A {
@@ -1419,17 +1452,17 @@ tests = testGroup "hevm"
           |]
         [acex,bcex,ccex,dcex] <- forM [a,b,c,d] $ \con -> do
           Left [cex] <- reachableUserAsserts con Nothing
-          assertEqual "wrong number of addresses" 1 (length (Map.keys cex.addrs))
+          assertEqualM "wrong number of addresses" 1 (length (Map.keys cex.addrs))
           pure cex
 
-        assertEqual "wrong model for a" (Addr 0) (fromJust $ Map.lookup (SymAddr "caller") acex.addrs)
-        assertEqual "wrong model for b" (Addr 1) (fromJust $ Map.lookup (SymAddr "coinbase") bcex.addrs)
-        assertEqual "wrong model for c" (Addr 2) (fromJust $ Map.lookup (SymAddr "origin") ccex.addrs)
-        assertEqual "wrong model for d" (Addr 3) (fromJust $ Map.lookup (SymAddr "entrypoint") dcex.addrs)
+        assertEqualM "wrong model for a" (Addr 0) (fromJust $ Map.lookup (SymAddr "caller") acex.addrs)
+        assertEqualM "wrong model for b" (Addr 1) (fromJust $ Map.lookup (SymAddr "coinbase") bcex.addrs)
+        assertEqualM "wrong model for c" (Addr 2) (fromJust $ Map.lookup (SymAddr "origin") ccex.addrs)
+        assertEqualM "wrong model for d" (Addr 3) (fromJust $ Map.lookup (SymAddr "entrypoint") dcex.addrs)
     ]
   , testGroup "Symbolic execution"
       [
-     testCase "require-test" $ do
+     test "require-test" $ do
         Just c <- solcRuntime "MyContract"
             [i|
             contract MyContract {
@@ -1440,9 +1473,10 @@ tests = testGroup "hevm"
              }
             |]
         (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(int256)" [AbiIntType 256])) [] defaultVeriOpts
-        putStrLn "Require works as expected"
+        putStrLnM "Require works as expected"
      ,
-     testCase "ITE-with-bitwise-AND" $ do
+     -- here test
+     test "ITE-with-bitwise-AND" $ do
        Just c <- solcRuntime "C"
          [i|
          contract C {
@@ -1460,9 +1494,9 @@ tests = testGroup "hevm"
          |]
        -- should find a counterexample
        (_, [Cex _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "f(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
-       putStrLn "expected counterexample found"
+       putStrLnM "expected counterexample found"
      ,
-     testCase "ITE-with-bitwise-OR" $ do
+     test "ITE-with-bitwise-OR" $ do
        Just c <- solcRuntime "C"
          [i|
          contract C {
@@ -1478,14 +1512,14 @@ tests = testGroup "hevm"
          }
          |]
        (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "f(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
-       putStrLn "this should always be true, due to bitwise OR with positive value"
+       putStrLnM "this should always be true, due to bitwise OR with positive value"
     ,
     -- CopySlice check
     -- uses identity precompiled contract (0x4) to copy memory
     -- checks 9af114613075a2cd350633940475f8b6699064de (readByte + CopySlice had src/dest mixed up)
     -- without 9af114613 it dies with: `Exception: UnexpectedSymbolicArg 296 "MSTORE index"`
     --       TODO: check  9e734b9da90e3e0765128b1f20ce1371f3a66085 (bufLength + copySlice was off by 1)
-    testCase "copyslice-check" $ do
+    test "copyslice-check" $ do
       Just c <- solcRuntime "C"
         [i|
         contract C {
@@ -1506,10 +1540,10 @@ tests = testGroup "hevm"
       let sig = Just (Sig "checkval(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])
       (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s ->
         checkAssert s defaultPanicCodes c sig [] defaultVeriOpts
-      putStrLn $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"
+      putStrLnM $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"
      ,
      -- TODO look at tests here for SAR: https://github.com/dapphub/dapptools/blob/01ef8ea418c3fe49089a44d56013d8fcc34a1ec2/src/dapp-tests/pass/constantinople.sol#L250
-     testCase "opcode-sar-neg" $ do
+     test "opcode-sar-neg" $ do
         Just c <- solcRuntime "MyContract"
             [i|
             contract MyContract {
@@ -1524,9 +1558,9 @@ tests = testGroup "hevm"
              }
             |]
         (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(int256,int256)" [AbiIntType 256, AbiIntType 256])) [] defaultVeriOpts
-        putStrLn "SAR works as expected"
+        putStrLnM "SAR works as expected"
      ,
-     testCase "opcode-sar-pos" $ do
+     test "opcode-sar-pos" $ do
         Just c <- solcRuntime "MyContract"
             [i|
             contract MyContract {
@@ -1541,9 +1575,9 @@ tests = testGroup "hevm"
              }
             |]
         (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(int256,int256)" [AbiIntType 256, AbiIntType 256])) [] defaultVeriOpts
-        putStrLn "SAR works as expected"
+        putStrLnM "SAR works as expected"
      ,
-     testCase "opcode-sar-fixedval-pos" $ do
+     test "opcode-sar-fixedval-pos" $ do
         Just c <- solcRuntime "MyContract"
             [i|
             contract MyContract {
@@ -1558,9 +1592,9 @@ tests = testGroup "hevm"
              }
             |]
         (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(int256,int256)" [AbiIntType 256, AbiIntType 256])) [] defaultVeriOpts
-        putStrLn "SAR works as expected"
+        putStrLnM "SAR works as expected"
      ,
-     testCase "opcode-sar-fixedval-neg" $ do
+     test "opcode-sar-fixedval-neg" $ do
         Just c <- solcRuntime "MyContract"
             [i|
             contract MyContract {
@@ -1575,9 +1609,9 @@ tests = testGroup "hevm"
              }
             |]
         (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(int256,int256)" [AbiIntType 256, AbiIntType 256])) [] defaultVeriOpts
-        putStrLn "SAR works as expected"
+        putStrLnM "SAR works as expected"
      ,
-     testCase "opcode-div-zero-1" $ do
+     test "opcode-div-zero-1" $ do
         Just c <- solcRuntime "MyContract"
             [i|
             contract MyContract {
@@ -1592,9 +1626,9 @@ tests = testGroup "hevm"
             }
             |]
         (_, [Qed _])  <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
-        putStrLn "sdiv works as expected"
+        putStrLnM "sdiv works as expected"
       ,
-     testCase "opcode-sdiv-zero-1" $ do
+     test "opcode-sdiv-zero-1" $ do
         Just c <- solcRuntime "MyContract"
             [i|
             contract MyContract {
@@ -1609,9 +1643,9 @@ tests = testGroup "hevm"
             }
             |]
         (_, [Qed _])  <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
-        putStrLn "sdiv works as expected"
+        putStrLnM "sdiv works as expected"
       ,
-     testCase "opcode-sdiv-zero-2" $ do
+     test "opcode-sdiv-zero-2" $ do
         Just c <- solcRuntime "MyContract"
             [i|
             contract MyContract {
@@ -1626,9 +1660,9 @@ tests = testGroup "hevm"
             }
             |]
         (_, [Qed _])  <- withSolvers CVC5 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
-        putStrLn "sdiv works as expected"
+        putStrLnM "sdiv works as expected"
       ,
-     testCase "signed-overflow-checks" $ do
+     test "signed-overflow-checks" $ do
         Just c <- solcRuntime "C"
             [i|
             contract C {
@@ -1638,9 +1672,9 @@ tests = testGroup "hevm"
             }
             |]
         (_, [Cex (_, _)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x11] c (Just (Sig "fun(int256)" [AbiIntType 256])) [] defaultVeriOpts
-        putStrLn "expected cex discovered"
+        putStrLnM "expected cex discovered"
       ,
-     testCase "opcode-signextend-neg" $ do
+     test "opcode-signextend-neg" $ do
         Just c <- solcRuntime "MyContract"
             [i|
             contract MyContract {
@@ -1660,9 +1694,9 @@ tests = testGroup "hevm"
             }
             |]
         (_, [Qed _])  <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "foo(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
-        putStrLn "signextend works as expected"
+        putStrLnM "signextend works as expected"
       ,
-     testCase "opcode-signextend-pos-nochop" $ do
+     test "opcode-signextend-pos-nochop" $ do
         Just c <- solcRuntime "MyContract"
             [i|
             contract MyContract {
@@ -1678,9 +1712,9 @@ tests = testGroup "hevm"
             }
             |]
         (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256,uint8)" [AbiUIntType 256, AbiUIntType 8])) [] defaultVeriOpts
-        putStrLn "signextend works as expected"
+        putStrLnM "signextend works as expected"
       ,
-      testCase "opcode-signextend-pos-chopped" $ do
+      test "opcode-signextend-pos-chopped" $ do
         Just c <- solcRuntime "MyContract"
             [i|
             contract MyContract {
@@ -1696,10 +1730,10 @@ tests = testGroup "hevm"
             }
             |]
         (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256,uint8)" [AbiUIntType 256, AbiUIntType 8])) [] defaultVeriOpts
-        putStrLn "signextend works as expected"
+        putStrLnM "signextend works as expected"
       ,
       -- when b is too large, value is unchanged
-      testCase "opcode-signextend-pos-b-toolarge" $ do
+      test "opcode-signextend-pos-b-toolarge" $ do
         Just c <- solcRuntime "MyContract"
             [i|
             contract MyContract {
@@ -1714,9 +1748,9 @@ tests = testGroup "hevm"
             }
             |]
         (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256,uint8)" [AbiUIntType 256, AbiUIntType 8])) [] defaultVeriOpts
-        putStrLn "signextend works as expected"
+        putStrLnM "signextend works as expected"
      ,
-     testCase "opcode-shl" $ do
+     test "opcode-shl" $ do
         Just c <- solcRuntime "MyContract"
             [i|
             contract MyContract {
@@ -1732,9 +1766,9 @@ tests = testGroup "hevm"
              }
             |]
         (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
-        putStrLn "SAR works as expected"
+        putStrLnM "SAR works as expected"
      ,
-     testCase "opcode-xor-cancel" $ do
+     test "opcode-xor-cancel" $ do
         Just c <- solcRuntime "MyContract"
             [i|
             contract MyContract {
@@ -1749,9 +1783,9 @@ tests = testGroup "hevm"
              }
             |]
         (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
-        putStrLn "XOR works as expected"
+        putStrLnM "XOR works as expected"
       ,
-      testCase "opcode-xor-reimplement" $ do
+      test "opcode-xor-reimplement" $ do
         Just c <- solcRuntime "MyContract"
             [i|
             contract MyContract {
@@ -1765,9 +1799,9 @@ tests = testGroup "hevm"
              }
             |]
         (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
-        putStrLn "XOR works as expected"
+        putStrLnM "XOR works as expected"
       ,
-      testCase "opcode-add-commutative" $ do
+      test "opcode-add-commutative" $ do
         Just c <- solcRuntime "MyContract"
             [i|
             contract MyContract {
@@ -1787,14 +1821,14 @@ tests = testGroup "hevm"
           (_, [Cex (_, ctr)]) -> do
             let x = getVar ctr "arg1"
             let y = getVar ctr "arg2"
-            putStrLn $ "y:" <> show y
-            putStrLn $ "x:" <> show x
-            assertEqual "Addition is not commutative... that's wrong" False True
+            putStrLnM $ "y:" <> show y
+            putStrLnM $ "x:" <> show x
+            assertEqualM "Addition is not commutative... that's wrong" False True
           (_, [Qed _]) -> do
-            putStrLn "adding is commutative"
+            putStrLnM "adding is commutative"
           _ -> internalError "Unexpected"
       ,
-      testCase "opcode-div-res-zero-on-div-by-zero" $ do
+      test "opcode-div-res-zero-on-div-by-zero" $ do
         Just c <- solcRuntime "MyContract"
             [i|
             contract MyContract {
@@ -1809,11 +1843,11 @@ tests = testGroup "hevm"
             }
             |]
         (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint16)" [AbiUIntType 16])) [] defaultVeriOpts
-        putStrLn "DIV by zero is zero"
+        putStrLnM "DIV by zero is zero"
       ,
       -- Somewhat tautological since we are asserting the precondition
       -- on the same form as the actual "requires" clause.
-      testCase "SafeAdd success case" $ do
+      test "SafeAdd success case" $ do
         Just safeAdd <- solcRuntime "SafeAdd"
           [i|
           contract SafeAdd {
@@ -1838,10 +1872,10 @@ tests = testGroup "hevm"
             sig = Just (Sig "add(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])
         (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s ->
           verifyContract s safeAdd sig [] defaultVeriOpts (Just pre) (Just post)
-        putStrLn $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"
+        putStrLnM $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"
      ,
 
-      testCase "x == y => x + y == 2 * y" $ do
+      test "x == y => x + y == 2 * y" $ do
         Just safeAdd <- solcRuntime "SafeAdd"
           [i|
           contract SafeAdd {
@@ -1865,9 +1899,9 @@ tests = testGroup "hevm"
                    _ -> PBool True
         (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s ->
           verifyContract s safeAdd (Just (Sig "add(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts (Just pre) (Just post)
-        putStrLn $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"
+        putStrLnM $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"
       ,
-      testCase "summary storage writes" $ do
+      test "summary storage writes" $ do
         Just c <- solcRuntime "A"
           [i|
           contract A {
@@ -1896,11 +1930,11 @@ tests = testGroup "hevm"
             sig = Just (Sig "f(uint256)" [AbiUIntType 256])
         (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s ->
           verifyContract s c sig [] defaultVeriOpts (Just pre) (Just post)
-        putStrLn $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"
+        putStrLnM $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"
         ,
         -- tests how whiffValue handles Neg via application of the triple IsZero simplification rule
         -- regression test for: https://github.com/dapphub/dapptools/pull/698
-        testCase "Neg" $ do
+        test "Neg" $ do
             let src =
                   [i|
                     object "Neg" {
@@ -1919,11 +1953,11 @@ tests = testGroup "hevm"
                       }
                     }
                     |]
-            Just c <- yulRuntime "Neg" src
+            Just c <- liftIO $ yulRuntime "Neg" src
             (res, [Qed _]) <- withSolvers Z3 4 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "hello(address)" [AbiAddressType])) [] defaultVeriOpts
-            putStrLn $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"
+            putStrLnM $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"
         ,
-        testCase "catch-storage-collisions-noproblem" $ do
+        test "catch-storage-collisions-noproblem" $ do
           Just c <- solcRuntime "A"
             [i|
             contract A {
@@ -1958,11 +1992,11 @@ tests = testGroup "hevm"
               sig = Just (Sig "f(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])
           (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s ->
             verifyContract s c sig [] defaultVeriOpts (Just pre) (Just post)
-          putStrLn "Correct, this can never fail"
+          putStrLnM "Correct, this can never fail"
         ,
         -- Inspired by these `msg.sender == to` token bugs
         -- which break linearity of totalSupply.
-        testCase "catch-storage-collisions-good" $ do
+        test "catch-storage-collisions-good" $ do
           Just c <- solcRuntime "A"
             [i|
             contract A {
@@ -1997,12 +2031,12 @@ tests = testGroup "hevm"
             verifyContract s c sig [] defaultVeriOpts (Just pre) (Just post)
           let x = getVar ctr "arg1"
           let y = getVar ctr "arg2"
-          putStrLn $ "y:" <> show y
-          putStrLn $ "x:" <> show x
-          assertEqual "Catch storage collisions" x y
-          putStrLn "expected counterexample found"
+          putStrLnM $ "y:" <> show y
+          putStrLnM $ "x:" <> show x
+          assertEqualM "Catch storage collisions" x y
+          putStrLnM "expected counterexample found"
         ,
-        testCase "simple-assert" $ do
+        test "simple-assert" $ do
           Just c <- solcRuntime "C"
             [i|
             contract C {
@@ -2012,9 +2046,9 @@ tests = testGroup "hevm"
              }
             |]
           (_, [Cex (Failure _ _ (Revert msg), _)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "foo()" [])) [] defaultVeriOpts
-          assertEqual "incorrect revert msg" msg (ConcreteBuf $ panicMsg 0x01)
+          assertEqualM "incorrect revert msg" msg (ConcreteBuf $ panicMsg 0x01)
         ,
-        testCase "simple-assert-2" $ do
+        test "simple-assert-2" $ do
           Just c <- solcRuntime "C"
             [i|
             contract C {
@@ -2024,10 +2058,10 @@ tests = testGroup "hevm"
              }
             |]
           (_, [(Cex (_, ctr))]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "foo(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
-          assertEqual "Must be 10" 10 $ getVar ctr "arg1"
-          putStrLn "Got 10 Cex, as expected"
+          assertEqualM "Must be 10" 10 $ getVar ctr "arg1"
+          putStrLnM "Got 10 Cex, as expected"
         ,
-        testCase "assert-fail-equal" $ do
+        test "assert-fail-equal" $ do
           Just c <- solcRuntime "AssertFailEqual"
             [i|
             contract AssertFailEqual {
@@ -2039,10 +2073,10 @@ tests = testGroup "hevm"
             |]
           (_, [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"
+          assertBoolM "0 must be one of the Cex-es" $ isJust $ List.elemIndex 0 ints
+          putStrLnM "expected 2 counterexamples found, one Cex is the 0 value"
         ,
-        testCase "assert-fail-notequal" $ do
+        test "assert-fail-notequal" $ do
           Just c <- solcRuntime "AssertFailNotEqual"
             [i|
             contract AssertFailNotEqual {
@@ -2055,10 +2089,10 @@ tests = testGroup "hevm"
           (_, [Cex (_, a), Cex (_, b)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
           let x = getVar a "arg1"
           let y = getVar b "arg1"
-          assertBool "At least one has to be 0, to go through the first assert" (x == 0 || y == 0)
-          putStrLn "expected 2 counterexamples found."
+          assertBoolM "At least one has to be 0, to go through the first assert" (x == 0 || y == 0)
+          putStrLnM "expected 2 counterexamples found."
         ,
-        testCase "assert-fail-twoargs" $ do
+        test "assert-fail-twoargs" $ do
           Just c <- solcRuntime "AssertFailTwoParams"
             [i|
             contract AssertFailTwoParams {
@@ -2069,9 +2103,9 @@ tests = testGroup "hevm"
              }
             |]
           (_, [Cex _, Cex _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
-          putStrLn "expected 2 counterexamples found"
+          putStrLnM "expected 2 counterexamples found"
         ,
-        testCase "assert-2nd-arg" $ do
+        test "assert-2nd-arg" $ do
           Just c <- solcRuntime "AssertFailTwoParams"
             [i|
             contract AssertFailTwoParams {
@@ -2081,11 +2115,11 @@ tests = testGroup "hevm"
              }
             |]
           (_, [Cex (_, ctr)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
-          assertEqual "Must be 666" 666 $ getVar ctr "arg2"
-          putStrLn "Found arg2 Ctx to be 666"
+          assertEqualM "Must be 666" 666 $ getVar ctr "arg2"
+          putStrLnM "Found arg2 Ctx to be 666"
         ,
         -- LSB is zeroed out, byte(31,x) takes LSB, so y==0 always holds
-        testCase "check-lsb-msb1" $ do
+        test "check-lsb-msb1" $ do
           Just c <- solcRuntime "C"
             [i|
             contract C {
@@ -2098,11 +2132,11 @@ tests = testGroup "hevm"
             }
             |]
           (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "foo(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
-          putStrLn $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"
+          putStrLnM $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"
         ,
         -- We zero out everything but the LSB byte. However, byte(31,x) takes the LSB byte
         -- so there is a counterexamle, where LSB of x is not zero
-        testCase "check-lsb-msb2" $ do
+        test "check-lsb-msb2" $ do
           Just c <- solcRuntime "C"
             [i|
             contract C {
@@ -2115,12 +2149,12 @@ tests = testGroup "hevm"
             }
             |]
           (_, [Cex (_, ctr)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "foo(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
-          assertBool "last byte must be non-zero" $ ((Data.Bits..&.) (getVar ctr "arg1") 0xff) > 0
-          putStrLn "Expected counterexample found"
+          assertBoolM "last byte must be non-zero" $ ((Data.Bits..&.) (getVar ctr "arg1") 0xff) > 0
+          putStrLnM "Expected counterexample found"
         ,
         -- We zero out everything but the 2nd LSB byte. However, byte(31,x) takes the 2nd LSB byte
         -- so there is a counterexamle, where 2nd LSB of x is not zero
-        testCase "check-lsb-msb3 -- 2nd byte" $ do
+        test "check-lsb-msb3 -- 2nd byte" $ do
           Just c <- solcRuntime "C"
             [i|
             contract C {
@@ -2133,11 +2167,11 @@ tests = testGroup "hevm"
             }
             |]
           (_, [Cex (_, ctr)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "foo(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
-          assertBool "second to last byte must be non-zero" $ ((Data.Bits..&.) (getVar ctr "arg1") 0xff00) > 0
-          putStrLn "Expected counterexample found"
+          assertBoolM "second to last byte must be non-zero" $ ((Data.Bits..&.) (getVar ctr "arg1") 0xff00) > 0
+          putStrLnM "Expected counterexample found"
         ,
         -- Reverse of thest above
-        testCase "check-lsb-msb4 2nd byte rev" $ do
+        test "check-lsb-msb4 2nd byte rev" $ do
           Just c <- solcRuntime "C"
             [i|
             contract C {
@@ -2152,10 +2186,10 @@ tests = testGroup "hevm"
             }
             |]
           (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "foo(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
-          putStrLn $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"
+          putStrLnM $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"
         ,
         -- Bitwise OR operation test
-        testCase "opcode-bitwise-or-full-1s" $ do
+        test "opcode-bitwise-or-full-1s" $ do
           Just c <- solcRuntime "C"
             [i|
             contract C {
@@ -2168,10 +2202,10 @@ tests = testGroup "hevm"
             }
             |]
           (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "foo(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
-          putStrLn "When OR-ing with full 1's we should get back full 1's"
+          putStrLnM "When OR-ing with full 1's we should get back full 1's"
         ,
         -- Bitwise OR operation test
-        testCase "opcode-bitwise-or-byte-of-1s" $ do
+        test "opcode-bitwise-or-byte-of-1s" $ do
           Just c <- solcRuntime "C"
             [i|
             contract C {
@@ -2185,9 +2219,9 @@ tests = testGroup "hevm"
             }
             |]
           (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "foo(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
-          putStrLn "When OR-ing with a byte of 1's, we should get 1's back there"
+          putStrLnM "When OR-ing with a byte of 1's, we should get 1's back there"
         ,
-        testCase "Deposit contract loop (z3)" $ do
+        test "Deposit contract loop (z3)" $ do
           Just c <- solcRuntime "Deposit"
             [i|
             contract Deposit {
@@ -2207,9 +2241,9 @@ tests = testGroup "hevm"
              }
             |]
           (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "deposit(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
-          putStrLn $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"
+          putStrLnM $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"
         ,
-        testCase "Deposit-contract-loop-error-version" $ do
+        test "Deposit-contract-loop-error-version" $ do
           Just c <- solcRuntime "Deposit"
             [i|
             contract Deposit {
@@ -2229,10 +2263,10 @@ tests = testGroup "hevm"
              }
             |]
           (_, [Cex (_, ctr)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s allPanicCodes c (Just (Sig "deposit(uint8)" [AbiUIntType 8])) [] defaultVeriOpts
-          assertEqual "Must be 255" 255 $ getVar ctr "arg1"
-          putStrLn  $ "expected counterexample found, and it's correct: " <> (show $ getVar ctr "arg1")
+          assertEqualM "Must be 255" 255 $ getVar ctr "arg1"
+          putStrLnM  $ "expected counterexample found, and it's correct: " <> (show $ getVar ctr "arg1")
         ,
-        testCase "explore function dispatch" $ do
+        test "explore function dispatch" $ do
           Just c <- solcRuntime "A"
             [i|
             contract A {
@@ -2242,9 +2276,9 @@ tests = testGroup "hevm"
             }
             |]
           (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts
-          putStrLn $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"
+          putStrLnM $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"
         ,
-        testCase "check-asm-byte-in-bounds" $ do
+        test "check-asm-byte-in-bounds" $ do
           Just c <- solcRuntime "C"
             [i|
             contract C {
@@ -2261,9 +2295,9 @@ tests = testGroup "hevm"
             }
             |]
           (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts
-          putStrLn "in bounds byte reads return the expected value"
+          putStrLnM "in bounds byte reads return the expected value"
         ,
-        testCase "check-div-mod-sdiv-smod-by-zero-constant-prop" $ do
+        test "check-div-mod-sdiv-smod-by-zero-constant-prop" $ do
           Just c <- solcRuntime "C"
             [i|
             contract C {
@@ -2291,9 +2325,9 @@ tests = testGroup "hevm"
             }
             |]
           (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "foo(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
-          putStrLn "div/mod/sdiv/smod by zero works as expected during constant propagation"
+          putStrLnM "div/mod/sdiv/smod by zero works as expected during constant propagation"
         ,
-        testCase "check-asm-byte-oob" $ do
+        test "check-asm-byte-oob" $ do
           Just c <- solcRuntime "C"
             [i|
             contract C {
@@ -2306,9 +2340,9 @@ tests = testGroup "hevm"
             }
             |]
           (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts
-          putStrLn "oob byte reads always return 0"
+          putStrLnM "oob byte reads always return 0"
         ,
-        testCase "injectivity of keccak (diff sizes)" $ do
+        test "injectivity of keccak (diff sizes)" $ do
           Just c <- solcRuntime "A"
             [i|
             contract A {
@@ -2323,7 +2357,7 @@ tests = testGroup "hevm"
           Right _ <- reachableUserAsserts c (Just $ Sig "f(uint128,uint256)" [AbiUIntType 128, AbiUIntType 256])
           pure ()
         ,
-        testCase "injectivity of keccak (32 bytes)" $ do
+        test "injectivity of keccak (32 bytes)" $ do
           Just c <- solcRuntime "A"
             [i|
             contract A {
@@ -2333,9 +2367,9 @@ tests = testGroup "hevm"
             }
             |]
           (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "f(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
-          putStrLn $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"
+          putStrLnM $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"
         ,
-        testCase "injectivity of keccak contrapositive (32 bytes)" $ do
+        test "injectivity of keccak contrapositive (32 bytes)" $ do
           Just c <- solcRuntime "A"
             [i|
             contract A {
@@ -2346,9 +2380,9 @@ tests = testGroup "hevm"
             }
             |]
           (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "f(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
-          putStrLn $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"
+          putStrLnM $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"
         ,
-        testCase "injectivity of keccak (64 bytes)" $ do
+        test "injectivity of keccak (64 bytes)" $ do
           Just c <- solcRuntime "A"
             [i|
             contract A {
@@ -2362,11 +2396,11 @@ tests = testGroup "hevm"
           let y = getVar ctr "arg2"
           let w = getVar ctr "arg3"
           let z = getVar ctr "arg4"
-          assertEqual "x==y for hash collision" x y
-          assertEqual "w==z for hash collision" w z
-          putStrLn "expected counterexample found"
+          assertEqualM "x==y for hash collision" x y
+          assertEqualM "w==z for hash collision" w z
+          putStrLnM "expected counterexample found"
         ,
-        testCase "calldata beyond calldatasize is 0 (symbolic calldata)" $ do
+        test "calldata beyond calldatasize is 0 (symbolic calldata)" $ do
           Just c <- solcRuntime "A"
             [i|
             contract A {
@@ -2381,9 +2415,9 @@ tests = testGroup "hevm"
             }
             |]
           (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts
-          putStrLn $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"
+          putStrLnM $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"
         ,
-        testCase "calldata beyond calldatasize is 0 (concrete dalldata prefix)" $ do
+        test "calldata beyond calldatasize is 0 (concrete dalldata prefix)" $ do
           Just c <- solcRuntime "A"
             [i|
             contract A {
@@ -2398,9 +2432,9 @@ tests = testGroup "hevm"
             }
             |]
           (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "f(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
-          putStrLn $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"
+          putStrLnM $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"
         ,
-        testCase "calldata symbolic access" $ do
+        test "calldata symbolic access" $ do
           Just c <- solcRuntime "A"
             [i|
             contract A {
@@ -2418,9 +2452,9 @@ tests = testGroup "hevm"
             }
             |]
           (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "f(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
-          putStrLn $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"
+          putStrLnM $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"
         ,
-        testCase "multiple-contracts" $ do
+        test "multiple-contracts" $ do
           let code =
                 [i|
                   contract C {
@@ -2441,7 +2475,7 @@ tests = testGroup "hevm"
           Just c <- solcRuntime "C" code
           Just a <- solcRuntime "A" code
           (_, [Cex (_, cex)]) <- withSolvers Z3 1 Nothing $ \s -> do
-            vm <- stToIO $ abstractVM (mkCalldata (Just (Sig "call_A()" [])) []) c Nothing False
+            vm <- liftIO $ stToIO $ abstractVM (mkCalldata (Just (Sig "call_A()" [])) []) c Nothing False
                     <&> set (#state % #callvalue) (Lit 0)
                     <&> over (#env % #contracts)
                        (Map.insert aAddr (initialContract (RuntimeCode (ConcreteRuntimeCode a))))
@@ -2454,10 +2488,10 @@ tests = testGroup "hevm"
                               (Just x, Nothing) -> x /= 0
                               _ -> False
                           _ -> False
-          assertBool "Did not find expected storage cex" testCex
-          putStrLn "expected counterexample found"
+          assertBoolM "Did not find expected storage cex" testCex
+          putStrLnM "expected counterexample found"
         ,
-        expectFail $ testCase "calling unique contracts (read from storage)" $ do
+        expectFail $ test "calling unique contracts (read from storage)" $ do
           Just c <- solcRuntime "C"
             [i|
               contract C {
@@ -2475,9 +2509,9 @@ tests = testGroup "hevm"
               }
             |]
           (_, [Cex _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "call_A()" [])) [] defaultVeriOpts
-          putStrLn "expected counterexample found"
+          putStrLnM "expected counterexample found"
         ,
-        testCase "keccak concrete and sym agree" $ do
+        test "keccak concrete and sym agree" $ do
           Just c <- solcRuntime "C"
             [i|
               contract C {
@@ -2489,9 +2523,9 @@ tests = testGroup "hevm"
               }
             |]
           (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "kecc(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
-          putStrLn $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"
+          putStrLnM $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"
         ,
-        testCase "keccak concrete and sym injectivity" $ do
+        test "keccak concrete and sym injectivity" $ do
           Just c <- solcRuntime "A"
             [i|
               contract A {
@@ -2501,15 +2535,15 @@ tests = testGroup "hevm"
               }
             |]
           (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "f(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
-          putStrLn $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"
+          putStrLnM $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"
         ,
-        testCase "safemath-distributivity-yul" $ do
+        test "safemath-distributivity-yul" $ do
           let yulsafeDistributivity = hex "6355a79a6260003560e01c14156016576015601f565b5b60006000fd60a1565b603d602d604435600435607c565b6039602435600435607c565b605d565b6052604b604435602435605d565b600435607c565b141515605a57fe5b5b565b6000828201821115151560705760006000fd5b82820190505b92915050565b6000818384048302146000841417151560955760006000fd5b82820290505b92915050565b"
-          vm <- stToIO $ abstractVM (mkCalldata (Just (Sig "distributivity(uint256,uint256,uint256)" [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) []) yulsafeDistributivity Nothing False
+          vm <- liftIO $ stToIO $ abstractVM (mkCalldata (Just (Sig "distributivity(uint256,uint256,uint256)" [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) []) yulsafeDistributivity Nothing False
           (_, [Qed _]) <-  withSolvers Z3 1 Nothing $ \s -> verify s defaultVeriOpts vm (Just $ checkAssertions defaultPanicCodes)
-          putStrLn "Proven"
+          putStrLnM "Proven"
         ,
-        testCase "safemath-distributivity-sol" $ do
+        test "safemath-distributivity-sol" $ do
           Just c <- solcRuntime "C"
             [i|
               contract C {
@@ -2532,9 +2566,9 @@ tests = testGroup "hevm"
             |]
 
           (_, [Qed _]) <- withSolvers CVC5 1 (Just 99999999) $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "distributivity(uint256,uint256,uint256)" [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
-          putStrLn "Proven"
+          putStrLnM "Proven"
         ,
-        testCase "storage-cex-1" $ do
+        test "storage-cex-1" $ do
           Just c <- solcRuntime "C"
             [i|
             contract C {
@@ -2554,10 +2588,10 @@ tests = testGroup "hevm"
                                       (Just x, Just y) -> x /= y
                                       _ -> False
                           _ -> False
-          assertBool "Did not find expected storage cex" testCex
-          putStrLn "Expected counterexample found"
+          assertBoolM "Did not find expected storage cex" testCex
+          putStrLnM "Expected counterexample found"
         ,
-        testCase "storage-cex-2" $ do
+        test "storage-cex-2" $ do
           Just c <- solcRuntime "C"
             [i|
             contract C {
@@ -2578,10 +2612,10 @@ tests = testGroup "hevm"
                                       (Just x, Just y) -> x >= y
                                       _ -> False
                           _ -> False
-          assertBool "Did not find expected storage cex" testCex
-          putStrLn "Expected counterexample found"
+          assertBoolM "Did not find expected storage cex" testCex
+          putStrLnM "Expected counterexample found"
         ,
-        testCase "storage-cex-concrete" $ do
+        test "storage-cex-concrete" $ do
           Just c <- solcRuntime "C"
             [i|
             contract C {
@@ -2603,51 +2637,51 @@ tests = testGroup "hevm"
                                       (Just x, Just y) -> x == y
                                       _ -> False
                           _ -> False
-          assertBool "Did not find expected storage cex" testCex
-          putStrLn "Expected counterexample found"
+          assertBoolM "Did not find expected storage cex" testCex
+          putStrLnM "Expected counterexample found"
   ]
   , testGroup "simplification-working"
   [
-    testCase "prop-simp-bool1" $ do
+    test "prop-simp-bool1" $ do
       let
         a = successGen [PAnd (PBool True) (PBool False)]
         b = Expr.simplify a
-      assertEqual "Must simplify down" (successGen [PBool False]) b
-    , testCase "prop-simp-bool2" $ do
+      assertEqualM "Must simplify down" (successGen [PBool False]) b
+    , test "prop-simp-bool2" $ do
       let
         a = successGen [POr (PBool True) (PBool False)]
         b = Expr.simplify a
-      assertEqual "Must simplify down" (successGen []) b
-    , testCase "prop-simp-LT" $ do
+      assertEqualM "Must simplify down" (successGen []) b
+    , test "prop-simp-LT" $ do
       let
         a = successGen [PLT (Lit 1) (Lit 2)]
         b = Expr.simplify a
-      assertEqual "Must simplify down" (successGen []) b
-    , testCase "prop-simp-GEq" $ do
+      assertEqualM "Must simplify down" (successGen []) b
+    , test "prop-simp-GEq" $ do
       let
         a = successGen [PGEq (Lit 1) (Lit 2)]
         b = Expr.simplify a
-      assertEqual "Must simplify down" (successGen [PBool False]) b
-    , testCase "prop-simp-multiple" $ do
+      assertEqualM "Must simplify down" (successGen [PBool False]) b
+    , test "prop-simp-multiple" $ do
       let
         a = successGen [PBool False, PBool True]
         b = Expr.simplify a
-      assertEqual "Must simplify down" (successGen [PBool False]) b
-    , testCase "prop-simp-expr" $ do
+      assertEqualM "Must simplify down" (successGen [PBool False]) b
+    , test "prop-simp-expr" $ do
       let
         a = successGen [PEq (Add (Lit 1) (Lit 2)) (Sub (Lit 4) (Lit 1))]
         b = Expr.simplify a
-      assertEqual "Must simplify down" (successGen []) b
-    , testCase "prop-simp-impl" $ do
+      assertEqualM "Must simplify down" (successGen []) b
+    , test "prop-simp-impl" $ do
       let
         a = successGen [PImpl (PBool False) (PEq (Var "abc") (Var "bcd"))]
         b = Expr.simplify a
-      assertEqual "Must simplify down" (successGen []) b
+      assertEqualM "Must simplify down" (successGen []) b
   ]
   , testGroup "equivalence-checking"
     [
-      testCase "eq-yul-simple-cex" $ do
-        Just aPrgm <- yul ""
+      test "eq-yul-simple-cex" $ do
+        Just aPrgm <- liftIO $ yul ""
           [i|
           {
             calldatacopy(0, 0, 32)
@@ -2657,7 +2691,7 @@ tests = testGroup "hevm"
             default { invalid() }
           }
           |]
-        Just bPrgm <- yul ""
+        Just bPrgm <- liftIO $ yul ""
           [i|
           {
             calldatacopy(0, 0, 32)
@@ -2669,9 +2703,9 @@ tests = testGroup "hevm"
           |]
         withSolvers Z3 3 Nothing $ \s -> do
           a <- equivalenceCheck s aPrgm bPrgm defaultVeriOpts (mkCalldata Nothing [])
-          assertBool "Must have a difference" (any isCex a)
+          assertBoolM "Must have a difference" (any isCex a)
       ,
-      testCase "eq-sol-exp-qed" $ do
+      test "eq-sol-exp-qed" $ do
         Just aPrgm <- solcRuntime "C"
           [i|
             contract C {
@@ -2694,9 +2728,9 @@ tests = testGroup "hevm"
           |]
         withSolvers Z3 3 Nothing $ \s -> do
           a <- equivalenceCheck s aPrgm bPrgm defaultVeriOpts (mkCalldata Nothing [])
-          assertEqual "Must have no difference" [Qed ()] a
+          assertEqualM "Must have no difference" [Qed ()] a
       ,
-      testCase "eq-balance-differs" $ do
+      test "eq-balance-differs" $ do
         Just aPrgm <- solcRuntime "C"
           [i|
             contract Send {
@@ -2725,10 +2759,10 @@ tests = testGroup "hevm"
           |]
         withSolvers Z3 3 Nothing $ \s -> do
           a <- equivalenceCheck s aPrgm bPrgm defaultVeriOpts (mkCalldata Nothing [])
-          assertBool "Must differ" (all isCex a)
+          assertBoolM "Must differ" (all isCex a)
       ,
       -- TODO: this fails because we don't check equivalence of deployed contracts
-      expectFail $ testCase "eq-handles-contract-deployment" $ do
+      expectFail $ test "eq-handles-contract-deployment" $ do
         Just aPrgm <- solcRuntime "B"
           [i|
             contract Send {
@@ -2786,9 +2820,9 @@ tests = testGroup "hevm"
           |]
         withSolvers Z3 3 Nothing $ \s -> do
           a <- equivalenceCheck s aPrgm bPrgm defaultVeriOpts (mkCalldata Nothing [])
-          assertBool "Must differ" (all isCex a)
+          assertBoolM "Must differ" (all isCex a)
       ,
-      testCase "eq-unknown-addr" $ do
+      test "eq-unknown-addr" $ do
         Just aPrgm <- solcRuntime "C"
           [i|
             contract C {
@@ -2810,9 +2844,9 @@ tests = testGroup "hevm"
         withSolvers Z3 3 Nothing $ \s -> do
           let cd = mkCalldata (Just (Sig "a(address,address)" [AbiAddressType, AbiAddressType])) []
           a <- equivalenceCheck s aPrgm bPrgm defaultVeriOpts cd
-          assertEqual "Must be different" (any isCex a) True
+          assertEqualM "Must be different" (any isCex a) True
       ,
-      testCase "eq-sol-exp-cex" $ do
+      test "eq-sol-exp-cex" $ do
         Just aPrgm <- solcRuntime "C"
             [i|
               contract C {
@@ -2835,8 +2869,8 @@ tests = testGroup "hevm"
           |]
         withSolvers Z3 3 Nothing $ \s -> do
           a <- equivalenceCheck s aPrgm bPrgm defaultVeriOpts (mkCalldata Nothing [])
-          assertEqual "Must be different" (any isCex a) True
-      , testCase "eq-all-yul-optimization-tests" $ do
+          assertEqualM "Must be different" (any isCex a) True
+      , test "eq-all-yul-optimization-tests" $ do
         let opts = defaultVeriOpts{ maxIter = Just 5, askSmtIters = 20, loopHeuristic = Naive }
             ignoredTests =
                     -- unbounded loop --
@@ -3042,9 +3076,9 @@ tests = testGroup "hevm"
                     , "reasoningBasedSimplifier/signed_division.yul" -- ACTUAL bug, SDIV
                     ]
 
-        solcRepo <- fromMaybe (internalError "cannot find solidity repo") <$> (lookupEnv "HEVM_SOLIDITY_REPO")
+        solcRepo <- liftIO $ fromMaybe (internalError "cannot find solidity repo") <$> (lookupEnv "HEVM_SOLIDITY_REPO")
         let testDir = solcRepo <> "/test/libyul/yulOptimizerTests"
-        dircontents <- System.Directory.listDirectory testDir
+        dircontents <- liftIO $ System.Directory.listDirectory testDir
         let
           fullpaths = map ((testDir ++ "/") ++) dircontents
           recursiveList :: [FilePath] -> [FilePath] -> IO [FilePath]
@@ -3057,13 +3091,13 @@ tests = testGroup "hevm"
                     recursiveList (ax++fs2) b
                 False -> recursiveList ax (a:b)
           recursiveList [] b = pure b
-        files <- recursiveList fullpaths []
+        files <- liftIO $ recursiveList fullpaths []
         let filesFiltered = filter (\file -> not $ any (`List.isSubsequenceOf` file) ignoredTests) files
 
         -- Takes one file which follows the Solidity Yul optimizer unit tests format,
         -- extracts both the nonoptimized and the optimized versions, and checks equivalence.
         forM_ filesFiltered (\f-> do
-          origcont <- readFile f
+          origcont <- liftIO $ readFile f
           let
             onlyAfter pattern (a:ax) = if a =~ pattern then (a:ax) else onlyAfter pattern ax
             onlyAfter _ [] = []
@@ -3085,31 +3119,32 @@ tests = testGroup "hevm"
             unfiltered = lines origcont
             filteredASym = symbolicMem [ x | x <- unfiltered, (not $ x =~ [re|^//|]) && (not $ x =~ [re|^$|]) ]
             filteredBSym = symbolicMem [ replaceAll "" $ x *=~[re|^//|] | x <- onlyAfter [re|^// step:|] unfiltered, not $ x =~ [re|^$|] ]
-          start <- getCurrentTime
-          putStrLn $ "Checking file: " <> f
-          when opts.debug $ do
-            putStrLn "-------------Original Below-----------------"
+          start <- liftIO $ getCurrentTime
+          putStrLnM $ "Checking file: " <> f
+          conf <- readConfig
+          when conf.debug $ liftIO $ do
+            putStrLnM "-------------Original Below-----------------"
             mapM_ putStrLn unfiltered
-            putStrLn "------------- Filtered A + Symb below-----------------"
+            putStrLnM "------------- Filtered A + Symb below-----------------"
             mapM_ putStrLn filteredASym
-            putStrLn "------------- Filtered B + Symb below-----------------"
+            putStrLnM "------------- Filtered B + Symb below-----------------"
             mapM_ putStrLn filteredBSym
-            putStrLn "------------- END -----------------"
-          Just aPrgm <- yul "" $ T.pack $ unlines filteredASym
-          Just bPrgm <- yul "" $ T.pack $ unlines filteredBSym
-          procs <- getNumProcessors
+            putStrLnM "------------- END -----------------"
+          Just aPrgm <- liftIO $ yul "" $ T.pack $ unlines filteredASym
+          Just bPrgm <- liftIO $ yul "" $ T.pack $ unlines filteredBSym
+          procs <- liftIO $ getNumProcessors
           withSolvers CVC5 (unsafeInto procs) (Just 100) $ \s -> do
             res <- equivalenceCheck s aPrgm bPrgm opts (mkCalldata Nothing [])
-            end <- getCurrentTime
+            end <- liftIO $ getCurrentTime
             case any isCex res of
-              False -> do
+              False -> liftIO $ do
                 print $ "OK. Took " <> (show $ diffUTCTime end start) <> " seconds"
                 let timeouts = filter isTimeout res
                 unless (null timeouts) $ do
-                  putStrLn $ "But " <> (show $ length timeouts) <> " timeout(s) occurred"
+                  putStrLnM $ "But " <> (show $ length timeouts) <> " timeout(s) occurred"
                   internalError "Encountered timeouts"
-              True -> do
-                putStrLn $ "Not OK: " <> show f <> " Got: " <> show res
+              True -> liftIO $ do
+                putStrLnM $ "Not OK: " <> show f <> " Got: " <> show res
                 internalError "Was NOT equivalent"
            )
     ]
@@ -3117,32 +3152,34 @@ tests = testGroup "hevm"
   where
     (===>) = assertSolidityComputation
 
-checkEquivProp :: Prop -> Prop -> IO Bool
+checkEquivProp :: App m => Prop -> Prop -> m Bool
 checkEquivProp = checkEquivBase (\l r -> PNeg (PImpl l r .&& PImpl r l))
 
-checkEquiv :: (Typeable a) => Expr a -> Expr a -> IO Bool
+checkEquiv :: (Typeable a, App m) => Expr a -> Expr a -> m Bool
 checkEquiv = checkEquivBase (./=)
 
-checkEquivBase :: Eq a => (a -> a -> Prop) -> a -> a -> IO Bool
-checkEquivBase mkprop l r = withSolvers Z3 1 (Just 1) $ \solvers -> do
-  if l == r
-     then do
-       putStrLn "skip"
-       pure True
-     else do
-       let smt = assertPropsNoSimp abstRefineDefault [mkprop l r]
-       res <- checkSat solvers smt
-       print res
-       pure $ case res of
-         Unsat -> True
-         EVM.Solvers.Unknown -> True
-         Sat _ -> False
-         Error _ -> False
+checkEquivBase :: (Eq a, App m) => (a -> a -> Prop) -> a -> a -> m Bool
+checkEquivBase mkprop l r = do
+  conf <-  readConfig
+  withSolvers Z3 1 (Just 1) $ \solvers -> liftIO $ do
+    if l == r
+       then do
+         putStrLnM "skip"
+         pure True
+       else do
+         let smt = assertPropsNoSimp conf [mkprop l r]
+         res <- checkSat solvers smt
+         print res
+         pure $ case res of
+           Unsat -> True
+           EVM.Solvers.Unknown -> True
+           Sat _ -> False
+           Error _ -> False
 
 -- | Takes a runtime code and calls it with the provided calldata
 
 -- | Takes a creation code and some calldata, runs the creation code, and calls the resulting contract with the provided calldata
-runSimpleVM :: ByteString -> ByteString -> IO (Maybe ByteString)
+runSimpleVM :: App m => ByteString -> ByteString -> m (Maybe ByteString)
 runSimpleVM x ins = do
   loadVM x >>= \case
     Nothing -> pure Nothing
@@ -3155,14 +3192,15 @@ runSimpleVM x ins = do
        s -> internalError $ show s
 
 -- | Takes a creation code and returns a vm with the result of executing the creation code
-loadVM :: ByteString -> IO (Maybe (VM RealWorld))
+loadVM :: App m => ByteString -> m (Maybe (VM RealWorld))
 loadVM x = do
-  vm <- stToIO $ vmForEthrunCreation x
+  vm <- liftIO $ stToIO $ vmForEthrunCreation x
   vm1 <- Stepper.interpret (Fetch.zero 0 Nothing) vm Stepper.runFully
   case vm1.result of
      Just (VMSuccess (ConcreteBuf targetCode)) -> do
        let target = vm1.state.contract
        vm2 <- Stepper.interpret (Fetch.zero 0 Nothing) vm1 (prepVm target targetCode >> Stepper.run)
+       writeTrace vm2
        pure $ Just vm2
      _ -> pure Nothing
   where
@@ -3196,14 +3234,12 @@ defaultDataLocation t =
   then "memory"
   else ""
 
-runFunction :: Text -> ByteString -> IO (Maybe ByteString)
+runFunction :: App m => Text -> ByteString -> m (Maybe ByteString)
 runFunction c input = do
-  Just x <- singleContract "X" c
-  runSimpleVM x input
+  x <- liftIO $ singleContract "X" c
+  runSimpleVM (fromJust x) input
 
-runStatements
-  :: Text -> [AbiValue] -> AbiType
-  -> IO (Maybe ByteString)
+runStatements :: App m => Text -> [AbiValue] -> AbiType -> m (Maybe ByteString)
 runStatements stmts args t = do
   let params =
         T.intercalate ", "
@@ -3778,10 +3814,10 @@ data Invocation
   = SolidityCall Text [AbiValue]
   deriving Show
 
-assertSolidityComputation :: Invocation -> AbiValue -> IO ()
+assertSolidityComputation :: App m => Invocation -> AbiValue -> m ()
 assertSolidityComputation (SolidityCall s args) x =
   do y <- runStatements s args (abiValueType x)
-     assertEqual (T.unpack s)
+     liftIO $ assertEqual (T.unpack s)
        (fmap Bytes (Just (encodeAbiValue x)))
        (fmap Bytes y)
 
@@ -3799,17 +3835,17 @@ checkBadCheatCode sig _ = \case
   (Failure _ _ (BadCheatCode s)) -> (ConcreteBuf $ into s.unFunctionSelector) ./= (ConcreteBuf $ selector sig)
   _ -> PBool True
 
-allBranchesFail :: ByteString -> Maybe Sig -> IO (Either [SMTCex] (Expr End))
+allBranchesFail :: App m => ByteString -> Maybe Sig -> m (Either [SMTCex] (Expr End))
 allBranchesFail = checkPost (Just p)
   where
     p _ = \case
       Success _ _ _ _ -> PBool False
       _ -> PBool True
 
-reachableUserAsserts :: ByteString -> Maybe Sig -> IO (Either [SMTCex] (Expr End))
+reachableUserAsserts :: App m => ByteString -> Maybe Sig -> m (Either [SMTCex] (Expr End))
 reachableUserAsserts = checkPost (Just $ checkAssertions [0x01])
 
-checkPost :: Maybe (Postcondition RealWorld) -> ByteString -> Maybe Sig -> IO (Either [SMTCex] (Expr End))
+checkPost :: App m => Maybe (Postcondition RealWorld) -> ByteString -> Maybe Sig -> m (Either [SMTCex] (Expr End))
 checkPost post c sig = do
   (e, res) <- withSolvers Z3 1 Nothing $ \s ->
     verifyContract s c sig [] defaultVeriOpts Nothing post