diff --git a/CHANGELOG.md b/CHANGELOG.md
index a6c3faa25..f3df19bc8 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -36,6 +36,9 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
   against incorrectly trivial UNSAT queries
 - Allow --num-solvers option for equivalence checking, use num cores by default
 - Preliminary support for multi-threaded Z3
+- Skip over SMT generation issues due to e.g. CopySlice with symbolic arguments, and return
+  partial results instead of erroring out
+- Fix interpreter's MCOPY handling so that it doesn't error out on symbolic arguments
 
 ## Fixed
 - `concat` is a 2-ary, not an n-ary function in SMT2LIB, declare-const does not exist in QF_AUFBV, replacing
diff --git a/cli/cli.hs b/cli/cli.hs
index 24ee152d7..149e2d0a5 100644
--- a/cli/cli.hs
+++ b/cli/cli.hs
@@ -260,8 +260,10 @@ equivalence cmd = do
     case any isCex res of
       False -> liftIO $ do
         putStrLn "No discrepancies found"
-        when (any isTimeout res) $ do
-          putStrLn "But timeout(s) occurred"
+        when (any isUnknown res || any isError res) $ do
+          putStrLn "But the following issues occurred:"
+          forM_ (groupIssues (filter isError res)) $ \(num, str) -> putStrLn $ "      " <> show num <> "x -> " <> str
+          forM_ (groupIssues (filter isUnknown res)) $ \(num, str) -> putStrLn $ "      " <> show num <> "x -> " <> str
           exitFailure
       True -> liftIO $ do
         let cexs = mapMaybe getCex res
@@ -345,7 +347,7 @@ assert cmd = do
         showExtras solvers cmd calldata expr
       _ -> do
         let cexs = snd <$> mapMaybe getCex res
-            timeouts = mapMaybe getTimeout res
+            smtUnknowns = mapMaybe getUnknown res
             counterexamples
               | null cexs = []
               | otherwise =
@@ -354,15 +356,15 @@ assert cmd = do
                  , ""
                  ] <> fmap (formatCex (fst calldata) Nothing) cexs
             unknowns
-              | null timeouts = []
+              | null smtUnknowns = []
               | otherwise =
                  [ ""
                  , "Could not determine reachability of the following end state(s):"
                  , ""
-                 ] <> fmap (formatExpr) timeouts
+                 ] <> fmap (formatExpr) smtUnknowns
         liftIO $ T.putStrLn $ T.unlines (counterexamples <> unknowns)
         showExtras solvers cmd calldata expr
-        liftIO $ exitFailure
+        liftIO exitFailure
 
 showExtras :: App m => SolverGroup -> Command Options.Unwrapped -> (Expr Buf, [Prop]) -> Expr End -> m ()
 showExtras solvers cmd calldata expr = do
diff --git a/src/EVM.hs b/src/EVM.hs
index f18729fd3..1bf87a7b8 100644
--- a/src/EVM.hs
+++ b/src/EVM.hs
@@ -656,16 +656,22 @@ exec1 = do
                   burn (g_verylow + (unsafeInto g_mcopy)) $
                     accessMemoryRange srcOff sz $ accessMemoryRange dstOff sz $ do
                       next
-                      m <- gets (.state.memory)
-                      case m of
-                        ConcreteMemory mem -> do
-                          buf <- freezeMemory mem
-                          copyBytesToMemory buf sz srcOff dstOff
-                        SymbolicMemory mem -> do
-                          assign (#state % #memory) (SymbolicMemory $ copySlice srcOff dstOff sz mem mem)
-                      assign (#state % #stack) xs
-                _ -> internalError "symbolic size in MCOPY"
+                      mcopy sz srcOff dstOff
+                _ -> do
+                  -- symbolic, ignore gas
+                  next
+                  mcopy sz srcOff dstOff
+              assign (#state % #stack) xs
             _ -> underrun
+            where
+            mcopy sz srcOff dstOff = do
+                  m <- gets (.state.memory)
+                  case m of
+                    ConcreteMemory mem -> do
+                      buf <- freezeMemory mem
+                      copyBytesToMemory buf sz srcOff dstOff
+                    SymbolicMemory mem -> do
+                      assign (#state % #memory) (SymbolicMemory $ copySlice srcOff dstOff sz mem mem)
 
         OpMstore ->
           case stk of
diff --git a/src/EVM/Fetch.hs b/src/EVM/Fetch.hs
index 8b546c686..81c2ab2be 100644
--- a/src/EVM/Fetch.hs
+++ b/src/EVM/Fetch.hs
@@ -19,7 +19,6 @@ import Data.Text (Text, unpack, pack)
 import Data.Map.Strict qualified as Map
 import Data.Maybe (fromMaybe)
 import Data.List (foldl')
-import Data.Text qualified as T
 import Data.Vector qualified as RegularVector
 import Network.Wreq
 import Network.Wreq.Session (Session)
@@ -200,7 +199,7 @@ oracle solvers info q = do
   case q of
     PleaseDoFFI vals envs continue -> case vals of
        cmd : args -> do
-          existingEnv <- liftIO $ getEnvironment
+          existingEnv <- liftIO getEnvironment
           let mergedEnv = Map.toList $ Map.union envs $ Map.fromList existingEnv
           let process = (proc cmd args :: CreateProcess) { env = Just mergedEnv }
           (_, stdout', _) <- liftIO $ readCreateProcessWithExitCode process ""
@@ -259,9 +258,7 @@ checkBranch solvers branchcondition pathconditions = do
         Unsat -> pure $ Case True
         -- Yes. Both branches possible
         Sat _ -> pure EVM.Types.Unknown
-        -- Explore both branches in case of timeout
-        EVM.Solvers.Unknown -> pure EVM.Types.Unknown
-        Error e -> internalError $ "SMT Solver pureed with an error: " <> T.unpack e
-    -- If the query times out, we simply explore both paths
-    EVM.Solvers.Unknown -> pure EVM.Types.Unknown
-    Error e -> internalError $ "SMT Solver pureed with an error: " <> T.unpack e
+    -- If the query times out, or can't be executed (e.g. symbolic copyslice) we simply explore both paths
+        _ -> pure EVM.Types.Unknown
+    -- If the query times out, or can't be executed (e.g. symbolic copyslice) we simply explore both paths
+    _ -> pure EVM.Types.Unknown
diff --git a/src/EVM/SMT.hs b/src/EVM/SMT.hs
index bf93b8161..41cad6d72 100644
--- a/src/EVM/SMT.hs
+++ b/src/EVM/SMT.hs
@@ -17,6 +17,7 @@ import Data.List.NonEmpty (NonEmpty((:|)))
 import Data.List.NonEmpty qualified as NonEmpty
 import Data.String.Here
 import Data.Maybe (fromJust, fromMaybe, isJust)
+import Data.Either.Extra (fromRight')
 import Data.Map.Strict (Map)
 import Data.Map.Strict qualified as Map
 import Data.Set (Set)
@@ -167,22 +168,26 @@ formatSMT2 (SMT2 ls _ _ ps) = expr <> smt2
  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
-declareIntermediates bufs stores =
+declareIntermediates :: BufEnv -> StoreEnv -> Err SMT2
+declareIntermediates bufs stores = do
   let encSs = Map.mapWithKey encodeStore 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 mempty):decls
-  in  foldr (<>) (SMT2[""] mempty mempty mempty) smt2
+  decls <- mapM snd sorted
+  let smt2 = (SMT2 [fromText "; intermediate buffers & stores"] mempty mempty mempty):decls
+  pure $ foldr (<>) mempty smt2
   where
     compareFst (l, _) (r, _) = compare l r
-    encodeBuf n expr =
-      SMT2 ["(define-fun buf" <> (fromString . show $ n) <> "() Buf " <> exprToSMT expr <> ")\n"]  mempty mempty mempty <> encodeBufLen n expr
-    encodeBufLen n expr =
-      SMT2 ["(define-fun buf" <> (fromString . show $ n) <>"_length () (_ BitVec 256) " <> exprToSMT (bufLengthEnv bufs True expr) <> ")"] mempty mempty mempty
-    encodeStore n expr =
-      SMT2 ["(define-fun store" <> (fromString . show $ n) <> " () Storage " <> exprToSMT expr <> ")"] mempty mempty mempty
+    encodeBuf n expr = do
+      buf <- exprToSMT expr
+      bufLen <- encodeBufLen n expr
+      pure $ SMT2 ["(define-fun buf" <> (fromString . show $ n) <> "() Buf " <> buf <> ")\n"]  mempty mempty mempty <> bufLen
+    encodeBufLen n expr = do
+      bufLen <- exprToSMT (bufLengthEnv bufs True expr)
+      pure $ SMT2 ["(define-fun buf" <> (fromString . show $ n) <>"_length () (_ BitVec 256) " <> bufLen <> ")"] mempty mempty mempty
+    encodeStore n expr = do
+      storage <- exprToSMT expr
+      pure $ SMT2 ["(define-fun store" <> (fromString . show $ n) <> " () Storage " <> storage <> ")"] mempty mempty mempty
 
 data AbstState = AbstState
   { words :: Map (Expr EWord) Int
@@ -221,7 +226,7 @@ abstractAwayProps conf ps = runState (mapM abstrAway ps) (AbstState mempty 0)
 smt2Line :: Builder -> SMT2
 smt2Line txt = SMT2 [txt] mempty mempty mempty
 
-assertProps :: Config -> [Prop] -> SMT2
+assertProps :: Config -> [Prop] -> Err SMT2
 -- simplify to rewrite sload/sstore combos
 -- notice: it is VERY important not to concretize, because Keccak assumptions
 --         will be generated by assertPropsNoSimp, and that needs unconcretized Props
@@ -239,12 +244,16 @@ assertProps conf ps = assertPropsNoSimp conf (decompose . Expr.simplifyProps $ p
 -- Note: we need a version that does NOT call simplify,
 -- because we make use of it to verify the correctness of our simplification
 -- passes through property-based testing.
-assertPropsNoSimp :: Config -> [Prop] -> SMT2
-assertPropsNoSimp config psPreConc =
-  let encs = map propToSMT psElimAbst
-      abstSMT = map propToSMT abstProps
-      intermediates = declareIntermediates bufs stores in
-  prelude
+assertPropsNoSimp :: Config -> [Prop] -> Err SMT2
+assertPropsNoSimp config psPreConc = do
+ encs <- mapM propToSMT psElimAbst
+ abstSMT <- mapM propToSMT abstProps
+ intermediates <- declareIntermediates bufs stores
+ readAssumes' <- readAssumes
+ keccakAssertions' <- keccakAssertions
+ frameCtxs <- (declareFrameContext . nubOrd $ foldl (<>) [] frameCtx)
+ blockCtxs <- (declareBlockContext . nubOrd $ foldl (<>) [] blockCtx)
+ pure $ prelude
   <> (declareAbstractStores abstractStores)
   <> smt2Line ""
   <> (declareAddrs addresses)
@@ -253,14 +262,14 @@ assertPropsNoSimp config psPreConc =
   <> smt2Line ""
   <> (declareVars . nubOrd $ foldl (<>) [] allVars)
   <> smt2Line ""
-  <> (declareFrameContext . nubOrd $ foldl (<>) [] frameCtx)
+  <> frameCtxs
   <> smt2Line ""
-  <> (declareBlockContext . nubOrd $ foldl (<>) [] blockCtx)
+  <> blockCtxs
   <> smt2Line ""
   <> intermediates
   <> smt2Line ""
-  <> keccakAssertions
-  <> readAssumes
+  <> keccakAssertions'
+  <> readAssumes'
   <> smt2Line ""
   <> SMT2 (fmap (\p -> "(assert " <> p <> ")") encs) mempty mempty mempty
   <> SMT2 mempty (RefinementEqs (fmap (\p -> "(assert " <> p <> ")") abstSMT) (psElimAbst <> abstProps)) mempty mempty
@@ -302,16 +311,18 @@ assertPropsNoSimp config psPreConc =
     --      This will make sure concrete values of Keccak are asserted, if they can be computed (i.e. can be concretized)
     keccAssump = keccakAssumptions psPreConc bufVals storeVals
     keccComp = keccakCompute psPreConc bufVals storeVals
-    keccakAssertions
-      = smt2Line "; keccak assumptions"
-      <> SMT2 (fmap (\p -> "(assert " <> propToSMT p <> ")") keccAssump) mempty mempty mempty
-      <> smt2Line "; keccak computations"
-      <> SMT2 (fmap (\p -> "(assert " <> propToSMT p <> ")") keccComp) mempty mempty mempty
+    keccakAssertions = do
+      assumps <- mapM assertSMT keccAssump
+      comps <- mapM assertSMT keccComp
+      pure $ smt2Line "; keccak assumptions"
+        <> SMT2 assumps mempty mempty mempty
+        <> smt2Line "; keccak computations"
+        <> SMT2 comps mempty mempty mempty
 
     -- assert that reads beyond size of buffer & storage is zero
-    readAssumes
-      = smt2Line "; read assumptions"
-        <> SMT2 (fmap (\p -> "(assert " <> propToSMT p <> ")") (assertReads psElim bufs stores)) mempty mempty mempty
+    readAssumes = do
+      assumps <- mapM assertSMT $ assertReads psElim bufs stores
+      pure $ smt2Line "; read assumptions" <> SMT2 assumps mempty mempty mempty
 
 referencedAbstractStores :: TraversableTerm a => a -> Set Builder
 referencedAbstractStores term = foldTerm go mempty term
@@ -467,11 +478,14 @@ declareAddrs names = SMT2 (["; symbolic addresseses"] <> fmap declare names) mem
     declare n = "(declare-fun " <> n <> " () Addr)"
     cexvars = (mempty :: CexVars){ addrs = fmap toLazyText names }
 
-declareFrameContext :: [(Builder, [Prop])] -> SMT2
-declareFrameContext names = SMT2 (["; frame context"] <> concatMap declare names) mempty cexvars mempty
+declareFrameContext :: [(Builder, [Prop])] -> Err SMT2
+declareFrameContext names = do
+  decls <- concatMapM declare names
+  pure $ SMT2 (["; frame context"] <> decls) mempty cexvars mempty
   where
-    declare (n,props) = [ "(declare-fun " <> n <> " () (_ BitVec 256))" ]
-                        <> fmap (\p -> "(assert " <> propToSMT p <> ")") props
+    declare (n,props) = do
+      asserts <- mapM assertSMT props
+      pure $ [ "(declare-fun " <> n <> " () (_ BitVec 256))" ] <> asserts
     cexvars = (mempty :: CexVars){ txContext = fmap (toLazyText . fst) names }
 
 declareAbstractStores :: [Builder] -> SMT2
@@ -479,13 +493,21 @@ declareAbstractStores names = SMT2 (["; abstract base stores"] <> fmap declare n
   where
     declare n = "(declare-fun " <> n <> " () Storage)"
 
-declareBlockContext :: [(Builder, [Prop])] -> SMT2
-declareBlockContext names = SMT2 (["; block context"] <> concatMap declare names) mempty cexvars mempty
+declareBlockContext :: [(Builder, [Prop])] -> Err SMT2
+declareBlockContext names = do
+  decls <- concatMapM declare names
+  pure $ SMT2 (["; block context"] <> decls) mempty cexvars mempty
   where
-    declare (n, props) = [ "(declare-fun " <> n <> " () (_ BitVec 256))" ]
-                         <> fmap (\p -> "(assert " <> propToSMT p <> ")") props
+    declare (n, props) = do
+      asserts <- mapM assertSMT props
+      pure $ [ "(declare-fun " <> n <> " () (_ BitVec 256))" ] <> asserts
     cexvars = (mempty :: CexVars){ blockContext = fmap (toLazyText . fst) names }
 
+assertSMT :: Prop -> Either String Builder
+assertSMT p = do
+  p' <- propToSMT p
+  pure $ "(assert " <> p' <> ")"
+
 prelude :: SMT2
 prelude =  SMT2 src mempty mempty mempty
   where
@@ -703,12 +725,12 @@ prelude =  SMT2 src mempty mempty mempty
     (ite (= b (_ bv30 256)) ((_ sign_extend 8  ) ((_ extract 247  0) val)) val))))))))))))))))))))))))))))))))
   |]
 
-exprToSMT :: Expr a -> Builder
+exprToSMT :: Expr a -> Err Builder
 exprToSMT = \case
-  Lit w -> fromLazyText $ "(_ bv" <> (T.pack $ show (into w :: Integer)) <> " 256)"
-  Var s -> fromText s
-  GVar (BufVar n) -> fromString $ "buf" <> (show n)
-  GVar (StoreVar n) -> fromString $ "store" <> (show n)
+  Lit w -> pure $ fromLazyText $ "(_ bv" <> (T.pack $ show (into w :: Integer)) <> " 256)"
+  Var s -> pure $ fromText s
+  GVar (BufVar n) -> pure $ fromString $ "buf" <> (show n)
+  GVar (StoreVar n) -> pure $ fromString $ "store" <> (show n)
   JoinBytes
     z o two three four five six seven
     eight nine ten eleven twelve thirteen fourteen fifteen
@@ -725,39 +747,39 @@ exprToSMT = \case
   Mul a b -> op2 "bvmul" a b
   Exp a b -> case b of
                Lit b' -> expandExp a b'
-               _ -> internalError "cannot encode symbolic exponentiation into SMT"
-  Min a b ->
-    let aenc = exprToSMT a
-        benc = exprToSMT b in
-    "(ite (bvule " <> aenc `sp` benc <> ") " <> aenc `sp` benc <> ")"
-  Max a b ->
-    let aenc = exprToSMT a
-        benc = exprToSMT b in
-    "(max " <> aenc `sp` benc <> ")"
-  LT a b ->
-    let cond = op2 "bvult" a b in
-    "(ite " <> cond `sp` one `sp` zero <> ")"
-  SLT a b ->
-    let cond = op2 "bvslt" a b in
-    "(ite " <> cond `sp` one `sp` zero <> ")"
-  SGT a b ->
-    let cond = op2 "bvsgt" a b in
-    "(ite " <> cond `sp` one `sp` zero <> ")"
-  GT a b ->
-    let cond = op2 "bvugt" a b in
-    "(ite " <> cond `sp` one `sp` zero <> ")"
-  LEq a b ->
-    let cond = op2 "bvule" a b in
-    "(ite " <> cond `sp` one `sp` zero <> ")"
-  GEq a b ->
-    let cond = op2 "bvuge" a b in
-    "(ite " <> cond `sp` one `sp` zero <> ")"
-  Eq a b ->
-    let cond = op2 "=" a b in
-    "(ite " <> cond `sp` one `sp` zero <> ")"
-  IsZero a ->
-    let cond = op2 "=" a (Lit 0) in
-    "(ite " <> cond `sp` one `sp` zero <> ")"
+               _ -> Left "cannot encode symbolic exponentiation into SMT"
+  Min a b -> do
+    aenc <- exprToSMT a
+    benc <- exprToSMT b
+    pure $ "(ite (bvule " <> aenc `sp` benc <> ") " <> aenc `sp` benc <> ")"
+  Max a b -> do
+    aenc <- exprToSMT a
+    benc <- exprToSMT b
+    pure $ "(max " <> aenc `sp` benc <> ")"
+  LT a b -> do
+    cond <- op2 "bvult" a b
+    pure $ "(ite " <> cond `sp` one `sp` zero <> ")"
+  SLT a b -> do
+    cond <- op2 "bvslt" a b
+    pure $ "(ite " <> cond `sp` one `sp` zero <> ")"
+  SGT a b -> do
+    cond <- op2 "bvsgt" a b
+    pure $ "(ite " <> cond `sp` one `sp` zero <> ")"
+  GT a b -> do
+    cond <- op2 "bvugt" a b
+    pure $ "(ite " <> cond `sp` one `sp` zero <> ")"
+  LEq a b -> do
+    cond <- op2 "bvule" a b
+    pure $ "(ite " <> cond `sp` one `sp` zero <> ")"
+  GEq a b -> do
+    cond <- op2 "bvuge" a b
+    pure $ "(ite " <> cond `sp` one `sp` zero <> ")"
+  Eq a b -> do
+    cond <- op2 "=" a b
+    pure $ "(ite " <> cond `sp` one `sp` zero <> ")"
+  IsZero a -> do
+    cond <- op2 "=" a (Lit 0)
+    pure $ "(ite " <> cond `sp` one `sp` zero <> ")"
   And a b -> op2 "bvand" a b
   Or a b -> op2 "bvor" a b
   Xor a b -> op2 "bvxor" a b
@@ -771,108 +793,112 @@ exprToSMT = \case
   Mod a b -> op2CheckZero "bvurem" a b
   SMod a b -> op2CheckZero "bvsrem" a b
   -- NOTE: this needs to do the MUL at a higher precision, then MOD, then downcast
-  MulMod a b c ->
-    let aExp = exprToSMT a
-        bExp = exprToSMT b
-        cExp = exprToSMT c
-        aLift = "(concat (_ bv0 256) " <> aExp <> ")"
+  MulMod a b c -> do
+    aExp <- exprToSMT a
+    bExp <- exprToSMT b
+    cExp <- exprToSMT c
+    let aLift = "(concat (_ bv0 256) " <> aExp <> ")"
         bLift = "(concat (_ bv0 256) " <> bExp <> ")"
         cLift = "(concat (_ bv0 256) " <> cExp <> ")"
-    in  "((_ extract 255 0) (ite (= " <> cExp <> " (_ bv0 256)) (_ bv0 512) (bvurem (bvmul " <> aLift `sp` bLift <> ")" <> cLift <> ")))"
-  AddMod a b c ->
-    let aExp = exprToSMT a
-        bExp = exprToSMT b
-        cExp = exprToSMT c
-        aLift = "(concat (_ bv0 256) " <> aExp <> ")"
+    pure $ "((_ extract 255 0) (ite (= " <> cExp <> " (_ bv0 256)) (_ bv0 512) (bvurem (bvmul " <> aLift `sp` bLift <> ")" <> cLift <> ")))"
+  AddMod a b c -> do
+    aExp <- exprToSMT a
+    bExp <- exprToSMT b
+    cExp <- exprToSMT c
+    let aLift = "(concat (_ bv0 256) " <> aExp <> ")"
         bLift = "(concat (_ bv0 256) " <> bExp <> ")"
         cLift = "(concat (_ bv0 256) " <> cExp <> ")"
-    in  "((_ extract 255 0) (ite (= " <> cExp <> " (_ bv0 256)) (_ bv0 512) (bvurem (bvadd " <> aLift `sp` bLift <> ")" <> cLift <> ")))"
-  EqByte a b ->
-    let cond = op2 "=" a b in
-    "(ite " <> cond `sp` one `sp` zero <> ")"
-  Keccak a -> let
-      enc = exprToSMT a
-      sz = exprToSMT $ Expr.bufLength a
-    in "(keccak " <> enc <> " " <> sz <> ")"
-  SHA256 a -> let
-      enc = exprToSMT a
-      sz = exprToSMT $ Expr.bufLength a
-    in "(sha256 " <> enc <> " " <> sz <> ")"
-
-  TxValue -> fromString "txvalue"
-  Balance a -> fromString "balance_" <> formatEAddr a
-
-  Origin ->  "origin"
-  BlockHash a ->
-    let enc = exprToSMT a in
-    "(blockhash " <> enc <> ")"
-  CodeSize a ->
-    let enc = exprToSMT a in
-    "(codesize " <> enc <> ")"
-  Coinbase -> "coinbase"
-  Timestamp -> "timestamp"
-  BlockNumber -> "blocknumber"
-  PrevRandao -> "prevrandao"
-  GasLimit -> "gaslimit"
-  ChainId -> "chainid"
-  BaseFee -> "basefee"
-
-  a@(SymAddr _) -> formatEAddr a
-  WAddr(a@(SymAddr _)) -> "((_ zero_extend 96)" `sp` exprToSMT a `sp` ")"
-
-  LitByte b -> fromLazyText $ "(_ bv" <> T.pack (show (into b :: Integer)) <> " 8)"
+    pure $ "((_ extract 255 0) (ite (= " <> cExp <> " (_ bv0 256)) (_ bv0 512) (bvurem (bvadd " <> aLift `sp` bLift <> ")" <> cLift <> ")))"
+  EqByte a b -> do
+    cond <- op2 "=" a b
+    pure $ "(ite " <> cond `sp` one `sp` zero <> ")"
+  Keccak a -> do
+    enc <- exprToSMT a
+    sz  <- exprToSMT $ Expr.bufLength a
+    pure $ "(keccak " <> enc <> " " <> sz <> ")"
+  SHA256 a -> do
+    enc <- exprToSMT a
+    sz  <- exprToSMT $ Expr.bufLength a
+    pure $ "(sha256 " <> enc <> " " <> sz <> ")"
+
+  TxValue -> pure $ fromString "txvalue"
+  Balance a -> pure $ fromString "balance_" <> formatEAddr a
+
+  Origin ->  pure "origin"
+  BlockHash a -> do
+    enc <- exprToSMT a
+    pure $ "(blockhash " <> enc <> ")"
+  CodeSize a -> do
+    enc <- exprToSMT a
+    pure $ "(codesize " <> enc <> ")"
+  Coinbase -> pure "coinbase"
+  Timestamp -> pure "timestamp"
+  BlockNumber -> pure "blocknumber"
+  PrevRandao -> pure "prevrandao"
+  GasLimit -> pure "gaslimit"
+  ChainId -> pure "chainid"
+  BaseFee -> pure "basefee"
+
+  a@(SymAddr _) -> pure $ formatEAddr a
+  WAddr(a@(SymAddr _)) -> do
+    wa <- exprToSMT a
+    pure $ "((_ zero_extend 96)" `sp` wa `sp` ")"
+
+  LitByte b -> pure $ fromLazyText $ "(_ bv" <> T.pack (show (into b :: Integer)) <> " 8)"
   IndexWord idx w -> case idx of
     Lit n -> if n >= 0 && n < 32
-             then
-               let enc = exprToSMT w in
-               fromLazyText ("(indexWord" <> T.pack (show (into n :: Integer))) `sp` enc <> ")"
+             then do
+               enc <- exprToSMT w
+               pure $ fromLazyText ("(indexWord" <> T.pack (show (into n :: Integer))) `sp` enc <> ")"
              else exprToSMT (LitByte 0)
     _ -> op2 "indexWord" idx w
   ReadByte idx src -> op2 "select" src idx
 
-  ConcreteBuf "" -> "((as const Buf) #b00000000)"
+  ConcreteBuf "" -> pure "((as const Buf) #b00000000)"
   ConcreteBuf bs -> writeBytes bs mempty
-  AbstractBuf s -> fromText s
+  AbstractBuf s -> pure $ fromText s
   ReadWord idx prev -> op2 "readWord" idx prev
-  BufLength (AbstractBuf b) -> fromText b <> "_length"
-  BufLength (GVar (BufVar n)) -> fromLazyText $ "buf" <> (T.pack . show $ n) <> "_length"
+  BufLength (AbstractBuf b) -> pure $ fromText b <> "_length"
+  BufLength (GVar (BufVar n)) -> pure $ fromLazyText $ "buf" <> (T.pack . show $ n) <> "_length"
   BufLength b -> exprToSMT (bufLength b)
-  WriteByte idx val prev ->
-    let encIdx = exprToSMT idx
-        encVal = exprToSMT val
-        encPrev = exprToSMT prev in
-    "(store " <> encPrev `sp` encIdx `sp` encVal <> ")"
-  WriteWord idx val prev ->
-    let encIdx = exprToSMT idx
-        encVal = exprToSMT val
-        encPrev = exprToSMT prev in
-    "(writeWord " <> encIdx `sp` encVal `sp` encPrev <> ")"
-  CopySlice srcIdx dstIdx size src dst ->
-    copySlice srcIdx dstIdx size (exprToSMT src) (exprToSMT dst)
+  WriteByte idx val prev -> do
+    encIdx  <- exprToSMT idx
+    encVal  <- exprToSMT val
+    encPrev <- exprToSMT prev
+    pure $ "(store " <> encPrev `sp` encIdx `sp` encVal <> ")"
+  WriteWord idx val prev -> do
+    encIdx  <- exprToSMT idx
+    encVal  <- exprToSMT val
+    encPrev <- exprToSMT prev
+    pure $ "(writeWord " <> encIdx `sp` encVal `sp` encPrev <> ")"
+  CopySlice srcIdx dstIdx size src dst -> do
+    srcSMT <- exprToSMT src
+    dstSMT <- exprToSMT dst
+    copySlice srcIdx dstIdx size srcSMT dstSMT
 
   -- we need to do a bit of processing here.
   ConcreteStore s -> encodeConcreteStore s
-  AbstractStore a idx -> storeName a idx
-  SStore idx val prev ->
-    let encIdx = exprToSMT idx
-        encVal = exprToSMT val
-        encPrev = exprToSMT prev in
-    "(store" `sp` encPrev `sp` encIdx `sp` encVal <> ")"
+  AbstractStore a idx -> pure $ storeName a idx
+  SStore idx val prev -> do
+    encIdx  <- exprToSMT idx
+    encVal  <- exprToSMT val
+    encPrev <- exprToSMT prev
+    pure $ "(store" `sp` encPrev `sp` encIdx `sp` encVal <> ")"
   SLoad idx store -> op2 "select" store idx
 
   a -> internalError $ "TODO: implement: " <> show a
   where
-    op1 op a =
-      let enc =  exprToSMT a in
-      "(" <> op `sp` enc <> ")"
-    op2 op a b =
-      let aenc = exprToSMT a
-          benc = exprToSMT b in
-      "(" <> op `sp` aenc `sp` benc <> ")"
-    op2CheckZero op a b =
-      let aenc = exprToSMT a
-          benc = exprToSMT b in
-      "(ite (= " <> benc <> " (_ bv0 256)) (_ bv0 256) " <>  "(" <> op `sp` aenc `sp` benc <> "))"
+    op1 op a = do
+      enc <- exprToSMT a
+      pure $ "(" <> op `sp` enc <> ")"
+    op2 op a b = do
+       aenc <- exprToSMT a
+       benc <- exprToSMT b
+       pure $ "(" <> op `sp` aenc `sp` benc <> ")"
+    op2CheckZero op a b = do
+      aenc <- exprToSMT a
+      benc <- exprToSMT b
+      pure $ "(ite (= " <> benc <> " (_ bv0 256)) (_ bv0 256) " <>  "(" <> op `sp` aenc `sp` benc <> "))"
 
 sp :: Builder -> Builder -> Builder
 a `sp` b = a <> (fromText " ") <> b
@@ -883,34 +909,34 @@ zero = "(_ bv0 256)"
 one :: Builder
 one = "(_ bv1 256)"
 
-propToSMT :: Prop -> Builder
+propToSMT :: Prop -> Err Builder
 propToSMT = \case
   PEq a b -> op2 "=" a b
   PLT a b -> op2 "bvult" a b
   PGT a b -> op2 "bvugt" a b
   PLEq a b -> op2 "bvule" a b
   PGEq a b -> op2 "bvuge" a b
-  PNeg a ->
-    let enc = propToSMT a in
-    "(not " <> enc <> ")"
-  PAnd a b ->
-    let aenc = propToSMT a
-        benc = propToSMT b in
-    "(and " <> aenc <> " " <> benc <> ")"
-  POr a b ->
-    let aenc = propToSMT a
-        benc = propToSMT b in
-    "(or " <> aenc <> " " <> benc <> ")"
-  PImpl a b ->
-    let aenc = propToSMT a
-        benc = propToSMT b in
-    "(=> " <> aenc <> " " <> benc <> ")"
-  PBool b -> if b then "true" else "false"
+  PNeg a -> do
+    enc <- propToSMT a
+    pure $ "(not " <> enc <> ")"
+  PAnd a b -> do
+    aenc <- propToSMT a
+    benc <- propToSMT b
+    pure $ "(and " <> aenc <> " " <> benc <> ")"
+  POr a b -> do
+    aenc <- propToSMT a
+    benc <- propToSMT b
+    pure $ "(or " <> aenc <> " " <> benc <> ")"
+  PImpl a b -> do
+    aenc <- propToSMT a
+    benc <- propToSMT b
+    pure $ "(=> " <> aenc <> " " <> benc <> ")"
+  PBool b -> pure $ if b then "true" else "false"
   where
-    op2 op a b =
-      let aenc = exprToSMT a
-          benc = exprToSMT b in
-      "(" <> op <> " " <> aenc <> " " <> benc <> ")"
+    op2 op a b = do
+      aenc <- exprToSMT a
+      benc <- exprToSMT b
+      pure $ "(" <> op <> " " <> aenc <> " " <> benc <> ")"
 
 
 
@@ -918,61 +944,67 @@ propToSMT = \case
 
 
 -- | Stores a region of src into dst
-copySlice :: Expr EWord -> Expr EWord -> Expr EWord -> Builder -> Builder -> Builder
-copySlice srcOffset dstOffset size0@(Lit _) src dst =
-  "(let ((src " <> src <> ")) " <> internal size0 <> ")"
+copySlice :: Expr EWord -> Expr EWord -> Expr EWord -> Builder -> Builder -> Err Builder
+copySlice srcOffset dstOffset size0@(Lit _) src dst = do
+  sz <- internal size0
+  pure $ "(let ((src " <> src <> ")) " <> sz <> ")"
   where
-    internal (Lit 0) = dst
-    internal size =
+    internal (Lit 0) = pure dst
+    internal size = do
       let size' = (Expr.sub size (Lit 1))
-          encDstOff = exprToSMT (Expr.add dstOffset size')
-          encSrcOff = exprToSMT (Expr.add srcOffset size')
-          child = internal size' in
-      "(store " <> child `sp` encDstOff `sp` "(select src " <> encSrcOff <> "))"
-copySlice _ _ _ _ _ = internalError "TODO: implement copySlice with a symbolically sized region"
+      encDstOff <- exprToSMT (Expr.add dstOffset size')
+      encSrcOff <- exprToSMT (Expr.add srcOffset size')
+      child <- internal size'
+      pure $ "(store " <> child `sp` encDstOff `sp` "(select src " <> encSrcOff <> "))"
+copySlice _ _ _ _ _ = Left "CopySlice with a symbolically sized region not currently implemented, cannot execute SMT solver on this query"
 
 -- | Unrolls an exponentiation into a series of multiplications
-expandExp :: Expr EWord -> W256 -> Builder
+expandExp :: Expr EWord -> W256 -> Err Builder
 expandExp base expnt
   | expnt == 1 = exprToSMT base
-  | otherwise =
-    let b = exprToSMT base
-        n = expandExp base (expnt - 1) in
-    "(bvmul " <> b `sp` n <> ")"
+  | otherwise = do
+    b <- exprToSMT base
+    n <- expandExp base (expnt - 1)
+    pure $ "(bvmul " <> b `sp` n <> ")"
 
 -- | Concatenates a list of bytes into a larger bitvector
-concatBytes :: [Expr Byte] -> Builder
-concatBytes bytes =
+concatBytes :: [Expr Byte] -> Err Builder
+concatBytes bytes = do
   let bytesRev = reverse bytes
-      a2 = exprToSMT (head bytesRev) in
-  foldl wrap a2 $ tail bytesRev
+  a2 <- exprToSMT (head bytesRev)
+  foldM wrap a2 $ tail bytesRev
   where
-    wrap inner byte =
-      let byteSMT = exprToSMT byte in
-      "(concat " <> byteSMT `sp` inner <> ")"
+    wrap :: Builder -> Expr a -> Err Builder
+    wrap inner byte = do
+      byteSMT <- exprToSMT byte
+      pure $ "(concat " <> byteSMT `sp` inner <> ")"
 
 -- | Concatenates a list of bytes into a larger bitvector
-writeBytes :: ByteString -> Expr Buf -> Builder
-writeBytes bytes buf = snd $ BS.foldl' wrap (0, exprToSMT buf) bytes
+writeBytes :: ByteString -> Expr Buf -> Err Builder
+writeBytes bytes buf =  do
+  buf' <- exprToSMT buf
+  ret <- foldM wrap (0, buf') $ BS.unpack bytes
+  pure $ snd ret
   where
     -- we don't need to store zeros if the base buffer is empty
     skipZeros = buf == mempty
-    wrap :: (Int, Builder) -> Word8 -> (Int, Builder)
+    wrap :: (Int, Builder) -> Word8 -> Err (Int, Builder)
     wrap (idx, inner) byte =
       if skipZeros && byte == 0
-      then (idx + 1, inner)
-      else let
-          byteSMT = exprToSMT (LitByte byte)
-          idxSMT = exprToSMT . Lit . unsafeInto $ idx
-        in (idx + 1, "(store " <> inner `sp` idxSMT `sp` byteSMT <> ")")
-
-encodeConcreteStore :: Map W256 W256 -> Builder
-encodeConcreteStore s = foldl encodeWrite "((as const Storage) #x0000000000000000000000000000000000000000000000000000000000000000)" (Map.toList s)
+      then pure (idx + 1, inner)
+      else do
+          byteSMT <- exprToSMT (LitByte byte)
+          idxSMT <- exprToSMT . Lit . unsafeInto $ idx
+          pure (idx + 1, "(store " <> inner `sp` idxSMT `sp` byteSMT <> ")")
+
+encodeConcreteStore :: Map W256 W256 -> Err Builder
+encodeConcreteStore s = foldM encodeWrite ("((as const Storage) #x0000000000000000000000000000000000000000000000000000000000000000)") (Map.toList s)
   where
-    encodeWrite prev (key, val) = let
-        encKey = exprToSMT (Lit key)
-        encVal = exprToSMT (Lit val)
-      in "(store " <> prev `sp` encKey `sp` encVal <> ")"
+    encodeWrite :: Builder -> (W256, W256) -> Err Builder
+    encodeWrite prev (key, val) = do
+      encKey <- exprToSMT $ Lit key
+      encVal <- exprToSMT $ Lit val
+      pure $ "(store " <> prev `sp` encKey `sp` encVal <> ")"
 
 storeName :: Expr EAddr -> Maybe W256 -> Builder
 storeName a Nothing = fromString ("baseStore_") <> formatEAddr a
@@ -1163,7 +1195,8 @@ getStore getVal abstractReads =
 queryValue :: (Text -> IO Text) -> Expr EWord -> IO W256
 queryValue _ (Lit w) = pure w
 queryValue getVal w = do
-  let expr = toLazyText $ exprToSMT w
+  -- this exprToSMT should never fail, since we have already ran the solver
+  let expr = toLazyText $ fromRight' $ exprToSMT w
   raw <- getVal expr
   case parseCommentFreeFileMsg getValueRes (T.toStrict raw) of
     Right (ResSpecific (valParsed :| [])) ->
diff --git a/src/EVM/Solvers.hs b/src/EVM/Solvers.hs
index 17d48bea2..3a8a90e06 100644
--- a/src/EVM/Solvers.hs
+++ b/src/EVM/Solvers.hs
@@ -17,7 +17,7 @@ import Data.Char (isSpace)
 import Data.Map (Map)
 import Data.Map qualified as Map
 import Data.Maybe (fromMaybe, isJust, fromJust)
-import Data.Text qualified as TS
+import Data.Either (isLeft)
 import Data.Text.Lazy (Text)
 import Data.Text.Lazy qualified as T
 import Data.Text.Lazy.IO qualified as T
@@ -28,7 +28,7 @@ import EVM.Effects
 import EVM.Fuzz (tryCexFuzz)
 
 import EVM.SMT
-import EVM.Types (W256, Expr(AbstractBuf), internalError)
+import EVM.Types (W256, Expr(AbstractBuf), internalError, Err, getError, getNonError)
 
 -- | Supported solvers
 data Solver
@@ -65,30 +65,28 @@ data Task = Task
 data CheckSatResult
   = Sat SMTCex
   | Unsat
-  | Unknown
-  | Error TS.Text
+  | Unknown String
+  | Error String
   deriving (Show, Eq)
 
 isSat :: CheckSatResult -> Bool
 isSat (Sat _) = True
 isSat _ = False
 
-isErr :: CheckSatResult -> Bool
-isErr (Error _) = True
-isErr _ = False
-
 isUnsat :: CheckSatResult -> Bool
 isUnsat Unsat = True
 isUnsat _ = False
 
-checkSat :: SolverGroup -> SMT2 -> IO CheckSatResult
+checkSat :: SolverGroup -> Err SMT2 -> IO CheckSatResult
 checkSat (SolverGroup taskQueue) script = do
-  -- prepare result channel
-  resChan <- newChan
-  -- send task to solver group
-  writeChan taskQueue (Task script resChan)
-  -- collect result
-  readChan resChan
+  if isLeft script then pure $ Error $ getError script
+  else do
+    -- prepare result channel
+    resChan <- newChan
+    -- send task to solver group
+    writeChan taskQueue (Task (getNonError script) resChan)
+    -- collect result
+    readChan resChan
 
 writeSMT2File :: SMT2 -> Int -> String -> IO ()
 writeSMT2File smt2 count abst =
@@ -139,15 +137,15 @@ withSolvers solver count threads timeout cont = do
             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))
+              Left e -> writeChan r (Error $ "Error while writing SMT to solver: " <> T.unpack 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
+                      "timeout" -> pure $ Unknown "Result timeout by SMT solver"
+                      "unknown" -> pure $ Unknown "Result unknown by SMT solver"
                       "sat" -> if null refineEqs then Sat <$> getModel inst cexvars
                                else do
                                     let refinedSMT2 = SMT2 refineEqs mempty mempty (ps <> refps)
@@ -156,15 +154,15 @@ withSolvers solver count threads timeout cont = do
                                     sat2 <- sendLine inst "(check-sat)"
                                     case sat2 of
                                       "unsat" -> pure Unsat
-                                      "timeout" -> pure Unknown
-                                      "unknown" -> pure Unknown
+                                      "timeout" -> pure $ Unknown "Result timeout by SMT solver"
+                                      "unknown" -> pure $ Unknown "Result unknown by SMT solver"
                                       "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
+                                      _ -> pure . Error $ "Unable to parse solver output: " <> T.unpack sat2
+                      _ -> pure . Error $ "Unable to parse SMT solver output: " <> T.unpack sat
                 writeChan r res
           else do
             when (conf.debug) $ putStrLn "Fuzzing failed to find a Cex, not trying SMT due to onlyCexFuzz"
-            writeChan r Unknown
+            writeChan r $ Error "Option onlyCexFuzz enabled, not running SMT"
 
         -- put the instance back in the list of available instances
         writeChan availableInstances inst
@@ -401,8 +399,8 @@ getSExpr :: Text -> (Text, Text)
 getSExpr l = go LPar l 0 []
   where
     go _ text 0 prev@(_:_) = (T.intercalate "" (reverse prev), text)
-    go _ _ r _ | r < 0 = internalError "Unbalanced SExpression"
-    go _ "" _ _  = internalError "Unbalanced SExpression"
+    go _ _ r _ | r < 0 = internalError $ "Unbalanced SExpression: " <> show l
+    go _ "" _ _  = internalError $ "Unbalanced SExpression: " <> show l
     -- find the next left parenthesis
     go LPar line r prev = -- r is how many right parentheses we are missing
       let (before, after) = T.breakOn "(" line in
diff --git a/src/EVM/SymExec.hs b/src/EVM/SymExec.hs
index 98dec14ec..72ba513e8 100644
--- a/src/EVM/SymExec.hs
+++ b/src/EVM/SymExec.hs
@@ -15,7 +15,7 @@ import Data.ByteString (ByteString)
 import Data.ByteString qualified as BS
 import Data.Containers.ListUtils (nubOrd)
 import Data.DoubleWord (Word256)
-import Data.List (foldl', sortBy)
+import Data.List (foldl', sortBy, sort, group)
 import Data.Maybe (fromMaybe, mapMaybe)
 import Data.Map.Strict (Map)
 import Data.Map.Strict qualified as Map
@@ -56,23 +56,37 @@ data LoopHeuristic
   | StackBased
   deriving (Eq, Show, Read, ParseField, ParseFields, ParseRecord, Generic)
 
-data ProofResult a b c = Qed a | Cex b | Timeout c
+data ProofResult a b c d = Qed a | Cex b | Unknown c | Error d
   deriving (Show, Eq)
-type VerifyResult = ProofResult () (Expr End, SMTCex) (Expr End)
-type EquivResult = ProofResult () (SMTCex) ()
+type VerifyResult = ProofResult () (Expr End, SMTCex) (Expr End) String
+type EquivResult = ProofResult () (SMTCex) () String
 
-isTimeout :: ProofResult a b c -> Bool
-isTimeout (Timeout _) = True
-isTimeout _ = False
+isUnknown :: ProofResult a b c d -> Bool
+isUnknown (EVM.SymExec.Unknown _) = True
+isUnknown _ = False
 
-isCex :: ProofResult a b c -> Bool
+isError :: ProofResult a b c d -> Bool
+isError (EVM.SymExec.Error _) = True
+isError _ = False
+
+isCex :: ProofResult a b c d -> Bool
 isCex (Cex _) = True
 isCex _ = False
 
-isQed :: ProofResult a b c -> Bool
+isQed :: ProofResult a b c d -> Bool
 isQed (Qed _) = True
 isQed _ = False
 
+groupIssues :: [ProofResult a b c String] -> [(Integer, String)]
+groupIssues results = map (\g -> (into (length g), head g)) grouped
+  where
+    getErr :: ProofResult a b c String -> String
+    getErr (EVM.SymExec.Error k) = k
+    getErr (EVM.SymExec.Unknown _) = "SMT result timeout/unknown"
+    getErr _ = internalError "shouldn't happen"
+    sorted = sort $ map getErr results
+    grouped = group sorted
+
 data VeriOpts = VeriOpts
   { simp :: Bool
   , maxIter :: Maybe Integer
@@ -545,8 +559,8 @@ reachable solvers e = do
         let query = assertProps conf pcs
         res <- checkSat solvers query
         case res of
-          Sat _ -> pure ([query], Just leaf)
-          Unsat -> pure ([query], Nothing)
+          Sat _ -> pure ([getNonError query], Just leaf)
+          Unsat -> pure ([getNonError query], Nothing)
           r -> internalError $ "Invalid solver result: " <> show r
 
 -- | Extract constraints stored in Expr End nodes
@@ -629,9 +643,9 @@ verify solvers opts preState maybepost = do
     toVRes :: (CheckSatResult, Expr End) -> VerifyResult
     toVRes (res, leaf) = case res of
       Sat model -> Cex (leaf, expandCex preState model)
-      EVM.Solvers.Unknown -> Timeout leaf
+      EVM.Solvers.Unknown _ -> EVM.SymExec.Unknown leaf
+      EVM.Solvers.Error e -> EVM.SymExec.Error e
       Unsat -> Qed ()
-      Error e -> internalError $ "solver responded with error: " <> show e
 
 expandCex :: VM Symbolic s -> SMTCex -> SMTCex
 expandCex prestate c = c { store = Map.union c.store concretePreStore }
@@ -742,8 +756,8 @@ equivalenceCheck' solvers branchesA branchesB = do
               -- potential race, but it doesn't matter for correctness
               atomically $ readTVar knownUnsat >>= writeTVar knownUnsat . (props :)
               pure (Qed (), False)
-        (_, EVM.Solvers.Unknown) -> pure (Timeout (), False)
-        (_, Error txt) -> internalError $ "solver returned: " <> (T.unpack txt)
+        (_, EVM.Solvers.Unknown _) -> pure (EVM.SymExec.Unknown (), False)
+        (_, EVM.Solvers.Error txt) -> pure (EVM.SymExec.Error txt, False)
 
     -- 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
@@ -833,12 +847,15 @@ produceModels solvers expr = do
 showModel :: Expr Buf -> (Expr End, CheckSatResult) -> IO ()
 showModel cd (expr, res) = do
   case res of
-    Unsat -> pure () -- ignore unreachable branches
-    Error e -> internalError $ "smt solver returned an error: " <> show e
-    EVM.Solvers.Unknown -> do
+    EVM.Solvers.Unsat -> pure () -- ignore unreachable branches
+    EVM.Solvers.Error e -> do
+      putStrLn ""
+      putStrLn "--- Branch ---"
+      putStrLn $ "Error during SMT solving, cannot check branch " <> e
+    EVM.Solvers.Unknown reason -> do
       putStrLn ""
       putStrLn "--- Branch ---"
-      putStrLn "Unable to produce a model for the following end state:"
+      putStrLn $ "Unable to produce a model for the following end state due to '" <> reason <> "' :"
       T.putStrLn $ indent 2 $ formatExpr expr
       putStrLn ""
     Sat cex -> do
@@ -1045,10 +1062,10 @@ subStores model b = Map.foldlWithKey subStore b model
                else v
           e -> e
 
-getCex :: ProofResult a b c -> Maybe b
+getCex :: ProofResult a b c d -> Maybe b
 getCex (Cex c) = Just c
 getCex _ = Nothing
 
-getTimeout :: ProofResult a b c -> Maybe c
-getTimeout (Timeout c) = Just c
-getTimeout _ = Nothing
+getUnknown :: ProofResult a b c d-> Maybe c
+getUnknown (EVM.SymExec.Unknown c) = Just c
+getUnknown _ = Nothing
diff --git a/src/EVM/Types.hs b/src/EVM/Types.hs
index 24bc36106..0c9f53c0b 100644
--- a/src/EVM/Types.hs
+++ b/src/EVM/Types.hs
@@ -517,6 +517,14 @@ isPBool _ = False
 
 -- Errors ------------------------------------------------------------------------------------------
 
+-- General error helper
+type Err a = Either String a
+getError :: Err a -> String
+getError (Left a) = a
+getError _ = internalError "getLeft on a Right"
+getNonError :: Err a -> a
+getNonError (Right a) = a
+getNonError _ = internalError "getRight on a Left"
 
 -- | Core EVM Error Types
 data EvmError
diff --git a/src/EVM/UnitTest.hs b/src/EVM/UnitTest.hs
index e65b7b93b..998629bc3 100644
--- a/src/EVM/UnitTest.hs
+++ b/src/EVM/UnitTest.hs
@@ -15,13 +15,13 @@ import EVM.FeeSchedule (feeSchedule)
 import EVM.Fetch qualified as Fetch
 import EVM.Format
 import EVM.Solidity
-import EVM.SymExec (defaultVeriOpts, symCalldata, verify, isQed, extractCex, runExpr, prettyCalldata, panicMsg, VeriOpts(..), flattenExpr)
+import EVM.SymExec (defaultVeriOpts, symCalldata, verify, isQed, extractCex, runExpr, prettyCalldata, panicMsg, VeriOpts(..), flattenExpr, isUnknown, isError, groupIssues)
 import EVM.Types
 import EVM.Transaction (initTx)
 import EVM.Stepper (Stepper)
 import EVM.Stepper qualified as Stepper
 
-import Control.Monad (void, when, forM)
+import Control.Monad (void, when, forM, forM_)
 import Control.Monad.ST (RealWorld, ST, stToIO)
 import Control.Monad.State.Strict (execState, get, put, liftIO)
 import Optics.Core
@@ -224,6 +224,10 @@ symRun opts@UnitTestOptions{..} vm (Sig testName types) = do
     -- check postconditions against vm
     (e, results) <- verify solvers (makeVeriOpts opts) (symbolify vm') (Just postcondition)
     let allReverts = not . (any Expr.isSuccess) . flattenExpr $ e
+    when (any isUnknown results || any isError results) $ liftIO $ do
+      putStrLn $ "      \x1b[33mWARNING\x1b[0m: hevm was only able to partially explore the test " <> Text.unpack testName <> " due to: ";
+      forM_ (groupIssues (filter isError results)) $ \(num, str) -> putStrLn $ "      " <> show num <> "x -> " <> str
+      forM_ (groupIssues (filter isUnknown results)) $ \(num, str) -> putStrLn $ "      " <> show num <> "x -> " <> str
 
     -- display results
     if all isQed results
diff --git a/test/test.hs b/test/test.hs
index d84fd1ddd..213bc1830 100644
--- a/test/test.hs
+++ b/test/test.hs
@@ -896,9 +896,8 @@ tests = testGroup "hevm"
         (Expr.indexWord (Lit 2) (Lit 0xff22bb4455667788990011223344556677889900112233445566778899001122))
     , 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)])
+        (pure "(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)])
     , test "indexword-oob-sym" $ assertEqualM ""
         -- indexWord should return 0 for oob access
         (LitByte 0x0)
@@ -1296,6 +1295,51 @@ tests = testGroup "hevm"
         let a = fromJust $ Map.lookup (Var "arg1") cex.vars
         assertEqualM "unexpected cex value" a 44
         putStrLnM "expected counterexample found"
+      ,
+      test "symbolic-mcopy" $ do
+        Just c <- solcRuntime "MyContract"
+            [i|
+            contract MyContract {
+              function fun(uint256 a, uint256 s) external returns (uint) {
+                require(a < 5);
+                assembly {
+                    mcopy(0x2, 0, s)
+                    a:=mload(s)
+                }
+                assert(a < 5);
+                return a;
+              }
+             }
+            |]
+        let sig = Just (Sig "fun(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])
+        (_, k) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c sig [] defaultVeriOpts
+        putStrLnM $ "Ret: " <> (show k)
+      ,
+      test "symbolic-copyslice" $ do
+        Just c <- solcRuntime "MyContract"
+            [i|
+            contract MyContract {
+              function fun(uint256 a, uint256 s) external returns (uint) {
+                require(a < 10);
+                if (a >= 8) {
+                  assembly {
+                      calldatacopy(0x5, s, s)
+                      a:=mload(s)
+                  }
+                } else {
+                  assembly {
+                      calldatacopy(0x2, 0x2, 5)
+                      a:=mload(s)
+                  }
+                }
+                assert(a < 9);
+                return a;
+              }
+             }
+            |]
+        let sig = Just (Sig "fun(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])
+        (_, k) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c sig [] defaultVeriOpts
+        putStrLnM $ "Ret: " <> (show k)
   ]
   , 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...
@@ -2319,7 +2363,7 @@ tests = testGroup "hevm"
             post prestate leaf =
               let y = case getStaticAbiArgs 1 prestate of
                         [y'] -> y'
-                        _ -> error "expected 1 arg"
+                        _ -> internalError "expected 1 arg"
                   this = prestate.state.codeContract
                   prestore = (fromJust (Map.lookup this prestate.env.contracts)).storage
                   prex = Expr.readStorage' (Lit 0) prestore
@@ -3661,10 +3705,11 @@ tests = testGroup "hevm"
             case any isCex res of
               False -> liftIO $ do
                 print $ "OK. Took " <> (show $ diffUTCTime end start) <> " seconds"
-                let timeouts = filter isTimeout res
-                unless (null timeouts) $ do
-                  putStrLnM $ "But " <> (show $ length timeouts) <> " timeout(s) occurred"
-                  internalError "Encountered timeouts"
+                let timeouts = filter isUnknown res
+                let errors = filter isError res
+                unless (null timeouts && null errors) $ do
+                  putStrLnM $ "But " <> (show $ length timeouts) <> " timeout(s) and " <>  (show $ length errors) <> " error(s) occurred"
+                  internalError "Encountered timeout(s) and/or error(s)"
               True -> liftIO $ do
                 putStrLnM $ "Not OK: " <> show f <> " Got: " <> show res
                 internalError "Was NOT equivalent"
@@ -3712,8 +3757,8 @@ checkEquivBase mkprop l r expect = do
        ret = case res of
          Unsat -> Just True
          Sat _ -> Just False
-         Error _ -> Just (not expect)
-         EVM.Solvers.Unknown -> Nothing
+         EVM.Solvers.Error _ -> Just (not expect)
+         EVM.Solvers.Unknown _ -> Nothing
      when (ret == Just (not expect)) $ print res
      pure ret