diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,12 +1,29 @@
 # hevm changelog
 
+## 0.42.0 - 2020-10-31
+
+### Changed
+
+- z3 updated to 4.8.8
+- optimize SMT queries
+- More useful trace output for unknown calls
+- Default to on chain values for `coinbase`, `timestamp`, `difficulty`, `blocknumber` when rpc is provided
+- Perform tx initialization (gas payment, value transfer) in `hevm exec`, `hevm symbolic` and `hevm dapp-test`.
+
+### Added
+
+- TTY commands `P` and `c-p` for taking larger steps backwards in the debuger.
+- `--cache` flag for `dapp-test`, `exec`, `symbolic`, `interactive`,
+  enabling caching of contracts received by rpc.
+- `load(address,bytes32)` cheat code allowing storage reads from arbitrary contracts.
+
 ## 0.41.0 - 2020-08-19
 
 ### Changed
 
 - Switched to [PVP](https://github.com/haskell/pvp/blob/master/pvp-faq.md) for version control, starting now at `0.41.0` (MAJOR.MAJOR.MINOR).
 - z3 updated to 4.8.7
-- Generate more interesting values in property based testing, 
+- Generate more interesting values in property based testing,
  and implement proper shrinking for all abi values.
 - Fixed soundness bug when using KECCAK or SHA256 opcode/precompile
 - Fixed an issue in debug mode where backstepping could cause path information to be forgotten
@@ -34,9 +51,9 @@
   - state.caller: `Addr` -> `SAddr`.
   - state.returndata: `ByteString` -> `[SWord 8]`.
   - state.calldata: `ByteString` -> `([SWord 8], (SWord 32))`. The first element is a list of symbolic bytes, the second is the length of calldata. We have `fst calldata !! i .== 0` for all `snd calldata < i`.
-  
+
   - tx.value: `W256` -> `SymWord`.
-  
+
   - contract.storage: `Map Word Word` -> `Storage`, defined as:
 ```hs
 data Storage
@@ -53,7 +70,7 @@
 See the README for details on usage.
 
 The new module `EVM.SymExec` exposes several library functions dealing with symbolic execution.
-In particular, 
+In particular,
  - `SymExec.interpret`: implements an operational monad script similar to `TTY.interpret` and `Stepper.interpret`, but returns a list of final VM states rather than a single VM.
  - `SymExec.verify`: takes a prestate and a postcondition, symbolically executes the prestate and checks that all final states matches the postcondition.
 
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
@@ -9,19 +9,21 @@
 {-# Language NumDecimals #-}
 {-# Language OverloadedStrings #-}
 {-# Language TypeOperators #-}
+{-# Language RecordWildCards #-}
 
 module Main where
 
 import EVM (StorageModel(..))
 import qualified EVM
-import EVM.Concrete (createAddress, w256)
-import EVM.Symbolic (forceLitBytes, litBytes, litAddr, w256lit, sw256, SymWord(..), Buffer(..), len)
+import EVM.Concrete (createAddress, w256, wordValue)
+import EVM.Symbolic (forceLitBytes, litAddr, w256lit, sw256, SymWord(..), len, forceLit, litWord)
 import qualified EVM.FeeSchedule as FeeSchedule
 import qualified EVM.Fetch
 import qualified EVM.Flatten
 import qualified EVM.Stepper
 import qualified EVM.TTY
 import qualified EVM.Emacs
+import EVM.Dev (concatMapM)
 
 #if MIN_VERSION_aeson(1, 0, 0)
 import qualified EVM.VMTest as VMTest
@@ -105,8 +107,10 @@
       , difficulty    :: w ::: Maybe W256       <?> "Block: difficulty"
       , chainid       :: w ::: Maybe W256       <?> "Env: chainId"
   -- remote state opts
-      , rpc         :: w ::: Maybe URL        <?> "Fetch state from a remote node"
-      , block       :: w ::: Maybe W256       <?> "Block state is be fetched from"
+      , rpc           :: w ::: Maybe URL        <?> "Fetch state from a remote node"
+      , block         :: w ::: Maybe W256       <?> "Block state is be fetched from"
+      , state         :: w ::: Maybe String     <?> "Path to state repository"
+      , cache         :: w ::: Maybe String     <?> "Path to rpc cache repository"
 
   -- symbolic execution opts
       , jsonFile      :: w ::: Maybe String       <?> "Filename or path to dapp build output (default: out/*.solc.json)"
@@ -127,6 +131,7 @@
       , smttimeout    :: w ::: Maybe Integer <?> "Timeout given to SMT solver in milliseconds (default: 20000)"
       , maxIterations :: w ::: Maybe Integer <?> "Number of times we may revisit a particular branching point"
       , solver        :: w ::: Maybe Text    <?> "Used SMT solver: z3 (default) or cvc4"
+      , smtoutput     :: w ::: Bool          <?> "Print verbose smt output"
       }
   | Exec -- Execute a given program with specified env & calldata
       { code        :: w ::: Maybe ByteString <?> "Program bytecode"
@@ -149,6 +154,7 @@
       , debug       :: w ::: Bool             <?> "Run interactively"
       , trace       :: w ::: Bool             <?> "Dump trace"
       , state       :: w ::: Maybe String     <?> "Path to state repository"
+      , cache       :: w ::: Maybe String     <?> "Path to rpc cache repository"
       , rpc         :: w ::: Maybe URL        <?> "Fetch state from a remote node"
       , block       :: w ::: Maybe W256       <?> "Block state is be fetched from"
       , jsonFile    :: w ::: Maybe String     <?> "Filename or path to dapp build output (default: out/*.solc.json)"
@@ -164,6 +170,7 @@
       , verbose     :: w ::: Maybe Int                <?> "Append call trace: {1} failures {2} all"
       , coverage    :: w ::: Bool                     <?> "Coverage analysis"
       , state       :: w ::: Maybe String             <?> "Path to state repository"
+      , cache       :: w ::: Maybe String             <?> "Path to rpc cache repository"
       , match       :: w ::: Maybe String             <?> "Test case filter - only run methods matching regex"
       }
   | Interactive -- Browse & run unit tests interactively
@@ -171,6 +178,7 @@
       , dappRoot :: w ::: Maybe String <?> "Path to dapp project root directory (default: . )"
       , rpc      :: w ::: Maybe URL    <?> "Fetch state from a remote node"
       , state    :: w ::: Maybe String <?> "Path to state repository"
+      , cache    :: w ::: Maybe String <?> "Path to rpc cache repository"
       , replay   :: w ::: Maybe (Text, ByteString) <?> "Custom fuzz case to run/debug"
       }
   | BcTest -- Run an Ethereum Blockhain/GeneralState test
@@ -225,6 +233,24 @@
 optsMode :: Command Options.Unwrapped -> Mode
 optsMode x = if debug x then Debug else Run
 
+applyCache :: (Maybe String, Maybe String) -> IO (EVM.VM -> EVM.VM)
+applyCache (state, cache) =
+  let applyState = flip Facts.apply
+      applyCache = flip Facts.applyCache
+  in case (state, cache) of
+    (Nothing, Nothing) -> do
+      pure id
+    (Nothing, Just cachePath) -> do
+      facts <- Git.loadFacts (Git.RepoAt cachePath)
+      pure $ applyCache facts
+    (Just statePath, Nothing) -> do
+      facts <- Git.loadFacts (Git.RepoAt statePath)
+      pure $ applyState facts
+    (Just statePath, Just cachePath) -> do
+      cacheFacts <- Git.loadFacts (Git.RepoAt cachePath)
+      stateFacts <- Git.loadFacts (Git.RepoAt statePath)
+      pure $ (applyState stateFacts) . (applyCache cacheFacts)
+
 unitTestOptions :: Command Options.Unwrapped -> String -> IO UnitTestOptions
 unitTestOptions cmd testFile = do
   let root = fromMaybe "." (dappRoot cmd)
@@ -233,15 +259,9 @@
     Just (contractMap, sourceCache) ->
       pure $ dappInfo root contractMap sourceCache
 
-  vmModifier <-
-    case state cmd of
-      Nothing ->
-        pure id
-      Just repoPath -> do
-        facts <- Git.loadFacts (Git.RepoAt repoPath)
-        pure (flip Facts.apply facts)
+  vmModifier <- applyCache (state cmd, cache cmd)
 
-  params <- getParametersFromEnvironmentVariables
+  params <- getParametersFromEnvironmentVariables (rpc cmd)
 
   let
     testn = testNumber params
@@ -286,7 +306,7 @@
         testOpts <- unitTestOptions cmd testFile
         case (coverage cmd, optsMode cmd) of
           (False, Run) ->
-            dappTest testOpts (optsMode cmd) testFile
+            dappTest testOpts (optsMode cmd) testFile (cache cmd)
           (False, Debug) ->
             EVM.TTY.main testOpts root testFile
           (True, _) ->
@@ -354,15 +374,28 @@
         , intercalate ", " xs
         ]
 
-dappTest :: UnitTestOptions -> Mode -> String -> IO ()
-dappTest opts _ solcFile =
+dappTest :: UnitTestOptions -> Mode -> String -> Maybe String -> IO ()
+dappTest opts _ solcFile cache =
   readSolc solcFile >>=
     \case
-      Just (contractMap, cache) -> do
+      Just (contractMap, sourceCache) -> do
         let matcher = regexMatches (EVM.UnitTest.match opts)
             unitTests = (findUnitTests matcher) (Map.elems contractMap)
-        results <- mapM (runUnitTestContract opts contractMap cache) unitTests
-        when (any (== False) results) exitFailure
+
+        results <- concatMapM (runUnitTestContract opts contractMap sourceCache) unitTests
+        let (passing, vms) = unzip results
+
+        case cache of
+          Nothing ->
+            pure ()
+          Just path ->
+            -- merge all of the post-vm caches and save into the state
+            let
+              cache' = mconcat [view EVM.cache vm | vm <- vms]
+            in
+              Git.saveFacts (Git.RepoAt path) (Facts.cacheFacts cache')
+
+        unless (all id passing) exitFailure
       Nothing ->
         error ("Failed to read Solidity JSON for `" ++ solcFile ++ "'")
 
@@ -468,7 +501,7 @@
       io $ void $ EVM.TTY.runFromVM
         (maxIterations cmd)
         srcInfo
-        (EVM.Fetch.oracle smtState rpcinfo model)
+        (EVM.Fetch.oracle (Just smtState) rpcinfo model True)
         preState
 
   else
@@ -527,13 +560,13 @@
 dappCoverage opts _ solcFile =
   readSolc solcFile >>=
     \case
-      Just (contractMap, cache) -> do
+      Just (contractMap, sourceCache) -> do
         let matcher = regexMatches (EVM.UnitTest.match opts)
         let unitTests = (findUnitTests matcher) (Map.elems contractMap)
-        covs <- mconcat <$> mapM (coverageForUnitTestContract opts contractMap cache) unitTests
+        covs <- mconcat <$> mapM (coverageForUnitTestContract opts contractMap sourceCache) unitTests
 
         let
-          dapp = dappInfo "." contractMap cache
+          dapp = dappInfo "." contractMap sourceCache
           f (k, vs) = do
             putStr "***** hevm coverage for "
             putStrLn (unpack k)
@@ -556,19 +589,10 @@
 launchExec :: Command Options.Unwrapped -> IO ()
 launchExec cmd = do
   dapp <- getSrcInfo cmd
-
   vm <- vmFromCommand cmd
-  vm1 <- case state cmd of
-    Nothing -> pure vm
-    Just path ->
-      -- Note: this will load the code, so if you've specified a state
-      -- repository, then you effectively can't change `--code' after
-      -- the first run.
-      Facts.apply vm <$> Git.loadFacts (Git.RepoAt path)
-
   case optsMode cmd of
     Run -> do
-      vm' <- execStateT (interpret fetcher Nothing . void $ EVM.Stepper.execFully) vm1
+      vm' <- execStateT (EVM.Stepper.interpret fetcher . void $ EVM.Stepper.execFully) vm
       when (trace cmd) $ hPutStr stderr (showTraceTree dapp vm')
       case view EVM.result vm' of
         Nothing ->
@@ -588,7 +612,12 @@
             Nothing -> pure ()
             Just path ->
               Git.saveFacts (Git.RepoAt path) (Facts.vmFacts vm')
-    Debug -> void $ EVM.TTY.runFromVM Nothing dapp fetcher vm1
+          case cache cmd of
+            Nothing -> pure ()
+            Just path ->
+              Git.saveFacts (Git.RepoAt path) (Facts.cacheFacts (view EVM.cache vm'))
+
+    Debug -> void $ EVM.TTY.runFromVM Nothing dapp fetcher vm
    where fetcher = maybe EVM.Fetch.zero (EVM.Fetch.http block') (rpc cmd)
          block'  = maybe EVM.Fetch.Latest EVM.Fetch.BlockNumber (block cmd)
 
@@ -654,25 +683,48 @@
 -- | Creates a (concrete) VM from command line options
 vmFromCommand :: Command Options.Unwrapped -> IO EVM.VM
 vmFromCommand cmd = do
-  vm <- case (rpc cmd, address cmd) of
-    (Just url, Just addr') -> do
+  withCache <- applyCache (state cmd, cache cmd)
+
+  (miner,ts,blockNum,diff) <- case rpc cmd of
+    Nothing -> return (0,0,0,0)
+    Just url -> EVM.Fetch.fetchBlockFrom block' url >>= \case
+      Nothing -> error $ "Could not fetch block"
+      Just EVM.Block{..} -> return (_coinbase
+                                   , wordValue $ forceLit $ _timestamp
+                                   , wordValue _number
+                                   , wordValue _difficulty
+                                   )
+
+  contract <- case (rpc cmd, address cmd, code cmd) of
+    (Just url, Just addr', Just c) -> do
       EVM.Fetch.fetchContractFrom block' url addr' >>= \case
-        Nothing -> error $ "contract not found: " <> show address'
-        Just contract' -> case code cmd of
-          Nothing -> return (vm1 contract')
+        Nothing ->
+          error $ "contract not found: " <> show address'
+        Just contract' ->
           -- if both code and url is given,
           -- fetch the contract and overwrite the code
-          Just c -> return . vm1 $
+          return $
             EVM.initialContract  (codeType $ hexByteString "--code" $ strip0x c)
               & set EVM.storage  (view EVM.storage  contract')
               & set EVM.balance  (view EVM.balance  contract')
               & set EVM.nonce    (view EVM.nonce    contract')
               & set EVM.external (view EVM.external contract')
 
-    _ -> return . vm1 . EVM.initialContract . codeType $ bytes code ""
+    (Just url, Just addr', Nothing) ->
+      EVM.Fetch.fetchContractFrom block' url addr' >>= \case
+        Nothing ->
+          error $ "contract not found: " <> show address'
+        Just contract' -> return contract'
 
-  return $ vm & EVM.env . EVM.contracts . ix address' . EVM.balance +~ (w256 value')
-      where
+    (_, _, Just c)  ->
+      return $
+        EVM.initialContract (codeType $ hexByteString "--code" $ strip0x c)
+
+    (_, _, Nothing) ->
+      error $ "must provide at least (rpc + address) or code"
+
+  return $ VMTest.initTx $ withCache (vm0 miner ts blockNum diff contract)
+    where
         decipher = hexByteString "bytes" . strip0x
         block'   = maybe EVM.Fetch.Latest EVM.Fetch.BlockNumber (block cmd)
         value'   = word value 0
@@ -684,7 +736,7 @@
               then createAddress origin' (word nonce 0)
               else addr address 0xacab
 
-        vm1 c = EVM.makeVm $ EVM.VMOpts
+        vm0 miner ts blockNum diff c = EVM.makeVm $ EVM.VMOpts
           { EVM.vmoptContract      = c
           , EVM.vmoptCalldata      = (calldata', literal . num $ len calldata')
           , EVM.vmoptValue         = w256lit value'
@@ -693,13 +745,13 @@
           , EVM.vmoptOrigin        = origin'
           , EVM.vmoptGas           = word gas 0
           , EVM.vmoptGaslimit      = word gas 0
-          , EVM.vmoptCoinbase      = addr coinbase 0
-          , EVM.vmoptNumber        = word number 0
-          , EVM.vmoptTimestamp     = word timestamp 0
+          , EVM.vmoptCoinbase      = addr coinbase miner
+          , EVM.vmoptNumber        = word number blockNum
+          , EVM.vmoptTimestamp     = w256lit $ word timestamp ts
           , EVM.vmoptBlockGaslimit = word gaslimit 0
           , EVM.vmoptGasprice      = word gasprice 0
           , EVM.vmoptMaxCodeSize   = word maxcodesize 0xffffffff
-          , EVM.vmoptDifficulty    = word difficulty 0
+          , EVM.vmoptDifficulty    = word difficulty diff
           , EVM.vmoptSchedule      = FeeSchedule.istanbul
           , EVM.vmoptChainId       = word chainid 1
           , EVM.vmoptCreate        = create cmd
@@ -711,7 +763,18 @@
 
 symvmFromCommand :: Command Options.Unwrapped -> Query EVM.VM
 symvmFromCommand cmd = do
+
+  (miner,blockNum,diff) <- case rpc cmd of
+    Nothing -> return (0,0,0)
+    Just url -> io $ EVM.Fetch.fetchBlockFrom block' url >>= \case
+      Nothing -> error $ "Could not fetch block"
+      Just EVM.Block{..} -> return (_coinbase
+                                   , wordValue _number
+                                   , wordValue _difficulty
+                                   )
+
   caller' <- maybe (SAddr <$> freshVar_) (return . litAddr) (caller cmd)
+  ts <- maybe (sw256 <$> freshVar_) (return . w256lit) (timestamp cmd)
   callvalue' <- maybe (sw256 <$> freshVar_) (return . w256lit) (value cmd)
   (calldata', cdlen, pathCond) <- case (calldata cmd, sig cmd) of
     -- fully abstract calldata (up to 1024 bytes)
@@ -742,34 +805,33 @@
     Just SymbolicS -> EVM.Symbolic <$> freshArray_ Nothing
     Nothing -> EVM.Symbolic <$> freshArray_ (if create cmd then (Just 0) else Nothing)
 
-  vm <- case (rpc cmd, address cmd, code cmd) of
+  withCache <- io $ applyCache (state cmd, cache cmd)
+
+  contract' <- case (rpc cmd, address cmd, code cmd) of
     (Just url, Just addr', _) ->
       io (EVM.Fetch.fetchContractFrom block' url addr') >>= \case
         Nothing ->
           error $ "contract not found."
-        Just contract' ->
-          return $
-            vm1 cdlen calldata' callvalue' caller' (contract'' & set EVM.storage store)
+        Just contract' -> return contract''
           where
             contract'' = case code cmd of
               Nothing -> contract'
               -- if both code and url is given,
               -- fetch the contract and overwrite the code
               Just c -> EVM.initialContract (codeType $ decipher c)
-                        & set EVM.storage     (view EVM.storage contract')
                         & set EVM.origStorage (view EVM.origStorage contract')
                         & set EVM.balance     (view EVM.balance contract')
                         & set EVM.nonce       (view EVM.nonce contract')
                         & set EVM.external    (view EVM.external contract')
 
     (_, _, Just c)  ->
-      return $
-        vm1 cdlen calldata' callvalue' caller' $
-          (EVM.initialContract . codeType $ decipher c) & set EVM.storage store
+      return $ (EVM.initialContract . codeType $ decipher c)
     (_, _, Nothing) ->
       error $ "must provide at least (rpc + address) or code"
 
-  return $ vm & over EVM.pathConditions (<> [pathCond])
+  return $ (VMTest.initTx $ withCache $ vm0 miner ts blockNum diff cdlen calldata' callvalue' caller' contract')
+    & over EVM.pathConditions (<> [pathCond])
+    & set (EVM.env . EVM.contracts . (ix address') . EVM.storage) store
 
   where
     decipher = hexByteString "bytes" . strip0x
@@ -779,7 +841,7 @@
     address' = if create cmd
           then createAddress origin' (word nonce 0)
           else addr address 0xacab
-    vm1 cdlen calldata' callvalue' caller' c = EVM.makeVm $ EVM.VMOpts
+    vm0 miner ts blockNum diff cdlen calldata' callvalue' caller' c = EVM.makeVm $ EVM.VMOpts
       { EVM.vmoptContract      = c
       , EVM.vmoptCalldata      = (calldata', cdlen)
       , EVM.vmoptValue         = callvalue'
@@ -788,13 +850,13 @@
       , EVM.vmoptOrigin        = origin'
       , EVM.vmoptGas           = word gas 0xffffffffffffffff
       , EVM.vmoptGaslimit      = word gas 0xffffffffffffffff
-      , EVM.vmoptCoinbase      = addr coinbase 0
-      , EVM.vmoptNumber        = word number 0
-      , EVM.vmoptTimestamp     = word timestamp 0
+      , EVM.vmoptCoinbase      = addr coinbase miner
+      , EVM.vmoptNumber        = word number blockNum
+      , EVM.vmoptTimestamp     = ts
       , EVM.vmoptBlockGaslimit = word gaslimit 0
       , EVM.vmoptGasprice      = word gasprice 0
       , EVM.vmoptMaxCodeSize   = word maxcodesize 0xffffffff
-      , EVM.vmoptDifficulty    = word difficulty 0
+      , EVM.vmoptDifficulty    = word difficulty diff
       , EVM.vmoptSchedule      = FeeSchedule.istanbul
       , EVM.vmoptChainId       = word chainid 1
       , EVM.vmoptCreate        = create cmd
diff --git a/hevm.cabal b/hevm.cabal
--- a/hevm.cabal
+++ b/hevm.cabal
@@ -2,7 +2,7 @@
 name:
   hevm
 version:
-  0.41.0
+  0.42.0
 synopsis:
   Ethereum virtual machine evaluator
 description:
@@ -81,10 +81,10 @@
   install-includes:
     ethjet/tinykeccak.h, ethjet/ethjet.h, ethjet/ethjet-ff.h, ethjet/blake2.h
   build-depends:
-    QuickCheck                        >= 2.13.2 && < 2.14,
+    QuickCheck                        >= 2.13.2 && < 2.15,
     containers                        >= 0.6.0 && < 0.7,
     deepseq                           >= 1.4.4 && < 1.5,
-    time                              >= 1.8.0 && < 1.9,
+    time                              >= 1.8.0 && < 1.11,
     transformers                      >= 0.5.6 && < 0.6,
     tree-view                         == 0.5,
     abstract-par                      >= 0.3.3 && < 0.4,
@@ -97,38 +97,37 @@
     vector                            >= 0.12.1 && < 0.13,
     ansi-wl-pprint                    >= 0.6.9 && < 0.7,
     base16-bytestring                 >= 0.1.1 && < 0.2,
-    brick                             >= 0.47.1 && < 0.48,
-    megaparsec                        >= 7.0.5 && < 7.1,
+    brick                             >= 0.47.1 && < 0.56,
+    megaparsec                        >= 7.0.5 && < 8.1,
     mtl                               >= 2.2.2 && < 2.3,
     directory                         >= 1.3.3 && < 1.4,
     filepath                          >= 1.4.2 && < 1.5,
-    vty                               >= 5.25.1 && < 5.26,
-    cborg                             >= 0.2.2 && < 0.3,
+    vty                               >= 5.25.1 && < 5.31,
     cereal                            >= 0.5.8 && < 0.6,
-    cryptonite                        >= 0.25 && < 0.26,
-    memory                            >= 0.14.18 && < 0.15,
+    cryptonite                        >= 0.25 && < 0.28,
+    memory                            >= 0.14.18 && < 0.16,
     data-dword                        >= 0.3.1 && < 0.4,
     fgl                               >= 5.7.0 && < 5.8,
     free                              >= 5.1.3 && < 5.2,
     haskeline                         >= 0.7.4 && < 0.8,
     process                           >= 1.6.5 && < 1.7,
-    lens                              >= 4.17.1 && < 4.18,
-    lens-aeson                        >= 1.0.2 && < 1.1,
+    lens                              >= 4.17.1 && < 4.20,
+    lens-aeson                        >= 1.0.2 && < 1.2,
     monad-par                         >= 0.3.5 && < 0.4,
     multiset                          >= 0.3.4 && < 0.4,
     operational                       >= 0.2.3 && < 0.3,
-    optparse-generic                  >= 1.3.1 && < 1.4,
+    optparse-generic                  >= 1.3.1 && < 1.5,
     quickcheck-text                   >= 0.1.2 && < 0.2,
     restless-git                      >= 0.7 && < 0.8,
     rosezipper                        >= 0.2 && < 0.3,
     s-cargot                          >= 0.1.4 && < 0.2,
-    sbv                               >= 8.7.5 && < 8.8,
+    sbv                               >= 8.7.5 && < 8.9,
     semver-range                      >= 0.2.7 && < 0.3,
     temporary                         >= 1.3 && < 1.4,
     text-format                       >= 0.3.2 && < 0.4,
     witherable                        >= 0.3.5 && < 0.4,
     wreq                              >= 0.5.3 && < 0.6,
-    regex-tdfa                        >= 1.2.3 && < 1.3,
+    regex-tdfa                        >= 1.2.3 && < 1.4,
     base                              >= 4.9 && < 5
   hs-source-dirs:
     src
diff --git a/src/EVM.hs b/src/EVM.hs
--- a/src/EVM.hs
+++ b/src/EVM.hs
@@ -128,7 +128,7 @@
 data Query where
   PleaseFetchContract :: Addr         -> (Contract   -> EVM ()) -> Query
   PleaseFetchSlot     :: Addr -> Word -> (Word       -> EVM ()) -> Query
-  PleaseAskSMT        :: SymWord -> [SBool] -> (JumpCondition -> EVM ()) -> Query
+  PleaseAskSMT        :: SBool -> [SBool] -> (BranchCondition -> EVM ()) -> Query
 
 data Choose where
   PleaseChoosePath    :: (Bool -> EVM ()) -> Choose
@@ -156,9 +156,9 @@
 
 type CodeLocation = (Addr, Int)
 
--- | The possible return values of a SMT query regarding JUMPI
-data JumpCondition = Iszero Bool | Unknown | Inconsistent
-  deriving (Show)
+-- | The possible return values of a SMT query
+data BranchCondition = Case Bool | Unknown | Inconsistent
+  deriving Show
 
 -- | The cache is data that can be persisted for efficiency:
 -- any expensive query that is constant at least within a block.
@@ -178,7 +178,7 @@
   , vmoptGas :: W256
   , vmoptGaslimit :: W256
   , vmoptNumber :: W256
-  , vmoptTimestamp :: W256
+  , vmoptTimestamp :: SymWord
   , vmoptCoinbase :: Addr
   , vmoptDifficulty :: W256
   , vmoptMaxCodeSize :: W256
@@ -207,7 +207,9 @@
     , creationContextSubstate  :: SubState
     }
   | CallContext
-    { callContextOffset    :: Word
+    { callContextTarget    :: Addr
+    , callContextContext   :: Addr
+    , callContextOffset    :: Word
     , callContextSize      :: Word
     , callContextCodehash  :: W256
     , callContextAbi       :: Maybe Word
@@ -325,13 +327,13 @@
 -- | Data about the block
 data Block = Block
   { _coinbase    :: Addr
-  , _timestamp   :: Word
+  , _timestamp   :: SymWord
   , _number      :: Word
   , _difficulty  :: Word
   , _gaslimit    :: Word
   , _maxCodeSize :: Word
   , _schedule    :: FeeSchedule Word
-  }
+  } deriving Show
 
 blankState :: FrameState
 blankState = FrameState
@@ -370,10 +372,20 @@
 
 instance Semigroup Cache where
   a <> b = Cache
-    { _fetched = mappend (view fetched a) (view fetched b),
-      _path = mappend (view path a) (view path b)
+    { _fetched = Map.unionWith unifyCachedContract (view fetched a) (view fetched b)
+    , _path = mappend (view path a) (view path b)
     }
 
+-- only intended for use in Cache merges, where we expect
+-- everything to be Concrete
+unifyCachedContract :: Contract -> Contract -> Contract
+unifyCachedContract a b = a & set storage merged
+  where merged = case (view storage a, view storage b) of
+                   (Concrete sa, Concrete sb) ->
+                     Concrete (mappend sa sb)
+                   _ ->
+                     view storage a
+
 instance Monoid Cache where
   mempty = Cache { _fetched = mempty,
                    _path = mempty
@@ -406,7 +418,7 @@
   , _traces = Zipper.fromForest []
   , _block = Block
     { _coinbase = vmoptCoinbase o
-    , _timestamp = w256 $ vmoptTimestamp o
+    , _timestamp = vmoptTimestamp o
     , _number = w256 $ vmoptNumber o
     , _difficulty = w256 $ vmoptDifficulty o
     , _maxCodeSize = w256 $ vmoptMaxCodeSize o
@@ -436,9 +448,7 @@
     , _keccakUsed = mempty
     , _storageModel = vmoptStorageModel o
     }
-  , _cache = Cache (Map.fromList
-    [(vmoptAddress o, vmoptContract o)])
-    mempty
+  , _cache = Cache mempty mempty
   , _burned = 0
   , _pathConditions = []
   , _iterations = mempty
@@ -455,14 +465,15 @@
       keccak (stripBytecodeMetadata theCode)
   , _storage  = Concrete mempty
   , _balance  = 0
-  , _nonce    = 0
+  , _nonce    = if creation then 1 else 0
   , _opIxMap  = mkOpIxMap theCode
   , _codeOps  = mkCodeOps theCode
   , _external = False
   , _origStorage = mempty
-  } where theCode = case theContractCode of
-            InitCode b    -> b
-            RuntimeCode b -> b
+  } where
+      (creation, theCode) = case theContractCode of
+            InitCode b    -> (True, b)
+            RuntimeCode b -> (False, b)
 
 contractWithStore :: ContractCode -> Storage -> Contract
 contractWithStore theContractCode store =
@@ -643,7 +654,7 @@
         -- op: SHL
         0x1b -> stackOp2 (const g_verylow) $ \((S _ n), (S _ x)) -> sw256 $ sShiftLeft x n
         -- op: SHR
-        0x1c -> stackOp2 (const g_verylow) $ \((S _ n), (S _ x)) -> sw256 $ sShiftRight x n
+        0x1c -> stackOp2 (const g_verylow) $ uncurry shiftRight'
         -- op: SAR
         0x1d -> stackOp2 (const g_verylow) $ \((S _ n), (S _ x)) -> sw256 $ sSignedShiftArithRight x n
 
@@ -850,7 +861,7 @@
         -- op: TIMESTAMP
         0x42 ->
           limitStack 1 . burn g_base $
-            next >> push (the block timestamp)
+            next >> pushSym (the block timestamp)
 
         -- op: NUMBER
         0x43 ->
@@ -996,7 +1007,7 @@
                   in case maybeLitWord y of
                       Just y' -> jump (0 == y')
                       -- if the jump condition is symbolic, an smt query has to be made.
-                      Nothing -> askSMT (self, the state pc) y jump
+                      Nothing -> askSMT (self, the state pc) (0 .== y) jump
             _ -> underrun
 
         -- op: PC
@@ -1075,9 +1086,7 @@
                               assign callvalue (litWord xValue)
                               assign caller (litAddr self)
                               assign contract xTo
-                            zoom (env . contracts) $ do
-                              ix self . balance -= xValue
-                              ix xTo  . balance += xValue
+                            transfer self xTo xValue
                             touchAccount self
                             touchAccount xTo
             _ ->
@@ -1246,6 +1255,12 @@
         xxx ->
           vmError (UnrecognizedOpcode xxx)
 
+transfer :: Addr -> Addr -> Word -> EVM ()
+transfer xFrom xTo xValue =
+  zoom (env . contracts) $ do
+    ix xFrom . balance -= xValue
+    ix xTo  . balance += xValue
+
 -- | Checks a *CALL for failure; OOG, too many callframes, memory access etc.
 callChecks
   :: (?op :: Word8)
@@ -1299,9 +1314,7 @@
         Just 1 ->
           fetchAccount recipient $ \_ -> do
 
-          zoom (env . contracts) $ do
-            ix self . balance -= xValue
-            ix recipient  . balance += xValue
+          transfer self recipient xValue
           touchAccount self
           touchAccount recipient
           touchAccount precompileAddr
@@ -1509,8 +1522,8 @@
 getCodeLocation vm = (view (state . contract) vm, view (state . pc) vm)
 
 -- | Construct SMT Query and halt execution until resolved
-askSMT :: CodeLocation -> SymWord -> (Bool -> EVM ()) -> EVM ()
-askSMT codeloc jumpcondition continue = do
+askSMT :: CodeLocation -> SBool -> (Bool -> EVM ()) -> EVM ()
+askSMT codeloc condition continue = do
   -- We keep track of how many times we have come across this particular
   -- (contract, pc) combination in the `iteration` mapping.
   iteration <- use (iterations . at codeloc . non 0)
@@ -1519,23 +1532,23 @@
   -- already. So we first check the cache to see if the result is known
   use (cache . path . at (codeloc, iteration)) >>= \case
      -- If the query has been done already, select path or select the only available
-     Just w -> choosePath (Iszero w)
+     Just w -> choosePath (Case w)
      -- If this is a new query, run the query, cache the result
      -- increment the iterations and select appropriate path
      Nothing -> do pathconds <- use pathConditions
                    assign result . Just . VMFailure . Query $ PleaseAskSMT
-                     jumpcondition pathconds choosePath
+                     condition pathconds choosePath
 
    where -- Only one path is possible
-         choosePath :: JumpCondition -> EVM ()
-         choosePath (Iszero v) = do assign result Nothing
-                                    pathConditions <>= if v then [litWord 0 .== jumpcondition] else [litWord 0 ./= jumpcondition]
-                                    iteration <- use (iterations . at codeloc . non 0)
-                                    assign (cache . path . at (codeloc, iteration)) (Just v)
-                                    assign (iterations . at codeloc) (Just (iteration + 1))
-                                    continue v
+         choosePath :: BranchCondition -> EVM ()
+         choosePath (Case v) = do assign result Nothing
+                                  pushTo pathConditions (if v then condition else sNot condition)
+                                  iteration <- use (iterations . at codeloc . non 0)
+                                  assign (cache . path . at (codeloc, iteration)) (Just v)
+                                  assign (iterations . at codeloc) (Just (iteration + 1))
+                                  continue v
          -- Both paths are possible; we ask for more input
-         choosePath Unknown = assign result . Just . VMFailure . Choose . PleaseChoosePath $ choosePath . Iszero
+         choosePath Unknown = assign result . Just . VMFailure . Choose . PleaseChoosePath $ choosePath . Case
          -- None of the paths are possible; fail this branch
          choosePath Inconsistent = vmError DeadPath
 
@@ -1814,46 +1827,47 @@
     input = readMemory (inOffset + 4) (inSize - 4) vm
   case fromSized <$> unliteral abi of
     Nothing -> vmError UnexpectedSymbolicArg
-    Just abi ->
-              case Map.lookup abi cheatActions of
-                Nothing ->
-                  vmError (BadCheatCode (Just abi))
-                Just (argTypes, action) ->
-                  case input of
-                    SymbolicBuffer _ -> vmError UnexpectedSymbolicArg
-                    ConcreteBuffer input' ->
-                      case runGetOrFail
-                             (getAbiSeq (length argTypes) argTypes)
-                             (LS.fromStrict input') of
-                        Right ("", _, args) ->
-                          action (toList args) >>= \case
-                            Nothing -> do
-                              next
-                              push 1
-                            Just (encodeAbiValue -> bs) -> do
-                              next
-                              modifying (state . memory)
-                                (writeMemory (ConcreteBuffer bs) outSize 0 outOffset)
-                              push 1
-                        _ ->
-                          vmError (BadCheatCode (Just abi))
+    Just abi' ->
+      case Map.lookup abi' cheatActions of
+        Nothing ->
+          vmError (BadCheatCode (Just abi'))
+        Just (argTypes, action) ->
+          case input of
+            SymbolicBuffer _ -> vmError UnexpectedSymbolicArg
+            ConcreteBuffer input' ->
+              case runGetOrFail
+                     (getAbiSeq (length argTypes) argTypes)
+                     (LS.fromStrict input') of
+                Right ("", _, args) -> do
+                  action outOffset outSize (toList args)
+                  next
+                  push 1
+                _ ->
+                  vmError (BadCheatCode (Just abi'))
 
-type CheatAction = ([AbiType], [AbiValue] -> EVM (Maybe AbiValue))
+type CheatAction = ([AbiType], Word -> Word -> [AbiValue] -> EVM ())
 
 cheatActions :: Map Word32 CheatAction
 cheatActions =
   Map.fromList
     [ action "warp(uint256)" [AbiUIntType 256] $
-        \[AbiUInt 256 x] -> do
-          assign (block . timestamp) (w256 (W256 x))
-          return Nothing,
+        \_ _ [AbiUInt 256 x] ->
+          assign (block . timestamp) (sw256 $ num x),
+      action "roll(uint256)" [AbiUIntType 256] $
+        \_ _ [AbiUInt 256 x] ->
+          assign (block . number) (w256 (W256 x)),
       action "store(address,bytes32,bytes32)" [AbiAddressType, AbiBytesType 32, AbiBytesType 32] $
-        \[AbiAddress a, AbiBytes 32 x, AbiBytes 32 y] -> do
+        \_ _ [AbiAddress a, AbiBytes 32 x, AbiBytes 32 y] -> do
           let slot = w256lit $ word x
               new  = w256lit $ word y
           fetchAccount a $ \_ -> do
-            modifying (env . contracts . ix a . storage) (writeStorage slot new)
-          return Nothing
+            modifying (env . contracts . ix a . storage) (writeStorage slot new),
+      action "load(address,bytes32)" [AbiAddressType, AbiBytesType 32] $
+        \outOffset _ [AbiAddress a, AbiBytes 32 x] -> do
+          let slot = w256lit $ word x
+          accessStorage a slot $ \res -> do
+            assign (state . returndata . word256At 0) res
+            assign (state . memory . word256At outOffset) res
     ]
   where
     action s ts f = (abiKeccak s, (ts, f))
@@ -1875,11 +1889,13 @@
         Just target ->
           burn xGas $ do
             let newContext = CallContext
-                  { callContextOffset = xOutOffset
-                  , callContextSize = xOutSize
-                  , callContextCodehash = view codehash target
+                  { callContextTarget    = xTo
+                  , callContextContext   = xContext
+                  , callContextOffset    = xOutOffset
+                  , callContextSize      = xOutSize
+                  , callContextCodehash  = view codehash target
                   , callContextReversion = view (env . contracts) vm0
-                  , callContextSubState = view (tx . substate) vm0
+                  , callContextSubState  = view (tx . substate) vm0
                   , callContextAbi =
                       if xInSize >= 4
                       then case unliteral $ readMemoryWord32 xInOffset (view (state . memory) vm0)
@@ -1959,15 +1975,13 @@
 
         zoom (env . contracts) $ do
           oldAcc <- use (at newAddr)
-          let oldBal = case oldAcc of
-                Nothing -> 0
-                Just c  -> view balance c
-          assign (at newAddr) (Just newContract)
-          assign (ix newAddr . balance) (oldBal + xValue)
-          assign (ix newAddr . nonce) 1
-          modifying (ix self . balance) (flip (-) xValue)
+          let oldBal = maybe 0 (view balance) oldAcc
+
+          assign (at newAddr) (Just (newContract & balance .~ oldBal))
           modifying (ix self . nonce) succ
 
+        transfer self newAddr xValue
+
         pushTrace (FrameTrace newContext)
         next
         vm1 <- get
@@ -1999,7 +2013,7 @@
           & set balance (view balance now)
           & set nonce   (view nonce now)
         RuntimeCode _ ->
-          error "internal error: can't replace code of deployed contract"
+          error ("internal error: can't replace code of deployed contract " <> show target)
       Nothing ->
         error "internal error: can't replace code of nonexistent contract"
 
@@ -2084,7 +2098,7 @@
       case view frameContext nextFrame of
 
         -- Were we calling?
-        CallContext (num -> outOffset) (num -> outSize) _ _ _ reversion substate' -> do
+        CallContext _ _ (num -> outOffset) (num -> outSize) _ _ _ reversion substate' -> do
 
           let
             revertContracts = assign (env . contracts) reversion
diff --git a/src/EVM/ABI.hs b/src/EVM/ABI.hs
--- a/src/EVM/ABI.hs
+++ b/src/EVM/ABI.hs
@@ -30,6 +30,8 @@
 module EVM.ABI
   ( AbiValue (..)
   , AbiType (..)
+  , AbiKind (..)
+  , abiKind
   , Event (..)
   , Anonymity (..)
   , Indexed (..)
@@ -437,7 +439,7 @@
    AbiTupleType ts ->
      AbiTuple <$> mapM genAbiValue ts
   where
-    genUInt n = AbiUInt n <$> arbitraryIntegralWithMax n
+    genUInt n = AbiUInt n <$> arbitraryIntegralWithMax (2^n-1)
 
 instance Arbitrary AbiType where
   arbitrary = sized $ \n -> oneof $ -- prevent empty tuples
@@ -533,7 +535,7 @@
 -- Essentially a mix between three types of generators:
 -- one that strongly prefers values close to 0, one that prefers values close to max
 -- and one that chooses uniformly.
-arbitraryIntegralWithMax :: (Integral a) => Int -> Gen a
+arbitraryIntegralWithMax :: (Integral a) => Integer -> Gen a
 arbitraryIntegralWithMax maxbound =
   sized $ \s ->
     do let mn = 0 :: Int
diff --git a/src/EVM/Concrete.hs b/src/EVM/Concrete.hs
--- a/src/EVM/Concrete.hs
+++ b/src/EVM/Concrete.hs
@@ -7,7 +7,7 @@
 
 import EVM.Keccak (keccak)
 import EVM.RLP
-import EVM.Types (Addr, W256 (..), num, word, padRight, word160Bytes, word256Bytes)
+import EVM.Types (Addr, W256 (..), num, word, padRight, word160Bytes, word256Bytes, Buffer)
 
 import Control.Lens    ((^?), ix)
 import Data.Bits       (Bits (..), FiniteBits (..), shiftL, shiftR)
@@ -40,6 +40,7 @@
 data Whiff = Dull
            | FromKeccak ByteString
            | Var String
+           | FromBytes Buffer
            | InfixBinOp String Whiff Whiff
            | BinOp String Whiff Whiff
            | UnOp String Whiff
diff --git a/src/EVM/Dev.hs b/src/EVM/Dev.hs
--- a/src/EVM/Dev.hs
+++ b/src/EVM/Dev.hs
@@ -20,6 +20,10 @@
 import qualified Data.Map as Map
 import qualified Data.ByteString.Lazy   as LazyByteString
 
+concatMapM :: Monad m => (a -> m [b]) -> [a] -> m [b]
+concatMapM op = foldr f (pure [])
+    where f x xs = do x <- op x; if null x then xs else do xs <- xs; pure $ x++xs
+
 loadDappInfo :: String -> String -> IO DappInfo
 loadDappInfo path file =
   withCurrentDirectory path $
@@ -40,7 +44,7 @@
         Just repoPath -> do
           facts <- Git.loadFacts (Git.RepoAt repoPath)
           pure (flip Facts.apply facts)
-    params <- getParametersFromEnvironmentVariables
+    params <- getParametersFromEnvironmentVariables Nothing
     let
       opts = UnitTestOptions
         { oracle = EVM.Fetch.zero
@@ -56,7 +60,10 @@
       \case
         Just (contractMap, cache) -> do
           let unitTests = findUnitTests ("test" `isPrefixOf`) (Map.elems contractMap)
-          mapM (runUnitTestContract opts contractMap cache) unitTests
+          results <- concatMapM (runUnitTestContract opts contractMap cache) unitTests
+          let (passing, _) = unzip results
+          pure passing
+
         Nothing ->
           error ("Failed to read Solidity JSON for `" ++ path ++ "'")
 
@@ -90,7 +97,7 @@
         Just repoPath -> do
           facts <- Git.loadFacts (Git.RepoAt repoPath)
           pure (flip Facts.apply facts)
-    params <- getParametersFromEnvironmentVariables
+    params <- getParametersFromEnvironmentVariables Nothing
     let
       testOpts = UnitTestOptions
         { oracle = EVM.Fetch.zero
diff --git a/src/EVM/Emacs.hs b/src/EVM/Emacs.hs
--- a/src/EVM/Emacs.hs
+++ b/src/EVM/Emacs.hs
@@ -516,7 +516,7 @@
 
 defaultUnitTestOptions :: MonadIO m => m UnitTestOptions
 defaultUnitTestOptions = do
-  params <- liftIO getParametersFromEnvironmentVariables
+  params <- liftIO $ getParametersFromEnvironmentVariables Nothing
   pure UnitTestOptions
     { oracle            = Fetch.zero
     , verbose           = Nothing
diff --git a/src/EVM/Facts.hs b/src/EVM/Facts.hs
--- a/src/EVM/Facts.hs
+++ b/src/EVM/Facts.hs
@@ -27,16 +27,18 @@
   , Data (..)
   , Path (..)
   , apply
+  , applyCache
+  , cacheFacts
   , contractFacts
   , vmFacts
   , factToFile
   , fileToFact
   ) where
 
-import EVM          (VM, Contract)
+import EVM          (VM, Contract, Cache)
 import EVM.Concrete (Word)
 import EVM.Symbolic (litWord, SymWord, forceLit)
-import EVM          (balance, nonce, storage, bytecode, env, contracts, contract, state)
+import EVM          (balance, nonce, storage, bytecode, env, contracts, contract, state, cache, fetched)
 import EVM.Types    (Addr)
 
 import qualified EVM
@@ -129,6 +131,11 @@
       , which = fromIntegral k
       }
 
+cacheFacts :: Cache -> Set Fact
+cacheFacts c = Set.fromList $ do
+  (k, v) <- Map.toList (view EVM.fetched c)
+  contractFacts k v
+
 vmFacts :: VM -> Set Fact
 vmFacts vm = Set.fromList $ do
   (k, v) <- Map.toList (view (env . contracts) vm)
@@ -154,6 +161,19 @@
     NonceFact   {..} ->
       vm & set (env . contracts . ix addr . nonce) what
 
+apply2 :: VM -> Fact -> VM
+apply2 vm fact =
+  case fact of
+    CodeFact    {..} -> flip execState vm $ do
+      assign (cache . fetched . at addr) (Just (EVM.initialContract (EVM.RuntimeCode blob)))
+      when (view (state . contract) vm == addr) $ EVM.loadContract addr
+    StorageFact {..} ->
+      vm & over (cache . fetched . ix addr . storage) (EVM.writeStorage (litWord which) (litWord what))
+    BalanceFact {..} ->
+      vm & set (cache . fetched . ix addr . balance) what
+    NonceFact   {..} ->
+      vm & set (cache . fetched . ix addr . nonce) what
+
 -- Sort facts in the right order for `apply1` to work.
 instance Ord Fact where
   compare = comparing f
@@ -169,6 +189,12 @@
 apply =
   -- The set's ordering is relevant; see `apply1`.
   foldl apply1
+--
+-- Applies a set of facts to a VM.
+applyCache :: VM -> Set Fact -> VM
+applyCache =
+  -- The set's ordering is relevant; see `apply1`.
+  foldl apply2
 
 factToFile :: Fact -> File
 factToFile fact = case fact of
diff --git a/src/EVM/Fetch.hs b/src/EVM/Fetch.hs
--- a/src/EVM/Fetch.hs
+++ b/src/EVM/Fetch.hs
@@ -1,5 +1,6 @@
 {-# Language GADTs #-}
 {-# Language StandaloneDeriving #-}
+{-# Language LambdaCase #-}
 
 module EVM.Fetch where
 
@@ -7,7 +8,9 @@
 
 import EVM.Types    (Addr, W256, hexText)
 import EVM.Concrete (Word, w256)
-import EVM          (EVM, Contract, StorageModel, initialContract, nonce, balance, external)
+import EVM.Symbolic (litWord)
+import EVM          (EVM, Contract, Block, StorageModel, initialContract, nonce, balance, external)
+import qualified EVM.FeeSchedule as FeeSchedule
 
 import qualified EVM
 
@@ -20,7 +23,7 @@
 import Data.Aeson
 import Data.Aeson.Lens
 import Data.ByteString (ByteString)
-import Data.Text (Text, unpack)
+import Data.Text (Text, unpack, pack)
 import Network.Wreq
 import Network.Wreq.Session (Session)
 
@@ -29,6 +32,7 @@
 -- | Abstract representation of an RPC fetch request
 data RpcQuery a where
   QueryCode    :: Addr         -> RpcQuery ByteString
+  QueryBlock   ::                 RpcQuery Block
   QueryBalance :: Addr         -> RpcQuery W256
   QueryNonce   :: Addr         -> RpcQuery W256
   QuerySlot    :: Addr -> W256 -> RpcQuery W256
@@ -38,7 +42,7 @@
 
 deriving instance Show (RpcQuery a)
 
-rpc :: String -> [String] -> Value
+rpc :: String -> [Value] -> Value
 rpc method args = object
   [ "jsonrpc" .= ("2.0" :: String)
   , "id"      .= Number 1
@@ -47,17 +51,20 @@
   ]
 
 class ToRPC a where
-  toRPC :: a -> String
+  toRPC :: a -> Value
 
 instance ToRPC Addr where
-  toRPC = show
+  toRPC = String . pack . show
 
 instance ToRPC W256 where
-  toRPC = show
+  toRPC = String . pack . show
 
+instance ToRPC Bool where
+  toRPC = Bool
+
 instance ToRPC BlockNumber where
-  toRPC Latest          = "latest"
-  toRPC (BlockNumber n) = show n
+  toRPC Latest          = String "latest"
+  toRPC (BlockNumber n) = String . pack $ show n
 
 readText :: Read a => Text -> a
 readText = read . unpack
@@ -65,32 +72,45 @@
 fetchQuery
   :: Show a
   => BlockNumber
-  -> (Value -> IO (Maybe Text))
+  -> (Value -> IO (Maybe Value))
   -> RpcQuery a
   -> IO (Maybe a)
 fetchQuery n f q = do
   x <- case q of
-    QueryCode addr ->
-      fmap hexText  <$>
-        f (rpc "eth_getCode" [toRPC addr, toRPC n])
-    QueryNonce addr ->
-      fmap readText <$>
-        f (rpc "eth_getTransactionCount" [toRPC addr, toRPC n])
-    QueryBalance addr ->
-      fmap readText <$>
-        f (rpc "eth_getBalance" [toRPC addr, toRPC n])
-    QuerySlot addr slot ->
-      fmap readText <$>
-        f (rpc "eth_getStorageAt" [toRPC addr, toRPC slot, toRPC n])
-    QueryChainId ->
-      fmap readText <$>
-        f (rpc "eth_chainId" [toRPC n])
+    QueryCode addr -> do
+        m <- f (rpc "eth_getCode" [toRPC addr, toRPC n])
+        return $ hexText <$> view _String <$> m
+    QueryNonce addr -> do
+        m <- f (rpc "eth_getTransactionCount" [toRPC addr, toRPC n])
+        return $ readText <$> view _String <$> m
+    QueryBlock -> do
+      m <- f (rpc "eth_getBlockByNumber" [toRPC n, toRPC False])
+      return $ m >>= parseBlock
+    QueryBalance addr -> do
+        m <- f (rpc "eth_getBalance" [toRPC addr, toRPC n])
+        return $ readText <$> view _String <$> m
+    QuerySlot addr slot -> do
+        m <- f (rpc "eth_getStorageAt" [toRPC addr, toRPC slot, toRPC n])
+        return $ readText <$> view _String <$> m
+    QueryChainId -> do
+        m <- f (rpc "eth_chainId" [toRPC n])
+        return $ readText <$> view _String <$> m
   return x
 
-fetchWithSession :: Text -> Session -> Value -> IO (Maybe Text)
+
+parseBlock :: (AsValue s, Show s) => s -> Maybe EVM.Block
+parseBlock json = do
+  coinbase   <- readText <$> json ^? key "miner" . _String
+  timestamp  <- litWord <$> readText <$> json ^? key "timestamp" . _String
+  number     <- readText <$> json ^? key "number" . _String
+  difficulty <- readText <$> json ^? key "difficulty" . _String
+  -- default codesize, default gas limit, default feescedule
+  return $ EVM.Block coinbase timestamp number difficulty 0xffffffff 0xffffffff FeeSchedule.istanbul
+
+fetchWithSession :: Text -> Session -> Value -> IO (Maybe Value)
 fetchWithSession url sess x = do
   r <- asValue =<< Session.post sess (unpack url) x
-  return (r ^? responseBody . key "result" . _String)
+  return (r ^? responseBody . key "result")
 
 fetchContractWithSession
   :: BlockNumber -> Text -> Addr -> Session -> IO (Maybe Contract)
@@ -115,6 +135,16 @@
   fmap w256 <$>
     fetchQuery n (fetchWithSession url sess) (QuerySlot addr slot)
 
+fetchBlockWithSession
+  :: BlockNumber -> Text -> Session -> IO (Maybe Block)
+fetchBlockWithSession n url sess =
+  fetchQuery n (fetchWithSession url sess) QueryBlock
+
+fetchBlockFrom :: BlockNumber -> Text -> IO (Maybe Block)
+fetchBlockFrom n url =
+  Session.withAPISession
+    (fetchBlockWithSession n url)
+
 fetchContractFrom :: BlockNumber -> Text -> Addr -> IO (Maybe Contract)
 fetchContractFrom n url addr =
   Session.withAPISession
@@ -126,91 +156,109 @@
     (\s -> fetchSlotWithSession n url s addr slot)
 
 http :: BlockNumber -> Text -> Fetcher
-http n url q =
-  case q of
-    EVM.PleaseFetchContract addr continue ->
-      fetchContractFrom n url addr >>= \case
-        Just x  ->
-          return (continue x)
-        Nothing -> error ("oracle error: " ++ show q)
-    EVM.PleaseFetchSlot addr slot continue ->
-      fetchSlotFrom n url addr (fromIntegral slot) >>= \case
-        Just x  -> return (continue x)
-        Nothing -> error ("oracle error: " ++ show q)
-    EVM.PleaseAskSMT _ _ _ -> error "smt calls not available for this oracle"
-
-zero :: Fetcher
-zero q =
-  case q of
-    EVM.PleaseFetchContract _ continue ->
-      return (continue (initialContract (EVM.RuntimeCode mempty)))
-    EVM.PleaseFetchSlot _ _ continue ->
-      return (continue 0)
-    EVM.PleaseAskSMT _ _ continue ->
-      return $ continue EVM.Unknown
-
-
-
-type Fetcher = EVM.Query -> IO (EVM ())
+http n url = oracle Nothing (Just (n, url)) EVM.ConcreteS True
 
 -- smtsolving + (http or zero)
-oracle :: SBV.State -> Maybe (BlockNumber, Text) -> StorageModel -> Fetcher
-oracle state info model q = do
+oracle :: Maybe SBV.State -> Maybe (BlockNumber, Text) -> StorageModel -> Bool -> Fetcher
+oracle smtstate info model ensureConsistency q = do
   case q of
-    EVM.PleaseAskSMT jumpcondition pathconditions continue ->
-      flip runReaderT state $ SBV.runQueryT $ do
+    EVM.PleaseAskSMT branchcondition pathconditions continue ->
+      case smtstate of
+        Nothing -> return $ continue EVM.Unknown
+        Just state -> flip runReaderT state $ SBV.runQueryT $ do
          let pathconds = sAnd pathconditions
-         noJump <- checksat $ pathconds .&& jumpcondition ./= 0
-         case noJump of
-            -- Unsat means condition
-            -- cannot be nonzero
-            Unsat -> do jump <- checksat $ pathconds .&& jumpcondition .== 0
-                        -- can it be zero?
-                        case jump of
-                          -- No. We are on an inconsistent path.
-                          Unsat -> return $ continue EVM.Inconsistent
-                          -- Yes. It must be 0.
-                          Sat -> return $ continue (EVM.Iszero True)
-                          -- Assume 0 is still possible.
-                          Unk -> return $ continue (EVM.Iszero True)
-            -- Sat means its possible for condition
-            -- to be nonzero.
-            Sat -> do jump <- checksat $ pathconds .&& jumpcondition .== 0
-                      -- can it also be zero?
-                      case jump of
-                        -- No. It must be nonzero
-                        Unsat -> return $ continue (EVM.Iszero False)
-                        -- Yes. Both branches possible
-                        Sat -> return $ continue EVM.Unknown
-                        -- Explore both branches in case of timeout
-                        Unk -> return $ continue EVM.Unknown
+         -- Is is possible to satisfy the condition?
+         continue <$> checkBranch pathconds branchcondition ensureConsistency
 
-            -- If the query times out, we simply explore both paths
-            Unk -> return $ continue EVM.Unknown
     -- if we are using a symbolic storage model,
     -- 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 mempty)
                     Just (n, url) -> fetchContractFrom n url addr
       case contract of
-        Just x  -> case model of
+        Just x -> case model of
           EVM.ConcreteS -> return $ continue x
-          EVM.InitialS  -> return $ continue $ x & set EVM.storage (EVM.Symbolic $ SBV.sListArray 0 [])
-          EVM.SymbolicS -> 
-            flip runReaderT state $ SBV.runQueryT $ do
-              store <- freshArray_ Nothing
-              return $ continue $ x & set EVM.storage (EVM.Symbolic store)
+          EVM.InitialS  -> return $ continue $ x
+             & set EVM.storage (EVM.Symbolic $ SBV.sListArray 0 [])
+          EVM.SymbolicS -> case smtstate of
+            Nothing -> return (continue $ x
+                               & set EVM.storage (EVM.Symbolic $ SBV.sListArray 0 []))
+
+            Just state ->
+              flip runReaderT state $ SBV.runQueryT $ do
+                store <- freshArray_ Nothing
+                return $ continue $ x
+                  & set EVM.storage (EVM.Symbolic store)
         Nothing -> error ("oracle error: " ++ show q)
 
     --- for other queries (there's only slot left right now) we default to zero or http
-    _ -> case info of
-      Nothing -> zero q
-      Just (n, url) -> http n url q
+    EVM.PleaseFetchSlot addr slot continue ->
+      case info of
+        Nothing -> return (continue 0)
+        Just (n, url) ->
+         fetchSlotFrom n url addr (fromIntegral slot) >>= \case
+           Just x  -> return (continue x)
+           Nothing ->
+             error ("oracle error: " ++ show q)
 
+zero :: Fetcher
+zero = oracle Nothing Nothing EVM.ConcreteS True
+
+type Fetcher = EVM.Query -> IO (EVM ())
+
 checksat :: SBool -> Query CheckSatResult
-checksat b = do resetAssertions
+checksat b = do push 1
                 constrain b
                 m <- checkSat
-                resetAssertions
+                pop 1
                 return m
+
+-- | Checks which branches are satisfiable, checking the pathconditions for consistency
+-- if the third argument is true.
+-- When in debug mode, we do not want to be able to navigate to dead paths,
+-- but for normal execution paths with inconsistent pathconditions
+-- will be pruned anyway.
+checkBranch :: SBool -> SBool -> Bool -> Query EVM.BranchCondition
+checkBranch pathconds branchcondition False = do
+  constrain pathconds
+  checksat branchcondition >>= \case
+     -- the condition is unsatisfiable
+     Unsat -> -- if pathconditions are consistent then the condition must be false
+            return $ EVM.Case False
+     -- Sat means its possible for condition to hold
+     Sat -> -- is its negation also possible?
+            checksat (sNot branchcondition) >>= \case
+               -- No. The condition must hold
+               Unsat -> return $ EVM.Case True
+               -- Yes. Both branches possible
+               Sat -> return EVM.Unknown
+               -- Explore both branches in case of timeout
+               Unk -> return EVM.Unknown
+     -- If the query times out, we simply explore both paths
+     Unk -> return EVM.Unknown
+
+checkBranch pathconds branchcondition True = do
+  constrain pathconds
+  checksat branchcondition >>= \case
+     -- the condition is unsatisfiable
+     Unsat -> -- are the pathconditions even consistent?
+              checksat (sNot branchcondition) >>= \case
+                -- No. We are on an inconsistent path.
+                Unsat -> return EVM.Inconsistent
+                -- Yes. The condition must be false.
+                Sat -> return $ EVM.Case False
+                -- Assume the negated condition is still possible.
+                Unk -> return $ EVM.Case False
+     -- Sat means its possible for condition to hold
+     Sat -> -- is its negation also possible?
+            checksat (sNot branchcondition) >>= \case
+               -- No. The condition must hold
+               Unsat -> return $ EVM.Case True
+               -- Yes. Both branches possible
+               Sat -> return EVM.Unknown
+               -- Explore both branches in case of timeout
+               Unk -> return EVM.Unknown
+
+     -- If the query times out, we simply explore both paths
+     Unk -> return EVM.Unknown
diff --git a/src/EVM/Flatten.hs b/src/EVM/Flatten.hs
--- a/src/EVM/Flatten.hs
+++ b/src/EVM/Flatten.hs
@@ -18,7 +18,7 @@
 -- 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)
+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!)
@@ -36,10 +36,10 @@
 import Data.ByteString (ByteString)
 import Data.Foldable (foldl', toList)
 import Data.List (sort, nub)
-import Data.Map (Map, (!))
-import Data.Maybe (mapMaybe, isJust)
+import Data.Map (Map, (!), (!?))
+import Data.Maybe (mapMaybe, isJust, catMaybes, fromMaybe)
 import Data.Monoid ((<>))
-import Data.Text (Text, unpack, pack)
+import Data.Text (Text, unpack, pack, intercalate)
 import Data.Text.Encoding (encodeUtf8)
 import Text.Read (readMaybe)
 
@@ -97,6 +97,57 @@
     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 = mconcat $ fmap f $ Map.elems asts
+        xs' = repeated $ fmap snd xs
+        scope = preview (key "attributes" . key "scope" . _Integer)
+        name = preview (key "attributes" . key "name" . _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 = preview (key "attributes" . key "scope" . _Integer)
+        cname = preview (key "attributes" . key "canonicalName" . _String)
+        id' = preview (key "id" . _Integer)
+        p x = (nodeIs "StructDefinition" x)
+          && (fromJust' "line:137 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
@@ -116,7 +167,7 @@
 
         -- Take the highest Solidity version from all pragmas.
         pragma :: Text
-        pragma = maximalPragma (Map.elems asts)
+        pragma = maximalPragma (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.
@@ -125,7 +176,13 @@
           src <- BS.readFile (unpack path)
           pure $ mconcat
             [ "////// ", encodeUtf8 path, "\n"
-            , stripImportsAndPragmas src (asts ! path), "\n"
+            -- Fold over a list of source transforms
+            , fst
+                (prefixContractAst
+                  contractsAndStructsToRename
+                  contractStructs
+                  (stripImportsAndPragmas (src, 0) (asts ! path))
+                  (asts ! path)), "\n"
             ]
 
       -- Force all evaluation before any printing happens, to avoid
@@ -140,15 +197,43 @@
 -- 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
-    [] -> error "no Solidity version pragmas in any source files"
-    xs ->
-      "pragma solidity "
-        <> pack (show (rangeIntersection xs))
-        <> ";\n"
+maximalPragma asts = (
+    case mapMaybe versions asts of
+      [] -> error "no Solidity version pragmas in any source files"
+      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 =
+      \case
+        String "solidity" : _ -> True
+        _ -> False
+
+    pragmaComponents :: Value -> [[Value]]
+    pragmaComponents ast = components
+      where
+        ps :: [Value]
+        ps = filter (nodeIs "PragmaDirective") (universe ast)
+
+        components :: [[Value]]
+        components = catMaybes $ fmap
+          ((fmap toList) . preview (key "attributes" . key "literals" . _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".
@@ -160,30 +245,26 @@
     versions :: Value -> Maybe SemVerRange
     versions ast = fmap grok components
       where
-        pragma :: Maybe Value
-        pragma =
-          case filter (nodeIs "PragmaDirective") (universe ast) of
-            [x] -> Just x
-            []  -> Nothing
-            _   -> error "multiple version pragmas"
-
         components :: Maybe [Value]
-        components = fmap toList
-          (pragma >>= preview (key "attributes" . key "literals" . _Array))
+        components =
+          case filter isVersionPragma (pragmaComponents ast) of
+            [_:xs] -> Just xs
+            []  -> Nothing
+            x   -> error $ "multiple version pragmas" ++ show x
 
         grok :: [Value] -> SemVerRange
-        grok = \case
-          String "solidity" : 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)
-          x ->
-            error ("unrecognized pragma: " ++ show x)
+        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
@@ -192,29 +273,20 @@
     hasRightName =
       Just t == preview (key "name" . _String) x
 
-stripImportsAndPragmas :: ByteString -> Value -> ByteString
-stripImportsAndPragmas bs ast = stripAstNodes bs ast p
+stripImportsAndPragmas :: (ByteString, Int) -> Value -> (ByteString, Int)
+stripImportsAndPragmas bso ast = stripAstNodes bso ast p
   where
     p x = nodeIs "ImportDirective" x || nodeIs "PragmaDirective" x
 
-stripAstNodes :: ByteString -> Value -> (Value -> Bool) -> ByteString
-stripAstNodes bs ast p =
+stripAstNodes :: (ByteString, Int)-> Value -> (Value -> Bool) -> (ByteString, Int)
+stripAstNodes bso ast p =
   cutRanges [sourceRange node | node <- universe ast, p node]
 
   where
-    -- 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"
-
     -- Removes a set of non-overlapping ranges from a bytestring
     -- by commenting them out.
-    cutRanges :: [(Int, Int)] -> ByteString
-    cutRanges (sort -> rs) = fst (foldl' f (bs, 0) rs)
+    cutRanges :: [(Int, Int)] -> (ByteString, Int)
+    cutRanges (sort -> rs) = foldl' f bso rs
       where
         f (bs', n) (i, j) =
           ( cut bs' (i + n) (j + n)
@@ -228,3 +300,134 @@
 
 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 = preview (key "attributes" . key "referencedDeclaration" . _Integer)
+    name = preview (key "attributes" . key "name" . _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)
+        && (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
+        x :: Maybe (Int, Integer)
+        x = case preview (key "name" . _String) v of
+          Just 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"
+          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,15 +6,15 @@
 
 import EVM (VM, cheatCode, traceForest, traceData, Error (..))
 import EVM (Trace, TraceData (..), Log (..), Query (..), FrameContext (..))
-import EVM.Dapp (DappInfo, dappSolcByHash, showTraceLocation, dappEventMap)
+import EVM.Dapp (DappInfo, dappSolcByHash, dappSolcByName, showTraceLocation, dappEventMap)
 import EVM.Concrete (Word (..), wordValue)
-import EVM.Symbolic (maybeLitWord, Buffer(..), len)
-import EVM.Types (W256 (..), num)
+import EVM.Symbolic (maybeLitWord, len)
+import EVM.Types (W256 (..), num, Buffer(..))
 import EVM.ABI (AbiValue (..), Event (..), AbiType (..))
 import EVM.ABI (Indexed (NotIndexed), getAbiSeq, getAbi)
 import EVM.ABI (parseTypeName)
 import EVM.Solidity (SolcContract, contractName, abiMap)
-import EVM.Solidity (methodOutput, methodSignature)
+import EVM.Solidity (methodOutput, methodSignature, methodName)
 
 import Control.Arrow ((>>>))
 import Control.Lens (view, preview, ix, _2, to, _Just)
@@ -58,6 +58,17 @@
 showWordExact :: Word -> Text
 showWordExact (C _ (W256 w)) = humanizeInteger w
 
+showWordExplanation :: W256 -> DappInfo -> Text
+showWordExplanation w _ | w > 0xffffffff = showDec Unsigned w
+showWordExplanation w dapp =
+  let
+    fullAbiMap =
+      mconcat (map (view abiMap) (Map.elems (view dappSolcByName dapp)))
+  in
+    case Map.lookup (fromIntegral w) fullAbiMap of
+      Nothing -> showDec Unsigned w
+      Just x  -> "keccak(\"" <> view methodSignature x <> "\")"
+
 humanizeInteger :: (Num a, Integral a, Show a) => a -> Text
 humanizeInteger =
   Text.intercalate ","
@@ -149,6 +160,8 @@
       case showTraceLocation dapp trace of
         Left x -> " \x1b[90m" <> x <> "\x1b[0m"
         Right x -> " \x1b[90m(" <> x <> ")\x1b[0m"
+    fullAbiMap =
+      mconcat (map (view abiMap) (Map.elems (view dappSolcByName dapp)))
   in case view traceData trace of
     EventTrace (Log _ bytes topics) ->
       case topics of
@@ -198,10 +211,19 @@
         _ ->
           "\x1b[91merror\x1b[0m " <> pack (show e) <> pos
 
-    ReturnTrace out (CallContext _ _ hash (Just abi) _ _ _) ->
+    ReturnTrace out (CallContext _ _ _ _ hash (Just abi) _ _ _) ->
       case getAbiMethodOutput dapp hash abi of
         Nothing ->
-          "← " <> formatSBinary out
+          "← " <>
+            case Map.lookup (fromIntegral abi) fullAbiMap of
+              Just m  ->
+                case (view methodOutput m) of
+                  Just (_, t) ->
+                    pack (show t) <> " " <> showValue t out
+                  Nothing ->
+                    formatSBinary out
+              Nothing ->
+                formatSBinary out
         Just (_, t) ->
           "← " <> pack (show t) <> " " <> showValue t out
     ReturnTrace out (CallContext {}) ->
@@ -213,12 +235,25 @@
       t
     FrameTrace (CreationContext hash _ _ ) ->
       "create " <> maybeContractName (preview (dappSolcByHash . ix hash . _2) dapp) <> pos
-    FrameTrace (CallContext _ _ hash abi calldata _ _) ->
-      case preview (dappSolcByHash . ix hash . _2) dapp of
+    FrameTrace (CallContext target context _ _ hash abi calldata _ _) ->
+      let calltype = if target == context
+                     then "call "
+                     else "delegatecall "
+      in case preview (dappSolcByHash . ix hash . _2) dapp of
         Nothing ->
-          "call [unknown]" <> pos
+          calltype
+            <> pack (show target)
+            <> pack "::"
+            <> case Map.lookup (fromIntegral (fromMaybe 0x00 abi)) fullAbiMap of
+                 Just m  ->
+                   view methodName m
+                   <> showCall (catMaybes (getAbiTypes (view methodSignature m))) calldata
+                 Nothing ->
+                   formatSBinary calldata
+            <> pos
+
         Just solc ->
-          "call "
+          calltype
             <> "\x1b[1m"
             <> view (contractName . to contractNamePart) solc
             <> "::"
@@ -226,7 +261,6 @@
                  (fromMaybe "[unknown method]" . maybeAbiName solc)
                  abi
             <> maybe ("(" <> formatSBinary calldata <> ")")
-                 -- todo: if unknown method, then just show raw calldata
                  (\x -> showCall (catMaybes x) calldata)
                  (abi >>= fmap getAbiTypes . maybeAbiName solc)
             <> "\x1b[0m"
@@ -260,7 +294,7 @@
   _             -> formatBinary bs
 
 showValues :: [AbiType] -> Buffer -> Text
-showValues ts (SymbolicBuffer sbs) = "symbolic: " <> (pack . show $ AbiTupleType (fromList ts))
+showValues ts (SymbolicBuffer  _) = "symbolic: " <> (pack . show $ AbiTupleType (fromList ts))
 showValues ts (ConcreteBuffer bs) =
   case runGetOrFail (getAbiSeq (length ts) ts) (fromStrict bs) of
     Right (_, _, xs) -> showAbiValues xs
diff --git a/src/EVM/Solidity.hs b/src/EVM/Solidity.hs
--- a/src/EVM/Solidity.hs
+++ b/src/EVM/Solidity.hs
@@ -6,6 +6,7 @@
 module EVM.Solidity
   ( solidity
   , solcRuntime
+  , solidity'
   , JumpType (..)
   , SolcContract (..)
   , StorageItem (..)
@@ -49,18 +50,13 @@
 import EVM.Keccak
 import EVM.Types
 
-import Codec.CBOR.Term      (decodeTerm)
-import Codec.CBOR.Read      (deserialiseFromBytes)
 import Control.Applicative
 import Control.Lens         hiding (Indexed)
 import Data.Aeson           (Value (..))
 import Data.Aeson.Lens
 import Data.Scientific
-import Data.Binary.Get      (runGet, getWord16be)
 import Data.ByteString      (ByteString)
-import Data.ByteString.Lazy (fromStrict)
 import Data.Char            (isDigit)
-import Data.Either          (isRight)
 import Data.Foldable
 import Data.Map.Strict      (Map)
 import Data.Maybe
@@ -88,7 +84,7 @@
 import qualified Data.Vector            as Vector
 
 data StorageItem = StorageItem {
-  _type  :: SlotType,
+  _type   :: SlotType,
   _offset :: Int,
   _slot   :: Int
   } deriving (Show, Eq)
@@ -440,14 +436,23 @@
 -- as the codehash matches otherwise, we don't care if there is some
 -- difference there.
 stripBytecodeMetadata :: ByteString -> ByteString
-stripBytecodeMetadata bc | BS.length cl /= 2 = bc
-                         | BS.length h >= cl' && (isRight . deserialiseFromBytes decodeTerm $ fromStrict cbor) = bc'
-                         | otherwise = bc
-  where
-      l = BS.length bc
-      (h, cl) = BS.splitAt (l - 2) bc
-      cl' = fromIntegral . runGet getWord16be $ fromStrict cl
-      (bc', cbor) = BS.splitAt (BS.length h - cl') h
+stripBytecodeMetadata bs =
+  let stripCandidates = flip BS.breakSubstring bs <$> knownBzzrPrefixes in
+    case find ((/= mempty) . snd) stripCandidates of
+      Nothing -> bs
+      Just (b, _) -> b
+
+knownBzzrPrefixes :: [ByteString]
+knownBzzrPrefixes = [
+  -- a1 65 "bzzr0" 0x58 0x20 (solc <= 0.5.8)
+  BS.pack [0xa1, 0x65, 98, 122, 122, 114, 48, 0x58, 0x20],
+  -- a2 65 "bzzr0" 0x58 0x20 (solc >= 0.5.9)
+  BS.pack [0xa2, 0x65, 98, 122, 122, 114, 48, 0x58, 0x20],
+  -- a2 65 "bzzr1" 0x58 0x20 (solc >= 0.5.11)
+  BS.pack [0xa2, 0x65, 98, 122, 122, 114, 49, 0x58, 0x20],
+  -- a2 64 "ipfs" 0x58 0x22 (solc >= 0.6.0)
+  BS.pack [0xa2, 0x64, 0x69, 0x70, 0x66, 0x73, 0x58, 0x22]
+  ]
 
 -- | Every node in the AST has an ID, and other nodes reference those
 -- IDs.  This function recurses through the tree looking for objects
diff --git a/src/EVM/Stepper.hs b/src/EVM/Stepper.hs
--- a/src/EVM/Stepper.hs
+++ b/src/EVM/Stepper.hs
@@ -33,7 +33,7 @@
 import Control.Lens (use)
 import Data.Binary.Get (runGetOrFail)
 import Data.Text (Text)
-import EVM.Symbolic (Buffer)
+import EVM.Types (Buffer)
 
 import EVM (EVM, VM, VMResult (VMFailure, VMSuccess), Error (Query, Choose), Query, Choose)
 import qualified EVM
diff --git a/src/EVM/SymExec.hs b/src/EVM/SymExec.hs
--- a/src/EVM/SymExec.hs
+++ b/src/EVM/SymExec.hs
@@ -16,7 +16,7 @@
 import qualified EVM.Stepper as Stepper
 import qualified Control.Monad.Operational as Operational
 import EVM.Types hiding (Word)
-import EVM.Symbolic (litBytes, SymWord(..), sw256, Buffer(..))
+import EVM.Symbolic (SymWord(..), sw256)
 import EVM.Concrete (createAddress, Word)
 import qualified EVM.FeeSchedule as FeeSchedule
 import Data.SBV.Trans.Control
@@ -133,6 +133,7 @@
     }) & set (env . contracts . at (createAddress ethrunAddress 1))
              (Just (contractWithStore x initStore))
 
+
 -- | Interpreter which explores all paths at
 -- | branching points.
 -- | returns a list of possible final evm states
@@ -140,14 +141,14 @@
   :: Fetch.Fetcher
   -> Maybe Integer --max iterations
   -> Stepper a
-  -> StateT VM IO [a]
+  -> StateT VM Query [a]
 interpret fetcher maxIter =
   eval . Operational.view
 
   where
     eval
       :: Operational.ProgramView Stepper.Action a
-      -> StateT VM IO [a]
+      -> StateT VM Query [a]
 
     eval (Operational.Return x) =
       pure [x]
@@ -161,14 +162,33 @@
         Stepper.Ask (EVM.PleaseChoosePath continue) -> do
           vm <- get
           case maxIterationsReached vm maxIter of
-            Nothing -> do a <- interpret fetcher maxIter (Stepper.evm (continue True) >>= k)
+            Nothing -> do push 1
+                          a <- interpret fetcher maxIter (Stepper.evm (continue True) >>= k)
                           put vm
+                          pop 1
+                          push 1
                           b <- interpret fetcher maxIter (Stepper.evm (continue False) >>= k)
+                          pop 1
                           return $ a <> b
             Just n -> interpret fetcher maxIter (Stepper.evm (continue (not n)) >>= k)
-        Stepper.Wait q ->
-          do m <- liftIO (fetcher q)
-             interpret fetcher maxIter (Stepper.evm m >>= k)
+        Stepper.Wait q -> do
+          let performQuery =
+                do m <- liftIO (fetcher q)
+                   interpret fetcher maxIter (Stepper.evm m >>= k)
+
+          case q of
+            PleaseAskSMT _ _ continue -> do
+              codelocation <- getCodeLocation <$> get
+              iters <- use (iterations . at codelocation)
+              case iters of
+                -- if this is the first time we are branching at this point,
+                -- explore both branches without consulting SMT.
+                -- Exploring too many branches is a lot cheaper than
+                -- consulting our SMT solver.
+                Nothing -> interpret fetcher maxIter (Stepper.evm (continue EVM.Unknown) >>= k)
+                _ -> performQuery
+            _ -> performQuery
+
         Stepper.EVM m ->
           State.state (runState m) >>= interpret fetcher maxIter . k
 
@@ -184,23 +204,20 @@
 type Precondition = VM -> SBool
 type Postcondition = (VM, VM) -> SBool
 
-checkAssert :: ContractCode -> Maybe Integer -> Maybe (Text, [AbiType]) -> [String] -> Query (Either (VM, [VM]) VM)
-checkAssert c maxIter signature' concreteArgs = verifyContract c maxIter signature' concreteArgs SymbolicS (const sTrue) (Just checkAssertions)
+checkAssert :: ByteString -> Maybe (Text, [AbiType]) -> [String] -> Query (Either (VM, [VM]) VM)
+checkAssert c signature' concreteArgs = verifyContract c signature' concreteArgs SymbolicS (const sTrue) (Just checkAssertions)
 
 checkAssertions :: Postcondition
 checkAssertions (_, out) = case view result out of
   Just (EVM.VMFailure (EVM.UnrecognizedOpcode 254)) -> sFalse
   _ -> sTrue
 
-verifyContract :: ContractCode -> Maybe Integer -> Maybe (Text, [AbiType]) -> [String] -> StorageModel -> Precondition -> Maybe Postcondition -> Query (Either (VM, [VM]) VM)
-verifyContract code' maxIter signature' concreteArgs storagemodel pre maybepost = do
+verifyContract :: ByteString -> Maybe (Text, [AbiType]) -> [String] -> StorageModel -> Precondition -> Maybe Postcondition -> Query (Either (VM, [VM]) VM)
+verifyContract theCode signature' concreteArgs storagemodel pre maybepost = do
     preStateRaw <- abstractVM signature' concreteArgs theCode  storagemodel
     -- add the pre condition to the pathconditions to ensure that we are only exploring valid paths
     let preState = over pathConditions ((++) [pre preStateRaw]) preStateRaw
-    verify preState maxIter Nothing maybepost
-  where theCode = case code' of
-          InitCode b    -> b
-          RuntimeCode b -> b
+    verify preState Nothing Nothing maybepost
 
 pruneDeadPaths :: [VM] -> [VM]
 pruneDeadPaths =
@@ -215,10 +232,11 @@
 verify preState maxIter rpcinfo maybepost = do
   let model = view (env . storageModel) preState
   smtState <- queryState
-  results <- io $ fst <$> runStateT (interpret (Fetch.oracle smtState rpcinfo model) maxIter Stepper.runFully) preState
+  results <- fst <$> runStateT (interpret (Fetch.oracle (Just smtState) rpcinfo model False) maxIter Stepper.runFully) preState
   case maybepost of
     (Just post) -> do
       let livePaths = pruneDeadPaths results
+      -- can also do these queries individually (even concurrently!). Could save time and report multiple violations
           postC = sOr $ fmap (\postState -> (sAnd (view pathConditions postState)) .&& sNot (post (preState, postState))) livePaths
       -- is there any path which can possibly violate
       -- the postcondition?
@@ -232,7 +250,7 @@
                     return $ Left (preState, livePaths)
         Sat -> return $ Right preState
 
-    Nothing -> do io $ putStrLn "Q.E.D."
+    Nothing -> do io $ putStrLn "Nothing to check"
                   return $ Left (preState, pruneDeadPaths results)
 
 -- | Compares two contract runtimes for trace equivalence by running two VMs and comparing the end states.
@@ -249,8 +267,12 @@
       preStateB = loadSymVM (RuntimeCode bytecodeB) prestorage SymbolicS precaller callvalue' (calldata', cdlen) & set pathConditions pathconds
 
   smtState <- queryState
-  (aVMs, bVMs) <- both (\x -> io $ fst <$> runStateT (interpret (Fetch.oracle smtState Nothing SymbolicS) maxiter Stepper.runFully) x)
-    (preStateA, preStateB)
+  push 1
+  aVMs <- fst <$> runStateT (interpret (Fetch.oracle (Just smtState) Nothing SymbolicS False) maxiter Stepper.runFully) preStateA
+  pop 1
+  push 1
+  bVMs <- fst <$> runStateT (interpret (Fetch.oracle (Just smtState) Nothing SymbolicS False) maxiter Stepper.runFully) preStateB
+  pop 1
   -- Check each pair of endstates for equality:
   let differingEndStates = uncurry distinct <$> [(a,b) | a <- pruneDeadPaths aVMs, b <- pruneDeadPaths bVMs]
       distinct a b =
@@ -279,7 +301,6 @@
         in sAnd aPath .&& sAnd bPath .&& differingResults
   -- If there exists a pair of endstates where this is not the case,
   -- the following constraint is satisfiable
-  resetAssertions
   constrain $ sOr differingEndStates
 
   checkSat >>= \case
diff --git a/src/EVM/Symbolic.hs b/src/EVM/Symbolic.hs
--- a/src/EVM/Symbolic.hs
+++ b/src/EVM/Symbolic.hs
@@ -34,9 +34,6 @@
 litAddr :: Addr -> SAddr
 litAddr = SAddr . literal . toSizzle
 
-litBytes :: ByteString -> [SWord 8]
-litBytes bs = fmap (toSized . literal) (BS.unpack bs)
-
 maybeLitWord :: SymWord -> Maybe Word
 maybeLitWord (S whiff a) = fmap (C whiff . fromSizzle) (unliteral a)
 
@@ -59,6 +56,9 @@
 forceLitBytes :: [SWord 8] -> ByteString
 forceLitBytes = BS.pack . fmap (fromSized . fromJust . unliteral)
 
+forceBuffer :: Buffer -> ByteString
+forceBuffer (ConcreteBuffer b) = b
+forceBuffer (SymbolicBuffer b) = forceLitBytes b
 
 -- | Arithmetic operations on SymWord
 
@@ -92,6 +92,13 @@
 sgt (S _ x) (S _ y) =
   sw256 $ ite (sFromIntegral x .> (sFromIntegral y :: (SInt 256))) 1 0
 
+shiftRight' :: SymWord -> SymWord -> SymWord
+shiftRight' (S _ a') b@(S _ b') = case (num <$> unliteral a', b) of
+  (Just n, (S (FromBytes (SymbolicBuffer a)) _)) | n `mod` 8 == 0 && n <= 256 ->
+    let bs = replicate (n `div` 8) 0 <> (take ((256 - n) `div` 8) a)
+    in S (FromBytes (SymbolicBuffer bs)) (fromBytes bs)
+  _ -> sw256 $ sShiftRight b' a'
+
 -- | Operations over symbolic memory (list of symbolic bytes)
 swordAt :: Int -> [SWord 8] -> SymWord
 swordAt i bs = sw256 . fromBytes $ truncpad 32 $ drop i bs
@@ -144,9 +151,14 @@
 -- the index is symbolic, but it still seems (kind of) manageable
 -- for the solvers.
 readSWordWithBound :: SWord 32 -> Buffer -> SWord 32 -> SymWord
-readSWordWithBound ind (SymbolicBuffer xs) bound =
-  let boundedList = [ite (i .<= bound) x 0 | (x, i) <- zip xs [1..]]
-  in sw256 . fromBytes $ [select' boundedList 0 (ind + j) | j <- [0..31]]
+readSWordWithBound ind (SymbolicBuffer xs) bound = case (num <$> fromSized <$> unliteral ind, num <$> fromSized <$> unliteral bound) of
+  (Just i, Just b) ->
+    let bs = truncpad 32 $ drop i (take b xs)
+    in S (FromBytes (SymbolicBuffer bs)) (fromBytes bs)
+  _ -> 
+    let boundedList = [ite (i .<= bound) x 0 | (x, i) <- zip xs [1..]]
+    in sw256 . fromBytes $ [select' boundedList 0 (ind + j) | j <- [0..31]]
+
 readSWordWithBound ind (ConcreteBuffer xs) bound =
   case fromSized <$> unliteral ind of
     Nothing -> readSWordWithBound ind (SymbolicBuffer (litBytes xs)) bound
@@ -154,32 +166,6 @@
        -- INVARIANT: bound should always be length xs for concrete bytes
        -- so we should be able to safely ignore it here
          litWord $ Concrete.readMemoryWord (num x') xs
-
-
--- | Operations over buffers (concrete or symbolic)
-
--- | A buffer is a list of bytes. For concrete execution, this is simply `ByteString`.
--- In symbolic settings, it is a list of symbolic bitvectors of size 8.
-data Buffer
-  = ConcreteBuffer ByteString
-  | SymbolicBuffer [SWord 8]
-  deriving (Show)
-
-instance Semigroup Buffer where
-  ConcreteBuffer a <> ConcreteBuffer b = ConcreteBuffer (a <> b)
-  ConcreteBuffer a <> SymbolicBuffer b = SymbolicBuffer (litBytes a <> b)
-  SymbolicBuffer a <> ConcreteBuffer b = SymbolicBuffer (a <> litBytes b)
-  SymbolicBuffer a <> SymbolicBuffer b = SymbolicBuffer (a <> b)
-
-instance Monoid Buffer where
-  mempty = ConcreteBuffer mempty
-
-instance EqSymbolic Buffer where
-  ConcreteBuffer a .== ConcreteBuffer b = literal (a == b)
-  ConcreteBuffer a .== SymbolicBuffer b = litBytes a .== b
-  SymbolicBuffer a .== ConcreteBuffer b = a .== litBytes b
-  SymbolicBuffer a .== SymbolicBuffer b = a .== b
-
 
 -- a whole foldable instance seems overkill, but length is always good to have!
 len :: Buffer -> Int
diff --git a/src/EVM/TTY.hs b/src/EVM/TTY.hs
--- a/src/EVM/TTY.hs
+++ b/src/EVM/TTY.hs
@@ -12,13 +12,13 @@
 
 import EVM
 import EVM.ABI (abiTypeSolidity, decodeAbiValue, AbiType(..), emptyAbi)
-import EVM.Symbolic (SymWord(..), Buffer(..))
+import EVM.Symbolic (SymWord(..))
 import EVM.SymExec (maxIterationsReached)
 import EVM.Dapp (DappInfo, dappInfo)
 import EVM.Dapp (dappUnitTests, unitTestMethods, dappSolcByName, dappSolcByHash, dappSources)
 import EVM.Dapp (dappAstSrcMap)
 import EVM.Debug
-import EVM.Format (Signedness (..), showDec, showWordExact)
+import EVM.Format (showWordExact, showWordExplanation)
 import EVM.Format (contractNamePart, contractPathPart, showTraceTree)
 import EVM.Hexdump (prettyHex)
 import EVM.Op
@@ -40,9 +40,9 @@
 import Data.Aeson.Lens
 import Data.ByteString (ByteString)
 import Data.Maybe (isJust, fromJust, fromMaybe)
-import Data.Map (Map, insert, lookupLT, singleton)
+import Data.Map (Map, insert, lookupLT, singleton, filter)
 import Data.Monoid ((<>))
-import Data.Text (Text, unpack, pack)
+import Data.Text (Text, pack)
 import Data.Text.Encoding (decodeUtf8)
 import Data.List (sort, lookup)
 import Data.Version (showVersion)
@@ -309,6 +309,27 @@
     m = interpret mode (view uiStepper ui)
     nxt = runStateT (m <* modify renderVm) ui
 
+backstep
+  :: (?fetcher :: Fetcher
+     ,?maxIter :: Maybe Integer)
+  => UiVmState -> EventM n UiVmState
+backstep s = case view uiStep s of
+  0 -> return s
+  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"
+
 appEvent
   :: (?fetcher::Fetcher, ?maxIter :: Maybe Integer) =>
   UiState ->
@@ -422,7 +443,7 @@
 
       in takeStep s' (Step 0)
 
--- Vm Overview: p - step
+-- Vm Overview: p - backstep
 appEvent st@(ViewVm s) (VtyEvent (V.EvKey (V.KChar 'p') [])) =
   case view uiStep s of
     0 ->
@@ -445,6 +466,70 @@
 
       takeStep s1 (Step stepsToTake)
 
+-- 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
+      s1 <- backstep s
+      let
+        -- find a vm with a different source location than s1
+        snapshots' = Data.Map.filter (isNextSourcePosition s1 . fst) (view uiSnapshots s1)
+      case lookupLT n snapshots' of
+          -- s2 source position is the first one. 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 we reach the source location of s1
+          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 . isNextSourcePosition s1))
+
+-- Vm Overview: c-p - backstep
+appEvent st@(ViewVm s) (VtyEvent (V.EvKey (V.KChar 'p') [V.MCtrl])) =
+  case view uiStep s of
+    0 ->
+      -- We're already at the first step; ignore command.
+      continue st
+    n -> do
+      s1 <- backstep s
+      let
+        -- find a vm with a different source location than s1
+        snapshots' = Data.Map.filter (isNextSourcePositionWithoutEntering s1 . fst) (view uiSnapshots s1)
+      case lookupLT n snapshots' of
+          -- s2 source position is the first one. 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 we reach the source location of s1
+          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 . isNextSourcePosition s1))
+
 -- Vm Overview: 0 - choose no jump
 appEvent (ViewVm s) (VtyEvent (V.EvKey (V.KChar '0') [])) =
   case view (uiVm . result) s of
@@ -571,6 +656,8 @@
         "N      Step fwds to the next source position\n" <>
         "C-n    Step fwds to the next source position skipping CALL & CREATE\n" <>
         "p      Step back by one instruction\n\n" <>
+        "P      Step back to the previous source position\n\n" <>
+        "C-p    Step back to the previous source position skipping CALL & CREATE\n\n" <>
         "m      Toggle memory pane\n" <>
         "0      Choose the branch which does not jump \n" <>
         "1      Choose the branch which does jump \n" <>
@@ -834,17 +921,6 @@
            ])
       False
       (view uiStackList ui)
-
-showWordExplanation :: W256 -> DappInfo -> Text
-showWordExplanation w _ | w > 0xffffffff = showDec Unsigned w
-showWordExplanation w dapp =
-  let
-    fullAbiMap =
-      mconcat (map (view abiMap) (Map.elems (view dappSolcByName dapp)))
-  in
-    case Map.lookup (fromIntegral w) fullAbiMap of
-      Nothing -> showDec Unsigned w
-      Just x  -> "keccak(\"" <> view methodSignature x <> "\")"
 
 drawBytecodePane :: UiVmState -> UiWidget
 drawBytecodePane ui =
diff --git a/src/EVM/Types.hs b/src/EVM/Types.hs
--- a/src/EVM/Types.hs
+++ b/src/EVM/Types.hs
@@ -84,6 +84,34 @@
 instance (ToSizzleBV Addr)
 instance (FromSizzleBV (WordN 160))
 
+
+litBytes :: ByteString -> [SWord 8]
+litBytes bs = fmap (toSized . literal) (BS.unpack bs)
+
+-- | Operations over buffers (concrete or symbolic)
+
+-- | A buffer is a list of bytes. For concrete execution, this is simply `ByteString`.
+-- In symbolic settings, it is a list of symbolic bitvectors of size 8.
+data Buffer
+  = ConcreteBuffer ByteString
+  | SymbolicBuffer [SWord 8]
+  deriving (Show)
+
+instance Semigroup Buffer where
+  ConcreteBuffer a <> ConcreteBuffer b = ConcreteBuffer (a <> b)
+  ConcreteBuffer a <> SymbolicBuffer b = SymbolicBuffer (litBytes a <> b)
+  SymbolicBuffer a <> ConcreteBuffer b = SymbolicBuffer (a <> litBytes b)
+  SymbolicBuffer a <> SymbolicBuffer b = SymbolicBuffer (a <> b)
+
+instance Monoid Buffer where
+  mempty = ConcreteBuffer mempty
+
+instance EqSymbolic Buffer where
+  ConcreteBuffer a .== ConcreteBuffer b = literal (a == b)
+  ConcreteBuffer a .== SymbolicBuffer b = litBytes a .== b
+  SymbolicBuffer a .== ConcreteBuffer b = a .== litBytes b
+  SymbolicBuffer a .== SymbolicBuffer b = a .== b
+
 newtype Addr = Addr { addressWord160 :: Word160 }
   deriving (Num, Integral, Real, Ord, Enum, Eq, Bits, Generic)
 
diff --git a/src/EVM/UnitTest.hs b/src/EVM/UnitTest.hs
--- a/src/EVM/UnitTest.hs
+++ b/src/EVM/UnitTest.hs
@@ -1,3 +1,5 @@
+{-# Language LambdaCase #-}
+
 module EVM.UnitTest where
 
 import Prelude hiding (Word)
@@ -12,6 +14,8 @@
 import EVM.Format
 import EVM.Solidity
 import EVM.Types
+import EVM.VMTest
+import qualified EVM.Fetch
 
 import qualified EVM.FeeSchedule as FeeSchedule
 
@@ -20,7 +24,6 @@
 import qualified Control.Monad.Operational as Operational
 
 import Control.Lens hiding (Indexed)
-import Control.Monad ((>=>))
 import Control.Monad.State.Strict hiding (state)
 import qualified Control.Monad.State.Strict as State
 
@@ -29,7 +32,8 @@
 
 import qualified Data.ByteString.Lazy as BSLazy
 import Data.ByteString    (ByteString)
-import Data.SBV
+import Data.SBV    hiding (verbose)
+import Data.Either        (isRight)
 import Data.Foldable      (toList)
 import Data.Map           (Map)
 import Data.Maybe         (fromMaybe, catMaybes, fromJust, isJust, fromMaybe, mapMaybe)
@@ -352,7 +356,7 @@
   -> Map Text SolcContract
   -> SourceCache
   -> (Text, [(Text, [AbiType])])
-  -> IO Bool
+  -> IO [(Bool, VM)]
 runUnitTestContract
   opts@(UnitTestOptions {..}) contractMap sources (name, testSigs) = do
 
@@ -381,90 +385,114 @@
           Text.putStrLn "\x1b[31m[FAIL]\x1b[0m setUp()"
           tick "\n"
           tick $ failOutput vm1 opts "setUp()"
-          pure False
+          pure [(False, vm1)]
         Just (VMSuccess _) -> do
-
-          -- Define the thread spawner for normal test cases
           let
-            runOne testName args = do
-              let argInfo = pack (if args == emptyAbi then "" else " with arguments: " <> show args)
-              (bailed, vm2) <-
-                runStateT
-                  (interpret oracle (execTest opts testName args))
-                  vm1
-              (success, vm) <- runStateT (interpret oracle (checkFailures opts testName args bailed)) vm2
-              if success
-              then
-                 let gasSpent = num (testGasCall testParams) - view (state . gas) vm2
-                     gasText = pack . show $ (fromIntegral gasSpent :: Integer)
-                 in
-                    pure
-                      ("\x1b[32m[PASS]\x1b[0m "
-                       <> testName <> argInfo <> " (gas: " <> gasText <> ")"
-                       , Right (passOutput vm opts testName)
-                      )
-              else
-                    pure
-                      ("\x1b[31m[FAIL]\x1b[0m "
-                       <> testName <> argInfo
-                       , Left (failOutput vm opts testName)
-                      )
-
-          -- Define the thread spawner for property based tests
-          let fuzzRun (testName, types) = do
-                let args = Args{ replay          = Nothing
-                               , maxSuccess      = fuzzRuns
-                               , maxDiscardRatio = 10
-                               , maxSize         = 100
-                               , chatty          = isJust verbose
-                               , maxShrinks      = maxBound
-                               }
-                res <- quickCheckWithResult args (fuzzTest opts testName types vm1)
-                case res of
-                  Success numTests _ _ _ _ _ ->
-                    pure ("\x1b[32m[PASS]\x1b[0m "
-                           <> testName <> " (runs: " <> (pack $ show numTests) <> ")",
-                           -- vm1 isn't quite the post vm we want...
-                           -- but the vm we want is not accessible here anyway...
-                           Right (passOutput vm1 opts testName))
-                  Failure _ _ _ _ _ _ _ _ _ _ failCase _ _ ->
-                    let abiValue = decodeAbiValue (AbiTupleType (Vector.fromList types)) $ BSLazy.fromStrict $ hexText (pack $ concat failCase)
-                        ppOutput = pack $ show abiValue
-                    in do
-                    -- Run the failing test again to get a proper trace
-                    vm2 <- execStateT (interpret oracle (runUnitTest opts testName abiValue)) vm1
-                    pure ("\x1b[31m[FAIL]\x1b[0m "
-                             <> testName <> ". Counterexample: " <> ppOutput
-                             <> "\nRun:\n dapp test --replay '(\"" <> testName <> "\",\""
-                             <> (pack (concat failCase)) <> "\")'\nto test this case again, or \n dapp debug --replay '(\""
-                             <> testName <> "\",\"" <> (pack (concat failCase)) <> "\")'\nto debug it.",
-                             Left (failOutput vm2 opts testName))
-                  _ -> pure ("\x1b[31m[OOPS]\x1b[0m "
-                              <> testName, Left (failOutput vm1 opts testName))
-
-          let runTest (testName, []) = runOne testName emptyAbi
-              runTest (testName, types) = case replay of
-                Nothing -> fuzzRun (testName, types)
-                Just (sig, callData) -> if sig == testName
-                                         then runOne testName $
-                                              decodeAbiValue (AbiTupleType (Vector.fromList types)) callData
-                                         else fuzzRun (testName, types)
-
-          let inform (x, y) = Text.putStrLn x >> pure y
+            runCache :: ([(Either Text Text, VM)], VM) -> (Text, [AbiType])
+                        -> IO ([(Either Text Text, VM)], VM)
+            runCache (results, vm) (testName, types) = do
+              (t, r, vm') <- runTest opts vm (testName, types)
+              Text.putStrLn t
+              let vmCached = vm & set (cache . fetched) (view (cache . fetched) vm')
+              pure (((r, vm'): results), vmCached)
 
-          -- Run all the test cases and print their status updates
-          details <-
-            mapM (runTest >=> inform) testSigs
+          -- Run all the test cases and print their status updates,
+          -- accumulating the vm cache throughout
+          (details, _) <- foldM runCache ([], vm1) testSigs
 
-          let running = [x | Right x <- details]
-          let bailing = [x | Left x <- details]
+          let running = [x | (Right x, _) <- details]
+          let bailing = [x | (Left  x, _) <- details]
 
           tick "\n"
           tick (Text.unlines (filter (not . Text.null) running))
           tick (Text.unlines (filter (not . Text.null) bailing))
 
-          pure (null bailing)
+          pure [(isRight r, vm) | (r, vm) <- details]
 
+
+
+runTest :: UnitTestOptions -> VM -> (Text, [AbiType]) -> IO (Text, Either Text Text, VM)
+runTest opts@UnitTestOptions{..} vm (testName, []) = runOne opts vm testName emptyAbi
+runTest opts@UnitTestOptions{..} vm (testName, types) = case replay of
+  Nothing ->
+    fuzzRun opts vm testName types
+  Just (sig, callData) ->
+    if sig == testName
+    then runOne opts vm testName $
+      decodeAbiValue (AbiTupleType (Vector.fromList types)) callData
+    else fuzzRun opts vm testName types
+
+-- | Define the thread spawner for normal test cases 
+runOne :: UnitTestOptions -> VM -> ABIMethod -> AbiValue -> IO (Text, Either Text Text, VM)
+runOne opts@UnitTestOptions{..} vm testName args = do
+  let argInfo = pack (if args == emptyAbi then "" else " with arguments: " <> show args)
+  (bailed, vm') <-
+    runStateT
+      (interpret oracle (execTest opts testName args))
+      vm
+  (success, vm'') <-
+    runStateT
+      (interpret oracle (checkFailures opts testName args bailed)) vm'
+  if success
+  then
+     let gasSpent = num (testGasCall testParams) - view (state . gas) vm'
+         gasText = pack $ show (fromIntegral gasSpent :: Integer)
+     in
+        pure
+          ("\x1b[32m[PASS]\x1b[0m "
+           <> testName <> argInfo <> " (gas: " <> gasText <> ")"
+          , Right (passOutput vm'' opts testName)
+          , vm''
+          )
+  else
+        pure
+          ("\x1b[31m[FAIL]\x1b[0m "
+           <> testName <> argInfo
+          , Left (failOutput vm'' opts testName)
+          , vm''
+          )
+
+-- | Define the thread spawner for property based tests
+fuzzRun :: UnitTestOptions -> VM -> Text -> [AbiType] -> IO (Text, Either Text Text, VM)
+fuzzRun opts@UnitTestOptions{..} vm testName types = do
+  let args = Args{ replay          = Nothing
+                 , maxSuccess      = fuzzRuns
+                 , maxDiscardRatio = 10
+                 , maxSize         = 100
+                 , chatty          = isJust verbose
+                 , maxShrinks      = maxBound
+                 }
+  quickCheckWithResult args (fuzzTest opts testName types vm) >>= \case
+    Success numTests _ _ _ _ _ ->
+      pure ("\x1b[32m[PASS]\x1b[0m "
+             <> testName <> " (runs: " <> (pack $ show numTests) <> ")"
+             -- this isn't the post vm we actually want, as we
+             -- can't retrieve the correct vm from quickcheck
+           , Right (passOutput vm opts testName)
+           , vm
+           )
+    Failure _ _ _ _ _ _ _ _ _ _ failCase _ _ ->
+      let abiValue = decodeAbiValue (AbiTupleType (Vector.fromList types)) $ BSLazy.fromStrict $ hexText (pack $ concat failCase)
+          ppOutput = pack $ show abiValue
+      in do
+        -- Run the failing test again to get a proper trace
+        vm' <- execStateT (interpret oracle (runUnitTest opts testName abiValue)) vm
+        pure ("\x1b[31m[FAIL]\x1b[0m "
+               <> testName <> ". Counterexample: " <> ppOutput
+               <> "\nRun:\n dapp test --replay '(\"" <> testName <> "\",\""
+               <> (pack (concat failCase)) <> "\")'\nto test this case again, or \n dapp debug --replay '(\""
+               <> testName <> "\",\"" <> (pack (concat failCase)) <> "\")'\nto debug it."
+             , Left (failOutput vm' opts testName)
+             , vm'
+             )
+    _ -> pure ("\x1b[31m[OOPS]\x1b[0m "
+               <> testName
+              , Left (failOutput vm opts testName)
+              , vm
+              )
+
+
+
 indentLines :: Int -> Text -> Text
 indentLines n s =
   let p = Text.replicate n " "
@@ -548,14 +576,18 @@
 word32Bytes x = BS.pack [byteAt x (3 - i) | i <- [0..3]]
 
 setupCall :: TestVMParams -> Text -> AbiValue -> EVM ()
-setupCall TestVMParams{..} sig args  = do
+setupCall TestVMParams{..} sig args = do
   resetState
-  use (env . contracts) >>= assign (tx . txReversion)
   assign (tx . isCreate) False
   loadContract testAddress
-  assign (state . calldata) $ (ConcreteBuffer $ abiMethod sig args, literal . num . BS.length $ abiMethod sig args)
+  assign (state . calldata) (ConcreteBuffer $ abiMethod sig args, literal . num . BS.length $ abiMethod sig args)
   assign (state . caller) (litAddr testCaller)
   assign (state . gas) (w256 testGasCall)
+  origin' <- fromMaybe (initialContract (RuntimeCode mempty)) <$> use (env . contracts . at testOrigin)
+  let originBal = view balance origin'
+  when (originBal <= (w256 testGasprice) * (w256 testGasCall)) $ error "insufficient balance for gas cost"
+  vm <- get
+  put $ initTx vm
 
 initialUnitTestVm :: UnitTestOptions -> SolcContract -> VM
 initialUnitTestVm (UnitTestOptions {..}) theContract =
@@ -572,7 +604,7 @@
            , vmoptGaslimit = testGasCreate
            , vmoptCoinbase = testCoinbase
            , vmoptNumber = testNumber
-           , vmoptTimestamp = testTimestamp
+           , vmoptTimestamp = litWord $ w256 $ testTimestamp
            , vmoptBlockGaslimit = testGaslimit
            , vmoptGasprice = testGasprice
            , vmoptMaxCodeSize = testMaxCodeSize
@@ -589,8 +621,26 @@
   in vm
     & set (env . contracts . at ethrunAddress) (Just creator)
 
-getParametersFromEnvironmentVariables :: IO TestVMParams
-getParametersFromEnvironmentVariables = do
+
+maybeM :: (Monad m) => b -> (a -> b) -> m (Maybe a) -> m b
+maybeM def f mayb = do
+  may <- mayb
+  return $ maybe def f may
+
+getParametersFromEnvironmentVariables :: Maybe Text -> IO TestVMParams
+getParametersFromEnvironmentVariables rpc = do
+  block' <- maybeM EVM.Fetch.Latest (EVM.Fetch.BlockNumber . read) (lookupEnv "DAPP_TEST_NUMBER")
+
+  (miner,ts,blockNum,diff) <-
+    case rpc of
+      Nothing  -> return (0,0,0,0)
+      Just url -> EVM.Fetch.fetchBlockFrom block' url >>= \case
+        Nothing -> error $ "Could not fetch block"
+        Just EVM.Block{..} -> return (  _coinbase
+                                      , wordValue $ forceLit $ _timestamp
+                                      , wordValue _number
+                                      , wordValue _difficulty
+                                      )
   let
     getWord s def = maybe def read <$> lookupEnv s
     getAddr s def = maybe def read <$> lookupEnv s
@@ -603,11 +653,11 @@
     <*> getWord "DAPP_TEST_GAS_CALL" defaultGasForInvoking
     <*> getWord "DAPP_TEST_BALANCE_CREATE" defaultBalanceForCreator
     <*> getWord "DAPP_TEST_BALANCE_CALL" defaultBalanceForCreated
-    <*> getAddr "DAPP_TEST_COINBASE" 0
-    <*> getWord "DAPP_TEST_NUMBER" 0
-    <*> getWord "DAPP_TEST_TIMESTAMP" 1
+    <*> getAddr "DAPP_TEST_COINBASE" miner
+    <*> getWord "DAPP_TEST_NUMBER" blockNum
+    <*> getWord "DAPP_TEST_TIMESTAMP" ts
     <*> getWord "DAPP_TEST_GAS_LIMIT" 0
     <*> getWord "DAPP_TEST_GAS_PRICE" 0
     <*> getWord "DAPP_TEST_MAXCODESIZE" defaultMaxCodeSize
-    <*> getWord "DAPP_TEST_DIFFICULTY" 1
+    <*> getWord "DAPP_TEST_DIFFICULTY" diff
     <*> getWord "DAPP_TEST_CHAINID" 99
diff --git a/src/EVM/VMTest.hs b/src/EVM/VMTest.hs
--- a/src/EVM/VMTest.hs
+++ b/src/EVM/VMTest.hs
@@ -4,14 +4,16 @@
 module EVM.VMTest
   ( Case
 #if MIN_VERSION_aeson(1, 0, 0)
-  , parseSuite
   , parseBCSuite
 #endif
+  , initTx
+  , setupTx
   , vmForCase
   , checkExpectation
   ) where
 
 import qualified EVM
+import EVM (contractcode, storage, origStorage, balance, nonce, Storage(..), initialContract)
 import qualified EVM.Concrete as EVM
 import qualified EVM.FeeSchedule
 
@@ -25,12 +27,10 @@
 import Control.Lens
 import Control.Monad
 
-import Data.ByteString (ByteString)
-import Data.Aeson ((.:), (.:?), FromJSON (..))
-import Data.Bifunctor (bimap)
+import Data.Aeson ((.:), FromJSON (..))
 import Data.Foldable (fold)
 import Data.Map (Map)
-import Data.Maybe (fromMaybe)
+import Data.Maybe (fromMaybe, isNothing, isJust)
 import Data.Witherable (Filterable, catMaybes)
 
 import qualified Data.Map          as Map
@@ -52,47 +52,25 @@
 
 data Case = Case
   { testVmOpts      :: EVM.VMOpts
-  , checkContracts  :: Map Addr Contract
-  , testExpectation :: Maybe Expectation
+  , checkContracts  :: Map Addr EVM.Contract
+  , testExpectation :: Map Addr EVM.Contract
   } deriving Show
 
 data BlockchainCase = BlockchainCase
   { blockchainBlocks  :: [Block]
-  , blockchainPre     :: Map Addr Contract
-  , blockchainPost    :: Map Addr Contract
+  , blockchainPre     :: Map Addr EVM.Contract
+  , blockchainPost    :: Map Addr EVM.Contract
   , blockchainNetwork :: String
   } deriving Show
 
-data Contract = Contract
-  { _balance :: W256
-  , _code    :: EVM.ContractCode
-  , _nonce   :: W256
-  , _storage :: Map W256 W256
-  , _create  :: Bool
-  } deriving Show
-
-data Expectation = Expectation
-  { expectedOut       :: Maybe ByteString
-  , expectedContracts :: Map Addr Contract
-  , expectedGas       :: Maybe W256
-  } deriving Show
-
-makeLenses ''Contract
-
-accountAt :: Addr -> Getter (Map Addr Contract) Contract
+accountAt :: Addr -> Getter (Map Addr EVM.Contract) EVM.Contract
 accountAt a = (at a) . (to $ fromMaybe newAccount)
 
-touchAccount :: Addr -> Map Addr Contract -> Map Addr Contract
+touchAccount :: Addr -> Map Addr EVM.Contract -> Map Addr EVM.Contract
 touchAccount a = Map.insertWith (flip const) a newAccount
 
-newAccount :: Contract
-newAccount = Contract
-  { _balance = 0
-  , _code    = EVM.RuntimeCode mempty
-  , _nonce   = 0
-  , _storage = mempty
-  , _create  = False
-  }
+newAccount :: EVM.Contract
+newAccount = initialContract $ EVM.RuntimeCode mempty
 
 splitEithers :: (Filterable f) => f (Either a b) -> (f a, f b)
 splitEithers =
@@ -100,12 +78,16 @@
   . (fmap fst &&& fmap snd)
   . (fmap (preview _Left &&& preview _Right))
 
-checkStateFail :: Bool -> Case -> Expectation -> EVM.VM -> (Bool, Bool, Bool, Bool, Bool) -> IO Bool
-checkStateFail diff x expectation vm (okState, okMoney, okNonce, okData, okCode) = do
+checkStateFail :: Bool -> Case -> EVM.VM -> (Bool, Bool, Bool, Bool, Bool) -> IO Bool
+checkStateFail diff x vm (okState, okMoney, okNonce, okData, okCode) = do
   let
-    printField :: (v -> String) -> Map Addr v -> IO ()
-    printField f d = putStrLn $ Map.foldrWithKey (\k v acc ->
-      acc ++ show k ++ " : " ++ f v ++ "\n") "" d
+    printContracts :: Map Addr EVM.Contract -> IO ()
+    printContracts cs = putStrLn $ Map.foldrWithKey (\k v acc ->
+      acc ++ show k ++ " : "
+                   ++ (show . toInteger  $ (view nonce v)) ++ " "
+                   ++ (show . toInteger  $ (view balance v)) ++ " "
+                   ++ (printStorage $ (view storage v))
+        ++ "\n") "" cs
 
     reason = map fst (filter (not . snd)
         [ ("bad-state",       okMoney || okNonce || okData  || okCode || okState)
@@ -115,54 +97,28 @@
         , ("bad-code",    not okCode  || okMoney || okNonce || okData || okState)
         ])
     check = checkContracts x
-    initial = initTx x
-    expected = expectedContracts expectation
+    expected = testExpectation x
     actual = view (EVM.env . EVM.contracts . to (fmap (clearZeroStorage.clearOrigStorage))) vm
     printStorage (EVM.Symbolic c) = show c
     printStorage (EVM.Concrete c) = show $ Map.toList c
 
   putStr (unwords reason)
   when (diff && (not okState)) $ do
-    putStrLn "\nCheck balance/state: "
-    printField (\v -> (show . toInteger  $ _nonce v) ++ " "
-                   ++ (show . toInteger  $ _balance v) ++ " "
-                   ++ (show . Map.toList $ _storage v)) check
-    putStrLn "\nInitial balance/state: "
-    printField (\v -> (show . toInteger  $ _nonce v) ++ " "
-                   ++ (show . toInteger  $ _balance v) ++ " "
-                   ++ (show . Map.toList $ _storage v)) initial
+    putStrLn "\nPre balance/state: "
+    printContracts check
     putStrLn "\nExpected balance/state: "
-    printField (\v -> (show . toInteger  $ _nonce v) ++ " "
-                   ++ (show . toInteger  $ _balance v) ++ " "
-                   ++ (show . Map.toList $ _storage v)) expected
+    printContracts expected
     putStrLn "\nActual balance/state: "
-    printField (\v -> (show . toInteger  $ EVM._nonce v) ++ " "
-                   ++ (show . toInteger  $ EVM._balance v) ++ " "
-                   ++ (printStorage      $ EVM._storage v)) actual
+    printContracts actual
   return okState
 
 checkExpectation :: Bool -> Case -> EVM.VM -> IO Bool
-checkExpectation diff x vm =
-  case (testExpectation x, view EVM.result vm) of
-    (Just expectation, _) -> do
-      let (okState, b2, b3, b4, b5) =
-            checkExpectedContracts vm (expectedContracts expectation)
-      _ <- if not okState then
-               checkStateFail
-                 diff x expectation vm (okState, b2, b3, b4, b5)
-           else return True
-      return okState
-
-    (Nothing, Just (EVM.VMSuccess _)) -> do
-      putStr "unexpected-success"
-      return False
-
-    (Nothing, Just (EVM.VMFailure _)) ->
-      return True
-
-    (_, Nothing) -> do
-      print (view EVM.result vm)
-      error "internal error"
+checkExpectation diff x vm = do
+  let expectation = testExpectation x
+  let (okState, b2, b3, b4, b5) = checkExpectedContracts vm $ expectation
+  unless okState $ void $ checkStateFail
+    diff x vm (okState, b2, b3, b4, b5)
+  return okState
 
 -- quotient account state by nullness
 (~=) :: Map Addr EVM.Contract -> Map Addr EVM.Contract -> Bool
@@ -173,10 +129,10 @@
         padded_cs  = padNewAccounts cs  (Map.keys cs')
     in padded_cs == padded_cs'
 
-checkExpectedContracts :: EVM.VM -> Map Addr Contract -> (Bool, Bool, Bool, Bool, Bool)
+checkExpectedContracts :: EVM.VM -> Map Addr EVM.Contract -> (Bool, Bool, Bool, Bool, Bool)
 checkExpectedContracts vm expected =
   let cs = vm ^. EVM.env . EVM.contracts . to (fmap (clearZeroStorage.clearOrigStorage))
-      expectedCs = clearOrigStorage <$> realizeContracts expected
+      expectedCs = clearOrigStorage <$> expected
   in ( (expectedCs ~= cs)
      , (clearBalance <$> expectedCs) ~= (clearBalance <$> cs)
      , (clearNonce   <$> expectedCs) ~= (clearNonce   <$> cs)
@@ -185,45 +141,44 @@
      )
 
 clearOrigStorage :: EVM.Contract -> EVM.Contract
-clearOrigStorage = set EVM.origStorage mempty
+clearOrigStorage = set origStorage mempty
 
 clearZeroStorage :: EVM.Contract -> EVM.Contract
-clearZeroStorage c = case EVM._storage c of
+clearZeroStorage c = case view storage c of
   EVM.Symbolic _ -> c
   EVM.Concrete m -> let store = Map.filter (\x -> forceLit x /= 0) m
                     in set EVM.storage (EVM.Concrete store) c
 
 clearStorage :: EVM.Contract -> EVM.Contract
-clearStorage = set EVM.storage (EVM.Concrete mempty)
+clearStorage = set storage (EVM.Concrete mempty)
 
 clearBalance :: EVM.Contract -> EVM.Contract
-clearBalance = set EVM.balance 0
+clearBalance = set balance 0
 
 clearNonce :: EVM.Contract -> EVM.Contract
-clearNonce = set EVM.nonce 0
+clearNonce = set nonce 0
 
 clearCode :: EVM.Contract -> EVM.Contract
-clearCode = set EVM.contractcode (EVM.RuntimeCode mempty)
+clearCode = set contractcode (EVM.RuntimeCode mempty)
 
 #if MIN_VERSION_aeson(1, 0, 0)
 
-instance FromJSON Contract where
-  parseJSON (JSON.Object v) = Contract
-    <$> v .: "balance"
-    <*> (EVM.RuntimeCode <$> (hexText <$> v .: "code"))
-    <*> v .: "nonce"
-    <*> v .: "storage"
-    <*> pure False
-  parseJSON invalid =
-    JSON.typeMismatch "VM test case contract" invalid
+instance FromJSON EVM.Contract where
+  parseJSON (JSON.Object v) = do
+    code <- (EVM.RuntimeCode <$> (hexText <$> v .: "code"))
+    storage' <- Map.mapKeys EVM.w256 <$> v .: "storage"
+    balance' <- v .: "balance"
+    nonce'   <- v .: "nonce"
+    return
+      $
+      EVM.initialContract code
+       & balance .~ EVM.w256 balance'
+       & nonce   .~ EVM.w256 nonce'
+       & storage .~ EVM.Concrete (fmap (litWord . EVM.w256) storage')
+       & origStorage .~ fmap EVM.w256 storage'
 
-instance FromJSON Case where
-  parseJSON (JSON.Object v) = Case
-    <$> parseVmOpts v
-    <*> parseContracts Pre v
-    <*> parseExpectation v
   parseJSON invalid =
-    JSON.typeMismatch "VM test case" invalid
+    JSON.typeMismatch "Contract" invalid
 
 instance FromJSON BlockchainCase where
   parseJSON (JSON.Object v) = BlockchainCase
@@ -247,63 +202,19 @@
   parseJSON invalid =
     JSON.typeMismatch "Block" invalid
 
-parseVmOpts :: JSON.Object -> JSON.Parser EVM.VMOpts
-parseVmOpts v =
-  do envV  <- v .: "env"
-     execV <- v .: "exec"
-     case (envV, execV) of
-       (JSON.Object env, JSON.Object exec) ->
-         EVM.VMOpts
-           <$> (dataField exec "code" >>= pure . EVM.initialContract . EVM.RuntimeCode)
-           <*> (dataField exec "data" >>= \a -> pure ( (ConcreteBuffer a), literal . num $ BS.length a))
-           <*> (w256lit <$> wordField exec "value")
-           <*> addrField exec "address"
-           <*> (litAddr <$> addrField exec "caller")
-           <*> addrField exec "origin"
-           <*> wordField exec "gas" -- XXX: correct?
-           <*> wordField exec "gas" -- XXX: correct?
-           <*> wordField env  "currentNumber"
-           <*> wordField env  "currentTimestamp"
-           <*> addrField env  "currentCoinbase"
-           <*> wordField env  "currentDifficulty"
-           <*> pure 0xffffffff
-           <*> wordField env  "currentGasLimit"
-           <*> wordField exec "gasPrice"
-           <*> pure (EVM.FeeSchedule.istanbul)
-           <*> pure 1
-           <*> pure False
-           <*> pure EVM.ConcreteS
-       _ ->
-         JSON.typeMismatch "VM test case" (JSON.Object v)
-
 parseContracts ::
-  Which -> JSON.Object -> JSON.Parser (Map Addr Contract)
+  Which -> JSON.Object -> JSON.Parser (Map Addr EVM.Contract)
 parseContracts w v =
   v .: which >>= parseJSON
   where which = case w of
           Pre  -> "pre"
           Post -> "postState"
 
-parseExpectation :: JSON.Object -> JSON.Parser (Maybe Expectation)
-parseExpectation v =
-  do out       <- fmap hexText <$> v .:? "out"
-     contracts <- v .:? "post"
-     gas       <- v .:? "gas"
-     case (out, contracts, gas) of
-       (Just x, Just y, Just z) ->
-         return (Just (Expectation (Just x) y (Just z)))
-       _ ->
-         return Nothing
-
-parseSuite ::
-  Lazy.ByteString -> Either String (Map String Case)
-parseSuite = JSON.eitherDecode'
-
 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)
+  Right bcCases -> let allCases = fromBlockchainCase <$> bcCases
                        keepError (Left e) = errorFatal e
                        keepError _        = True
                        filteredCases = Map.filter keepError allCases
@@ -315,32 +226,10 @@
     else Right parsedCases
 #endif
 
-realizeContracts :: Map Addr Contract -> Map Addr EVM.Contract
-realizeContracts = Map.fromList . map f . Map.toList
-  where
-    f (a, x) = (a, realizeContract x)
-
-realizeContract :: Contract -> EVM.Contract
-realizeContract x =
-  EVM.initialContract (x ^. code)
-    & EVM.balance .~ EVM.w256 (x ^. balance)
-    & EVM.nonce   .~ EVM.w256 (x ^. nonce)
-    & EVM.storage .~ EVM.Concrete (
-        Map.fromList .
-        map (bimap EVM.w256 (litWord . EVM.w256)) .
-        Map.toList $ x ^. storage
-        )
-    & EVM.origStorage .~ (
-        Map.fromList .
-        map (bimap EVM.w256 EVM.w256) .
-        Map.toList $ x ^. storage
-        )
-
 data BlockchainError
   = TooManyBlocks
   | TooManyTxs
   | NoTxs
-  | TargetMissing
   | SignatureUnverified
   | InvalidTx
   | OldNetwork
@@ -350,7 +239,6 @@
 errorFatal :: BlockchainError -> Bool
 errorFatal TooManyBlocks = True
 errorFatal TooManyTxs = True
-errorFatal TargetMissing = True
 errorFatal SignatureUnverified = True
 errorFatal InvalidTx = True
 errorFatal _ = False
@@ -359,75 +247,32 @@
 fromBlockchainCase (BlockchainCase blocks preState postState network) =
   case (blocks, network) of
     ([block], "Istanbul") -> case blockTxs block of
-      [tx] -> case txToAddr tx of
-        Nothing -> fromCreateBlockchainCase block tx preState postState
-        Just _  -> fromNormalBlockchainCase block tx preState postState
+      [tx] -> fromBlockchainCase' block tx preState postState
       []        -> Left NoTxs
       _         -> Left TooManyTxs
     ([_], _) -> Left OldNetwork
     (_, _)        -> Left TooManyBlocks
 
-fromCreateBlockchainCase :: Block -> Transaction
-                         -> Map Addr Contract -> Map Addr Contract
-                         -> Either BlockchainError Case
-fromCreateBlockchainCase block tx preState postState =
-  case (sender 1 tx,
-        checkCreateTx tx block preState) of
-    (Nothing, _) -> Left SignatureUnverified
-    (_, Nothing) -> Left FailedCreate
-    (Just origin, Just (checkState, createdAddr)) -> let
-      feeSchedule = EVM.FeeSchedule.istanbul
-      in Right $ Case
-         (EVM.VMOpts
-          { vmoptContract      = EVM.initialContract (EVM.InitCode (txData tx))
-          , vmoptCalldata      = (mempty, 0)
-          , vmoptValue         = w256lit $ txValue tx
-          , vmoptAddress       = createdAddr
-          , vmoptCaller        = (litAddr origin)
-          , vmoptOrigin        = origin
-          , vmoptGas           = txGasLimit tx - fromIntegral (txGasCost feeSchedule tx)
-          , vmoptGaslimit      = txGasLimit tx
-          , vmoptNumber        = blockNumber block
-          , vmoptTimestamp     = blockTimestamp block
-          , vmoptCoinbase      = blockCoinbase block
-          , vmoptDifficulty    = blockDifficulty block
-          , vmoptMaxCodeSize   = 24576
-          , vmoptBlockGaslimit = blockGasLimit block
-          , vmoptGasprice      = txGasPrice tx
-          , vmoptSchedule      = feeSchedule
-          , vmoptChainId       = 1
-          , vmoptCreate        = True
-          , vmoptStorageModel  = EVM.ConcreteS
-          })
-        checkState
-        (Just $ Expectation Nothing postState Nothing)
-
-
-fromNormalBlockchainCase :: Block -> Transaction
-                       -> Map Addr Contract -> Map Addr Contract
+fromBlockchainCase' :: Block -> Transaction
+                       -> Map Addr EVM.Contract -> Map Addr EVM.Contract
                        -> Either BlockchainError Case
-fromNormalBlockchainCase block tx preState postState =
-  let Just toAddr = txToAddr tx
-      feeSchedule = EVM.FeeSchedule.istanbul
-      toCode = Map.lookup toAddr preState
-      theCode = case toCode of
-          Nothing -> EVM.RuntimeCode mempty
-          Just c -> view code c
-  in case (toAddr , toCode , sender 1 tx , checkNormalTx tx block preState) of
-      (_, _, Nothing, _) -> Left SignatureUnverified
-      (_, _, _, Nothing) -> Left InvalidTx
-      (_, _, Just origin, Just checkState) -> Right $ 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      = (ConcreteBuffer $ txData tx, literal . num . BS.length $ txData tx)
+         , vmoptCalldata      = cd
          , vmoptValue         = litWord (EVM.w256 $ txValue tx)
          , vmoptAddress       = toAddr
-         , vmoptCaller        = (litAddr origin)
+         , vmoptCaller        = litAddr origin
          , vmoptOrigin        = origin
          , vmoptGas           = txGasLimit tx - fromIntegral (txGasCost feeSchedule tx)
          , vmoptGaslimit      = txGasLimit tx
          , vmoptNumber        = blockNumber block
-         , vmoptTimestamp     = blockTimestamp block
+         , vmoptTimestamp     = litWord $ EVM.w256 $ blockTimestamp block
          , vmoptCoinbase      = blockCoinbase block
          , vmoptDifficulty    = blockDifficulty block
          , vmoptMaxCodeSize   = 24576
@@ -435,92 +280,96 @@
          , vmoptGasprice      = txGasPrice tx
          , vmoptSchedule      = feeSchedule
          , vmoptChainId       = 1
-         , vmoptCreate        = False
+         , vmoptCreate        = isCreate
          , vmoptStorageModel  = EVM.ConcreteS
          })
         checkState
-        (Just $ Expectation Nothing postState Nothing)
+        postState
+          where
+            toAddr = fromMaybe (EVM.createAddress origin senderNonce) (txToAddr tx)
+            senderNonce = EVM.wordValue $ view (accountAt origin . nonce) preState
+            feeSchedule = EVM.FeeSchedule.istanbul
+            toCode = Map.lookup toAddr preState
+            theCode = if isCreate
+                      then EVM.InitCode (txData tx)
+                      else maybe (EVM.RuntimeCode mempty) (view contractcode) toCode
+            cd = if isCreate
+                 then (mempty, 0)
+                 else (ConcreteBuffer $ txData tx, literal . num . BS.length $ txData tx)
 
 
-validateTx :: Transaction -> Map Addr Contract -> Maybe Bool
+validateTx :: Transaction -> Map Addr EVM.Contract -> Maybe ()
 validateTx tx cs = do
   origin        <- sender 1 tx
   originBalance <- (view balance) <$> view (at origin) cs
   originNonce   <- (view nonce)   <$> view (at origin) cs
-  let gasDeposit = fromIntegral (txGasPrice tx) * (txGasLimit tx)
-  return $ gasDeposit + (txValue tx) <= originBalance
-    && (txNonce tx) == originNonce
-
-checkNormalTx :: Transaction -> Block -> Map Addr Contract -> Maybe (Map Addr Contract)
-checkNormalTx tx block prestate = do
-  toAddr <- txToAddr tx
-  origin <- sender 1 tx
-  valid  <- validateTx tx prestate
-  let gasDeposit = fromIntegral (txGasPrice tx) * (txGasLimit tx)
-      coinbase   = blockCoinbase block
-  if not valid then mzero else
-    return $
-    (Map.adjust ((over nonce   (+ 1))
-               . (over balance (subtract gasDeposit))) origin)
-    . touchAccount origin
-    . touchAccount toAddr
-    . touchAccount coinbase $ prestate
+  let gasDeposit = EVM.w256 $ (txGasPrice tx) * (txGasLimit tx)
+  if gasDeposit + (EVM.w256 $ txValue tx) <= originBalance
+    && (EVM.w256 $ txNonce tx) == originNonce
+  then Just ()
+  else Nothing
 
-checkCreateTx :: Transaction -> Block -> Map Addr Contract -> Maybe ((Map Addr Contract), Addr)
-checkCreateTx tx block prestate = do
+checkTx :: Transaction -> Block -> Map Addr EVM.Contract -> Maybe (Map Addr EVM.Contract)
+checkTx tx block prestate = do
   origin <- sender 1 tx
-  valid  <- validateTx tx prestate
-  let gasDeposit  = fromIntegral (txGasPrice tx) * (txGasLimit tx)
-      coinbase    = blockCoinbase block
-      senderNonce = view (accountAt origin . nonce) prestate
-      createdAddr = EVM.createAddress origin senderNonce
-      prevCode    = view (accountAt createdAddr .  code) prestate
-      prevNonce   = view (accountAt createdAddr . nonce) prestate
-  if (prevCode /= EVM.RuntimeCode mempty) || (prevNonce /= 0) || (not valid)
+  validateTx tx prestate
+  let isCreate   = isNothing (txToAddr tx)
+      senderNonce = EVM.wordValue $ view (accountAt origin . nonce) prestate
+      toAddr      = fromMaybe (EVM.createAddress origin senderNonce) (txToAddr tx)
+      prevCode    = view (accountAt toAddr . contractcode) prestate
+      prevNonce   = view (accountAt toAddr . nonce) prestate
+  if isCreate && ((prevCode /= EVM.RuntimeCode mempty) || (prevNonce /= 0))
   then mzero
   else
-    return
-    ((Map.adjust ((over nonce   (+ 1))
-                 . (over balance (subtract gasDeposit))) origin)
-    . touchAccount origin
-    . touchAccount createdAddr
-    . touchAccount coinbase $ prestate, createdAddr)
-
-initTx :: Case -> Map Addr Contract
-initTx x =
-  let
-    checkState = checkContracts x
-    opts     = testVmOpts x
-    toAddr   = EVM.vmoptAddress  opts
-    origin   = EVM.vmoptOrigin   opts
-    value    = EVM.vmoptValue    opts
-    initcode = EVM._contractcode (EVM.vmoptContract opts)
-    creation = EVM.vmoptCreate   opts
-  in
-    (Map.adjust (over balance (subtract (EVM.wordValue $ forceLit value))) origin)
-    . (Map.adjust (over balance (+ (EVM.wordValue $ forceLit value))) toAddr)
-    . (if creation
-       then (Map.adjust (set code initcode) toAddr)
-          . (Map.adjust (set nonce 1) toAddr)
-          . (Map.adjust (set storage mempty) toAddr)
-          . (Map.adjust (set create True) toAddr)
-       else id)
-    $ checkState
+    return $ prestate
 
 vmForCase :: Case -> EVM.VM
 vmForCase x =
   let
-    checkState = checkContracts x
-    initState = initTx x
-    opts = testVmOpts x
-    creation = EVM.vmoptCreate opts
-    touchedAccounts =
-      if creation then
-        [EVM.vmoptOrigin opts]
-      else
-        [EVM.vmoptOrigin opts, EVM.vmoptAddress opts]
+    vm = EVM.makeVm (testVmOpts x)
+      & set (EVM.env . EVM.contracts) (checkContracts x)
   in
-    EVM.makeVm (testVmOpts x)
-    & EVM.env . EVM.contracts .~ realizeContracts initState
-    & EVM.tx . EVM.txReversion .~ realizeContracts checkState
-    & EVM.tx . EVM.substate . EVM.touchedAccounts .~ touchedAccounts
+    initTx vm
+
+-- | Increments origin nonce and pays gas deposit
+setupTx :: Addr -> Addr -> EVM.Word -> EVM.Word -> Map Addr EVM.Contract -> Map Addr EVM.Contract
+setupTx origin coinbase gasPrice gasLimit prestate =
+  let gasCost = gasPrice * gasLimit
+  in (Map.adjust ((over nonce   (+ 1))
+               . (over balance (subtract gasCost))) origin)
+    . touchAccount origin
+    . touchAccount coinbase $ prestate
+
+-- | Given a valid tx loaded into the vm state,
+-- subtract gas payment from the origin, increment the nonce
+-- and pay receiving address
+initTx :: EVM.VM -> EVM.VM
+initTx vm = let
+    toAddr   = view (EVM.state . EVM.contract) vm
+    origin   = view (EVM.tx . EVM.origin) vm
+    gasPrice = view (EVM.tx . EVM.gasprice) vm
+    gasLimit = view (EVM.tx . EVM.txgaslimit) vm
+    coinbase = view (EVM.block . EVM.coinbase) vm
+    value    = view (EVM.state . EVM.callvalue) vm
+    toContract = initialContract (EVM.InitCode (view (EVM.state . EVM.code) vm))
+    preState = setupTx origin coinbase gasPrice gasLimit $ view (EVM.env . EVM.contracts) vm
+    oldBalance = view (accountAt toAddr . balance) preState
+    creation = view (EVM.tx . EVM.isCreate) vm
+    initState =
+      (if isJust (maybeLitWord value)
+       then (Map.adjust (over balance (subtract (forceLit value))) origin)
+        . (Map.adjust (over balance (+ (forceLit value))) toAddr)
+       else id)
+      . (if creation
+         then Map.insert toAddr (toContract & balance .~ oldBalance)
+         else touchAccount toAddr)
+      $ preState
+
+    touched = if creation
+              then [origin]
+              else [origin, toAddr]
+
+    in
+      vm & EVM.env . EVM.contracts .~ initState
+         & EVM.tx . EVM.txReversion .~ preState
+         & EVM.tx . EVM.substate . EVM.touchedAccounts .~ touched
diff --git a/test/test.hs b/test/test.hs
--- a/test/test.hs
+++ b/test/test.hs
@@ -1,4 +1,5 @@
 {-# Language OverloadedStrings #-}
+{-# Language LambdaCase #-}
 {-# Language QuasiQuotes #-}
 {-# Language TypeSynonymInstances #-}
 {-# Language FlexibleInstances #-}
@@ -18,23 +19,28 @@
 import Test.Tasty.QuickCheck-- hiding (forAll)
 import Test.Tasty.HUnit
 
-import Control.Monad.State.Strict (execState, runState)
+import Control.Monad.State.Strict (execState, runState, when)
 import Control.Lens hiding (List, pre)
 
 import qualified Data.Vector as Vector
 import Data.String.Here
 
 import Control.Monad.Fail
+import Debug.Trace
 
 import Data.Binary.Put (runPut)
-import Data.SBV hiding ((===), forAll)
+import Data.SBV hiding ((===), forAll, sList)
 import Data.SBV.Control
+import Data.SBV.Trans (sList)
+import Data.SBV.List (implode)
+import qualified Data.SBV.List as SL
 import qualified Data.Map as Map
 import Data.Binary.Get (runGetOrFail)
 
 import EVM hiding (Query)
 import EVM.SymExec
 import EVM.Symbolic
+import EVM.Concrete (w256)
 import EVM.ABI
 import EVM.Exec
 import EVM.Patricia as Patricia
@@ -117,6 +123,31 @@
         in x == y
     ]
 
+  , testGroup "metadata stripper"
+    [ testCase "it strips the metadata for solc => 0.6" $ do
+        let code = hexText "0x608060405234801561001057600080fd5b50600436106100365760003560e01c806317bf8bac1461003b578063acffee6b1461005d575b600080fd5b610043610067565b604051808215151515815260200191505060405180910390f35b610065610073565b005b60008060015414905090565b6000809054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1663f8a8fd6d6040518163ffffffff1660e01b815260040160206040518083038186803b1580156100da57600080fd5b505afa1580156100ee573d6000803e3d6000fd5b505050506040513d602081101561010457600080fd5b810190808051906020019092919050505060018190555056fea265627a7a723158205d775f914dcb471365a430b5f5b2cfe819e615cbbb5b2f1ccc7da1fd802e43c364736f6c634300050b0032"
+            stripped = stripBytecodeMetadata code
+        assertEqual "failed to strip metadata" (show (ByteStringS stripped)) "0x608060405234801561001057600080fd5b50600436106100365760003560e01c806317bf8bac1461003b578063acffee6b1461005d575b600080fd5b610043610067565b604051808215151515815260200191505060405180910390f35b610065610073565b005b60008060015414905090565b6000809054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1663f8a8fd6d6040518163ffffffff1660e01b815260040160206040518083038186803b1580156100da57600080fd5b505afa1580156100ee573d6000803e3d6000fd5b505050506040513d602081101561010457600080fd5b810190808051906020019092919050505060018190555056fe"
+    ,
+      testCase "it strips the metadata and constructor args" $ do
+        let srccode =
+              [i|
+                contract A {
+                  uint y;
+                  constructor(uint x) public {
+                    y = x;
+                  }
+                }
+                |]
+
+        (json, path) <- solidity' srccode
+        let Just (solc, _, _) = readJSON json
+            initCode :: ByteString
+            Just initCode = solc ^? ix (path <> ":A") . creationCode
+        -- add constructor arguments
+        assertEqual "constructor args screwed up metadata stripping" (stripBytecodeMetadata (initCode <> encodeAbiValue (AbiUInt 256 1))) (stripBytecodeMetadata initCode)
+    ]
+
   , testGroup "RLP encodings"
     [ testProperty "rlp decode is a retraction (bytes)" $ \(Bytes bs) ->
 --      withMaxSuccess 100000 $
@@ -155,19 +186,15 @@
             }
           }
           |]
-        let asWord :: [SWord 8] -> SWord 256
-            asWord = fromBytes
-            pre preVM = let SymbolicBuffer bs = ditch 4 (fst $ view (state . calldata) preVM)
-                            (x, y) = splitAt 32 bs
-                        in asWord x .<= asWord x + asWord y
+        let pre preVM = let [x, y] = getStaticAbiArgs preVM
+                        in x .<= x + y
                            .&& view (state . callvalue) preVM .== 0
             post = Just $ \(prestate, poststate) ->
-              let SymbolicBuffer input = fst $ view (state.calldata) prestate
-                  (x, y) = splitAt 32 (drop 4 input)
+              let [x, y] = getStaticAbiArgs prestate
               in case view result poststate of
-                Just (VMSuccess (SymbolicBuffer out)) -> (asWord out) .== (asWord x) + (asWord y)
+                Just (VMSuccess (SymbolicBuffer out)) -> (fromBytes out) .== x + y
                 _ -> sFalse
-        Left (_, res) <- runSMT $ query $ verifyContract (RuntimeCode safeAdd) Nothing (Just ("add(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] SymbolicS pre post
+        Left (_, res) <- runSMT $ query $ verifyContract safeAdd (Just ("add(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] SymbolicS pre post
         putStrLn $ "successfully explored: " <> show (length res) <> " paths"
      ,
 
@@ -180,21 +207,17 @@
             }
           }
           |]
-        let asWord :: [SWord 8] -> SWord 256
-            asWord = fromBytes
-            pre preVM = let SymbolicBuffer bs = ditch 4 (fst $ view (state . calldata) preVM)
-                            (x, y) = splitAt 32 bs
-                           in (asWord x .<= asWord x + asWord y)
-                              .&& (x .== y)
-                              .&& view (state . callvalue) preVM .== 0
-            post = Just $ \(prestate, poststate)
-              -> let SymbolicBuffer input = fst $ view (state.calldata) prestate
-                     (_, y) = splitAt 32 (drop 4 input)
-                 in case view result poststate of
-                      Just (VMSuccess (SymbolicBuffer out)) -> asWord out .== 2 * asWord y
+        let pre preVM = let [x, y] = getStaticAbiArgs preVM
+                        in (x .<= x + y)
+                           .&& (x .== y)
+                           .&& view (state . callvalue) preVM .== 0
+            post (prestate, poststate) =
+              let [_, y] = getStaticAbiArgs prestate
+              in case view result poststate of
+                      Just (VMSuccess (SymbolicBuffer out)) -> fromBytes out .== 2 * y
                       _ -> sFalse
         Left (_, res) <- runSMTWith z3 $ query $
-          verifyContract (RuntimeCode safeAdd) Nothing (Just ("add(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] SymbolicS pre post
+          verifyContract safeAdd (Just ("add(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] SymbolicS pre (Just post)
         putStrLn $ "successfully explored: " <> show (length res) <> " paths"
       ,
         testCase "factorize 973013" $ do
@@ -208,15 +231,15 @@
           }
           |]
         bs <- runSMTWith cvc4 $ query $ do
-          Right vm <- checkAssert (RuntimeCode factor) Nothing (Just ("factor(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) []
+          Right vm <- checkAssert factor (Just ("factor(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) []
           case view (state . calldata . _1) vm of
             SymbolicBuffer bs -> BS.pack <$> mapM (getValue.fromSized) bs
             ConcreteBuffer _ -> error "unexpected"
 
-        let AbiTuple xy = decodeAbiValue (AbiTupleType $ Vector.fromList [AbiUIntType 256, AbiUIntType 256]) (BS.fromStrict (BS.drop 4 bs))
-            [AbiUInt 256 x, AbiUInt 256 y] = Vector.toList xy
+        let [AbiUInt 256 x, AbiUInt 256 y] = decodeAbiValues [AbiUIntType 256, AbiUIntType 256] bs
         assertEqual "" True (x == 953 && y == 1021 || x == 1021 && y == 953)
         ,
+
         testCase "summary storage writes" $ do
         Just c <- solcRuntime "A"
           [i|
@@ -230,7 +253,7 @@
           |]
         let pre vm = 0 .== view (state . callvalue) vm
             post = Just $ \(prestate, poststate) ->
-              let SymbolicBuffer y = ditch 4 $ fst (view (state.calldata) prestate)
+              let [y] = getStaticAbiArgs prestate
                   this = view (state . codeContract) prestate
                   Just preC = view (env.contracts . at this) prestate
                   Just postC = view (env.contracts . at this) poststate
@@ -239,9 +262,9 @@
                   prex = readArray prestore 0
                   postx = readArray poststore 0
               in case view result poststate of
-                Just (VMSuccess _) -> prex + 2 * (fromBytes y) .== postx
+                Just (VMSuccess _) -> prex + 2 * y .== postx
                 _ -> sFalse
-        Left (_, res) <- runSMT $ query $ verifyContract (RuntimeCode c) Nothing (Just ("f(uint256)", [AbiUIntType 256])) [] SymbolicS pre post
+        Left (_, res) <- runSMT $ query $ verifyContract c (Just ("f(uint256)", [AbiUIntType 256])) [] SymbolicS pre post
         putStrLn $ "successfully explored: " <> show (length res) <> " paths"
         ,
         -- Inspired by these `msg.sender == to` token bugs
@@ -261,9 +284,8 @@
           }
           |]
         let pre vm = 0 .== view (state . callvalue) vm
-            post = Just $ \(prestate, poststate) ->
-              let SymbolicBuffer bs = fst (view (state.calldata) prestate)
-                  (x,y) = over both (fromBytes) (splitAt 32 $ drop 4 bs)
+            post (prestate, poststate) =
+              let [x,y] = getStaticAbiArgs prestate
                   this = view (state . codeContract) prestate
                   (Just preC, Just postC) = both' (view (env.contracts . at this)) (prestate, poststate)
                   --Just postC = view (env.contracts . at this) poststate
@@ -274,13 +296,12 @@
                 Just (VMSuccess _) -> prex + prey .== postx + (posty :: SWord 256)
                 _ -> sFalse
         bs <- runSMT $ query $ do
-          Right vm <- verifyContract (RuntimeCode c) Nothing (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] SymbolicS pre post
+          Right vm <- verifyContract c (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] SymbolicS pre (Just post)
           case view (state . calldata . _1) vm of
             SymbolicBuffer bs -> BS.pack <$> mapM (getValue.fromSized) bs
             ConcreteBuffer bs -> error "unexpected"
 
-        let AbiTuple xyz = decodeAbiValue (AbiTupleType $ Vector.fromList [AbiUIntType 256, AbiUIntType 256]) (BS.fromStrict (BS.drop 4 bs))
-            [AbiUInt 256 x, AbiUInt 256 y] = Vector.toList xyz
+        let [AbiUInt 256 x, AbiUInt 256 y] = decodeAbiValues [AbiUIntType 256, AbiUIntType 256] bs
         assertEqual "Catch storage collisions" x y
         ,
         testCase "Deposit contract loop (z3)" $ do
@@ -302,7 +323,7 @@
               }
              }
             |]
-          Left (_, res) <- runSMTWith z3 $ query $ checkAssert (RuntimeCode c) Nothing (Just ("deposit(uint256)", [AbiUIntType 256])) []
+          Left (_, res) <- runSMTWith z3 $ query $ checkAssert c (Just ("deposit(uint256)", [AbiUIntType 256])) []
           putStrLn $ "successfully explored: " <> show (length res) <> " paths"
         ,
                 testCase "Deposit contract loop (cvc4)" $ do
@@ -324,7 +345,7 @@
               }
              }
             |]
-          Left (_, res) <- runSMTWith cvc4 $ query $ checkAssert (RuntimeCode c) Nothing (Just ("deposit(uint256)", [AbiUIntType 256])) []
+          Left (_, res) <- runSMTWith cvc4 $ query $ checkAssert c (Just ("deposit(uint256)", [AbiUIntType 256])) []
           putStrLn $ "successfully explored: " <> show (length res) <> " paths"
         ,
         testCase "Deposit contract loop (error version)" $ do
@@ -347,15 +368,14 @@
              }
             |]
           bs <- runSMT $ query $ do
-            Right vm <- checkAssert (RuntimeCode c) Nothing (Just ("deposit(uint8)", [AbiUIntType 8])) []
+            Right vm <- checkAssert c (Just ("deposit(uint8)", [AbiUIntType 8])) []
             case view (state . calldata . _1) vm of
               SymbolicBuffer bs -> BS.pack <$> mapM (getValue.fromSized) bs
               ConcreteBuffer _ -> error "unexpected"
 
-          let deposit = decodeAbiValue (AbiUIntType 8) (BS.fromStrict (BS.drop 4 bs))
+          let [deposit] = decodeAbiValues [AbiUIntType 8] bs
           assertEqual "overflowing uint8" deposit (AbiUInt 8 255)
      ,
-        -- This test uses cvc4 instead of z3
         testCase "explore function dispatch" $ do
         Just c <- solcRuntime "A"
           [i|
@@ -365,7 +385,9 @@
             }
           }
           |]
-        Left (_, res) <- runSMTWith cvc4 $ query $ checkAssert (RuntimeCode c) Nothing Nothing []
+        Left (_, res) <- runSMTWith z3 $ do
+          setTimeOut 5000
+          query $ checkAssert c Nothing []
         putStrLn $ "successfully explored: " <> show (length res) <> " paths"
         ,
 
@@ -378,7 +400,7 @@
               }
             }
             |]
-          Left (_, res) <- runSMTWith cvc4 $ query $ checkAssert (RuntimeCode c) Nothing Nothing []
+          Left (_, res) <- runSMTWith cvc4 $ query $ checkAssert c (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) []
           putStrLn $ "successfully explored: " <> show (length res) <> " paths"
         ,
         testCase "injectivity of keccak (32 bytes)" $ do
@@ -390,7 +412,7 @@
               }
             }
             |]
-          Left (_, res) <- runSMTWith cvc4 $ query $ checkAssert (RuntimeCode c) Nothing Nothing []
+          Left (_, res) <- runSMTWith z3 $ query $ checkAssert c (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) []
           putStrLn $ "successfully explored: " <> show (length res) <> " paths"
        ,
 
@@ -404,15 +426,18 @@
             }
             |]
           bs <- runSMTWith z3 $ query $ do
-            Right vm <- checkAssert (RuntimeCode c) Nothing (Just ("f(uint256,uint256,uint256,uint256)", replicate 4 (AbiUIntType 256))) []
+            Right vm <- checkAssert c (Just ("f(uint256,uint256,uint256,uint256)", replicate 4 (AbiUIntType 256))) []
             case view (state . calldata . _1) vm of
               SymbolicBuffer bs -> BS.pack <$> mapM (getValue.fromSized) bs
               ConcreteBuffer _ -> error "unexpected"
               
-          let AbiTuple xywz = decodeAbiValue (AbiTupleType $ Vector.fromList
-                                              [AbiUIntType 256, AbiUIntType 256,
-                                               AbiUIntType 256, AbiUIntType 256]) (BS.fromStrict (BS.drop 4 bs))
-              [AbiUInt 256 x, AbiUInt 256 y, AbiUInt 256 w, AbiUInt 256 z] = Vector.toList xywz
+          let [AbiUInt 256 x,
+               AbiUInt 256 y,
+               AbiUInt 256 w,
+               AbiUInt 256 z] = decodeAbiValues [AbiUIntType 256,
+                                                 AbiUIntType 256,
+                                                 AbiUIntType 256,
+                                                 AbiUIntType 256] bs
           assertEqual "x == w" x w
           assertEqual "y == z" y z
        ,
@@ -431,7 +456,9 @@
               }
             }
             |]
-          Left (_, res) <- runSMTWith z3 $ query $ checkAssert (RuntimeCode c) Nothing Nothing []
+          Left (_, res) <- runSMTWith z3 $ do
+            setTimeOut 5000
+            query $ checkAssert c Nothing []
           putStrLn $ "successfully explored: " <> show (length res) <> " paths"
 
        ,
@@ -448,7 +475,7 @@
               }
             |]
           -- should find a counterexample
-          Right counterexample <- runSMTWith cvc4 $ query $ checkAssert (RuntimeCode c) Nothing Nothing []
+          Right counterexample <- runSMTWith cvc4 $ query $ checkAssert c (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) []
           putStrLn $ "found counterexample:"
 
 
@@ -507,6 +534,7 @@
   where
     (===>) = assertSolidityComputation
 
+
 runSimpleVM :: ByteString -> ByteString -> Maybe ByteString
 runSimpleVM x ins = case loadVM x of
                       Nothing -> Nothing
@@ -574,6 +602,17 @@
       ${stmts}
     }
   |] (abiCalldata s (Vector.fromList args))
+
+getStaticAbiArgs :: VM -> [SWord 256]
+getStaticAbiArgs vm =
+  let SymbolicBuffer bs = ditch 4 $ view (state . calldata . _1) vm
+  in fmap (\i -> fromBytes $ take 32 (drop (i*32) bs)) [0..((length bs) `div` 32 - 1)]
+
+-- 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))
+  in Vector.toList xy
 
 newtype Bytes = Bytes ByteString
   deriving Eq