diff --git a/CHANGELOG.md b/CHANGELOG.md
index 876d6bc88..e3f65a892 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -12,6 +12,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## Added
 - Optimized smt queries that significantly improve performance when dealing with solidity mappings and arrays
+- Support for using Bitwuzla as a solver
 - Symbolic tests now support statically sized arrays as parameters
 - `hevm test` now has a `num-solvers` parameter that controls how many solver instances to spawn
 - New solc-specific simplification rules that should make the final Props a lot more readable
diff --git a/cli/cli.hs b/cli/cli.hs
index 3bc74bdd9..b943d821c 100644
--- a/cli/cli.hs
+++ b/cli/cli.hs
@@ -41,7 +41,8 @@ import EVM.Solvers
 import EVM.Stepper qualified
 import EVM.SymExec
 import EVM.Transaction qualified
-import EVM.Types hiding (word, Env)
+import EVM.Types hiding (word, Env, Symbolic)
+import EVM.Types qualified
 import EVM.UnitTest
 import EVM.Effects
 
@@ -84,7 +85,7 @@ data Command w
       , showReachableTree :: w ::: Bool           <?> "Print only reachable branches explored in tree view"
       , smttimeout    :: w ::: Maybe Natural      <?> "Timeout given to SMT solver in seconds (default: 300)"
       , maxIterations :: w ::: Maybe Integer      <?> "Number of times we may revisit a particular branching point"
-      , solver        :: w ::: Maybe Text         <?> "Used SMT solver: z3 (default) or cvc5"
+      , solver        :: w ::: Maybe Text         <?> "Used SMT solver: z3 (default), cvc5, or bitwuzla"
       , smtdebug      :: w ::: Bool               <?> "Print smt queries sent to the solver"
       , debug         :: w ::: Bool               <?> "Debug printing of internal behaviour"
       , trace         :: w ::: Bool               <?> "Dump trace"
@@ -104,7 +105,7 @@ data Command w
       , calldata      :: w ::: Maybe ByteString <?> "Tx: calldata"
       , smttimeout    :: w ::: Maybe Natural    <?> "Timeout given to SMT solver in seconds (default: 300)"
       , maxIterations :: w ::: Maybe Integer    <?> "Number of times we may revisit a particular branching point"
-      , solver        :: w ::: Maybe Text       <?> "Used SMT solver: z3 (default) or cvc5"
+      , solver        :: w ::: Maybe Text       <?> "Used SMT solver: z3 (default), cvc5, or bitwuzla"
       , smtoutput     :: w ::: Bool             <?> "Print verbose smt output"
       , smtdebug      :: w ::: Bool             <?> "Print smt queries sent to the solver"
       , debug         :: w ::: Bool             <?> "Debug printing of internal behaviour"
@@ -150,7 +151,7 @@ data Command w
       , verbose       :: w ::: Maybe Int                <?> "Append call trace: {1} failures {2} all"
       , coverage      :: w ::: Bool                     <?> "Coverage analysis"
       , match         :: w ::: Maybe String             <?> "Test case filter - only run methods matching regex"
-      , solver        :: w ::: Maybe Text               <?> "Used SMT solver: z3 (default) or cvc5"
+      , solver        :: w ::: Maybe Text               <?> "Used SMT solver: z3 (default), cvc5, or bitwuzla"
       , numSolvers    :: w ::: Maybe Natural            <?> "Number of solver instances to use (default: number of cpu cores)"
       , smtdebug      :: w ::: Bool                     <?> "Print smt queries sent to the solver"
       , debug         :: w ::: Bool                     <?> "Debug printing of internal behaviour"
@@ -265,6 +266,7 @@ getSolver cmd = case cmd.solver of
                   Just s -> case T.unpack s of
                               "z3" -> pure Z3
                               "cvc5" -> pure CVC5
+                              "bitwuzla" -> pure Bitwuzla
                               input -> do
                                 putStrLn $ "unrecognised solver: " <> input
                                 exitFailure
@@ -407,7 +409,7 @@ launchExec cmd = do
         internalError "no EVM result"
 
 -- | Creates a (concrete) VM from command line options
-vmFromCommand :: Command Options.Unwrapped -> IO (VM RealWorld)
+vmFromCommand :: Command Options.Unwrapped -> IO (VM Concrete RealWorld)
 vmFromCommand cmd = do
   (miner,ts,baseFee,blockNum,prevRan) <- case cmd.rpc of
     Nothing -> pure (LitAddr 0,Lit 0,0,0,0)
@@ -492,14 +494,13 @@ vmFromCommand cmd = do
           , baseState      = EmptyBase
           , txAccessList   = mempty -- TODO: support me soon
           , allowFFI       = False
-          , symbolic       = False
           }
         word f def = fromMaybe def (f cmd)
         word64 f def = fromMaybe def (f cmd)
         addr f def = maybe def LitAddr (f cmd)
         bytes f def = maybe def decipher (f cmd)
 
-symvmFromCommand :: Command Options.Unwrapped -> (Expr Buf, [Prop]) -> IO (VM RealWorld)
+symvmFromCommand :: Command Options.Unwrapped -> (Expr Buf, [Prop]) -> IO (VM EVM.Types.Symbolic RealWorld)
 symvmFromCommand cmd calldata = do
   (miner,blockNum,baseFee,prevRan) <- case cmd.rpc of
     Nothing -> pure (SymAddr "miner",0,0,0)
@@ -557,7 +558,7 @@ symvmFromCommand cmd calldata = do
       , address        = address
       , caller         = caller
       , origin         = origin
-      , gas            = word64 (.gas) 0xffffffffffffffff
+      , gas            = ()
       , gaslimit       = word64 (.gaslimit) 0xffffffffffffffff
       , baseFee        = baseFee
       , priorityFee    = word (.priorityFee) 0
@@ -574,7 +575,6 @@ symvmFromCommand cmd calldata = do
       , baseState      = maybe AbstractBase parseInitialStorage (cmd.initialStorage)
       , txAccessList   = mempty
       , allowFFI       = False
-      , symbolic       = True
       }
     word f def = fromMaybe def (f cmd)
     word64 f def = fromMaybe def (f cmd)
diff --git a/doc/src/equivalence.md b/doc/src/equivalence.md
index 9f78ee44e..1a5fd5553 100644
--- a/doc/src/equivalence.md
+++ b/doc/src/equivalence.md
@@ -18,7 +18,7 @@ Available options:
   --smttimeout NATURAL     Timeout given to SMT solver in seconds (default: 300)
   --max-iterations INTEGER Number of times we may revisit a particular branching
                            point
-  --solver TEXT            Used SMT solver: z3 (default) or cvc5
+  --solver TEXT            Used SMT solver: z3 (default), cvc5, or bitwuzla
   --smtoutput              Print verbose smt output
   --smtdebug               Print smt queries sent to the solver
   --ask-smt-iterations INTEGER
diff --git a/doc/src/symbolic.md b/doc/src/symbolic.md
index ec9b49316..4fd691aa6 100644
--- a/doc/src/symbolic.md
+++ b/doc/src/symbolic.md
@@ -55,7 +55,7 @@ Available options:
   --smttimeout NATURAL     Timeout given to SMT solver in seconds (default: 300)
   --max-iterations INTEGER Number of times we may revisit a particular branching
                            point
-  --solver TEXT            Used SMT solver: z3 (default) or cvc5
+  --solver TEXT            Used SMT solver: z3 (default), cvc5, or bitwuzla
   --smtdebug               Print smt queries sent to the solver
   --assertions [WORD256]   Comma separated list of solc panic codes to check for
                            (default: user defined assertion violations only)
diff --git a/doc/src/test.md b/doc/src/test.md
index b9936db6d..b545e5603 100644
--- a/doc/src/test.md
+++ b/doc/src/test.md
@@ -1,4 +1,4 @@
-# `hevm dapp-test`
+# `hevm test`
 
 ```
 Usage: hevm test [--root STRING] [--project-type PROJECTTYPE] [--rpc TEXT]
@@ -18,7 +18,8 @@ Available options:
   --verbose INT            Append call trace: {1} failures {2} all
   --coverage               Coverage analysis
   --match STRING           Test case filter - only run methods matching regex
-  --solver TEXT            Used SMT solver: z3 (default) or cvc5
+  --solver TEXT            Used SMT solver: z3 (default), cvc5, or bitwuzla
+
   --num-solvers NATURAL    Number of solver instances to use (default: number of cpu cores)
   --smtdebug               Print smt queries sent to the solver
   --ffi                    Allow the usage of the hevm.ffi() cheatcode (WARNING:
diff --git a/flake.lock b/flake.lock
index ca6a58032..e44af729d 100644
--- a/flake.lock
+++ b/flake.lock
@@ -1,5 +1,21 @@
 {
   "nodes": {
+    "bitwuzla-pkgs": {
+      "locked": {
+        "lastModified": 1705259768,
+        "narHash": "sha256-eHetoB0ckEQ06QDa7EZqeC+qFJEC606K90q/PliNTA4=",
+        "owner": "d-xo",
+        "repo": "nixpkgs",
+        "rev": "6e7c9e4267f3c2df116bf76d8e31c2602e2d543d",
+        "type": "github"
+      },
+      "original": {
+        "owner": "d-xo",
+        "repo": "nixpkgs",
+        "rev": "6e7c9e4267f3c2df116bf76d8e31c2602e2d543d",
+        "type": "github"
+      }
+    },
     "cabal-head": {
       "flake": false,
       "locked": {
@@ -150,6 +166,7 @@
     },
     "root": {
       "inputs": {
+        "bitwuzla-pkgs": "bitwuzla-pkgs",
         "cabal-head": "cabal-head",
         "ethereum-tests": "ethereum-tests",
         "flake-compat": "flake-compat",
diff --git a/flake.nix b/flake.nix
index 76f37d3e2..1df0480d6 100644
--- a/flake.nix
+++ b/flake.nix
@@ -5,6 +5,7 @@
     flake-utils.url = "github:numtide/flake-utils";
     nixpkgs.url = "github:nixos/nixpkgs/nixpkgs-unstable";
     foundry.url = "github:shazow/foundry.nix/monthly";
+    bitwuzla-pkgs.url = "github:d-xo/nixpkgs/6e7c9e4267f3c2df116bf76d8e31c2602e2d543d";
     flake-compat = {
       url = "github:edolstra/flake-compat";
       flake = false;
@@ -27,16 +28,18 @@
     };
   };
 
-  outputs = { self, nixpkgs, flake-utils, solidity, forge-std, ethereum-tests, foundry, cabal-head, ... }:
+  outputs = { self, nixpkgs, flake-utils, solidity, forge-std, ethereum-tests, foundry, cabal-head, bitwuzla-pkgs, ... }:
     flake-utils.lib.eachDefaultSystem (system:
       let
         pkgs = (import nixpkgs { inherit system; config = { allowBroken = true; }; });
+        bitwuzla = (import bitwuzla-pkgs { inherit system; }).bitwuzla;
         testDeps = with pkgs; [
           go-ethereum
           solc
           z3
           cvc5
           git
+          bitwuzla
         ] ++ lib.optional (!(pkgs.stdenv.isDarwin && pkgs.stdenv.isAarch64)) [
           foundry.defaultPackage.${system}
         ];
@@ -126,7 +129,7 @@
           buildInputs = [ makeWrapper ];
           postBuild = ''
             wrapProgram $out/bin/hevm \
-              --prefix PATH : "${lib.makeBinPath ([ bash coreutils git solc z3 cvc5 ])}"
+              --prefix PATH : "${lib.makeBinPath ([ bash coreutils git solc z3 cvc5 bitwuzla ])}"
           '';
         };
 
diff --git a/hevm.cabal b/hevm.cabal
index 4683e5f2f..b07cf56e7 100644
--- a/hevm.cabal
+++ b/hevm.cabal
@@ -59,6 +59,8 @@ common shared
     -Wno-orphans
     -Wno-ambiguous-fields
     -optc-Wno-ignored-attributes
+    -fspecialize-aggressively
+    -fexpose-all-unfoldings
   default-language: GHC2021
   default-extensions:
     DuplicateRecordFields
diff --git a/src/EVM.hs b/src/EVM.hs
index 2cd7895ef..879b4f5f6 100644
--- a/src/EVM.hs
+++ b/src/EVM.hs
@@ -20,6 +20,7 @@ import EVM.Op
 import EVM.Precompiled qualified
 import EVM.Solidity
 import EVM.Types
+import EVM.Types qualified as Expr (Expr(Gas))
 import EVM.Sign qualified
 import EVM.Concrete qualified as Concrete
 
@@ -57,7 +58,7 @@ import Crypto.Hash (Digest, SHA256, RIPEMD160)
 import Crypto.Hash qualified as Crypto
 import Crypto.Number.ModArithmetic (expFast)
 
-blankState :: ST s (FrameState s)
+blankState :: VMOps t => ST s (FrameState t s)
 blankState = do
   memory <- ConcreteMemory <$> VUnboxed.Mutable.new 0
   pure $ FrameState
@@ -71,7 +72,7 @@ blankState = do
     , calldata     = mempty
     , callvalue    = Lit 0
     , caller       = LitAddr 0
-    , gas          = 0
+    , gas          = initialGas
     , returndata   = mempty
     , static       = False
     }
@@ -87,13 +88,13 @@ bytecode = #code % to f
 
 -- * Data accessors
 
-currentContract :: VM s -> Maybe Contract
+currentContract :: VM t s -> Maybe Contract
 currentContract vm =
   Map.lookup vm.state.codeContract vm.env.contracts
 
 -- * Data constructors
 
-makeVm :: VMOpts -> ST s (VM s)
+makeVm :: VMOps t => VMOpts t -> ST s (VM t s)
 makeVm o = do
   let txaccessList = o.txAccessList
       txorigin = o.origin
@@ -150,9 +151,10 @@ makeVm o = do
       { chainId = o.chainId
       , contracts = Map.fromList ((o.address,o.contract):o.otherContracts)
       , freshAddresses = 0
+      , freshGasVals = 0
       }
     , cache = Cache mempty mempty
-    , burned = 0
+    , burned = initialGas
     , constraints = snd o.calldata
     , iterations = mempty
     , config = RuntimeConfig
@@ -160,7 +162,6 @@ makeVm o = do
       , overrideCaller = Nothing
       , baseState = o.baseState
       }
-    , symbolic = o.symbolic
     }
 
 -- | Initialize an abstract contract with unknown code
@@ -218,11 +219,11 @@ isCreation = \case
 -- * Opcode dispatch (exec1)
 
 -- | Update program counter
-next :: (?op :: Word8) => EVM s ()
+next :: (?op :: Word8) => EVM t s ()
 next = modifying (#state % #pc) (+ (opSize ?op))
 
 -- | Executes the EVM one step
-exec1 :: EVM s ()
+exec1 :: forall (t :: VMType) s. VMOps t => EVM t s ()
 exec1 = do
   vm <- get
 
@@ -241,28 +242,25 @@ exec1 = do
   if isJust litSelf && (fromJust litSelf) > 0x0 && (fromJust litSelf) <= 0x9 then do
     -- call to precompile
     let ?op = 0x00 -- dummy value
-    case bufLength vm.state.calldata of
-      Lit calldatasize -> do
-          copyBytesToMemory vm.state.calldata (Lit calldatasize) (Lit 0) (Lit 0)
-          executePrecompile (fromJust litSelf) vm.state.gas 0 calldatasize 0 0 []
-          vmx <- get
-          case vmx.state.stack of
-            x:_ -> case x of
-              Lit 0 ->
-                fetchAccount self $ \_ -> do
-                  touchAccount self
-                  vmError PrecompileFailure
-              Lit _ ->
-                fetchAccount self $ \_ -> do
-                  touchAccount self
-                  out <- use (#state % #returndata)
-                  finishFrame (FrameReturned out)
-              e -> partial $
-                     UnexpectedSymbolicArg vmx.state.pc "precompile returned a symbolic value" (wrap [e])
-            _ ->
-              underrun
-      e -> partial $
-             UnexpectedSymbolicArg vm.state.pc "cannot call precompiles with symbolic data" (wrap [e])
+    let calldatasize = bufLength vm.state.calldata
+    copyBytesToMemory vm.state.calldata calldatasize (Lit 0) (Lit 0)
+    executePrecompile (fromJust litSelf) vm.state.gas (Lit 0) calldatasize (Lit 0) (Lit 0) []
+    vmx <- get
+    case vmx.state.stack of
+      x:_ -> case x of
+        Lit 0 ->
+          fetchAccount self $ \_ -> do
+            touchAccount self
+            vmError PrecompileFailure
+        Lit _ ->
+          fetchAccount self $ \_ -> do
+            touchAccount self
+            out <- use (#state % #returndata)
+            finishFrame (FrameReturned out)
+        e -> partial $
+               UnexpectedSymbolicArg vmx.state.pc "precompile returned a symbolic value" (wrap [e])
+      _ ->
+        underrun
 
   else if vm.state.pc >= opslen vm.state.code
     then doStop
@@ -320,23 +318,19 @@ exec1 = do
         OpLog n ->
           notStatic $
           case stk of
-            (xOffset':xSize':xs) ->
+            (xOffset:xSize:xs) ->
               if length xs < (into n)
               then underrun
-              else
-                forceConcrete2 (xOffset', xSize') "LOG" $ \(xOffset, xSize) -> do
-                    bytes <- readMemory xOffset' xSize'
-                    let (topics, xs') = splitAt (into n) xs
-                        logs'         = (LogEntry (WAddr self) bytes topics) : vm.logs
-                    case (tryFrom xSize) of
-                      (Right sz) ->
-                        burn (g_log + g_logdata * sz + (into n) * g_logtopic) $
-                          accessMemoryRange xOffset xSize $ do
-                            traceTopLog logs'
-                            next
-                            assign (#state % #stack) xs'
-                            assign #logs logs'
-                      _ -> vmError IllegalOverflow
+              else do
+                bytes <- readMemory xOffset xSize
+                let (topics, xs') = splitAt (into n) xs
+                    logs'         = (LogEntry (WAddr self) bytes topics) : vm.logs
+                burnLog xSize n $
+                  accessMemoryRange xOffset xSize $ do
+                    traceTopLog logs'
+                    next
+                    assign (#state % #stack) xs'
+                    assign #logs logs'
             _ ->
               underrun
 
@@ -378,18 +372,17 @@ exec1 = do
         -- more accurately refered to as KECCAK
         OpSha3 ->
           case stk of
-            xOffset':xSize':xs ->
-              forceConcrete xOffset' "sha3 offset must be concrete" $
-                \xOffset -> forceConcrete xSize' "sha3 size must be concrete" $ \xSize ->
-                  burn (g_sha3 + g_sha3word * ceilDiv (unsafeInto xSize) 32) $
-                    accessMemoryRange xOffset xSize $ do
-                      hash <- readMemory xOffset' xSize' >>= \case
-                        orig@(ConcreteBuf bs) ->
-                          if vm.symbolic then pure $ Keccak orig
-                                         else pure $ Lit (keccak' bs)
-                        buf -> pure $ Keccak buf
-                      next
-                      assign (#state % #stack) (hash : xs)
+            xOffset:xSize:xs ->
+              burnSha3 xSize $
+                accessMemoryRange xOffset xSize $ do
+                  hash <- readMemory xOffset xSize >>= \case
+                    orig@(ConcreteBuf bs) ->
+                      whenSymbolicElse
+                        (pure $ Keccak orig)
+                        (pure $ Lit (keccak' bs))
+                    buf -> pure $ Keccak buf
+                  next
+                  assign (#state % #stack) (hash : xs)
             _ -> underrun
 
         OpAddress ->
@@ -428,14 +421,12 @@ exec1 = do
 
         OpCalldatacopy ->
           case stk of
-            xTo':xFrom:xSize':xs ->
-              forceConcrete2 (xTo', xSize') "CALLDATACOPY" $
-                \(xTo, xSize) ->
-                  burn (g_verylow + g_copy * ceilDiv (unsafeInto xSize) 32) $
-                    accessMemoryRange xTo xSize $ do
-                      next
-                      assign (#state % #stack) xs
-                      copyBytesToMemory vm.state.calldata xSize' xFrom xTo'
+            xTo:xFrom:xSize:xs ->
+              burnCalldatacopy xSize $
+                accessMemoryRange xTo xSize $ do
+                  next
+                  assign (#state % #stack) xs
+                  copyBytesToMemory vm.state.calldata xSize xFrom xTo
             _ -> underrun
 
         OpCodesize ->
@@ -444,21 +435,14 @@ exec1 = do
 
         OpCodecopy ->
           case stk of
-            memOffset':codeOffset:n':xs ->
-              forceConcrete2 (memOffset', n') "CODECOPY" $
-                \(memOffset,n) -> do
-                  case toWord64 n of
-                    Nothing -> vmError IllegalOverflow
-                    Just n'' ->
-                      if n'' <= ( (maxBound :: Word64) - g_verylow ) `div` g_copy * 32 then
-                        burn (g_verylow + g_copy * ceilDiv (unsafeInto n) 32) $
-                          accessMemoryRange memOffset n $ do
-                            next
-                            assign (#state % #stack) xs
-                            case toBuf vm.state.code of
-                              Just b -> copyBytesToMemory b n' codeOffset memOffset'
-                              Nothing -> internalError "Cannot produce a buffer from UnknownCode"
-                      else vmError IllegalOverflow
+            memOffset:codeOffset:n:xs ->
+              burnCodecopy n $ do
+                accessMemoryRange memOffset n $ do
+                  next
+                  assign (#state % #stack) xs
+                  case toBuf vm.state.code of
+                    Just b -> copyBytesToMemory b n codeOffset memOffset
+                    Nothing -> internalError "Cannot produce a buffer from UnknownCode"
             _ -> underrun
 
         OpGasprice ->
@@ -488,21 +472,18 @@ exec1 = do
 
         OpExtcodecopy ->
           case stk of
-            extAccount':memOffset':codeOffset:codeSize':xs ->
-              forceConcrete2 (memOffset', codeSize') "EXTCODECOPY" $ \(memOffset, codeSize) -> do
-                forceAddr extAccount' "EXTCODECOPY" $ \extAccount -> do
-                  acc <- accessAccountForGas extAccount
-                  let cost = if acc then g_warm_storage_read else g_cold_account_access
-                  burn (cost + g_copy * ceilDiv (unsafeInto codeSize) 32) $
-                    accessMemoryRange memOffset codeSize $
-                      fetchAccount extAccount $ \c -> do
-                        next
-                        assign (#state % #stack) xs
-                        case view bytecode c of
-                          Just b -> copyBytesToMemory b codeSize' codeOffset memOffset'
-                          Nothing -> do
-                            pc <- use (#state % #pc)
-                            partial $ UnexpectedSymbolicArg pc "Cannot copy from unknown code at" (wrap [extAccount])
+            extAccount':memOffset:codeOffset:codeSize:xs ->
+              forceAddr extAccount' "EXTCODECOPY" $ \extAccount -> do
+                burnExtcodecopy extAccount codeSize $
+                  accessMemoryRange memOffset codeSize $
+                    fetchAccount extAccount $ \c -> do
+                      next
+                      assign (#state % #stack) xs
+                      case view bytecode c of
+                        Just b -> copyBytesToMemory b codeSize codeOffset memOffset
+                        Nothing -> do
+                          pc <- use (#state % #pc)
+                          partial $ UnexpectedSymbolicArg pc "Cannot copy from unknown code at" (wrap [extAccount])
             _ -> underrun
 
         OpReturndatasize ->
@@ -511,23 +492,22 @@ exec1 = do
 
         OpReturndatacopy ->
           case stk of
-            xTo':xFrom:xSize':xs -> forceConcrete2 (xTo', xSize') "RETURNDATACOPY" $
-              \(xTo, xSize) ->
-                burn (g_verylow + g_copy * ceilDiv (unsafeInto xSize) 32) $
-                  accessMemoryRange xTo xSize $ do
-                    next
-                    assign (#state % #stack) xs
+            xTo:xFrom:xSize:xs ->
+              burnReturndatacopy xSize $
+                accessMemoryRange xTo xSize $ do
+                  next
+                  assign (#state % #stack) xs
 
-                    let jump True = vmError ReturnDataOutOfBounds
-                        jump False = copyBytesToMemory vm.state.returndata xSize' xFrom xTo'
+                  let jump True = vmError ReturnDataOutOfBounds
+                      jump False = copyBytesToMemory vm.state.returndata xSize xFrom xTo
 
-                    case (xFrom, bufLength vm.state.returndata) of
-                      (Lit f, Lit l) ->
-                        jump $ l < f + xSize || f + xSize < f
-                      _ -> do
-                        let oob = Expr.lt (bufLength vm.state.returndata) (Expr.add xFrom xSize')
-                            overflow = Expr.lt (Expr.add xFrom xSize') (xFrom)
-                        branch (Expr.or oob overflow) jump
+                  case (xFrom, bufLength vm.state.returndata, xSize) of
+                    (Lit f, Lit l, Lit sz) ->
+                      jump $ l < f + sz || f + sz < f
+                    _ -> do
+                      let oob = Expr.lt (bufLength vm.state.returndata) (Expr.add xFrom xSize)
+                          overflow = Expr.lt (Expr.add xFrom xSize) (xFrom)
+                      branch (Expr.or oob overflow) jump
             _ -> underrun
 
         OpExtcodehash ->
@@ -593,18 +573,18 @@ exec1 = do
 
         OpMload ->
           case stk of
-            x':xs -> forceConcrete x' "MLOAD" $ \x ->
+            x:xs ->
               burn g_verylow $
                 accessMemoryWord x $ do
                   next
-                  buf <- readMemory (Lit x) (Lit 32)
+                  buf <- readMemory x (Lit 32)
                   let w = Expr.readWordFromBytes (Lit 0) buf
                   assign (#state % #stack) (w : xs)
             _ -> underrun
 
         OpMstore ->
           case stk of
-            x':y:xs -> forceConcrete x' "MSTORE index" $ \x ->
+            x:y:xs ->
               burn g_verylow $
                 accessMemoryWord x $ do
                   next
@@ -612,34 +592,34 @@ exec1 = do
                     ConcreteMemory mem -> do
                       case y of
                         Lit w ->
-                          writeMemory mem (unsafeInto x) (word256Bytes w)
+                          copyBytesToMemory (ConcreteBuf (word256Bytes w)) (Lit 32) (Lit 0) x
                         _ -> do
                           -- copy out and move to symbolic memory
                           buf <- freezeMemory mem
-                          assign (#state % #memory) (SymbolicMemory $ writeWord (Lit x) y buf)
+                          assign (#state % #memory) (SymbolicMemory $ writeWord x y buf)
                     SymbolicMemory mem ->
-                      assign (#state % #memory) (SymbolicMemory $ writeWord (Lit x) y mem)
+                      assign (#state % #memory) (SymbolicMemory $ writeWord x y mem)
                   assign (#state % #stack) xs
             _ -> underrun
 
         OpMstore8 ->
           case stk of
-            x':y:xs -> forceConcrete x' "MSTORE8" $ \x ->
+            x:y:xs ->
               burn g_verylow $
-                accessMemoryRange x 1 $ do
+                accessMemoryRange x (Lit 1) $ do
                   let yByte = indexWord (Lit 31) y
                   next
                   gets (.state.memory) >>= \case
                     ConcreteMemory mem -> do
                       case yByte of
                         LitByte byte ->
-                          writeMemory mem (unsafeInto x) (BS.pack [byte])
+                          copyBytesToMemory (ConcreteBuf (BS.pack [byte])) (Lit 1) (Lit 0) x
                         _ -> do
                           -- copy out and move to symbolic memory
                           buf <- freezeMemory mem
-                          assign (#state % #memory) (SymbolicMemory $ writeByte (Lit x) yByte buf)
+                          assign (#state % #memory) (SymbolicMemory $ writeByte x yByte buf)
                     SymbolicMemory mem ->
-                      assign (#state % #memory) (SymbolicMemory $ writeByte (Lit x) yByte mem)
+                      assign (#state % #memory) (SymbolicMemory $ writeByte x yByte mem)
 
                   assign (#state % #stack) xs
             _ -> underrun
@@ -660,11 +640,7 @@ exec1 = do
           case stk of
             x:new:xs ->
               accessStorage self x $ \current -> do
-                availableGas <- use (#state % #gas)
-
-                if availableGas <= g_callstipend then
-                  finishFrame (FrameErrored (OutOfGas availableGas g_callstipend))
-                else do
+                ensureGas g_callstipend $ do
                   let
                     original =
                       case Expr.concKeccakSimpExpr $ SLoad x this.origStorage of
@@ -718,16 +694,16 @@ exec1 = do
                   Just i -> checkJump i xs
             _ -> underrun
 
-        OpJumpi -> do
+        OpJumpi ->
           case stk of
-            (x:y:xs) -> forceConcrete x "JUMPI: symbolic jumpdest" $ \x' ->
-                burn g_high $
-                  let jump :: Bool -> EVM s ()
-                      jump False = assign (#state % #stack) xs >> next
-                      jump _    = case toInt x' of
-                        Nothing -> vmError BadJumpDestination
-                        Just i -> checkJump i xs
-                  in branch y jump
+            x:y:xs -> forceConcrete x "JUMPI: symbolic jumpdest" $ \x' ->
+              burn g_high $
+                let jump :: Bool -> EVM t s ()
+                    jump False = assign (#state % #stack) xs >> next
+                    jump _    = case toInt x' of
+                      Nothing -> vmError BadJumpDestination
+                      Just i -> checkJump i xs
+                in branch y jump
             _ -> underrun
 
         OpPc ->
@@ -740,7 +716,7 @@ exec1 = do
 
         OpGas ->
           limitStack 1 . burn g_base $
-            next >> push (into (vm.state.gas - g_base))
+            next >> pushGas
 
         OpJumpdest -> burn g_jumpdest next
 
@@ -749,13 +725,10 @@ exec1 = do
           --       https://hackage.haskell.org/package/sbv-9.0/docs/src/Data.SBV.Core.Model.html#.%5E
           --       However, it requires symbolic gas, since the gas depends on the exponent
           case stk of
-            base:exponent':xs -> forceConcrete exponent' "EXP: symbolic exponent" $ \exponent ->
-              let cost = if exponent == 0
-                         then g_exp
-                         else g_exp + g_expbyte * unsafeInto (ceilDiv (1 + log2 exponent) 8)
-              in burn cost $ do
+            base:exponent:xs ->
+              burnExp exponent $ do
                 next
-                (#state % #stack) .= Expr.exp base exponent' : xs
+                (#state % #stack) .= Expr.exp base exponent : xs
             _ -> underrun
 
         OpSignextend -> stackOp2 g_low Expr.sex
@@ -763,67 +736,62 @@ exec1 = do
         OpCreate ->
           notStatic $
           case stk of
-            xValue:xOffset':xSize':xs -> forceConcrete2 (xOffset', xSize') "CREATE" $
-              \(xOffset, xSize) -> do
-                accessMemoryRange xOffset xSize $ do
-                  availableGas <- use (#state % #gas)
-                  let
-                    (cost, gas') = costOfCreate fees availableGas xSize False
-                  newAddr <- createAddress self this.nonce
-                  _ <- accessAccountForGas newAddr
-                  burn cost $ do
-                    initCode <- readMemory xOffset' xSize'
-                    create self this xSize gas' xValue xs newAddr initCode
+            xValue:xOffset:xSize:xs ->
+              accessMemoryRange xOffset xSize $ do
+                availableGas <- use (#state % #gas)
+                let
+                  (cost, gas') = costOfCreate fees availableGas xSize False
+                newAddr <- createAddress self this.nonce
+                _ <- accessAccountForGas newAddr
+                burn' cost $ do
+                  initCode <- readMemory xOffset xSize
+                  create self this xSize gas' xValue xs newAddr initCode
             _ -> underrun
 
         OpCall ->
           case stk of
-            xGas':xTo':xValue:xInOffset':xInSize':xOutOffset':xOutSize':xs ->
-              forceConcrete5 (xGas', xInOffset', xInSize', xOutOffset', xOutSize') "CALL" $
-              \(xGas, xInOffset, xInSize, xOutOffset, xOutSize) ->
-                branch (Expr.gt xValue (Lit 0)) $ \gt0 -> do
-                  (if gt0 then notStatic else id) $
-                    forceAddr xTo' "unable to determine a call target" $ \xTo ->
-                      case tryFrom xGas of
-                        Left _ -> vmError IllegalOverflow
-                        Right gas ->
-                          delegateCall this gas xTo xTo xValue xInOffset xInSize xOutOffset xOutSize xs $
-                            \callee -> do
-                              let from' = fromMaybe self vm.config.overrideCaller
-                              zoom #state $ do
-                                assign #callvalue xValue
-                                assign #caller from'
-                                assign #contract callee
-                              assign (#config % #overrideCaller) Nothing
-                              touchAccount from'
-                              touchAccount callee
-                              transfer from' callee xValue
+            xGas:xTo':xValue:xInOffset:xInSize:xOutOffset:xOutSize:xs ->
+              branch (Expr.gt xValue (Lit 0)) $ \gt0 -> do
+                (if gt0 then notStatic else id) $
+                  forceAddr xTo' "unable to determine a call target" $ \xTo ->
+                    case gasTryFrom xGas of
+                      Left _ -> vmError IllegalOverflow
+                      Right gas ->
+                        delegateCall this gas xTo xTo xValue xInOffset xInSize xOutOffset xOutSize xs $
+                          \callee -> do
+                            let from' = fromMaybe self vm.config.overrideCaller
+                            zoom #state $ do
+                              assign #callvalue xValue
+                              assign #caller from'
+                              assign #contract callee
+                            assign (#config % #overrideCaller) Nothing
+                            touchAccount from'
+                            touchAccount callee
+                            transfer from' callee xValue
             _ ->
               underrun
 
         OpCallcode ->
           case stk of
-            xGas':xTo':xValue:xInOffset':xInSize':xOutOffset':xOutSize':xs ->
-              forceConcrete5 (xGas', xInOffset', xInSize', xOutOffset', xOutSize') "CALLCODE" $
-              \(xGas, xInOffset, xInSize, xOutOffset, xOutSize) ->
-                forceAddr xTo' "unable to determine a call target" $ \xTo ->
-                  case tryFrom xGas of
-                    Left _ -> vmError IllegalOverflow
-                    Right gas ->
-                      delegateCall this gas xTo self xValue xInOffset xInSize xOutOffset xOutSize xs $ \_ -> do
-                        zoom #state $ do
-                          assign #callvalue xValue
-                          assign #caller $ fromMaybe self vm.config.overrideCaller
-                        assign (#config % #overrideCaller) Nothing
-                        touchAccount self
+            xGas:xTo':xValue:xInOffset:xInSize:xOutOffset:xOutSize:xs ->
+              forceAddr xTo' "unable to determine a call target" $ \xTo ->
+                case gasTryFrom xGas of
+                  Left _ -> vmError IllegalOverflow
+                  Right gas ->
+                    delegateCall this gas xTo self xValue xInOffset xInSize xOutOffset xOutSize xs $ \_ -> do
+                      zoom #state $ do
+                        assign #callvalue xValue
+                        assign #caller $ fromMaybe self vm.config.overrideCaller
+                      assign (#config % #overrideCaller) Nothing
+                      touchAccount self
             _ ->
               underrun
 
         OpReturn ->
           case stk of
-            xOffset':xSize':_ -> forceConcrete2 (xOffset', xSize') "RETURN" $ \(xOffset, xSize) ->
+            xOffset:xSize:_ ->
               accessMemoryRange xOffset xSize $ do
-                output <- readMemory xOffset' xSize'
+                output <- readMemory xOffset xSize
                 let
                   codesize = fromMaybe (internalError "processing opcode RETURN. Cannot return dynamically sized abstract data")
                                . maybeLitWord . bufLength $ output
@@ -854,64 +822,59 @@ exec1 = do
 
         OpDelegatecall ->
           case stk of
-            xGas':xTo:xInOffset':xInSize':xOutOffset':xOutSize':xs ->
-              forceConcrete5 (xGas', xInOffset', xInSize', xOutOffset', xOutSize') "DELEGATECALL" $
-              \(xGas, xInOffset, xInSize, xOutOffset, xOutSize) ->
-                case wordToAddr xTo of
-                  Nothing -> do
-                    loc <- codeloc
-                    let msg = "Unable to determine a call target"
-                    partial $ UnexpectedSymbolicArg (snd loc) msg [SomeExpr xTo]
-                  Just xTo' ->
-                    case tryFrom xGas of
-                      Left _ -> vmError IllegalOverflow
-                      Right gas ->
-                        delegateCall this gas xTo' self (Lit 0) xInOffset xInSize xOutOffset xOutSize xs $
-                          \_ -> touchAccount self
+            xGas:xTo:xInOffset:xInSize:xOutOffset:xOutSize:xs ->
+              case wordToAddr xTo of
+                Nothing -> do
+                  loc <- codeloc
+                  let msg = "Unable to determine a call target"
+                  partial $ UnexpectedSymbolicArg (snd loc) msg [SomeExpr xTo]
+                Just xTo' ->
+                  case gasTryFrom xGas of
+                    Left _ -> vmError IllegalOverflow
+                    Right gas ->
+                      delegateCall this gas xTo' self (Lit 0) xInOffset xInSize xOutOffset xOutSize xs $
+                        \_ -> touchAccount self
             _ -> underrun
 
         OpCreate2 -> notStatic $
           case stk of
-            xValue:xOffset':xSize':xSalt':xs ->
-              forceConcrete3 (xOffset', xSize', xSalt') "CREATE2" $
-              \(xOffset, xSize, xSalt) ->
+            xValue:xOffset:xSize:xSalt':xs ->
+              forceConcrete xSalt' "CREATE2" $ \(xSalt) ->
                 accessMemoryRange xOffset xSize $ do
                   availableGas <- use (#state % #gas)
-                  buf <- readMemory xOffset' xSize'
+                  buf <- readMemory xOffset xSize
                   forceConcreteBuf buf "CREATE2" $
                     \initCode -> do
                       let
                         (cost, gas') = costOfCreate fees availableGas xSize True
                       newAddr <- create2Address self xSalt initCode
                       _ <- accessAccountForGas newAddr
-                      burn cost $
+                      burn' cost $
                         create self this xSize gas' xValue xs newAddr (ConcreteBuf initCode)
             _ -> underrun
 
         OpStaticcall ->
           case stk of
-            xGas':xTo:xInOffset':xInSize':xOutOffset':xOutSize':xs ->
-              forceConcrete5 (xGas', xInOffset', xInSize', xOutOffset', xOutSize') "STATICCALL" $
-              \(xGas, xInOffset, xInSize, xOutOffset, xOutSize) -> do
-                case wordToAddr xTo of
-                  Nothing -> do
-                    loc <- codeloc
-                    let msg = "Unable to determine a call target"
-                    partial $ UnexpectedSymbolicArg (snd loc) msg [SomeExpr xTo]
-                  Just xTo' ->
-                    case tryFrom xGas of
-                      Left _ -> vmError IllegalOverflow
-                      Right gas ->
-                        delegateCall this gas xTo' xTo' (Lit 0) xInOffset xInSize xOutOffset xOutSize xs $
-                          \callee -> do
-                            zoom #state $ do
-                              assign #callvalue (Lit 0)
-                              assign #caller $ fromMaybe self (vm.config.overrideCaller)
-                              assign #contract callee
-                              assign #static True
-                            assign (#config % #overrideCaller) Nothing
-                            touchAccount self
-                            touchAccount callee
+            xGas:xTo:xInOffset:xInSize:xOutOffset:xOutSize:xs ->
+              case wordToAddr xTo of
+                Nothing -> do
+                  loc <- codeloc
+                  let msg = "Unable to determine a call target"
+                  partial $ UnexpectedSymbolicArg (snd loc) msg [SomeExpr xTo]
+                Just xTo' ->
+                  case gasTryFrom xGas of
+                    Left _ -> vmError IllegalOverflow
+                    Right gas ->
+                      delegateCall this gas xTo' xTo' (Lit 0) xInOffset xInSize xOutOffset xOutSize xs $
+                        \callee -> do
+                          zoom #state $ do
+                            assign #callvalue (Lit 0)
+                            assign #caller $ fromMaybe self (vm.config.overrideCaller)
+                            assign #contract callee
+                            assign #static True
+                          assign (#config % #overrideCaller) Nothing
+                          touchAccount self
+                          touchAccount callee
             _ ->
               underrun
 
@@ -946,16 +909,16 @@ exec1 = do
 
         OpRevert ->
           case stk of
-            xOffset':xSize':_ -> forceConcrete2 (xOffset', xSize') "REVERT" $ \(xOffset, xSize) ->
+            xOffset:xSize:_ ->
               accessMemoryRange xOffset xSize $ do
-                output <- readMemory xOffset' xSize'
+                output <- readMemory xOffset xSize
                 finishFrame (FrameReverted output)
             _ -> underrun
 
         OpUnknown xxx ->
           vmError $ UnrecognizedOpcode xxx
 
-transfer :: Expr EAddr -> Expr EAddr -> Expr EWord -> EVM s ()
+transfer :: VMOps t => Expr EAddr -> Expr EAddr -> Expr EWord -> EVM t s ()
 transfer _ _ (Lit 0) = pure ()
 transfer src dst val = do
   sb <- preuse $ #env % #contracts % ix src % #balance
@@ -995,11 +958,20 @@ transfer src dst val = do
 
 -- | Checks a *CALL for failure; OOG, too many callframes, memory access etc.
 callChecks
-  :: (?op :: Word8)
-  => Contract -> Word64 -> Expr EAddr -> Expr EAddr -> Expr EWord -> W256 -> W256 -> W256 -> W256 -> [Expr EWord]
-   -- continuation with gas available for call
-  -> (Word64 -> EVM s ())
-  -> EVM s ()
+  :: forall (t :: VMType) s. (?op :: Word8, VMOps t)
+  => Contract
+  -> Gas t
+  -> Expr EAddr
+  -> Expr EAddr
+  -> Expr EWord
+  -> Expr EWord
+  -> Expr EWord
+  -> Expr EWord
+  -> Expr EWord
+  -> [Expr EWord]
+  -- continuation with gas available for call
+  -> (Gas t -> EVM t s ())
+  -> EVM t s ()
 callChecks this xGas xContext xTo xValue xInOffset xInSize xOutOffset xOutSize xs continue = do
   vm <- get
   let fees = vm.block.schedule
@@ -1007,62 +979,62 @@ callChecks this xGas xContext xTo xValue xInOffset xInSize xOutOffset xOutSize x
     accessMemoryRange xOutOffset xOutSize $ do
       availableGas <- use (#state % #gas)
       let recipientExists = accountExists xContext vm
-      (cost, gas') <- costOfCall fees recipientExists xValue availableGas xGas xTo
       let from = fromMaybe vm.state.contract vm.config.overrideCaller
       fromBal <- preuse $ #env % #contracts % ix from % #balance
-      let checkCallDepth =
-            if length vm.frames >= 1024
-            then do
-              assign (#state % #stack) (Lit 0 : xs)
-              assign (#state % #returndata) mempty
-              pushTrace $ ErrorTrace CallDepthLimitReached
-              next
-            else continue gas'
-      case (fromBal, xValue) of
-        -- we're not transfering any value, and can skip the balance check
-        (_, Lit 0) -> burn (cost - gas') checkCallDepth
-
-        -- from is in the state, we check if they have enough balance
-        (Just fb, _) -> do
-          burn (cost - gas') $
-            branch (Expr.gt xValue fb) $ \case
-              True -> do
+      costOfCall fees recipientExists xValue availableGas xGas xTo $ \cost gas' -> do
+        let checkCallDepth =
+              if length vm.frames >= 1024
+              then do
                 assign (#state % #stack) (Lit 0 : xs)
                 assign (#state % #returndata) mempty
-                pushTrace $ ErrorTrace (BalanceTooLow xValue this.balance)
+                pushTrace $ ErrorTrace CallDepthLimitReached
                 next
-              False -> checkCallDepth
+              else continue (toGas gas')
+        case (fromBal, xValue) of
+          -- we're not transfering any value, and can skip the balance check
+          (_, Lit 0) -> burn (cost - gas') checkCallDepth
+
+          -- from is in the state, we check if they have enough balance
+          (Just fb, _) -> do
+            burn (cost - gas') $
+              branch (Expr.gt xValue fb) $ \case
+                True -> do
+                  assign (#state % #stack) (Lit 0 : xs)
+                  assign (#state % #returndata) mempty
+                  pushTrace $ ErrorTrace (BalanceTooLow xValue this.balance)
+                  next
+                False -> checkCallDepth
 
-        -- from is not in the state, we insert it if safe to do so and run the checks again
-        (Nothing, _) -> case from of
-          LitAddr _ -> do
-            -- insert an entry in the state
-            let contract = case vm.config.baseState of
-                  AbstractBase -> unknownContract from
-                  EmptyBase -> emptyContract
-            (#env % #contracts) %= (Map.insert from contract)
-            -- run callChecks again
-            callChecks this xGas xContext xTo xValue xInOffset xInSize xOutOffset xOutSize xs continue
+          -- from is not in the state, we insert it if safe to do so and run the checks again
+          (Nothing, _) -> case from of
+            LitAddr _ -> do
+              -- insert an entry in the state
+              let contract = case vm.config.baseState of
+                    AbstractBase -> unknownContract from
+                    EmptyBase -> emptyContract
+              (#env % #contracts) %= (Map.insert from contract)
+              -- run callChecks again
+              callChecks this xGas xContext xTo xValue xInOffset xInSize xOutOffset xOutSize xs continue
 
-          -- adding a symbolic address into the state here would be unsound (due to potential aliasing)
-          SymAddr _ -> do
-            pc <- use (#state % #pc)
-            partial $ UnexpectedSymbolicArg pc "Attempting to transfer eth from a symbolic address that is not present in the state" (wrap [from])
-          GVar _ -> internalError "Unexpected GVar"
+            -- adding a symbolic address into the state here would be unsound (due to potential aliasing)
+            SymAddr _ -> do
+              pc <- use (#state % #pc)
+              partial $ UnexpectedSymbolicArg pc "Attempting to transfer eth from a symbolic address that is not present in the state" (wrap [from])
+            GVar _ -> internalError "Unexpected GVar"
 
 
 
 
 precompiledContract
-  :: (?op :: Word8)
+  :: (?op :: Word8, VMOps t)
   => Contract
-  -> Word64
+  -> Gas t
   -> Addr
   -> Addr
   -> Expr EWord
-  -> W256 -> W256 -> W256 -> W256
+  -> Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord
   -> [Expr EWord]
-  -> EVM s ()
+  -> EVM t s ()
 precompiledContract this xGas precompileAddr recipient xValue inOffset inSize outOffset outSize xs
   = callChecks this xGas (LitAddr recipient) (LitAddr precompileAddr) xValue inOffset inSize outOffset outSize xs $ \gas' ->
     do
@@ -1087,22 +1059,22 @@ precompiledContract this xGas precompileAddr recipient xValue inOffset inSize ou
         _ -> pure ()
 
 executePrecompile
-  :: (?op :: Word8)
+  :: (?op :: Word8, VMOps t)
   => Addr
-  -> Word64 -> W256 -> W256 -> W256 -> W256 -> [Expr EWord]
-  -> EVM s ()
+  -> Gas t -> Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord -> [Expr EWord]
+  -> EVM t s ()
 executePrecompile preCompileAddr gasCap inOffset inSize outOffset outSize xs  = do
   vm <- get
-  input <- readMemory (Lit inOffset) (Lit inSize)
+  input <- readMemory inOffset inSize
   let fees = vm.block.schedule
       cost = costOfPrecompile fees preCompileAddr input
       notImplemented = internalError $ "precompile at address " <> show preCompileAddr <> " not yet implemented"
-      precompileFail = burn (gasCap - cost) $ do
+      precompileFail = burn' (subGas gasCap cost) $ do
                          assign (#state % #stack) (Lit 0 : xs)
                          pushTrace $ ErrorTrace PrecompileFailure
                          next
-  if cost > gasCap then
-    burn gasCap $ do
+  if not (enoughGas cost gasCap) then
+    burn' gasCap $ do
       assign (#state % #stack) (Lit 0 : xs)
       next
   else burn cost $
@@ -1120,7 +1092,7 @@ executePrecompile preCompileAddr gasCap inOffset inSize outOffset outSize xs  =
             Just output -> do
               assign (#state % #stack) (Lit 1 : xs)
               assign (#state % #returndata) (ConcreteBuf output)
-              copyBytesToMemory (ConcreteBuf output) (Lit outSize) (Lit 0) (Lit outOffset)
+              copyBytesToMemory (ConcreteBuf output) outSize (Lit 0) outOffset
               next
 
       -- SHA2-256
@@ -1131,7 +1103,7 @@ executePrecompile preCompileAddr gasCap inOffset inSize outOffset outSize xs  =
             sha256Buf x = ConcreteBuf $ BA.convert (Crypto.hash x :: Digest SHA256)
           assign (#state % #stack) (Lit 1 : xs)
           assign (#state % #returndata) hash
-          copyBytesToMemory hash (Lit outSize) (Lit 0) (Lit outOffset)
+          copyBytesToMemory hash outSize (Lit 0) outOffset
           next
 
       -- RIPEMD-160
@@ -1144,14 +1116,14 @@ executePrecompile preCompileAddr gasCap inOffset inSize outOffset outSize xs  =
             hash  = ConcreteBuf $ padding <> hash'
           assign (#state % #stack) (Lit 1 : xs)
           assign (#state % #returndata) hash
-          copyBytesToMemory hash (Lit outSize) (Lit 0) (Lit outOffset)
+          copyBytesToMemory hash outSize (Lit 0) outOffset
           next
 
       -- IDENTITY
       0x4 -> do
           assign (#state % #stack) (Lit 1 : xs)
           assign (#state % #returndata) input
-          copyCallBytesToMemory input (Lit outSize) (Lit outOffset)
+          copyCallBytesToMemory input outSize outOffset
           next
 
       -- MODEXP
@@ -1173,7 +1145,7 @@ executePrecompile preCompileAddr gasCap inOffset inSize outOffset outSize xs  =
                   padLeft (unsafeInto lenm) (asBE (expFast b e m))
           assign (#state % #stack) (Lit 1 : xs)
           assign (#state % #returndata) output
-          copyBytesToMemory output (Lit outSize) (Lit 0) (Lit outOffset)
+          copyBytesToMemory output outSize (Lit 0) outOffset
           next
 
       -- ECADD
@@ -1186,7 +1158,7 @@ executePrecompile preCompileAddr gasCap inOffset inSize outOffset outSize xs  =
               let truncpaddedOutput = ConcreteBuf $ truncpadlit 64 output
               assign (#state % #stack) (Lit 1 : xs)
               assign (#state % #returndata) truncpaddedOutput
-              copyBytesToMemory truncpaddedOutput (Lit outSize) (Lit 0) (Lit outOffset)
+              copyBytesToMemory truncpaddedOutput outSize (Lit 0) outOffset
               next
 
       -- ECMUL
@@ -1199,7 +1171,7 @@ executePrecompile preCompileAddr gasCap inOffset inSize outOffset outSize xs  =
             let truncpaddedOutput = ConcreteBuf $ truncpadlit 64 output
             assign (#state % #stack) (Lit 1 : xs)
             assign (#state % #returndata) truncpaddedOutput
-            copyBytesToMemory truncpaddedOutput (Lit outSize) (Lit 0) (Lit outOffset)
+            copyBytesToMemory truncpaddedOutput outSize (Lit 0) outOffset
             next
 
       -- ECPAIRING
@@ -1212,7 +1184,7 @@ executePrecompile preCompileAddr gasCap inOffset inSize outOffset outSize xs  =
             let truncpaddedOutput = ConcreteBuf $ truncpadlit 32 output
             assign (#state % #stack) (Lit 1 : xs)
             assign (#state % #returndata) truncpaddedOutput
-            copyBytesToMemory truncpaddedOutput (Lit outSize) (Lit 0) (Lit outOffset)
+            copyBytesToMemory truncpaddedOutput outSize (Lit 0) outOffset
             next
 
       -- BLAKE2
@@ -1225,7 +1197,7 @@ executePrecompile preCompileAddr gasCap inOffset inSize outOffset outSize xs  =
                 let truncpaddedOutput = ConcreteBuf $ truncpadlit 64 output
                 assign (#state % #stack) (Lit 1 : xs)
                 assign (#state % #returndata) truncpaddedOutput
-                copyBytesToMemory truncpaddedOutput (Lit outSize) (Lit 0) (Lit outOffset)
+                copyBytesToMemory truncpaddedOutput outSize (Lit 0) outOffset
                 next
               Nothing -> precompileFail
             _ -> precompileFail
@@ -1273,16 +1245,16 @@ pushTo f x = f %= (x :)
 pushToSequence :: MonadState s m => Setter s s (Seq a) (Seq a) -> a -> m ()
 pushToSequence f x = f %= (Seq.|> x)
 
-getCodeLocation :: VM s -> CodeLocation
+getCodeLocation :: VM t s -> CodeLocation
 getCodeLocation vm = (vm.state.contract, vm.state.pc)
 
-query :: Query s -> EVM s ()
+query :: Query t s -> EVM t s ()
 query = assign #result . Just . HandleEffect . Query
 
-choose :: Choose s -> EVM s ()
+choose :: Choose t s -> EVM t s ()
 choose = assign #result . Just . HandleEffect . Choose
 
-branch :: forall s. Expr EWord -> (Bool -> EVM s ()) -> EVM s ()
+branch :: forall t s. Expr EWord -> (Bool -> EVM t s ()) -> EVM t s ()
 branch cond continue = do
   loc <- codeloc
   pathconds <- use #constraints
@@ -1290,7 +1262,7 @@ branch cond continue = do
   where
     condSimp = Expr.simplify cond
     condSimpConc = Expr.concKeccakSimpExpr condSimp
-    choosePath :: CodeLocation -> BranchCondition -> EVM s ()
+    choosePath :: CodeLocation -> BranchCondition -> EVM t s ()
     choosePath loc (Case v) = do
       assign #result Nothing
       pushTo #constraints $ if v then Expr.simplifyProp (condSimpConc ./= Lit 0) else Expr.simplifyProp (condSimpConc .== Lit 0)
@@ -1304,7 +1276,7 @@ branch cond continue = do
       choose . PleaseChoosePath condSimp $ choosePath loc . Case
 
 -- | Construct RPC Query and halt execution until resolved
-fetchAccount :: Expr EAddr -> (Contract -> EVM s ()) -> EVM s ()
+fetchAccount :: Expr EAddr -> (Contract -> EVM t s ()) -> EVM t s ()
 fetchAccount addr continue =
   use (#env % #contracts % at addr) >>= \case
     Just c -> continue c
@@ -1330,8 +1302,8 @@ fetchAccount addr continue =
 accessStorage
   :: Expr EAddr
   -> Expr EWord
-  -> (Expr EWord -> EVM s ())
-  -> EVM s ()
+  -> (Expr EWord -> EVM t s ())
+  -> EVM t s ()
 accessStorage addr slot continue = do
   let slotConc = Expr.concKeccakSimpExpr slot
   use (#env % #contracts % at addr) >>= \case
@@ -1371,7 +1343,7 @@ accessStorage addr slot continue = do
               assign #result Nothing
               continue (Lit x))
 
-accountExists :: Expr EAddr -> VM s -> Bool
+accountExists :: Expr EAddr -> VM t s -> Bool
 accountExists addr vm =
   case Map.lookup addr vm.env.contracts of
     Just c -> not (accountEmpty c)
@@ -1389,7 +1361,7 @@ accountEmpty c =
   && c.balance == Lit 0
 
 -- * How to finalize a transaction
-finalize :: EVM s ()
+finalize :: VMOps t => EVM t s ()
 finalize = do
   let
     revertContracts  = use (#tx % #txReversion) >>= assign (#env % #contracts)
@@ -1401,7 +1373,7 @@ finalize = do
       revertSubstate
     Just (VMFailure _) -> do
       -- burn remaining gas
-      assign (#state % #gas) 0
+      assign (#state % #gas) initialGas
       revertContracts
       revertSubstate
     Just (VMSuccess output) -> do
@@ -1427,21 +1399,10 @@ finalize = do
 
   -- compute and pay the refund to the caller and the
   -- corresponding payment to the miner
-  block        <- use #block
-  tx           <- use #tx
-  gasRemaining <- use (#state % #gas)
+  block <- use #block
 
-  let
-    sumRefunds   = sum (snd <$> tx.substate.refunds)
-    gasUsed      = tx.gaslimit - gasRemaining
-    cappedRefund = min (quot gasUsed 5) sumRefunds
-    originPay    = (into $ gasRemaining + cappedRefund) * tx.gasprice
-    minerPay     = tx.priorityFee * (into gasUsed)
+  payRefunds
 
-  modifying (#env % #contracts)
-     (Map.adjust (over #balance (Expr.add (Lit originPay))) tx.origin)
-  modifying (#env % #contracts)
-     (Map.adjust (over #balance (Expr.add (Lit minerPay))) block.coinbase)
   touchAccount block.coinbase
 
   -- perform state trie clearing (EIP 161), of selfdestructs
@@ -1462,7 +1423,7 @@ finalize = do
       (\k a -> not ((k `elem` touchedAddresses) && accountEmpty a)))
 
 -- | Loads the selected contract as the current contract to execute
-loadContract :: Expr EAddr -> State (VM s) ()
+loadContract :: Expr EAddr -> State (VM t s) ()
 loadContract target =
   preuse (#env % #contracts % ix target % #code) >>=
     \case
@@ -1473,121 +1434,81 @@ loadContract target =
         assign (#state % #code)     targetCode
         assign (#state % #codeContract) target
 
-limitStack :: Int -> EVM s () -> EVM s ()
+limitStack :: VMOps t => Int -> EVM (t :: VMType) s () -> EVM t s ()
 limitStack n continue = do
   stk <- use (#state % #stack)
   if length stk + n > 1024
     then vmError StackLimitExceeded
     else continue
 
-notStatic :: EVM s () -> EVM s ()
+notStatic :: VMOps t => EVM t s () -> EVM t s ()
 notStatic continue = do
   bad <- use (#state % #static)
   if bad
     then vmError StateChangeWhileStatic
     else continue
 
--- | Burn gas, failing if insufficient gas is available
-burn :: Word64 -> EVM s () -> EVM s ()
-burn n continue = do
-  available <- use (#state % #gas)
-  if n <= available
-    then do
-      #state % #gas %= (subtract n)
-      #burned %= (+ n)
-      continue
-    else
-      vmError (OutOfGas available n)
-
-forceAddr :: Expr EWord -> String -> (Expr EAddr -> EVM s ()) -> EVM s ()
+forceAddr :: Expr EWord -> String -> (Expr EAddr -> EVM t s ()) -> EVM t s ()
 forceAddr n msg continue = case wordToAddr n of
   Nothing -> do
     vm <- get
     partial $ UnexpectedSymbolicArg vm.state.pc msg (wrap [n])
   Just c -> continue c
 
-forceConcrete :: Expr EWord -> String -> (W256 -> EVM s ()) -> EVM s ()
+forceConcrete :: Expr EWord -> String -> (W256 -> EVM t s ()) -> EVM t s ()
 forceConcrete n msg continue = case maybeLitWord n of
   Nothing -> do
     vm <- get
     partial $ UnexpectedSymbolicArg vm.state.pc msg (wrap [n])
   Just c -> continue c
 
-forceConcreteAddr :: Expr EAddr -> String -> (Addr -> EVM s ()) -> EVM s ()
+forceConcreteAddr :: Expr EAddr -> String -> (Addr -> EVM t s ()) -> EVM t s ()
 forceConcreteAddr n msg continue = case maybeLitAddr n of
   Nothing -> do
     vm <- get
     partial $ UnexpectedSymbolicArg vm.state.pc msg (wrap [n])
   Just c -> continue c
 
-forceConcreteAddr2 :: (Expr EAddr, Expr EAddr) -> String -> ((Addr, Addr) -> EVM s ()) -> EVM s ()
+forceConcreteAddr2 :: (Expr EAddr, Expr EAddr) -> String -> ((Addr, Addr) -> EVM t s ()) -> EVM t s ()
 forceConcreteAddr2 (n,m) msg continue = case (maybeLitAddr n, maybeLitAddr m) of
   (Just c, Just d) -> continue (c,d)
   _ -> do
     vm <- get
     partial $ UnexpectedSymbolicArg vm.state.pc msg (wrap [n, m])
 
-forceConcrete2 :: (Expr EWord, Expr EWord) -> String -> ((W256, W256) -> EVM s ()) -> EVM s ()
+forceConcrete2 :: (Expr EWord, Expr EWord) -> String -> ((W256, W256) -> EVM t s ()) -> EVM t s ()
 forceConcrete2 (n,m) msg continue = case (maybeLitWord n, maybeLitWord m) of
   (Just c, Just d) -> continue (c, d)
   _ -> do
     vm <- get
     partial $ UnexpectedSymbolicArg vm.state.pc msg (wrap [n, m])
 
-forceConcrete3 :: (Expr EWord, Expr EWord, Expr EWord) -> String -> ((W256, W256, W256) -> EVM s ()) -> EVM s ()
-forceConcrete3 (k,n,m) msg continue = case (maybeLitWord k, maybeLitWord n, maybeLitWord m) of
-  (Just c, Just d, Just f) -> continue (c, d, f)
-  _ -> do
-    vm <- get
-    partial $ UnexpectedSymbolicArg vm.state.pc msg (wrap [k, n, m])
-
-forceConcrete4 :: (Expr EWord, Expr EWord, Expr EWord, Expr EWord) -> String -> ((W256, W256, W256, W256) -> EVM s ()) -> EVM s ()
-forceConcrete4 (k,l,n,m) msg continue = case (maybeLitWord k, maybeLitWord l, maybeLitWord n, maybeLitWord m) of
-  (Just b, Just c, Just d, Just f) -> continue (b, c, d, f)
-  _ -> do
-    vm <- get
-    partial $ UnexpectedSymbolicArg vm.state.pc msg (wrap [k, l, n, m])
-
-forceConcrete5 :: (Expr EWord, Expr EWord, Expr EWord, Expr EWord, Expr EWord) -> String -> ((W256, W256, W256, W256, W256) -> EVM s ()) -> EVM s ()
-forceConcrete5 (k,l,m,n,o) msg continue = case (maybeLitWord k, maybeLitWord l, maybeLitWord m, maybeLitWord n, maybeLitWord o) of
-  (Just a, Just b, Just c, Just d, Just e) -> continue (a, b, c, d, e)
-  _ -> do
-    vm <- get
-    partial $ UnexpectedSymbolicArg vm.state.pc msg (wrap [k, l, m, n, o])
-
-forceConcrete6 :: (Expr EWord, Expr EWord, Expr EWord, Expr EWord, Expr EWord, Expr EWord) -> String -> ((W256, W256, W256, W256, W256, W256) -> EVM s ()) -> EVM s ()
-forceConcrete6 (k,l,m,n,o,p) msg continue = case (maybeLitWord k, maybeLitWord l, maybeLitWord m, maybeLitWord n, maybeLitWord o, maybeLitWord p) of
-  (Just a, Just b, Just c, Just d, Just e, Just f) -> continue (a, b, c, d, e, f)
-  _ -> do
-    vm <- get
-    partial $ UnexpectedSymbolicArg vm.state.pc msg (wrap [k, l, m, n, o, p])
-
-forceConcreteBuf :: Expr Buf -> String -> (ByteString -> EVM s ()) -> EVM s ()
+forceConcreteBuf :: Expr Buf -> String -> (ByteString -> EVM t s ()) -> EVM t s ()
 forceConcreteBuf (ConcreteBuf b) _ continue = continue b
 forceConcreteBuf b msg _ = do
     vm <- get
     partial $ UnexpectedSymbolicArg vm.state.pc msg (wrap [b])
 
 -- * Substate manipulation
-refund :: Word64 -> EVM s ()
+refund :: Word64 -> EVM t s ()
 refund n = do
   self <- use (#state % #contract)
   pushTo (#tx % #substate % #refunds) (self, n)
 
-unRefund :: Word64 -> EVM s ()
+unRefund :: Word64 -> EVM t s ()
 unRefund n = do
   self <- use (#state % #contract)
   refs <- use (#tx % #substate % #refunds)
   assign (#tx % #substate % #refunds)
     (filter (\(a,b) -> not (a == self && b == n)) refs)
 
-touchAccount :: Expr EAddr -> EVM s ()
+touchAccount :: Expr EAddr -> EVM t s ()
 touchAccount = pushTo ((#tx % #substate) % #touchedAccounts)
 
-selfdestruct :: Expr EAddr -> EVM s ()
+selfdestruct :: Expr EAddr -> EVM t s ()
 selfdestruct = pushTo ((#tx % #substate) % #selfdestructs)
 
-accessAndBurn :: Expr EAddr -> EVM s () -> EVM s ()
+accessAndBurn :: VMOps t => Expr EAddr -> EVM t s () -> EVM t s ()
 accessAndBurn x cont = do
   FeeSchedule {..} <- use (#block % #schedule)
   acc <- accessAccountForGas x
@@ -1596,7 +1517,7 @@ accessAndBurn x cont = do
 
 -- | returns a wrapped boolean- if true, this address has been touched before in the txn (warm gas cost as in EIP 2929)
 -- otherwise cold
-accessAccountForGas :: Expr EAddr -> EVM s Bool
+accessAccountForGas :: Expr EAddr -> EVM t s Bool
 accessAccountForGas addr = do
   accessedAddrs <- use (#tx % #substate % #accessedAddresses)
   let accessed = member addr accessedAddrs
@@ -1605,7 +1526,7 @@ accessAccountForGas addr = do
 
 -- | returns a wrapped boolean- if true, this slot has been touched before in the txn (warm gas cost as in EIP 2929)
 -- otherwise cold
-accessStorageForGas :: Expr EAddr -> Expr EWord -> EVM s Bool
+accessStorageForGas :: Expr EAddr -> Expr EWord -> EVM t s Bool
 accessStorageForGas addr key = do
   accessedStrkeys <- use (#tx % #substate % #accessedStorageKeys)
   case maybeLitWord key of
@@ -1613,7 +1534,7 @@ accessStorageForGas addr key = do
       let accessed = member (addr, litword) accessedStrkeys
       assign (#tx % #substate % #accessedStorageKeys) (insert (addr, litword) accessedStrkeys)
       pure accessed
-    _ -> return False
+    _ -> pure False
 
 -- * Cheat codes
 
@@ -1625,13 +1546,13 @@ cheatCode :: Expr EAddr
 cheatCode = LitAddr $ unsafeInto (keccak' "hevm cheat code")
 
 cheat
-  :: (?op :: Word8)
-  => (W256, W256) -> (W256, W256)
-  -> EVM s ()
+  :: (?op :: Word8, VMOps t)
+  => (Expr EWord, Expr EWord) -> (Expr EWord, Expr EWord)
+  -> EVM t s ()
 cheat (inOffset, inSize) (outOffset, outSize) = do
   vm <- get
-  input <- readMemory (Lit $ inOffset + 4) (Lit $ inSize - 4)
-  abi <- readBytes 4 (Lit 0) <$> readMemory (Lit inOffset) (Lit 4)
+  input <- readMemory (Expr.add inOffset (Lit 4)) (Expr.sub inSize (Lit 4))
+  abi <- readBytes 4 (Lit 0) <$> readMemory inOffset (Lit 4)
   pushTrace $ FrameTrace (CallContext cheatCode cheatCode inOffset inSize (Lit 0) (maybeLitWord abi) input vm.env.contracts vm.tx.substate)
   case maybeLitWord abi of
     Nothing -> partial $ UnexpectedSymbolicArg vm.state.pc "symbolic cheatcode selector" (wrap [abi])
@@ -1640,14 +1561,14 @@ cheat (inOffset, inSize) (outOffset, outSize) = do
         Nothing ->
           vmError (BadCheatCode abi')
         Just action -> do
-            action (Lit outOffset) (Lit outSize) input
+            action outOffset outSize input
             popTrace
             next
             push 1
 
-type CheatAction s = Expr EWord -> Expr EWord -> Expr Buf -> EVM s ()
+type CheatAction t s = Expr EWord -> Expr EWord -> Expr Buf -> EVM t s ()
 
-cheatActions :: Map FunctionSelector (CheatAction s)
+cheatActions :: VMOps t => Map FunctionSelector (CheatAction t s)
 cheatActions =
   Map.fromList
     [ action "ffi(string[])" $
@@ -1721,7 +1642,7 @@ cheatActions =
         \sig outOffset _ input -> case decodeStaticArgs 0 2 input of
           [sk, hash] ->
             forceConcrete2 (sk, hash) "cannot sign symbolic data" $ \(sk', hash') -> do
-              let (v,r,s) = EVM.Sign.sign hash' (toInteger sk')
+              let (v,r,s) = EVM.Sign.sign hash' (into sk')
                   encoded = encodeAbiValue $
                     AbiTuple (V.fromList
                       [ AbiUInt 8 $ into v
@@ -1759,11 +1680,19 @@ cheatActions =
 -- * General call implementation ("delegateCall")
 -- note that the continuation is ignored in the precompile case
 delegateCall
-  :: (?op :: Word8)
-  => Contract -> Word64 -> Expr EAddr -> Expr EAddr -> Expr EWord -> W256 -> W256 -> W256 -> W256
+  :: (VMOps t, ?op :: Word8)
+  => Contract
+  -> Gas t
+  -> Expr EAddr
+  -> Expr EAddr
+  -> Expr EWord
+  -> Expr EWord
+  -> Expr EWord
+  -> Expr EWord
+  -> Expr EWord
   -> [Expr EWord]
-  -> (Expr EAddr -> EVM s ())
-  -> EVM s ()
+  -> (Expr EAddr -> EVM t s ())
+  -> EVM t s ()
 delegateCall this gasGiven xTo xContext xValue xInOffset xInSize xOutOffset xOutSize xs continue
   | isPrecompileAddr xTo
       = forceConcreteAddr2 (xTo, xContext) "Cannot call precompile with symbolic addresses" $
@@ -1781,9 +1710,9 @@ delegateCall this gasGiven xTo xContext xValue xInOffset xInSize xOutOffset xOut
                 pc <- use (#state % #pc)
                 partial $ UnexpectedSymbolicArg pc "call target has unknown code" (wrap [xTo])
               _ -> do
-                burn xGas $ do
-                  calldata <- readMemory (Lit xInOffset) (Lit xInSize)
-                  abi <- maybeLitWord . readBytes 4 (Lit 0) <$> readMemory (Lit xInOffset) (Lit 4)
+                burn' xGas $ do
+                  calldata <- readMemory xInOffset xInSize
+                  abi <- maybeLitWord . readBytes 4 (Lit 0) <$> readMemory xInOffset (Lit 4)
                   let newContext = CallContext
                                     { target    = xTo
                                     , context   = xContext
@@ -1832,12 +1761,12 @@ collision c' = case c' of
     _ -> True
   Nothing -> False
 
-create :: (?op :: Word8)
+create :: forall t s. (?op :: Word8, VMOps t)
   => Expr EAddr -> Contract
-  -> W256 -> Word64 -> Expr EWord -> [Expr EWord] -> Expr EAddr -> Expr Buf -> EVM s ()
+  -> Expr EWord -> Gas t -> Expr EWord -> [Expr EWord] -> Expr EAddr -> Expr Buf -> EVM t s ()
 create self this xSize xGas xValue xs newAddr initCode = do
   vm0 <- get
-  if xSize > vm0.block.maxCodeSize * 2
+  if xSize > Lit (vm0.block.maxCodeSize * 2)
   then do
     assign (#state % #stack) (Lit 0 : xs)
     assign (#state % #returndata) mempty
@@ -1855,7 +1784,7 @@ create self this xSize xGas xValue xs newAddr initCode = do
     pushTrace $ ErrorTrace CallDepthLimitReached
     next
   else if collision $ Map.lookup newAddr vm0.env.contracts
-  then burn xGas $ do
+  then burn' xGas $ do
     assign (#state % #stack) (Lit 0 : xs)
     assign (#state % #returndata) mempty
     modifying (#env % #contracts % ix self % #nonce) (fmap ((+) 1))
@@ -1870,7 +1799,7 @@ create self this xSize xGas xValue xs newAddr initCode = do
         touchAccount self
         touchAccount newAddr
       -- are we overflowing the nonce
-      False -> burn xGas $ do
+      False -> burn' xGas $ do
         case parseInitCode initCode of
           Nothing ->
             partial $ UnexpectedSymbolicArg vm0.state.pc "initcode must have a concrete prefix" []
@@ -1913,7 +1842,7 @@ create self this xSize xGas xValue xs newAddr initCode = do
               , state   = vm1.state { stack = xs }
               }
 
-            state <- lift blankState
+            state :: FrameState t s <- lift blankState
             assign #state $ state
               { contract     = newAddr
               , codeContract = newAddr
@@ -1947,7 +1876,7 @@ parseInitCode buf = if V.null conc
 
 -- | Replace a contract's code, like when CREATE returns
 -- from the constructor code.
-replaceCode :: Expr EAddr -> ContractCode -> EVM s ()
+replaceCode :: Expr EAddr -> ContractCode -> EVM t s ()
 replaceCode target newCode =
   zoom (#env % #contracts % at target) $
     get >>= \case
@@ -1966,28 +1895,28 @@ replaceCode target newCode =
       Nothing ->
         internalError "Can't replace code of nonexistent contract"
 
-replaceCodeOfSelf :: ContractCode -> EVM s ()
+replaceCodeOfSelf :: ContractCode -> EVM t s ()
 replaceCodeOfSelf newCode = do
   vm <- get
   replaceCode vm.state.contract newCode
 
-resetState :: EVM s ()
+resetState :: VMOps t => EVM t s ()
 resetState = do
   state <- lift blankState
   modify' $ \vm -> vm { result = Nothing, frames = [], state }
 
 -- * VM error implementation
 
-vmError :: EvmError -> EVM s ()
+vmError :: VMOps t => EvmError -> EVM t s ()
 vmError e = finishFrame (FrameErrored e)
 
-partial :: PartialExec -> EVM s ()
+partial :: PartialExec -> EVM t s ()
 partial e = assign #result (Just (Unfinished e))
 
 wrap :: Typeable a => [Expr a] -> [SomeExpr]
 wrap = fmap SomeExpr
 
-underrun :: EVM s ()
+underrun :: VMOps t => EVM t s ()
 underrun = vmError StackUnderrun
 
 -- | A stack frame can be popped in three ways.
@@ -2002,7 +1931,7 @@ data FrameResult
 --
 -- It also handles the case when the current stack frame is the only one;
 -- in this case, we set the final '_result' of the VM execution.
-finishFrame :: FrameResult -> EVM s ()
+finishFrame :: VMOps t => FrameResult -> EVM t s ()
 finishFrame how = do
   oldVm <- get
 
@@ -2035,20 +1964,12 @@ finishFrame how = do
       -- Install the state of the frame to which we shall return.
       assign #state nextFrame.state
 
-      -- When entering a call, the gas allowance is counted as burned
-      -- in advance; this unburns the remainder and adds it to the
-      -- parent frame.
-      let remainingGas = oldVm.state.gas
-          reclaimRemainingGasAllowance = do
-            modifying #burned (subtract remainingGas)
-            modifying (#state % #gas) (+ remainingGas)
-
       -- Now dispatch on whether we were creating or calling,
       -- and whether we shall return, revert, or internalError(six cases).
       case nextFrame.context of
 
         -- Were we calling?
-        CallContext _ _ (Lit -> outOffset) (Lit -> outSize) _ _ _ reversion substate' -> do
+        CallContext _ _ outOffset outSize _ _ _ reversion substate' -> do
 
           -- Excerpt K.1. from the yellow paper:
           -- K.1. Deletion of an Account Despite Out-of-gas.
@@ -2069,7 +1990,7 @@ finishFrame how = do
             FrameReturned output -> do
               assign (#state % #returndata) output
               copyCallBytesToMemory output outSize outOffset
-              reclaimRemainingGasAllowance
+              reclaimRemainingGasAllowance oldVm
               push 1
 
             -- Case 2: Reverting during a call?
@@ -2078,7 +1999,7 @@ finishFrame how = do
               revertSubstate
               assign (#state % #returndata) output
               copyCallBytesToMemory output outSize outOffset
-              reclaimRemainingGasAllowance
+              reclaimRemainingGasAllowance oldVm
               push 0
 
             -- Case 3: Error during a call?
@@ -2104,7 +2025,7 @@ finishFrame how = do
               let onContractCode contractCode = do
                     replaceCode createe contractCode
                     assign (#state % #returndata) mempty
-                    reclaimRemainingGasAllowance
+                    reclaimRemainingGasAllowance oldVm
                     pushAddr createe
               case output of
                 ConcreteBuf bs ->
@@ -2124,7 +2045,7 @@ finishFrame how = do
               revertContracts
               revertSubstate
               assign (#state % #returndata) output
-              reclaimRemainingGasAllowance
+              reclaimRemainingGasAllowance oldVm
               push 0
 
             -- Case 6: Error during a creation?
@@ -2138,10 +2059,10 @@ finishFrame how = do
 -- * Memory helpers
 
 accessUnboundedMemoryRange
-  :: Word64
+  :: VMOps t => Word64
   -> Word64
-  -> EVM s ()
-  -> EVM s ()
+  -> EVM t s ()
+  -> EVM t s ()
 accessUnboundedMemoryRange _ 0 continue = continue
 accessUnboundedMemoryRange f l continue = do
   m0 <- use (#state % #memorySize)
@@ -2152,25 +2073,28 @@ accessUnboundedMemoryRange f l continue = do
     continue
 
 accessMemoryRange
-  :: W256
-  -> W256
-  -> EVM s ()
-  -> EVM s ()
-accessMemoryRange _ 0 continue = continue
-accessMemoryRange offs sz continue =
+  :: VMOps t
+  => Expr EWord
+  -> Expr EWord
+  -> EVM t s ()
+  -> EVM t s ()
+accessMemoryRange _ (Lit 0) continue = continue
+accessMemoryRange (Lit offs) (Lit sz) continue =
   case (,) <$> toWord64 offs <*> toWord64 sz of
     Nothing -> vmError IllegalOverflow
     Just (offs64, sz64) ->
       if offs64 + sz64 < sz64
         then vmError IllegalOverflow
         else accessUnboundedMemoryRange offs64 sz64 continue
+-- we just ignore gas if we get symbolic inputs
+accessMemoryRange _ _ continue = continue
 
 accessMemoryWord
-  :: W256 -> EVM s () -> EVM s ()
-accessMemoryWord x = accessMemoryRange x 32
+  :: VMOps t => Expr EWord -> EVM t s () -> EVM t s ()
+accessMemoryWord x = accessMemoryRange x (Lit 32)
 
 copyBytesToMemory
-  :: Expr Buf -> Expr EWord -> Expr EWord -> Expr EWord -> EVM s ()
+  :: Expr Buf -> Expr EWord -> Expr EWord -> Expr EWord -> EVM t s ()
 copyBytesToMemory bs size srcOffset memOffset =
   if size == Lit 0 then noop
   else do
@@ -2197,11 +2121,11 @@ copyBytesToMemory bs size srcOffset memOffset =
           SymbolicMemory $ copySlice srcOffset memOffset size bs mem
 
 copyCallBytesToMemory
-  :: Expr Buf -> Expr EWord -> Expr EWord -> EVM s ()
+  :: Expr Buf -> Expr EWord -> Expr EWord -> EVM t s ()
 copyCallBytesToMemory bs size yOffset =
   copyBytesToMemory bs (Expr.min size (bufLength bs)) (Lit 0) yOffset
 
-readMemory :: Expr EWord -> Expr EWord -> EVM s (Expr Buf)
+readMemory :: Expr EWord -> Expr EWord -> EVM t s (Expr Buf)
 readMemory offset' size' = do
   vm <- get
   case vm.state.memory of
@@ -2229,7 +2153,7 @@ readMemory offset' size' = do
 
 -- * Tracing
 
-withTraceLocation :: TraceData -> EVM s Trace
+withTraceLocation :: TraceData -> EVM t s Trace
 withTraceLocation x = do
   vm <- get
   let this = fromJust $ currentContract vm
@@ -2239,19 +2163,19 @@ withTraceLocation x = do
     , opIx = fromMaybe 0 $ this.opIxMap SV.!? vm.state.pc
     }
 
-pushTrace :: TraceData -> EVM s ()
+pushTrace :: TraceData -> EVM t s ()
 pushTrace x = do
   trace <- withTraceLocation x
   modifying #traces $
     \t -> Zipper.children $ Zipper.insert (Node trace []) t
 
-insertTrace :: TraceData -> EVM s ()
+insertTrace :: TraceData -> EVM t s ()
 insertTrace x = do
   trace <- withTraceLocation x
   modifying #traces $
     \t -> Zipper.nextSpace $ Zipper.insert (Node trace []) t
 
-popTrace :: EVM s ()
+popTrace :: EVM t s ()
 popTrace =
   modifying #traces $
     \t -> case Zipper.parent t of
@@ -2264,7 +2188,7 @@ zipperRootForest z =
     Nothing -> Zipper.toForest z
     Just z' -> zipperRootForest (Zipper.nextSpace z')
 
-traceForest :: VM s -> Forest Trace
+traceForest :: VM t s -> Forest Trace
 traceForest vm = zipperRootForest vm.traces
 
 traceForest' :: Expr End -> Forest Trace
@@ -2281,7 +2205,7 @@ traceContext (Failure _ (Traces _ c) _) = c
 traceContext (ITE {}) = internalError"Internal Error: ITE does not contain a trace"
 traceContext (GVar {}) = internalError"Internal Error: Unexpected GVar"
 
-traceTopLog :: [Expr Log] -> EVM s ()
+traceTopLog :: [Expr Log] -> EVM t s ()
 traceTopLog [] = noop
 traceTopLog ((LogEntry addr bytes topics) : _) = do
   trace <- withTraceLocation (EventTrace addr bytes topics)
@@ -2291,22 +2215,22 @@ traceTopLog ((GVar _) : _) = internalError "unexpected global variable"
 
 -- * Stack manipulation
 
-push :: W256 -> EVM s ()
+push :: W256 -> EVM t s ()
 push = pushSym . Lit
 
-pushSym :: Expr EWord -> EVM s ()
+pushSym :: Expr EWord -> EVM t s ()
 pushSym x = #state % #stack %= (x :)
 
-pushAddr :: Expr EAddr -> EVM s ()
+pushAddr :: Expr EAddr -> EVM t s ()
 pushAddr (LitAddr x) = #state % #stack %= (Lit (into x) :)
 pushAddr x@(SymAddr _) = #state % #stack %= (WAddr x :)
 pushAddr (GVar _) = internalError "Unexpected GVar"
 
 stackOp1
-  :: (?op :: Word8)
+  :: (?op :: Word8, VMOps t)
   => Word64
   -> (Expr EWord -> Expr EWord)
-  -> EVM s ()
+  -> EVM t s ()
 stackOp1 cost f =
   use (#state % #stack) >>= \case
     x:xs ->
@@ -2318,10 +2242,10 @@ stackOp1 cost f =
       underrun
 
 stackOp2
-  :: (?op :: Word8)
+  :: (?op :: Word8, VMOps t)
   => Word64
   -> (Expr EWord -> Expr EWord -> Expr EWord)
-  -> EVM s ()
+  -> EVM t s ()
 stackOp2 cost f =
   use (#state % #stack) >>= \case
     x:y:xs ->
@@ -2332,10 +2256,10 @@ stackOp2 cost f =
       underrun
 
 stackOp3
-  :: (?op :: Word8)
+  :: (?op :: Word8, VMOps t)
   => Word64
   -> (Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord)
-  -> EVM s ()
+  -> EVM t s ()
 stackOp3 cost f =
   use (#state % #stack) >>= \case
     x:y:z:xs ->
@@ -2347,12 +2271,7 @@ stackOp3 cost f =
 
 -- * Bytecode data functions
 
-use' :: (VM s -> a) -> EVM s a
-use' f = do
-  vm <- get
-  pure (f vm)
-
-checkJump :: Int -> [Expr EWord] -> EVM s ()
+checkJump :: VMOps t => Int -> [Expr EWord] -> EVM t s ()
 checkJump x xs = noJumpIntoInitData x $ do
   vm <- get
   case isValidJumpDest vm x of
@@ -2362,7 +2281,7 @@ checkJump x xs = noJumpIntoInitData x $ do
     False -> vmError BadJumpDestination
 
 -- fails with partial if we're trying to jump into the symbolic region of an `InitCode`
-noJumpIntoInitData :: Int -> EVM s () -> EVM s ()
+noJumpIntoInitData :: Int -> EVM t s () -> EVM t s ()
 noJumpIntoInitData idx cont = do
   vm <- get
   case vm.state.code of
@@ -2377,7 +2296,7 @@ noJumpIntoInitData idx cont = do
     -- we're not executing init code, so nothing to check here
     _ -> cont
 
-isValidJumpDest :: VM s -> Int -> Bool
+isValidJumpDest :: VM t s -> Int -> Bool
 isValidJumpDest vm x = let
     code = vm.state.code
     self = vm.state.codeContract
@@ -2441,7 +2360,7 @@ mkOpIxMap (RuntimeCode (SymbolicRuntimeCode ops))
           {- PUSH data. -}        (n - 1,        i + 1, j,     m >> SV.write v i j)
 
 
-vmOp :: VM s -> Maybe Op
+vmOp :: VM t s -> Maybe Op
 vmOp vm =
   let i  = vm ^. #state % #pc
       code' = vm ^. #state % #code
@@ -2457,7 +2376,7 @@ vmOp vm =
      then Nothing
      else Just (readOp op pushdata)
 
-vmOpIx :: VM s -> Maybe Int
+vmOpIx :: VM t s -> Maybe Int
 vmOpIx vm =
   do self <- currentContract vm
      self.opIxMap SV.!? vm.state.pc
@@ -2486,38 +2405,6 @@ mkCodeOps contractCode =
 
 -- * Gas cost calculation helpers
 
--- Gas cost function for CALL, transliterated from the Yellow Paper.
-costOfCall
-  :: FeeSchedule Word64
-  -> Bool -> Expr EWord -> Word64 -> Word64 -> Expr EAddr
-  -> EVM s (Word64, Word64)
-costOfCall (FeeSchedule {..}) recipientExists (Lit xValue) availableGas xGas target = do
-  acc <- accessAccountForGas target
-  let call_base_gas = if acc then g_warm_storage_read else g_cold_account_access
-      c_new = if not recipientExists && xValue /= 0
-            then g_newaccount
-            else 0
-      c_xfer = if xValue /= 0  then g_callvalue else 0
-      c_extra = call_base_gas + c_xfer + c_new
-      c_gascap =  if availableGas >= c_extra
-                  then min xGas (allButOne64th (availableGas - c_extra))
-                  else xGas
-      c_callgas = if xValue /= 0 then c_gascap + g_callstipend else c_gascap
-  pure (c_gascap + c_extra, c_callgas)
--- calls are free if value is symbolic :)
-costOfCall _ _ _ _ _ _ = pure (0,0)
-
--- Gas cost of create, including hash cost if needed
-costOfCreate
-  :: FeeSchedule Word64
-  -> Word64 -> W256 -> Bool -> (Word64, Word64)
-costOfCreate (FeeSchedule {..}) availableGas size hashNeeded = (createCost, initGas)
-  where
-    byteCost   = if hashNeeded then g_sha3word + g_initcodeword else g_initcodeword
-    createCost = g_create + codeCost
-    codeCost   = byteCost * (ceilDiv (unsafeInto size) 32)
-    initGas    = allButOne64th (availableGas - createCost)
-
 concreteModexpGasFee :: ByteString -> Word64
 concreteModexpGasFee input =
   if lenb < into (maxBound :: Word32) &&
@@ -2618,22 +2505,22 @@ toBuf (InitCode ops args) = Just $ ConcreteBuf ops <> args
 toBuf (RuntimeCode (ConcreteRuntimeCode ops)) = Just $ ConcreteBuf ops
 toBuf (RuntimeCode (SymbolicRuntimeCode ops)) = Just $ Expr.fromList ops
 
-codeloc :: EVM s CodeLocation
+codeloc :: EVM t s CodeLocation
 codeloc = do
   vm <- get
   pure (vm.state.contract, vm.state.pc)
 
-createAddress :: Expr EAddr -> Maybe W64 -> EVM s (Expr EAddr)
+createAddress :: Expr EAddr -> Maybe W64 -> EVM t s (Expr EAddr)
 createAddress (LitAddr a) (Just n) = pure $ Concrete.createAddress a n
 createAddress (GVar _) _ = internalError "Unexpected GVar"
 createAddress _ _ = freshSymAddr
 
-create2Address :: Expr EAddr -> W256 -> ByteString -> EVM s (Expr EAddr)
+create2Address :: Expr EAddr -> W256 -> ByteString -> EVM t s (Expr EAddr)
 create2Address (LitAddr a) s b = pure $ Concrete.create2Address a s b
 create2Address (SymAddr _) _ _ = freshSymAddr
 create2Address (GVar _) _ _ = internalError "Unexpected GVar"
 
-freshSymAddr :: EVM s (Expr EAddr)
+freshSymAddr :: EVM t s (Expr EAddr)
 freshSymAddr = do
   modifying (#env % #freshAddresses) (+ 1)
   n <- use (#env % #freshAddresses)
@@ -2656,7 +2543,7 @@ allButOne64th n = n - div n 64
 log2 :: FiniteBits b => b -> Int
 log2 x = finiteBitSize x - 1 - countLeadingZeros x
 
-writeMemory :: MutableMemory s -> Int -> ByteString -> EVM s ()
+writeMemory :: MutableMemory s -> Int -> ByteString -> EVM t s ()
 writeMemory memory offset buf = do
   memory' <- expandMemory (offset + BS.length buf)
   mapM_ (uncurry (VUnboxed.Mutable.write memory'))
@@ -2671,6 +2558,192 @@ writeMemory memory offset buf = do
     else
       pure memory
 
-freezeMemory :: MutableMemory s -> EVM s (Expr Buf)
+freezeMemory :: MutableMemory s -> EVM t s (Expr Buf)
 freezeMemory memory =
   ConcreteBuf . BS.pack . VUnboxed.toList <$> VUnboxed.freeze memory
+
+
+instance VMOps Symbolic where
+  burn' _ continue = continue
+  burnExp _ continue = continue
+  burnSha3 _ continue = continue
+  burnCalldatacopy _ continue = continue
+  burnCodecopy _ continue = continue
+  burnExtcodecopy _ _ continue = continue
+  burnReturndatacopy _ continue = continue
+  burnLog _ _ continue = continue
+
+  initialGas = ()
+  ensureGas _ continue = continue
+  gasTryFrom _ = Right ()
+  costOfCreate _ _ _ _ = ((), ())
+  costOfCall _ _ _ _ _ _ continue = continue 0 0
+  reclaimRemainingGasAllowance _ = pure ()
+  payRefunds = pure ()
+  pushGas = do
+    modifying (#env % #freshGasVals) (+ 1)
+    n <- use (#env % #freshGasVals)
+    pushSym $ Expr.Gas n
+  enoughGas _ _ = True
+  subGas _ _ = ()
+  toGas _ = ()
+  whenSymbolicElse a _ = a
+
+instance VMOps Concrete where
+  burn' n continue = do
+    available <- use (#state % #gas)
+    if n <= available
+      then do
+        #state % #gas %= (subtract n)
+        #burned %= (+ n)
+        continue
+      else
+        vmError (OutOfGas available n)
+
+  burnExp (forceLit -> exponent) continue = do
+    FeeSchedule {..} <- gets (.block.schedule)
+    let cost = if exponent == 0
+          then g_exp
+          else g_exp + g_expbyte * unsafeInto (ceilDiv (1 + log2 exponent) 8)
+    burn cost continue
+
+  burnSha3 (forceLit -> xSize) continue = do
+    FeeSchedule {..} <- gets (.block.schedule)
+    burn (g_sha3 + g_sha3word * ceilDiv (unsafeInto xSize) 32) continue
+
+  burnCalldatacopy (forceLit -> xSize) continue = do
+    FeeSchedule {..} <- gets (.block.schedule)
+    burn (g_verylow + g_copy * ceilDiv (unsafeInto xSize) 32) continue
+
+  burnCodecopy (forceLit -> n) continue =
+    case tryFrom n of
+      Left _ -> vmError IllegalOverflow
+      Right n' -> do
+        FeeSchedule {..} <- gets (.block.schedule)
+        if n' <= ( (maxBound :: Word64) - g_verylow ) `div` g_copy * 32 then
+          burn (g_verylow + g_copy * ceilDiv (unsafeInto n) 32) continue
+        else vmError IllegalOverflow
+
+  burnExtcodecopy extAccount (forceLit -> codeSize) continue = do
+    FeeSchedule {..} <- gets (.block.schedule)
+    acc <- accessAccountForGas extAccount
+    let cost = if acc then g_warm_storage_read else g_cold_account_access
+    burn (cost + g_copy * ceilDiv (unsafeInto codeSize) 32) continue
+
+  burnReturndatacopy (forceLit -> xSize) continue = do
+    FeeSchedule {..} <- gets (.block.schedule)
+    burn (g_verylow + g_copy * ceilDiv (unsafeInto xSize) 32) continue
+
+  burnLog (forceLit -> xSize) n continue = do
+    case tryFrom xSize of
+      Right sz -> do
+        FeeSchedule {..} <- gets (.block.schedule)
+        burn (g_log + g_logdata * sz + (into n) * g_logtopic) continue
+      _ -> vmError IllegalOverflow
+
+  initialGas = 0
+
+  ensureGas amount continue = do
+    availableGas <- use (#state % #gas)
+
+    if availableGas <= amount then
+      vmError (OutOfGas availableGas amount)
+    else continue
+
+  gasTryFrom (forceLit -> w256) =
+    case tryFrom w256 of
+      Left _ -> Left ()
+      Right a -> Right a
+
+  -- Gas cost of create, including hash cost if needed
+  costOfCreate (FeeSchedule {..}) availableGas size hashNeeded = (createCost, initGas)
+    where
+      byteCost   = if hashNeeded then g_sha3word + g_initcodeword else g_initcodeword
+      createCost = g_create + codeCost
+      codeCost   = byteCost * (ceilDiv (unsafeInto (forceLit size)) 32)
+      initGas    = allButOne64th (availableGas - createCost)
+
+  -- Gas cost function for CALL, transliterated from the Yellow Paper.
+  costOfCall (FeeSchedule {..}) recipientExists (forceLit -> xValue) availableGas xGas target continue = do
+    acc <- accessAccountForGas target
+    let call_base_gas = if acc then g_warm_storage_read else g_cold_account_access
+        c_new = if not recipientExists && xValue /= 0
+              then g_newaccount
+              else 0
+        c_xfer = if xValue /= 0  then g_callvalue else 0
+        c_extra = call_base_gas + c_xfer + c_new
+        c_gascap =  if availableGas >= c_extra
+                    then min xGas (allButOne64th (availableGas - c_extra))
+                    else xGas
+        c_callgas = if xValue /= 0 then c_gascap + g_callstipend else c_gascap
+    let (cost, gas') = (c_gascap + c_extra, c_callgas)
+    continue cost gas'
+
+  -- When entering a call, the gas allowance is counted as burned
+  -- in advance; this unburns the remainder and adds it to the
+  -- parent frame.
+  reclaimRemainingGasAllowance oldVm = do
+    let remainingGas = oldVm.state.gas
+    modifying #burned (subtract remainingGas)
+    modifying (#state % #gas) (+ remainingGas)
+
+  payRefunds = do
+    -- compute and pay the refund to the caller and the
+    -- corresponding payment to the miner
+    block        <- use #block
+    tx           <- use #tx
+    gasRemaining <- use (#state % #gas)
+
+    let
+      sumRefunds   = sum (snd <$> tx.substate.refunds)
+      gasUsed      = tx.gaslimit - gasRemaining
+      cappedRefund = min (quot gasUsed 5) sumRefunds
+      originPay    = (into $ gasRemaining + cappedRefund) * tx.gasprice
+      minerPay     = tx.priorityFee * (into gasUsed)
+
+    modifying (#env % #contracts)
+       (Map.adjust (over #balance (Expr.add (Lit originPay))) tx.origin)
+    modifying (#env % #contracts)
+       (Map.adjust (over #balance (Expr.add (Lit minerPay))) block.coinbase)
+
+  pushGas = do
+    vm <- get
+    push (into vm.state.gas)
+
+  enoughGas cost gasCap = cost <= gasCap
+
+  subGas gasCap cost = gasCap - cost
+
+  toGas = id
+
+  whenSymbolicElse _ a = a
+
+-- Create symbolic VM from concrete VM
+symbolify :: VM Concrete s -> VM Symbolic s
+symbolify vm =
+  vm { result = symbolifyResult <$> vm.result
+     , state  = symbolifyFrameState vm.state
+     , frames = symbolifyFrame <$> vm.frames
+     , burned = ()
+     }
+
+symbolifyFrameState :: FrameState Concrete s -> FrameState Symbolic s
+symbolifyFrameState state = state { gas = () }
+
+symbolifyFrame :: Frame Concrete s -> Frame Symbolic s
+symbolifyFrame frame = frame { state = symbolifyFrameState frame.state }
+
+symbolifyResult :: VMResult Concrete s -> VMResult Symbolic s
+symbolifyResult result =
+  case result of
+    HandleEffect _ -> internalError "shouldn't happen"
+    VMFailure e -> VMFailure e
+    VMSuccess b -> VMSuccess b
+    Unfinished p -> Unfinished p
+
+forceLit :: Expr EWord -> W256
+forceLit (Lit w) = w
+forceLit _ = internalError "concrete vm, shouldn't ever happen"
+
+burn :: VMOps t => Word64 -> EVM t s () -> EVM t s ()
+burn = burn' . toGas
diff --git a/src/EVM/Effects.hs b/src/EVM/Effects.hs
index ee1f033cf..17fe4ebd7 100644
--- a/src/EVM/Effects.hs
+++ b/src/EVM/Effects.hs
@@ -80,12 +80,12 @@ class Monad m => TTY m where
   writeOutput :: Text -> m ()
   writeErr :: Text -> m ()
 
-writeTraceDapp :: App m => DappInfo -> VM RealWorld -> m ()
+writeTraceDapp :: App m => DappInfo -> VM t RealWorld -> m ()
 writeTraceDapp dapp vm = do
   conf <- readConfig
   liftIO $ when conf.dumpTrace $ T.writeFile "VM.trace" (showTraceTree dapp vm)
 
-writeTrace :: App m => VM RealWorld -> m ()
+writeTrace :: App m => VM t RealWorld -> m ()
 writeTrace vm = do
   conf <- readConfig
   liftIO $ when conf.dumpTrace $ writeFile "VM.trace" (show $ traceForest vm)
diff --git a/src/EVM/Exec.hs b/src/EVM/Exec.hs
index ca460ca42..38bd3ff11 100644
--- a/src/EVM/Exec.hs
+++ b/src/EVM/Exec.hs
@@ -14,7 +14,7 @@ import Control.Monad.ST (ST)
 ethrunAddress :: Addr
 ethrunAddress = Addr 0x00a329c0648769a73afac7f9381e08fb43dbea72
 
-vmForEthrunCreation :: ByteString -> ST s (VM s)
+vmForEthrunCreation :: VMOps t => ByteString -> ST s (VM t s)
 vmForEthrunCreation creationCode =
   (makeVm $ VMOpts
     { contract = initialContract (InitCode creationCode mempty)
@@ -31,7 +31,7 @@ vmForEthrunCreation creationCode =
     , blockGaslimit = 0
     , gasprice = 0
     , prevRandao = 42069
-    , gas = 0xffffffffffffffff
+    , gas = toGas 0xffffffffffffffff
     , gaslimit = 0xffffffffffffffff
     , baseFee = 0
     , priorityFee = 0
@@ -41,25 +41,24 @@ vmForEthrunCreation creationCode =
     , create = False
     , txAccessList = mempty
     , allowFFI = False
-    , symbolic = False
     }) <&> set (#env % #contracts % at (LitAddr ethrunAddress))
              (Just (initialContract (RuntimeCode (ConcreteRuntimeCode ""))))
 
-exec :: EVM s (VMResult s)
+exec :: VMOps t => EVM t s (VMResult t s)
 exec = do
   vm <- get
   case vm.result of
     Nothing -> exec1 >> exec
     Just r -> pure r
 
-run :: EVM s (VM s)
+run :: VMOps t => EVM t s (VM t s)
 run = do
   vm <- get
   case vm.result of
     Nothing -> exec1 >> run
     Just _ -> pure vm
 
-execWhile :: (VM s -> Bool) -> State (VM s) Int
+execWhile :: (VM t s -> Bool) -> State (VM t s) Int
 execWhile p = go 0
   where
     go i = do
diff --git a/src/EVM/Fetch.hs b/src/EVM/Fetch.hs
index a3acc2ff7..399be9cfe 100644
--- a/src/EVM/Fetch.hs
+++ b/src/EVM/Fetch.hs
@@ -184,18 +184,18 @@ fetchChainIdFrom url = do
   sess <- Session.newAPISession
   fetchQuery Latest (fetchWithSession url sess) QueryChainId
 
-http :: Natural -> Maybe Natural -> BlockNumber -> Text -> Fetcher m s
+http :: Natural -> Maybe Natural -> BlockNumber -> Text -> Fetcher t m s
 http smtjobs smttimeout n url q =
   withSolvers Z3 smtjobs smttimeout $ \s ->
     oracle s (Just (n, url)) q
 
-zero :: Natural -> Maybe Natural -> Fetcher m s
+zero :: Natural -> Maybe Natural -> Fetcher t m s
 zero smtjobs smttimeout q =
   withSolvers Z3 smtjobs smttimeout $ \s ->
     oracle s Nothing q
 
 -- smtsolving + (http or zero)
-oracle :: SolverGroup -> RpcInfo -> Fetcher m s
+oracle :: SolverGroup -> RpcInfo -> Fetcher t m s
 oracle solvers info q = do
   case q of
     PleaseDoFFI vals continue -> case vals of
@@ -231,7 +231,7 @@ oracle solvers info q = do
            Nothing ->
              internalError $ "oracle error: " ++ show q
 
-type Fetcher m s = App m => Query s -> m (EVM s ())
+type Fetcher t m s = App m => Query t s -> m (EVM t s ())
 
 -- | Checks which branches are satisfiable, checking the pathconditions for consistency
 -- if the third argument is true.
diff --git a/src/EVM/Format.hs b/src/EVM/Format.hs
index 468db4423..9afc2a272 100644
--- a/src/EVM/Format.hs
+++ b/src/EVM/Format.hs
@@ -191,7 +191,7 @@ formatSBinary (ConcreteBuf bs) = formatBinary bs
 formatSBinary (AbstractBuf t) = "<" <> t <> " abstract buf>"
 formatSBinary _ = internalError "formatSBinary: implement me"
 
-showTraceTree :: DappInfo -> VM s -> Text
+showTraceTree :: DappInfo -> VM t s -> Text
 showTraceTree dapp vm =
   let forest = traceForest vm
       traces = fmap (fmap (unpack . showTrace dapp (vm.env.contracts))) forest
diff --git a/src/EVM/SMT.hs b/src/EVM/SMT.hs
index e6a602c81..d44847903 100644
--- a/src/EVM/SMT.hs
+++ b/src/EVM/SMT.hs
@@ -160,11 +160,11 @@ declareIntermediates bufs stores =
   where
     compareFst (l, _) (r, _) = compare l r
     encodeBuf n expr =
-      SMT2 ["(define-const buf" <> (fromString . show $ n) <> " Buf " <> exprToSMT expr <> ")\n"]  mempty mempty mempty <> encodeBufLen n expr
+      SMT2 ["(define-fun buf" <> (fromString . show $ n) <> "() Buf " <> exprToSMT expr <> ")\n"]  mempty mempty mempty <> encodeBufLen n expr
     encodeBufLen n expr =
-      SMT2 ["(define-const buf" <> (fromString . show $ n) <>"_length" <> " (_ BitVec 256) " <> exprToSMT (bufLengthEnv bufs True expr) <> ")"] mempty mempty mempty
+      SMT2 ["(define-fun buf" <> (fromString . show $ n) <>"_length () (_ BitVec 256) " <> exprToSMT (bufLengthEnv bufs True expr) <> ")"] mempty mempty mempty
     encodeStore n expr =
-      SMT2 ["(define-const store" <> (fromString . show $ n) <> " Storage " <> exprToSMT expr <> ")"] mempty mempty mempty
+      SMT2 ["(define-fun store" <> (fromString . show $ n) <> " () Storage " <> exprToSMT expr <> ")"] mempty mempty mempty
 
 data AbstState = AbstState
   { words :: Map (Expr EWord) Int
diff --git a/src/EVM/Solvers.hs b/src/EVM/Solvers.hs
index 4c8aa260d..1f6aff7c6 100644
--- a/src/EVM/Solvers.hs
+++ b/src/EVM/Solvers.hs
@@ -22,7 +22,7 @@ import Data.Text.Lazy (Text)
 import Data.Text.Lazy qualified as T
 import Data.Text.Lazy.IO qualified as T
 import Data.Text.Lazy.Builder
-import System.Process (createProcess, cleanupProcess, proc, ProcessHandle, std_in, std_out, std_err, StdStream(..))
+import System.Process (createProcess, cleanupProcess, proc, ProcessHandle, std_in, std_out, std_err, StdStream(..), createPipe)
 import Witch (into)
 import EVM.Effects
 import EVM.Fuzz (tryCexFuzz)
@@ -49,7 +49,6 @@ data SolverInstance = SolverInstance
   { solvertype :: Solver
   , stdin      :: Handle
   , stdout     :: Handle
-  , stderr     :: Handle
   , process    :: ProcessHandle
   }
 
@@ -221,7 +220,7 @@ getModel inst cexvars = do
     shrinkBuf buf hint = do
       let encBound = "(_ bv" <> (T.pack $ show (into hint :: Integer)) <> " 256)"
       sat <- liftIO $ do
-        checkCommand inst "(push)"
+        checkCommand inst "(push 1)"
         checkCommand inst $ "(assert (bvule " <> buf <> "_length " <> encBound <> "))"
         sendLine inst "(check-sat)"
       case sat of
@@ -229,7 +228,7 @@ getModel inst cexvars = do
           model <- liftIO getRaw
           put model
         "unsat" -> do
-          liftIO $ checkCommand inst "(pop)"
+          liftIO $ checkCommand inst "(pop 1)"
           shrinkBuf buf (if hint == 0 then hint + 1 else hint * 2)
         e -> internalError $ "Unexpected solver output: " <> (T.unpack e)
 
@@ -257,7 +256,12 @@ mkTimeout t = T.pack $ show $ (1000 *)$ case t of
 -- | Arguments used when spawing a solver instance
 solverArgs :: Solver -> Maybe Natural -> [Text]
 solverArgs solver timeout = case solver of
-  Bitwuzla -> internalError "TODO: Bitwuzla args"
+  Bitwuzla ->
+    [ "--lang=smt2"
+    , "--produce-models"
+    , "--time-limit-per=" <> mkTimeout timeout
+    , "--bv-solver=preprop"
+    ]
   Z3 ->
     [ "-in" ]
   CVC5 ->
@@ -272,21 +276,31 @@ solverArgs solver timeout = case solver of
 -- | Spawns a solver instance, and sets the various global config options that we use for our queries
 spawnSolver :: Solver -> Maybe (Natural) -> IO SolverInstance
 spawnSolver solver timeout = do
-  let cmd = (proc (show solver) (fmap T.unpack $ solverArgs solver timeout)) { std_in = CreatePipe, std_out = CreatePipe, std_err = CreatePipe }
-  (Just stdin, Just stdout, Just stderr, process) <- createProcess cmd
+  (readout, writeout) <- createPipe
+  let cmd
+        = (proc (show solver) (fmap T.unpack $ solverArgs solver timeout))
+            { std_in = CreatePipe
+            , std_out = UseHandle writeout
+            , std_err = UseHandle writeout
+            }
+  (Just stdin, Nothing, Nothing, process) <- createProcess cmd
   hSetBuffering stdin (BlockBuffering (Just 1000000))
-  let solverInstance = SolverInstance solver stdin stdout stderr process
+  let solverInstance = SolverInstance solver stdin readout process
 
   case solver of
     CVC5 -> pure solverInstance
-    _ -> do
+    Bitwuzla -> do
+      _ <- sendLine solverInstance "(set-option :print-success true)"
+      pure solverInstance
+    Z3 -> do
       _ <- sendLine' solverInstance $ "(set-option :timeout " <> mkTimeout timeout <> ")"
       _ <- sendLine solverInstance "(set-option :print-success true)"
       pure solverInstance
+    Custom _ -> pure solverInstance
 
 -- | Cleanly shutdown a running solver instnace
 stopSolver :: SolverInstance -> IO ()
-stopSolver (SolverInstance _ stdin stdout stderr process) = cleanupProcess (Just stdin, Just stdout, Just stderr, process)
+stopSolver (SolverInstance _ stdin stdout process) = cleanupProcess (Just stdin, Just stdout, Nothing, process)
 
 -- | Sends a list of commands to the solver. Returns the first error, if there was one.
 sendScript :: SolverInstance -> SMT2 -> IO (Either Text ())
@@ -320,20 +334,20 @@ sendCommand inst cmd = do
 
 -- | Sends a string to the solver and appends a newline, returns the first available line from the output buffer
 sendLine :: SolverInstance -> Text -> IO Text
-sendLine (SolverInstance _ stdin stdout _ _) cmd = do
+sendLine (SolverInstance _ stdin stdout _) cmd = do
   T.hPutStr stdin (T.append cmd "\n")
   hFlush stdin
   T.hGetLine stdout
 
 -- | Sends a string to the solver and appends a newline, doesn't return stdout
 sendLine' :: SolverInstance -> Text -> IO ()
-sendLine' (SolverInstance _ stdin _ _ _) cmd = do
+sendLine' (SolverInstance _ stdin _ _) cmd = do
   T.hPutStr stdin (T.append cmd "\n")
   hFlush stdin
 
 -- | Returns a string representation of the model for the requested variable
 getValue :: SolverInstance -> Text -> IO Text
-getValue (SolverInstance _ stdin stdout _ _) var = do
+getValue (SolverInstance _ stdin stdout _) var = do
   T.hPutStr stdin (T.append (T.append "(get-value (" var) "))\n")
   hFlush stdin
   fmap (T.unlines . reverse) (readSExpr stdout)
diff --git a/src/EVM/Stepper.hs b/src/EVM/Stepper.hs
index 1f240af84..dc424c63d 100644
--- a/src/EVM/Stepper.hs
+++ b/src/EVM/Stepper.hs
@@ -37,48 +37,48 @@ import EVM.Effects
 import EVM.Expr (concKeccakSimpExpr)
 
 -- | The instruction type of the operational monad
-data Action s a where
+data Action t s a where
 
   -- | Keep executing until an intermediate result is reached
-  Exec :: Action s (VMResult s)
+  Exec :: Action t s (VMResult t s)
 
   -- | Wait for a query to be resolved
-  Wait :: Query s -> Action s ()
+  Wait :: Query t s -> Action t s ()
 
   -- | Multiple things can happen
-  Ask :: Choose s -> Action s ()
+  Ask :: Choose t s -> Action t s ()
 
   -- | Embed a VM state transformation
-  EVM  :: EVM s a -> Action s a
+  EVM  :: EVM t s a -> Action t s a
 
   -- | Perform an IO action
-  IOAct :: IO a -> Action s a
+  IOAct :: IO a -> Action t s a
 
 -- | Type alias for an operational monad of @Action@
-type Stepper s a = Program (Action s) a
+type Stepper t s a = Program (Action t s) a
 
 -- Singleton actions
 
-exec :: Stepper s (VMResult s)
+exec :: Stepper t s (VMResult t s)
 exec = singleton Exec
 
-run :: Stepper s (VM s)
+run :: Stepper t s (VM t s)
 run = exec >> evm get
 
-wait :: Query s -> Stepper s ()
+wait :: Query t s -> Stepper t s ()
 wait = singleton . Wait
 
-ask :: Choose s -> Stepper s ()
+ask :: Choose t s -> Stepper t s ()
 ask = singleton . Ask
 
-evm :: EVM s a -> Stepper s a
+evm :: EVM t s a -> Stepper t s a
 evm = singleton . EVM
 
-evmIO :: IO a -> Stepper s a
+evmIO :: IO a -> Stepper t s a
 evmIO = singleton . IOAct
 
 -- | Run the VM until final result, resolving all queries
-execFully :: Stepper s (Either EvmError (Expr Buf))
+execFully :: Stepper t s (Either EvmError (Expr Buf))
 execFully =
   exec >>= \case
     HandleEffect (Query q) ->
@@ -93,7 +93,7 @@ execFully =
       -> internalError $ "partial execution encountered during concrete execution: " <> show x
 
 -- | Run the VM until its final state
-runFully :: Stepper s (VM s)
+runFully :: Stepper t s (VM t s)
 runFully = do
   vm <- run
   case vm.result of
@@ -105,13 +105,18 @@ runFully = do
     Just _ ->
       pure vm
 
-enter :: Text -> Stepper s ()
+enter :: Text -> Stepper t s ()
 enter t = evm (EVM.pushTrace (EntryTrace t))
 
-interpret :: forall m a . (App m) => Fetch.Fetcher m RealWorld -> VM RealWorld -> Stepper RealWorld a -> m a
+interpret
+  :: forall m a . (App m)
+  => Fetch.Fetcher Concrete m RealWorld
+  -> VM Concrete RealWorld
+  -> Stepper Concrete RealWorld a
+  -> m a
 interpret fetcher vm = eval . view
   where
-    eval :: ProgramView (Action RealWorld) a -> m a
+    eval :: ProgramView (Action Concrete RealWorld) a -> m a
     eval (Return x) = pure x
     eval (action :>>= k) =
       case action of
diff --git a/src/EVM/SymExec.hs b/src/EVM/SymExec.hs
index 7ea06cb55..1a5342218 100644
--- a/src/EVM/SymExec.hs
+++ b/src/EVM/SymExec.hs
@@ -194,7 +194,7 @@ abstractVM
   -> ByteString
   -> Maybe (Precondition s)
   -> Bool
-  -> ST s (VM s)
+  -> ST s (VM Symbolic s)
 abstractVM cd contractCode maybepre create = do
   let value = TxValue
   let code = if create then InitCode contractCode (fst cd) else RuntimeCode (ConcreteRuntimeCode contractCode)
@@ -209,7 +209,7 @@ loadSymVM
   -> Expr EWord
   -> (Expr Buf, [Prop])
   -> Bool
-  -> ST s (VM s)
+  -> ST s (VM Symbolic s)
 loadSymVM x callvalue cd create =
   (makeVm $ VMOpts
     { contract = if create then initialContract x else abstractContract x (SymAddr "entrypoint")
@@ -226,7 +226,7 @@ loadSymVM x callvalue cd create =
     , blockGaslimit = 0
     , gasprice = 0
     , prevRandao = 42069
-    , gas = 0xffffffffffffffff
+    , gas = ()
     , gaslimit = 0xffffffffffffffff
     , baseFee = 0
     , priorityFee = 0
@@ -236,25 +236,24 @@ loadSymVM x callvalue cd create =
     , create = create
     , txAccessList = mempty
     , allowFFI = False
-    , symbolic = True
     })
 
 -- | Interpreter which explores all paths at branching points. Returns an
 -- 'Expr End' representing the possible executions.
 interpret
   :: forall m . App m
-  =>  Fetch.Fetcher m RealWorld
+  => Fetch.Fetcher Symbolic m RealWorld
   -> Maybe Integer -- max iterations
   -> Integer -- ask smt iterations
   -> LoopHeuristic
-  -> VM RealWorld
-  -> Stepper RealWorld (Expr End)
+  -> VM Symbolic RealWorld
+  -> Stepper Symbolic RealWorld (Expr End)
   -> m (Expr End)
 interpret fetcher maxIter askSmtIters heuristic vm =
   eval . Operational.view
   where
   eval
-    :: Operational.ProgramView (Stepper.Action RealWorld) (Expr End)
+    :: Operational.ProgramView (Stepper.Action Symbolic RealWorld) (Expr End)
     -> m (Expr End)
 
   eval (Operational.Return x) = pure x
@@ -328,7 +327,7 @@ interpret fetcher maxIter askSmtIters heuristic vm =
         (r, vm') <- liftIO $ stToIO $ runStateT m vm
         interpret fetcher maxIter askSmtIters heuristic vm' (k r)
 
-maxIterationsReached :: VM s -> Maybe Integer -> Maybe Bool
+maxIterationsReached :: VM Symbolic s -> Maybe Integer -> Maybe Bool
 maxIterationsReached _ Nothing = Nothing
 maxIterationsReached vm (Just maxIter) =
   let codelocation = getCodeLocation vm
@@ -337,7 +336,7 @@ maxIterationsReached vm (Just maxIter) =
      then Map.lookup (codelocation, iters - 1) vm.cache.path
      else Nothing
 
-askSmtItersReached :: VM s -> Integer -> Bool
+askSmtItersReached :: VM Symbolic s -> Integer -> Bool
 askSmtItersReached vm askSmtIters = let
     codelocation = getCodeLocation vm
     (iters, _) = view (at codelocation % non (0, [])) vm.iterations
@@ -351,7 +350,7 @@ askSmtItersReached vm askSmtIters = let
 
  This heuristic is not perfect, and can certainly be tricked, but should generally be good enough for most compiler generated and non pathological user generated loops.
  -}
-isLoopHead :: LoopHeuristic -> VM s -> Maybe Bool
+isLoopHead :: LoopHeuristic -> VM Symbolic s -> Maybe Bool
 isLoopHead Naive _ = Just True
 isLoopHead StackBased vm = let
     loc = getCodeLocation vm
@@ -362,8 +361,8 @@ isLoopHead StackBased vm = let
        Just (_, oldStack) -> Just $ filter isValid oldStack == filter isValid vm.state.stack
        Nothing -> Nothing
 
-type Precondition s = VM s -> Prop
-type Postcondition s = VM s -> Expr End -> Prop
+type Precondition s = VM Symbolic s -> Prop
+type Postcondition s = VM Symbolic s -> Expr End -> Prop
 
 checkAssert
   :: App m
@@ -455,7 +454,7 @@ verifyContract solvers theCode signature' concreteArgs opts maybepre maybepost =
   verify solvers opts preState maybepost
 
 -- | Stepper that parses the result of Stepper.runFully into an Expr End
-runExpr :: Stepper.Stepper RealWorld (Expr End)
+runExpr :: Stepper.Stepper Symbolic RealWorld (Expr End)
 runExpr = do
   vm <- Stepper.runFully
   let traces = Traces (Zipper.toForest vm.traces) vm.env.contracts
@@ -549,7 +548,7 @@ verify
   :: App m
   => SolverGroup
   -> VeriOpts
-  -> VM RealWorld
+  -> VM Symbolic RealWorld
   -> Maybe (Postcondition RealWorld)
   -> m (Expr End, [VerifyResult])
 verify solvers opts preState maybepost = do
@@ -603,7 +602,7 @@ verify solvers opts preState maybepost = do
       Unsat -> Qed ()
       Error e -> internalError $ "solver responded with error: " <> show e
 
-expandCex :: VM s -> SMTCex -> SMTCex
+expandCex :: VM Symbolic s -> SMTCex -> SMTCex
 expandCex prestate c = c { store = Map.union c.store concretePreStore }
   where
     concretePreStore = Map.mapMaybe (maybeConcreteStore . (.storage))
diff --git a/src/EVM/Transaction.hs b/src/EVM/Transaction.hs
index c962e2546..339931803 100644
--- a/src/EVM/Transaction.hs
+++ b/src/EVM/Transaction.hs
@@ -246,7 +246,7 @@ setupTx origin coinbase gasPrice gasLimit prestate =
 -- | Given a valid tx loaded into the vm state,
 -- subtract gas payment from the origin, increment the nonce
 -- and pay receiving address
-initTx :: VM s -> VM s
+initTx :: VM t s -> VM t s
 initTx vm = let
     toAddr   = vm.state.contract
     origin   = vm.tx.origin
diff --git a/src/EVM/Traversals.hs b/src/EVM/Traversals.hs
index 3535a7ee3..66bb1afa3 100644
--- a/src/EVM/Traversals.hs
+++ b/src/EVM/Traversals.hs
@@ -164,7 +164,7 @@ foldExpr f acc expr = acc <> (go expr)
 
       -- frame context
 
-      e@(Gas _ _) -> f e
+      e@(Gas _) -> f e
       e@(Balance {}) -> f e
 
       -- code
@@ -487,7 +487,7 @@ mapExprM f expr = case expr of
 
   -- frame context
 
-  Gas a b -> f (Gas a b)
+  Gas a -> f (Gas a)
   Balance a -> do
     a' <- mapExprM f a
     f (Balance a')
diff --git a/src/EVM/Types.hs b/src/EVM/Types.hs
index f113b4197..ebd017f01 100644
--- a/src/EVM/Types.hs
+++ b/src/EVM/Types.hs
@@ -4,6 +4,7 @@
 {-# LANGUAGE UndecidableInstances #-}
 
 {-# OPTIONS_GHC -Wno-inline-rule-shadowing #-}
+{-# LANGUAGE TypeFamilyDependencies #-}
 
 module EVM.Types where
 
@@ -284,7 +285,6 @@ data Expr (a :: EType) where
   Balance        :: Expr EAddr -> Expr EWord
 
   Gas            :: Int                -- frame idx
-                 -> Int                -- PC
                  -> Expr EWord
 
   -- code
@@ -530,7 +530,7 @@ data EvmError
   | InvalidMemoryAccess
   | CallDepthLimitReached
   | MaxCodeSizeExceeded W256 W256
-  | MaxInitCodeSizeExceeded W256 W256
+  | MaxInitCodeSizeExceeded W256 (Expr EWord)
   | InvalidFormat
   | PrecompileFailure
   | ReturnDataOutOfBounds
@@ -546,27 +546,27 @@ data PartialExec
   deriving (Show, Eq, Ord)
 
 -- | Effect types used by the vm implementation for side effects & control flow
-data Effect s
-  = Query (Query s)
-  | Choose (Choose s)
-deriving instance Show (Effect s)
+data Effect t s
+  = Query (Query t s)
+  | Choose (Choose t s)
+deriving instance Show (Effect t s)
 
 -- | Queries halt execution until resolved through RPC calls or SMT queries
-data Query s where
-  PleaseFetchContract :: Addr -> BaseState -> (Contract -> EVM s ()) -> Query s
-  PleaseFetchSlot     :: Addr -> W256 -> (W256 -> EVM s ()) -> Query s
-  PleaseAskSMT        :: Expr EWord -> [Prop] -> (BranchCondition -> EVM s ()) -> Query s
-  PleaseDoFFI         :: [String] -> (ByteString -> EVM s ()) -> Query s
+data Query t s where
+  PleaseFetchContract :: Addr -> BaseState -> (Contract -> EVM t s ()) -> Query t s
+  PleaseFetchSlot     :: Addr -> W256 -> (W256 -> EVM t s ()) -> Query t s
+  PleaseAskSMT        :: Expr EWord -> [Prop] -> (BranchCondition -> EVM t s ()) -> Query t s
+  PleaseDoFFI         :: [String] -> (ByteString -> EVM t s ()) -> Query t s
 
 -- | Execution could proceed down one of two branches
-data Choose s where
-  PleaseChoosePath    :: Expr EWord -> (Bool -> EVM s ()) -> Choose s
+data Choose t s where
+  PleaseChoosePath    :: Expr EWord -> (Bool -> EVM t s ()) -> Choose t s
 
 -- | The possible return values of a SMT query
 data BranchCondition = Case Bool | Unknown
   deriving Show
 
-instance Show (Query s) where
+instance Show (Query t s) where
   showsPrec _ = \case
     PleaseFetchContract addr base _ ->
       (("<EVM.Query: fetch contract " ++ show addr ++ show base ++ ">") ++)
@@ -581,46 +581,53 @@ instance Show (Query s) where
     PleaseDoFFI cmd _ ->
       (("<EVM.Query: do ffi: " ++ (show cmd)) ++)
 
-instance Show (Choose s) where
+instance Show (Choose t s) where
   showsPrec _ = \case
     PleaseChoosePath _ _ ->
       (("<EVM.Choice: waiting for user to select path (0,1)") ++)
 
 -- | The possible result states of a VM
-data VMResult s
+data VMResult t s
   = VMFailure EvmError      -- ^ An operation failed
   | VMSuccess (Expr Buf)    -- ^ Reached STOP, RETURN, or end-of-code
-  | HandleEffect (Effect s) -- ^ An effect must be handled for execution to continue
+  | HandleEffect (Effect t s) -- ^ An effect must be handled for execution to continue
   | Unfinished PartialExec  -- ^ Execution could not continue further
 
-deriving instance Show (VMResult s)
+deriving instance Show (VMResult t s)
 
 
 -- VM State ----------------------------------------------------------------------------------------
 
+data VMType = Symbolic | Concrete
+
+type family Gas (t :: VMType) = r | r -> t where
+  Gas Symbolic = ()
+  Gas Concrete = Word64
 
 -- | The state of a stepwise EVM execution
-data VM s = VM
-  { result         :: Maybe (VMResult s)
-  , state          :: FrameState s
-  , frames         :: [Frame s]
+data VM (t :: VMType) s = VM
+  { result         :: Maybe (VMResult t s)
+  , state          :: FrameState t s
+  , frames         :: [Frame t s]
   , env            :: Env
   , block          :: Block
   , tx             :: TxState
   , logs           :: [Expr Log]
   , traces         :: Zipper.TreePos Zipper.Empty Trace
   , cache          :: Cache
-  , burned         :: {-# UNPACK #-} !Word64
+  , burned         :: !(Gas t)
   , iterations     :: Map CodeLocation (Int, [Expr EWord])
   -- ^ how many times we've visited a loc, and what the contents of the stack were when we were there last
   , constraints    :: [Prop]
   , config         :: RuntimeConfig
-  , symbolic       :: Bool
   }
-  deriving (Show, Generic)
+  deriving (Generic)
+
+deriving instance Show (VM Symbolic s)
+deriving instance Show (VM Concrete s)
 
 -- | Alias for the type of e.g. @exec1@.
-type EVM s a = StateT (VM s) (ST s) a
+type EVM (t :: VMType) s a = StateT (VM t s) (ST s) a
 
 -- | The VM base state (i.e. should new contracts be created with abstract balance / storage?)
 data BaseState
@@ -637,11 +644,13 @@ data RuntimeConfig = RuntimeConfig
   deriving (Show)
 
 -- | An entry in the VM's "call/create stack"
-data Frame s = Frame
+data Frame (t :: VMType) s = Frame
   { context :: FrameContext
-  , state   :: FrameState s
+  , state   :: FrameState t s
   }
-  deriving (Show)
+
+deriving instance Show (Frame Symbolic s)
+deriving instance Show (Frame Concrete s)
 
 -- | Call/create info
 data FrameContext
@@ -654,8 +663,8 @@ data FrameContext
   | CallContext
     { target        :: Expr EAddr
     , context       :: Expr EAddr
-    , offset        :: W256
-    , size          :: W256
+    , offset        :: Expr EWord
+    , size          :: Expr EWord
     , codehash      :: Expr EWord
     , abi           :: Maybe W256
     , calldata      :: Expr Buf
@@ -676,7 +685,7 @@ data SubState = SubState
   deriving (Eq, Ord, Show)
 
 -- | The "registers" of the VM along with memory and data stack
-data FrameState s = FrameState
+data FrameState (t :: VMType) s = FrameState
   { contract     :: Expr EAddr
   , codeContract :: Expr EAddr
   , code         :: ContractCode
@@ -687,11 +696,14 @@ data FrameState s = FrameState
   , calldata     :: Expr Buf
   , callvalue    :: Expr EWord
   , caller       :: Expr EAddr
-  , gas          :: {-# UNPACK #-} !Word64
+  , gas          :: !(Gas t)
   , returndata   :: Expr Buf
   , static       :: Bool
   }
-  deriving (Show, Generic)
+  deriving (Generic)
+
+deriving instance Show (FrameState Symbolic s)
+deriving instance Show (FrameState Concrete s)
 
 data Memory s
   = ConcreteMemory (MutableMemory s)
@@ -722,6 +734,7 @@ data Env = Env
   { contracts      :: Map (Expr EAddr) Contract
   , chainId        :: W256
   , freshAddresses :: Int
+  , freshGasVals :: Int
   }
   deriving (Show, Generic)
 
@@ -751,6 +764,37 @@ data Contract = Contract
   }
   deriving (Show, Eq, Ord)
 
+class VMOps (t :: VMType) where
+  burn' :: Gas t -> EVM t s () -> EVM t s ()
+  -- TODO: change to EvmWord t
+  burnExp :: Expr EWord -> EVM t s () -> EVM t s ()
+  burnSha3 :: Expr EWord -> EVM t s () -> EVM t s ()
+  burnCalldatacopy :: Expr EWord -> EVM t s () -> EVM t s ()
+  burnCodecopy :: Expr EWord -> EVM t s () -> EVM t s ()
+  burnExtcodecopy :: Expr EAddr -> Expr EWord -> EVM t s () -> EVM t s ()
+  burnReturndatacopy :: Expr EWord -> EVM t s () -> EVM t s ()
+  burnLog :: Expr EWord -> Word8 -> EVM t s () -> EVM t s ()
+
+  initialGas :: Gas t
+  ensureGas :: Word64 -> EVM t s () -> EVM t s ()
+  -- TODO: change to EvmWord t
+  gasTryFrom :: Expr EWord -> Either () (Gas t)
+
+  -- Gas cost of create, including hash cost if needed
+  costOfCreate :: FeeSchedule Word64 -> Gas t -> Expr EWord -> Bool -> (Gas t, Gas t)
+
+  costOfCall
+    :: FeeSchedule Word64 -> Bool -> Expr EWord -> Gas t -> Gas t -> Expr EAddr
+    -> (Word64 -> Word64 -> EVM t s ()) -> EVM t s ()
+
+  reclaimRemainingGasAllowance :: VM t s -> EVM t s ()
+  payRefunds :: EVM t s ()
+  pushGas :: EVM t s ()
+  enoughGas :: Word64 -> Gas t -> Bool
+  subGas :: Gas t -> Word64 -> Gas t
+  toGas :: Word64 -> Gas t
+
+  whenSymbolicElse :: EVM t s a -> EVM t s a -> EVM t s a
 
 -- Bytecode Representations ------------------------------------------------------------------------
 
@@ -853,7 +897,7 @@ instance Monoid Traces where
 
 
 -- | A specification for an initial VM state
-data VMOpts = VMOpts
+data VMOpts (t :: VMType) = VMOpts
   { contract :: Contract
   , otherContracts :: [(Expr EAddr, Contract)]
   , calldata :: (Expr Buf, [Prop])
@@ -863,7 +907,7 @@ data VMOpts = VMOpts
   , address :: Expr EAddr
   , caller :: Expr EAddr
   , origin :: Expr EAddr
-  , gas :: Word64
+  , gas :: Gas t
   , gaslimit :: Word64
   , number :: W256
   , timestamp :: Expr EWord
@@ -878,8 +922,10 @@ data VMOpts = VMOpts
   , create :: Bool
   , txAccessList :: Map (Expr EAddr) [W256]
   , allowFFI :: Bool
-  , symbolic :: Bool
-  } deriving Show
+  }
+
+deriving instance Show (VMOpts Symbolic)
+deriving instance Show (VMOpts Concrete)
 
 
 -- Opcodes -----------------------------------------------------------------------------------------
diff --git a/src/EVM/UnitTest.hs b/src/EVM/UnitTest.hs
index 10519901a..a4ef2f3b0 100644
--- a/src/EVM/UnitTest.hs
+++ b/src/EVM/UnitTest.hs
@@ -110,7 +110,7 @@ unitTest opts (Contracts cs) = do
 
 -- | Assuming a constructor is loaded, this stepper will run the constructor
 -- to create the test contract, give it an initial balance, and run `setUp()'.
-initializeUnitTest :: UnitTestOptions s -> SolcContract -> Stepper s ()
+initializeUnitTest :: VMOps t => UnitTestOptions s -> SolcContract -> Stepper t s ()
 initializeUnitTest opts theContract = do
 
   let addr = opts.testParams.address
@@ -161,7 +161,7 @@ runUnitTestContract
 
     Just theContract -> do
       -- Construct the initial VM and begin the contract's constructor
-      vm0 <- liftIO $ stToIO $ initialUnitTestVm opts theContract
+      vm0 :: VM Concrete RealWorld <- liftIO $ stToIO $ initialUnitTestVm opts theContract
       vm1 <- Stepper.interpret (Fetch.oracle solvers rpcInfo) vm0 $ do
         Stepper.enter name
         initializeUnitTest opts theContract
@@ -192,9 +192,8 @@ runUnitTestContract
           pure $ fmap isRight details
         _ -> internalError "setUp() did not end with a result"
 
-
 -- | Define the thread spawner for symbolic tests
-symRun :: App m => UnitTestOptions RealWorld -> VM RealWorld -> Sig -> m (Text, Either Text Text)
+symRun :: App m => UnitTestOptions RealWorld -> VM Concrete RealWorld -> Sig -> m (Text, Either Text Text)
 symRun opts@UnitTestOptions{..} vm (Sig testName types) = do
     let cd = symCalldata testName types [] (AbstractBuf "txdata")
         shouldFail = "proveFail" `isPrefixOf` testName
@@ -229,7 +228,7 @@ symRun opts@UnitTestOptions{..} vm (Sig testName types) = do
     writeTraceDapp dapp vm'
 
     -- check postconditions against vm
-    (e, results) <- verify solvers (makeVeriOpts opts) vm' (Just postcondition)
+    (e, results) <- verify solvers (makeVeriOpts opts) (symbolify vm') (Just postcondition)
     let allReverts = not . (any Expr.isSuccess) . flattenExpr $ e
 
     -- display results
@@ -281,7 +280,7 @@ symFailure UnitTestOptions {..} testName cd types failures' =
             _ -> ""
         ]
 
-execSymTest :: UnitTestOptions RealWorld -> ABIMethod -> (Expr Buf, [Prop]) -> Stepper RealWorld (Expr End)
+execSymTest :: UnitTestOptions RealWorld -> ABIMethod -> (Expr Buf, [Prop]) -> Stepper Symbolic RealWorld (Expr End)
 execSymTest UnitTestOptions{ .. } method cd = do
   -- Set up the call to the test method
   Stepper.evm $ do
@@ -290,7 +289,7 @@ execSymTest UnitTestOptions{ .. } method cd = do
   -- Try running the test method
   runExpr
 
-checkSymFailures :: UnitTestOptions RealWorld -> Stepper RealWorld (VM RealWorld)
+checkSymFailures :: VMOps t => UnitTestOptions RealWorld -> Stepper t RealWorld (VM t RealWorld)
 checkSymFailures UnitTestOptions { .. } = do
   -- Ask whether any assertions failed
   Stepper.evm $ do
@@ -303,7 +302,7 @@ indentLines n s =
   let p = Text.replicate n " "
   in Text.unlines (map (p <>) (Text.lines s))
 
-passOutput :: VM s -> UnitTestOptions s -> Text -> Text
+passOutput :: VM t s -> UnitTestOptions s -> Text -> Text
 passOutput vm UnitTestOptions { .. } testName =
   let ?context = DappContext { info = dapp, env = vm.env.contracts }
   in let v = fromMaybe 0 verbose
@@ -318,7 +317,7 @@ passOutput vm UnitTestOptions { .. } testName =
       ]
     else ""
 
-failOutput :: VM s -> UnitTestOptions s -> Text -> Text
+failOutput :: VM t s -> UnitTestOptions s -> Text -> Text
 failOutput vm UnitTestOptions { .. } testName =
   let ?context = DappContext { info = dapp, env = vm.env.contracts }
   in mconcat
@@ -403,14 +402,14 @@ formatTestLog events (LogEntry _ args (topic:_)) =
                   _ -> Nothing
               _ -> Just "<symbolic decimal>"
 
-abiCall :: TestVMParams -> Either (Text, AbiValue) ByteString -> EVM s ()
+abiCall :: VMOps t => TestVMParams -> Either (Text, AbiValue) ByteString -> EVM t s ()
 abiCall params args =
   let cd = case args of
         Left (sig, args') -> abiMethod sig args'
         Right b -> b
   in makeTxCall params (ConcreteBuf cd, [])
 
-makeTxCall :: TestVMParams -> (Expr Buf, [Prop]) -> EVM s ()
+makeTxCall :: VMOps t => TestVMParams -> (Expr Buf, [Prop]) -> EVM t s ()
 makeTxCall params (cd, cdProps) = do
   resetState
   assign (#tx % #isCreate) False
@@ -418,14 +417,14 @@ makeTxCall params (cd, cdProps) = do
   assign (#state % #calldata) cd
   #constraints %= (<> cdProps)
   assign (#state % #caller) params.caller
-  assign (#state % #gas) params.gasCall
+  assign (#state % #gas) (toGas params.gasCall)
   origin <- fromMaybe (initialContract (RuntimeCode (ConcreteRuntimeCode ""))) <$> use (#env % #contracts % at params.origin)
   let insufficientBal = maybe False (\b -> b < params.gasprice * (into params.gasCall)) (maybeLitWord origin.balance)
   when insufficientBal $ internalError "insufficient balance for gas cost"
   vm <- get
   put $ initTx vm
 
-initialUnitTestVm :: UnitTestOptions s -> SolcContract -> ST s (VM s)
+initialUnitTestVm :: VMOps t => UnitTestOptions s -> SolcContract -> ST s (VM t s)
 initialUnitTestVm (UnitTestOptions {..}) theContract = do
   vm <- makeVm $ VMOpts
            { contract = initialContract (InitCode theContract.creationCode mempty)
@@ -435,7 +434,7 @@ initialUnitTestVm (UnitTestOptions {..}) theContract = do
            , address = testParams.address
            , caller = testParams.caller
            , origin = testParams.origin
-           , gas = testParams.gasCreate
+           , gas = toGas testParams.gasCreate
            , gaslimit = testParams.gasCreate
            , coinbase = testParams.coinbase
            , number = testParams.number
@@ -452,7 +451,6 @@ initialUnitTestVm (UnitTestOptions {..}) theContract = do
            , baseState = EmptyBase
            , txAccessList = mempty -- TODO: support unit test access lists???
            , allowFFI = ffiAllowed
-           , symbolic = True
            }
   let creator =
         initialContract (RuntimeCode (ConcreteRuntimeCode ""))
diff --git a/test/EVM/Test/BlockchainTests.hs b/test/EVM/Test/BlockchainTests.hs
index 91c3f9c95..a88115f0f 100644
--- a/test/EVM/Test/BlockchainTests.hs
+++ b/test/EVM/Test/BlockchainTests.hs
@@ -52,7 +52,7 @@ data Block = Block
   } deriving Show
 
 data Case = Case
-  { vmOpts      :: VMOpts
+  { vmOpts      :: VMOpts Concrete
   , checkContracts  :: Map Addr Contract
   , testExpectation :: Map Addr Contract
   } deriving Show
@@ -193,7 +193,7 @@ fromConcrete :: Expr Storage -> Map W256 W256
 fromConcrete (ConcreteStore s) = s
 fromConcrete s = internalError $ "unexpected abstract store: " <> show s
 
-checkStateFail :: Bool -> Case -> VM RealWorld -> (Bool, Bool, Bool, Bool) -> IO String
+checkStateFail :: Bool -> Case -> VM Concrete RealWorld -> (Bool, Bool, Bool, Bool) -> IO String
 checkStateFail diff x vm (okMoney, okNonce, okData, okCode) = do
   let
     printContracts :: Map Addr Contract -> IO ()
@@ -227,7 +227,7 @@ checkStateFail diff x vm (okMoney, okNonce, okData, okCode) = do
 
 checkExpectation
   :: App m
-  => Bool -> Case -> VM RealWorld -> m (Maybe String)
+  => Bool -> Case -> VM Concrete RealWorld -> m (Maybe String)
 checkExpectation diff x vm = do
   let expectation = x.testExpectation
       (okState, b2, b3, b4, b5) = checkExpectedContracts vm expectation
@@ -254,7 +254,7 @@ c1 === c2 =
       (RuntimeCode a', RuntimeCode b') -> a' == b'
       _ -> internalError "unexpected code"
 
-checkExpectedContracts :: VM RealWorld -> Map Addr Contract -> (Bool, Bool, Bool, Bool, Bool)
+checkExpectedContracts :: VM Concrete RealWorld -> Map Addr Contract -> (Bool, Bool, Bool, Bool, Bool)
 checkExpectedContracts vm expected =
   let cs = fmap (clearZeroStorage . clearOrigStorage) $ forceConcreteAddrs vm.env.contracts
   in ( (expected ~= cs)
@@ -413,7 +413,6 @@ fromBlockchainCase' block tx preState postState =
          , create         = isCreate
          , txAccessList   = Map.mapKeys LitAddr (txAccessMap tx)
          , allowFFI       = False
-         , symbolic       = False
          })
         checkState
         postState
@@ -482,7 +481,7 @@ checkTx tx block prestate = do
   else
     pure prestate
 
-vmForCase :: Case -> IO (VM RealWorld)
+vmForCase :: Case -> IO (VM Concrete RealWorld)
 vmForCase x = do
   vm <- stToIO $ makeVm x.vmOpts
     <&> set (#env % #contracts) (Map.mapKeys LitAddr x.checkContracts)
diff --git a/test/EVM/Test/Tracing.hs b/test/EVM/Test/Tracing.hs
index 6b391f2c5..d772484d9 100644
--- a/test/EVM/Test/Tracing.hs
+++ b/test/EVM/Test/Tracing.hs
@@ -46,7 +46,7 @@ import Witch (into, unsafeInto)
 import Optics.Core hiding (pre)
 import Optics.State
 
-import EVM (makeVm, initialContract, exec1)
+import EVM (makeVm, initialContract, exec1, symbolify)
 import EVM.Assembler (assemble)
 import EVM.Expr qualified as Expr
 import EVM.Concrete qualified as Concrete
@@ -413,12 +413,6 @@ deleteTraceOutputFiles evmtoolResult =
       System.Directory.removeFile traceFileName
       System.Directory.removeFile (traceFileName ++ ".json")
 
--- Create symbolic VM from concrete VM
-symbolify :: VM s -> VM s
-symbolify vm = vm { state = vm.state { calldata = AbstractBuf "calldata" }
-                  , symbolic = True
-                  }
-
 -- | Takes a runtime code and calls it with the provided calldata
 --   Uses evmtool's alloc and transaction to set up the VM correctly
 runCodeWithTrace
@@ -437,7 +431,7 @@ runCodeWithTrace rpcinfo evmEnv alloc txn fromAddr toAddress = withSolvers Z3 0
     Left x -> pure $ Left (x, trace)
     Right _ -> pure $ Right (expr, trace, vmres vm)
 
-vmForRuntimeCode :: ByteString -> Expr Buf -> EVMToolEnv -> EVMToolAlloc -> EVM.Transaction.Transaction -> Expr EAddr -> Expr EAddr -> ST s (VM s)
+vmForRuntimeCode :: ByteString -> Expr Buf -> EVMToolEnv -> EVMToolAlloc -> EVM.Transaction.Transaction -> Expr EAddr -> Expr EAddr -> ST s (VM Concrete s)
 vmForRuntimeCode runtimecode calldata' evmToolEnv alloc txn fromAddr toAddress =
   let contract = initialContract (RuntimeCode (ConcreteRuntimeCode runtimecode))
                  & set #balance (Lit alloc.balance)
@@ -466,7 +460,6 @@ vmForRuntimeCode runtimecode calldata' evmToolEnv alloc txn fromAddr toAddress =
     , create = False
     , txAccessList = mempty
     , allowFFI = False
-    , symbolic = False
     }) <&> set (#env % #contracts % at (LitAddr ethrunAddress))
              (Just (initialContract (RuntimeCode (ConcreteRuntimeCode BS.empty))))
        <&> set (#state % #calldata) calldata'
@@ -486,7 +479,7 @@ runCode rpcinfo code' calldata' = withSolvers Z3 0 Nothing $ \solvers -> do
     Left _ -> Nothing
     Right b -> Just b
 
-vmtrace :: VM s -> VMTrace
+vmtrace :: VM Concrete s -> VMTrace
 vmtrace vm =
   let
     memsize = vm.state.memorySize
@@ -501,7 +494,7 @@ vmtrace vm =
              , traceError = readoutError vm.result
              }
   where
-    readoutError :: Maybe (VMResult s) -> Maybe String
+    readoutError :: Maybe (VMResult t s) -> Maybe String
     readoutError (Just (VMFailure e)) = case e of
       -- NOTE: error text made to closely match go-ethereum's errors.go file
       OutOfGas {}             -> Just "out of gas"
@@ -524,7 +517,7 @@ vmtrace vm =
       err                     -> Just $ "HEVM error: " <> show err
     readoutError _ = Nothing
 
-vmres :: VM s -> VMTraceResult
+vmres :: VM Concrete s -> VMTraceResult
 vmres vm =
   let
     gasUsed' = vm.tx.gaslimit - vm.state.gas
@@ -539,14 +532,14 @@ vmres vm =
      , gasUsed = gasUsed'
      }
 
-type TraceState s = (VM s, [VMTrace])
+type TraceState s = (VM Concrete s, [VMTrace])
 
-execWithTrace :: App m => StateT (TraceState RealWorld) m (VMResult RealWorld)
+execWithTrace :: App m => StateT (TraceState RealWorld) m (VMResult Concrete RealWorld)
 execWithTrace = do
   _ <- runWithTrace
   fromJust <$> use (_1 % #result)
 
-runWithTrace :: App m => StateT (TraceState RealWorld) m (VM RealWorld)
+runWithTrace :: App m => StateT (TraceState RealWorld) m (VM Concrete RealWorld)
 runWithTrace = do
   -- This is just like `exec` except for every instruction evaluated,
   -- we also increment a counter indexed by the current code location.
@@ -568,15 +561,15 @@ runWithTrace = do
 
 interpretWithTrace
   :: forall m a . App m
-  => Fetch.Fetcher m RealWorld
-  -> Stepper.Stepper RealWorld a
+  => Fetch.Fetcher Concrete m RealWorld
+  -> Stepper.Stepper Concrete RealWorld a
   -> StateT (TraceState RealWorld) m a
 interpretWithTrace fetcher =
   eval . Operational.view
   where
     eval
       :: App m
-      => Operational.ProgramView (Stepper.Action RealWorld) a
+      => Operational.ProgramView (Stepper.Action Concrete RealWorld) a
       -> StateT (TraceState RealWorld) m a
     eval (Operational.Return x) = pure x
     eval (action Operational.:>>= k) =
@@ -817,7 +810,7 @@ forceLit _ = undefined
 randItem :: [a] -> IO a
 randItem = generate . Test.QuickCheck.elements
 
-getOp :: VM s -> Word8
+getOp :: VM t s -> Word8
 getOp vm =
   let pcpos  = vm ^. #state % #pc
       code' = vm ^. #state % #code
diff --git a/test/rpc.hs b/test/rpc.hs
index 0e04dc444..9624a853e 100644
--- a/test/rpc.hs
+++ b/test/rpc.hs
@@ -11,7 +11,7 @@ import Data.Text (Text)
 import Data.Vector qualified as V
 
 import Optics.Core
-import EVM (makeVm)
+import EVM (makeVm, symbolify)
 import EVM.ABI
 import EVM.Fetch
 import EVM.SMT
@@ -107,13 +107,13 @@ tests = testGroup "rpc"
           postc _ _ = PBool True
         vm <- liftIO $ weth9VM blockNum calldata'
         (_, [Cex (_, model)]) <- withSolvers Z3 1 Nothing $ \solvers ->
-          verify solvers (rpcVeriOpts (BlockNumber blockNum, testRpc)) vm (Just postc)
+          verify solvers (rpcVeriOpts (BlockNumber blockNum, testRpc)) (symbolify vm) (Just postc)
         liftIO $ assertBool "model should exceed caller balance" (getVar model "arg2" >= 695836005599316055372648)
     ]
   ]
 
 -- call into WETH9 from 0xf04a... (a large holder)
-weth9VM :: W256 -> (Expr Buf, [Prop]) -> IO (VM RealWorld)
+weth9VM :: W256 -> (Expr Buf, [Prop]) -> IO (VM Concrete RealWorld)
 weth9VM blockNum calldata' = do
   let
     caller' = LitAddr 0xf04a5cc80b1e94c69b48f5ee68a08cd2f09a7c3e
@@ -121,7 +121,7 @@ weth9VM blockNum calldata' = do
     callvalue' = Lit 0
   vmFromRpc blockNum calldata' callvalue' caller' weth9
 
-vmFromRpc :: W256 -> (Expr Buf, [Prop]) -> Expr EWord -> Expr EAddr -> Addr -> IO (VM RealWorld)
+vmFromRpc :: W256 -> (Expr Buf, [Prop]) -> Expr EWord -> Expr EAddr -> Addr -> IO (VM Concrete RealWorld)
 vmFromRpc blockNum calldata callvalue caller address = do
   ctrct <- fetchContractFrom (BlockNumber blockNum) testRpc address >>= \case
         Nothing -> internalError $ "contract not found: " <> show address
@@ -156,7 +156,6 @@ vmFromRpc blockNum calldata callvalue caller address = do
     , baseState      = EmptyBase
     , txAccessList   = mempty
     , allowFFI       = False
-    , symbolic       = False
     }) <&> set (#cache % #fetched % at address) (Just ctrct)
 
 testRpc :: Text
diff --git a/test/test.hs b/test/test.hs
index 8a63a411e..89bfab753 100644
--- a/test/test.hs
+++ b/test/test.hs
@@ -412,7 +412,7 @@ tests = testGroup "hevm"
         let dummyContract =
               (initialContract (RuntimeCode (ConcreteRuntimeCode mempty)))
                 { external = True }
-        vm <- liftIO $ stToIO $ vmForEthrunCreation ""
+        vm :: VM Concrete RealWorld <- liftIO $ stToIO $ vmForEthrunCreation ""
             -- perform the initial access
         vm1 <- liftIO $ stToIO $ execStateT (EVM.accessStorage (LitAddr 0) (Lit 0) (pure . pure ())) vm
         -- it should fetch the contract first
@@ -942,7 +942,7 @@ tests = testGroup "hevm"
               }
              }
             |]
-        (_, [Cex (_, ctr)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x12] c (Just (Sig "fun(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
+        (_, [Cex (_, ctr)]) <- withSolvers Bitwuzla 1 Nothing $ \s -> checkAssert s [0x12] c (Just (Sig "fun(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
         assertEqualM "Division by 0 needs b=0" (getVar ctr "arg2") 0
         putStrLnM "expected counterexample found"
      ,
@@ -955,7 +955,7 @@ tests = testGroup "hevm"
                }
              }
              |]
-         (_, [Cex _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x1] c Nothing [] defaultVeriOpts
+         (_, [Cex _]) <- withSolvers Bitwuzla 1 Nothing $ \s -> checkAssert s [0x1] c Nothing [] defaultVeriOpts
          putStrLnM "expected counterexample found"
       ,
      test "enum-conversion-fail" $ do
@@ -968,7 +968,7 @@ tests = testGroup "hevm"
               }
              }
             |]
-        (_, [Cex (_, ctr)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x21] c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
+        (_, [Cex (_, ctr)]) <- withSolvers Bitwuzla 1 Nothing $ \s -> checkAssert s [0x21] c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
         assertBoolM "Enum is only defined for 0 and 1" $ (getVar ctr "arg1") > 1
         putStrLnM "expected counterexample found"
      ,
@@ -1137,7 +1137,7 @@ tests = testGroup "hevm"
                 }
             }
           |]
-        withSolvers Z3 1 Nothing $ \s -> do
+        withSolvers Bitwuzla 1 Nothing $ \s -> do
           let calldata = (WriteWord (Lit 0x0) (Var "u") (ConcreteBuf ""), [])
           initVM <- liftIO $ stToIO $ abstractVM calldata initCode Nothing True
           expr <- Expr.simplify <$> interpret (Fetch.oracle s Nothing) Nothing 1 StackBased initVM runExpr
@@ -2782,7 +2782,7 @@ tests = testGroup "hevm"
               }
             |]
 
-          (_, [Qed _]) <- withSolvers CVC5 1 (Just 99999999) $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "distributivity(uint256,uint256,uint256)" [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
+          (_, [Qed _]) <- withSolvers Bitwuzla 1 (Just 99999999) $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "distributivity(uint256,uint256,uint256)" [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts
           putStrLnM "Proven"
         ,
         test "storage-cex-1" $ do
@@ -2937,7 +2937,7 @@ tests = testGroup "hevm"
         }
         |]
       let sig = (Sig "func(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])
-      (_, [Cex (_, ctr1), Cex (_, ctr2)]) <- withSolvers CVC5 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just sig) [] defaultVeriOpts
+      (_, [Cex (_, ctr1), Cex (_, ctr2)]) <- withSolvers Bitwuzla 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just sig) [] defaultVeriOpts
       putStrLnM  $ "expected counterexamples found.  ctr1: " <> (show ctr1) <> " ctr2: " <> (show ctr2)
     , testFuzz "fuzz-simple-fixed-value-store1" $ do
       Just c <- solcRuntime "MyContract"
@@ -3223,7 +3223,7 @@ tests = testGroup "hevm"
                 }
               }
           |]
-        withSolvers Z3 3 Nothing $ \s -> do
+        withSolvers Bitwuzla 3 Nothing $ \s -> do
           a <- equivalenceCheck s aPrgm bPrgm defaultVeriOpts (mkCalldata Nothing [])
           assertEqualM "Must be different" (any isCex a) True
       , test "eq-all-yul-optimization-tests" $ do
@@ -3548,7 +3548,7 @@ runSimpleVM x ins = do
        s -> internalError $ show s
 
 -- | Takes a creation code and returns a vm with the result of executing the creation code
-loadVM :: App m => ByteString -> m (Maybe (VM RealWorld))
+loadVM :: App m => ByteString -> m (Maybe (VM Concrete RealWorld))
 loadVM x = do
   vm <- liftIO $ stToIO $ vmForEthrunCreation x
   vm1 <- Stepper.interpret (Fetch.zero 0 Nothing) vm Stepper.runFully
@@ -3613,7 +3613,7 @@ runStatements stmts args t = do
     }
   |] (abiMethod s (AbiTuple $ V.fromList args))
 
-getStaticAbiArgs :: Int -> VM s -> [Expr EWord]
+getStaticAbiArgs :: Int -> VM Symbolic s -> [Expr EWord]
 getStaticAbiArgs n vm =
   let cd = vm.state.calldata
   in decodeStaticArgs 4 n cd