diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,10 +1,26 @@
 # hevm changelog
 
+## Unreleased
+
+## 0.48.0 - 2021-08-03
+
+### Changed
+
+- Updated to London hard fork!
+- The configuration variable `DAPP_TEST_BALANCE_CREATE` has been renamed to `DAPP_TEST_BALANCE`
+- Default `smttimeout` has been increased to 1 minute.
+- A new flag has been added to hevm (`--ask-smt-iterations`) that controls the number of iterations
+  at which the symbolic execution engine will stop eager evaluation and begin to query the smt
+  solver whether a given branch is reachable or not.
+- Contract fetching now happens asynchronously.
+- Fixed no contract definition crashes
+- Removed NoSuchContract failures
+
 ## 0.47.0 - 2021-07-01
 
 - A new test runner for checking invariants against random reachable contract states.
 - `hevm symbolic` can search for solc 0.8 style assertion violations, and a new `--assertions` flag
-    has been added allowing users to customize which assertions should be reported
+  has been added allowing users to customize which assertions should be reported
 - A new cheatcode `ffi(string[])` that executes an arbitrary command in the system shell
 
 ### Changed
@@ -67,7 +83,7 @@
 ### Fixed
 
 - Symbolic execution now generates calldata arguments restricted to the proper ranges,
-following the semantics of fuzzing.
+  following the semantics of fuzzing.
 - If the `--address` flag is present in `hevm exec` or `hevm symbolic`,
   it overrides the contract address at which a contract will be created.
 - Address pretty printing
@@ -138,11 +154,11 @@
 - 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,
- and implement proper shrinking for all abi values.
+  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
 - Ensure that pathconditions are consistent when branching, and end the execution with VMFailure: DeadPath if this is not the case
-- Fixed a soundness bug where nonzero jumpconditions  were assumed to equal one.
+- Fixed a soundness bug where nonzero jumpconditions were assumed to equal one.
 - default `--smttimeout` changed from unlimited to 20 seconds
 - `hevm symbolic --debug` now respects `--max-iterations`
 
@@ -157,18 +173,20 @@
 - hevm is now capable of symbolic execution!
 
 ### Changed
+
 As a result, the types of several registers of the EVM have changed to admit symbolic values as well as concrete ones.
 
-  - state.stack: `Word` -> `SymWord`.
-  - state.memory: `ByteString` -> `[SWord 8]`.
-  - state.callvalue: `W256` -> `SymWord`.
-  - 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`.
+- state.stack: `Word` -> `SymWord`.
+- state.memory: `ByteString` -> `[SWord 8]`.
+- state.callvalue: `W256` -> `SymWord`.
+- 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`.
+- tx.value: `W256` -> `SymWord`.
 
-  - contract.storage: `Map Word Word` -> `Storage`, defined as:
+- contract.storage: `Map Word Word` -> `Storage`, defined as:
+
 ```hs
 data Storage
   = Concrete (Map Word SymWord)
@@ -177,305 +195,364 @@
 ```
 
 ### Added
+
 New cli commands:
- - `hevm symbolic`: search for assertion violations, or step through a symbolic execution in debug mode.
- - `hevm equivalence`: compare two programs for equivalence.
 
+- `hevm symbolic`: search for assertion violations, or step through a symbolic execution in debug mode.
+- `hevm equivalence`: compare two programs for equivalence.
+
 See the README for details on usage.
 
 The new module `EVM.SymExec` exposes several library functions dealing with symbolic execution.
 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.
 
+- `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.
+
 ### Removed
 
 The concrete versions of a lot of arithmetic operations, replaced with their more general symbolic counterpart.
 
-
 ## 0.39 - 2020-07-13
- - Exposes abi encoding to cli
- - Added cheat code `hevm.store(address a, bytes32 location, bytes32 value)`
- - Removes `ExecMode`, always running as `ExecuteAsBlockchainTest`. This means that `hevm exec` now finalizes transactions as well.
- - `--code` is now entirely optional. Not supplying it returns an empty contract, or whatever is stored in `--state`.
 
+- Exposes abi encoding to cli
+- Added cheat code `hevm.store(address a, bytes32 location, bytes32 value)`
+- Removes `ExecMode`, always running as `ExecuteAsBlockchainTest`. This means that `hevm exec` now finalizes transactions as well.
+- `--code` is now entirely optional. Not supplying it returns an empty contract, or whatever is stored in `--state`.
+
 ## 0.38 - 2020-04-23
- - Exposes metadata stripping of bytecode to the cli: `hevm strip-metadata --code X`. [357](https://github.com/dapphub/dapptools/pull/357).
- - Fixes a bug in the srcmap parsing introduced in 0.37 [356](https://github.com/dapphub/dapptools/pull/356).
- - Fixes a bug in the abi-encoding of `bytes` with size > 32[358](https://github.com/dapphub/dapptools/pull/358).
 
+- Exposes metadata stripping of bytecode to the cli: `hevm strip-metadata --code X`. [357](https://github.com/dapphub/dapptools/pull/357).
+- Fixes a bug in the srcmap parsing introduced in 0.37 [356](https://github.com/dapphub/dapptools/pull/356).
+- Fixes a bug in the abi-encoding of `bytes` with size > 32[358](https://github.com/dapphub/dapptools/pull/358).
+
 ## 0.37 - 2020-03-24
- - Sourcemap parser now admits `solc-0.6.0` compiled `.sol.json` files.
 
+- Sourcemap parser now admits `solc-0.6.0` compiled `.sol.json` files.
+
 ## 0.36 - 2020-01-07
- - Implement Istanbul support [318](https://github.com/dapphub/dapptools/pull/318)
- - Fix a bug introduced in [280](https://github.com/dapphub/dapptools/pull/280) of rlp encoding of transactions and sender address [320](https://github.com/dapphub/dapptools/pull/320/).
- - Make InvalidTx a fatal error for vm tests and ci.
- - Suport property based testing in unit tests. [313](https://github.com/dapphub/dapptools/pull/313) Arguments to test functions are randomly generated based on the function abi. Fuzz tests are not present in the graphical debugger.
- - Added flags `--replay` and `--fuzz-run` to `hevm dapp-test`, allowing for particular fuzz run cases to be rerun, or for configuration of how many fuzz tests are run.
- - Correct gas readouts for unit tests
- - Prevent crash when trying to jump to next source code point if source code is missing
 
+- Implement Istanbul support [318](https://github.com/dapphub/dapptools/pull/318)
+- Fix a bug introduced in [280](https://github.com/dapphub/dapptools/pull/280) of rlp encoding of transactions and sender address [320](https://github.com/dapphub/dapptools/pull/320/).
+- Make InvalidTx a fatal error for vm tests and ci.
+- Suport property based testing in unit tests. [313](https://github.com/dapphub/dapptools/pull/313) Arguments to test functions are randomly generated based on the function abi. Fuzz tests are not present in the graphical debugger.
+- Added flags `--replay` and `--fuzz-run` to `hevm dapp-test`, allowing for particular fuzz run cases to be rerun, or for configuration of how many fuzz tests are run.
+- Correct gas readouts for unit tests
+- Prevent crash when trying to jump to next source code point if source code is missing
+
 ## 0.35 - 2019-11-02
- - Merkle Patricia trie support [280](https://github.com/dapphub/dapptools/pull/280)
- - RLP encoding and decoding functions [280](https://github.com/dapphub/dapptools/pull/280)
- - Extended support for Solidity ABI encoding [259](https://github.com/dapphub/dapptools/pull/259)
- - Bug fixes surrounding unit tests and gas accounting (https://github.com/dapphub/dapptools/commit/574ef401d3e744f2dcf994da056810cf69ef84fe, https://github.com/dapphub/dapptools/commit/5257574dd9df14edc29410786b75e9fb9c59069f)
 
+- Merkle Patricia trie support [280](https://github.com/dapphub/dapptools/pull/280)
+- RLP encoding and decoding functions [280](https://github.com/dapphub/dapptools/pull/280)
+- Extended support for Solidity ABI encoding [259](https://github.com/dapphub/dapptools/pull/259)
+- Bug fixes surrounding unit tests and gas accounting (https://github.com/dapphub/dapptools/commit/574ef401d3e744f2dcf994da056810cf69ef84fe, https://github.com/dapphub/dapptools/commit/5257574dd9df14edc29410786b75e9fb9c59069f)
+
 ## 0.34 - 2019-08-28
- - handle new solc bzzr metadata in codehash for source map
- - show VM hex outputs as hexadecimal
- - rpc defaults to latest block
- - `hevm interactive`:
-  - fix rpc fetch
-  - scrollable memory pane
- - Fix regression in VMTest compliance.
- - `hevm exec` ergonomics:
-  - Allow code/calldata prefixed with 0x
-  - create transactions with specific caller nonce
-  - interactive help pane
-  - memory pane scrolling
 
+- handle new solc bzzr metadata in codehash for source map
+- show VM hex outputs as hexadecimal
+- rpc defaults to latest block
+- `hevm interactive`:
+- fix rpc fetch
+- scrollable memory pane
+- Fix regression in VMTest compliance.
+- `hevm exec` ergonomics:
+- Allow code/calldata prefixed with 0x
+- create transactions with specific caller nonce
+- interactive help pane
+- memory pane scrolling
+
 ## 0.33 - 2019-08-06
- - Full compliance with the [General State Tests][245] (with the
-   BlockchainTest format), using the Yellow and Jello papers as
-   reference, for Constantinople Fix (aka Petersburg). Including:
-  - full precompile support
-  - correct substate accounting, including touched accounts,
-    selfdestructs and refunds
-  - memory read/write semantics
-  - many gas cost corrections
- - Show more information for non solc bytecode in interactive view
-   (trace and storage)
- - Help text for all cli options
- - Enable `--debug` flag in `hevm dapp-test`
 
+- Full compliance with the [General State Tests][245] (with the
+  BlockchainTest format), using the Yellow and Jello papers as
+  reference, for Constantinople Fix (aka Petersburg). Including:
+- full precompile support
+- correct substate accounting, including touched accounts,
+  selfdestructs and refunds
+- memory read/write semantics
+- many gas cost corrections
+- Show more information for non solc bytecode in interactive view
+  (trace and storage)
+- Help text for all cli options
+- Enable `--debug` flag in `hevm dapp-test`
+
 [245]: https://github.com/dapphub/dapptools/pull/245
 
 ## 0.32 - 2019-06-14
- - Fix dapp-test [nonce initialisation bug][224]
 
+- Fix dapp-test [nonce initialisation bug][224]
+
 [224]: https://github.com/dapphub/dapptools/pull/224
 
 ## 0.31 - 2019-05-29
- - Precompiles: SHA256, RIPEMD, IDENTITY, MODEXP, ECADD, ECMUL,
-   ECPAIRING, MODEXP
- - Show the hevm version with `hevm version`
- - Interactive mode:
-  - no longer exits on reaching halt
-  - new shortcuts: 'a' / 'e' for start / end
-  - allow returning to test picker screen
- - Exact integer formatting in dapp-test and tty
 
+- Precompiles: SHA256, RIPEMD, IDENTITY, MODEXP, ECADD, ECMUL,
+  ECPAIRING, MODEXP
+- Show the hevm version with `hevm version`
+- Interactive mode:
+- no longer exits on reaching halt
+- new shortcuts: 'a' / 'e' for start / end
+- allow returning to test picker screen
+- Exact integer formatting in dapp-test and tty
+
 ## 0.30 - 2019-05-09
- - Adjustable verbosity level for `dapp-test` with `--verbose={0,1,2}`
- - Working stack build
 
+- Adjustable verbosity level for `dapp-test` with `--verbose={0,1,2}`
+- Working stack build
+
 ## 0.29 - 2019-04-03
- - Significant jump in compliance with client tests
- - Add support for running GeneralStateTests
 
+- Significant jump in compliance with client tests
+- Add support for running GeneralStateTests
+
 ## 0.28 - 2019-03-22
- - Fix delegatecall gas metering, as reported in
-   https://github.com/dapphub/dapptools/issues/34
 
+- Fix delegatecall gas metering, as reported in
+  https://github.com/dapphub/dapptools/issues/34
+
 ## 0.27 - 2019-02-06
- - Fix [hevm flatten issue](https://github.com/dapphub/dapptools/issues/127)
-   related to SemVer ranges in Solidity version pragmas
 
+- Fix [hevm flatten issue](https://github.com/dapphub/dapptools/issues/127)
+  related to SemVer ranges in Solidity version pragmas
+
 ## 0.26 - 2019-02-05
- - Format Solidity Error(string) messages in trace
 
+- Format Solidity Error(string) messages in trace
+
 ## 0.25 - 2019-02-04
- - Add SHL, SHR and SAR opcodes
 
+- Add SHL, SHR and SAR opcodes
+
 ## 0.24 - 2019-01-23
- - Fix STATICCALL for precompiled contracts
- - Assume Solidity 0.5.2 in tests
 
+- Fix STATICCALL for precompiled contracts
+- Assume Solidity 0.5.2 in tests
+
 ## 0.23 - 2018-12-12
- - Show passing test traces with --verbose flag
 
+- Show passing test traces with --verbose flag
+
 ## 0.22 - 2018-11-13
- - Simple memory view in TTY
 
+- Simple memory view in TTY
+
 ## 0.21 - 2018-10-29
- - Fix Hackage package by including C header files for ethjet
 
+- Fix Hackage package by including C header files for ethjet
+
 ## 0.20 - 2018-10-27
- - Parse constructor inputs from Solidity AST
 
+- Parse constructor inputs from Solidity AST
+
 ## 0.19 - 2018-10-09
- - Enable experimental 'cheat' address, allowing for modification of the
-   EVM environment from within the tests. Currently just the block
-   timestamp can be adjusted.
 
+- Enable experimental 'cheat' address, allowing for modification of the
+  EVM environment from within the tests. Currently just the block
+  timestamp can be adjusted.
+
 ## 0.18 - 2018-10-09
- - Fix [duplicate address bug](https://github.com/dapphub/dapptools/issues/70)
 
+- Fix [duplicate address bug](https://github.com/dapphub/dapptools/issues/70)
+
 ## 0.17 - 2018-10-05
- - Semigroup/Monoid fix
 
+- Semigroup/Monoid fix
+
 ## 0.16 - 2018-09-19
- - Move ethjet into hevm
 
+- Move ethjet into hevm
+
 ## [0.15] - 2018-05-09
- - Fix SDIV/SMOD definitions for extreme case
 
+- Fix SDIV/SMOD definitions for extreme case
+
 ## [0.14.1] - 2018-04-17
- - Improve PC display in TTY
 
+- Improve PC display in TTY
+
 ## [0.14] - 2018-03-08
- - Implement STATICCALL
 
+- Implement STATICCALL
+
 ## [0.13] - 2018-02-28
- - Require specific block number for RPC debugging
- - Implement RETURNDATACOPY and RETURNDATASIZE
- - Fix bug where created contracts didn't get their balance
 
+- Require specific block number for RPC debugging
+- Implement RETURNDATACOPY and RETURNDATASIZE
+- Fix bug where created contracts didn't get their balance
+
 ## [0.12.3] - 2017-12-19
- - More useful RPC debugging because we strip the entire BZZR metadata
 
+- More useful RPC debugging because we strip the entire BZZR metadata
+
 ## [0.12.2] - 2017-12-17
- - Experimental new ecrecover implementation via libethjet
- - Correct error checking for setUp() invocations
 
+- Experimental new ecrecover implementation via libethjet
+- Correct error checking for setUp() invocations
+
 ## [0.12.1] - 2017-11-28
- - Test name regex matching via --match
- - Fixed source map parsing bug when used with solc --optimize
- - TTY: fix a padding-related display glitch
 
+- Test name regex matching via --match
+- Fixed source map parsing bug when used with solc --optimize
+- TTY: fix a padding-related display glitch
+
 ## [0.12] - 2017-11-14
- - Use 13 different environment variables to control block parameters
-   for unit testing, e.g. block number, timestamp, initial balance, etc.
 
-   Full list:
+- Use 13 different environment variables to control block parameters
+  for unit testing, e.g. block number, timestamp, initial balance, etc.
 
-     - `DAPP_TEST_ADDRESS`
-     - `DAPP_TEST_CALLER`
-     - `DAPP_TEST_ORIGIN`
-     - `DAPP_TEST_GAS_CREATE`
-     - `DAPP_TEST_GAS_CALL`
-     - `DAPP_TEST_BALANCE_CREATE`
-     - `DAPP_TEST_BALANCE_CALL`
-     - `DAPP_TEST_COINBASE`
-     - `DAPP_TEST_NUMBER`
-     - `DAPP_TEST_TIMESTAMP`
-     - `DAPP_TEST_GAS_LIMIT`
-     - `DAPP_TEST_GAS_PRICE`
-     - `DAPP_TEST_DIFFICULTY`
+  Full list:
 
+  - `DAPP_TEST_ADDRESS`
+  - `DAPP_TEST_CALLER`
+  - `DAPP_TEST_ORIGIN`
+  - `DAPP_TEST_GAS_CREATE`
+  - `DAPP_TEST_GAS_CALL`
+  - `DAPP_TEST_BALANCE_CREATE`
+  - `DAPP_TEST_BALANCE_CALL`
+  - `DAPP_TEST_COINBASE`
+  - `DAPP_TEST_NUMBER`
+  - `DAPP_TEST_TIMESTAMP`
+  - `DAPP_TEST_GAS_LIMIT`
+  - `DAPP_TEST_GAS_PRICE`
+  - `DAPP_TEST_DIFFICULTY`
+
 ## [0.11.5] - 2017-11-14
- - Use --state with --exec --debug
 
+- Use --state with --exec --debug
+
 ## [0.11.4] - 2017-11-12
- - Fix bug when unit test contract has creations in constructor
 
+- Fix bug when unit test contract has creations in constructor
+
 ## [0.11.3] - 2017-11-08
- - Fix array support in ABI module
 
+- Fix array support in ABI module
+
 ## [0.11.2] - 2017-11-04
- - TTY: show a help bar with key bindings at the bottom
 
+- TTY: show a help bar with key bindings at the bottom
+
 ## [0.11.1] - 2017-11-02
- - TTY: fix a display glitch
- - TTY: improve display of ABI hashes on the stack
 
+- TTY: fix a display glitch
+- TTY: improve display of ABI hashes on the stack
+
 ## [0.11] - 2017-10-31
- - Add "hevm flatten" for Etherscan-ish source code concatenation
- - Simplify code by removing concrete/symbolic machine abstraction
 
+- Add "hevm flatten" for Etherscan-ish source code concatenation
+- Simplify code by removing concrete/symbolic machine abstraction
+
 ## [0.10.9] - 2017-10-23
- - Fix bugs in ABI formatting
 
+- Fix bugs in ABI formatting
+
 ## [0.10.7] - 2017-10-19
- - Fix library linking bug
- - Fix gas consumption of DELEGATECALL
- - Better error tracing
- - Experimental "contract browser" (stupid list of addresses)
 
+- Fix library linking bug
+- Fix gas consumption of DELEGATECALL
+- Better error tracing
+- Experimental "contract browser" (stupid list of addresses)
+
 ## [0.10.6] - 2017-10-19
- - Enable library linking for unit tests and debugger
- - Use the same default gas/balance values as `ethrun`
 
+- Enable library linking for unit tests and debugger
+- Use the same default gas/balance values as `ethrun`
+
 ## [0.10.5] - 2017-10-17
- - Better trace output including arguments and return values
- - Proof of concept coverage analysis via `dapp-test --coverage`
 
+- Better trace output including arguments and return values
+- Proof of concept coverage analysis via `dapp-test --coverage`
+
 ## [0.10] - 2017-10-10
- - Enable new trace output by default for failing tests
- - Exit with failure code from test runner when tests fail
- - More fixes to improve Ethereum test suite compliance
 
+- Enable new trace output by default for failing tests
+- Exit with failure code from test runner when tests fail
+- More fixes to improve Ethereum test suite compliance
+
 ## [0.9.5] - 2017-10-06
- - Prototype of new trace output with `hevm dapp-test --verbose`
- - Nicer trace tree in the TTY debugger
- - Many fixes to improve Ethereum test suite compliance
 
+- Prototype of new trace output with `hevm dapp-test --verbose`
+- Nicer trace tree in the TTY debugger
+- Many fixes to improve Ethereum test suite compliance
+
 ## [0.9] - 2017-09-29
- - Integrates with live chains via RPC (read-only)
- - Exposes a special contract address with test-related functionality (time warp)
 
+- Integrates with live chains via RPC (read-only)
+- Exposes a special contract address with test-related functionality (time warp)
+
 ## [0.8.5] - 2017-09-22
- - Renames `hevm` from its maiden name `hsevm` :sparkles:
 
+- Renames `hevm` from its maiden name `hsevm` :sparkles:
+
 ## [0.8] - 2017-09-21
- - Implements gas metering (Metropolis rules by default)
- - Shows gas counter in the terminal interface
- - Enables debugger for consensus test executions
- - Consensus test runner script with HTML reporting
- - Passes 564 of the `VMTests`; fails 115 (see [0.8 test report])
- - Command line options for specifying initial gas amounts and balances
- - Improved TTY UI layout
 
+- Implements gas metering (Metropolis rules by default)
+- Shows gas counter in the terminal interface
+- Enables debugger for consensus test executions
+- Consensus test runner script with HTML reporting
+- Passes 564 of the `VMTests`; fails 115 (see [0.8 test report])
+- Command line options for specifying initial gas amounts and balances
+- Improved TTY UI layout
+
 ## [0.7] - 2017-09-07
- - Can save and load contract states to disk using a Git-backed store (only `--exec`)
- - Can debug raw EVM bytecode using `exec --debug`
- - Fixes `exec --value`
- - Has smarter defaults for command line when running tests or debugging
- - Fixes bug with `MSIZE` in `CALL` context
 
+- Can save and load contract states to disk using a Git-backed store (only `--exec`)
+- Can debug raw EVM bytecode using `exec --debug`
+- Fixes `exec --value`
+- Has smarter defaults for command line when running tests or debugging
+- Fixes bug with `MSIZE` in `CALL` context
+
 ## [0.6.5] - 2017-09-01
- - Fixes `exec` with regards to exit codes and error messages
 
+- Fixes `exec` with regards to exit codes and error messages
+
 ## [0.6.1] - 2017-08-03
- - TTY: Adds command `C-n` in TTY for "stepping over"
 
+- TTY: Adds command `C-n` in TTY for "stepping over"
+
 ## [0.6] - 2017-08-03
- - TTY: Adds second line to stack entries with humanized formatting
- - TTY: Gets rid of the separate log pane in favor of a unified trace pane
 
+- TTY: Adds second line to stack entries with humanized formatting
+- TTY: Gets rid of the separate log pane in favor of a unified trace pane
+
 ## [0.5] - 2017-08-02
- - TTY: Adds `p` command for stepping backwards
- - Adds ability to track origins of stack and heap words
- - Tracks Keccak preimage for words that come from the `SHA3` instruction
 
+- TTY: Adds `p` command for stepping backwards
+- Adds ability to track origins of stack and heap words
+- Tracks Keccak preimage for words that come from the `SHA3` instruction
+
 ## [0.4] - 2017-07-31
- - Parallelizes unit test runner
- - Improves speed by changing representation of memory
- - Internal refactoring for future support of symbolic execution
- - Adds logs to the trace pane
 
+- Parallelizes unit test runner
+- Improves speed by changing representation of memory
+- Internal refactoring for future support of symbolic execution
+- Adds logs to the trace pane
+
 ## [0.3.2] - 2017-06-17
- - Adds `REVERT` opcode
- - Sets `TIMESTAMP` value to `1` in unit tests
 
+- Adds `REVERT` opcode
+- Sets `TIMESTAMP` value to `1` in unit tests
+
 ## [0.3.0] - 2017-06-14
- - Reverts contract state after `CALL` fails
- - Improves test runner console output
 
+- Reverts contract state after `CALL` fails
+- Improves test runner console output
+
 ## [0.2.0] - 2017-06-13
- - Fixes bug in `CALL`
 
+- Fixes bug in `CALL`
+
 ## [0.1.0.1] - 2017-03-31
- - Highlights Solidity exactly on character level
- - Adds `N` command for stepping by Solidity source position instead of by opcode
 
+- Highlights Solidity exactly on character level
+- Adds `N` command for stepping by Solidity source position instead of by opcode
+
 ## 0.1.0.0 - 2017-03-29
- - First release
 
-[0.8 test report]: https://hydra.dapp.tools/build/135/download/1/index.html
+- First release
 
+[0.8 test report]: https://hydra.dapp.tools/build/135/download/1/index.html
 [0.12]: https://github.com/dapphub/hevm/compare/0.11.5...0.12
 [0.11.5]: https://github.com/dapphub/hevm/compare/0.11.4...0.11.5
 [0.11.4]: https://github.com/dapphub/hevm/compare/0.11.3...0.11.4
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
@@ -104,6 +104,8 @@
       , gas           :: w ::: Maybe W256       <?> "Tx: gas amount"
       , number        :: w ::: Maybe W256       <?> "Block: number"
       , timestamp     :: w ::: Maybe W256       <?> "Block: timestamp"
+      , basefee       :: w ::: Maybe W256       <?> "Block: base fee"
+      , priorityFee   :: w ::: Maybe W256       <?> "Tx: priority fee"
       , gaslimit      :: w ::: Maybe W256       <?> "Tx: gas limit"
       , gasprice      :: w ::: Maybe W256       <?> "Tx: gas price"
       , create        :: w ::: Bool             <?> "Tx: creation"
@@ -125,21 +127,23 @@
       , debug         :: w ::: Bool               <?> "Run interactively"
       , getModels     :: w ::: Bool               <?> "Print example testcase for each execution path"
       , showTree      :: w ::: Bool               <?> "Print branches explored in tree view"
-      , smttimeout    :: w ::: Maybe Integer      <?> "Timeout given to SMT solver in milliseconds (default: 30000)"
+      , smttimeout    :: w ::: Maybe Integer      <?> "Timeout given to SMT solver in milliseconds (default: 60000)"
       , 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"
       , smtdebug      :: w ::: Bool               <?> "Print smt queries sent to the solver"
       , assertions    :: w ::: Maybe [Word256]    <?> "Comma seperated list of solc panic codes to check for (default: everything except arithmetic overflow)"
+      , askSmtIterations :: w ::: Maybe Integer   <?> "Number of times we may revisit a particular branching point before we consult the smt solver to check reachability (default: 5)"
       }
   | Equivalence -- prove equivalence between two programs
-      { codeA         :: w ::: ByteString    <?> "Bytecode of the first program"
-      , codeB         :: w ::: ByteString    <?> "Bytecode of the second program"
-      , sig           :: w ::: Maybe Text    <?> "Signature of types to decode / encode"
-      , smttimeout    :: w ::: Maybe Integer <?> "Timeout given to SMT solver in milliseconds (default: 30000)"
-      , 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"
-      , smtdebug      :: w ::: Bool               <?> "Print smt queries sent to the solver"
+      { codeA         :: w ::: ByteString       <?> "Bytecode of the first program"
+      , codeB         :: w ::: ByteString       <?> "Bytecode of the second program"
+      , sig           :: w ::: Maybe Text       <?> "Signature of types to decode / encode"
+      , smttimeout    :: w ::: Maybe Integer    <?> "Timeout given to SMT solver in milliseconds (default: 60000)"
+      , 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"
+      , smtdebug      :: w ::: Bool             <?> "Print smt queries sent to the solver"
+      , askSmtIterations :: w ::: Maybe Integer <?> "Number of times we may revisit a particular branching point before we consult the smt solver to check reachability (default: 5)"
       }
   | Exec -- Execute a given program with specified env & calldata
       { code        :: w ::: Maybe ByteString <?> "Program bytecode"
@@ -153,6 +157,8 @@
       , gas         :: w ::: Maybe W256       <?> "Tx: gas amount"
       , number      :: w ::: Maybe W256       <?> "Block: number"
       , timestamp   :: w ::: Maybe W256       <?> "Block: timestamp"
+      , basefee     :: w ::: Maybe W256       <?> "Block: base fee"
+      , priorityFee :: w ::: Maybe W256       <?> "Tx: priority fee"
       , gaslimit    :: w ::: Maybe W256       <?> "Tx: gas limit"
       , gasprice    :: w ::: Maybe W256       <?> "Tx: gas price"
       , create      :: w ::: Bool             <?> "Tx: creation"
@@ -183,11 +189,12 @@
       , 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"
-      , smttimeout    :: w ::: Maybe Integer            <?> "Timeout given to SMT solver in milliseconds (default: 30000)"
-      , 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"
       , smtdebug      :: w ::: Bool                     <?> "Print smt queries sent to the solver"
       , ffi           :: w ::: Bool                     <?> "Allow the usage of the hevm.ffi() cheatcode (WARNING: this allows test authors to execute arbitrary code on your machine)"
+      , smttimeout    :: w ::: Maybe Integer            <?> "Timeout given to SMT solver in milliseconds (default: 60000)"
+      , maxIterations :: w ::: Maybe Integer            <?> "Number of times we may revisit a particular branching point"
+      , askSmtIterations :: w ::: Maybe Integer         <?> "Number of times we may revisit a particular branching point before we consult the smt solver to check reachability (default: 5)"
       }
   | BcTest -- Run an Ethereum Blockhain/GeneralState test
       { file      :: w ::: String    <?> "Path to .json test file"
@@ -288,6 +295,7 @@
          Just url -> EVM.Fetch.oracle (Just state) (Just (block', url)) True
          Nothing  -> EVM.Fetch.oracle (Just state) Nothing True
     , EVM.UnitTest.maxIter = maxIterations cmd
+    , EVM.UnitTest.askSmtIters = askSmtIterations cmd
     , EVM.UnitTest.smtTimeout = smttimeout cmd
     , EVM.UnitTest.solver = solver cmd
     , EVM.UnitTest.smtState = Just state
@@ -301,7 +309,7 @@
     , EVM.UnitTest.vmModifier = vmModifier
     , EVM.UnitTest.testParams = params
     , EVM.UnitTest.dapp = srcInfo
-    , EVM.UnitTest.allowFFI = ffi cmd
+    , EVM.UnitTest.ffiAllowed = ffi cmd
     }
 
 main :: IO ()
@@ -311,7 +319,7 @@
     root = fromMaybe "." (dappRoot cmd)
   case cmd of
     Version {} -> putStrLn (showVersion Paths.version)
-    Symbolic {} -> assert cmd
+    Symbolic {} -> withCurrentDirectory root $ assert cmd
     Equivalence {} -> equivalence cmd
     Exec {} ->
       launchExec cmd
@@ -419,17 +427,20 @@
                        return $ Just (view methodSignature method', snd <$> view methodInputs method')
 
      void . runSMTWithTimeOut (solver cmd) (smttimeout cmd) (smtdebug cmd) . query $
-       equivalenceCheck bytecodeA bytecodeB (maxIterations cmd) maybeSignature >>= \case
-         Right vm -> do io $ putStrLn "Not equal!"
-                        io $ putStrLn "Counterexample:"
-                        showCounterexample vm maybeSignature
-                        io exitFailure
-         Left (postAs, postBs) -> io $ do
+       equivalenceCheck bytecodeA bytecodeB (maxIterations cmd) (askSmtIterations cmd) maybeSignature >>= \case
+         Cex vm -> do
+           io $ putStrLn "Not equal!"
+           io $ putStrLn "Counterexample:"
+           showCounterexample vm maybeSignature
+           io exitFailure
+         Qed (postAs, postBs) -> io $ do
            putStrLn $ "Explored: " <> show (length postAs)
                        <> " execution paths of A and: "
                        <> show (length postBs) <> " paths of B."
            putStrLn "No discrepancies found."
-
+         Timeout () -> io $ do
+           hPutStr stderr "Solver timeout!"
+           exitFailure
 
 -- cvc4 sets timeout via a commandline option instead of smtlib `(set-option)`
 runSMTWithTimeOut :: Maybe Text -> Maybe Integer -> Bool -> Symbolic a -> IO a
@@ -438,7 +449,7 @@
   | solver == Just "z3" = runwithz3
   | solver == Nothing = runwithz3
   | otherwise = error "Unknown solver. Currently supported solvers; z3, cvc4"
- where timeout = fromMaybe 30000 maybeTimeout
+ where timeout = fromMaybe 60000 maybeTimeout
        runwithz3 = runSMTWith z3{SBV.verbose=smtdebug} $ (setTimeOut timeout) >> symb
        runwithcvc4 = do
          setEnv "SBV_CVC4_OPTIONS" ("--lang=smt --incremental --interactive --no-interactive-prompt --model-witness-value --tlimit-per=" <> show timeout)
@@ -515,13 +526,15 @@
     runSMTWithTimeOut (solver cmd) (smttimeout cmd) (smtdebug cmd) $ query $ do
       preState <- symvmFromCommand cmd
       let errCodes = fromMaybe defaultPanicCodes (assertions cmd)
-      verify preState (maxIterations cmd) rpcinfo (Just $ checkAssertions errCodes) >>= \case
-        Right tree -> do
+      verify preState (maxIterations cmd) (askSmtIterations cmd) rpcinfo (Just $ checkAssertions errCodes) >>= \case
+        Cex tree -> do
           io $ putStrLn "Assertion violation found."
           showCounterexample preState maybesig
           treeShowing tree
           io $ exitWith (ExitFailure 1)
-        Left tree -> do
+        Timeout _ -> do
+          io $ exitWith (ExitFailure 1)
+        Qed tree -> do
           io $ putStrLn $ "Explored: " <> show (length tree)
                        <> " branches without assertion violations"
           treeShowing tree
@@ -698,12 +711,13 @@
 vmFromCommand cmd = do
   withCache <- applyCache (state cmd, cache cmd)
 
-  (miner,ts,blockNum,diff) <- case rpc cmd of
-    Nothing -> return (0,0,0,0)
+  (miner,ts,baseFee,blockNum,diff) <- case rpc cmd of
+    Nothing -> return (0,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 _baseFee
                                    , wordValue _number
                                    , wordValue _difficulty
                                    )
@@ -736,7 +750,7 @@
     (_, _, Nothing) ->
       error "must provide at least (rpc + address) or code"
 
-  return $ VMTest.initTx $ withCache (vm0 miner ts blockNum diff contract)
+  return $ VMTest.initTx $ withCache (vm0 baseFee miner ts blockNum diff contract)
     where
         decipher = hexByteString "bytes" . strip0x
         block'   = maybe EVM.Fetch.Latest EVM.Fetch.BlockNumber (block cmd)
@@ -749,7 +763,7 @@
               then addr address (createAddress origin' (word nonce 0))
               else addr address 0xacab
 
-        vm0 miner ts blockNum diff c = EVM.makeVm $ EVM.VMOpts
+        vm0 baseFee miner ts blockNum diff c = EVM.makeVm $ EVM.VMOpts
           { EVM.vmoptContract      = c
           , EVM.vmoptCalldata      = (calldata', litWord (num $ len calldata'))
           , EVM.vmoptValue         = w256lit value'
@@ -757,6 +771,8 @@
           , EVM.vmoptCaller        = litAddr caller'
           , EVM.vmoptOrigin        = origin'
           , EVM.vmoptGas           = word gas 0
+          , EVM.vmoptBaseFee       = baseFee
+          , EVM.vmoptPriorityFee   = word priorityFee 0
           , EVM.vmoptGaslimit      = word gas 0
           , EVM.vmoptCoinbase      = addr coinbase miner
           , EVM.vmoptNumber        = word number blockNum
@@ -779,12 +795,13 @@
 symvmFromCommand :: Command Options.Unwrapped -> Query EVM.VM
 symvmFromCommand cmd = do
 
-  (miner,blockNum,diff) <- case rpc cmd of
-    Nothing -> return (0,0,0)
+  (miner,blockNum,baseFee,diff) <- case rpc cmd of
+    Nothing -> return (0,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 _baseFee
                                    , wordValue _difficulty
                                    )
 
@@ -844,7 +861,7 @@
     (_, _, Nothing) ->
       error "must provide at least (rpc + address) or code"
 
-  return $ (VMTest.initTx $ withCache $ vm0 miner ts blockNum diff cdlen calldata' callvalue' caller' contract')
+  return $ (VMTest.initTx $ withCache $ vm0 baseFee miner ts blockNum diff cdlen calldata' callvalue' caller' contract')
     & over EVM.constraints (<> [pathCond])
     & set (EVM.env . EVM.contracts . (ix address') . EVM.storage) store
 
@@ -856,7 +873,7 @@
     address' = if create cmd
           then addr address (createAddress origin' (word nonce 0))
           else addr address 0xacab
-    vm0 miner ts blockNum diff cdlen calldata' callvalue' caller' c = EVM.makeVm $ EVM.VMOpts
+    vm0 baseFee miner ts blockNum diff cdlen calldata' callvalue' caller' c = EVM.makeVm $ EVM.VMOpts
       { EVM.vmoptContract      = c
       , EVM.vmoptCalldata      = (calldata', cdlen)
       , EVM.vmoptValue         = callvalue'
@@ -865,6 +882,8 @@
       , EVM.vmoptOrigin        = origin'
       , EVM.vmoptGas           = word gas 0xffffffffffffffff
       , EVM.vmoptGaslimit      = word gas 0xffffffffffffffff
+      , EVM.vmoptBaseFee       = baseFee
+      , EVM.vmoptPriorityFee   = word priorityFee 0
       , EVM.vmoptCoinbase      = addr coinbase miner
       , EVM.vmoptNumber        = word number blockNum
       , EVM.vmoptTimestamp     = ts
diff --git a/hevm.cabal b/hevm.cabal
--- a/hevm.cabal
+++ b/hevm.cabal
@@ -2,7 +2,7 @@
 name:
   hevm
 version:
-  0.47.0
+  0.48.0
 synopsis:
   Ethereum virtual machine evaluator
 description:
@@ -81,6 +81,7 @@
     ethjet/tinykeccak.h, ethjet/ethjet.h, ethjet/ethjet-ff.h, ethjet/blake2.h
   build-depends:
     QuickCheck                        >= 2.13.2 && < 2.15,
+    async                             == 2.2.3,
     Decimal                           >= 0.5.1 && < 0.6,
     containers                        >= 0.6.0 && < 0.7,
     deepseq                           >= 1.4.4 && < 1.5,
@@ -104,7 +105,7 @@
     filepath                          >= 1.4.2 && < 1.5,
     vty                               >= 5.25.1 && < 5.34,
     cereal                            >= 0.5.8 && < 0.6,
-    cryptonite                        >= 0.27 && < 0.29,
+    cryptonite                        >= 0.27 && <= 0.29,
     memory                            >= 0.14.18 && < 0.16,
     data-dword                        >= 0.3.1 && < 0.4,
     fgl                               >= 5.7.0 && < 5.8,
diff --git a/src/EVM.hs b/src/EVM.hs
--- a/src/EVM.hs
+++ b/src/EVM.hs
@@ -75,7 +75,6 @@
   | StackUnderrun
   | BadJumpDestination
   | Revert ByteString
-  | NoSuchContract Addr
   | OutOfGas Word Word
   | BadCheatCode (Maybe Word32)
   | StackLimitExceeded
@@ -86,6 +85,7 @@
   | InvalidMemoryAccess
   | CallDepthLimitReached
   | MaxCodeSizeExceeded Word Word
+  | InvalidFormat
   | PrecompileFailure
   | UnexpectedSymbolicArg
   | DeadPath
@@ -195,6 +195,7 @@
   { vmoptContract :: Contract
   , vmoptCalldata :: (Buffer, SymWord)
   , vmoptValue :: SymWord
+  , vmoptPriorityFee :: W256
   , vmoptAddress :: Addr
   , vmoptCaller :: SAddr
   , vmoptOrigin :: Addr
@@ -207,6 +208,7 @@
   , vmoptMaxCodeSize :: W256
   , vmoptBlockGaslimit :: W256
   , vmoptGasprice :: W256
+  , vmoptBaseFee :: W256
   , vmoptSchedule :: FeeSchedule Integer
   , vmoptChainId :: W256
   , vmoptCreate :: Bool
@@ -269,6 +271,7 @@
 data TxState = TxState
   { _gasprice            :: Word
   , _txgaslimit          :: Word
+  , _txPriorityFee       :: Word
   , _origin              :: Addr
   , _toAddr              :: Addr
   , _value               :: SymWord
@@ -377,6 +380,7 @@
   , _number      :: Word
   , _difficulty  :: Word
   , _gaslimit    :: Word
+  , _baseFee     :: Word
   , _maxCodeSize :: Word
   , _schedule    :: FeeSchedule Integer
   } deriving Show
@@ -460,6 +464,7 @@
   , _tx = TxState
     { _gasprice = w256 $ vmoptGasprice o
     , _txgaslimit = w256 $ vmoptGaslimit o
+    , _txPriorityFee = w256 $ vmoptPriorityFee o
     , _origin = txorigin
     , _toAddr = txtoAddr
     , _value = vmoptValue o
@@ -478,6 +483,7 @@
     , _difficulty = w256 $ vmoptDifficulty o
     , _maxCodeSize = w256 $ vmoptMaxCodeSize o
     , _gaslimit = w256 $ vmoptBlockGaslimit o
+    , _baseFee = w256 $ vmoptBaseFee o
     , _schedule = vmoptSchedule o
     }
   , _state = FrameState
@@ -963,6 +969,11 @@
           limitStack 1 . burn g_low $
             next >> push (view balance this)
 
+        -- op: BASEFEE
+        0x48 ->
+          limitStack 1 . burn g_base $
+            next >> push (the block baseFee)
+
         -- op: POP
         0x50 ->
           case stk of
@@ -1052,12 +1063,12 @@
                             unless (current' == new') $
                               if current' == original
                               then when (original /= 0 && new' == 0) $
-                                      refund r_sclear
+                                      refund (g_sreset + g_access_list_storage_key)
                               else do
                                       when (original /= 0) $
                                         if new' == 0
-                                        then refund r_sclear
-                                        else unRefund r_sclear
+                                        then refund (g_sreset + g_access_list_storage_key)
+                                        else unRefund (g_sreset + g_access_list_storage_key)
                                       when (original == new') $
                                         if original == 0
                                         then refund (g_sset - g_sload)
@@ -1198,31 +1209,24 @@
                   output = readMemory xOffset xSize vm
                   codesize = num (len output)
                   maxsize = the block maxCodeSize
-                case view frames vm of
-                  [] ->
-                    case (the tx isCreate) of
-                      True ->
-                        if codesize > maxsize
-                        then
-                          finishFrame (FrameErrored (MaxCodeSizeExceeded maxsize codesize))
-                        else
-                          burn (g_codedeposit * num codesize) $
-                            finishFrame (FrameReturned output)
-                      False ->
+                  creation = case view frames vm of
+                    [] -> the tx isCreate
+                    frame:_ -> case view frameContext frame of
+                       CreationContext {} -> True
+                       CallContext {} -> False
+                if creation
+                then
+                  if codesize > maxsize
+                  then
+                    finishFrame (FrameErrored (MaxCodeSizeExceeded maxsize codesize))
+                  else
+                    if isConcretely (readByteOrZero 0 output) ((==) 0xef)
+                    then finishFrame $ FrameErrored InvalidFormat
+                    else do
+                      burn (g_codedeposit * num codesize) $
                         finishFrame (FrameReturned output)
-                  (frame: _) -> do
-                    let
-                      context = view frameContext frame
-                    case context of
-                      CreationContext {} ->
-                        if codesize > maxsize
-                        then
-                          finishFrame (FrameErrored (MaxCodeSizeExceeded maxsize codesize))
-                        else
-                          burn (g_codedeposit * num codesize) $
-                            finishFrame (FrameReturned output)
-                      CallContext {} ->
-                          finishFrame (FrameReturned output)
+                else
+                   finishFrame (FrameReturned output)
             _ -> underrun
 
         -- op: DELEGATECALL
@@ -1299,8 +1303,6 @@
                           then num g_selfdestruct_newaccount
                           else 0
               burn (g_selfdestruct + c_new + cost) $ do
-                   destructs <- use (tx . substate . selfdestructs)
-                   unless (elem self destructs) $ refund r_selfdestruct
                    selfdestruct self
                    touchAccount xTo
 
@@ -1621,9 +1623,9 @@
                      condition' (fst <$> pathconds) choosePath
 
    where condition' = simplifyCondition condition whiff
-     -- Only one path is possible
 
          choosePath :: BranchCondition -> EVM ()
+         -- Only one path is possible
          choosePath (Case v) = do assign result Nothing
                                   pushTo constraints $ if v then (condition', whiff) else (sNot condition', IsZero whiff)
                                   iteration <- use (iterations . at codeloc . non 0)
@@ -1652,12 +1654,7 @@
               (\c -> do assign (cache . fetched . at addr) (Just c)
                         assign (env . contracts . at addr) (Just c)
                         assign result Nothing
-                        tryContinue c)
-  where
-    tryContinue c =
-      if (view external c) && (accountEmpty c)
-        then vmError . NoSuchContract $ addr
-        else continue c
+                        continue c)
 
 readStorage :: Storage -> SymWord -> Maybe (SymWord)
 readStorage (Symbolic _ s) (S w loc) = Just $ S (FromStorage w s) $ readArray s loc
@@ -1750,15 +1747,17 @@
   miner        <- use (block . coinbase)
   blockReward  <- num . r_block <$> (use (block . schedule))
   gasPrice     <- use (tx . gasprice)
+  priorityFee  <- use (tx . txPriorityFee)
   gasLimit     <- use (tx . txgaslimit)
   gasRemaining <- use (state . gas)
 
   let
     gasUsed      = gasLimit - gasRemaining
-    cappedRefund = min (quot gasUsed 2) (num sumRefunds)
+    cappedRefund = min (quot gasUsed 5) (num sumRefunds)
     originPay    = (gasRemaining + cappedRefund) * gasPrice
-    minerPay     = gasPrice * (gasUsed - cappedRefund)
 
+    minerPay     = priorityFee * gasUsed
+
   modifying (env . contracts)
      (Map.adjust (over balance (+ originPay)) txOrigin)
   modifying (env . contracts)
@@ -2086,11 +2085,7 @@
         callChecks this gasGiven xContext' xTo' xValue xInOffset xInSize xOutOffset xOutSize xs $
         \xGas -> do
           vm0 <- get
-          fetchAccount xTo' . const $
-            preuse (env . contracts . ix xTo') >>= \case
-              Nothing ->
-                vmError (NoSuchContract xTo')
-              Just target -> do
+          fetchAccount xTo' $ \target ->
                 burn xGas $ do
                   let newContext = CallContext
                                     { callContextTarget    = xTo'
diff --git a/src/EVM/Dev.hs b/src/EVM/Dev.hs
--- a/src/EVM/Dev.hs
+++ b/src/EVM/Dev.hs
@@ -63,6 +63,7 @@
         { oracle = EVM.Fetch.zero
         , verbose = Nothing
         , maxIter = Nothing
+        , askSmtIters = Nothing
         , smtTimeout = Nothing
         , smtState = Nothing
         , solver = Nothing
@@ -73,7 +74,7 @@
         , dapp = emptyDapp
         , testParams = params
         , maxDepth = Nothing
-        , allowFFI = False
+        , ffiAllowed = False
         }
     readSolc path >>=
       \case
@@ -122,6 +123,7 @@
         { oracle = EVM.Fetch.zero
         , verbose = Nothing
         , maxIter = Nothing
+        , askSmtIters = Nothing
         , smtTimeout = Nothing
         , smtState = Nothing
         , solver = Nothing
@@ -132,7 +134,7 @@
         , dapp = emptyDapp
         , testParams = params
         , maxDepth = Nothing
-        , allowFFI = False
+        , ffiAllowed = False
         }
     EVM.TTY.main testOpts root path
 
diff --git a/src/EVM/Emacs.hs b/src/EVM/Emacs.hs
--- a/src/EVM/Emacs.hs
+++ b/src/EVM/Emacs.hs
@@ -505,20 +505,21 @@
 defaultUnitTestOptions = do
   params <- liftIO $ getParametersFromEnvironmentVariables Nothing
   pure UnitTestOptions
-    { oracle            = Fetch.zero
-    , verbose           = Nothing
-    , maxIter           = Nothing
-    , smtTimeout        = Nothing
-    , smtState          = Nothing
-    , solver            = Nothing
-    , match             = ""
-    , fuzzRuns          = 100
-    , replay            = Nothing
-    , vmModifier        = id
-    , dapp              = emptyDapp
-    , testParams        = params
-    , maxDepth          = Nothing
-    , allowFFI          = False
+    { oracle      = Fetch.zero
+    , verbose     = Nothing
+    , maxIter     = Nothing
+    , askSmtIters = Nothing
+    , smtTimeout  = Nothing
+    , smtState    = Nothing
+    , solver      = Nothing
+    , match       = ""
+    , fuzzRuns    = 100
+    , replay      = Nothing
+    , vmModifier  = id
+    , dapp        = emptyDapp
+    , testParams  = params
+    , maxDepth    = Nothing
+    , ffiAllowed  = False
     }
 
 initialStateForTest
diff --git a/src/EVM/Exec.hs b/src/EVM/Exec.hs
--- a/src/EVM/Exec.hs
+++ b/src/EVM/Exec.hs
@@ -35,6 +35,8 @@
     , vmoptDifficulty = 0
     , vmoptGas = 0xffffffffffffffff
     , vmoptGaslimit = 0xffffffffffffffff
+    , vmoptBaseFee = 0
+    , vmoptPriorityFee = 0
     , vmoptMaxCodeSize = 0xffffffff
     , vmoptSchedule = FeeSchedule.berlin
     , vmoptChainId = 1
diff --git a/src/EVM/Facts.hs b/src/EVM/Facts.hs
--- a/src/EVM/Facts.hs
+++ b/src/EVM/Facts.hs
@@ -47,7 +47,6 @@
 import Control.Lens    (view, set, at, ix, (&), over, assign)
 import Control.Monad.State.Strict (execState, when)
 import Data.ByteString (ByteString)
-import Data.Monoid     ((<>))
 import Data.Ord        (comparing)
 import Data.Set        (Set)
 import Text.Read       (readMaybe)
@@ -119,7 +118,7 @@
     , NonceFact   a (view nonce x)
     , CodeFact    a b
     ]
-  SymbolicBuffer b ->
+  SymbolicBuffer _ ->
     -- here simply ignore storing the bytecode
     storageFacts a x ++
     [ BalanceFact a (view balance x)
diff --git a/src/EVM/Fetch.hs b/src/EVM/Fetch.hs
--- a/src/EVM/Fetch.hs
+++ b/src/EVM/Fetch.hs
@@ -5,6 +5,7 @@
 module EVM.Fetch where
 
 import Prelude hiding (Word)
+import Data.Scientific
 
 import EVM.ABI
 import EVM.Types    (Addr, w256, W256, hexText, Word, Buffer(..))
@@ -16,12 +17,12 @@
 
 import Control.Lens hiding ((.=))
 import Control.Monad.Reader
-import Control.Monad.Trans.Maybe
 import Data.SBV.Trans.Control
 import qualified Data.SBV.Internals as SBV
 import Data.SBV.Trans hiding (Word)
 import Data.Aeson
 import Data.Aeson.Lens
+import Control.Concurrent.Async
 import qualified Data.ByteString as BS
 import Data.Text (Text, unpack, pack)
 
@@ -34,6 +35,7 @@
 
 -- | Abstract representation of an RPC fetch request
 data RpcQuery a where
+  QueryAccount :: Addr         -> RpcQuery (BS.ByteString, W256, W256)
   QueryCode    :: Addr         -> RpcQuery BS.ByteString
   QueryBlock   ::                 RpcQuery Block
   QueryBalance :: Addr         -> RpcQuery W256
@@ -45,10 +47,10 @@
 
 deriving instance Show (RpcQuery a)
 
-rpc :: String -> [Value] -> Value
-rpc method args = object
+rpc :: String -> [Value] -> Scientific -> Value
+rpc method args i = object
   [ "jsonrpc" .= ("2.0" :: String)
-  , "id"      .= Number 1
+  , "id"      .= Number i
   , "method"  .= method
   , "params"  .= args
   ]
@@ -79,36 +81,41 @@
   -> RpcQuery a
   -> IO (Maybe a)
 fetchQuery n f q = do
-  x <- case q of
+  case q of
+    QueryAccount addr -> do
+        [m, m', m''] <- mapConcurrently (\(x, i) -> f (rpc x [toRPC addr, toRPC n] i)) [("eth_getCode", 1), ("eth_getBalance", 2), ("eth_getTransactionCount", 3)]
+        return $ liftM3 (\a b c ->
+          (hexText . view _String $ a,
+           readText . view _String $ b,
+           readText . view _String $ c)) m m' m''
     QueryCode addr -> do
-        m <- f (rpc "eth_getCode" [toRPC addr, toRPC n])
+        m <- f (rpc "eth_getCode" [toRPC addr, toRPC n] 1)
         return $ hexText . view _String <$> m
     QueryNonce addr -> do
-        m <- f (rpc "eth_getTransactionCount" [toRPC addr, toRPC n])
+        m <- f (rpc "eth_getTransactionCount" [toRPC addr, toRPC n] 1)
         return $ readText . view _String <$> m
     QueryBlock -> do
-      m <- f (rpc "eth_getBlockByNumber" [toRPC n, toRPC False])
+      m <- f (rpc "eth_getBlockByNumber" [toRPC n, toRPC False] 1)
       return $ m >>= parseBlock
     QueryBalance addr -> do
-        m <- f (rpc "eth_getBalance" [toRPC addr, toRPC n])
+        m <- f (rpc "eth_getBalance" [toRPC addr, toRPC n] 1)
         return $ readText . view _String <$> m
     QuerySlot addr slot -> do
-        m <- f (rpc "eth_getStorageAt" [toRPC addr, toRPC slot, toRPC n])
+        m <- f (rpc "eth_getStorageAt" [toRPC addr, toRPC slot, toRPC n] 1)
         return $ readText . view _String <$> m
     QueryChainId -> do
-        m <- f (rpc "eth_chainId" [toRPC n])
+        m <- f (rpc "eth_chainId" [toRPC n] 1)
         return $ readText . view _String <$> m
-  return x
 
-
 parseBlock :: (AsValue s, Show s) => s -> Maybe EVM.Block
 parseBlock j = do
   coinbase   <- readText <$> j ^? key "miner" . _String
   timestamp  <- litWord . readText <$> j ^? key "timestamp" . _String
   number     <- readText <$> j ^? key "number" . _String
   difficulty <- readText <$> j ^? key "difficulty" . _String
+  baseFee    <- readText <$> j ^? key "baseFeePerGas" . _String
   -- default codesize, default gas limit, default feescedule
-  return $ EVM.Block coinbase timestamp number difficulty 0xffffffff 0xffffffff FeeSchedule.berlin
+  return $ EVM.Block coinbase timestamp number difficulty 0xffffffff baseFee 0xffffffff FeeSchedule.berlin
 
 fetchWithSession :: Text -> Session -> Value -> IO (Maybe Value)
 fetchWithSession url sess x = do
@@ -117,20 +124,19 @@
 
 fetchContractWithSession
   :: BlockNumber -> Text -> Addr -> Session -> IO (Maybe Contract)
-fetchContractWithSession n url addr sess = runMaybeT $ do
+fetchContractWithSession n url addr sess =
   let
     fetch :: Show a => RpcQuery a -> IO (Maybe a)
     fetch = fetchQuery n (fetchWithSession url sess)
-
-  theCode    <- MaybeT $ fetch (QueryCode addr)
-  theNonce   <- MaybeT $ fetch (QueryNonce addr)
-  theBalance <- MaybeT $ fetch (QueryBalance addr)
-
-  return $
-    initialContract (EVM.RuntimeCode (ConcreteBuffer theCode))
-      & set nonce    (w256 theNonce)
-      & set balance  (w256 theBalance)
-      & set external True
+  in
+   fetch (QueryAccount addr) >>= \case
+     Nothing -> return Nothing
+     Just (theCode, theBalance, theNonce) ->
+       return $ Just $ 
+          initialContract (EVM.RuntimeCode (ConcreteBuffer theCode))
+            & set nonce    (w256 theNonce)
+            & set balance  (w256 theBalance)
+            & set external True
 
 fetchSlotWithSession
   :: BlockNumber -> Text -> Session -> Addr -> W256 -> IO (Maybe Word)
diff --git a/src/EVM/Solidity.hs b/src/EVM/Solidity.hs
--- a/src/EVM/Solidity.hs
+++ b/src/EVM/Solidity.hs
@@ -9,6 +9,9 @@
   ( solidity
   , solcRuntime
   , solidity'
+  , yul'
+  , yul
+  , yulRuntime
   , JumpType (..)
   , SolcContract (..)
   , StorageItem (..)
@@ -293,6 +296,22 @@
         sourceCache <- makeSourceCache sources asts
         return $! Just (contracts, sourceCache)
 
+yul :: Text -> Text -> IO (Maybe ByteString)
+yul contract src = do
+  (json, path) <- yul' src
+  let (Just f) = json ^?! key "contracts" ^? key path
+      (Just c) = f ^? key (if Text.null contract then "object" else contract)
+      bytecode = c ^?! key "evm" ^?! key "bytecode" ^?! key "object" . _String
+  pure $ toCode <$> (Just bytecode)
+
+yulRuntime :: Text -> Text -> IO (Maybe ByteString)
+yulRuntime contract src = do
+  (json, path) <- yul' src
+  let (Just f) = json ^?! key "contracts" ^? key path
+      (Just c) = f ^? key (if Text.null contract then "object" else contract)
+      bytecode = c ^?! key "evm" ^?! key "deployedBytecode" ^?! key "object" . _String
+  pure $ toCode <$> (Just bytecode)
+
 solidity :: Text -> Text -> IO (Maybe ByteString)
 solidity contract src = do
   (json, path) <- solidity' src
@@ -334,8 +353,9 @@
       let
         theRuntimeCode = toCode (x ^?! key "bin-runtime" . _String)
         theCreationCode = toCode (x ^?! key "bin" . _String)
-        abis =
-          toList ((x ^?! key "abi" . _String) ^?! _Array)
+        abis = toList $ case (x ^?! key "abi") ^? _Array of
+                 Just v -> v                                       -- solc >= 0.8
+                 Nothing -> (x ^?! key "abi" . _String) ^?! _Array -- solc <  0.8
       in SolcContract {
         _runtimeCode      = theRuntimeCode,
         _creationCode     = theCreationCode,
@@ -347,7 +367,7 @@
         _constructorInputs = mkConstructor abis,
         _abiMap       = mkAbiMap abis,
         _eventMap     = mkEventMap abis,
-        _storageLayout = mkStorageLayout $ x ^? key "storage-layout" . _String,
+        _storageLayout = mkStorageLayout $ x ^? key "storage-layout",
         _immutableReferences = mempty -- TODO: deprecate combined-json
       }
 
@@ -389,7 +409,7 @@
         _constructorInputs = mkConstructor abis,
         _abiMap        = mkAbiMap abis,
         _eventMap      = mkEventMap abis,
-        _storageLayout = mkStorageLayout $ x ^? key "storageLayout" . _String,
+        _storageLayout = mkStorageLayout $ x ^? key "storageLayout",
         _immutableReferences = fromMaybe mempty $
           do x' <- runtime ^? key "immutableReferences"
              case fromJSON x' of
@@ -444,7 +464,7 @@
       [] -> [] -- default constructor has zero inputs
       _  -> error "strange: contract has multiple constructors"
 
-mkStorageLayout :: Maybe Text -> Maybe (Map Text StorageItem)
+mkStorageLayout :: Maybe Value -> Maybe (Map Text StorageItem)
 mkStorageLayout Nothing = Nothing
 mkStorageLayout (Just json) = do
   items <- json ^? key "storage" . _Array
@@ -534,6 +554,25 @@
           }
         }
       }
+    }
+    |]
+  x <- pack <$>
+    readProcess
+      "solc"
+      ["--allow-paths", path, "--standard-json", (path <> ".json")]
+      ""
+  return (x, pack path)
+
+yul' :: Text -> IO (Text, Text)
+yul' src = withSystemTempFile "hevm.yul" $ \path handle -> do
+  hClose handle
+  writeFile path src
+  writeFile (path <> ".json")
+    [Here.i|
+    {
+      "language": "Yul",
+      "sources": { ${path}: { "urls": [ ${path} ] } },
+      "settings": { "outputSelection": { "*": { "*": ["*"], "": [ "*" ] } } }
     }
     |]
   x <- pack <$>
diff --git a/src/EVM/StorageLayout.hs b/src/EVM/StorageLayout.hs
--- a/src/EVM/StorageLayout.hs
+++ b/src/EVM/StorageLayout.hs
@@ -6,7 +6,7 @@
 import EVM.Solidity (SolcContract, creationSrcmap, SlotType(..))
 import EVM.ABI (AbiType (..), parseTypeName)
 
-import Data.Aeson (Value (Number))
+import Data.Aeson (Value (..))
 import Data.Aeson.Lens
 
 import Control.Lens
@@ -43,7 +43,7 @@
   let
     root :: Value
     root =
-      fromMaybe (error "no contract definition AST")
+      fromMaybe Null
         (findContractDefinition dapp solc)
   in
     case preview ( key "attributes"
diff --git a/src/EVM/SymExec.hs b/src/EVM/SymExec.hs
--- a/src/EVM/SymExec.hs
+++ b/src/EVM/SymExec.hs
@@ -34,6 +34,10 @@
 import qualified Control.Monad.State.Class as State
 import Control.Applicative
 
+data ProofResult a b c = Qed a | Cex b | Timeout c
+type VerifyResult = ProofResult (Tree BranchInfo) (Tree BranchInfo) (Tree BranchInfo)
+type EquivalenceResult = ProofResult ([VM], [VM]) VM ()
+
 -- | Convenience functions for generating large symbolic byte strings
 sbytes32, sbytes128, sbytes256, sbytes512, sbytes1024 :: Query ([SWord 8])
 sbytes32 = toBytes <$> freshVar_ @ (WordN 256)
@@ -134,6 +138,8 @@
     , vmoptDifficulty = 0
     , vmoptGas = 0xffffffffffffffff
     , vmoptGaslimit = 0xffffffffffffffff
+    , vmoptBaseFee = 0
+    , vmoptPriorityFee = 0
     , vmoptMaxCodeSize = 0xffffffff
     , vmoptSchedule = FeeSchedule.berlin
     , vmoptChainId = 1
@@ -149,14 +155,14 @@
     _branchCondition    :: Maybe Whiff
   }
 
-doInterpret :: Fetch.Fetcher -> Maybe Integer -> VM -> Query (Tree BranchInfo)
-doInterpret fetcher maxIter vm = let
-      f (vm', cs) = Node (BranchInfo (if length cs == 0 then vm' else vm) Nothing) cs
-    in f <$> interpret' fetcher maxIter vm
+doInterpret :: Fetch.Fetcher -> Maybe Integer -> Maybe Integer -> VM -> Query (Tree BranchInfo)
+doInterpret fetcher maxIter askSmtIters vm = let
+      f (vm', cs) = Node (BranchInfo (if null cs then vm' else vm) Nothing) cs
+    in f <$> interpret' fetcher maxIter askSmtIters vm
 
-interpret' :: Fetch.Fetcher -> Maybe Integer -> VM -> Query (VM, [(Tree BranchInfo)])
-interpret' fetcher maxIter vm = let
-  cont s = interpret' fetcher maxIter $ execState s vm
+interpret' :: Fetch.Fetcher -> Maybe Integer -> Maybe Integer -> VM -> Query (VM, [Tree BranchInfo])
+interpret' fetcher maxIter askSmtIters vm = let
+  cont s = interpret' fetcher maxIter askSmtIters $ execState s vm
   in case view EVM.result vm of
 
     Nothing -> cont exec1
@@ -166,7 +172,7 @@
       iteration = num $ fromMaybe 0 $ view (iterations . at codelocation) vm
       -- as an optimization, we skip consulting smt
       -- if we've been at the location less than 5 times
-      in if iteration < (max (fromMaybe 0 maxIter) 5)
+      in if iteration < (fromMaybe 5 askSmtIters)
          then cont $ continue EVM.Unknown
          else io (fetcher q) >>= cont
 
@@ -179,10 +185,10 @@
           rvm = execState (continue False) vm
           in do
             push 1
-            (leftvm, left) <- interpret' fetcher maxIter lvm
+            (leftvm, left) <- interpret' fetcher maxIter askSmtIters lvm
             pop 1
             push 1
-            (rightvm, right) <- interpret' fetcher maxIter rvm
+            (rightvm, right) <- interpret' fetcher maxIter askSmtIters rvm
             pop 1
             return (vm, [Node (BranchInfo leftvm (Just whiff)) left, Node (BranchInfo rightvm (Just whiff)) right])
         Just n -> cont $ continue (not n)
@@ -195,10 +201,11 @@
 -- | returns a list of possible final evm states
 interpret
   :: Fetch.Fetcher
-  -> Maybe Integer --max iterations
+  -> Maybe Integer -- max iterations
+  -> Maybe Integer -- ask smt iterations
   -> Stepper a
   -> StateT VM Query [a]
-interpret fetcher maxIter =
+interpret fetcher maxIter askSmtIters =
   eval . Operational.view
 
   where
@@ -212,47 +219,47 @@
     eval (action Operational.:>>= k) =
       case action of
         Stepper.Exec ->
-          exec >>= interpret fetcher maxIter . k
+          exec >>= interpret fetcher maxIter askSmtIters . k
         Stepper.Run ->
-          run >>= interpret fetcher maxIter . k
+          run >>= interpret fetcher maxIter askSmtIters . k
         Stepper.IOAct q ->
-          mapStateT io q >>= interpret fetcher maxIter . k
+          mapStateT io q >>= interpret fetcher maxIter askSmtIters . k
         Stepper.Ask (EVM.PleaseChoosePath _ continue) -> do
           vm <- get
           case maxIterationsReached vm maxIter of
             Nothing -> do
               push 1
-              a <- interpret fetcher maxIter (Stepper.evm (continue True) >>= k)
+              a <- interpret fetcher maxIter askSmtIters (Stepper.evm (continue True) >>= k)
               put vm
               pop 1
               push 1
-              b <- interpret fetcher maxIter (Stepper.evm (continue False) >>= k)
+              b <- interpret fetcher maxIter askSmtIters (Stepper.evm (continue False) >>= k)
               pop 1
               return $ a <> b
             Just n ->
-              interpret fetcher maxIter (Stepper.evm (continue (not n)) >>= k)
+              interpret fetcher maxIter askSmtIters (Stepper.evm (continue (not n)) >>= k)
         Stepper.Wait q -> do
           let performQuery = do
                 m <- liftIO (fetcher q)
-                interpret fetcher maxIter (Stepper.evm m >>= k)
+                interpret fetcher maxIter askSmtIters (Stepper.evm m >>= k)
 
           case q of
             PleaseAskSMT _ _ continue -> do
               codelocation <- getCodeLocation <$> get
-              iteration <- num <$> fromMaybe 0 <$> use (iterations . at codelocation)
+              iteration <- num . fromMaybe 0 <$> use (iterations . at codelocation)
 
               -- 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.
-              if iteration < (max (fromMaybe 0 maxIter) 5)
-              then interpret fetcher maxIter (Stepper.evm (continue EVM.Unknown) >>= k)
+              if iteration < (fromMaybe 5 askSmtIters)
+              then interpret fetcher maxIter askSmtIters (Stepper.evm (continue EVM.Unknown) >>= k)
               else performQuery
 
             _ -> performQuery
 
         Stepper.EVM m ->
-          State.state (runState m) >>= interpret fetcher maxIter . k
+          State.state (runState m) >>= interpret fetcher maxIter askSmtIters . k
 
 maxIterationsReached :: VM -> Maybe Integer -> Maybe Bool
 maxIterationsReached _ Nothing = Nothing
@@ -266,7 +273,7 @@
 type Precondition = VM -> SBool
 type Postcondition = (VM, VM) -> SBool
 
-checkAssert :: [Word256] -> ByteString -> Maybe (Text, [AbiType]) -> [String] -> Query (Either (Tree BranchInfo) (Tree BranchInfo), VM)
+checkAssert :: [Word256] -> ByteString -> Maybe (Text, [AbiType]) -> [String] -> Query (VerifyResult, VM)
 checkAssert errs c signature' concreteArgs = verifyContract c signature' concreteArgs SymbolicS (const sTrue) (Just $ checkAssertions errs)
 
 {- |Checks if an assertion violation has been encountered
@@ -305,12 +312,12 @@
 panicMsg :: Word256 -> ByteString
 panicMsg err = (selector "Panic(uint256)") <> (encodeAbiValue $ AbiUInt 256 err)
 
-verifyContract :: ByteString -> Maybe (Text, [AbiType]) -> [String] -> StorageModel -> Precondition -> Maybe Postcondition -> Query (Either (Tree BranchInfo) (Tree BranchInfo), VM)
+verifyContract :: ByteString -> Maybe (Text, [AbiType]) -> [String] -> StorageModel -> Precondition -> Maybe Postcondition -> Query (VerifyResult, 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 constraints ((++) [(pre preStateRaw, Todo "assumptions" [])]) preStateRaw
-    v <- verify preState Nothing Nothing maybepost
+    v <- verify preState Nothing Nothing Nothing maybepost
     return (v, preState)
 
 pruneDeadPaths :: [VM] -> [VM]
@@ -347,36 +354,41 @@
 leaves (Node _ xs) = concatMap leaves xs
 
 -- | Symbolically execute the VM and check all endstates against the postcondition, if available.
--- Returns `Right (Tree BranchInfo)` if the postcondition can be violated, or
--- or `Left (Tree BranchInfo)`, if the postcondition holds for all endstates.
-verify :: VM -> Maybe Integer -> Maybe (Fetch.BlockNumber, Text) -> Maybe Postcondition -> Query (Either (Tree BranchInfo) (Tree BranchInfo))
-verify preState maxIter rpcinfo maybepost = do
+verify :: VM -> Maybe Integer -> Maybe Integer -> Maybe (Fetch.BlockNumber, Text) -> Maybe Postcondition -> Query VerifyResult
+verify preState maxIter askSmtIters rpcinfo maybepost = do
   smtState <- queryState
-  tree <- doInterpret (Fetch.oracle (Just smtState) rpcinfo False) maxIter preState
+  tree <- doInterpret (Fetch.oracle (Just smtState) rpcinfo False) maxIter askSmtIters preState
   case maybepost of
     (Just post) -> do
       let livePaths = pruneDeadPaths $ leaves tree
-      -- can also do these queries individually (even concurrently!). Could save time and report multiple violations
+          -- have we hit max iterations at any point in a given path
+          maxReached :: VM -> Bool
+          maxReached p = case maxIter of
+            Just maxI -> any (>= (fromInteger maxI)) (view iterations p)
+            Nothing -> False
+          -- is there any path which can possibly violate the postcondition?
+          -- can also do these queries individually (even concurrently!). Could save time and report multiple violations
           postC = sOr $ fmap (\postState -> (sAnd (fst <$> view constraints postState)) .&& sNot (post (preState, postState))) livePaths
-      -- is there any path which can possibly violate
-      -- the postcondition?
       resetAssertions
       constrain postC
       io $ putStrLn "checking postcondition..."
       checkSat >>= \case
         Unk -> do io $ putStrLn "postcondition query timed out"
-                  return $ Left tree
-        Unsat -> do io $ putStrLn "Q.E.D."
-                    return $ Left tree
-        Sat -> return $ Right tree
+                  return $ Timeout tree
+        Unsat -> do
+          if any maxReached livePaths
+            then io $ putStrLn "WARNING: max iterations reached, execution halted prematurely"
+            else io $ putStrLn "Q.E.D."
+          return $ Qed tree
+        Sat -> return $ Cex tree
         DSat _ -> error "unexpected DSAT"
 
     Nothing -> do io $ putStrLn "Nothing to check"
-                  return $ Left tree
+                  return $ Qed tree
 
 -- | Compares two contract runtimes for trace equivalence by running two VMs and comparing the end states.
-equivalenceCheck :: ByteString -> ByteString -> Maybe Integer -> Maybe (Text, [AbiType]) -> Query (Either ([VM], [VM]) VM)
-equivalenceCheck bytecodeA bytecodeB maxiter signature' = do
+equivalenceCheck :: ByteString -> ByteString -> Maybe Integer -> Maybe Integer -> Maybe (Text, [AbiType]) -> Query EquivalenceResult
+equivalenceCheck bytecodeA bytecodeB maxiter askSmtIters signature' = do
   let
     bytecodeA' = if BS.null bytecodeA then BS.pack [0] else bytecodeA
     bytecodeB' = if BS.null bytecodeB then BS.pack [0] else bytecodeB
@@ -392,10 +404,10 @@
 
   smtState <- queryState
   push 1
-  aVMs <- doInterpret (Fetch.oracle (Just smtState) Nothing False) maxiter preStateA
+  aVMs <- doInterpret (Fetch.oracle (Just smtState) Nothing False) maxiter askSmtIters preStateA
   pop 1
   push 1
-  bVMs <- doInterpret (Fetch.oracle (Just smtState) Nothing False) maxiter preStateB
+  bVMs <- doInterpret (Fetch.oracle (Just smtState) Nothing False) maxiter askSmtIters preStateB
   pop 1
   -- Check each pair of endstates for equality:
   let differingEndStates = uncurry distinct <$> [(a,b) | a <- pruneDeadPaths (leaves aVMs), b <- pruneDeadPaths (leaves bVMs)]
@@ -428,9 +440,9 @@
   constrain $ sOr differingEndStates
 
   checkSat >>= \case
-     Unk -> error "solver said unknown!"
-     Sat -> return $ Right preStateA
-     Unsat -> return $ Left (leaves aVMs, leaves bVMs)
+     Unk -> return $ Timeout ()
+     Sat -> return $ Cex preStateA
+     Unsat -> return $ Qed (leaves aVMs, leaves bVMs)
      DSat _ -> error "unexpected DSAT"
 
 both' :: (a -> b) -> (a, a) -> (b, b)
diff --git a/src/EVM/Symbolic.hs b/src/EVM/Symbolic.hs
--- a/src/EVM/Symbolic.hs
+++ b/src/EVM/Symbolic.hs
@@ -259,13 +259,13 @@
   Div x y       -> whiffValue x `sDiv` whiffValue y
   Mod x y       -> whiffValue x `sMod` whiffValue y
   Exp x y       -> whiffValue x .^ whiffValue y
-  Neg x         -> negate $ whiffValue x
+  Neg x         -> complement $ whiffValue x
   Var _ v       -> v
   FromKeccak (ConcreteBuffer bstr) -> literal $ num $ keccak bstr
   FromKeccak (SymbolicBuffer buf)  -> symkeccak' buf
   Literal x -> literal $ num $ x
   FromBytes buf -> rawVal $ readMemoryWord 0 buf
-  FromStorage ind arr -> readArray arr (whiffValue ind) 
+  FromStorage ind arr -> readArray arr (whiffValue ind)
 
 -- | Special cases that have proven useful in practice
 simplifyCondition :: SBool -> Whiff -> SBool
diff --git a/src/EVM/TTY.hs b/src/EVM/TTY.hs
--- a/src/EVM/TTY.hs
+++ b/src/EVM/TTY.hs
@@ -234,20 +234,21 @@
 
   let
     opts = UnitTestOptions
-      { oracle            = oracle'
-      , verbose           = Nothing
-      , maxIter           = maxIter'
-      , smtTimeout        = Nothing
-      , smtState          = Nothing
-      , solver            = Nothing
-      , maxDepth          = Nothing
-      , match             = ""
-      , fuzzRuns          = 1
-      , replay            = error "irrelevant"
-      , vmModifier        = id
-      , testParams        = error "irrelevant"
-      , dapp              = dappinfo
-      , allowFFI          = False
+      { oracle        = oracle'
+      , verbose       = Nothing
+      , maxIter       = maxIter'
+      , askSmtIters   = Nothing
+      , smtTimeout    = Nothing
+      , smtState      = Nothing
+      , solver        = Nothing
+      , maxDepth      = Nothing
+      , match         = ""
+      , fuzzRuns      = 1
+      , replay        = error "irrelevant"
+      , vmModifier    = id
+      , testParams    = error "irrelevant"
+      , dapp          = dappinfo
+      , ffiAllowed    = False
       }
     ui0 = initUiVmState vm opts (void Stepper.execFully)
 
@@ -623,7 +624,9 @@
   -> IO UiVmState
 initialUiVmStateForTest opts@UnitTestOptions{..} (theContractName, theTestName) = do
   let state' = fromMaybe (error "Internal Error: missing smtState") smtState
-  (buf, len) <- flip runReaderT state' $ SBV.runQueryT $ symCalldata theTestName types []
+  (buf, len) <- case test of
+    SymbolicTest _ -> flip runReaderT state' $ SBV.runQueryT $ symCalldata theTestName types []
+    _ -> return (error "unreachable", error "unreachable")
   let script = do
         Stepper.evm . pushTrace . EntryTrace $
           "test " <> theTestName <> " (" <> theContractName <> ")"
diff --git a/src/EVM/Transaction.hs b/src/EVM/Transaction.hs
--- a/src/EVM/Transaction.hs
+++ b/src/EVM/Transaction.hs
@@ -29,12 +29,13 @@
 
 data TxType = LegacyTransaction
             | AccessListTransaction
+            | EIP1559Transaction
   deriving (Show, Eq)
 
 data Transaction = Transaction {
     txData     :: ByteString,
     txGasLimit :: W256,
-    txGasPrice :: W256,
+    txGasPrice :: Maybe W256,
     txNonce    :: W256,
     txR        :: W256,
     txS        :: W256,
@@ -42,12 +43,13 @@
     txV        :: W256,
     txValue    :: W256,
     txType     :: TxType,
-    txAccessList :: [AccessListEntry]
+    txAccessList :: [AccessListEntry],
+    txMaxPriorityFeeGas :: Maybe W256,
+    txMaxFeePerGas :: Maybe W256
 } deriving Show
 
--- utility function for getting a more useful representation of accesslistentries
+-- | utility function for getting a more useful representation of accesslistentries
 -- duplicates only matter for gas computation
--- ugly! could use a review....
 txAccessMap :: Transaction -> Map Addr [W256]
 txAccessMap tx = ((Map.fromListWith (++)) . makeTups) $ txAccessList tx
   where makeTups = map (\ale -> (accessAddress ale, accessStorageKeys ale))
@@ -70,23 +72,27 @@
       then eip155Data
       else normalData
     AccessListTransaction -> eip2930Data
+    EIP1559Transaction -> eip1559Data
   where v          = fromIntegral (txV tx)
         to'        = case txToAddr tx of
           Just a  -> BS $ word160Bytes a
           Nothing -> BS mempty
+        Just maxFee = txMaxFeePerGas tx
+        Just maxPrio = txMaxPriorityFeeGas tx
+        Just gasPrice = txGasPrice tx
         accessList = txAccessList tx
         rlpAccessList = EVM.RLP.List $ map (\accessEntry ->
-          EVM.RLP.List [BS $ word160Bytes (accessAddress accessEntry), 
+          EVM.RLP.List [BS $ word160Bytes (accessAddress accessEntry),
                         EVM.RLP.List $ map rlpWordFull $ accessStorageKeys accessEntry]
           ) accessList
         normalData = rlpList [rlpWord256 (txNonce tx),
-                              rlpWord256 (txGasPrice tx),
+                              rlpWord256 gasPrice,
                               rlpWord256 (txGasLimit tx),
                               to',
                               rlpWord256 (txValue tx),
                               BS (txData tx)]
         eip155Data = rlpList [rlpWord256 (txNonce tx),
-                              rlpWord256 (txGasPrice tx),
+                              rlpWord256 gasPrice,
                               rlpWord256 (txGasLimit tx),
                               to',
                               rlpWord256 (txValue tx),
@@ -94,22 +100,33 @@
                               rlpWord256 (fromIntegral chainId),
                               rlpWord256 0x0,
                               rlpWord256 0x0]
+        eip1559Data = cons 0x02 $ rlpList [
+          rlpWord256 (fromIntegral chainId),
+          rlpWord256 (txNonce tx),
+          rlpWord256 maxPrio,
+          rlpWord256 maxFee,
+          rlpWord256 (txGasLimit tx),
+          to',
+          rlpWord256 (txValue tx),
+          BS (txData tx),
+          rlpAccessList]
+
         eip2930Data = cons 0x01 $ rlpList [
           rlpWord256 (fromIntegral chainId),
           rlpWord256 (txNonce tx),
-          rlpWord256 (txGasPrice tx),
+          rlpWord256 gasPrice,
           rlpWord256 (txGasLimit tx),
-          to', 
+          to',
           rlpWord256 (txValue tx),
           BS (txData tx),
           rlpAccessList]
 
 accessListPrice :: FeeSchedule Integer -> [AccessListEntry] -> Integer
 accessListPrice fs al =
-    sum (map 
-      (\ale -> 
-        g_access_list_address fs + 
-        (g_access_list_storage_key fs * (toInteger . length) (accessStorageKeys ale))) 
+    sum (map
+      (\ale ->
+        g_access_list_address fs +
+        (g_access_list_storage_key fs * (toInteger . length) (accessStorageKeys ale)))
         al)
 
 txGasCost :: FeeSchedule Integer -> Transaction -> Integer
@@ -118,7 +135,7 @@
       zeroBytes    = BS.count 0 calldata
       nonZeroBytes = BS.length calldata - zeroBytes
       baseCost     = g_transaction fs
-        + if isNothing (txToAddr tx) then g_txcreate fs else 0
+        + (if isNothing (txToAddr tx) then g_txcreate fs else 0)
         + (accessListPrice fs $ txAccessList tx)
       zeroCost     = g_txdatazero fs
       nonZeroCost  = g_txdatanonzero fs
@@ -127,8 +144,6 @@
 instance FromJSON AccessListEntry where
   parseJSON (JSON.Object val) = do
     accessAddress_ <- addrField val "address"
-    --storageKeys <- (val JSON..: "storageKeys")
-    --accessStorageKeys_ <- JSON.listParser (JSON.withText "W256" (return . readNull 0 . Text.unpack)) storageKeys
     accessStorageKeys_ <- (val JSON..: "storageKeys") >>= parseJSONList
     return $ AccessListEntry accessAddress_ accessStorageKeys_
   parseJSON invalid =
@@ -138,7 +153,9 @@
   parseJSON (JSON.Object val) = do
     tdata    <- dataField val "data"
     gasLimit <- wordField val "gasLimit"
-    gasPrice <- wordField val "gasPrice"
+    gasPrice <- fmap read <$> val JSON..:? "gasPrice"
+    maxPrio  <- fmap read <$> val JSON..:? "maxPriorityFeePerGas"
+    maxFee   <- fmap read <$> val JSON..:? "maxFeePerGas"
     nonce    <- wordField val "nonce"
     r        <- wordField val "r"
     s        <- wordField val "s"
@@ -146,14 +163,16 @@
     v        <- wordField val "v"
     value    <- wordField val "value"
     txType   <- fmap read <$> (val JSON..:? "type")
-    --let legacyTxn = Transaction tdata gasLimit gasPrice nonce r s toAddr v value
     case txType of
-      Just 0x00 -> return $ Transaction tdata gasLimit gasPrice nonce r s toAddr v value LegacyTransaction []
+      Just 0x00 -> return $ Transaction tdata gasLimit gasPrice nonce r s toAddr v value LegacyTransaction [] Nothing Nothing
       Just 0x01 -> do
         accessListEntries <- (val JSON..: "accessList") >>= parseJSONList
-        return $ Transaction tdata gasLimit gasPrice nonce r s toAddr v value AccessListTransaction accessListEntries
+        return $ Transaction tdata gasLimit gasPrice nonce r s toAddr v value AccessListTransaction accessListEntries Nothing Nothing
+      Just 0x02 -> do
+        accessListEntries <- (val JSON..: "accessList") >>= parseJSONList
+        return $ Transaction tdata gasLimit gasPrice nonce r s toAddr v value EIP1559Transaction accessListEntries maxPrio maxFee
       Just _ -> fail "unrecognized custom transaction type"
-      Nothing -> return $ Transaction tdata gasLimit gasPrice nonce r s toAddr v value LegacyTransaction []
+      Nothing -> return $ Transaction tdata gasLimit gasPrice nonce r s toAddr v value LegacyTransaction [] Nothing Nothing
   parseJSON invalid =
     JSON.typeMismatch "Transaction" invalid
 
diff --git a/src/EVM/Types.hs b/src/EVM/Types.hs
--- a/src/EVM/Types.hs
+++ b/src/EVM/Types.hs
@@ -245,8 +245,8 @@
       SGT x y     -> infix' " s> " x y
       IsZero x    -> "IsZero(" ++ show x ++ ")"
       SHL x y     -> infix' " << " x y
-      SHR x y     -> infix' " << " x y
-      SAR x y     -> infix' " a<< " x y
+      SHR x y     -> infix' " >> " x y
+      SAR x y     -> infix' " a>> " x y
       Add x y     -> infix' " + " x y
       Sub x y     -> infix' " - " x y
       Mul x y     -> infix' " * " x y
diff --git a/src/EVM/UnitTest.hs b/src/EVM/UnitTest.hs
--- a/src/EVM/UnitTest.hs
+++ b/src/EVM/UnitTest.hs
@@ -70,20 +70,21 @@
 import Test.QuickCheck hiding (verbose)
 
 data UnitTestOptions = UnitTestOptions
-  { oracle     :: EVM.Query -> IO (EVM ())
-  , verbose    :: Maybe Int
-  , maxIter    :: Maybe Integer
-  , maxDepth   :: Maybe Int
-  , smtTimeout :: Maybe Integer
-  , smtState   :: Maybe SBV.State
-  , solver     :: Maybe Text
-  , match      :: Text
-  , fuzzRuns   :: Int
-  , replay     :: Maybe (Text, BSLazy.ByteString)
-  , vmModifier :: VM -> VM
-  , dapp       :: DappInfo
-  , testParams :: TestVMParams
-  , allowFFI   :: Bool
+  { oracle      :: EVM.Query -> IO (EVM ())
+  , verbose     :: Maybe Int
+  , maxIter     :: Maybe Integer
+  , askSmtIters :: Maybe Integer
+  , maxDepth    :: Maybe Int
+  , smtTimeout  :: Maybe Integer
+  , smtState    :: Maybe SBV.State
+  , solver      :: Maybe Text
+  , match       :: Text
+  , fuzzRuns    :: Int
+  , replay      :: Maybe (Text, BSLazy.ByteString)
+  , vmModifier  :: VM -> VM
+  , dapp        :: DappInfo
+  , testParams  :: TestVMParams
+  , ffiAllowed  :: Bool
   }
 
 data TestVMParams = TestVMParams
@@ -92,8 +93,9 @@
   , testOrigin        :: Addr
   , testGasCreate     :: W256
   , testGasCall       :: W256
+  , testBaseFee       :: W256
+  , testPriorityFee   :: W256
   , testBalanceCreate :: W256
-  , testBalanceCall   :: W256
   , testCoinbase      :: Addr
   , testNumber        :: W256
   , testTimestamp     :: W256
@@ -110,11 +112,8 @@
 defaultGasForInvoking :: W256
 defaultGasForInvoking = 0xffffffffffff
 
-defaultBalanceForCreator :: W256
-defaultBalanceForCreator = 0xffffffffffffffffffffffff
-
-defaultBalanceForCreated :: W256
-defaultBalanceForCreated = 0xffffffffffffffffffffffff
+defaultBalanceForTestContract :: W256
+defaultBalanceForTestContract = 0xffffffffffffffffffffffff
 
 defaultMaxCodeSize :: W256
 defaultMaxCodeSize = 0xffffffff
@@ -441,7 +440,7 @@
 
 
 runTest :: UnitTestOptions -> VM -> (Test, [AbiType]) -> SBV.Query (Text, Either Text Text, VM)
-runTest opts@UnitTestOptions{..} vm (ConcreteTest testName, []) = liftIO $ runOne opts vm testName emptyAbi
+runTest opts@UnitTestOptions{} vm (ConcreteTest testName, []) = liftIO $ runOne opts vm testName emptyAbi
 runTest opts@UnitTestOptions{..} vm (ConcreteTest testName, types) = liftIO $ case replay of
   Nothing ->
     fuzzRun opts vm testName types
@@ -539,9 +538,9 @@
 
 getTargetContracts :: UnitTestOptions -> Stepper [Addr]
 getTargetContracts UnitTestOptions{..} = do
-  vm <- Stepper.evm $ get
-  let Just contract = currentContract vm
-      theAbi = view abiMap $ fromJust $ lookupCode (view contractcode contract) dapp
+  vm <- Stepper.evm get
+  let Just contract' = currentContract vm
+      theAbi = view abiMap $ fromJust $ lookupCode (view contractcode contract') dapp
       setUp  = abiKeccak (encodeUtf8 "targetContracts()")
   case Map.lookup setUp theAbi of
     Nothing -> return []
@@ -668,7 +667,7 @@
 
     -- get all posible postVMs for the test method
     allPaths <- fst <$> runStateT
-        (EVM.SymExec.interpret oracle maxIter (execSymTest opts testName cd')) vm
+        (EVM.SymExec.interpret oracle maxIter askSmtIters (execSymTest opts testName cd')) vm
     let consistentPaths = flip filter allPaths $
           \(_, vm') -> case view result vm' of
             Just (VMFailure DeadPath) -> False
@@ -704,7 +703,7 @@
               then Right ()
               else Left (vm', prettyCd)
           Unsat -> return $ Right ()
-          Unk -> return $ Left (vm', "unknown; query timeout")
+          Unk -> return $ Left (vm', "SMT Query Timeout! Try setting a higher timeout with the --smttimeout flag or the DAPP_TEST_SMTTIMEOUT environment variable.")
           DSat _ -> error "Unexpected DSat"
 
     if null $ lefts results
@@ -920,6 +919,8 @@
            , vmoptTimestamp = litWord $ w256 testTimestamp
            , vmoptBlockGaslimit = testGaslimit
            , vmoptGasprice = testGasprice
+           , vmoptBaseFee = testBaseFee
+           , vmoptPriorityFee = testPriorityFee
            , vmoptMaxCodeSize = testMaxCodeSize
            , vmoptDifficulty = testDifficulty
            , vmoptSchedule = FeeSchedule.berlin
@@ -927,7 +928,7 @@
            , vmoptCreate = True
            , vmoptStorageModel = ConcreteS -- TODO: support RPC
            , vmoptTxAccessList = mempty -- TODO: support unit test access lists???
-           , vmoptAllowFFI = allowFFI
+           , vmoptAllowFFI = ffiAllowed
            }
     creator =
       initialContract (RuntimeCode mempty)
@@ -975,8 +976,9 @@
     <*> getAddr "DAPP_TEST_ORIGIN" ethrunAddress
     <*> getWord "DAPP_TEST_GAS_CREATE" defaultGasForCreating
     <*> getWord "DAPP_TEST_GAS_CALL" defaultGasForInvoking
-    <*> getWord "DAPP_TEST_BALANCE_CREATE" defaultBalanceForCreator
-    <*> getWord "DAPP_TEST_BALANCE_CALL" defaultBalanceForCreated
+    <*> getWord "DAPP_TEST_BASEFEE" 0
+    <*> getWord "DAPP_TEST_PRIORITYFEE" 0
+    <*> getWord "DAPP_TEST_BALANCE" defaultBalanceForTestContract
     <*> getAddr "DAPP_TEST_COINBASE" miner
     <*> getWord "DAPP_TEST_NUMBER" blockNum
     <*> getWord "DAPP_TEST_TIMESTAMP" ts
diff --git a/src/EVM/VMTest.hs b/src/EVM/VMTest.hs
--- a/src/EVM/VMTest.hs
+++ b/src/EVM/VMTest.hs
@@ -30,7 +30,7 @@
 
 import GHC.Stack
 
-import Data.Aeson ((.:), FromJSON (..))
+import Data.Aeson ((.:), (.:?), FromJSON (..))
 import Data.Foldable (fold)
 import Data.Map (Map)
 import Data.Maybe (fromMaybe, isNothing)
@@ -48,6 +48,7 @@
   { blockCoinbase    :: Addr
   , blockDifficulty  :: W256
   , blockGasLimit    :: W256
+  , blockBaseFee     :: W256
   , blockNumber      :: W256
   , blockTimestamp   :: W256
   , blockTxs         :: [Transaction]
@@ -199,8 +200,9 @@
     difficulty <- wordField v' "difficulty"
     gasLimit   <- wordField v' "gasLimit"
     number     <- wordField v' "number"
+    baseFee    <- fmap read <$> v' .:? "baseFeePerGas"
     timestamp  <- wordField v' "timestamp"
-    return $ Block coinbase difficulty gasLimit number timestamp txs
+    return $ Block coinbase difficulty gasLimit (fromMaybe 0 baseFee) number timestamp txs
   parseJSON invalid =
     JSON.typeMismatch "Block" invalid
 
@@ -248,7 +250,7 @@
 fromBlockchainCase :: BlockchainCase -> Either BlockchainError Case
 fromBlockchainCase (BlockchainCase blocks preState postState network) =
   case (blocks, network) of
-    ([block], "Berlin") -> case blockTxs block of
+    ([block], "London") -> case blockTxs block of
       [tx] -> fromBlockchainCase' block tx preState postState
       []        -> Left NoTxs
       _         -> Left TooManyTxs
@@ -260,7 +262,7 @@
                        -> Either BlockchainError Case
 fromBlockchainCase' block tx preState postState =
   let isCreate = isNothing (txToAddr tx) in
-  case (sender 1 tx, checkTx tx preState) of
+  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
@@ -272,6 +274,8 @@
          , vmoptCaller        = litAddr origin
          , vmoptOrigin        = origin
          , vmoptGas           = txGasLimit tx - fromIntegral (txGasCost feeSchedule tx)
+         , vmoptBaseFee       = blockBaseFee block
+         , vmoptPriorityFee   = priorityFee tx (blockBaseFee block)
          , vmoptGaslimit      = txGasLimit tx
          , vmoptNumber        = blockNumber block
          , vmoptTimestamp     = litWord $ w256 $ blockTimestamp block
@@ -279,7 +283,7 @@
          , vmoptDifficulty    = blockDifficulty block
          , vmoptMaxCodeSize   = 24576
          , vmoptBlockGaslimit = blockGasLimit block
-         , vmoptGasprice      = txGasPrice tx
+         , vmoptGasprice      = effectiveGasPrice
          , vmoptSchedule      = feeSchedule
          , vmoptChainId       = 1
          , vmoptCreate        = isCreate
@@ -297,27 +301,53 @@
             theCode = if isCreate
                       then EVM.InitCode (ConcreteBuffer (txData tx))
                       else maybe (EVM.RuntimeCode mempty) (view contractcode) toCode
+            effectiveGasPrice = effectiveprice tx (blockBaseFee block)
             cd = if isCreate
                  then (mempty, 0)
                  else let l = num . BS.length $ txData tx
                       in (ConcreteBuffer $ txData tx, litWord l)
 
+effectiveprice :: Transaction -> W256 -> W256
+effectiveprice tx baseFee = priorityFee tx baseFee + baseFee
 
-validateTx :: Transaction -> Map Addr EVM.Contract -> Maybe ()
-validateTx tx cs = do
+priorityFee :: Transaction -> W256 -> W256
+priorityFee tx baseFee = let
+    (txPrioMax, txMaxFee) = case txType tx of
+               EIP1559Transaction ->
+                 let Just maxPrio = txMaxPriorityFeeGas tx
+                     Just maxFee = txMaxFeePerGas tx
+                 in (maxPrio, maxFee)
+               _ ->
+                 let Just gasPrice = txGasPrice tx
+                 in (gasPrice, gasPrice)
+  in min txPrioMax (txMaxFee - baseFee)
+
+maxBaseFee :: Transaction -> W256
+maxBaseFee tx =
+  case txType tx of
+     EIP1559Transaction ->
+       let Just maxFee = txMaxFeePerGas tx
+       in maxFee
+     _ ->
+       let Just gasPrice = txGasPrice tx
+       in gasPrice
+
+
+validateTx :: Transaction -> Block -> Map Addr EVM.Contract -> Maybe ()
+validateTx tx block cs = do
   origin        <- sender 1 tx
   originBalance <- (view balance) <$> view (at origin) cs
   originNonce   <- (view nonce)   <$> view (at origin) cs
-  let gasDeposit = w256 $ (txGasPrice tx) * (txGasLimit tx)
+  let gasDeposit = w256 $ (effectiveprice tx (blockBaseFee block)) * (txGasLimit tx)
   if gasDeposit + (w256 $ txValue tx) <= originBalance
-    && (w256 $ txNonce tx) == originNonce
+    && (w256 $ txNonce tx) == originNonce && blockBaseFee block <= maxBaseFee tx
   then Just ()
   else Nothing
 
-checkTx :: Transaction -> Map Addr EVM.Contract -> Maybe (Map Addr EVM.Contract)
-checkTx tx prestate = do
+checkTx :: Transaction -> Block -> Map Addr EVM.Contract -> Maybe (Map Addr EVM.Contract)
+checkTx tx block prestate = do
   origin <- sender 1 tx
-  validateTx tx prestate
+  validateTx tx block prestate
   let isCreate   = isNothing (txToAddr tx)
       senderNonce = EVM.wordValue $ view (accountAt origin . nonce) prestate
       toAddr      = fromMaybe (EVM.createAddress origin senderNonce) (txToAddr tx)
diff --git a/test/test.hs b/test/test.hs
--- a/test/test.hs
+++ b/test/test.hs
@@ -22,6 +22,7 @@
 import Test.Tasty
 import Test.Tasty.QuickCheck
 import Test.Tasty.HUnit
+import Test.Tasty.Runners
 
 import Control.Monad.State.Strict (execState, runState)
 import Control.Lens hiding (List, pre, (.>))
@@ -51,7 +52,15 @@
     fail = io . fail
 
 main :: IO ()
-main = defaultMain $ testGroup "hevm"
+main = defaultMain tests
+
+-- | run a subset of tests in the repl. p is a tasty pattern:
+-- https://github.com/UnkindPartition/tasty/tree/ee6fe7136fbcc6312da51d7f1b396e1a2d16b98a#patterns
+runSubSet :: String -> IO ()
+runSubSet p = defaultMain . applyPattern p $ tests
+
+tests :: TestTree
+tests = testGroup "hevm"
   [ testGroup "ABI"
     [ testProperty "Put/get inverse" $ \x ->
         case runGetOrFail (getAbi (abiValueType x)) (runPut (putAbi x)) of
@@ -145,8 +154,8 @@
 
   , testGroup "metadata stripper"
     [ testCase "it strips the metadata for solc => 0.6" $ do
-        let code = hexText "0x608060405234801561001057600080fd5b50600436106100365760003560e01c806317bf8bac1461003b578063acffee6b1461005d575b600080fd5b610043610067565b604051808215151515815260200191505060405180910390f35b610065610073565b005b60008060015414905090565b6000809054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1663f8a8fd6d6040518163ffffffff1660e01b815260040160206040518083038186803b1580156100da57600080fd5b505afa1580156100ee573d6000803e3d6000fd5b505050506040513d602081101561010457600080fd5b810190808051906020019092919050505060018190555056fea265627a7a723158205d775f914dcb471365a430b5f5b2cfe819e615cbbb5b2f1ccc7da1fd802e43c364736f6c634300050b0032"
-            stripped = stripBytecodeMetadata code
+        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
@@ -160,10 +169,10 @@
                 }
                 |]
 
-        (json, path) <- solidity' srccode
-        let Just (solc, _, _) = readJSON json
+        (json, path') <- solidity' srccode
+        let Just (solc', _, _) = readJSON json
             initCode :: ByteString
-            Just initCode = solc ^? ix (path <> ":A") . creationCode
+            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)
     ]
@@ -214,7 +223,7 @@
               in case view result poststate of
                 Just (VMSuccess (SymbolicBuffer out)) -> (fromBytes out) .== x + y
                 _ -> sFalse
-        (Left res, _) <- runSMT $ query $ verifyContract safeAdd (Just ("add(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] SymbolicS pre post
+        (Qed res, _) <- runSMT $ query $ verifyContract safeAdd (Just ("add(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] SymbolicS pre post
         putStrLn $ "successfully explored: " <> show (length res) <> " paths"
      ,
 
@@ -236,31 +245,11 @@
               in case view result poststate of
                       Just (VMSuccess (SymbolicBuffer out)) -> fromBytes out .== 2 * y
                       _ -> sFalse
-        (Left res, _) <- runSMTWith z3 $ query $
+        (Qed res, _) <- runSMTWith z3 $ query $
           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
-        Just factor <- solcRuntime "PrimalityCheck"
-          [i|
-          contract PrimalityCheck {
-            function factor(uint x, uint y) public pure  {
-                   require(1 < x && x < 973013 && 1 < y && y < 973013);
-                   assert(x*y != 973013);
-            }
-          }
-          |]
-        bs <- runSMTWith cvc4 $ query $ do
-          (Right _, vm) <- checkAssert defaultPanicCodes 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 [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
+      testCase "summary storage writes" $ do
         Just c <- solcRuntime "A"
           [i|
           contract A {
@@ -286,9 +275,35 @@
               in case view result poststate of
                 Just (VMSuccess _) -> prex + 2 * y .== postx
                 _ -> sFalse
-        (Left res, _) <- runSMT $ query $ verifyContract c (Just ("f(uint256)", [AbiUIntType 256])) [] SymbolicS pre post
+        (Qed res, _) <- runSMT $ query $ verifyContract c (Just ("f(uint256)", [AbiUIntType 256])) [] SymbolicS pre post
         putStrLn $ "successfully explored: " <> show (length res) <> " paths"
         ,
+        -- tests how whiffValue handles Neg via application of the triple IsZero simplification rule
+        -- regression test for: https://github.com/dapphub/dapptools/pull/698
+        testCase "Neg" $ do
+            let src =
+                  [i|
+                    object "Neg" {
+                      code {
+                        // Deploy the contract
+                        datacopy(0, dataoffset("runtime"), datasize("runtime"))
+                        return(0, datasize("runtime"))
+                      }
+                      object "runtime" {
+                        code {
+                          let v := calldataload(4)
+                          if iszero(iszero(and(v, not(0xffffffffffffffffffffffffffffffffffffffff)))) {
+                            invalid()
+                          }
+                        }
+                      }
+                    }
+                    |]
+            Just c <- yulRuntime "Neg" src
+            (Qed res, _) <- runSMTWith cvc4 $ query $ checkAssert defaultPanicCodes c (Just ("hello(address)", [AbiAddressType])) []
+            putStrLn $ "successfully explored: " <> show (length res) <> " paths"
+        ,
+
         -- Inspired by these `msg.sender == to` token bugs
         -- which break linearity of totalSupply.
         testCase "catch storage collisions" $ do
@@ -318,7 +333,7 @@
                 Just (VMSuccess _) -> prex + prey .== postx + (posty :: SWord 256)
                 _ -> sFalse
         bs <- runSMT $ query $ do
-          (Right _, vm) <- verifyContract c (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] SymbolicS pre (Just post)
+          (Cex _, 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 _ -> error "unexpected"
@@ -345,7 +360,7 @@
               }
              }
             |]
-          (Left res, _) <- runSMTWith z3 $ query $ checkAssert defaultPanicCodes c (Just ("deposit(uint256)", [AbiUIntType 256])) []
+          (Qed res, _) <- runSMTWith z3 $ query $ checkAssert defaultPanicCodes c (Just ("deposit(uint256)", [AbiUIntType 256])) []
           putStrLn $ "successfully explored: " <> show (length res) <> " paths"
         ,
                 testCase "Deposit contract loop (cvc4)" $ do
@@ -367,7 +382,7 @@
               }
              }
             |]
-          (Left res, _) <- runSMTWith cvc4 $ query $ checkAssert defaultPanicCodes c (Just ("deposit(uint256)", [AbiUIntType 256])) []
+          (Qed res, _) <- runSMTWith cvc4 $ query $ checkAssert defaultPanicCodes c (Just ("deposit(uint256)", [AbiUIntType 256])) []
           putStrLn $ "successfully explored: " <> show (length res) <> " paths"
         ,
         testCase "Deposit contract loop (error version)" $ do
@@ -390,7 +405,7 @@
              }
             |]
           bs <- runSMT $ query $ do
-            (Right _, vm) <- checkAssert allPanicCodes c (Just ("deposit(uint8)", [AbiUIntType 8])) []
+            (Cex _, vm) <- checkAssert allPanicCodes c (Just ("deposit(uint8)", [AbiUIntType 8])) []
             case view (state . calldata . _1) vm of
               SymbolicBuffer bs -> BS.pack <$> mapM (getValue.fromSized) bs
               ConcreteBuffer _ -> error "unexpected"
@@ -407,7 +422,7 @@
             }
           }
           |]
-        (Left res, _) <- runSMTWith z3 $ do
+        (Qed res, _) <- runSMTWith z3 $ do
           setTimeOut 5000
           query $ checkAssert defaultPanicCodes c Nothing []
         putStrLn $ "successfully explored: " <> show (length res) <> " paths"
@@ -422,7 +437,7 @@
               }
             }
             |]
-          (Left res, _) <- runSMTWith cvc4 $ query $ checkAssert defaultPanicCodes c (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) []
+          (Qed res, _) <- runSMTWith cvc4 $ query $ checkAssert defaultPanicCodes c (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) []
           putStrLn $ "successfully explored: " <> show (length res) <> " paths"
         ,
         testCase "injectivity of keccak (32 bytes)" $ do
@@ -434,7 +449,7 @@
               }
             }
             |]
-          (Left res, _) <- runSMTWith z3 $ query $ checkAssert defaultPanicCodes c (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) []
+          (Qed res, _) <- runSMTWith z3 $ query $ checkAssert defaultPanicCodes c (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) []
           putStrLn $ "successfully explored: " <> show (length res) <> " paths"
        ,
 
@@ -448,7 +463,7 @@
             }
             |]
           bs <- runSMTWith z3 $ query $ do
-            (Right _, vm) <- checkAssert defaultPanicCodes c (Just ("f(uint256,uint256,uint256,uint256)", replicate 4 (AbiUIntType 256))) []
+            (Cex _, vm) <- checkAssert defaultPanicCodes 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"
@@ -478,7 +493,7 @@
               }
             }
             |]
-          Left res <- runSMTWith z3 $ do
+          Qed res <- runSMTWith z3 $ do
             setTimeOut 5000
             query $ fst <$> checkAssert defaultPanicCodes c Nothing []
           putStrLn $ "successfully explored: " <> show (length res) <> " paths"
@@ -497,13 +512,13 @@
               }
             |]
           -- should find a counterexample
-          Right _ <- runSMTWith cvc4 $ query $ fst <$> checkAssert defaultPanicCodes c (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) []
+          Cex _ <- runSMTWith cvc4 $ query $ fst <$> checkAssert defaultPanicCodes c (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) []
           putStrLn "found counterexample:"
 
 
       ,
          testCase "multiple contracts" $ do
-          let code =
+          let code' =
                 [i|
                   contract C {
                     uint x;
@@ -519,9 +534,9 @@
                   }
                 |]
               aAddr = Addr 0x35D1b3F3D7966A1DFe207aa4514C12a259A0492B
-          Just c <- solcRuntime "C" code
-          Just a <- solcRuntime "A" code
-          Right _ <- runSMT $ query $ do
+          Just c <- solcRuntime "C" code'
+          Just a <- solcRuntime "A" code'
+          Cex _ <- runSMT $ query $ do
             vm0 <- abstractVM (Just ("call_A()", [])) [] c SymbolicS
             store <- freshArray (show aAddr) Nothing
             let vm = vm0
@@ -529,11 +544,11 @@
                   & over (env . contracts)
                        (Map.insert aAddr (initialContract (RuntimeCode $ ConcreteBuffer a) &
                                            set EVM.storage (EVM.Symbolic [] store)))
-            verify vm Nothing Nothing (Just $ checkAssertions defaultPanicCodes)
+            verify vm Nothing Nothing Nothing (Just $ checkAssertions defaultPanicCodes)
           putStrLn "found counterexample:"
       ,
          testCase "calling unique contracts (read from storage)" $ do
-          let code =
+          let code' =
                 [i|
                   contract C {
                     uint x;
@@ -549,16 +564,16 @@
                     uint public x;
                   }
                 |]
-          Just c <- solcRuntime "C" code
-          Right _ <- runSMT $ query $ do
+          Just c <- solcRuntime "C" code'
+          Cex _ <- runSMT $ query $ do
             vm0 <- abstractVM (Just ("call_A()", [])) [] c SymbolicS
             let vm = vm0 & set (state . callvalue) 0
-            verify vm Nothing Nothing (Just $ checkAssertions defaultPanicCodes)
+            verify vm Nothing Nothing Nothing (Just $ checkAssertions defaultPanicCodes)
           putStrLn "found counterexample:"
       ,
 
          testCase "keccak concrete and sym agree" $ do
-          let code =
+          let code' =
                 [i|
                   contract C {
                     function kecc(uint x) public pure {
@@ -568,22 +583,22 @@
                     }
                   }
                 |]
-          Just c <- solcRuntime "C" code
-          Left _ <- runSMT $ query $ do
+          Just c <- solcRuntime "C" code'
+          Qed _ <- runSMT $ query $ do
             vm0 <- abstractVM (Just ("kecc(uint256)", [AbiUIntType 256])) [] c SymbolicS
             let vm = vm0 & set (state . callvalue) 0
-            verify vm Nothing Nothing (Just $ checkAssertions defaultPanicCodes)
+            verify vm Nothing Nothing Nothing (Just $ checkAssertions defaultPanicCodes)
           putStrLn "found counterexample:"
 
       , testCase "safemath distributivity (yul)" $ do
-          Left _ <- runSMTWith cvc4 $ query $ do
+          Qed _ <- runSMTWith cvc4 $ query $ do
             let yulsafeDistributivity = hex "6355a79a6260003560e01c14156016576015601f565b5b60006000fd60a1565b603d602d604435600435607c565b6039602435600435607c565b605d565b6052604b604435602435605d565b600435607c565b141515605a57fe5b5b565b6000828201821115151560705760006000fd5b82820190505b92915050565b6000818384048302146000841417151560955760006000fd5b82820290505b92915050565b"
             vm <- abstractVM (Just ("distributivity(uint256,uint256,uint256)", [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) [] yulsafeDistributivity SymbolicS
-            verify vm Nothing Nothing (Just $ checkAssertions defaultPanicCodes)
+            verify vm Nothing Nothing Nothing (Just $ checkAssertions defaultPanicCodes)
           putStrLn "Proven"
 
       , testCase "safemath distributivity (sol)" $ do
-          let code =
+          let code' =
                 [i|
                   contract C {
                       function distributivity(uint x, uint y, uint z) public {
@@ -602,11 +617,11 @@
                       }
                  }
                 |]
-          Just c <- solcRuntime "C" code
+          Just c <- solcRuntime "C" code'
 
-          Left _ <- runSMTWith z3 $ query $ do
+          Qed _ <- runSMTWith cvc4 $ query $ do
             vm <- abstractVM (Just ("distributivity(uint256,uint256,uint256)", [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) [] c SymbolicS
-            verify vm Nothing Nothing (Just $ checkAssertions defaultPanicCodes)
+            verify vm Nothing Nothing Nothing (Just $ checkAssertions defaultPanicCodes)
           putStrLn "Proven"
 
     ]
@@ -614,20 +629,29 @@
     [
       testCase "yul optimized" $ do
         -- These yul programs are not equivalent: (try --calldata $(seth --to-uint256 2) for example)
-        --  A:                               B:
-        --  {                                {
-        --     calldatacopy(0, 0, 32)           calldatacopy(0, 0, 32)
-        --     switch mload(0)                  switch mload(0)
-        --     case 0 { }                       case 0 { }
-        --     case 1 { }                       case 2 { }
-        --     default { invalid() }            default { invalid() }
-        -- }                                 }
-        let aPrgm = hex "602060006000376000805160008114601d5760018114602457fe6029565b8191506029565b600191505b50600160015250"
-            bPrgm = hex "6020600060003760005160008114601c5760028114602057fe6021565b6021565b5b506001600152"
+        Just aPrgm <- yul ""
+          [i|
+          {
+              calldatacopy(0, 0, 32)
+              switch mload(0)
+              case 0 { }
+              case 1 { }
+              default { invalid() }
+          }
+          |]
+        Just bPrgm <- yul ""
+          [i|
+          {
+              calldatacopy(0, 0, 32)
+              switch mload(0)
+              case 0 { }
+              case 2 { }
+              default { invalid() }
+          }
+          |]
         runSMTWith z3 $ query $ do
-          Right _ <- equivalenceCheck aPrgm bPrgm Nothing Nothing
+          Cex _ <- equivalenceCheck aPrgm bPrgm Nothing Nothing Nothing
           return ()
-
     ]
   ]
   where
@@ -759,3 +783,5 @@
   b' <- f a'
   return (b, b')
 
+applyPattern :: String -> TestTree  -> TestTree
+applyPattern p = localOption (TestPattern (parseExpr p))