diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -5,6 +5,19 @@
 The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
 and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).
 
+## [0.50.1] - 2022-12-29
+
+## Fixed
+
+- `hevm exec` no longer fails with `hevm: No match in record selector smttimeout`
+- the `gas`, `gaslimit`, `priorityfee`, and `gasprice` cli options are now respected
+- cleaner formatting for the gas value in the visual debugger
+
+### Changed
+
+- we now build with ghc 9.2.4 by default
+- various perf improvements for concrete execution ([#157](https://github.com/ethereum/hevm/pull/157), [#152](https://github.com/ethereum/hevm/pull/152))
+
 ## [0.50.0] - 2022-12-19
 
 ### Changed
@@ -13,13 +26,22 @@
 symbolic execution decompiles bytecode into a custom IR, and smt queries are constructed based on
 the structure of the term in this IR.
 
-This gives us much deeper control over the encoding, and makes the addition of custom static
-analysis and simplification passes much easier to implement.
+This gives us much deeper control over the encoding, and makes custom static analysis and
+simplification passes much easier to implement.
 
 The symbolic execution engine is now parallel by default, and will distribute granular SMT queries
 across a pool of solvers, allowing analysis to be scaled out horizontally across many CPUs.
 
 more details can be found in the [architecuture](../../architecture.md) docs.
+
+### Removed
+
+The following cli commands have been removed:
+
+- `abiencode`
+- `rlp`
+- `flatten`
+- `strip-metadata`
 
 ## [0.49.0] - 2021-11-12
 
diff --git a/Setup.hs b/Setup.hs
deleted file mode 100644
--- a/Setup.hs
+++ /dev/null
@@ -1,2 +0,0 @@
-import Distribution.Simple
-main = defaultMain
diff --git a/hevm-cli/hevm-cli.hs b/hevm-cli/hevm-cli.hs
--- a/hevm-cli/hevm-cli.hs
+++ b/hevm-cli/hevm-cli.hs
@@ -1,9 +1,7 @@
 -- Main file of the hevm CLI program
 
-{-# Language CPP #-}
 {-# Language DataKinds #-}
 {-# Language DeriveAnyClass #-}
-{-# Language GADTs #-}
 
 module Main where
 
@@ -14,13 +12,8 @@
 import qualified EVM.Fetch
 import qualified EVM.Stepper
 
-
-import qualified EVM.VMTest as VMTest
-
-
 import EVM.SymExec
 import EVM.Debug
-import EVM.ABI
 import qualified EVM.Expr as Expr
 import EVM.SMT
 import qualified EVM.TTY as TTY
@@ -31,36 +24,25 @@
 import EVM.Dapp (findUnitTests, dappInfo, DappInfo, emptyDapp)
 import GHC.Natural
 import EVM.Format (showTraceTree, formatExpr)
-import qualified EVM.Patricia as Patricia
-import Data.Map (Map)
+import Data.Word (Word64)
 
 import qualified EVM.Facts     as Facts
 import qualified EVM.Facts.Git as Git
 import qualified EVM.UnitTest
 
-import GHC.Stack
 import GHC.Conc
-import Control.Concurrent.Async   (async, waitCatch)
 import Control.Lens hiding (pre, passing)
 import Control.Monad              (void, when, forM_, unless)
 import Control.Monad.State.Strict (execStateT, liftIO)
 import Data.ByteString            (ByteString)
 import Data.List                  (intercalate, isSuffixOf)
 import Data.Text                  (unpack, pack)
-import Data.Text.Encoding         (encodeUtf8)
-import Data.Maybe                 (fromMaybe, fromJust, mapMaybe)
+import Data.Maybe                 (fromMaybe, mapMaybe)
 import Data.Version               (showVersion)
 import Data.DoubleWord            (Word256)
-import System.IO                  (hFlush, stdout, stderr)
+import System.IO                  (stderr)
 import System.Directory           (withCurrentDirectory, listDirectory)
 import System.Exit                (exitFailure, exitWith, ExitCode(..))
-import System.Process             (callProcess)
-import qualified Data.Aeson        as JSON
-import qualified Data.Aeson.Types  as JSON
-import Data.Aeson (FromJSON (..), (.:))
-import Data.Aeson.Lens hiding (values)
-import qualified Data.Vector as V
-import qualified Data.ByteString.Lazy  as Lazy
 
 import qualified Data.ByteString        as ByteString
 import qualified Data.ByteString.Char8  as Char8
@@ -68,11 +50,11 @@
 import qualified Data.Map               as Map
 import qualified Data.Text              as T
 import qualified Data.Text.IO           as T
-import qualified System.Timeout         as Timeout
 
 import qualified Paths_hevm      as Paths
 
 import Options.Generic as Options
+import qualified EVM.Transaction
 
 -- This record defines the program's command-line options
 -- automatically via the `optparse-generic` package.
@@ -87,12 +69,12 @@
       , coinbase      :: w ::: Maybe Addr       <?> "Block: coinbase"
       , value         :: w ::: Maybe W256       <?> "Tx: Eth amount"
       , nonce         :: w ::: Maybe W256       <?> "Nonce of origin"
-      , gas           :: w ::: Maybe W256       <?> "Tx: gas amount"
+      , gas           :: w ::: Maybe Word64     <?> "Tx: gas amount"
       , number        :: w ::: Maybe W256       <?> "Block: number"
       , timestamp     :: w ::: Maybe W256       <?> "Block: timestamp"
       , basefee       :: w ::: Maybe W256       <?> "Block: base fee"
       , priorityFee   :: w ::: Maybe W256       <?> "Tx: priority fee"
-      , gaslimit      :: w ::: Maybe W256       <?> "Tx: gas limit"
+      , gaslimit      :: w ::: Maybe Word64     <?> "Tx: gas limit"
       , gasprice      :: w ::: Maybe W256       <?> "Tx: gas price"
       , create        :: w ::: Bool             <?> "Tx: creation"
       , maxcodesize   :: w ::: Maybe W256       <?> "Block: max code size"
@@ -142,12 +124,12 @@
       , coinbase    :: w ::: Maybe Addr       <?> "Block: coinbase"
       , value       :: w ::: Maybe W256       <?> "Tx: Eth amount"
       , nonce       :: w ::: Maybe W256       <?> "Nonce of origin"
-      , gas         :: w ::: Maybe W256       <?> "Tx: gas amount"
+      , gas         :: w ::: Maybe Word64     <?> "Tx: gas amount"
       , number      :: w ::: Maybe W256       <?> "Block: number"
       , timestamp   :: w ::: Maybe W256       <?> "Block: timestamp"
       , basefee     :: w ::: Maybe W256       <?> "Block: base fee"
       , priorityFee :: w ::: Maybe W256       <?> "Tx: priority fee"
-      , gaslimit    :: w ::: Maybe W256       <?> "Tx: gas limit"
+      , gaslimit    :: w ::: Maybe Word64     <?> "Tx: gas limit"
       , gasprice    :: w ::: Maybe W256       <?> "Tx: gas price"
       , create      :: w ::: Bool             <?> "Tx: creation"
       , maxcodesize :: w ::: Maybe W256       <?> "Block: max code size"
@@ -185,25 +167,6 @@
       , maxIterations :: w ::: Maybe Integer            <?> "Number of times we may revisit a particular branching point"
       , askSmtIterations :: w ::: Maybe Integer         <?> "Number of times we may revisit a particular branching point before we consult the smt solver to check reachability (default: 5)"
       }
-  | BcTest -- Run an Ethereum Blockchain/GeneralState test
-      { file      :: w ::: String    <?> "Path to .json test file"
-      , test      :: w ::: [String]  <?> "Test case filter - only run specified test method(s)"
-      , debug     :: w ::: Bool      <?> "Run interactively"
-      , jsontrace :: w ::: Bool      <?> "Print json trace output at every step"
-      , diff      :: w ::: Bool      <?> "Print expected vs. actual state on failure"
-      , timeout   :: w ::: Maybe Int <?> "Execution timeout (default: 10 sec.)"
-      }
-  | Compliance -- Run Ethereum Blockchain compliance report
-      { tests   :: w ::: String       <?> "Path to Ethereum Tests directory"
-      , group   :: w ::: Maybe String <?> "Report group to run: VM or Blockchain (default: Blockchain)"
-      , match   :: w ::: Maybe String <?> "Test case filter - only run methods matching regex"
-      , skip    :: w ::: Maybe String <?> "Test case filter - skip tests containing string"
-      , html    :: w ::: Bool         <?> "Output html report"
-      , timeout :: w ::: Maybe Int    <?> "Execution timeout (default: 10 sec.)"
-      }
-  | MerkleTest -- Insert a set of key values and check against the given root
-      { file :: w ::: String <?> "Path to .json test file"
-      }
   | Version
 
   deriving (Options.Generic)
@@ -299,8 +262,6 @@
     Equivalence {} -> equivalence cmd
     Exec {} ->
       launchExec cmd
-    BcTest {} ->
-      launchTest cmd
     DappTest {} ->
       withCurrentDirectory root $ do
         cores <- num <$> getNumProcessors
@@ -314,26 +275,7 @@
             (False, Debug) -> liftIO $ TTY.main testOpts root testFile
             (False, JsonTrace) -> error "json traces not implemented for dappTest"
             (True, _) -> liftIO $ dappCoverage testOpts (optsMode cmd) testFile
-    Compliance {} ->
-      case (group cmd) of
-        Just "Blockchain" -> launchScript "/run-blockchain-tests" cmd
-        Just "VM" -> launchScript "/run-consensus-tests" cmd
-        _ -> launchScript "/run-blockchain-tests" cmd
-    MerkleTest {} -> merkleTest cmd
 
-launchScript :: String -> Command Options.Unwrapped -> IO ()
-launchScript script cmd =
-  withCurrentDirectory (tests cmd) $ do
-    dataDir <- Paths.getDataDir
-    callProcess "bash"
-      [ dataDir ++ script
-      , "."
-      , show (html cmd)
-      , fromMaybe "" (match cmd)
-      , fromMaybe "" (skip cmd)
-      , show $ fromMaybe 10 (timeout cmd)
-      ]
-
 findJsonFile :: Maybe String -> IO String
 findJsonFile (Just s) = pure s
 findJsonFile Nothing = do
@@ -377,19 +319,6 @@
         putStrLn $ "Not equivalent. Counterexample(s):" <> show res
         exitFailure
 
-checkForVMErrors :: [EVM.VM] -> [String]
-checkForVMErrors [] = []
-checkForVMErrors (vm:vms) =
-  case view EVM.result vm of
-    Just (EVM.VMFailure (EVM.UnexpectedSymbolicArg pc msg _)) ->
-      ("Unexpected symbolic argument at opcode: "
-      <> show pc
-      <> ". "
-      <> msg
-      ) : checkForVMErrors vms
-    _ ->
-      checkForVMErrors vms
-
 getSrcInfo :: Command Options.Unwrapped -> IO DappInfo
 getSrcInfo cmd =
   let root = fromMaybe "." (dappRoot cmd)
@@ -536,8 +465,8 @@
 launchExec cmd = do
   dapp <- getSrcInfo cmd
   vm <- vmFromCommand cmd
-  smtjobs <- fromIntegral <$> getNumProcessors
-  withSolvers Z3 smtjobs (smttimeout cmd) $ \solvers -> do
+  -- TODO: we shouldn't need solvers to execute this code
+  withSolvers Z3 0 Nothing $ \solvers -> do
     case optsMode cmd of
       Run -> do
         vm' <- execStateT (EVM.Stepper.interpret (EVM.Fetch.oracle solvers rpcinfo) . void $ EVM.Stepper.execFully) vm
@@ -574,65 +503,6 @@
      where block' = maybe EVM.Fetch.Latest EVM.Fetch.BlockNumber (block cmd)
            rpcinfo = (,) block' <$> rpc cmd
 
-data Testcase = Testcase {
-  _entries :: [(Text, Maybe Text)],
-  _root :: Text
-} deriving Show
-
-parseTups :: JSON.Value -> JSON.Parser [(Text, Maybe Text)]
-parseTups (JSON.Array arr) = do
-  tupList <- mapM parseJSON (V.toList arr)
-  mapM (\[k, v] -> do
-                  rhs <- parseJSON v
-                  lhs <- parseJSON k
-                  return (lhs, rhs))
-         tupList
-parseTups invalid = JSON.typeMismatch "Malformed array" invalid
-
-
-parseTrieTest :: JSON.Object -> JSON.Parser Testcase
-parseTrieTest p = do
-  kvlist <- p .: "in"
-  entries <- parseTups kvlist
-  root <- p .: "root"
-  return $ Testcase entries root
-
-instance FromJSON Testcase where
-  parseJSON (JSON.Object p) = parseTrieTest p
-  parseJSON invalid = JSON.typeMismatch "Merkle test case" invalid
-
-parseTrieTests :: Lazy.ByteString -> Either String (Map String Testcase)
-parseTrieTests = JSON.eitherDecode'
-
-merkleTest :: Command Options.Unwrapped -> IO ()
-merkleTest cmd = do
-  parsed <- parseTrieTests <$> LazyByteString.readFile (file cmd)
-  case parsed of
-    Left err -> print err
-    Right testcases -> mapM_ runMerkleTest testcases
-
-runMerkleTest :: Testcase -> IO ()
-runMerkleTest (Testcase entries root) =
-  case Patricia.calcRoot entries' of
-    Nothing ->
-      error "Test case failed"
-    Just n ->
-      case n == strip0x (hexText root) of
-        True ->
-          putStrLn "Test case success"
-        False ->
-          error ("Test case failure; expected " <> show root
-                 <> " but got " <> show (ByteStringS n))
-  where entries' = fmap (\(k, v) ->
-                           (tohexOrText k,
-                            tohexOrText (fromMaybe mempty v)))
-                   entries
-
-tohexOrText :: Text -> ByteString
-tohexOrText s = case "0x" `Char8.isPrefixOf` encodeUtf8 s of
-                  True -> hexText s
-                  False -> encodeUtf8 s
-
 -- | Creates a (concrete) VM from command line options
 vmFromCommand :: Command Options.Unwrapped -> IO EVM.VM
 vmFromCommand cmd = do
@@ -680,7 +550,7 @@
         Just t -> t
         Nothing -> error "unexpected symbolic timestamp when executing vm test"
 
-  return $ VMTest.initTx $ withCache (vm0 baseFee miner ts' blockNum prevRan contract)
+  return $ EVM.Transaction.initTx $ withCache (vm0 baseFee miner ts' blockNum prevRan contract)
     where
         block'   = maybe EVM.Fetch.Latest EVM.Fetch.BlockNumber (block cmd)
         value'   = word value 0
@@ -690,7 +560,7 @@
         decipher = hexByteString "bytes" . strip0x
         mkCode bs = if create cmd
                     then EVM.InitCode bs mempty
-                    else EVM.RuntimeCode (fromJust $ Expr.toList (ConcreteBuf bs))
+                    else EVM.RuntimeCode (EVM.ConcreteRuntimeCode bs)
         address' = if create cmd
               then addr address (createAddress origin' (word nonce 0))
               else addr address 0xacab
@@ -702,15 +572,15 @@
           , EVM.vmoptAddress       = address'
           , EVM.vmoptCaller        = litAddr caller'
           , EVM.vmoptOrigin        = origin'
-          , EVM.vmoptGas           = 0
+          , EVM.vmoptGas           = word64 gas 0xffffffffffffffff
           , EVM.vmoptBaseFee       = baseFee
-          , EVM.vmoptPriorityFee   = 0
-          , EVM.vmoptGaslimit      = 0
+          , EVM.vmoptPriorityFee   = word priorityFee 0
+          , EVM.vmoptGaslimit      = word64 gaslimit 0xffffffffffffffff
           , EVM.vmoptCoinbase      = addr coinbase miner
           , EVM.vmoptNumber        = word number blockNum
           , EVM.vmoptTimestamp     = Lit $ word timestamp ts
-          , EVM.vmoptBlockGaslimit = 0
-          , EVM.vmoptGasprice      = 0
+          , EVM.vmoptBlockGaslimit = word64 gaslimit 0xffffffffffffffff
+          , EVM.vmoptGasprice      = word gasprice 0
           , EVM.vmoptMaxCodeSize   = word maxcodesize 0xffffffff
           , EVM.vmoptPrevRandao    = word prevRandao prevRan
           , EVM.vmoptSchedule      = FeeSchedule.berlin
@@ -721,6 +591,7 @@
           , EVM.vmoptAllowFFI      = False
           }
         word f def = fromMaybe def (f cmd)
+        word64 f def = fromMaybe def (f cmd)
         addr f def = fromMaybe def (f cmd)
         bytes f def = maybe def decipher (f cmd)
 
@@ -776,7 +647,7 @@
     (_, _, Nothing) ->
       error "must provide at least (rpc + address) or code"
 
-  return $ (VMTest.initTx $ withCache $ vm0 baseFee miner ts blockNum prevRan calldata' callvalue' caller' contract')
+  return $ (EVM.Transaction.initTx $ withCache $ vm0 baseFee miner ts blockNum prevRan calldata' callvalue' caller' contract')
     & set (EVM.env . EVM.storage) store
 
   where
@@ -785,7 +656,7 @@
     origin'  = addr origin 0
     mkCode bs = if create cmd
                    then EVM.InitCode bs mempty
-                   else EVM.RuntimeCode (fromJust . Expr.toList $ ConcreteBuf bs)
+                   else EVM.RuntimeCode (EVM.ConcreteRuntimeCode bs)
     address' = if create cmd
           then addr address (createAddress origin' (word nonce 0))
           else addr address 0xacab
@@ -796,15 +667,15 @@
       , EVM.vmoptAddress       = address'
       , EVM.vmoptCaller        = caller'
       , EVM.vmoptOrigin        = origin'
-      , EVM.vmoptGas           = 0xffffffffffffffff
-      , EVM.vmoptGaslimit      = 0xffffffffffffffff
+      , EVM.vmoptGas           = word64 gas 0xffffffffffffffff
+      , EVM.vmoptGaslimit      = word64 gaslimit 0xffffffffffffffff
       , EVM.vmoptBaseFee       = baseFee
       , EVM.vmoptPriorityFee   = word priorityFee 0
       , EVM.vmoptCoinbase      = addr coinbase miner
       , EVM.vmoptNumber        = word number blockNum
       , EVM.vmoptTimestamp     = ts
-      , EVM.vmoptBlockGaslimit = 0
-      , EVM.vmoptGasprice      = 0
+      , EVM.vmoptBlockGaslimit = word64 gaslimit 0xffffffffffffffff
+      , EVM.vmoptGasprice      = word gasprice 0
       , EVM.vmoptMaxCodeSize   = word maxcodesize 0xffffffff
       , EVM.vmoptPrevRandao    = word prevRandao prevRan
       , EVM.vmoptSchedule      = FeeSchedule.berlin
@@ -816,65 +687,4 @@
       }
     word f def = fromMaybe def (f cmd)
     addr f def = fromMaybe def (f cmd)
-
-launchTest :: HasCallStack => Command Options.Unwrapped ->  IO ()
-launchTest cmd = do
-  parsed <- VMTest.parseBCSuite <$> LazyByteString.readFile (file cmd)
-  case parsed of
-     Left "No cases to check." -> putStrLn "no-cases ok"
-     Left err -> print err
-     Right allTests ->
-       let testFilter =
-             if null (test cmd)
-             then id
-             else filter (\(x, _) -> elem x (test cmd))
-       in
-         mapM_ (runVMTest (diff cmd) (optsMode cmd) (timeout cmd)) $
-           testFilter (Map.toList allTests)
-
-runVMTest :: HasCallStack => Bool -> Mode -> Maybe Int -> (String, VMTest.Case) -> IO Bool
-runVMTest diffmode mode timelimit (name, x) =
- do
-  let vm0 = VMTest.vmForCase x
-  putStr (name ++ " ")
-  hFlush stdout
-  result <- do
-    action <- async $
-      case mode of
-        Run ->
-          Timeout.timeout (1000000 * (fromMaybe 10 timelimit)) $
-            execStateT (EVM.Stepper.interpret (EVM.Fetch.zero 0 (Just 0)) . void $ EVM.Stepper.execFully) vm0
-        Debug ->
-          withSolvers Z3 0 Nothing $ \solvers -> Just <$> TTY.runFromVM solvers Nothing Nothing emptyDapp vm0
-        JsonTrace ->
-          error "JsonTrace: implement me"
-          -- Just <$> execStateT (EVM.UnitTest.interpretWithCoverage EVM.Fetch.zero EVM.Stepper.runFully) vm0
-    waitCatch action
-  case result of
-    Right (Just vm1) -> do
-      ok <- VMTest.checkExpectation diffmode x vm1
-      putStrLn (if ok then "ok" else "")
-      return ok
-    Right Nothing -> do
-      putStrLn "timeout"
-      return False
-    Left e -> do
-      putStrLn $ "error: " ++ if diffmode
-        then show e
-        else (head . lines . show) e
-      return False
-
-parseAbi :: (AsValue s) => s -> (Text, [AbiType])
-parseAbi abijson =
-  (signature abijson, snd
-    <$> parseMethodInput
-    <$> V.toList
-      (fromMaybe (error "Malformed function abi") (abijson ^? key "inputs" . _Array)))
-
-abiencode :: (AsValue s) => Maybe s -> [String] -> ByteString
-abiencode Nothing _ = error "missing required argument: abi"
-abiencode (Just abijson) args =
-  let (sig', declarations) = parseAbi abijson
-  in if length declarations == length args
-     then abiMethod sig' $ AbiTuple . V.fromList $ zipWith makeAbiValue declarations args
-     else error $ "wrong number of arguments:" <> show (length args) <> ": " <> show args
+    word64 f def = fromMaybe def (f cmd)
diff --git a/hevm.cabal b/hevm.cabal
--- a/hevm.cabal
+++ b/hevm.cabal
@@ -2,7 +2,7 @@
 name:
   hevm
 version:
-  0.50.0
+  0.50.1
 synopsis:
   Ethereum virtual machine evaluator
 description:
@@ -22,9 +22,6 @@
   Ethereum
 build-type:
   Simple
-data-files:
-  run-blockchain-tests
-  run-consensus-tests
 extra-source-files:
   CHANGELOG.md
   test/contracts/lib/test.sol
@@ -43,32 +40,25 @@
   test/contracts/fail/dsProveFail.sol
   test/contracts/fail/invariantFail.sol
 
+flag ci
+  description: Sets flags for compilation in CI
+  default:     False
+  manual:      True
+
+source-repository head
+  type:     git
+  location: https://github.com/ethereum/hevm.git
+
 common shared
-  default-language:
-    Haskell2010
+  if flag(ci)
+    ghc-options: -Werror
+  default-language: GHC2021
   default-extensions:
     LambdaCase
     OverloadedStrings
     RecordWildCards
     TypeFamilies
     ViewPatterns
-    -- GHC2021 default extensions, remove me when GHC is updated to 9.2
-    BangPatterns
-    ConstraintKinds
-    DeriveDataTypeable
-    DeriveFunctor
-    DeriveGeneric
-    DoAndIfThenElse
-    EmptyDataDecls
-    FlexibleContexts
-    FlexibleInstances
-    ForeignFunctionInterface
-    GeneralizedNewtypeDeriving
-    PolyKinds
-    RankNTypes
-    ScopedTypeVariables
-    StandaloneDeriving
-    TypeOperators
 
 library
   import: shared
@@ -85,7 +75,6 @@
     EVM.Exec,
     EVM.Facts,
     EVM.Facts.Git,
-    EVM.Flatten,
     EVM.Format,
     EVM.Fetch,
     EVM.FeeSchedule,
@@ -106,7 +95,6 @@
     EVM.TTYCenteredList,
     EVM.Types,
     EVM.UnitTest,
-    EVM.VMTest
   other-modules:
     Paths_hevm
   autogen-modules:
@@ -130,12 +118,12 @@
     Decimal                           >= 0.5.1 && < 0.6,
     containers                        >= 0.6.0 && < 0.7,
     deepseq                           >= 1.4.4 && < 1.5,
-    time                              >= 1.8.0 && < 1.11,
+    time                              >= 1.11.1.1 && < 1.12,
     transformers                      >= 0.5.6 && < 0.6,
     tree-view                         >= 0.5 && < 0.6,
     abstract-par                      >= 0.3.3 && < 0.4,
     aeson                             >= 2.0.0 && < 2.1,
-    bytestring                        >= 0.10.8 && < 0.11,
+    bytestring                        >= 0.11.3.1 && < 0.12,
     scientific                        >= 0.3.6 && < 0.4,
     binary                            >= 0.8.6 && < 0.9,
     text                              >= 1.2.3 && < 1.3,
@@ -143,22 +131,22 @@
     vector                            >= 0.12.1 && < 0.13,
     ansi-wl-pprint                    >= 0.6.9 && < 0.7,
     base16-bytestring                 >= 1.0.0 && < 2.0,
-    brick                             >= 0.68 && < 0.69,
+    brick                             >= 1.4 && < 1.5,
     megaparsec                        >= 9.0.0 && < 10.0,
     mtl                               >= 2.2.2 && < 2.3,
     directory                         >= 1.3.3 && < 1.4,
     filepath                          >= 1.4.2 && < 1.5,
-    vty                               >= 5.25.1 && < 5.34,
+    vty                               >= 5.37 && < 5.38,
     cereal                            >= 0.5.8 && < 0.6,
-    cryptonite                        >= 0.27 && <= 0.29,
+    cryptonite                        >= 0.30 && < 0.31,
     memory                            >= 0.16.0 && < 0.20,
     data-dword                        >= 0.3.1 && < 0.4,
     fgl                               >= 5.7.0 && < 5.8,
     free                              >= 5.1.3 && < 5.2,
     haskeline                         >= 0.8.0 && < 0.9,
     process                           >= 1.6.5 && < 1.7,
-    lens                              >= 5.0.0 && < 5.1,
-    lens-aeson                        >= 1.0.2 && < 1.2,
+    lens                              >= 5.1.1 && < 5.2,
+    lens-aeson                        >= 1.2.2 && < 1.3,
     monad-par                         >= 0.3.5 && < 0.4,
     async                             >= 2.2.4 && < 2.3,
     multiset                          >= 0.3.4 && < 0.4,
@@ -179,7 +167,7 @@
     smt2-parser                       >= 0.1.0.1,
     word-wrap                         >= 0.5 && < 0.6,
     spool                             >= 0.1 && < 0.2,
-    parsec                            >= 3.1.14.0 && < 3.1.15
+    parsec                            >= 3.1.15 && < 3.2,
   hs-source-dirs:
     src
 
@@ -247,12 +235,15 @@
     HUnit >= 1.6,
     QuickCheck,
     quickcheck-instances,
+    aeson,
     base,
     base16-bytestring,
     binary,
     containers,
     directory,
     bytestring,
+    filemanip,
+    filepath,
     here,
     hevm,
     lens,
@@ -270,6 +261,7 @@
     time,
     array,
     vector,
+    witherable,
     smt2-parser >= 0.1.0.1
 
 library test-utils
@@ -283,10 +275,14 @@
     test-base
   build-depends:
     test-utils
+  other-modules:
+    EVM.TestUtils
   if os(darwin)
-     extra-libraries: c++
+    extra-libraries: c++
+    -- https://gitlab.haskell.org/ghc/ghc/-/issues/11829
+    ld-options: -Wl,-keep_dwarf_unwind
   else
-     extra-libraries: stdc++
+    extra-libraries: stdc++
 
 --- Test Suites ---
 
@@ -307,3 +303,11 @@
     exitcode-stdio-1.0
   main-is:
     rpc.hs
+
+test-suite ethereum-tests
+  import:
+    test-common
+  type:
+    exitcode-stdio-1.0
+  main-is:
+    BlockchainTests.hs
diff --git a/run-blockchain-tests b/run-blockchain-tests
deleted file mode 100644
--- a/run-blockchain-tests
+++ /dev/null
@@ -1,150 +0,0 @@
-#!/usr/bin/env bash
-set -e
-
-# Invoke with hevm e.g.
-# hevm compliance --tests ~/ethereum-tests --skip modexp --timeout 20 --html
-
-HEVM=${HEVM:-hevm}
-
-if [[ "$#" -lt 1 ]]; then
-  echo >&2 "usage: $(basename "$0") <tests-dir>"
-  exit 1
-fi
-
-tests=$1
-html=$2
-match=$3
-skip=$4
-timeout=${5:-10}
-
-_html () {
-cat <<.
-<!doctype html>
-<title>hevm test results</title>
-<style>
-* { font-family:
-"latin modern mono", "fantasque sans mono",
-inconsolata, menlo, monospace;
-font-size: 22px;
-line-height: 26px; }
-body { margin: 2rem; }
-header { text-align: center; margin: 4rem 0; }
-table { border-collapse: collapse; width: 100%; }
-tr:nth-child(even) { background: rgba(0, 0, 0, 0.05); }
-td:not(:first-child):not(:last-child) { padding: 0 1rem; }
-.category { opacity: 0.6; text-align: right }
-a { color: darkblue; text-decoration: none; }
-h1, h2 { text-align: center; margin-top: 2rem  }
-.testcase { font-weight: bold }
-#failed .testcase { color: rgb(200, 0, 0) }
-#balancefailed .testcase { color: rgb(200, 200, 0) }
-#passed .testcase { color: rgb(0, 150, 0) }
-#skipped .testcase { color: rgb(0, 100, 250) }
-#timeout .testcase { color: rgb(0, 0, 250) }
-</style>
-<header>
-<h1>hevm consensus test report</h1>
-<p>$(date +%Y-%m-%d)</p>
-<p>$(echo "$npass passed, $nbal bad-balance, $nnon bad-nonce, $nstr bad-storage, $nfail failed, $nskip skipped, $ntime timeout")</p>
-(Test suite: <span class=GeneralStateTests</span>GeneralStateTests</span> for Berlin)
-</header>
-<h2>Failed tests</h2>
-<table id=failed>
-<tbody>
-$(echo $noncefailed)
-$(echo $storagefailed)
-$(echo $failed)
-</table>
-<h2>Failed tests (due to balance only)</h2>
-<table id=balancefailed>
-<tbody>
-$(echo $balancefailed)
-</table>
-<h2>Timeout tests</h2>
-<table id=timeout>
-<tbody>
-$(echo $timeouts)
-</table>
-<h2>Skipped tests</h2>
-<table id=skipped>
-<tbody>
-$(echo $skipped)
-</table>
-<h2>Passed tests</h2>
-<table id=passed>
-<tbody>
-$(echo $passed)
-</table>
-.
-}
-
-shopt -s nocasematch
-{
-  cd "$tests"
-  for x in BlockchainTests/GeneralStateTests/*/*; do
-    if [ -d $x ]; then
-      for y in $x/*; do
-        if [[ $y =~ .*$match.* ]] && [[ -n $skip && $y =~ .*$skip.* ]]; then
-          for job in $(<$y jq '.|keys[]' -r); do
-            echo -n "$job " ; echo "skip"
-          done
-        elif [[ $y =~ .*$match.* ]]; then
-          set +e
-          "$HEVM" bc-test --file $y --timeout $timeout 2>&1
-          set -e
-        fi
-      done
-    else
-      if [[ $x =~ .*$match.* ]] && [[ -n $skip && $x =~ .*$skip.* ]]; then
-        for job in $(<$x jq '.|keys[]' -r); do
-          echo -n "$job " ; echo "skip"
-        done
-      elif [[ $x =~ .*$match.* ]]; then
-        set +e
-        "$HEVM" bc-test --file $x --timeout $timeout 2>&1
-        set -e
-      fi
-    fi
-  done
-} | {
-  while read test outcome; do
-    echo >&2 "$test $outcome"
-    row="<tr><td class=testcase>$test<td>$outcome"
-    row+=$'\n'
-    case $outcome in
-      ok)          passed+=$row ;;
-      bad-balance) balancefailed+=$row ;;
-      bad-nonce)   noncefailed+=$row ;;
-      bad-storage) storagefailed+=$row ;;
-      timeout)     timeouts+=$row ;;
-      skip)        skipped+=$row ;;
-      *)           failed+=$row ;;
-    esac
-  done
-
-  sum () { echo -ne "$1" | wc -l | awk '{print $1}'; }
-
-  npass=$(sum "$passed")
-  nbal=$(sum "$balancefailed")
-  nnon=$(sum "$noncefailed")
-  nstr=$(sum "$storagefailed")
-  nfail=$(sum "$failed")
-  ntime=$(sum "$timeouts")
-  nskip=$(sum "$skipped")
-
-  echo >&2 "passed: $npass"
-  echo >&2 "bad-balance: $nbal"
-  echo >&2 "bad-nonce: $nnon"
-  echo >&2 "bad-storage: $nstr"
-  echo >&2 "failed: $nfail"
-  echo >&2 "timeout: $ntime"
-  echo >&2 "skipped: $nskip"
-
-  if [[ $html == "True" ]]; then
-    _html
-  fi
-
-  nbad=$(($nbal + $nnon + $nstr + $nfail))
-
-  [[ $nbad -gt 0 ]] && exit 1 || exit 0
-}
diff --git a/run-consensus-tests b/run-consensus-tests
deleted file mode 100644
--- a/run-consensus-tests
+++ /dev/null
@@ -1,110 +0,0 @@
-#!/usr/bin/env bash
-set -e
-
-# Invoke with hevm e.g.
-# hevm compliance --tests ~/ethereum-tests --group VM --skip quadratic --html
-
-HEVM=${HEVM:-hevm}
-
-if [[ "$#" -lt 1 ]]; then
-  echo >&2 "usage: $(basename "$0") <tests-dir>"
-  exit 1
-fi
-
-tests=$1
-html=$2
-match=$3
-skip=$4
-timeout=${5:-10}
-
-_html() {
-cat <<.
-<!doctype html>
-<title>hevm test results</title>
-<style>
-* { font-family:
-"latin modern mono", "fantasque sans mono",
-inconsolata, menlo, monospace;
-font-size: 22px;
-line-height: 26px; }
-body { margin: 2rem; }
-header { text-align: center; margin: 4rem 0; }
-table { border-collapse: collapse; width: 100%; }
-tr:nth-child(even) { background: rgba(0, 0, 0, 0.05); }
-td:not(:first-child):not(:last-child) { padding: 0 1rem; }
-.category { opacity: 0.6; text-align: right }
-a { color: darkblue; text-decoration: none; }
-h1, h2 { text-align: center; margin-top: 2rem  }
-.testcase { font-weight: bold }
-#failed .testcase { color: rgb(200, 0, 0) }
-#passed .testcase { color: rgb(0, 150, 0) }
-#skipped .testcase { color: rgb(0, 100, 250) }
-</style>
-<header>
-<h1>hevm consensus test report</h1>
-<p>$(date +%Y-%m-%d)</p>
-<p>$(echo "$npass passed, $nfail failed, $nskip skipped")</p>
-(Test suite: <span class=VMTests</span>VMTests</span> for ConstantinopleFix)
-</header>
-<h2>Failed tests</h2>
-<table id=failed>
-<tbody>
-$(echo $failed)
-</table>
-<h2>Skipped tests</h2>
-<table id=skipped>
-<tbody>
-$(echo $skipped)
-</table>
-<h2>Passed tests</h2>
-<table id=passed>
-<tbody>
-$(echo $passed)
-</table>
-.
-}
-
-{
-  cd "$tests"
-  for x in VMTests/*/*; do
-    if [[ $x =~ .*$match.* ]] && [[ -n $skip && $x =~ .*$skip.* ]]; then
-      for job in $(<$x jq '.|keys[]' -r); do
-        echo "$x $job skip"
-      done
-    elif [[ $x =~ .*$match.* ]]; then
-      echo -n "$x " ; "$HEVM" vm-test --file $x --timeout $timeout 2>&1
-    fi
-  done
-} | {
-  while read path test outcome; do
-    echo >&2 "$path $test $outcome"
-    category=$(dirname "$path")
-    testcase=$(basename "${path%.json}")
-    row="<tr><td class=testcase>$testcase<td>$outcome<td class=category>$category"
-    row+=$'\n'
-    case $outcome in
-      ok)      passed+=$row ;;
-      skip)    skipped+=$row ;;
-      timeout) timouts+=row ;;
-      *)       failed+=$row ;;
-    esac
-  done
-
-  sum () { echo -ne "$1" | wc -l | awk '{print $1}'; }
-
-  nfail=$(sum "$failed")
-  npass=$(sum "$passed")
-  nskip=$(sum "$skipped")
-  ntime=$(sum "$timeouts")
-
-  echo >&2 "passed: $npass"
-  echo >&2 "failed: $nfail"
-  echo >&2 "timeout: $ntime"
-  echo >&2 "skipped: $nskip"
-
-  if [[ $html == "True" ]]; then
-    _html
-  fi
-
-  [[ $nfail -gt 0 ]] && exit 1 || exit 0
-}
diff --git a/src/EVM.hs b/src/EVM.hs
--- a/src/EVM.hs
+++ b/src/EVM.hs
@@ -11,11 +11,11 @@
 import Data.Text (unpack)
 import Data.Text.Encoding (decodeUtf8, encodeUtf8)
 import EVM.ABI
-import EVM.Types hiding (IllegalOverflow)
+import EVM.Types hiding (IllegalOverflow, Error)
 import EVM.Solidity
 import EVM.Concrete (createAddress, create2Address)
 import EVM.Op
-import EVM.Expr (readStorage, writeStorage, readByte, readWord, writeWord, writeByte, bufLength, indexWord, litAddr, readBytes, word256At, copySlice, isLitByte)
+import EVM.Expr (readStorage, writeStorage, readByte, readWord, writeWord, writeByte, bufLength, indexWord, litAddr, readBytes, word256At, copySlice)
 import EVM.FeeSchedule (FeeSchedule (..))
 import Options.Generic as Options
 import qualified EVM.Precompiled
@@ -28,7 +28,7 @@
 import Data.ByteString.Lazy         (fromStrict)
 import Data.Map.Strict              (Map)
 import Data.Set                     (Set, insert, member, fromList)
-import Data.Maybe                   (fromMaybe)
+import Data.Maybe                   (fromMaybe, fromJust)
 import Data.Sequence                (Seq)
 import Data.Vector.Storable         (Vector)
 import Data.Foldable                (toList)
@@ -58,7 +58,6 @@
 import Crypto.PubKey.ECC.ECDSA (signDigestWith, PrivateKey(..), Signature(..))
 import Crypto.PubKey.ECC.Types (getCurveByName, CurveName(..), Point(..))
 import Crypto.PubKey.ECC.Generate (generateQ)
-import Data.DoubleWord (Word256(Word256), Word128 (Word128))
 
 -- * Data types
 
@@ -305,10 +304,18 @@
   hopefully we do not have to deal with dynamic immutable before we get a real data section...
 -}
 data ContractCode
-  = InitCode ByteString (Expr Buf)     -- ^ "Constructor" code, during contract creation
-  | RuntimeCode (V.Vector (Expr Byte)) -- ^ "Instance" code, after contract creation
+  = InitCode ByteString (Expr Buf) -- ^ "Constructor" code, during contract creation
+  | RuntimeCode RuntimeCode -- ^ "Instance" code, after contract creation
   deriving (Show)
 
+-- | We have two variants here to optimize the fully concrete case.
+-- ConcreteRuntimeCode just wraps a ByteString
+-- SymbolicRuntimeCode is a fixed length vector of potentially symbolic bytes, which lets us handle symbolic pushdata (e.g. from immutable variables in solidity).
+data RuntimeCode
+  = ConcreteRuntimeCode ByteString
+  | SymbolicRuntimeCode (V.Vector (Expr Byte))
+  deriving (Show, Eq, Ord)
+
 -- runtime err when used for symbolic code
 instance Eq ContractCode where
   (InitCode a b) == (InitCode c d) = a == c && b == d
@@ -392,7 +399,7 @@
 blankState = FrameState
   { _contract     = 0
   , _codeContract = 0
-  , _code         = RuntimeCode mempty
+  , _code         = RuntimeCode (ConcreteRuntimeCode "")
   , _pc           = 0
   , _stack        = mempty
   , _memory       = mempty
@@ -421,7 +428,8 @@
 bytecode :: Getter Contract (Expr Buf)
 bytecode = contractcode . to f
   where f (InitCode _ _) = mempty
-        f (RuntimeCode ops) = Expr.fromList ops
+        f (RuntimeCode (ConcreteRuntimeCode bs)) = ConcreteBuf bs
+        f (RuntimeCode (SymbolicRuntimeCode ops)) = Expr.fromList ops
 
 instance Semigroup Cache where
   a <> b = Cache
@@ -603,7 +611,8 @@
     else do
       let ?op = case (the state code) of
                   InitCode conc _ -> BS.index conc (the state pc)
-                  RuntimeCode ops ->
+                  RuntimeCode (ConcreteRuntimeCode bs) -> BS.index bs (the state pc)
+                  RuntimeCode (SymbolicRuntimeCode ops) ->
                     fromMaybe (error "could not analyze symbolic code") $
                       unlitByte $ ops V.! the state pc
 
@@ -614,13 +623,10 @@
           let !n = num x - 0x60 + 1
               !xs = case the state code of
                 InitCode conc _ -> Lit $ word $ padRight n $ BS.take n (BS.drop (1 + the state pc) conc)
-                RuntimeCode ops ->
+                RuntimeCode (ConcreteRuntimeCode bs) -> Lit $ word $ BS.take n $ BS.drop (1 + the state pc) bs
+                RuntimeCode (SymbolicRuntimeCode ops) ->
                   let bytes = V.take n $ V.drop (1 + the state pc) ops
-                  in if all isLitByte bytes then -- optimize concrete path
-                       let litBytes = V.toList $ V.catMaybes $ unlitByte <$> bytes
-                           padded = BS.replicate (32 - length litBytes) 0 <> BS.pack litBytes
-                       in Lit $ word padded
-                     else readWord (Lit 0) $ Expr.fromList $ padLeft' 32 bytes
+                  in readWord (Lit 0) $ Expr.fromList $ padLeft' 32 bytes
           limitStack 1 $
             burn g_verylow $ do
               next
@@ -1075,7 +1081,9 @@
           case stk of
             (x:xs) ->
               burn g_mid $ forceConcrete x "JUMP: symbolic jumpdest" $ \x' ->
-                checkJump x' xs
+                case toInt x' of
+                  Nothing -> vmError EVM.BadJumpDestination
+                  Just i -> checkJump i xs
             _ -> underrun
 
         -- op: JUMPI
@@ -1085,7 +1093,9 @@
                 burn g_high $
                   let jump :: Bool -> EVM ()
                       jump False = assign (state . stack) xs >> next
-                      jump _    = checkJump x' xs
+                      jump _    = case toInt x' of
+                        Nothing -> vmError EVM.BadJumpDestination
+                        Just i -> checkJump i xs
                   in case maybeLitWord y of
                       Just y' -> jump (0 /= y')
                       -- if the jump condition is symbolic, we explore both sides
@@ -1674,7 +1684,8 @@
 accountEmpty :: Contract -> Bool
 accountEmpty c =
   case view contractcode c of
-    RuntimeCode b -> null b
+    RuntimeCode (ConcreteRuntimeCode "") -> True
+    RuntimeCode (SymbolicRuntimeCode b) -> null b
     _ -> False
   && (view nonce c == 0)
   && (view balance c == 0)
@@ -1703,10 +1714,17 @@
       creation <- use (tx . isCreate)
       createe  <- use (state . contract)
       createeExists <- (Map.member createe) <$> use (env . contracts)
-      case Expr.toList output of
-        Nothing -> vmError $ UnexpectedSymbolicArg pc' "runtime code cannot have an abstract lentgh" [output]
-        Just ops ->
-          when (creation && createeExists) $ replaceCode createe (RuntimeCode ops)
+      let onContractCode contractCode =
+            when (creation && createeExists) $ replaceCode createe contractCode
+      case output of
+        ConcreteBuf bs ->
+          onContractCode $ RuntimeCode (ConcreteRuntimeCode bs)
+        _ ->
+          case Expr.toList output of
+            Nothing ->
+              vmError $ UnexpectedSymbolicArg pc' "runtime code cannot have an abstract lentgh" [output]
+            Just ops ->
+              onContractCode $ RuntimeCode (SymbolicRuntimeCode ops)
 
   -- compute and pay the refund to the caller and the
   -- corresponding payment to the miner
@@ -1735,7 +1753,7 @@
   -- pay out the block reward, recreating the miner if necessary
   preuse (env . contracts . ix miner) >>= \case
     Nothing -> modifying (env . contracts)
-      (Map.insert miner (initialContract (EVM.RuntimeCode mempty)))
+      (Map.insert miner (initialContract (EVM.RuntimeCode (ConcreteRuntimeCode ""))))
     Just _  -> noop
   modifying (env . contracts)
     (Map.adjust (over balance (+ blockReward)) miner)
@@ -2119,7 +2137,8 @@
 collision :: Maybe Contract -> Bool
 collision c' = case c' of
   Just c -> (view nonce c /= 0) || case view contractcode c of
-    RuntimeCode b -> not $ null b
+    RuntimeCode (ConcreteRuntimeCode "") -> False
+    RuntimeCode (SymbolicRuntimeCode b) -> not $ null b
     _ -> True
   Nothing -> False
 
@@ -2368,17 +2387,23 @@
           case how of
             -- Case 4: Returning during a creation?
             FrameReturned output -> do
-                case Expr.toList output of
-                  Nothing -> vmError $
-                    UnexpectedSymbolicArg
-                      (view (state . pc) oldVm)
-                      "runtime code cannot have an abstract length"
-                      [output]
-                  Just newCode -> do
-                    replaceCode createe (RuntimeCode newCode)
+              let onContractCode contractCode = do
+                    replaceCode createe contractCode
                     assign (state . returndata) mempty
                     reclaimRemainingGasAllowance
                     push (num createe)
+              case output of
+                ConcreteBuf bs ->
+                  onContractCode $ RuntimeCode (ConcreteRuntimeCode bs)
+                _ ->
+                  case Expr.toList output of
+                    Nothing -> vmError $
+                      UnexpectedSymbolicArg
+                        (view (state . pc) oldVm)
+                        "runtime code cannot have an abstract length"
+                        [output]
+                    Just newCode -> do
+                      onContractCode $ RuntimeCode (SymbolicRuntimeCode newCode)
 
             -- Case 5: Reverting during a creation?
             FrameReverted output -> do
@@ -2459,9 +2484,7 @@
   :: (MonadState VM m) => TraceData -> m Trace
 withTraceLocation x = do
   vm <- get
-  let
-    Just this =
-      currentContract vm
+  let this = fromJust $ currentContract vm
   pure Trace
     { _traceData = x
     , _traceContract = this
@@ -2558,19 +2581,16 @@
 
 -- * Bytecode data functions
 
-checkJump :: (Integral n) => n -> [Expr EWord] -> EVM ()
+checkJump :: Int -> [Expr EWord] -> EVM ()
 checkJump x xs = do
   theCode <- use (state . code)
   self <- use (state . codeContract)
   theCodeOps <- use (env . contracts . ix self . codeOps)
   theOpIxMap <- use (env . contracts . ix self . opIxMap)
-  let ops = case theCode of
-        InitCode ops' _ -> V.fromList $ LitByte <$> BS.unpack ops'
-        RuntimeCode ops' -> ops'
-      op = do
-        -- TODO: not a big fan of how bounds are checked, change this
-        b <- if x < num (length ops) then ops V.!? num x else Nothing
-        unlitByte b
+  let op = case theCode of
+        InitCode ops _ -> BS.indexMaybe ops x
+        RuntimeCode (ConcreteRuntimeCode ops) -> BS.indexMaybe ops x
+        RuntimeCode (SymbolicRuntimeCode ops) -> ops V.!? x >>= unlitByte
   case op of
     Nothing -> vmError EVM.BadJumpDestination
     Just b ->
@@ -2606,7 +2626,10 @@
         go v (n, !i, !j, !m) _ =
           {- PUSH data. -}        (n - 1,        i + 1, j,     m >> Vector.write v i j)
 
-mkOpIxMap (RuntimeCode ops)
+mkOpIxMap (RuntimeCode (ConcreteRuntimeCode ops)) =
+  mkOpIxMap (InitCode ops mempty) -- a bit hacky
+
+mkOpIxMap (RuntimeCode (SymbolicRuntimeCode ops))
   = Vector.create $ Vector.new (length ops) >>= \v ->
       let (_, _, _, m) = foldl (go v) (0, 0, 0, return ()) (stripBytecodeMetadataSym $ V.toList ops)
       in m >> return v
@@ -2632,7 +2655,9 @@
       (op, pushdata) = case code' of
         InitCode xs' _ ->
           (BS.index xs' i, fmap LitByte $ BS.unpack $ BS.drop i xs')
-        RuntimeCode xs' ->
+        RuntimeCode (ConcreteRuntimeCode xs') ->
+          (BS.index xs' i, fmap LitByte $ BS.unpack $ BS.drop i xs')
+        RuntimeCode (SymbolicRuntimeCode xs') ->
           ( fromMaybe (error "unexpected symbolic code") . unlitByte $ xs' V.! i , V.toList $ V.drop i xs')
   in if (opslen code' < i)
      then Nothing
@@ -2756,25 +2781,24 @@
 
 -- Maps operation indicies into a pair of (bytecode index, operation)
 mkCodeOps :: ContractCode -> RegularVector.Vector (Int, Op)
-mkCodeOps (InitCode bytes _) = RegularVector.fromList . toList $ go 0 bytes
+mkCodeOps contractCode =
+  let l = case contractCode of
+            InitCode bytes _ ->
+              LitByte <$> (BS.unpack bytes)
+            RuntimeCode (ConcreteRuntimeCode ops) ->
+              LitByte <$> (BS.unpack $ stripBytecodeMetadata ops)
+            RuntimeCode (SymbolicRuntimeCode ops) ->
+              stripBytecodeMetadataSym $ V.toList ops
+  in RegularVector.fromList . toList $ go 0 l
   where
     go !i !xs =
-      case BS.uncons xs of
-        Nothing ->
-          mempty
-        Just (x, xs') ->
-          let j = opSize x
-          in (i, readOp x (fmap LitByte $ BS.unpack xs')) Seq.<| go (i + j) (BS.drop j xs)
-mkCodeOps (RuntimeCode ops) = RegularVector.fromList . toList $ go' 0 (stripBytecodeMetadataSym $ V.toList ops)
-  where
-    go' !i !xs =
       case uncons xs of
         Nothing ->
           mempty
         Just (x, xs') ->
           let x' = fromMaybe (error "unexpected symbolic code argument") $ unlitByte x
               j = opSize x'
-          in (i, readOp x' xs') Seq.<| go' (i + j) (drop j xs)
+          in (i, readOp x' xs') Seq.<| go (i + j) (drop j xs)
 
 -- * Gas cost calculation helpers
 
@@ -2889,23 +2913,27 @@
 
 hashcode :: ContractCode -> Expr EWord
 hashcode (InitCode ops args) = keccak $ (ConcreteBuf ops) <> args
-hashcode (RuntimeCode ops) = keccak . Expr.fromList $ ops
+hashcode (RuntimeCode (ConcreteRuntimeCode ops)) = keccak (ConcreteBuf ops)
+hashcode (RuntimeCode (SymbolicRuntimeCode ops)) = keccak . Expr.fromList $ ops
 
 -- | The length of the code ignoring any constructor args.
 -- This represents the region that can contain executable opcodes
 opslen :: ContractCode -> Int
 opslen (InitCode ops _) = BS.length ops
-opslen (RuntimeCode ops) = length ops
+opslen (RuntimeCode (ConcreteRuntimeCode ops)) = BS.length ops
+opslen (RuntimeCode (SymbolicRuntimeCode ops)) = length ops
 
 -- | The length of the code including any constructor args.
 -- This can return an abstract value
 codelen :: ContractCode -> Expr EWord
 codelen c@(InitCode {}) = bufLength $ toBuf c
-codelen (RuntimeCode ops) = Lit . num $ length ops
+codelen (RuntimeCode (ConcreteRuntimeCode ops)) = Lit . num $ BS.length ops
+codelen (RuntimeCode (SymbolicRuntimeCode ops)) = Lit . num $ length ops
 
 toBuf :: ContractCode -> Expr Buf
 toBuf (InitCode ops args) = ConcreteBuf ops <> args
-toBuf (RuntimeCode ops) = Expr.fromList ops
+toBuf (RuntimeCode (ConcreteRuntimeCode ops)) = ConcreteBuf ops
+toBuf (RuntimeCode (SymbolicRuntimeCode ops)) = Expr.fromList ops
 
 
 codeloc :: EVM CodeLocation
@@ -2914,12 +2942,6 @@
   let self = view (state . contract) vm
       loc = view (state . pc) vm
   pure (self, loc)
-
-toWord64 :: W256 -> Maybe Word64
-toWord64 n =
-  if n <= num (maxBound :: Word64)
-    then let (W256 (Word256 _ (Word128 _ n'))) = n in Just n'
-    else Nothing
 
 -- * Emacs setup
 
diff --git a/src/EVM/ABI.hs b/src/EVM/ABI.hs
--- a/src/EVM/ABI.hs
+++ b/src/EVM/ABI.hs
@@ -384,7 +384,9 @@
       | (x, i) <- zip (map fromIntegral xs) [1..] ]
 
 asUInt :: Integral i => Int -> (i -> a) -> Get a
-asUInt n f = (\(AbiUInt _ x) -> f (fromIntegral x)) <$> getAbi (AbiUIntType n)
+asUInt n f = y <$> getAbi (AbiUIntType n)
+  where y (AbiUInt _ x) = f (fromIntegral x)
+        y _ = error "can't happen"
 
 getWord256 :: Get Word256
 getWord256 = pack32 8 <$> replicateM 8 getWord32be
@@ -405,13 +407,12 @@
 
 genAbiValue :: AbiType -> Gen AbiValue
 genAbiValue = \case
-   AbiUIntType n -> genUInt n
-   AbiIntType n ->
-     do a <- genUInt n
-        let AbiUInt _ x = a
-        pure $ AbiInt n (signedWord (x - 2^(n-1)))
+   AbiUIntType n -> AbiUInt n <$> genUInt n
+   AbiIntType n -> do
+     x <- genUInt n
+     pure $ AbiInt n (signedWord (x - 2^(n-1)))
    AbiAddressType ->
-     (\(AbiUInt _ x) -> AbiAddress (fromIntegral x)) <$> genUInt 20
+     AbiAddress . fromIntegral <$> genUInt 20
    AbiBoolType ->
      elements [AbiBool False, AbiBool True]
    AbiBytesType n ->
@@ -430,7 +431,8 @@
    AbiTupleType ts ->
      AbiTuple <$> mapM genAbiValue ts
   where
-    genUInt n = AbiUInt n <$> arbitraryIntegralWithMax (2^n-1)
+    genUInt :: Int -> Gen Word256
+    genUInt n = arbitraryIntegralWithMax (2^n-1) :: Gen Word256
 
 instance Arbitrary AbiType where
   arbitrary = oneof
diff --git a/src/EVM/Dapp.hs b/src/EVM/Dapp.hs
--- a/src/EVM/Dapp.hs
+++ b/src/EVM/Dapp.hs
@@ -2,7 +2,7 @@
 
 module EVM.Dapp where
 
-import EVM (Trace, traceContract, traceOpIx, ContractCode(..), Contract(..), codehash, contractcode)
+import EVM (Trace, traceContract, traceOpIx, ContractCode(..), Contract(..), codehash, contractcode, RuntimeCode (..))
 import EVM.ABI (Event, AbiType, SolError)
 import EVM.Debug (srcMapCodePos)
 import EVM.Solidity
@@ -68,7 +68,7 @@
   let
     solcs = Map.elems solcByName
     astIds = astIdMap $ snd <$> toList (view sourceAsts sources)
-    immutables = filter ((/=) mempty . _immutableReferences) solcs
+    immutables = filter ((/=) mempty . (view immutableReferences)) solcs
 
   in DappInfo
     { _dappRoot = root
@@ -176,7 +176,11 @@
 lookupCode :: ContractCode -> DappInfo -> Maybe SolcContract
 lookupCode (InitCode c _) a =
   snd <$> preview (dappSolcByHash . ix (keccak' (stripBytecodeMetadata c))) a
-lookupCode (RuntimeCode c) a = let
+lookupCode (RuntimeCode (ConcreteRuntimeCode c)) a =
+  case snd <$> preview (dappSolcByHash . ix (keccak' (stripBytecodeMetadata c))) a of
+    Just x -> return x
+    Nothing -> snd <$> find (compareCode c . fst) (view dappSolcByCode a)
+lookupCode (RuntimeCode (SymbolicRuntimeCode c)) a = let
     code = BS.pack $ mapMaybe unlitByte $ V.toList c
   in case snd <$> preview (dappSolcByHash . ix (keccak' (stripBytecodeMetadata code))) a of
     Just x -> return x
diff --git a/src/EVM/Dev.hs b/src/EVM/Dev.hs
--- a/src/EVM/Dev.hs
+++ b/src/EVM/Dev.hs
@@ -7,7 +7,7 @@
 -}
 module EVM.Dev where
 
-import Data.ByteString hiding (putStrLn, writeFile, zip)
+import Data.ByteString hiding (writeFile, zip)
 import Control.Monad.State.Strict hiding (state)
 import Data.Maybe (fromJust)
 import System.Directory
@@ -30,7 +30,6 @@
 import System.Exit (exitFailure)
 import qualified EVM.Fetch as Fetch
 import qualified EVM.FeeSchedule as FeeSchedule
-import qualified Data.Vector as V
 
 checkEquiv :: (Typeable a) => Expr a -> Expr a -> IO ()
 checkEquiv a b = withSolvers Z3 1 Nothing $ \s -> do
@@ -363,7 +362,7 @@
 initVm :: ByteString -> VM
 initVm bs = vm
   where
-    contractCode = RuntimeCode $ V.fromList $ LitByte <$> unpack bs
+    contractCode = RuntimeCode (ConcreteRuntimeCode bs)
     c = Contract
       { _contractcode = contractCode
       , _balance      = 0
diff --git a/src/EVM/Exec.hs b/src/EVM/Exec.hs
--- a/src/EVM/Exec.hs
+++ b/src/EVM/Exec.hs
@@ -45,7 +45,7 @@
     , vmoptTxAccessList = mempty
     , vmoptAllowFFI = False
     }) & set (env . contracts . at ethrunAddress)
-             (Just (initialContract (RuntimeCode mempty)))
+             (Just (initialContract (RuntimeCode (ConcreteRuntimeCode ""))))
 
 exec :: MonadState VM m => m VMResult
 exec =
diff --git a/src/EVM/Expr.hs b/src/EVM/Expr.hs
--- a/src/EVM/Expr.hs
+++ b/src/EVM/Expr.hs
@@ -8,7 +8,7 @@
 module EVM.Expr where
 
 import Prelude hiding (LT, GT)
-import Data.Bits
+import Data.Bits hiding (And, Xor)
 import Data.DoubleWord (Int256, Word256(Word256), Word128(Word128))
 import Data.Int (Int32)
 import Data.Word
@@ -266,13 +266,16 @@
 -- Attempts to read a concrete word from a buffer by reading 32 individual bytes and joining them together
 -- returns an abstract ReadWord expression if a concrete word cannot be constructed
 readWordFromBytes :: Expr EWord -> Expr Buf -> Expr EWord
+readWordFromBytes (Lit idx) (ConcreteBuf bs) =
+  case toInt idx of
+    Nothing -> Lit 0
+    Just i -> Lit $ word $ padRight 32 $ BS.take 32 $ BS.drop i bs
 readWordFromBytes i@(Lit idx) buf = let
     bytes = [readByte (Lit i') buf | i' <- [idx .. idx + 31]]
   in if Prelude.and . (fmap isLitByte) $ bytes
      then Lit (bytesToW256 . mapMaybe unlitByte $ bytes)
      else ReadWord i buf
 readWordFromBytes idx buf = ReadWord idx buf
-
 
 {- | Copies a slice of src into dst.
 
diff --git a/src/EVM/Facts.hs b/src/EVM/Facts.hs
--- a/src/EVM/Facts.hs
+++ b/src/EVM/Facts.hs
@@ -54,7 +54,6 @@
 import qualified Data.ByteString.Char8 as Char8
 import qualified Data.Map as Map
 import qualified Data.Set as Set
-import qualified Data.Vector as V
 
 -- We treat everything as ASCII byte strings because
 -- we only use hex digits (and the letter 'x').
@@ -159,7 +158,7 @@
 apply1 vm fact =
   case fact of
     CodeFact    {..} -> flip execState vm $ do
-      assign (env . contracts . at addr) (Just (EVM.initialContract (EVM.RuntimeCode (V.fromList $ LitByte <$> BS.unpack blob))))
+      assign (env . contracts . at addr) (Just (EVM.initialContract (EVM.RuntimeCode (EVM.ConcreteRuntimeCode blob))))
       when (view (state . contract) vm == addr) $ EVM.loadContract addr
     StorageFact {..} ->
       vm & over (env . storage) (writeStorage (litAddr addr) (Lit which) (Lit what))
@@ -172,7 +171,7 @@
 apply2 vm fact =
   case fact of
     CodeFact    {..} -> flip execState vm $ do
-      assign (cache . fetchedContracts . at addr) (Just (EVM.initialContract (EVM.RuntimeCode (V.fromList $ LitByte <$> BS.unpack blob))))
+      assign (cache . fetchedContracts . at addr) (Just (EVM.initialContract (EVM.RuntimeCode (EVM.ConcreteRuntimeCode blob))))
       when (view (state . contract) vm == addr) $ EVM.loadContract addr
     StorageFact {..} -> let
         store = view (cache . fetchedStorage) vm
diff --git a/src/EVM/Fetch.hs b/src/EVM/Fetch.hs
--- a/src/EVM/Fetch.hs
+++ b/src/EVM/Fetch.hs
@@ -6,7 +6,7 @@
 import Prelude hiding (Word)
 
 import EVM.ABI
-import EVM.Types    (Addr, W256, hexText, Expr(Lit, LitByte), Expr(..), Prop(..), (.&&), (./=))
+import EVM.Types    (Addr, W256, hexText, Expr(Lit), Expr(..), Prop(..), (.&&), (./=))
 import EVM.SMT
 import EVM          (EVM, Contract, Block, initialContract, nonce, balance, external)
 import qualified EVM.FeeSchedule as FeeSchedule
@@ -29,7 +29,6 @@
 import System.Process
 
 import qualified Network.Wreq.Session as Session
-import qualified Data.Vector as V
 import Numeric.Natural (Natural)
 
 -- | Abstract representation of an RPC fetch request
@@ -143,7 +142,7 @@
   theBalance <- MaybeT $ fetch (QueryBalance addr)
 
   return $
-    initialContract (EVM.RuntimeCode (V.fromList $ LitByte <$> BS.unpack theCode))
+    initialContract (EVM.RuntimeCode (EVM.ConcreteRuntimeCode theCode))
       & set nonce    theNonce
       & set balance  theBalance
       & set external True
@@ -203,7 +202,7 @@
     -- we generate a new array to the fetched contract here
     EVM.PleaseFetchContract addr continue -> do
       contract <- case info of
-                    Nothing -> return $ Just $ initialContract (EVM.RuntimeCode mempty)
+                    Nothing -> return $ Just $ initialContract (EVM.RuntimeCode (EVM.ConcreteRuntimeCode ""))
                     Just (n, url) -> fetchContractFrom n url addr
       case contract of
         Just x -> return $ continue x
diff --git a/src/EVM/Flatten.hs b/src/EVM/Flatten.hs
deleted file mode 100644
--- a/src/EVM/Flatten.hs
+++ /dev/null
@@ -1,466 +0,0 @@
-module EVM.Flatten (flatten) where
-
--- This module concatenates all the imported dependencies
--- of a given source file, so that you can paste the result
--- into Remix or the Etherscan contract verification page.
---
--- The concatenated files are stripped of import directives
--- and compiler version pragmas are merged into just one.
---
--- This module is mostly independent from the rest of Hevm,
--- using only the source code metadata support modules.
-
-import EVM.Dapp (DappInfo, dappSources)
-import EVM.Types (regexMatches)
-import EVM.Solidity (sourceAsts)
-import EVM.Demand (demand)
-
--- We query and alter the Solidity code using the compiler's AST.
--- The AST is a deep JSON structure, so we use Aeson and Lens.
-import Control.Lens (preview, view, universe)
-import Data.Aeson (Value (String))
-import Data.Aeson.Lens (key, _String, _Array, _Integer)
-
--- We use the FGL graph library for the topological sort.
--- (We use four FGL functions and they're all in different modules!)
-import qualified Data.Graph.Inductive.Graph as Fgl
-import qualified Data.Graph.Inductive.PatriciaTree as Fgl
-import qualified Data.Graph.Inductive.Query.BFS as Fgl
-import qualified Data.Graph.Inductive.Query.DFS as Fgl
-
--- The Solidity version pragmas can be arbitrary SemVer ranges,
--- so we use this library to parse them.
-import Data.SemVer (SemVerRange, parseSemVerRange)
-import qualified Data.SemVer as SemVer
-
-import Control.Monad (forM)
-import Data.ByteString (ByteString)
-import Data.Foldable (foldl', toList)
-import Data.List (sort, nub, (\\))
-import Data.Map (Map, (!), (!?))
-import Data.Maybe (mapMaybe, isJust, catMaybes, fromMaybe)
-import Data.Text (Text, unpack, pack, intercalate)
-import Data.Text.Encoding (encodeUtf8, decodeUtf8)
-import Text.Read (readMaybe)
-
-import qualified Data.Map as Map
-import qualified Data.Text as Text
-import qualified Data.ByteString as BS
-
--- Define an alias for FGL graphs with text nodes and unlabeled edges.
-type FileGraph = Fgl.Gr Text ()
-
--- | Get field either inside 'attributes' object (combined-json format)
--- or directly.
-getAttribute :: Text -> Value -> Maybe Value
-getAttribute s v = case preview (key "attributes" . key s) v of
-  Nothing -> preview (key s) v
-  Just r  -> Just r
-
--- Given the AST of a source file, resolve all its imported paths.
-importsFrom :: Value -> [Text]
-importsFrom ast =
-  let
-    -- We use the astonishing `universe` function from Lens
-    -- to get a lazy list of every node in the AST structure.
-    allNodes :: [Value]
-    allNodes = universe ast
-
-    -- Given some subvalue in the AST, we check if it's an import,
-    -- and if so, return its resolved import path.
-    resolveImport :: Value -> Maybe Text
-    resolveImport node =
-      case preview (key "nodeType") node of
-        Just (String "ImportDirective") -> view _String <$> getAttribute "absolutePath" node
-        _ ->
-          case preview (key "name") node of
-            Just (String "ImportDirective") ->
-              view _String <$> getAttribute "absolutePath" node
-            _ ->
-              Nothing
-
-  -- Now we just try to resolve import paths at all subnodes.
-  in mapMaybe resolveImport allNodes
-
-flatten :: DappInfo -> Text -> IO ()
-flatten dapp target = do
-  let
-    -- The nodes and edges are defined below.
-    graph :: FileGraph
-    graph = Fgl.mkGraph nodes edges
-
-    -- The graph nodes are ints with source paths as labels.
-    nodes :: [(Int, Text)]
-    nodes = zip [1..] (Map.keys asts)
-
-    -- The graph edges are defined by module imports.
-    edges =
-      [ (indices ! s, indices ! t, ()) -- Edge from S to T
-      | (s, v) <- Map.toList asts      -- for every file S
-      , t      <- importsFrom v ]      -- and every T imported by S.
-
-    -- We can look up the node index for a source file path.
-    indices :: Map Text Int
-    indices = Map.fromList [(v, k) | (k, v) <- nodes]
-
-    -- The JSON ASTs are indexed by source file path.
-    asts :: Map Text Value
-    asts = view (dappSources . sourceAsts) dapp
-
-    topScopeIds :: [Integer]
-    topScopeIds = mconcat $ fmap f $ Map.elems asts
-      where
-        id' = preview (key "id" . _Integer)
-        f ast =
-          [ fromJust' "no id for SourceUnit" $ id' node
-          | node <- universe ast
-          , nodeIs "SourceUnit" node
-          ]
-
-    contractsAndStructsToRename :: Map Integer Text
-    contractsAndStructsToRename =
-      Map.fromList
-        $ indexed [ x | x <- xs, (snd x) `elem` xs' ]
-      where
-        xs = concatMap f $ Map.elems asts
-        xs' = repeated $ fmap snd xs
-        scope x = getAttribute "scope" x >>= preview _Integer
-        name x = getAttribute "name" x >>= preview _String
-        id' = preview (key "id" . _Integer)
-        p x = (nodeIs "ContractDefinition" x || nodeIs "StructDefinition" x)
-          && (fromJust' "no contract/struct scope" $ scope x) `elem` topScopeIds
-        f ast =
-          [ ( fromJust' "no id for top scoped contract or struct" $ id' node
-            , fromJust' "no id for top scoped contract or struct" $ name node
-            )
-          | node <- universe ast
-          , p node
-          ]
-
-    contractStructs :: [(Integer, (Integer, Text))]
-    contractStructs = mconcat $ fmap f $ Map.elems asts
-      where
-        scope x = getAttribute "scope" x >>= preview _Integer
-        cname x = getAttribute "canonicalName" x >>= preview _String
-        id' = preview (key "id" . _Integer)
-        p x = (nodeIs "StructDefinition" x)
-          && (fromJust' "nested struct" $ scope x) `Map.member` contractsAndStructsToRename
-        f ast =
-          [ let
-              id'' = fromJust' "no id for nested struct" $ id' node
-              cname' = fromJust'
-                ("no canonical name of nested struct with id:" ++ show id'') $ cname node
-              ref = fromJust'
-                ("no scope of nested struct with id:" ++ show id'') $ scope node
-            in
-              (id'', (ref, cname'))
-          | node <- universe ast
-          , p node
-          ]
-
-  -- We use the target source file to make a relevant subgraph
-  -- with only files transitively depended on from the target.
-  case Map.lookup target indices of
-    Nothing ->
-      error "didn't find contract AST"
-    Just root -> do
-      let
-        -- Restrict the graph to only the needed nodes,
-        -- discovered via breadth-first search from the target.
-        subgraph :: Fgl.Gr Text ()
-        subgraph = Fgl.subgraph (Fgl.bfs root graph) graph
-
-        -- Now put the source file paths in the right order
-        -- by sorting topologically.
-        ordered :: [Text]
-        ordered = reverse (Fgl.topsort' subgraph)
-
-        -- Take the highest Solidity version from all pragmas.
-        pragma :: Text
-        pragma = maximalPragma (Map.elems (Map.filterWithKey (\k _ -> k `elem` ordered) asts))
-
-        license :: Text
-        license = joinLicenses (Map.elems (Map.filterWithKey (\k _ -> k `elem` ordered) asts))
-      -- Read the source files in order and strip unwanted directives.
-      -- Also add an informative comment with the original source file path.
-      sources <-
-        forM ordered $ \path -> do
-          src <- BS.readFile (unpack path)
-          pure $ mconcat
-            [ "////// ", encodeUtf8 path, "\n"
-            -- Fold over a list of source transforms
-            , fst
-                (prefixContractAst
-                  contractsAndStructsToRename
-                  contractStructs
-                  (stripImportsAndPragmas (stripLicense src) (asts ! path))
-                  (asts ! path))
-            , "\n"
-            ]
-
-      -- Force all evaluation before any printing happens, to avoid
-      -- partial output.
-      demand target; demand pragma; demand sources
-
-      -- Finally print the whole concatenation.
-      putStrLn $ "// hevm: flattened sources of " <> unpack target
-      putStrLn (unpack license)
-      putStrLn (unpack pragma)
-      BS.putStr (mconcat sources)
-
-joinLicenses :: [Value] -> Text
-joinLicenses asts =
-  case nub $ mapMaybe (\ast -> getAttribute "license" ast >>= preview _String) asts of
-    [] -> ""
-    x -> "// SPDX-License-Identifier: " <> intercalate " AND " x
-
--- | Construct a new Solidity version pragma for the highest mentioned version
---  given a list of source file ASTs.
-maximalPragma :: [Value] -> Text
-maximalPragma asts = (
-    case mapMaybe versions asts of
-      [] -> "" -- allow for no pragma
-      xs ->
-        "pragma solidity "
-          <> pack (show (rangeIntersection xs))
-          <> ";\n"
-  )
-  <> (
-    mconcat . nub . sort . fmap (\ast ->
-      mconcat $ fmap
-        (\xs -> "pragma "
-          <> intercalate " " [x | String x <- xs]
-          <> ";\n")
-        (otherPragmas ast)
-    )
-  ) asts
-
-
-  where
-    isVersionPragma :: [Value] -> Bool
-    isVersionPragma (String "solidity" : _) = True
-    isVersionPragma _ = False
-
-    pragmaComponents :: Value -> [[Value]]
-    pragmaComponents ast = components
-      where
-        ps :: [Value]
-        ps = filter (nodeIs "PragmaDirective") (universe ast)
-
-        components :: [[Value]]
-        components = catMaybes $
-          fmap
-          ((fmap toList) . (\x -> getAttribute "literals" x >>= preview _Array))
-          ps
-
-    -- Simple way to combine many SemVer ranges.  We don't actually
-    -- optimize these boolean expressions, so the resulting pragma
-    -- might be redundant, like ">=0.4.23 >=0.5.0 <0.6.0".
-    rangeIntersection :: [SemVerRange] -> SemVerRange
-    rangeIntersection = foldr1 SemVer.And . nub . sort
-
-    -- Get the semantic version range from a source file's pragma,
-    -- or nothing if no pragma present.
-    versions :: Value -> Maybe SemVerRange
-    versions ast = fmap grok components
-      where
-        components :: Maybe [Value]
-        components =
-          case filter isVersionPragma (pragmaComponents ast) of
-            [_:xs] -> Just xs
-            []  -> Nothing
-            x   -> error $ "multiple version pragmas" ++ show x
-
-        grok :: [Value] -> SemVerRange
-        grok xs =
-          let
-            rangeText = mconcat [x | String x <- xs]
-          in
-            case parseSemVerRange rangeText of
-              Right r -> r
-              Left _ ->
-                error ("failed to parse SemVer range " ++ show rangeText)
-
-    otherPragmas :: Value -> [[Value]]
-    otherPragmas = (filter (not . isVersionPragma)) . pragmaComponents
-
-nodeIs :: Text -> Value -> Bool
-nodeIs t x = isSourceNode && hasRightName
-  where
-    isSourceNode =
-      isJust (preview (key "src") x)
-    hasRightName =
-      Just t == preview (key "name" . _String) x
-      || Just t == preview (key "nodeType" . _String) x
-
--- | Removes all lines containing "SPDX-License-Identifier"
-stripLicense :: ByteString -> (ByteString, Int)
-stripLicense bs =
-  (encodeUtf8 $ Text.unlines (lines' \\ licenseLines), - sum (((1 +) . Text.length) <$> licenseLines))
-  where lines' = Text.lines $ decodeUtf8 bs
-        licenseLines = filter (regexMatches "SPDX-License-Identifier") lines'
-
--- | (bytes, offset) where offset is added or incremeneted as text is
--- inserted or removed from the source file
-stripImportsAndPragmas :: (ByteString, Int) -> Value -> (ByteString, Int)
-stripImportsAndPragmas bso ast = stripAstNodes bso ast p
-  where
-    p x = nodeIs "ImportDirective" x || nodeIs "PragmaDirective" x
-
-stripAstNodes :: (ByteString, Int)-> Value -> (Value -> Bool) -> (ByteString, Int)
-stripAstNodes bso ast p =
-  cutRanges [sourceRange node | node <- universe ast, p node]
-
-  where
-    -- Removes a set of non-overlapping ranges from a bytestring
-    -- by commenting them out.
-    cutRanges :: [(Int, Int)] -> (ByteString, Int)
-    cutRanges (sort -> rs) = foldl' f bso rs
-      where
-        f (bs', n) (i, j) =
-          ( cut bs' (i + n) (j + n)
-          , n + length ("/*  */" :: String))
-
-    -- Comments out the bytes between two indices from a bytestring.
-    cut :: ByteString -> Int -> Int -> ByteString
-    cut x i j =
-      let (a, b) = BS.splitAt i x
-      in a <> "/* " <> BS.take (j - i) b <> " */" <> BS.drop (j - i) b
-
-readAs :: Read a => Text -> Maybe a
-readAs = readMaybe . Text.unpack
-
-prefixContractAst :: Map Integer Text -> [(Integer, (Integer, Text))] -> (ByteString, Int) -> Value -> (ByteString, Int)
-prefixContractAst castr cs bso ast = prefixAstNodes
-  where
-    bs = fst bso
-    refDec x = getAttribute "referencedDeclaration" x >>= preview _Integer
-    name x = getAttribute "name" x >>= preview _String
-    id' = preview (key "id" . _Integer)
-
-    -- Is node top level defined type (contract/interface/struct)
-    p x = (nodeIs "ContractDefinition" x || nodeIs "StructDefinition" x)
-      && (fromJust' "id of any" $ id' x) `Map.member` castr
-
-    -- Is node identifier that is referencing top level defined type
-    p' x =
-      (nodeIs "Identifier" x || nodeIs "UserDefinedTypeName" x)
-        && (isJust $ refDec x) && (fromJust' "refDec of ident/userdef" $ refDec x) `Map.member` castr
-
-    -- Is node identifier that is referencing a struct nested in a top level
-    -- defined contract/interface
-    p'' x =
-      (nodeIs "Identifier" x || nodeIs "UserDefinedTypeName" x)
-      && (isJust $ name x)
-      && (
-        let
-          refs = fmap fst cs
-          i = fromJust' "no id for ident/userdef" $ id' x
-          ref = fromJust' ("no refDec for ident/userdef: " ++ show i) $ refDec x
-          n = fromJust' ("no name for ident/userdef: " ++ show i) $ name x
-          cn = fromJust'
-            ("no match for lookup in nested structs: "
-              ++ show i
-              ++ " -> "
-              ++ show ref
-            ) $ lookup ref cs
-        in
-          -- XXX: comparing canonical name with name of nested structs
-          -- might not be super great
-          ref `elem` refs && n == snd cn
-      )
-
-    p''' x = p x || p' x || p'' x
-
-    prefixAstNodes :: (ByteString, Int)
-    prefixAstNodes  =
-      cutRanges [sourceId node | node <- universe ast, p''' node]
-
-    -- Parses the `id` and `attributes.referencedDeclaration` field of an AST node
-    -- into a pair of byte indices.
-    sourceId :: Value -> (Int, Integer)
-    sourceId v =
-      if (not $ p v || p' v) &&  p'' v then (
-        let
-          ref = fromJust' "refDec of nested struct ref" $ refDec v
-          cn = fromJust' "no match for lookup in nested structs" $ lookup ref cs
-        in
-          (end, fst cn)
-      ) else
-        fromJust' "internal error: no id found for contract reference" x
-
-      where
-        (start, end) = sourceRange v
-        f :: Text -> Maybe (Int, Integer)
-        f t | t `elem` ["ContractDefinition", "StructDefinition"] =
-              let
-                name' = encodeUtf8 $ fromJust' "no name for contract/struct" $ name v
-                bs' = snd $ BS.splitAt (start + snd bso) bs
-                pos = start
-                  + (BS.length $ fst $ BS.breakSubstring name' bs')
-                  + (BS.length name')
-              in
-                fmap ((,) pos) $ id' v
-            | t `elem` ["UserDefinedTypeName", "Identifier"] =
-              fmap ((,) end) $ refDec v
-            | otherwise =
-                error $ "internal error: not a contract reference: " ++ show t
-
-        x :: Maybe (Int, Integer)
-        x = case preview (key "nodeType" . _String) v of
-          Just t -> f t
-          Nothing -> case preview (key "name" . _String) v of
-            Just t -> f t
-            Nothing ->
-              error "internal error: not a contract reference"
-
-    -- Prefix a set of non-overlapping ranges from a bytestring
-    -- by commenting them out.
-    cutRanges :: [(Int, Integer)] -> (ByteString, Int)
-    cutRanges (sort -> rs) = foldl' f bso rs
-      where
-        f (bs', n) (i, t) =
-          let
-            t' = "_" <> (castr ! t)
-          in
-            ( prefix t' bs' (i + n)
-            , n + Text.length t' )
-
-    -- Comments out the bytes between two indices from a bytestring.
-    prefix :: Text -> ByteString -> Int -> ByteString
-    prefix t x i =
-      let (a, b) = BS.splitAt i x
-      in a <> encodeUtf8 t <> b
-
--- Parses the `src` field of an AST node into a pair of byte indices.
-sourceRange :: Value -> (Int, Int)
-sourceRange v =
-  case preview (key "src" . _String) v of
-    Just (Text.splitOn ":" -> [readAs -> Just i, readAs -> Just n, _]) ->
-      (i, i + n)
-    _ ->
-      error "internal error: no source position for AST node"
-
-fromJust' :: String -> Maybe a -> a
-fromJust' msg = \case
-  Just x -> x
-  Nothing -> error msg
-
-repeated :: Eq a => [a] -> [a]
-repeated = fmap fst $ foldl' f ([], [])
-  where
-    f (acc, seen) x =
-      ( if (x `elem` seen) && (not $ x `elem` acc)
-        then x : acc
-        else acc
-      , x : seen
-      )
-
-indexed :: [(Integer, Text)] -> [(Integer, Text)]
-indexed = fst . foldl' f ([], Map.empty) -- (zip (fmap snd xs) $ replicate (length xs) 0) xs
-  where
-    f (acc, seen) (id', n) =
-      let
-        count = (fromMaybe 0 $ seen !? n) + 1
-      in
-        ((id', pack $ show count) : acc, Map.insert n count seen)
diff --git a/src/EVM/Format.hs b/src/EVM/Format.hs
--- a/src/EVM/Format.hs
+++ b/src/EVM/Format.hs
@@ -6,8 +6,10 @@
   ( formatExpr
   , contractNamePart
   , contractPathPart
+  , showError
   , showTree
   , showTraceTree
+  , showValues
   , prettyvmresult
   , showCall
   , showWordExact
@@ -31,7 +33,7 @@
 import EVM (VM, cheatCode, traceForest, traceData, Error (..))
 import EVM (Trace, TraceData (..), Query (..), FrameContext (..))
 import EVM.Types (maybeLitWord, W256 (..), num, word, Expr(..), EType(..))
-import EVM.Types (Addr, ByteStringS(..))
+import EVM.Types (Addr, ByteStringS(..), Error(..))
 import EVM.ABI (AbiValue (..), Event (..), AbiType (..), SolError (..))
 import EVM.ABI (Indexed (NotIndexed), getAbiSeq)
 import EVM.ABI (parseTypeName, formatString)
@@ -48,7 +50,7 @@
 import Data.ByteString.Lazy (toStrict, fromStrict)
 import Data.DoubleWord (signedWord)
 import Data.Foldable (toList)
-import Data.Maybe (catMaybes, fromMaybe)
+import Data.Maybe (catMaybes, fromMaybe, fromJust)
 import Data.Text (Text, pack, unpack, intercalate)
 import Data.Text (dropEnd, splitOn)
 import Data.Text.Encoding (decodeUtf8, decodeUtf8')
@@ -68,20 +70,17 @@
   deriving (Show)
 
 showDec :: Signedness -> W256 -> Text
-showDec signed (W256 w) =
-  let
+showDec signed (W256 w)
+  | i == num cheatCode = "<hevm cheat address>"
+  | (i :: Integer) == 2 ^ (256 :: Integer) - 1 = "MAX_UINT256"
+  | otherwise = Text.pack (show (i :: Integer))
+  where
     i = case signed of
           Signed   -> num (signedWord w)
           Unsigned -> num w
-  in
-    if i == num cheatCode
-    then "<hevm cheat address>"
-    else if (i :: Integer) == 2 ^ (256 :: Integer) - 1
-    then "MAX_UINT256"
-    else Text.pack (show (i :: Integer))
 
 showWordExact :: W256 -> Text
-showWordExact w = humanizeInteger w
+showWordExact w = humanizeInteger (toInteger w)
 
 showWordExplanation :: W256 -> DappInfo -> Text
 showWordExplanation w _ | w > 0xffffffff = showDec Unsigned w
@@ -318,7 +317,7 @@
       let calltype = if target == context
                      then "call "
                      else "delegatecall "
-          Lit hash' = hash -- FIXME: irrefutable pattern, handle symbolic
+          hash' = fromJust $ maybeLitWord hash
       in case preview (dappSolcByHash . ix hash' . _2) dapp of
         Nothing ->
           calltype
@@ -372,18 +371,27 @@
 contractPathPart :: Text -> Text
 contractPathPart x = Text.split (== ':') x !! 0
 
+prettyError :: EVM.Types.Error -> String
+prettyError= \case
+  Invalid -> "Invalid Opcode"
+  EVM.Types.IllegalOverflow -> "Illegal Overflow"
+  SelfDestruct -> "Self Destruct"
+  EVM.Types.StackLimitExceeded -> "Stack limit exceeded"
+  EVM.Types.InvalidMemoryAccess -> "Invalid memory access"
+  EVM.Types.BadJumpDestination -> "Bad jump destination"
+  TmpErr err -> "Temp error: " <> err
+
+
 prettyvmresult :: (?context :: DappContext) => Expr End -> String
 prettyvmresult (EVM.Types.Revert _ (ConcreteBuf "")) = "Revert"
 prettyvmresult (EVM.Types.Revert _ msg) = "Revert: " ++ (unpack $ showError msg)
-prettyvmresult (EVM.Types.Invalid _) = "Invalid Opcode"
 prettyvmresult (EVM.Types.Return _ (ConcreteBuf msg) _) =
   if BS.null msg
   then "Stop"
   else "Return: " <> show (ByteStringS msg)
 prettyvmresult (EVM.Types.Return _ _ _) =
   "Return: <symbolic>"
-prettyvmresult (EVM.Types.IllegalOverflow _) = "Illegal Overflow"
-prettyvmresult (EVM.Types.SelfDestruct _) = "Self Destruct"
+prettyvmresult (Failure _ err) = prettyError err
 prettyvmresult e = error "Internal Error: Invalid Result: " <> show e
 
 indent :: Int -> Text -> Text
diff --git a/src/EVM/SMT.hs b/src/EVM/SMT.hs
--- a/src/EVM/SMT.hs
+++ b/src/EVM/SMT.hs
@@ -25,7 +25,6 @@
 import Data.Word
 import Numeric (readHex)
 import Data.ByteString (ByteString)
-import Data.Maybe (fromMaybe)
 
 import qualified Data.ByteString as BS
 import qualified Data.List as List
@@ -785,10 +784,10 @@
   t -> error $ "Internal Error: cannot parse " <> t <> " into an Expr"
 
 getVars :: (TS.Text -> Expr EWord) -> SolverInstance -> [TS.Text] -> IO (Map (Expr EWord) W256)
-getVars parseFn inst names = Map.mapKeys parseFn <$> foldM getVar mempty names
+getVars parseFn inst names = Map.mapKeys parseFn <$> foldM getOne mempty names
   where
-    getVar :: Map TS.Text W256 -> TS.Text -> IO (Map TS.Text W256)
-    getVar acc name = do
+    getOne :: Map TS.Text W256 -> TS.Text -> IO (Map TS.Text W256)
+    getOne acc name = do
       raw <- getValue inst (T.fromStrict name)
       let
         parsed = case parseCommentFreeFileMsg getValueRes (T.toStrict raw) of
diff --git a/src/EVM/Solidity.hs b/src/EVM/Solidity.hs
--- a/src/EVM/Solidity.hs
+++ b/src/EVM/Solidity.hs
@@ -47,6 +47,7 @@
   , sourceFiles
   , sourceLines
   , sourceAsts
+  , immutableReferences
   , stripBytecodeMetadata
   , stripBytecodeMetadataSym
   , signature
@@ -94,6 +95,7 @@
 import System.Process
 import Text.Read            (readMaybe)
 
+import qualified Data.Aeson.Key as Key
 import qualified Data.ByteString        as BS
 import qualified Data.ByteString.Base16 as BS16
 import qualified Data.HashMap.Strict    as HMap
@@ -131,7 +133,9 @@
 
 instance Read SlotType where
   readsPrec _ ('m':'a':'p':'p':'i':'n':'g':'(':s) =
-    let (lhs:rhs) = Text.splitOn " => " (pack s)
+    let (lhs,rhs) = case Text.splitOn " => " (pack s) of
+          (l:r) -> (l,r)
+          _ -> error "could not parse storage item"
         first = fromJust $ parseTypeName mempty lhs
         target = fromJust $ parseTypeName mempty (Text.replace ")" "" (last rhs))
         rest = fmap (fromJust . (parseTypeName mempty . (Text.replace "mapping(" ""))) (take (length rhs - 1) rhs)
@@ -303,35 +307,35 @@
 yul :: Text -> Text -> IO (Maybe ByteString)
 yul contract src = do
   (json, path) <- yul' src
-  let (Just f) = json ^?! key "contracts" ^? key path
-      (Just c) = f ^? key (if Text.null contract then "object" else contract)
+  let f = (json ^?! key "contracts") ^?! key (Key.fromText path)
+      c = f ^?! key (Key.fromText $ if Text.null contract then "object" else contract)
       bytecode = c ^?! key "evm" ^?! key "bytecode" ^?! key "object" . _String
   pure $ toCode <$> (Just bytecode)
 
 yulRuntime :: Text -> Text -> IO (Maybe ByteString)
 yulRuntime contract src = do
   (json, path) <- yul' src
-  let (Just f) = json ^?! key "contracts" ^? key path
-      (Just c) = f ^? key (if Text.null contract then "object" else contract)
+  let f = (json ^?! key "contracts") ^?! key (Key.fromText path)
+      c = f ^?! key (Key.fromText $ if Text.null contract then "object" else contract)
       bytecode = c ^?! key "evm" ^?! key "deployedBytecode" ^?! key "object" . _String
   pure $ toCode <$> (Just bytecode)
 
 solidity :: Text -> Text -> IO (Maybe ByteString)
 solidity contract src = do
   (json, path) <- solidity' src
-  let Just (sol, _, _) = readJSON json
+  let (sol, _, _) = fromJust $ readJSON json
   return (sol ^? ix (path <> ":" <> contract) . creationCode)
 
 solcRuntime :: Text -> Text -> IO (Maybe ByteString)
 solcRuntime contract src = do
   (json, path) <- solidity' src
-  let Just (sol, _, _) = readJSON json
+  let (sol, _, _) = fromJust $ readJSON json
   return (sol ^? ix (path <> ":" <> contract) . runtimeCode)
 
 functionAbi :: Text -> IO Method
 functionAbi f = do
   (json, path) <- solidity' ("contract ABI { function " <> f <> " public {}}")
-  let Just (sol, _, _) = readJSON json
+  let (sol, _, _) = fromJust $ readJSON json
   case Map.toList $ sol ^?! ix (path <> ":ABI") . abiMap of
      [(_,b)] -> return b
      _ -> error "hevm internal error: unexpected abi format"
@@ -347,11 +351,11 @@
 -- deprecate me soon
 readCombinedJSON :: Text -> Maybe (Map Text SolcContract, Map Text Value, [(Text, Maybe ByteString)])
 readCombinedJSON json = do
-  contracts <- f <$> (json ^? key "contracts" . _Object)
+  contracts <- f . KeyMap.toHashMapText <$> (json ^? key "contracts" . _Object)
   sources <- toList . fmap (view _String) <$> json ^? key "sourceList" . _Array
   return (contracts, Map.fromList (HMap.toList asts), [ (x, Nothing) | x <- sources])
   where
-    asts = fromMaybe (error "JSON lacks abstract syntax trees.") (json ^? key "sources" . _Object)
+    asts = KeyMap.toHashMapText $ fromMaybe (error "JSON lacks abstract syntax trees.") (json ^? key "sources" . _Object)
     f x = Map.fromList . HMap.toList $ HMap.mapWithKey g x
     g s x =
       let
@@ -378,9 +382,9 @@
 
 readStdJSON :: Text -> Maybe (Map Text SolcContract, Map Text Value, [(Text, Maybe ByteString)])
 readStdJSON json = do
-  contracts <- json ^? key "contracts" ._Object
+  contracts <- KeyMap.toHashMapText <$> json ^? key "contracts" ._Object
   -- TODO: support the general case of "urls" and "content" in the standard json
-  sources <- json ^? key "sources" . _Object
+  sources <- KeyMap.toHashMapText <$>  json ^? key "sources" . _Object
   let asts = force "JSON lacks abstract syntax trees." . preview (key "ast") <$> sources
       contractMap = f contracts
       contents src = (src, encodeUtf8 <$> HMap.lookup src (mconcat $ Map.elems $ snd <$> contractMap))
@@ -388,7 +392,7 @@
   where
     f :: (AsValue s) => HMap.HashMap Text s -> (Map Text (SolcContract, (HMap.HashMap Text Text)))
     f x = Map.fromList . (concatMap g) . HMap.toList $ x
-    g (s, x) = h s <$> HMap.toList (view _Object x)
+    g (s, x) = h s <$> HMap.toList (KeyMap.toHashMapText (view _Object x))
     h :: Text -> (Text, Value) -> (Text, (SolcContract, HMap.HashMap Text Text))
     h s (c, x) =
       let
@@ -399,7 +403,7 @@
         theCreationCode = toCode $ fromMaybe "" $ creation ^? key "object" . _String
         srcContents :: Maybe (HMap.HashMap Text Text)
         srcContents = do metadata <- x ^? key "metadata" . _String
-                         srcs <- metadata ^? key "sources" . _Object
+                         srcs <- KeyMap.toHashMapText <$> metadata ^? key "sources" . _Object
                          return $ (view (key "content" . _String)) <$> (HMap.filter (isJust . preview (key "content")) srcs)
         abis = force ("abi key not found in " <> show x) $
           toList <$> x ^? key "abi" . _Array
@@ -498,7 +502,7 @@
     do name <- item ^? key "label" . _String
        offset <- item ^? key "offset" . _Number >>= toBoundedInteger
        slot <- item ^? key "slot" . _String
-       typ <- item ^? key "type" . _String
+       typ <- Key.fromText <$> item ^? key "type" . _String
        slotType <- types ^?! key typ ^? key "label" . _String
        return (name, StorageItem (read $ Text.unpack slotType) offset (read $ Text.unpack slot)))
 
@@ -688,7 +692,7 @@
     candidates = (flip Data.List.isInfixOf concretes) <$> bzzrs
   in case elemIndex True candidates of
     Nothing -> b
-    Just i -> let Just ind = infixIndex (bzzrs !! i) concretes
+    Just i -> let ind = fromJust $ infixIndex (bzzrs !! i) concretes
               in take ind b
 
 infixIndex :: (Eq a) => [a] -> [a] -> Maybe Int
diff --git a/src/EVM/SymExec.hs b/src/EVM/SymExec.hs
--- a/src/EVM/SymExec.hs
+++ b/src/EVM/SymExec.hs
@@ -173,7 +173,7 @@
               ConcreteS -> ConcreteStore mempty
     caller' = Caller 0
     value' = CallValue 0
-    code' = RuntimeCode $ fromJust $ Expr.toList (ConcreteBuf contractCode)
+    code' = RuntimeCode (ConcreteRuntimeCode contractCode)
     vm' = loadSymVM code' store caller' value' calldata' calldataProps
     precond = case maybepre of
                 Nothing -> []
@@ -346,14 +346,14 @@
     Nothing -> error "Internal Error: vm in intermediate state after call to runFully"
     Just (VMSuccess buf) -> Return asserts buf (view (env . EVM.storage) vm)
     Just (VMFailure e) -> case e of
-      UnrecognizedOpcode _ -> Invalid asserts
-      SelfDestruction -> SelfDestruct asserts
-      EVM.StackLimitExceeded -> EVM.Types.StackLimitExceeded asserts
-      EVM.IllegalOverflow -> EVM.Types.IllegalOverflow asserts
+      UnrecognizedOpcode _ -> Failure asserts Invalid
+      SelfDestruction -> Failure asserts SelfDestruct
+      EVM.StackLimitExceeded -> Failure asserts EVM.Types.StackLimitExceeded
+      EVM.IllegalOverflow -> Failure asserts EVM.Types.IllegalOverflow
       EVM.Revert buf -> EVM.Types.Revert asserts buf
-      EVM.InvalidMemoryAccess -> EVM.Types.InvalidMemoryAccess asserts
-      EVM.BadJumpDestination -> EVM.Types.BadJumpDestination asserts
-      e' -> EVM.Types.TmpErr asserts $ show e'
+      EVM.InvalidMemoryAccess -> Failure asserts EVM.Types.InvalidMemoryAccess
+      EVM.BadJumpDestination -> Failure asserts EVM.Types.BadJumpDestination
+      e' -> Failure asserts $ EVM.Types.TmpErr (show e')
 
 -- | Converts a given top level expr into a list of final states and the associated path conditions for each state
 flattenExpr :: Expr End -> [([Prop], Expr End)]
@@ -362,15 +362,10 @@
     go :: [Prop] -> Expr End -> [([Prop], Expr End)]
     go pcs = \case
       ITE c t f -> go (PNeg ((PEq c (Lit 0))) : pcs) t <> go (PEq c (Lit 0) : pcs) f
-      e@(Invalid _)  -> [(pcs, e)]
-      e@(SelfDestruct _) -> [(pcs, e)]
       e@(Revert _ _) -> [(pcs, e)]
       e@(Return _ _ _) -> [(pcs, e)]
-      e@(EVM.Types.IllegalOverflow _) -> [(pcs, e)]
-      e@(EVM.Types.StackLimitExceeded _ ) -> [(pcs, e)]
-      e@(EVM.Types.InvalidMemoryAccess _) -> [(pcs, e)]
-      e@(EVM.Types.BadJumpDestination _) -> [(pcs, e)]
-      TmpErr _ s -> error s
+      Failure _ (TmpErr s) -> error s
+      e@(Failure _ _) -> [(pcs, e)]
       GVar _ -> error "cannot flatten an Expr containing a GVar"
 
 -- | Strips unreachable branches from a given expr
@@ -413,6 +408,7 @@
           Unsat -> pure ([query], Nothing)
           r -> error $ "Invalid solver result: " <> show r
 
+
 -- | Evaluate the provided proposition down to its most concrete result
 evalProp :: Prop -> Prop
 evalProp = \case
@@ -450,15 +446,9 @@
 extractProps :: Expr End -> [Prop]
 extractProps = \case
   ITE _ _ _ -> []
-  Invalid asserts -> asserts
-  SelfDestruct asserts -> asserts
   Revert asserts _ -> asserts
   Return asserts _ _ -> asserts
-  EVM.Types.IllegalOverflow asserts -> asserts
-  EVM.Types.StackLimitExceeded asserts -> asserts
-  EVM.Types.InvalidMemoryAccess asserts -> asserts
-  EVM.Types.BadJumpDestination asserts -> asserts
-  TmpErr asserts _ -> asserts
+  Failure asserts _ -> asserts
   GVar _ -> error "cannot extract props from a GVar"
 
 
@@ -538,14 +528,13 @@
             (Revert _ a, Revert _ b) -> if a==b then PBool False else a ./= b
             (Revert _ _, _) -> PBool True
             (_, Revert _ _) -> PBool True
-            (Invalid _, Invalid _) -> PBool False
-            (Invalid _, _ ) -> PBool True
-            (_, Invalid _) -> PBool True
-            (EVM.Types.StackLimitExceeded _, EVM.Types.StackLimitExceeded _ ) -> PBool False
-            (EVM.Types.StackLimitExceeded _, _) -> PBool True
-            (_, EVM.Types.StackLimitExceeded _) -> PBool True
-            (a, b) -> if a == b then PBool False
-                                else error $ "Unimplemented, see TODO about EVM failures and TmpExpr. Left: " <> show a <> " Right: " <> show b
+            (Failure _ erra, Failure _ errb) -> if erra==errb then PBool False else PBool True
+            (GVar _, _) -> error "Expressions cannot contain global vars"
+            (_ , GVar _) -> error "Expressions cannot contain global vars"
+            (Failure _ (TmpErr s), _) -> error $ "Unhandled error: " <> s
+            (_, Failure _ (TmpErr s)) -> error $ "Unhandled error: " <> s
+            (ITE _ _ _, _ ) -> error "Expressions must be flattened"
+            (_, ITE _ _ _) -> error "Expressions must be flattened"
 
         -- if the SMT solver can find a common input that satisfies BOTH sets of path conditions
         -- AND the output differs, then we are in trouble. We do this for _every_ pair of paths, which
diff --git a/src/EVM/TTY.hs b/src/EVM/TTY.hs
--- a/src/EVM/TTY.hs
+++ b/src/EVM/TTY.hs
@@ -41,7 +41,7 @@
 
 import Data.Aeson.Lens
 import Data.ByteString (ByteString)
-import Data.Maybe (isJust, fromJust, fromMaybe)
+import Data.Maybe (isJust, fromJust, fromMaybe, isNothing)
 import Data.Map (Map, insert, lookupLT, singleton, filter)
 import Data.Text (Text, pack)
 import Data.Text.Encoding (decodeUtf8)
@@ -184,7 +184,7 @@
 
         -- Stepper wants to make a query and wait for the results?
         Stepper.IOAct q -> do
-          zoom uiVm (StateT (runStateT q)) >>= interpret mode . k
+          Brick.zoom uiVm (StateT (runStateT q)) >>= interpret mode . k
 
         -- Stepper wants to modify the VM.
         Stepper.EVM m -> do
@@ -317,13 +317,13 @@
      ,?maxIter :: Maybe Integer)
   => UiVmState
   -> StepMode
-  -> EventM n (Next UiState)
+  -> EventM n UiState ()
 takeStep ui mode =
   liftIO nxt >>= \case
-    (Stopped (), ui') ->
-      continue (ViewVm ui')
-    (Continue steps, ui') -> do
-      continue (ViewVm (ui' & set uiStepper steps))
+    (Stopped (), _) ->
+      pure ()
+    (Continue steps, ui') ->
+      put (ViewVm (ui' & set uiStepper steps))
   where
     m = interpret mode (view uiStepper ui)
     nxt = runStateT m ui
@@ -331,128 +331,140 @@
 backstepUntil
   :: (?fetcher :: Fetcher
      ,?maxIter :: Maybe Integer)
-  => (UiVmState -> Pred VM) -> UiVmState -> EventM n (Next UiState)
-backstepUntil p s =
-  case view uiStep s of
-    0 -> continue (ViewVm s)
-    n -> do
-      s1 <- backstep s
-      let
-        -- find a previous vm that satisfies the predicate
-        snapshots' = Data.Map.filter (p s1 . fst) (view uiSnapshots s1)
-      case lookupLT n snapshots' of
-        -- If no such vm exists, go to the beginning
-        Nothing ->
-          let
-            (step', (vm', stepper')) = fromJust $ lookupLT (n - 1) (view uiSnapshots s)
-            s2 = s1
-              & set uiVm vm'
-              & set (uiVm . cache) (view (uiVm . cache) s1)
-              & set uiStep step'
-              & set uiStepper stepper'
-          in takeStep s2 (Step 0)
-        -- step until the predicate doesn't hold
-        Just (step', (vm', stepper')) ->
-          let
-            s2 = s1
-              & set uiVm vm'
-              & set (uiVm . cache) (view (uiVm . cache) s1)
-              & set uiStep step'
-              & set uiStepper stepper'
-          in takeStep s2 (StepUntil (not . p s1))
+  => (UiVmState -> Pred VM) -> EventM n UiState ()
+backstepUntil p = get >>= \case
+  ViewVm s ->
+    case view uiStep s of
+      0 -> pure ()
+      n -> do
+        s1 <- liftIO $ backstep s
+        let
+          -- find a previous vm that satisfies the predicate
+          snapshots' = Data.Map.filter (p s1 . fst) (view uiSnapshots s1)
+        case lookupLT n snapshots' of
+          -- If no such vm exists, go to the beginning
+          Nothing ->
+            let
+              (step', (vm', stepper')) = fromJust $ lookupLT (n - 1) (view uiSnapshots s)
+              s2 = s1
+                & set uiVm vm'
+                & set (uiVm . cache) (view (uiVm . cache) s1)
+                & set uiStep step'
+                & set uiStepper stepper'
+            in takeStep s2 (Step 0)
+          -- step until the predicate doesn't hold
+          Just (step', (vm', stepper')) ->
+            let
+              s2 = s1
+                & set uiVm vm'
+                & set (uiVm . cache) (view (uiVm . cache) s1)
+                & set uiStep step'
+                & set uiStepper stepper'
+            in takeStep s2 (StepUntil (not . p s1))
+  _ -> pure ()
 
 backstep
   :: (?fetcher :: Fetcher
      ,?maxIter :: Maybe Integer)
-  => UiVmState -> EventM n UiVmState
-backstep s = case view uiStep s of
-  -- We're already at the first step; ignore command.
-  0 -> return s
-  -- To step backwards, we revert to the previous snapshot
-  -- and execute n - 1 `mod` snapshotInterval steps from there.
+  => UiVmState -> IO UiVmState
+backstep s =
+  case view uiStep s of
+    -- We're already at the first step; ignore command.
+    0 -> pure s
+    -- To step backwards, we revert to the previous snapshot
+    -- and execute n - 1 `mod` snapshotInterval steps from there.
 
-  -- We keep the current cache so we don't have to redo
-  -- any blocking queries, and also the memory view.
-  n ->
-    let
-      (step, (vm, stepper)) = fromJust $ lookupLT n (view uiSnapshots s)
-      s1 = s
-        & set uiVm vm
-        & set (uiVm . cache) (view (uiVm . cache) s)
-        & set uiStep step
-        & set uiStepper stepper
-      stepsToTake = n - step - 1
+    -- We keep the current cache so we don't have to redo
+    -- any blocking queries, and also the memory view.
+    n ->
+      let
+        (step, (vm, stepper)) = fromJust $ lookupLT n (view uiSnapshots s)
+        s1 = s
+          & set uiVm vm
+          & set (uiVm . cache) (view (uiVm . cache) s)
+          & set uiStep step
+          & set uiStepper stepper
+        stepsToTake = n - step - 1
 
-    in
-      liftIO $ runStateT (interpret (Step stepsToTake) stepper) s1 >>= \case
-        (Continue steps, ui') -> return $ ui' & set uiStepper steps
-        _ -> error "unexpected end"
+      in
+        runStateT (interpret (Step stepsToTake) stepper) s1 >>= \case
+          (Continue steps, ui') -> pure $ ui' & set uiStepper steps
+          _ -> error "unexpected end"
 
 appEvent
   :: (?fetcher::Fetcher, ?maxIter :: Maybe Integer) =>
-  UiState ->
   BrickEvent Name e ->
-  EventM Name (Next UiState)
+  EventM Name UiState ()
 
 -- Contracts: Down - list down
-appEvent (ViewContracts s) (VtyEvent e@(V.EvKey V.KDown [])) = do
-  s' <- handleEventLensed s
-    browserContractList
-    handleListEvent
-    e
-  continue (ViewContracts s')
+appEvent (VtyEvent e@(V.EvKey V.KDown [])) = get >>= \case
+  ViewContracts _s -> do
+    Brick.zoom
+      (_ViewContracts . browserContractList)
+      (handleListEvent e)
+    pure ()
+  _ -> pure ()
 
 -- Contracts: Up - list up
-appEvent (ViewContracts s) (VtyEvent e@(V.EvKey V.KUp [])) = do
-  s' <- handleEventLensed s
-    browserContractList
-    handleListEvent
-    e
-  continue (ViewContracts s')
+-- Page: Up - scroll
+appEvent (VtyEvent e@(V.EvKey V.KUp [])) = get >>= \case
+  ViewContracts _s -> do
+    Brick.zoom
+      (_ViewContracts . browserContractList)
+      (handleListEvent e)
+  _ -> pure ()
 
 -- Vm Overview: Esc - return to test picker or exit
-appEvent st@(ViewVm s) (VtyEvent (V.EvKey V.KEsc [])) =
-  let opts = view uiTestOpts s
-      dapp' = dapp (view uiTestOpts s)
-      tests = concatMap
-                (debuggableTests opts)
-                (view dappUnitTests dapp')
-  in case tests of
-    [] -> halt st
-    ts ->
-      continue . ViewPicker $
-      UiTestPickerState
-        { _testPickerList =
-            list
-              TestPickerPane
-              (Vec.fromList
-              ts)
-              1
-        , _testPickerDapp = dapp'
-        , _testOpts = opts
-        }
+-- Any: Esc - return to Vm Overview or Exit
+appEvent (VtyEvent (V.EvKey V.KEsc [])) = get >>= \case
+  ViewVm s -> do
+    let opts = s ^. uiTestOpts
+        dapp' = dapp opts
+        tests = concatMap (debuggableTests opts) (dapp' ^. dappUnitTests)
+    case tests of
+      [] -> halt
+      ts ->
+        put $ ViewPicker $ UiTestPickerState
+          { _testPickerList = list TestPickerPane (Vec.fromList ts) 1
+          , _testPickerDapp = dapp'
+          , _testOpts = opts
+          }
+  ViewHelp s -> put (ViewVm s)
+  ViewContracts s -> put (ViewVm $ s ^. browserVm)
+  _ -> halt
 
 -- Vm Overview: Enter - open contracts view
-appEvent (ViewVm s) (VtyEvent (V.EvKey V.KEnter [])) =
-  continue . ViewContracts $ UiBrowserState
-    { _browserContractList =
-        list
-          BrowserPane
-          (Vec.fromList (Map.toList (view (uiVm . env . contracts) s)))
-          2
-    , _browserVm = s
-    }
+-- UnitTest Picker: Enter - select from list
+appEvent (VtyEvent (V.EvKey V.KEnter [])) = get >>= \case
+  ViewVm s ->
+    put . ViewContracts $ UiBrowserState
+      { _browserContractList =
+          list
+            BrowserPane
+            (Vec.fromList (Map.toList (view (uiVm . env . contracts) s)))
+            2
+      , _browserVm = s
+      }
+  ViewPicker s ->
+    case listSelectedElement (view testPickerList s) of
+      Nothing -> error "nothing selected"
+      Just (_, x) -> do
+        let initVm  = initialUiVmStateForTest (view testOpts s) x
+        put (ViewVm initVm)
+  _ -> pure ()
 
 -- Vm Overview: m - toggle memory pane
-appEvent (ViewVm s) (VtyEvent (V.EvKey (V.KChar 'm') [])) =
-  continue (ViewVm (over uiShowMemory not s))
+appEvent (VtyEvent (V.EvKey (V.KChar 'm') [])) = get >>= \case
+  ViewVm s -> put (ViewVm $ over uiShowMemory not s)
+  _ -> pure ()
 
 -- Vm Overview: h - open help view
-appEvent (ViewVm s) (VtyEvent (V.EvKey (V.KChar 'h') []))
-  = continue . ViewHelp $ s
+appEvent (VtyEvent (V.EvKey (V.KChar 'h') [])) = get >>= \case
+  ViewVm s -> put (ViewHelp s)
+  _ -> pure ()
 
 -- Vm Overview: spacebar - read input
-appEvent (ViewVm s) (VtyEvent (V.EvKey (V.KChar ' ') [])) =
+appEvent (VtyEvent (V.EvKey (V.KChar ' ') [])) =
   let
     loop = do
       Readline.getInputLine "% " >>= \case
@@ -461,153 +473,126 @@
       Readline.getInputLine "% " >>= \case
         Just hey' -> Readline.outputStrLn hey'
         Nothing   -> pure ()
-      return (ViewVm s)
-  in
-    suspendAndResume $
+   in do
+    s <- get
+    suspendAndResume $ do
       Readline.runInputT Readline.defaultSettings loop
+      pure s
 
 -- todo refactor to zipper step forward
 -- Vm Overview: n - step
-appEvent (ViewVm s) (VtyEvent (V.EvKey (V.KChar 'n') [])) =
-  if isJust $ view (uiVm . result) s
-  then continue (ViewVm s)
-  else takeStep s (Step 1)
+appEvent (VtyEvent (V.EvKey (V.KChar 'n') [])) = get >>= \case
+  ViewVm s ->
+    when (isNothing (s ^. uiVm . result)) $
+      takeStep s (Step 1)
+  _ -> pure ()
 
 -- Vm Overview: N - step
-appEvent (ViewVm s) (VtyEvent (V.EvKey (V.KChar 'N') [])) =
-  if isJust $ view (uiVm . result) s
-  then continue (ViewVm s)
-  else takeStep s
-       (StepUntil (isNextSourcePosition s))
+appEvent (VtyEvent (V.EvKey (V.KChar 'N') [])) = get >>= \case
+  ViewVm s ->
+    when (isNothing (s ^. uiVm . result)) $
+      takeStep s (StepUntil (isNextSourcePosition s))
+  _ -> pure ()
 
 -- Vm Overview: C-n - step
-appEvent (ViewVm s) (VtyEvent (V.EvKey (V.KChar 'n') [V.MCtrl])) =
-  if isJust $ view (uiVm . result) s
-  then continue (ViewVm s)
-  else takeStep s
-    (StepUntil (isNextSourcePositionWithoutEntering s))
+appEvent (VtyEvent (V.EvKey (V.KChar 'n') [V.MCtrl])) = get >>= \case
+  ViewVm s ->
+    when (isNothing (s ^. uiVm . result)) $
+      takeStep s (StepUntil (isNextSourcePositionWithoutEntering s))
+  _ -> pure ()
 
 -- Vm Overview: e - step
-appEvent (ViewVm s) (VtyEvent (V.EvKey (V.KChar 'e') [])) =
-  if isJust $ view (uiVm . result) s
-  then continue (ViewVm s)
-  else takeStep s
-    (StepUntil (isExecutionHalted s))
+appEvent (VtyEvent (V.EvKey (V.KChar 'e') [])) = get >>= \case
+  ViewVm s ->
+    when (isNothing (s ^. uiVm . result)) $
+      takeStep s (StepUntil (isExecutionHalted s))
+  _ -> pure ()
 
 -- Vm Overview: a - step
-appEvent (ViewVm s) (VtyEvent (V.EvKey (V.KChar 'a') [])) =
-      -- We keep the current cache so we don't have to redo
-      -- any blocking queries.
-      let
-        (vm, stepper) = fromJust (Map.lookup 0 (view uiSnapshots s))
-        s' = s
-          & set uiVm vm
-          & set (uiVm . cache) (view (uiVm . cache) s)
-          & set uiStep 0
-          & set uiStepper stepper
+appEvent (VtyEvent (V.EvKey (V.KChar 'a') [])) = get >>= \case
+  ViewVm s ->
+    -- We keep the current cache so we don't have to redo
+    -- any blocking queries.
+    let
+      (vm, stepper) = fromJust (Map.lookup 0 (view uiSnapshots s))
+      s' = s
+        & set uiVm vm
+        & set (uiVm . cache) (view (uiVm . cache) s)
+        & set uiStep 0
+        & set uiStepper stepper
 
-      in takeStep s' (Step 0)
+    in takeStep s' (Step 0)
+  _ -> pure ()
 
 -- Vm Overview: p - backstep
-appEvent st@(ViewVm s) (VtyEvent (V.EvKey (V.KChar 'p') [])) =
-  case view uiStep s of
-    0 ->
-      -- We're already at the first step; ignore command.
-      continue st
-    n -> do
-      -- To step backwards, we revert to the previous snapshot
-      -- and execute n - 1 `mod` snapshotInterval steps from there.
+appEvent (VtyEvent (V.EvKey (V.KChar 'p') [])) = get >>= \case
+  ViewVm s ->
+    case view uiStep s of
+      0 ->
+        -- We're already at the first step; ignore command.
+        pure ()
+      n -> do
+        -- To step backwards, we revert to the previous snapshot
+        -- and execute n - 1 `mod` snapshotInterval steps from there.
 
-      -- We keep the current cache so we don't have to redo
-      -- any blocking queries, and also the memory view.
-      let
-        (step, (vm, stepper)) = fromJust $ lookupLT n (view uiSnapshots s)
-        s1 = s
-          & set uiVm vm -- set the vm to the one from the snapshot
-          & set (uiVm . cache) (view (uiVm . cache) s) -- persist the cache
-          & set uiStep step
-          & set uiStepper stepper
-        stepsToTake = n - step - 1
+        -- We keep the current cache so we don't have to redo
+        -- any blocking queries, and also the memory view.
+        let
+          (step, (vm, stepper)) = fromJust $ lookupLT n (view uiSnapshots s)
+          s1 = s
+            & set uiVm vm -- set the vm to the one from the snapshot
+            & set (uiVm . cache) (view (uiVm . cache) s) -- persist the cache
+            & set uiStep step
+            & set uiStepper stepper
+          stepsToTake = n - step - 1
 
-      takeStep s1 (Step stepsToTake)
+        takeStep s1 (Step stepsToTake)
+  _ -> pure ()
 
 -- Vm Overview: P - backstep to previous source
-appEvent (ViewVm s) (VtyEvent (V.EvKey (V.KChar 'P') [])) =
-  backstepUntil isNextSourcePosition s
+appEvent (VtyEvent (V.EvKey (V.KChar 'P') [])) =
+  backstepUntil isNextSourcePosition
 
 -- Vm Overview: c-p - backstep to previous source avoiding CALL and CREATE
-appEvent (ViewVm s) (VtyEvent (V.EvKey (V.KChar 'p') [V.MCtrl])) =
-  backstepUntil isNextSourcePositionWithoutEntering s
+appEvent (VtyEvent (V.EvKey (V.KChar 'p') [V.MCtrl])) =
+  backstepUntil isNextSourcePositionWithoutEntering
 
 -- Vm Overview: 0 - choose no jump
-appEvent (ViewVm s) (VtyEvent (V.EvKey (V.KChar '0') [])) =
-  case view (uiVm . result) s of
-    Just (VMFailure (Choose (PleaseChoosePath _ contin))) ->
-      takeStep (s & set uiStepper (Stepper.evm (contin True) >> (view uiStepper s)))
-        (Step 1)
-    _ -> continue (ViewVm s)
+appEvent (VtyEvent (V.EvKey (V.KChar '0') [])) = get >>= \case
+  ViewVm s ->
+    case view (uiVm . result) s of
+      Just (VMFailure (Choose (PleaseChoosePath _ contin))) ->
+        takeStep (s & set uiStepper (Stepper.evm (contin True) >> (view uiStepper s)))
+          (Step 1)
+      _ -> pure ()
+  _ -> pure ()
 
 -- Vm Overview: 1 - choose jump
-appEvent (ViewVm s) (VtyEvent (V.EvKey (V.KChar '1') [])) =
-  case view (uiVm . result) s of
-    Just (VMFailure (Choose (PleaseChoosePath _ contin))) ->
-      takeStep (s & set uiStepper (Stepper.evm (contin False) >> (view uiStepper s)))
-        (Step 1)
-    _ -> continue (ViewVm s)
-
-
--- Any: Esc - return to Vm Overview or Exit
-appEvent s (VtyEvent (V.EvKey V.KEsc [])) =
-  case s of
-    (ViewHelp x) -> overview x
-    (ViewContracts x) -> overview $ view browserVm x
-    _ -> halt s
-  where
-    overview = continue . ViewVm
-
--- UnitTest Picker: Enter - select from list
-appEvent (ViewPicker s) (VtyEvent (V.EvKey V.KEnter [])) =
-  case listSelectedElement (view testPickerList s) of
-    Nothing -> error "nothing selected"
-    Just (_, x) -> do
-      let initVm  = initialUiVmStateForTest (view testOpts s) x
-      continue . ViewVm $ initVm
-
--- UnitTest Picker: (main) - render list
-appEvent (ViewPicker s) (VtyEvent e) = do
-  s' <- handleEventLensed s
-    testPickerList
-    handleListEvent
-    e
-  continue (ViewPicker s')
-
--- Page: Down - scroll
-appEvent (ViewVm s) (VtyEvent (V.EvKey V.KDown [])) =
-  if view uiShowMemory s then
-    vScrollBy (viewportScroll TracePane) 1 >> continue (ViewVm s)
-  else
-    if isJust $ view (uiVm . result) s
-    then continue (ViewVm s)
-    else takeStep s
-         (StepUntil (isNewTraceAdded s))
-
--- Page: Up - scroll
-appEvent (ViewVm s) (VtyEvent (V.EvKey V.KUp [])) =
-  if view uiShowMemory s then
-    vScrollBy (viewportScroll TracePane) (-1) >> continue (ViewVm s)
-  else
-    backstepUntil isNewTraceAdded s
+appEvent (VtyEvent (V.EvKey (V.KChar '1') [])) = get >>= \case
+  ViewVm s ->
+    case view (uiVm . result) s of
+      Just (VMFailure (Choose (PleaseChoosePath _ contin))) ->
+        takeStep (s & set uiStepper (Stepper.evm (contin False) >> (view uiStepper s)))
+          (Step 1)
+      _ -> pure ()
+  _ -> pure ()
 
 -- Page: C-f - Page down
-appEvent s (VtyEvent (V.EvKey (V.KChar 'f') [V.MCtrl])) =
-  vScrollPage (viewportScroll TracePane) Down >> continue s
+appEvent (VtyEvent (V.EvKey (V.KChar 'f') [V.MCtrl])) =
+  vScrollPage (viewportScroll TracePane) Down
 
 -- Page: C-b - Page up
-appEvent s (VtyEvent (V.EvKey (V.KChar 'b') [V.MCtrl])) =
-  vScrollPage (viewportScroll TracePane) Up >> continue s
+appEvent (VtyEvent (V.EvKey (V.KChar 'b') [V.MCtrl])) =
+  vScrollPage (viewportScroll TracePane) Up
 
+-- UnitTest Picker: (main) - render list
+appEvent (VtyEvent e) = do
+  Brick.zoom
+    (_ViewPicker . testPickerList)
+    (handleListEvent e)
+
 -- Default
-appEvent s _ = continue s
+appEvent _ = pure ()
 
 app :: UnitTestOptions -> App UiState () Name
 app UnitTestOptions{..} =
@@ -617,7 +602,7 @@
   { appDraw = drawUi
   , appChooseCursor = neverShowCursor
   , appHandleEvent = appEvent
-  , appStartEvent = return
+  , appStartEvent = pure ()
   , appAttrMap = const (attrMap V.defAttr myTheme)
   }
 
@@ -630,9 +615,8 @@
     cd = case test of
       SymbolicTest _ -> symCalldata theTestName types [] (AbstractBuf "txdata")
       _ -> (error "unreachable", error "unreachable")
-    Just (test, types) = find (\(test',_) -> extractSig test' == theTestName) $ unitTestMethods testContract
-    Just testContract =
-      view (dappSolcByName . at theContractName) dapp
+    (test, types) = fromJust $ find (\(test',_) -> extractSig test' == theTestName) $ unitTestMethods testContract
+    testContract = fromJust $ view (dappSolcByName . at theContractName) dapp
     vm0 =
       initialUnitTestVm opts testContract
     script = do
@@ -763,7 +747,7 @@
   ]
   where
     dapp' = dapp (view (browserVm . uiTestOpts) ui)
-    Just (_, (_, c)) = listSelectedElement (view browserContractList ui)
+    (_, (_, c)) = fromJust $ listSelectedElement (view browserContractList ui)
 --        currentContract  = view (dappSolcByHash . ix ) dapp
     maybeHash ch = fromJust (error "Internal error: cannot find concrete codehash for partially symbolic code") (maybeLitWord (view codehash ch))
 
@@ -1051,8 +1035,8 @@
 opWidget :: (Integral a, Show a) => (a, Op) -> Widget n
 opWidget = txt . pack . opString
 
-selectedAttr :: AttrName; selectedAttr = "selected"
-dimAttr :: AttrName; dimAttr = "dim"
-wordAttr :: AttrName; wordAttr = "word"
-boldAttr :: AttrName; boldAttr = "bold"
-activeAttr :: AttrName; activeAttr = "active"
+selectedAttr :: AttrName; selectedAttr = attrName "selected"
+dimAttr :: AttrName; dimAttr = attrName "dim"
+wordAttr :: AttrName; wordAttr = attrName "word"
+boldAttr :: AttrName; boldAttr = attrName "bold"
+activeAttr :: AttrName; activeAttr = attrName "active"
diff --git a/src/EVM/Transaction.hs b/src/EVM/Transaction.hs
--- a/src/EVM/Transaction.hs
+++ b/src/EVM/Transaction.hs
@@ -15,7 +15,7 @@
 import Data.Aeson (FromJSON (..))
 import Data.ByteString (ByteString)
 import Data.Map (Map)
-import Data.Maybe (fromMaybe, isNothing)
+import Data.Maybe (fromMaybe, isNothing, fromJust)
 
 import qualified Data.Aeson        as JSON
 import qualified Data.Aeson.Types  as JSON
@@ -78,9 +78,9 @@
         to'        = case txToAddr tx of
           Just a  -> BS $ word160Bytes a
           Nothing -> BS mempty
-        Just maxFee = txMaxFeePerGas tx
-        Just maxPrio = txMaxPriorityFeeGas tx
-        Just gasPrice = txGasPrice tx
+        maxFee = fromJust $ txMaxFeePerGas tx
+        maxPrio = fromJust $ txMaxPriorityFeeGas tx
+        gasPrice = fromJust $ txGasPrice tx
         accessList = txAccessList tx
         rlpAccessList = EVM.RLP.List $ map (\accessEntry ->
           EVM.RLP.List [BS $ word160Bytes (accessAddress accessEntry),
@@ -163,7 +163,7 @@
     toAddr   <- addrFieldMaybe val "to"
     v        <- wordField val "v"
     value    <- wordField val "value"
-    txType   <- fmap read <$> (val JSON..:? "type")
+    txType   <- fmap (read :: String -> Int) <$> (val JSON..:? "type")
     case txType of
       Just 0x00 -> return $ Transaction tdata gasLimit gasPrice nonce r s toAddr v value LegacyTransaction [] Nothing Nothing
       Just 0x01 -> do
@@ -184,7 +184,7 @@
 touchAccount a = Map.insertWith (flip const) a newAccount
 
 newAccount :: EVM.Contract
-newAccount = initialContract $ EVM.RuntimeCode mempty
+newAccount = initialContract $ EVM.RuntimeCode (EVM.ConcreteRuntimeCode "")
 
 -- | Increments origin nonce and pays gas deposit
 setupTx :: Addr -> Addr -> W256 -> Word64 -> Map Addr EVM.Contract -> Map Addr EVM.Contract
diff --git a/src/EVM/Traversals.hs b/src/EVM/Traversals.hs
--- a/src/EVM/Traversals.hs
+++ b/src/EVM/Traversals.hs
@@ -66,16 +66,10 @@
 
       -- control flow
 
-      e@(Invalid a) -> f e <> (foldl (foldProp f) mempty a)
-      e@(StackLimitExceeded a) -> f e <> (foldl (foldProp f) mempty a)
-      e@(InvalidMemoryAccess a) -> f e <> (foldl (foldProp f) mempty a)
-      e@(BadJumpDestination a) -> f e <> (foldl (foldProp f) mempty a)
-      e@(SelfDestruct a) -> f e <> (foldl (foldProp f) mempty a)
-      e@(IllegalOverflow a) -> f e <> (foldl (foldProp f) mempty a)
       e@(Revert a b) -> f e <> (foldl (foldProp f) mempty a) <> (go b)
       e@(Return a b c) -> f e <> (foldl (foldProp f) mempty a) <> (go b) <> (go c)
       e@(ITE a b c) -> f e <> (go a) <> (go b) <> (go c)
-      e@(TmpErr a _) -> f e <> (foldl (foldProp f) mempty a)
+      e@(Failure a _) -> f e <> (foldl (foldProp f) mempty a)
 
       -- integers
 
@@ -314,24 +308,9 @@
 
   -- control flow
 
-  Invalid a -> do
-    a' <- mapM (mapPropM f) a
-    f (Invalid a')
-  SelfDestruct a -> do
-    a' <- mapM (mapPropM f) a
-    f (SelfDestruct a')
-  IllegalOverflow a -> do
-    a' <- mapM (mapPropM f) a
-    f (IllegalOverflow a')
-  InvalidMemoryAccess a -> do
-    a' <- mapM (mapPropM f) a
-    f (InvalidMemoryAccess a')
-  StackLimitExceeded a -> do
-    a' <- mapM (mapPropM f) a
-    f (StackLimitExceeded a')
-  BadJumpDestination a -> do
+  Failure a b -> do
     a' <- mapM (mapPropM f) a
-    f (BadJumpDestination a')
+    f (Failure a' b)
   Revert a b -> do
     a' <- mapM (mapPropM f) a
     b' <- mapExprM f b
@@ -347,10 +326,6 @@
     b' <- mapExprM f b
     c' <- mapExprM f c
     f (ITE a' b' c')
-
-  TmpErr a b -> do
-    a' <- mapM (mapPropM f) a
-    f (TmpErr a' b)
 
   -- integers
 
diff --git a/src/EVM/Types.hs b/src/EVM/Types.hs
--- a/src/EVM/Types.hs
+++ b/src/EVM/Types.hs
@@ -5,6 +5,8 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE DefaultSignatures #-}
 
+{-# OPTIONS_GHC -Wno-error=inline-rule-shadowing #-}
+
 module EVM.Types where
 
 import Prelude hiding  (Word, LT, GT)
@@ -115,6 +117,17 @@
   | End
   deriving (Typeable)
 
+-- EVM errors
+data Error
+  = Invalid
+  | IllegalOverflow
+  | StackLimitExceeded
+  | InvalidMemoryAccess
+  | BadJumpDestination
+  | SelfDestruct
+  | TmpErr String
+  deriving (Show, Eq, Ord)
+
 -- Variables refering to a global environment
 data GVar (a :: EType) where
   BufVar :: Int -> GVar Buf
@@ -152,17 +165,11 @@
                  -> Expr EWord
   -- control flow
 
-  Invalid             :: [Prop] -> Expr End
-  IllegalOverflow     :: [Prop] -> Expr End
-  SelfDestruct        :: [Prop] -> Expr End
-  StackLimitExceeded  :: [Prop] -> Expr End
-  InvalidMemoryAccess :: [Prop] -> Expr End
-  BadJumpDestination  :: [Prop] -> Expr End
   Revert              :: [Prop] -> Expr Buf -> Expr End
+  Failure             :: [Prop] -> Error -> Expr End
   Return              :: [Prop] -> Expr Buf -> Expr Storage -> Expr End
   ITE                 :: Expr EWord -> Expr End -> Expr End -> Expr End
-  TmpErr              :: [Prop] -> String -> Expr End -- TODO this is a crutch to help us not deal with all EVM failure modes in Expr
-                                                      --      should be removed once EVM failure modes are handled in Expr
+
   -- integers
 
   Add            :: Expr EWord -> Expr EWord -> Expr EWord
@@ -657,6 +664,18 @@
 packNibbles [] = mempty
 packNibbles (n1:n2:ns) = BS.singleton (toByte n1 n2) <> packNibbles ns
 packNibbles _ = error "can't pack odd number of nibbles"
+
+toWord64 :: W256 -> Maybe Word64
+toWord64 n =
+  if n <= num (maxBound :: Word64)
+    then let (W256 (Word256 _ (Word128 _ n'))) = n in Just n'
+    else Nothing
+
+toInt :: W256 -> Maybe Int
+toInt n =
+  if n <= num (maxBound :: Int)
+    then let (W256 (Word256 _ (Word128 _ n'))) = n in Just (fromIntegral n')
+    else Nothing
 
 -- Keccak hashing
 
diff --git a/src/EVM/UnitTest.hs b/src/EVM/UnitTest.hs
--- a/src/EVM/UnitTest.hs
+++ b/src/EVM/UnitTest.hs
@@ -17,7 +17,7 @@
 import EVM.Solidity
 import qualified EVM.SymExec as SymExec
 import EVM.SymExec (defaultVeriOpts, symCalldata, verify, isQed, extractCex, runExpr, subModel, VeriOpts)
-import EVM.Types
+import EVM.Types hiding (Failure)
 import EVM.Transaction (initTx)
 import EVM.RLP
 import qualified EVM.Facts     as Facts
@@ -244,7 +244,9 @@
     res <- Stepper.execFully
     case res of
       Right (ConcreteBuf r) ->
-        let AbiBool failed = decodeAbiValue AbiBoolType (BSLazy.fromStrict r)
+        let failed = case decodeAbiValue AbiBoolType (BSLazy.fromStrict r) of
+              AbiBool f -> f
+              _ -> error "fix me with better types"
         in pure (shouldFail == failed)
       c -> error $ "internal error: unexpected failure code: " <> show c
 
@@ -501,7 +503,11 @@
 decodeCalls :: BSLazy.ByteString -> [ExploreTx]
 decodeCalls b = fromMaybe (error "could not decode replay data") $ do
   List v <- rlpdecode $ BSLazy.toStrict b
-  return $ flip fmap v $ \(List [BS caller', BS target, BS cd, BS ts]) -> (num (word caller'), num (word target), cd, word ts)
+  pure $ unList <$> v
+  where
+    unList (List [BS caller', BS target, BS cd, BS ts]) =
+      (num (word caller'), num (word target), cd, word ts)
+    unList _ = error "fix me with better types"
 
 -- | Runs an invariant test, calls the invariant before execution begins
 initialExplorationStepper :: UnitTestOptions -> ABIMethod -> [ExploreTx] -> [Addr] -> Int -> Stepper (Bool, RLP)
@@ -523,7 +529,8 @@
        vm <- get
        let cs = view (env . contracts) vm
            noCode c = case view contractcode c of
-             RuntimeCode c' -> null c'
+             RuntimeCode (ConcreteRuntimeCode "") -> True
+             RuntimeCode (SymbolicRuntimeCode c') -> null c'
              _ -> False
            mutable m = view methodMutability m `elem` [NonPayable, Payable]
            knownAbis :: Map Addr SolcContract
@@ -585,7 +592,7 @@
 getTargetContracts :: UnitTestOptions -> Stepper [Addr]
 getTargetContracts UnitTestOptions{..} = do
   vm <- Stepper.evm get
-  let Just contract' = currentContract vm
+  let contract' = fromJust $ currentContract vm
       theAbi = view abiMap $ fromJust $ lookupCode (view contractcode contract') dapp
       setUp  = abiKeccak (encodeUtf8 "targetContracts()")
   case Map.lookup setUp theAbi of
@@ -595,9 +602,16 @@
       res <- Stepper.execFully
       case res of
         Right (ConcreteBuf r) ->
-          let AbiTuple vs = decodeAbiValue (AbiTupleType (Vector.fromList [AbiArrayDynamicType AbiAddressType])) (BSLazy.fromStrict r)
-              [AbiArrayDynamic AbiAddressType targets] = Vector.toList vs
-          in return $ fmap (\(AbiAddress a) -> a) (Vector.toList targets)
+          let vs = case decodeAbiValue (AbiTupleType (Vector.fromList [AbiArrayDynamicType AbiAddressType])) (BSLazy.fromStrict r) of
+                AbiTuple v -> v
+                _ -> error "fix me with better types"
+              targets = case Vector.toList vs of
+                [AbiArrayDynamic AbiAddressType ts] ->
+                  let unAbiAddress (AbiAddress a) = a
+                      unAbiAddress _ = error "fix me with better types"
+                  in unAbiAddress <$> Vector.toList ts
+                _ -> error "fix me with better types"
+          in pure targets
         _ -> error "internal error: unexpected failure code"
 
 exploreRun :: UnitTestOptions -> VM -> ABIMethod -> [ExploreTx] -> IO (Text, Either Text Text, VM)
@@ -903,7 +917,9 @@
           log_unnamed =
             Just $ showValue (head ts) args
           log_named =
-            let [key, val] = take 2 (textValues ts args)
+            let (key, val) = case take 2 (textValues ts args) of
+                  [k, v] -> (k, v)
+                  _ -> error "shouldn't happen"
             in Just $ unquote key <> ": " <> val
           showDecimal dec val =
             pack $ show $ Decimal (num dec) val
@@ -938,7 +954,7 @@
   constraints %= (<> cdProps)
   assign (state . caller) (litAddr testCaller)
   assign (state . gas) testGasCall
-  origin' <- fromMaybe (initialContract (RuntimeCode mempty)) <$> use (env . contracts . at testOrigin)
+  origin' <- fromMaybe (initialContract (RuntimeCode (ConcreteRuntimeCode ""))) <$> use (env . contracts . at testOrigin)
   let originBal = view balance origin'
   when (originBal < testGasprice * (num testGasCall)) $ error "insufficient balance for gas cost"
   vm <- get
@@ -974,7 +990,7 @@
            , vmoptAllowFFI = ffiAllowed
            }
     creator =
-      initialContract (RuntimeCode mempty)
+      initialContract (RuntimeCode (ConcreteRuntimeCode ""))
         & set nonce 1
         & set balance testBalanceCreate
   in vm
diff --git a/src/EVM/VMTest.hs b/src/EVM/VMTest.hs
deleted file mode 100644
--- a/src/EVM/VMTest.hs
+++ /dev/null
@@ -1,374 +0,0 @@
-{-# Language CPP #-}
-{-# LANGUAGE TupleSections #-}
-
-module EVM.VMTest
-  ( Case
-  , BlockchainCase
-
-  , parseBCSuite
-
-  , initTx
-  , setupTx
-  , vmForCase
-  , checkExpectation
-  ) where
-
-import Prelude hiding (Word)
-
-import qualified EVM
-import EVM (contractcode, storage, origStorage, balance, nonce, initialContract, StorageBase(..))
-import EVM.Expr (litCode, litAddr)
-import qualified EVM.Concrete as EVM
-import qualified EVM.FeeSchedule
-
-import EVM.Transaction
-import EVM.Types
-
-import Control.Arrow ((***), (&&&))
-import Control.Lens
-import Control.Monad
-
-import GHC.Stack
-
-import Data.Aeson ((.:), (.:?), FromJSON (..))
-import Data.Map (Map)
-import Data.Maybe (fromMaybe, isNothing)
-import Data.Witherable (Filterable, catMaybes)
-
-import qualified Data.Map          as Map
-import qualified Data.Aeson        as JSON
-import qualified Data.Aeson.Types  as JSON
-import qualified Data.ByteString.Lazy  as Lazy
-import qualified Data.Vector as V
-import Data.Word (Word64)
-
-type Storage = Map W256 W256
-
-data Which = Pre | Post
-
-data Block = Block
-  { blockCoinbase    :: Addr
-  , blockDifficulty  :: W256
-  , blockGasLimit    :: Word64
-  , blockBaseFee     :: W256
-  , blockNumber      :: W256
-  , blockTimestamp   :: W256
-  , blockTxs         :: [Transaction]
-  } deriving Show
-
-data Case = Case
-  { testVmOpts      :: EVM.VMOpts
-  , checkContracts  :: Map Addr (EVM.Contract, Storage)
-  , testExpectation :: Map Addr (EVM.Contract, Storage)
-  } deriving Show
-
-data BlockchainCase = BlockchainCase
-  { blockchainBlocks  :: [Block]
-  , blockchainPre     :: Map Addr (EVM.Contract, Storage)
-  , blockchainPost    :: Map Addr (EVM.Contract, Storage)
-  , blockchainNetwork :: String
-  } deriving Show
-
-splitEithers :: (Filterable f) => f (Either a b) -> (f a, f b)
-splitEithers =
-  (catMaybes *** catMaybes)
-  . (fmap fst &&& fmap snd)
-  . (fmap (preview _Left &&& preview _Right))
-
-checkStateFail :: Bool -> Case -> EVM.VM -> (Bool, Bool, Bool, Bool, Bool) -> IO Bool
-checkStateFail diff x vm (okState, okMoney, okNonce, okData, okCode) = do
-  let
-    printContracts :: Map Addr (EVM.Contract, Storage) -> IO ()
-    printContracts cs = putStrLn $ Map.foldrWithKey (\k (c, s) acc ->
-      acc ++ show k ++ " : "
-                   ++ (show . toInteger  $ (view nonce c)) ++ " "
-                   ++ (show . toInteger  $ (view balance c)) ++ " "
-                   ++ (printStorage s)
-        ++ "\n") "" cs
-
-    reason = map fst (filter (not . snd)
-        [ ("bad-state",       okMoney || okNonce || okData  || okCode || okState)
-        , ("bad-balance", not okMoney || okNonce || okData  || okCode || okState)
-        , ("bad-nonce",   not okNonce || okMoney || okData  || okCode || okState)
-        , ("bad-storage", not okData  || okMoney || okNonce || okCode || okState)
-        , ("bad-code",    not okCode  || okMoney || okNonce || okData || okState)
-        ])
-    check = checkContracts x
-    expected = testExpectation x
-    actual = Map.map (,mempty) $ view (EVM.env . EVM.contracts) vm -- . to (fmap (clearZeroStorage.clearOrigStorage))) vm
-    printStorage = show -- TODO: fixme
-
-  putStr (unwords reason)
-  when (diff && (not okState)) $ do
-    putStrLn "\nPre balance/state: "
-    printContracts check
-    putStrLn "\nExpected balance/state: "
-    printContracts expected
-    putStrLn "\nActual balance/state: "
-    printContracts actual
-  return okState
-
-checkExpectation :: HasCallStack => Bool -> Case -> EVM.VM -> IO Bool
-checkExpectation diff x vm = do
-  let expectation = testExpectation x
-      (okState, b2, b3, b4, b5) = checkExpectedContracts vm expectation
-  putStrLn $ show expectation
-  unless okState $ void $ checkStateFail
-    diff x vm (okState, b2, b3, b4, b5)
-  return okState
-
--- quotient account state by nullness
-(~=) :: Map Addr (EVM.Contract, Storage) -> Map Addr (EVM.Contract, Storage) -> Bool
-(~=) cs1 cs2 =
-    let nullAccount = EVM.initialContract (EVM.RuntimeCode mempty)
-        padNewAccounts cs ks = Map.union cs $ Map.fromList [(k, (nullAccount, mempty)) | k <- ks]
-        padded_cs1 = padNewAccounts cs1 (Map.keys cs2)
-        padded_cs2 = padNewAccounts cs2 (Map.keys cs1)
-    in and $ zipWith (===) (Map.elems padded_cs1) (Map.elems padded_cs2)
-
-(===) :: (EVM.Contract, Storage) -> (EVM.Contract, Storage) -> Bool
-(c1, s1) === (c2, s2) =
-  codeEqual && storageEqual && (c1 ^. balance == c2 ^. balance) && (c1 ^. nonce ==  c2 ^. nonce)
-  where
-    storageEqual = s1 == s2
-    codeEqual = case (c1 ^. contractcode, c2 ^. contractcode) of
-      (EVM.RuntimeCode a', EVM.RuntimeCode b') -> a' == b'
-      _ -> error "unexpected code"
-
-checkExpectedContracts :: HasCallStack => EVM.VM -> Map Addr (EVM.Contract, Storage) -> (Bool, Bool, Bool, Bool, Bool)
-checkExpectedContracts vm expected =
-  let cs = zipWithStorages $ vm ^. EVM.env . EVM.contracts -- . to (fmap (clearZeroStorage.clearOrigStorage))
-      expectedCs = clearStorage <$> expected
-  in ( (expectedCs ~= cs)
-     , (clearBalance <$> expectedCs) ~= (clearBalance <$> cs)
-     , (clearNonce   <$> expectedCs) ~= (clearNonce   <$> cs)
-     , (clearStorage <$> expectedCs) ~= (clearStorage <$> cs)
-     , (clearCode    <$> expectedCs) ~= (clearCode    <$> cs)
-     )
-  where
-  zipWithStorages = Map.mapWithKey (\addr c -> (c, lookupStorage addr))
-  lookupStorage _ =
-    case vm ^. EVM.env . EVM.storage of
-      ConcreteStore _ -> mempty -- clearZeroStorage $ fromMaybe mempty $ Map.lookup (num addr) s
-      EmptyStore -> mempty
-      AbstractStore -> mempty -- error "AbstractStore, should this be handled?"
-      SStore {} -> mempty -- error "SStore, should this be handled?"
-      GVar _ -> error "unexpected global variable"
-
-clearStorage :: (EVM.Contract, Storage) -> (EVM.Contract, Storage)
-clearStorage (c, _) = (c, mempty)
-
-clearBalance :: (EVM.Contract, Storage) -> (EVM.Contract, Storage)
-clearBalance (c, s) = (set balance 0 c, s)
-
-clearNonce :: (EVM.Contract, Storage) -> (EVM.Contract, Storage)
-clearNonce (c, s) = (set nonce 0 c, s)
-
-clearCode :: (EVM.Contract, Storage) -> (EVM.Contract, Storage)
-clearCode (c, s) = (set contractcode (EVM.RuntimeCode mempty) c, s)
-
-
-
-newtype ContractWithStorage = ContractWithStorage { unContractWithStorage :: (EVM.Contract, Storage) }
-
-instance FromJSON ContractWithStorage where
-  parseJSON (JSON.Object v) = do
-    code <- (EVM.RuntimeCode . V.fromList . litCode <$> (hexText <$> v .: "code"))
-    storage' <- v .: "storage"
-    balance' <- v .: "balance"
-    nonce'   <- v .: "nonce"
-    let c = EVM.initialContract code
-              & balance .~ balance'
-              & nonce   .~ nonce'
-    return $ ContractWithStorage (c, storage')
-
-  parseJSON invalid =
-    JSON.typeMismatch "Contract" invalid
-
-instance FromJSON BlockchainCase where
-  parseJSON (JSON.Object v) = BlockchainCase
-    <$> v .: "blocks"
-    <*> parseContracts Pre v
-    <*> parseContracts Post v
-    <*> v .: "network"
-  parseJSON invalid =
-    JSON.typeMismatch "GeneralState test case" invalid
-
-instance FromJSON Block where
-  parseJSON (JSON.Object v) = do
-    v'         <- v .: "blockHeader"
-    txs        <- v .: "transactions"
-    coinbase   <- addrField v' "coinbase"
-    difficulty <- wordField v' "difficulty"
-    gasLimit   <- word64Field v' "gasLimit"
-    number     <- wordField v' "number"
-    baseFee    <- fmap read <$> v' .:? "baseFeePerGas"
-    timestamp  <- wordField v' "timestamp"
-    return $ Block coinbase difficulty gasLimit (fromMaybe 0 baseFee) number timestamp txs
-  parseJSON invalid =
-    JSON.typeMismatch "Block" invalid
-
-parseContracts ::
-  Which -> JSON.Object -> JSON.Parser (Map Addr (EVM.Contract, Storage))
-parseContracts w v =
-  (Map.map unContractWithStorage) <$> (v .: which >>= parseJSON)
-  where which = case w of
-          Pre  -> "pre"
-          Post -> "postState"
-
-parseBCSuite ::
-  Lazy.ByteString -> Either String (Map String Case)
-parseBCSuite x = case (JSON.eitherDecode' x) :: Either String (Map String BlockchainCase) of
-  Left e        -> Left e
-  Right bcCases -> let allCases = fromBlockchainCase <$> bcCases
-                       keepError (Left e) = errorFatal e
-                       keepError _        = True
-                       filteredCases = Map.filter keepError allCases
-                       (erroredCases, parsedCases) = splitEithers filteredCases
-    in if Map.size erroredCases > 0
-    then Left ("errored case: " ++ (show erroredCases))
-    else if Map.size parsedCases == 0
-    then Left "No cases to check."
-    else Right parsedCases
-
-
-data BlockchainError
-  = TooManyBlocks
-  | TooManyTxs
-  | NoTxs
-  | SignatureUnverified
-  | InvalidTx
-  | OldNetwork
-  | FailedCreate
-  deriving Show
-
-errorFatal :: BlockchainError -> Bool
-errorFatal TooManyBlocks = True
-errorFatal TooManyTxs = True
-errorFatal SignatureUnverified = True
-errorFatal InvalidTx = True
-errorFatal _ = False
-
-fromBlockchainCase :: BlockchainCase -> Either BlockchainError Case
-fromBlockchainCase (BlockchainCase blocks preState postState network) =
-  case (blocks, network) of
-    ([block], "London") -> case blockTxs block of
-      [tx] -> fromBlockchainCase' block tx preState postState
-      []        -> Left NoTxs
-      _         -> Left TooManyTxs
-    ([_], _) -> Left OldNetwork
-    (_, _)   -> Left TooManyBlocks
-
-fromBlockchainCase' :: Block -> Transaction
-                       -> Map Addr (EVM.Contract, Storage) -> Map Addr (EVM.Contract, Storage)
-                       -> Either BlockchainError Case
-fromBlockchainCase' block tx preState postState =
-  let isCreate = isNothing (txToAddr tx) in
-  case (sender 1 tx, checkTx tx block preState) of
-      (Nothing, _) -> Left SignatureUnverified
-      (_, Nothing) -> Left (if isCreate then FailedCreate else InvalidTx)
-      (Just origin, Just checkState) -> Right $ Case
-        (EVM.VMOpts
-         { vmoptContract      = EVM.initialContract theCode
-         , vmoptCalldata      = (cd, [])
-         , vmoptValue         = Lit (txValue tx)
-         , vmoptAddress       = toAddr
-         , vmoptCaller        = litAddr origin
-         , vmoptStorageBase   = Concrete
-         , vmoptOrigin        = origin
-         , vmoptGas           = txGasLimit tx - fromIntegral (txGasCost feeSchedule tx)
-         , vmoptBaseFee       = blockBaseFee block
-         , vmoptPriorityFee   = priorityFee tx (blockBaseFee block)
-         , vmoptGaslimit      = txGasLimit tx
-         , vmoptNumber        = blockNumber block
-         , vmoptTimestamp     = Lit $ blockTimestamp block
-         , vmoptCoinbase      = blockCoinbase block
-         , vmoptPrevRandao    = blockDifficulty block
-         , vmoptMaxCodeSize   = 24576
-         , vmoptBlockGaslimit = blockGasLimit block
-         , vmoptGasprice      = effectiveGasPrice
-         , vmoptSchedule      = feeSchedule
-         , vmoptChainId       = 1
-         , vmoptCreate        = isCreate
-         , vmoptTxAccessList  = txAccessMap tx
-         , vmoptAllowFFI      = False
-         })
-        checkState
-        postState
-          where
-            toAddr = fromMaybe (EVM.createAddress origin senderNonce) (txToAddr tx)
-            senderNonce = view (accountAt origin . nonce) (Map.map fst preState)
-            feeSchedule = EVM.FeeSchedule.berlin
-            toCode = Map.lookup toAddr preState
-            theCode = if isCreate
-                      then EVM.InitCode (txData tx) mempty
-                      else maybe (EVM.RuntimeCode mempty) (view contractcode) (fst <$> toCode)
-            effectiveGasPrice = effectiveprice tx (blockBaseFee block)
-            cd = if isCreate
-                 then mempty
-                 else ConcreteBuf $ txData tx
-
-effectiveprice :: Transaction -> W256 -> W256
-effectiveprice tx baseFee = priorityFee tx baseFee + baseFee
-
-priorityFee :: Transaction -> W256 -> W256
-priorityFee tx baseFee = let
-    (txPrioMax, txMaxFee) = case txType tx of
-               EIP1559Transaction ->
-                 let Just maxPrio = txMaxPriorityFeeGas tx
-                     Just maxFee = txMaxFeePerGas tx
-                 in (maxPrio, maxFee)
-               _ ->
-                 let Just gasPrice = txGasPrice tx
-                 in (gasPrice, gasPrice)
-  in min txPrioMax (txMaxFee - baseFee)
-
-maxBaseFee :: Transaction -> W256
-maxBaseFee tx =
-  case txType tx of
-     EIP1559Transaction ->
-       let Just maxFee = txMaxFeePerGas tx
-       in maxFee
-     _ ->
-       let Just gasPrice = txGasPrice tx
-       in gasPrice
-
-
-validateTx :: Transaction -> Block -> Map Addr (EVM.Contract, Storage) -> Maybe ()
-validateTx tx block cs = do
-  let cs' = Map.map fst cs
-  origin        <- sender 1 tx
-  originBalance <- (view balance) <$> view (at origin) cs'
-  originNonce   <- (view nonce)   <$> view (at origin) cs'
-  let gasDeposit = (effectiveprice tx (blockBaseFee block)) * (num $ txGasLimit tx)
-  if gasDeposit + (txValue tx) <= originBalance
-    && txNonce tx == originNonce && blockBaseFee block <= maxBaseFee tx
-  then Just ()
-  else Nothing
-
-checkTx :: Transaction -> Block -> Map Addr (EVM.Contract, Storage) -> Maybe (Map Addr (EVM.Contract, Storage))
-checkTx tx block prestate = do
-  origin <- sender 1 tx
-  validateTx tx block prestate
-  let isCreate   = isNothing (txToAddr tx)
-      senderNonce = view (accountAt origin . nonce) (Map.map fst prestate)
-      toAddr      = fromMaybe (EVM.createAddress origin senderNonce) (txToAddr tx)
-      prevCode    = view (accountAt toAddr . contractcode) (Map.map fst prestate)
-      prevNonce   = view (accountAt toAddr . nonce) (Map.map fst prestate)
-  if isCreate && ((case prevCode of {EVM.RuntimeCode b -> not (null b); _ -> True}) || (prevNonce /= 0))
-  then mzero
-  else
-    return prestate
-
-vmForCase :: Case -> EVM.VM
-vmForCase x =
-  let
-    a = checkContracts x
-    cs = Map.map fst a
-    st = Map.mapKeys num $ Map.map snd a
-    vm = EVM.makeVm (testVmOpts x)
-      & set (EVM.env . EVM.contracts) cs
-      & set (EVM.env . EVM.storage) (ConcreteStore st)
-      & set (EVM.env . EVM.origStorage) st
-  in
-    initTx vm
diff --git a/test/BlockchainTests.hs b/test/BlockchainTests.hs
new file mode 100644
--- /dev/null
+++ b/test/BlockchainTests.hs
@@ -0,0 +1,466 @@
+{-# LANGUAGE ImportQualifiedPost #-}
+{-# LANGUAGE TupleSections #-}
+
+module Main where
+
+import Prelude hiding (Word)
+
+import EVM qualified
+import EVM (contractcode, storage, origStorage, balance, nonce, initialContract, StorageBase(..))
+import EVM.Concrete qualified as EVM
+import EVM.Dapp (emptyDapp)
+import EVM.Expr (litAddr)
+import EVM.FeeSchedule qualified
+import EVM.Fetch qualified
+import EVM.Stepper qualified
+import EVM.SMT (withSolvers, Solver(Z3))
+import EVM.Transaction
+import EVM.TTY qualified as TTY
+import EVM.Types
+
+import Control.Arrow ((***), (&&&))
+import Control.Lens
+import Control.Monad
+import Control.Monad.State.Strict (execStateT)
+import Data.Aeson ((.:), (.:?), FromJSON (..))
+import Data.Aeson qualified as JSON
+import Data.Aeson.Types qualified as JSON
+import Data.ByteString qualified as BS
+import Data.ByteString.Lazy qualified as Lazy
+import Data.ByteString.Lazy qualified as LazyByteString
+import Data.List (isInfixOf)
+import Data.Map (Map)
+import Data.Map qualified as Map
+import Data.Maybe (fromJust, fromMaybe, isNothing, isJust)
+import Data.Word (Word64)
+import System.Environment (lookupEnv, getEnv)
+import System.FilePath.Find qualified as Find
+import System.FilePath.Posix (makeRelative, (</>))
+import Witherable (Filterable, catMaybes)
+
+import Test.Tasty
+import Test.Tasty.ExpectedFailure
+import Test.Tasty.HUnit
+
+type Storage = Map W256 W256
+
+data Which = Pre | Post
+
+data Block = Block
+  { blockCoinbase    :: Addr
+  , blockDifficulty  :: W256
+  , blockGasLimit    :: Word64
+  , blockBaseFee     :: W256
+  , blockNumber      :: W256
+  , blockTimestamp   :: W256
+  , blockTxs         :: [Transaction]
+  } deriving Show
+
+data Case = Case
+  { testVmOpts      :: EVM.VMOpts
+  , checkContracts  :: Map Addr (EVM.Contract, Storage)
+  , testExpectation :: Map Addr (EVM.Contract, Storage)
+  } deriving Show
+
+data BlockchainCase = BlockchainCase
+  { blockchainBlocks  :: [Block]
+  , blockchainPre     :: Map Addr (EVM.Contract, Storage)
+  , blockchainPost    :: Map Addr (EVM.Contract, Storage)
+  , blockchainNetwork :: String
+  } deriving Show
+
+main :: IO ()
+main = do
+  tests <- prepareTests
+  defaultMain tests
+
+prepareTests :: IO TestTree
+prepareTests = do
+  repo <- 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"
+  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."
+  pure $ testGroup "ethereum-tests" groups
+
+testsFromFile :: String -> Map String (TestTree -> TestTree) -> IO [TestTree]
+testsFromFile file problematicTests = do
+  parsed <- parseBCSuite <$> 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 False (name, x)) <$> Map.toList allTests
+  where
+  testCase' name assertion =
+    case Map.lookup name problematicTests of
+      Just f -> f (testCase name assertion)
+      Nothing -> testCase name assertion
+
+-- CI has issues with some heaver tests, disable in bulk
+ciIgnoredFiles :: [String]
+ciIgnoredFiles =
+  [ "BlockchainTests/GeneralStateTests/VMTests/vmPerformance"
+  , "BlockchainTests/GeneralStateTests/stQuadraticComplexityTest"
+  , "BlockchainTests/GeneralStateTests/stStaticCall"
+  ]
+
+commonProblematicTests :: Map String (TestTree -> TestTree)
+commonProblematicTests = Map.fromList
+  [ ("twoOps_d0g0v0_London", expectFailBecause "TODO: regression")
+  , ("sar_2^256-1_0_d0g0v0_London", expectFailBecause "TODO: regression")
+  , ("shiftCombinations_d0g0v0_London", expectFailBecause "TODO: regression")
+  , ("shiftSignedCombinations_d0g0v0_London", expectFailBecause "TODO: regression")
+  , ("bufferSrcOffset_d14g0v0_London", expectFailBecause "TODO: regression")
+  , ("bufferSrcOffset_d38g0v0_London", expectFailBecause "TODO: regression")
+  , ("loopMul_d0g0v0_London", ignoreTestBecause "hevm is too slow")
+  , ("loopMul_d1g0v0_London", ignoreTestBecause "hevm is too slow")
+  , ("loopMul_d2g0v0_London", ignoreTestBecause "hevm is too slow")
+  , ("CALLBlake2f_MaxRounds_d0g0v0_London", ignoreTestBecause "very slow, bypasses timeout due time spent in FFI")
+  ]
+
+ciProblematicTests :: Map String (TestTree -> TestTree)
+ciProblematicTests = Map.fromList
+  [ ("Return50000_d0g1v0_London", ignoreTest)
+  , ("Return50000_2_d0g1v0_London", ignoreTest)
+  , ("randomStatetest177_d0g0v0_London", ignoreTest)
+  , ("static_Call50000_d0g0v0_London", ignoreTest)
+  , ("static_Call50000_d1g0v0_London", ignoreTest)
+  , ("static_Call50000bytesContract50_1_d1g0v0_London", ignoreTest)
+  , ("static_Call50000bytesContract50_2_d1g0v0_London", ignoreTest)
+  , ("static_Return50000_2_d0g0v0_London", ignoreTest)
+  , ("loopExp_d10g0v0_London", ignoreTest)
+  , ("loopExp_d11g0v0_London", ignoreTest)
+  , ("loopExp_d12g0v0_London", ignoreTest)
+  , ("loopExp_d13g0v0_London", ignoreTest)
+  , ("loopExp_d14g0v0_London", ignoreTest)
+  , ("loopExp_d8g0v0_London", ignoreTest)
+  , ("loopExp_d9g0v0_London", ignoreTest)
+  ]
+
+runVMTest :: Bool -> (String, Case) -> IO ()
+runVMTest diffmode (_name, x) =
+ do
+  let vm0 = vmForCase x
+  result <- execStateT (EVM.Stepper.interpret (EVM.Fetch.zero 0 (Just 0)) . void $ EVM.Stepper.execFully) vm0
+  maybeReason <- checkExpectation diffmode x result
+  case maybeReason of
+    Just reason -> assertFailure reason
+    Nothing -> pure ()
+
+-- | Example usage:
+-- | $ cabal new-repl ethereum-tests
+-- | ghci> debugVMTest "BlockchainTests/GeneralStateTests/VMTests/vmArithmeticTest/twoOps.json" "twoOps_d0g0v0_London"
+debugVMTest :: String -> String -> IO ()
+debugVMTest 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
+        [(_, x')] -> x'
+        _ -> error "test not found"
+  let vm0 = vmForCase x
+  result <- withSolvers Z3 0 Nothing $ \solvers ->
+    TTY.runFromVM solvers Nothing Nothing emptyDapp vm0
+  void $ checkExpectation True x result
+
+splitEithers :: (Filterable f) => f (Either a b) -> (f a, f b)
+splitEithers =
+  (catMaybes *** catMaybes)
+  . (fmap fst &&& fmap snd)
+  . (fmap (preview _Left &&& preview _Right))
+
+checkStateFail :: Bool -> Case -> EVM.VM -> (Bool, Bool, Bool, Bool) -> IO String
+checkStateFail diff x vm (okMoney, okNonce, okData, okCode) = do
+  let
+    printContracts :: Map Addr (EVM.Contract, Storage) -> IO ()
+    printContracts cs = putStrLn $ Map.foldrWithKey (\k (c, s) acc ->
+      acc ++ show k ++ " : "
+                   ++ (show . toInteger  $ (view nonce c)) ++ " "
+                   ++ (show . toInteger  $ (view balance c)) ++ " "
+                   ++ (printStorage s)
+        ++ "\n") "" cs
+
+    reason = map fst (filter (not . snd)
+        [ ("bad-state",       okMoney || okNonce || okData  || okCode)
+        , ("bad-balance", not okMoney || okNonce || okData  || okCode)
+        , ("bad-nonce",   not okNonce || okMoney || okData  || okCode)
+        , ("bad-storage", not okData  || okMoney || okNonce || okCode)
+        , ("bad-code",    not okCode  || okMoney || okNonce || okData)
+        ])
+    check = checkContracts x
+    expected = testExpectation x
+    actual = Map.map (,mempty) $ view (EVM.env . EVM.contracts) vm -- . to (fmap (clearZeroStorage.clearOrigStorage))) vm
+    printStorage = show -- TODO: fixme
+
+  when diff $ do
+    putStr (unwords reason)
+    putStrLn "\nPre balance/state: "
+    printContracts check
+    putStrLn "\nExpected balance/state: "
+    printContracts expected
+    putStrLn "\nActual balance/state: "
+    printContracts actual
+  pure (unwords reason)
+
+checkExpectation :: Bool -> Case -> EVM.VM -> IO (Maybe String)
+checkExpectation diff x vm = do
+  let expectation = testExpectation x
+      (okState, b2, b3, b4, b5) = checkExpectedContracts vm expectation
+  if okState then
+    pure Nothing
+  else
+    Just <$> checkStateFail diff x vm (b2, b3, b4, b5)
+
+-- quotient account state by nullness
+(~=) :: Map Addr (EVM.Contract, Storage) -> Map Addr (EVM.Contract, Storage) -> Bool
+(~=) cs1 cs2 =
+    let nullAccount = EVM.initialContract (EVM.RuntimeCode (EVM.ConcreteRuntimeCode ""))
+        padNewAccounts cs ks = Map.union cs $ Map.fromList [(k, (nullAccount, mempty)) | k <- ks]
+        padded_cs1 = padNewAccounts cs1 (Map.keys cs2)
+        padded_cs2 = padNewAccounts cs2 (Map.keys cs1)
+    in and $ zipWith (===) (Map.elems padded_cs1) (Map.elems padded_cs2)
+
+(===) :: (EVM.Contract, Storage) -> (EVM.Contract, Storage) -> Bool
+(c1, s1) === (c2, s2) =
+  codeEqual && storageEqual && (c1 ^. balance == c2 ^. balance) && (c1 ^. nonce ==  c2 ^. nonce)
+  where
+    storageEqual = s1 == s2
+    codeEqual = case (c1 ^. contractcode, c2 ^. contractcode) of
+      (EVM.RuntimeCode a', EVM.RuntimeCode b') -> a' == b'
+      _ -> error "unexpected code"
+
+checkExpectedContracts :: EVM.VM -> Map Addr (EVM.Contract, Storage) -> (Bool, Bool, Bool, Bool, Bool)
+checkExpectedContracts vm expected =
+  let cs = zipWithStorages $ vm ^. EVM.env . EVM.contracts -- . to (fmap (clearZeroStorage.clearOrigStorage))
+      expectedCs = clearStorage <$> expected
+  in ( (expectedCs ~= cs)
+     , (clearBalance <$> expectedCs) ~= (clearBalance <$> cs)
+     , (clearNonce   <$> expectedCs) ~= (clearNonce   <$> cs)
+     , (clearStorage <$> expectedCs) ~= (clearStorage <$> cs)
+     , (clearCode    <$> expectedCs) ~= (clearCode    <$> cs)
+     )
+  where
+  zipWithStorages = Map.mapWithKey (\addr c -> (c, lookupStorage addr))
+  lookupStorage _ =
+    case vm ^. EVM.env . EVM.storage of
+      ConcreteStore _ -> mempty -- clearZeroStorage $ fromMaybe mempty $ Map.lookup (num addr) s
+      EmptyStore -> mempty
+      AbstractStore -> mempty -- error "AbstractStore, should this be handled?"
+      SStore {} -> mempty -- error "SStore, should this be handled?"
+      GVar _ -> error "unexpected global variable"
+
+clearStorage :: (EVM.Contract, Storage) -> (EVM.Contract, Storage)
+clearStorage (c, _) = (c, mempty)
+
+clearBalance :: (EVM.Contract, Storage) -> (EVM.Contract, Storage)
+clearBalance (c, s) = (set balance 0 c, s)
+
+clearNonce :: (EVM.Contract, Storage) -> (EVM.Contract, Storage)
+clearNonce (c, s) = (set nonce 0 c, s)
+
+clearCode :: (EVM.Contract, Storage) -> (EVM.Contract, Storage)
+clearCode (c, s) = (set contractcode (EVM.RuntimeCode (EVM.ConcreteRuntimeCode "")) c, s)
+
+newtype ContractWithStorage = ContractWithStorage { unContractWithStorage :: (EVM.Contract, Storage) }
+
+instance FromJSON ContractWithStorage where
+  parseJSON (JSON.Object v) = do
+    code <- (EVM.RuntimeCode . EVM.ConcreteRuntimeCode <$> (hexText <$> v .: "code"))
+    storage' <- v .: "storage"
+    balance' <- v .: "balance"
+    nonce'   <- v .: "nonce"
+    let c = EVM.initialContract code
+              & balance .~ balance'
+              & nonce   .~ nonce'
+    return $ ContractWithStorage (c, storage')
+
+  parseJSON invalid =
+    JSON.typeMismatch "Contract" invalid
+
+instance FromJSON BlockchainCase where
+  parseJSON (JSON.Object v) = BlockchainCase
+    <$> v .: "blocks"
+    <*> parseContracts Pre v
+    <*> parseContracts Post v
+    <*> v .: "network"
+  parseJSON invalid =
+    JSON.typeMismatch "GeneralState test case" invalid
+
+instance FromJSON Block where
+  parseJSON (JSON.Object v) = do
+    v'         <- v .: "blockHeader"
+    txs        <- v .: "transactions"
+    coinbase   <- addrField v' "coinbase"
+    difficulty <- wordField v' "difficulty"
+    gasLimit   <- word64Field v' "gasLimit"
+    number     <- wordField v' "number"
+    baseFee    <- fmap read <$> v' .:? "baseFeePerGas"
+    timestamp  <- wordField v' "timestamp"
+    return $ Block coinbase difficulty gasLimit (fromMaybe 0 baseFee) number timestamp txs
+  parseJSON invalid =
+    JSON.typeMismatch "Block" invalid
+
+parseContracts ::
+  Which -> JSON.Object -> JSON.Parser (Map Addr (EVM.Contract, Storage))
+parseContracts w v =
+  (Map.map unContractWithStorage) <$> (v .: which >>= parseJSON)
+  where which = case w of
+          Pre  -> "pre"
+          Post -> "postState"
+
+parseBCSuite ::
+  Lazy.ByteString -> Either String (Map String Case)
+parseBCSuite x = case (JSON.eitherDecode' x) :: Either String (Map String BlockchainCase) of
+  Left e        -> Left e
+  Right bcCases -> let allCases = fromBlockchainCase <$> bcCases
+                       keepError (Left e) = errorFatal e
+                       keepError _        = True
+                       filteredCases = Map.filter keepError allCases
+                       (erroredCases, parsedCases) = splitEithers filteredCases
+    in if Map.size erroredCases > 0
+    then Left ("errored case: " ++ (show erroredCases))
+    else if Map.size parsedCases == 0
+    then Left "No cases to check."
+    else Right parsedCases
+
+
+data BlockchainError
+  = TooManyBlocks
+  | TooManyTxs
+  | NoTxs
+  | SignatureUnverified
+  | InvalidTx
+  | OldNetwork
+  | FailedCreate
+  deriving Show
+
+errorFatal :: BlockchainError -> Bool
+errorFatal TooManyBlocks = True
+errorFatal TooManyTxs = True
+errorFatal SignatureUnverified = True
+errorFatal InvalidTx = True
+errorFatal _ = False
+
+fromBlockchainCase :: BlockchainCase -> Either BlockchainError Case
+fromBlockchainCase (BlockchainCase blocks preState postState network) =
+  case (blocks, network) of
+    ([block], "London") -> case blockTxs block of
+      [tx] -> fromBlockchainCase' block tx preState postState
+      []        -> Left NoTxs
+      _         -> Left TooManyTxs
+    ([_], _) -> Left OldNetwork
+    (_, _)   -> Left TooManyBlocks
+
+fromBlockchainCase' :: Block -> Transaction
+                       -> Map Addr (EVM.Contract, Storage) -> Map Addr (EVM.Contract, Storage)
+                       -> Either BlockchainError Case
+fromBlockchainCase' block tx preState postState =
+  let isCreate = isNothing (txToAddr tx) in
+  case (sender 1 tx, checkTx tx block preState) of
+      (Nothing, _) -> Left SignatureUnverified
+      (_, Nothing) -> Left (if isCreate then FailedCreate else InvalidTx)
+      (Just origin, Just checkState) -> Right $ Case
+        (EVM.VMOpts
+         { vmoptContract      = EVM.initialContract theCode
+         , vmoptCalldata      = (cd, [])
+         , vmoptValue         = Lit (txValue tx)
+         , vmoptAddress       = toAddr
+         , vmoptCaller        = litAddr origin
+         , vmoptStorageBase   = Concrete
+         , vmoptOrigin        = origin
+         , vmoptGas           = txGasLimit tx - fromIntegral (txGasCost feeSchedule tx)
+         , vmoptBaseFee       = blockBaseFee block
+         , vmoptPriorityFee   = priorityFee tx (blockBaseFee block)
+         , vmoptGaslimit      = txGasLimit tx
+         , vmoptNumber        = blockNumber block
+         , vmoptTimestamp     = Lit $ blockTimestamp block
+         , vmoptCoinbase      = blockCoinbase block
+         , vmoptPrevRandao    = blockDifficulty block
+         , vmoptMaxCodeSize   = 24576
+         , vmoptBlockGaslimit = blockGasLimit block
+         , vmoptGasprice      = effectiveGasPrice
+         , vmoptSchedule      = feeSchedule
+         , vmoptChainId       = 1
+         , vmoptCreate        = isCreate
+         , vmoptTxAccessList  = txAccessMap tx
+         , vmoptAllowFFI      = False
+         })
+        checkState
+        postState
+          where
+            toAddr = fromMaybe (EVM.createAddress origin senderNonce) (txToAddr tx)
+            senderNonce = view (accountAt origin . nonce) (Map.map fst preState)
+            feeSchedule = EVM.FeeSchedule.berlin
+            toCode = Map.lookup toAddr preState
+            theCode = if isCreate
+                      then EVM.InitCode (txData tx) mempty
+                      else maybe (EVM.RuntimeCode (EVM.ConcreteRuntimeCode "")) (view contractcode . fst) toCode
+            effectiveGasPrice = effectiveprice tx (blockBaseFee block)
+            cd = if isCreate
+                 then mempty
+                 else ConcreteBuf $ txData tx
+
+effectiveprice :: Transaction -> W256 -> W256
+effectiveprice tx baseFee = priorityFee tx baseFee + baseFee
+
+priorityFee :: Transaction -> W256 -> W256
+priorityFee tx baseFee = let
+    (txPrioMax, txMaxFee) = case txType tx of
+               EIP1559Transaction ->
+                 let maxPrio = fromJust $ txMaxPriorityFeeGas tx
+                     maxFee = fromJust $ txMaxFeePerGas tx
+                 in (maxPrio, maxFee)
+               _ ->
+                 let gasPrice = fromJust $ txGasPrice tx
+                 in (gasPrice, gasPrice)
+  in min txPrioMax (txMaxFee - baseFee)
+
+maxBaseFee :: Transaction -> W256
+maxBaseFee tx =
+  case txType tx of
+     EIP1559Transaction -> fromJust $ txMaxFeePerGas tx
+     _ -> fromJust $ txGasPrice tx
+
+validateTx :: Transaction -> Block -> Map Addr (EVM.Contract, Storage) -> Maybe ()
+validateTx tx block cs = do
+  let cs' = Map.map fst cs
+  origin        <- sender 1 tx
+  originBalance <- (view balance) <$> view (at origin) cs'
+  originNonce   <- (view nonce)   <$> view (at origin) cs'
+  let gasDeposit = (effectiveprice tx (blockBaseFee block)) * (num $ txGasLimit tx)
+  if gasDeposit + (txValue tx) <= originBalance
+    && txNonce tx == originNonce && blockBaseFee block <= maxBaseFee tx
+  then Just ()
+  else Nothing
+
+checkTx :: Transaction -> Block -> Map Addr (EVM.Contract, Storage) -> Maybe (Map Addr (EVM.Contract, Storage))
+checkTx tx block prestate = do
+  origin <- sender 1 tx
+  validateTx tx block prestate
+  let isCreate   = isNothing (txToAddr tx)
+      senderNonce = view (accountAt origin . nonce) (Map.map fst prestate)
+      toAddr      = fromMaybe (EVM.createAddress origin senderNonce) (txToAddr tx)
+      prevCode    = view (accountAt toAddr . contractcode) (Map.map fst prestate)
+      prevNonce   = view (accountAt toAddr . nonce) (Map.map fst prestate)
+  if isCreate && ((case prevCode of {EVM.RuntimeCode (EVM.ConcreteRuntimeCode b) -> not (BS.null b); _ -> True}) || (prevNonce /= 0))
+  then mzero
+  else
+    return prestate
+
+vmForCase :: Case -> EVM.VM
+vmForCase x =
+  let
+    a = checkContracts x
+    cs = Map.map fst a
+    st = Map.mapKeys num $ Map.map snd a
+    vm = EVM.makeVm (testVmOpts x)
+      & set (EVM.env . EVM.contracts) cs
+      & set (EVM.env . EVM.storage) (ConcreteStore st)
+      & set (EVM.env . EVM.origStorage) st
+  in
+    initTx vm
diff --git a/test/rpc.hs b/test/rpc.hs
--- a/test/rpc.hs
+++ b/test/rpc.hs
@@ -75,10 +75,14 @@
         postVm <- withSolvers Z3 1 Nothing $ \solvers ->
           execStateT (Stepper.interpret (Fetch.oracle solvers (Just (BlockNumber blockNum, testRpc))) . void $ Stepper.execFully) vm
         let
-          (ConcreteStore postStore) = view (env . storage) postVm
+          postStore = case view (env . storage) postVm of
+            ConcreteStore s -> s
+            _ -> error "ConcreteStore expected"
           wethStore = fromJust $ Map.lookup 0xC02aaA39b223FE8D0A0e5C4F27eAD9083C756Cc2 postStore
           receiverBal = fromJust $ Map.lookup (keccak' (word256Bytes 0xdead <> word256Bytes 0x3)) wethStore
-          (Just (VMSuccess msg)) = view result postVm
+          msg = case view result postVm of
+            Just (VMSuccess m) -> m
+            _ -> error "VMSuccess expected"
         assertEqual "should succeed" msg (ConcreteBuf $ word256Bytes 0x1)
         assertEqual "should revert" receiverBal (W256 $ 2595433725034301 + wad)
 
diff --git a/test/test.hs b/test/test.hs
--- a/test/test.hs
+++ b/test/test.hs
@@ -7,7 +7,7 @@
 
 import Data.Text (Text)
 import Data.ByteString (ByteString)
-import Data.Bits
+import Data.Bits hiding (And, Xor)
 import System.Directory
 import GHC.Natural
 import Control.Monad
@@ -19,19 +19,18 @@
 import Prelude hiding (fail, LT, GT)
 
 import qualified Data.ByteString as BS
-import qualified Data.ByteString.Lazy as BS (fromStrict)
 import qualified Data.ByteString.Base16 as Hex
 import Data.Maybe
 import Data.Typeable
 import Data.List (elemIndex)
 import Data.DoubleWord
 import Test.Tasty
-import Test.Tasty.QuickCheck
+import Test.Tasty.QuickCheck hiding (Failure)
 import Test.QuickCheck.Instances.Text()
 import Test.QuickCheck.Instances.Natural()
 import Test.QuickCheck.Instances.ByteString()
 import Test.Tasty.HUnit
-import Test.Tasty.Runners
+import Test.Tasty.Runners hiding (Failure)
 import Test.Tasty.ExpectedFailure
 
 import Control.Monad.State.Strict (execState, runState)
@@ -329,7 +328,9 @@
           -- traceM ("encoding: " ++ (show y) ++ " : " ++ show (abiValueType y))
           Just encoded <- runStatements [i| x = abi.encode(a);|]
             [y] AbiBytesDynamicType
-          let AbiTuple (Vector.toList -> [solidityEncoded]) = decodeAbiValue (AbiTupleType $ Vector.fromList [AbiBytesDynamicType]) (BS.fromStrict encoded)
+          let solidityEncoded = case decodeAbiValue (AbiTupleType $ Vector.fromList [AbiBytesDynamicType]) (BS.fromStrict encoded) of
+                AbiTuple (Vector.toList -> [e]) -> e
+                _ -> error "AbiTuple expected"
           let hevmEncoded = encodeAbiValue (AbiTuple $ Vector.fromList [y])
           -- traceM ("encoded (solidity): " ++ show solidityEncoded)
           -- traceM ("encoded (hevm): " ++ show (AbiBytesDynamic hevmEncoded))
@@ -340,7 +341,9 @@
           -- traceM ("encoding: " ++ (show x') ++ ", " ++ (show y')  ++ " : " ++ show (abiValueType x') ++ ", " ++ show (abiValueType y'))
           Just encoded <- runStatements [i| x = abi.encode(a, b);|]
             [x', y'] AbiBytesDynamicType
-          let AbiTuple (Vector.toList -> [solidityEncoded]) = decodeAbiValue (AbiTupleType $ Vector.fromList [AbiBytesDynamicType]) (BS.fromStrict encoded)
+          let solidityEncoded = case decodeAbiValue (AbiTupleType $ Vector.fromList [AbiBytesDynamicType]) (BS.fromStrict encoded) of
+                AbiTuple (Vector.toList -> [e]) -> e
+                _ -> error "AbiTuple expected"
           let hevmEncoded = encodeAbiValue (AbiTuple $ Vector.fromList [x',y'])
           -- traceM ("encoded (solidity): " ++ show solidityEncoded)
           -- traceM ("encoded (hevm): " ++ show (AbiBytesDynamic hevmEncoded))
@@ -421,9 +424,9 @@
                 |]
 
         (json, path') <- solidity' srccode
-        let Just (solc', _, _) = readJSON json
+        let (solc', _, _) = fromJust $ readJSON json
             initCode :: ByteString
-            Just initCode = solc' ^? ix (path' <> ":A") . creationCode
+            initCode = fromJust $ solc' ^? ix (path' <> ":A") . creationCode
         -- add constructor arguments
         assertEqual "constructor args screwed up metadata stripping" (stripBytecodeMetadata (initCode <> encodeAbiValue (AbiUInt 256 1))) (stripBytecodeMetadata initCode)
     ]
@@ -1036,11 +1039,15 @@
             }
           }
           |]
-        let pre preVM = let [x, y] = getStaticAbiArgs 2 preVM
+        let pre preVM = let (x, y) = case getStaticAbiArgs 2 preVM of
+                                       [x', y'] -> (x', y')
+                                       _ -> error "expected 2 args"
                         in (x .<= Expr.add x y)
                            .&& view (state . callvalue) preVM .== Lit 0
             post prestate leaf =
-              let [x, y] = getStaticAbiArgs 2 prestate
+              let (x, y) = case getStaticAbiArgs 2 prestate of
+                             [x', y'] -> (x', y')
+                             _ -> error "expected 2 args"
               in case leaf of
                    Return _ b _ -> (ReadWord (Lit 0) b) .== (Add x y)
                    _ -> PBool True
@@ -1057,12 +1064,16 @@
             }
           }
           |]
-        let pre preVM = let [x, y] = getStaticAbiArgs  2 preVM
+        let pre preVM = let (x, y) = case getStaticAbiArgs 2 preVM of
+                                       [x', y'] -> (x', y')
+                                       _ -> error "expected 2 args"
                         in (x .<= Expr.add x y)
                            .&& (x .== y)
                            .&& view (state . callvalue) preVM .== Lit 0
             post prestate leaf =
-              let [_, y] = getStaticAbiArgs 2 prestate
+              let (_, y) = case getStaticAbiArgs 2 prestate of
+                             [x', y'] -> (x', y')
+                             _ -> error "expected 2 args"
               in case leaf of
                    Return _ b _ -> (ReadWord (Lit 0) b) .== (Mul (Lit 2) y)
                    _ -> PBool True
@@ -1085,7 +1096,9 @@
           |]
         let pre vm = Lit 0 .== view (state . callvalue) vm
             post prestate leaf =
-              let [y] = getStaticAbiArgs 1 prestate
+              let y = case getStaticAbiArgs 1 prestate of
+                        [y'] -> y'
+                        _ -> error "expected 1 arg"
                   this = Expr.litAddr $ view (state . codeContract) prestate
                   prex = Expr.readStorage' this (Lit 0) (view (env . storage) prestate)
               in case leaf of
@@ -1137,7 +1150,9 @@
             |]
           let pre vm = (Lit 0) .== view (state . callvalue) vm
               post prestate poststate =
-                let [x,y] = getStaticAbiArgs 2 prestate
+                let (x,y) = case getStaticAbiArgs 2 prestate of
+                        [x',y'] -> (x',y')
+                        _ -> error "expected 2 args"
                     this = Expr.litAddr $ view (state . codeContract) prestate
                     prestore =  view (env . storage) prestate
                     prex = Expr.readStorage' this x prestore
@@ -1169,7 +1184,9 @@
             |]
           let pre vm = (Lit 0) .== view (state . callvalue) vm
               post prestate poststate =
-                let [x,y] = getStaticAbiArgs 2 prestate
+                let (x,y) = case getStaticAbiArgs 2 prestate of
+                        [x',y'] -> (x',y')
+                        _ -> error "expected 2 args"
                     this = Expr.litAddr $ view (state . codeContract) prestate
                     prestore =  view (env . storage) prestate
                     prex = Expr.readStorage' this x prestore
@@ -1613,7 +1630,7 @@
             let vm = vm0
                   & set (state . callvalue) (Lit 0)
                   & over (env . contracts)
-                       (Map.insert aAddr (initialContract (RuntimeCode (fromJust $ Expr.toList $ ConcreteBuf a))))
+                       (Map.insert aAddr (initialContract (RuntimeCode (ConcreteRuntimeCode a))))
                   -- NOTE: this used to as follows, but there is no _storage field in Contract record
                   -- (Map.insert aAddr (initialContract (RuntimeCode $ ConcreteBuffer a) &
                   --                     set EVM.storage (EVM.Symbolic [] store)))
@@ -2124,7 +2141,7 @@
     case runState exec (vmForEthrunCreation x) of
        (VMSuccess (ConcreteBuf targetCode), vm1) -> do
          let target = view (state . contract) vm1
-             vm2 = execState (replaceCodeOfSelf (RuntimeCode (fromJust $ Expr.toList $ ConcreteBuf targetCode))) vm1
+             vm2 = execState (replaceCodeOfSelf (RuntimeCode (ConcreteRuntimeCode targetCode))) vm1
          return $ snd $ flip runState vm2
                 (do resetState
                     assign (state . gas) 0xffffffffffffffff -- kludge
@@ -2188,7 +2205,9 @@
 -- includes shaving off 4 byte function sig
 decodeAbiValues :: [AbiType] -> ByteString -> [AbiValue]
 decodeAbiValues types bs =
-  let AbiTuple xy = decodeAbiValue (AbiTupleType $ Vector.fromList types) (BS.fromStrict (BS.drop 4 bs))
+  let xy = case decodeAbiValue (AbiTupleType $ Vector.fromList types) (BS.fromStrict (BS.drop 4 bs)) of
+        AbiTuple xy' -> xy'
+        _ -> error "AbiTuple expected"
   in Vector.toList xy
 
 newtype Bytes = Bytes ByteString
@@ -2270,13 +2289,14 @@
 genNat = fmap fromIntegral (arbitrary :: Gen Natural)
 
 genName :: Gen Text
-genName = fmap T.pack $ listOf1 (oneof . (fmap pure) $ ['a'..'z'] <> ['A'..'Z'])
+-- In order not to generate SMT reserved words, we prepend with "esc_"
+genName = fmap (T.pack . ("esc_" <> )) $ listOf1 (oneof . (fmap pure) $ ['a'..'z'] <> ['A'..'Z'])
 
 genEnd :: Int -> Gen (Expr End)
 genEnd 0 = oneof
- [ pure $ Invalid []
- , pure $ EVM.Types.IllegalOverflow []
- , pure $ SelfDestruct []
+ [ pure $ Failure [] Invalid
+ , pure $ Failure [] EVM.Types.IllegalOverflow
+ , pure $ Failure [] SelfDestruct
  ]
 genEnd sz = oneof
  [ fmap (EVM.Types.Revert []) subBuf