diff --git a/haskell.nix b/haskell.nix
index 44c2ebb0f..58b707f5a 100644
--- a/haskell.nix
+++ b/haskell.nix
@@ -15,7 +15,7 @@ in self-hs: super-hs:
 
     sbv_prepatch = pkgs.haskell.lib.dontCheck (self-hs.callCabal2nix "sbv" (builtins.fetchGit {
         url = "https://github.com/LeventErkok/sbv/";
-        rev = "91637c043d206530bc64d7eac88d2f80e8db0b85";
+        rev = "fe5f5aff026307a1582cc7eafbbabd26796ef434";
     })    {inherit (pkgs) z3;});
 
   in {
diff --git a/nix/hevm-tests/default.nix b/nix/hevm-tests/default.nix
index e18ff5b33..bb3283b55 100644
--- a/nix/hevm-tests/default.nix
+++ b/nix/hevm-tests/default.nix
@@ -14,6 +14,6 @@ in
   yulEquivalence-cvc4 = runWithSolver ./yul-equivalence.nix "cvc4";
 
   # z3 takes 3hrs to run these tests on a fast machine, and even then ~180 timeout
-  #smtChecker-z3 = runWithSolver ./smt-checker.nix "z3";
+  smtChecker-z3 = runWithSolver ./smt-checker.nix "z3";
   smtChecker-cvc4 = runWithSolver ./smt-checker.nix "cvc4";
 }
diff --git a/nix/hevm-tests/smt-checker.nix b/nix/hevm-tests/smt-checker.nix
index 56edc20d6..67146d262 100644
--- a/nix/hevm-tests/smt-checker.nix
+++ b/nix/hevm-tests/smt-checker.nix
@@ -47,6 +47,35 @@ let
     "types/array_dynamic_3_fail.sol"
   ];
 
+  z3Timeout = [
+    "operators/compound_assignment_division_1.sol"
+    "operators/compound_assignment_division_2.sol"
+    "operators/delete_array_index_2d.sol"
+  ];
+
+  dynamic = [
+    # OpCalldatacopy
+    "loops/for_loop_array_assignment_memory_memory.sol"
+    "loops/for_loop_array_assignment_memory_storage.sol"
+    "loops/while_loop_array_assignment_memory_memory.sol"
+    "loops/while_loop_array_assignment_memory_storage.sol"
+    "types/address_call.sol"
+    "types/address_delegatecall.sol"
+    "types/address_staticcall.sol"
+    "types/array_aliasing_storage_2.sol"
+    "types/array_aliasing_storage_3.sol"
+    "types/array_aliasing_storage_5.sol"
+    "types/array_branch_1d.sol"
+    "types/array_branches_1d.sol"
+    "types/array_dynamic_parameter_1.sol"
+    "types/array_dynamic_parameter_1_fail.sol"
+    "types/bytes_1.sol"
+    "types/bytes_2.sol"
+    "types/bytes_2_fail.sol"
+    "types/mapping_unsupported_key_type_1.sol"
+    "types/function_type_array_as_reference_type.sol"
+  ];
+
   ignored = [
 
     # --- constructor arguments ---
@@ -115,26 +144,26 @@ let
     # OpJump
     "complex/slither/external_function.sol"
 
-    # OpCalldatacopy
-    "loops/for_loop_array_assignment_memory_memory.sol"
-    "loops/for_loop_array_assignment_memory_storage.sol"
-    "loops/while_loop_array_assignment_memory_memory.sol"
-    "loops/while_loop_array_assignment_memory_storage.sol"
-    "types/address_call.sol"
-    "types/address_delegatecall.sol"
-    "types/address_staticcall.sol"
-    "types/array_aliasing_storage_2.sol"
-    "types/array_aliasing_storage_3.sol"
-    "types/array_aliasing_storage_5.sol"
-    "types/array_branch_1d.sol"
-    "types/array_branches_1d.sol"
-    "types/array_dynamic_parameter_1.sol"
-    "types/array_dynamic_parameter_1_fail.sol"
-    "types/bytes_1.sol"
-    "types/bytes_2.sol"
-    "types/bytes_2_fail.sol"
-    "types/mapping_unsupported_key_type_1.sol"
-    "types/function_type_array_as_reference_type.sol"
+    # # OpCalldatacopy
+    # "loops/for_loop_array_assignment_memory_memory.sol"
+    # "loops/for_loop_array_assignment_memory_storage.sol"
+    # "loops/while_loop_array_assignment_memory_memory.sol"
+    # "loops/while_loop_array_assignment_memory_storage.sol"
+    # "types/address_call.sol"
+    # "types/address_delegatecall.sol"
+    # "types/address_staticcall.sol"
+    # "types/array_aliasing_storage_2.sol"
+    # "types/array_aliasing_storage_3.sol"
+    # "types/array_aliasing_storage_5.sol"
+    # "types/array_branch_1d.sol"
+    # "types/array_branches_1d.sol"
+    # "types/array_dynamic_parameter_1.sol"
+    # "types/array_dynamic_parameter_1_fail.sol"
+    # "types/bytes_1.sol"
+    # "types/bytes_2.sol"
+    # "types/bytes_2_fail.sol"
+    # "types/mapping_unsupported_key_type_1.sol"
+    # "types/function_type_array_as_reference_type.sol"
 
     # OpBlockhash
     "special/blockhash.sol"
@@ -223,8 +252,8 @@ let
   # symbolic` on all contracts within.
   # $1 == input file
   # $2 == hevm smt backend
+  # $3 == dynamic?
   checkWithHevm = pkgs.writeShellScript "checkWithHevm" ''
-
     # write json file to store for later debugging
     testName=$(${testName} $1)
     json=$out/jsonFiles/$testName.json
@@ -236,7 +265,7 @@ let
 
     explore() {
       set -x
-      hevm_output=$(${timeout} 90s ${hevm} symbolic --code "$1" --solver "$2" --json-file "$3" $4 2>&1)
+      hevm_output=$(${timeout} 90s ${hevm} symbolic --code "$1" --solver "$2" --json-file "$3" $4 $5 2>&1)
       status=$?
       set +x
 
@@ -273,10 +302,15 @@ let
         iterations="--max-iterations 3"
       fi
 
+      dynamic=""
+      if ! [[ -z "$3" ]]; then
+        dynamic="--calldata-model DynamicCD"
+      fi
+
       ${echo}
       ${echo} exploring runtime bytecode:
       bin_runtime=$(${jq} -r --arg c $contract -c '.contracts[$c]."bin-runtime"' $json)
-      explore "$bin_runtime" "$2" "$json" "$iterations"
+      explore "$bin_runtime" "$2" "$json" "$iterations" "$dynamic"
     done
 
     exit 0
@@ -305,6 +339,27 @@ let
         exit 0
     fi
 
+    z3Timeouts=(${toString z3Timeout})
+    if [[ " ''${z3Timeouts[@]} " =~ " ''${testName} " ]] && [[ $2 = "z3" ]]; then
+        ${echo} "skipping test:" ${testName}
+        ${echo} "${strings.ignore}"
+        exit 0
+    fi
+
+    dynamicFlag=""
+    dynamicTests=(${toString dynamic})
+    if [[ " ''${dynamicTests[@]} " =~ " ''${testName} " ]]; then
+        # echo $2
+        if [[ $2 = "z3" ]]; then
+          dynamicFlag=1
+        else
+          ${echo} "skipping test:" ${testName}
+          ${echo} "${strings.ignore}"
+
+          exit 0
+        fi
+    fi
+
     ${grep} -q 'Error trying to invoke SMT solver.' $1
     if [ $? == 0 ]; then ${echo} ${strings.smtCheckerFailed} && exit; fi
     ${grep} -q 'Assertion checker does not yet implement' $1
@@ -312,7 +367,7 @@ let
     ${grep} -q 'Assertion checker does not yet support' $1
     if [ $? == 0 ]; then ${echo} ${strings.smtCheckerFailed} && exit; fi
 
-    hevm_output=$(${checkWithHevm} $1 $2 2>&1)
+    hevm_output=$(${checkWithHevm} $1 $2 "$dynamicFlag" 2>&1)
     echo "$hevm_output"
 
     ${grep} -q '${strings.timeout}' <<< "$hevm_output"
diff --git a/src/dapp-tests/bytes.sol b/src/dapp-tests/bytes.sol
new file mode 100644
index 000000000..dbec0336c
--- /dev/null
+++ b/src/dapp-tests/bytes.sol
@@ -0,0 +1,7 @@
+contract Bytes
+{
+    function f(bytes memory b1, bytes memory b2) public pure {
+        b1 = b2;
+        assert(b1[1] == b2[1]);
+    }
+}
diff --git a/src/dapp-tests/integration/tests.sh b/src/dapp-tests/integration/tests.sh
index 5296a50fa..05a82427a 100755
--- a/src/dapp-tests/integration/tests.sh
+++ b/src/dapp-tests/integration/tests.sh
@@ -66,6 +66,10 @@ test_hevm_symbolic() {
     solc --bin-runtime -o . --overwrite AB.sol
     hevm equivalence --code-a $(<A.bin-runtime) --code-b $(<B.bin-runtime) --solver cvc4
     rm -rf A.bin-runtime B.bin-runtime
+
+    # simple dynamic calldata example
+    solc --bin-runtime -o . --overwrite bytes.sol
+    timeout 2m hevm symbolic --code $(<Bytes.bin-runtime) --calldata-model DynamicCD
 }
 
 test_hevm_symbolic
diff --git a/src/dapp-tests/shell.nix b/src/dapp-tests/shell.nix
index 4af1f539c..5e079068d 100644
--- a/src/dapp-tests/shell.nix
+++ b/src/dapp-tests/shell.nix
@@ -5,5 +5,5 @@
 pkgs.mkShell {
   name = "dapp-tests";
 
-  buildInputs = with pkgs; [ killall cacert bashInteractive curl dapp gnumake hevm procps seth solc ];
+  buildInputs = with pkgs; [ coreutils killall cacert bashInteractive curl dapp gnumake hevm procps seth solc ];
 }
diff --git a/src/hevm/hevm-cli/hevm-cli.hs b/src/hevm/hevm-cli/hevm-cli.hs
index 7dbd6608c..3639fe6e5 100644
--- a/src/hevm/hevm-cli/hevm-cli.hs
+++ b/src/hevm/hevm-cli/hevm-cli.hs
@@ -12,10 +12,10 @@
 
 module Main where
 
-import EVM (StorageModel(..))
+import EVM (StorageModel(..), CalldataModel(..))
 import qualified EVM
 import EVM.Concrete (createAddress, w256)
-import EVM.Symbolic (forceLitBytes, litAddr, w256lit, sw256, SymWord(..), len)
+import EVM.Symbolic (forceLitBytes, litAddr, w256lit, sw256, SymWord(..), len, Calldata(..))
 import qualified EVM.FeeSchedule as FeeSchedule
 import qualified EVM.Fetch
 import qualified EVM.Flatten
@@ -57,6 +57,8 @@ import Data.Text.IO               (hPutStr)
 import Data.Maybe                 (fromMaybe, fromJust)
 import Data.Version               (showVersion)
 import Data.SBV hiding (Word, solver, verbose, name)
+import qualified Data.SBV.List as SList
+import qualified Data.SBV as SBV
 import Data.SBV.Control hiding (Version, timeout, create)
 import System.IO                  (hFlush, hPrint, stdout, stderr)
 import System.Directory           (withCurrentDirectory, listDirectory)
@@ -109,16 +111,18 @@ data Command w
       , block       :: w ::: Maybe W256       <?> "Block state is be fetched from"
 
   -- symbolic execution opts
-      , jsonFile      :: w ::: Maybe String       <?> "Filename or path to dapp build output (default: out/*.solc.json)"
-      , dappRoot      :: w ::: Maybe String       <?> "Path to dapp project root directory (default: . )"
-      , storageModel  :: w ::: Maybe StorageModel <?> "Select storage model: ConcreteS, SymbolicS (default) or InitialS"
-      , sig           :: w ::: Maybe Text         <?> "Signature of types to decode / encode"
-      , arg           :: w ::: [String]           <?> "Values to encode"
-      , debug         :: w ::: Bool               <?> "Run interactively"
-      , getModels     :: w ::: Bool               <?> "Print example testcase for each execution path"
-      , smttimeout    :: w ::: Maybe Integer      <?> "Timeout given to SMT solver in milliseconds (default: 20000)"
-      , maxIterations :: w ::: Maybe Integer      <?> "Number of times we may revisit a particular branching point"
-      , solver        :: w ::: Maybe Text         <?> "Used SMT solver: z3 (default) or cvc4"
+      , jsonFile      :: w ::: Maybe String        <?> "Filename or path to dapp build output (default: out/*.solc.json)"
+      , dappRoot      :: w ::: Maybe String        <?> "Path to dapp project root directory (default: . )"
+      , storageModel  :: w ::: Maybe StorageModel  <?> "Select storage model: ConcreteS, SymbolicS (default) or InitialS"
+      , calldataModel :: w ::: Maybe CalldataModel <?> "Select calldata model: BoundedCD (default), or DynamicCD"
+      , sig           :: w ::: Maybe Text          <?> "Signature of types to decode / encode"
+      , arg           :: w ::: [String]            <?> "Values to encode"
+      , debug         :: w ::: Bool                <?> "Run interactively"
+      , getModels     :: w ::: Bool                <?> "Print example testcase for each execution path"
+      , smttimeout    :: w ::: Maybe Integer       <?> "Timeout given to SMT solver in milliseconds (default: 20000)"
+      , maxIterations :: w ::: Maybe Integer       <?> "Number of times we may revisit a particular branching point"
+      , solver        :: w ::: Maybe Text          <?> "Used SMT solver: z3 (default) or cvc4"
+      , smtoutput     :: w ::: Bool                <?> "Print verbose smt output"
       }
   | Equivalence -- prove equivalence between two programs
       { codeA         :: w ::: ByteString    <?> "Bytecode of the first program"
@@ -387,7 +391,7 @@ equivalence cmd =
        Just sig' -> do method' <- functionAbi sig'
                        return $ Just (view methodSignature method', snd <$> view methodInputs method')
 
-     void . runSMTWithTimeOut (solver cmd) (smttimeout cmd) . query $
+     void . runSMTWithTimeOut (solver cmd) (smttimeout cmd) (smtoutput cmd) . query $
        equivalenceCheck bytecodeA bytecodeB (maxIterations cmd) maybeSignature >>= \case
          Right vm -> do io $ putStrLn "Not equal!"
                         io $ putStrLn "Counterexample:"
@@ -401,18 +405,18 @@ equivalence cmd =
 
 
 -- cvc4 sets timeout via a commandline option instead of smtlib `(set-option)`
-runSMTWithTimeOut :: Maybe Text -> Maybe Integer -> Symbolic a -> IO a
-runSMTWithTimeOut solver maybeTimeout sym
+runSMTWithTimeOut :: Maybe Text -> Maybe Integer -> Bool -> Symbolic a -> IO a
+runSMTWithTimeOut solver maybeTimeout verbose' sym 
   | solver == Just "cvc4" = do
       setEnv "SBV_CVC4_OPTIONS" ("--lang=smt --incremental --interactive --no-interactive-prompt --model-witness-value --tlimit-per=" <> show timeout)
-      a <- runSMTWith cvc4 sym
+      a <- runSMTWith cvc4{SBV.verbose=verbose'} sym
       setEnv "SBV_CVC4_OPTIONS" ""
       return a
   | solver == Just "z3" = runwithz3
   | solver == Nothing = runwithz3
   | otherwise = error "Unknown solver. Currently supported solvers; z3, cvc4"
  where timeout = fromMaybe 20000 maybeTimeout
-       runwithz3 = runSMTWith z3 $ (setTimeOut timeout) >> sym
+       runwithz3 = runSMTWith z3{SBV.verbose=verbose'} $ (setTimeOut timeout) >> sym
 
 
 checkForVMErrors :: [EVM.VM] -> [String]
@@ -463,7 +467,7 @@ assert cmd = do
           name = view methodSignature method'
       return $ Just (name,typ)
   if debug cmd then
-    runSMTWithTimeOut (solver cmd) (smttimeout cmd) $ query $ do
+    runSMTWithTimeOut (solver cmd) (smttimeout cmd) (smtoutput cmd) $ query $ do
       preState <- symvmFromCommand cmd
       smtState <- queryState
       io $ void $ EVM.TTY.runFromVM
@@ -473,7 +477,7 @@ assert cmd = do
         preState
 
   else
-    runSMTWithTimeOut (solver cmd) (smttimeout cmd) $ query $ do
+    runSMTWithTimeOut (solver cmd) (smttimeout cmd) (smtoutput cmd) $ query $ do
       preState <- symvmFromCommand cmd
       verify preState (maxIterations cmd) rpcinfo (Just checkAssertions) >>= \case
         Right _ -> do
@@ -519,7 +523,7 @@ assert cmd = do
                         "Stopped"
                       else io $ putStrLn $
                         "Returned: " <> show (ByteStringS msg)
-                    Just (EVM.VMSuccess (SymbolicBuffer msg)) -> do
+                    Just (EVM.VMSuccess (StaticSymBuffer msg)) -> do
                       out <- mapM (getValue.fromSized) msg
                       io . putStrLn $
                         "Returned: " <> show (ByteStringS (ByteString.pack out))
@@ -582,7 +586,7 @@ launchExec cmd = do
           exitWith (ExitFailure 2)
         Just (EVM.VMSuccess buf) -> do
           let msg = case buf of
-                SymbolicBuffer msg' -> forceLitBytes msg'
+                StaticSymBuffer msg' -> forceLitBytes msg'
                 ConcreteBuffer msg' -> msg'
           print $ ByteStringS msg
           case state cmd of
@@ -679,7 +683,7 @@ vmFromCommand cmd = do
         value'   = word value 0
         caller'  = addr caller 0
         origin'  = addr origin 0
-        calldata' = ConcreteBuffer $ bytes calldata ""
+        calldata' = CalldataBuffer $ ConcreteBuffer $ bytes calldata ""
         codeType = if create cmd then EVM.InitCode else EVM.RuntimeCode
         address' = if create cmd
               then createAddress origin' (word nonce 0)
@@ -687,7 +691,7 @@ vmFromCommand cmd = do
 
         vm1 c = EVM.makeVm $ EVM.VMOpts
           { EVM.vmoptContract      = c
-          , EVM.vmoptCalldata      = (calldata', literal . num $ len calldata')
+          , EVM.vmoptCalldata      = calldata'
           , EVM.vmoptValue         = w256lit value'
           , EVM.vmoptAddress       = address'
           , EVM.vmoptCaller        = litAddr caller'
@@ -714,22 +718,29 @@ symvmFromCommand :: Command Options.Unwrapped -> Query EVM.VM
 symvmFromCommand cmd = do
   caller' <- maybe (SAddr <$> freshVar_) (return . litAddr) (caller cmd)
   callvalue' <- maybe (sw256 <$> freshVar_) (return . w256lit) (value cmd)
-  (calldata', cdlen, pathCond) <- case (calldata cmd, sig cmd) of
-    -- fully abstract calldata (up to 1024 bytes)
-    (Nothing, Nothing) -> do
+  (calldata', preCond) <- case (calldata cmd, sig cmd, calldataModel cmd) of
+    -- dynamic calldata via smt lists
+    (Nothing, Nothing, Just DynamicCD) -> do
+      cd <- freshVar_
+      return (CalldataBuffer (DynamicSymBuffer cd),
+              SList.length cd .< 1000 .&&
+               sw256 (sFromIntegral (SList.length cd)) .< sw256 1000)
+
+    -- dynamic calldata via (bounded) haskell list
+    (Nothing, Nothing, _) -> do
       cd <- sbytes256
-      len <- freshVar_
-      return (SymbolicBuffer cd, len, len .<= 256)
+      len <- sw256 <$> freshVar_
+      return (CalldataDynamic (cd, len), len .<= 256)
+
     -- fully concrete calldata
-    (Just c, Nothing) ->
-      let cd = ConcreteBuffer $ decipher c
-      in return (cd, num (len cd), sTrue)
+    (Just c, Nothing, _) ->
+      return (CalldataBuffer (ConcreteBuffer $ decipher c), sTrue)
     -- calldata according to given abi with possible specializations from the `arg` list
-    (Nothing, Just sig') -> do
+    (Nothing, Just sig', _) -> do
       method' <- io $ functionAbi sig'
       let typs = snd <$> view methodInputs method'
-      (cd, cdlen) <- symCalldata (view methodSignature method') typs (arg cmd)
-      return (SymbolicBuffer cd, cdlen, sTrue)
+      cd <- staticCalldata (view methodSignature method') typs (arg cmd)
+      return (CalldataBuffer (StaticSymBuffer cd), sTrue)
 
     _ -> error "incompatible options: calldata and abi"
 
@@ -750,7 +761,10 @@ symvmFromCommand cmd = do
           error $ "contract not found."
         Just contract' ->
           return $
-            vm1 cdlen calldata' callvalue' caller' (contract'' & set EVM.storage store)
+            vm1 calldata' callvalue' caller'
+                (contract''
+                   & set EVM.storage store
+                   & set EVM.origStorage store)
           where
             contract'' = case code cmd of
               Nothing -> contract'
@@ -765,12 +779,14 @@ symvmFromCommand cmd = do
 
     (_, _, Just c)  ->
       return $
-        vm1 cdlen calldata' callvalue' caller' $
-          (EVM.initialContract . codeType $ decipher c) & set EVM.storage store
+        vm1 calldata' callvalue' caller' $
+          (EVM.initialContract . codeType $ decipher c)
+             & set EVM.storage store
+             & set EVM.origStorage store
     (_, _, Nothing) ->
       error $ "must provide at least (rpc + address) or code"
 
-  return $ vm & over EVM.pathConditions (<> [pathCond])
+  return $ vm & over EVM.pathConditions (<> [preCond])
 
   where
     decipher = hexByteString "bytes" . strip0x
@@ -780,9 +796,9 @@ symvmFromCommand cmd = do
     address' = if create cmd
           then createAddress origin' (word nonce 0)
           else addr address 0xacab
-    vm1 cdlen calldata' callvalue' caller' c = EVM.makeVm $ EVM.VMOpts
+    vm1 calldata' callvalue' caller' c = EVM.makeVm $ EVM.VMOpts
       { EVM.vmoptContract      = c
-      , EVM.vmoptCalldata      = (calldata', cdlen)
+      , EVM.vmoptCalldata      = calldata'
       , EVM.vmoptValue         = callvalue'
       , EVM.vmoptAddress       = address'
       , EVM.vmoptCaller        = caller'
diff --git a/src/hevm/src/EVM.hs b/src/hevm/src/EVM.hs
index df266bf32..a0f591169 100644
--- a/src/hevm/src/EVM.hs
+++ b/src/hevm/src/EVM.hs
@@ -16,6 +16,7 @@ module EVM where
 import Prelude hiding (log, Word, exponent)
 
 import Data.SBV hiding (Word, output, Unknown)
+import Data.SBV.List (implode, subList)
 import Data.Proxy (Proxy(..))
 import EVM.ABI
 import EVM.Types
@@ -170,7 +171,7 @@ data Cache = Cache
 -- | A way to specify an initial VM state
 data VMOpts = VMOpts
   { vmoptContract :: Contract
-  , vmoptCalldata :: (Buffer, (SWord 32)) -- maximum size of uint32 as per eip 1985
+  , vmoptCalldata :: Calldata
   , vmoptValue :: SymWord
   , vmoptAddress :: Addr
   , vmoptCaller :: SAddr
@@ -207,8 +208,8 @@ data FrameContext
     , creationContextSubstate  :: SubState
     }
   | CallContext
-    { callContextOffset    :: Word
-    , callContextSize      :: Word
+    { callContextOffset    :: SymWord
+    , callContextSize      :: SymWord
     , callContextCodehash  :: W256
     , callContextAbi       :: Maybe Word
     , callContextData      :: Buffer
@@ -224,8 +225,8 @@ data FrameState = FrameState
   , _pc           :: Int
   , _stack        :: [SymWord]
   , _memory       :: Buffer
-  , _memorySize   :: Int
-  , _calldata     :: (Buffer, (SWord 32))
+  , _memorySize   :: SymWord
+  , _calldata     :: Calldata
   , _callvalue    :: SymWord
   , _caller       :: SAddr
   , _gas          :: Word
@@ -249,7 +250,7 @@ data TxState = TxState
 data SubState = SubState
   { _selfdestructs   :: [Addr]
   , _touchedAccounts :: [Addr]
-  , _refunds         :: [(Addr, Word)]
+  , _refunds         :: Word -- TODO: make symbolic as well
   -- in principle we should include logs here, but do not for now
   }
 
@@ -288,7 +289,7 @@ data Contract = Contract
   , _opIxMap      :: Vector Int
   , _codeOps      :: RegularVector.Vector (Int, Op)
   , _external     :: Bool
-  , _origStorage  :: Map Word Word
+  , _origStorage  :: Storage
   }
 
 deriving instance Show Contract
@@ -312,6 +313,14 @@ data StorageModel
 
 instance ParseField StorageModel
 
+-- | Calldata can either by a normal buffer, or a custom "pseudo dynamic" encoding. See EVM.Symbolic for details
+data CalldataModel
+  = DynamicCD
+  | BoundedCD
+  deriving (Read, Show)
+
+instance ParseField CalldataModel
+
 -- | Various environmental data
 data Env = Env
   { _contracts    :: Map Addr Contract
@@ -342,7 +351,7 @@ blankState = FrameState
   , _stack        = mempty
   , _memory       = mempty
   , _memorySize   = 0
-  , _calldata     = (mempty, 0)
+  , _calldata     = CalldataBuffer mempty
   , _callvalue    = 0
   , _caller       = 0
   , _gas          = 0
@@ -397,7 +406,7 @@ makeVm o = VM
     , _origin = vmoptOrigin o
     , _toAddr = vmoptAddress o
     , _value = vmoptValue o
-    , _substate = SubState mempty mempty mempty
+    , _substate = SubState mempty mempty 0
     , _isCreate = vmoptCreate o
     , _txReversion = Map.fromList
       [(vmoptAddress o, vmoptContract o)]
@@ -459,14 +468,16 @@ initialContract theContractCode = Contract
   , _opIxMap  = mkOpIxMap theCode
   , _codeOps  = mkCodeOps theCode
   , _external = False
-  , _origStorage = mempty
+  , _origStorage = Concrete mempty
   } where theCode = case theContractCode of
             InitCode b    -> b
             RuntimeCode b -> b
 
 contractWithStore :: ContractCode -> Storage -> Contract
 contractWithStore theContractCode store =
-  initialContract theContractCode & set storage store
+  initialContract theContractCode
+    & set storage store
+    & set origStorage store
 
 -- * Opcode dispatch (exec1)
 
@@ -497,29 +508,25 @@ exec1 = do
 
   if self > 0x0 && self <= 0x9 then do
     -- call to precompile
+
     let ?op = 0x00 -- dummy value
-    let
-      calldatasize = snd (the state calldata)
-    case unliteral calldatasize of
+    copyCalldataToMemory (the state calldata) (cdlen $ the state calldata) 0 0
+    executePrecompile self (the state gas) 0 (cdlen $ the state calldata) 0 0 []
+    vmx <- get
+    case view (state.stack) vmx of
+      (x:_) -> case maybeLitWord x of
+        Just 0 -> do
+          fetchAccount self $ \_ -> do
+            touchAccount self
+            vmError PrecompileFailure
+        Just _ ->
+          fetchAccount self $ \_ -> do
+            touchAccount self
+            out <- use (state . returndata)
+            finishFrame (FrameReturned out)
         Nothing -> vmError UnexpectedSymbolicArg
-        Just calldatasize' -> do
-          copyBytesToMemory (fst $ the state calldata) (num calldatasize') 0 0
-          executePrecompile self (the state gas) 0 (num calldatasize') 0 0 []
-          vmx <- get
-          case view (state.stack) vmx of
-            (x:_) -> case maybeLitWord x of
-              Just 0 -> do
-                fetchAccount self $ \_ -> do
-                  touchAccount self
-                  vmError PrecompileFailure
-              Just _ ->
-                fetchAccount self $ \_ -> do
-                  touchAccount self
-                  out <- use (state . returndata)
-                  finishFrame (FrameReturned out)
-              Nothing -> vmError UnexpectedSymbolicArg
-            _ ->
-              underrun
+      _ ->
+        underrun
 
   else if the state pc >= num (BS.length (the state code))
     then doStop
@@ -567,16 +574,15 @@ exec1 = do
           notStatic $
           let n = (num x - 0xa0) in
           case stk of
-            (xOffset':xSize':xs) ->
+            (xOffset:xSize:xs) ->
               if length xs < n
               then underrun
-              else
-                forceConcrete2 (xOffset', xSize') $ \(xOffset, xSize) -> do
+              else do
                     let (topics, xs') = splitAt n xs
-                        bytes         = readMemory (num xOffset) (num xSize) vm
+                        bytes         = readMemory xOffset xSize vm
                         log           = Log self bytes topics
 
-                    burn (g_log + g_logdata * xSize + num n * g_logtopic) $
+                    burnSym (litWord g_log + litWord g_logdata * xSize + litWord (num n * g_logtopic)) $
                       accessMemoryRange fees xOffset xSize $ do
                         traceLog log
                         next
@@ -589,96 +595,95 @@ exec1 = do
         0x00 -> doStop
 
         -- op: ADD
-        0x01 -> stackOp2 (const g_verylow) (uncurry (+))
+        0x01 -> stackOp2 (const (litWord g_verylow)) (uncurry (+))
         -- op: MUL
-        0x02 -> stackOp2 (const g_low) (uncurry (*))
+        0x02 -> stackOp2 (const (litWord g_low)) (uncurry (*))
         -- op: SUB
-        0x03 -> stackOp2 (const g_verylow) (uncurry (-))
+        0x03 -> stackOp2 (const (litWord g_verylow)) (uncurry (-))
 
         -- op: DIV
-        0x04 -> stackOp2 (const g_low) (uncurry (sDiv))
+        0x04 -> stackOp2 (const (litWord g_low)) (uncurry (sDiv))
 
         -- op: SDIV
         0x05 ->
-          stackOp2 (const g_low) (uncurry sdiv)
+          stackOp2 (const (litWord g_low)) (uncurry sdiv)
 
         -- op: MOD
-        0x06 -> stackOp2 (const g_low) $ \(x, y) -> ite (y .== 0) 0 (x `sMod` y)
+        0x06 -> stackOp2 (const (litWord g_low)) $ \(x, y) -> ite (y .== 0) 0 (x `sMod` y)
 
         -- op: SMOD
-        0x07 -> stackOp2 (const g_low) $ uncurry smod
+        0x07 -> stackOp2 (const (litWord g_low)) $ uncurry smod
         -- op: ADDMOD
         0x08 -> stackOp3 (const g_mid) (\(x, y, z) -> addmod x y z)
         -- op: MULMOD
         0x09 -> stackOp3 (const g_mid) (\(x, y, z) -> mulmod x y z)
 
         -- op: LT
-        0x10 -> stackOp2 (const g_verylow) $ \(x, y) -> ite (x .< y) 1 0
+        0x10 -> stackOp2 (const (litWord g_verylow)) $ \(x, y) -> ite (x .< y) 1 0
         -- op: GT
-        0x11 -> stackOp2 (const g_verylow) $ \(x, y) -> ite (x .> y) 1 0
+        0x11 -> stackOp2 (const (litWord g_verylow)) $ \(x, y) -> ite (x .> y) 1 0
         -- op: SLT
-        0x12 -> stackOp2 (const g_verylow) $ uncurry slt
+        0x12 -> stackOp2 (const (litWord g_verylow)) $ uncurry slt
         -- op: SGT
-        0x13 -> stackOp2 (const g_verylow) $ uncurry sgt
+        0x13 -> stackOp2 (const (litWord g_verylow)) $ uncurry sgt
 
         -- op: EQ
-        0x14 -> stackOp2 (const g_verylow) $ \(x, y) -> ite (x .== y) 1 0
+        0x14 -> stackOp2 (const (litWord g_verylow)) $ \(x, y) -> ite (x .== y) 1 0
         -- op: ISZERO
         0x15 -> stackOp1 (const g_verylow) $ \x -> ite (x .== 0) 1 0
 
         -- op: AND
-        0x16 -> stackOp2 (const g_verylow) $ uncurry (.&.)
+        0x16 -> stackOp2 (const (litWord g_verylow)) $ uncurry (.&.)
         -- op: OR
-        0x17 -> stackOp2 (const g_verylow) $ uncurry (.|.)
+        0x17 -> stackOp2 (const (litWord g_verylow)) $ uncurry (.|.)
         -- op: XOR
-        0x18 -> stackOp2 (const g_verylow) $ uncurry xor
+        0x18 -> stackOp2 (const (litWord g_verylow)) $ uncurry xor
         -- op: NOT
         0x19 -> stackOp1 (const g_verylow) complement
 
         -- op: BYTE
-        0x1a -> stackOp2 (const g_verylow) $ \case
+        0x1a -> stackOp2 (const (litWord g_verylow)) $ \case
           (n, _) | (forceLit n) >= 32 -> 0
           (n, x) | otherwise          -> 0xff .&. shiftR x (8 * (31 - num (forceLit n)))
 
         -- op: SHL
-        0x1b -> stackOp2 (const g_verylow) $ \((S _ n), (S _ x)) -> sw256 $ sShiftLeft x n
+        0x1b -> stackOp2 (const (litWord g_verylow)) $ \((S _ n), (S _ x)) -> sw256 $ sShiftLeft x n
         -- op: SHR
-        0x1c -> stackOp2 (const g_verylow) $ uncurry shiftRight'
+        0x1c -> stackOp2 (const (litWord g_verylow)) $ uncurry shiftRight'
         -- op: SAR
-        0x1d -> stackOp2 (const g_verylow) $ \((S _ n), (S _ x)) -> sw256 $ sSignedShiftArithRight x n
+        0x1d -> stackOp2 (const (litWord g_verylow)) $ \((S _ n), (S _ x)) -> sw256 $ sSignedShiftArithRight x n
 
         -- op: SHA3
         -- more accurately refered to as KECCAK
         0x20 ->
           case stk of
-            (xOffset' : xSize' : xs) ->
-              forceConcrete xOffset' $
-                \xOffset -> forceConcrete xSize' $ \xSize -> do
-                  (hash, invMap) <- case readMemory xOffset xSize vm of
-                                     ConcreteBuffer bs -> pure (litWord $ keccakBlob bs, Map.singleton (keccakBlob bs) bs)
-
-                                     -- Although we would like to simply assert that the uninterpreted function symkeccak'
-                                     -- is injective, this proves to cause a lot of concern for our smt solvers, probably
-                                     -- due to the introduction of universal quantifiers into the queries.
-
-                                     -- Instead, we keep track of all of the particular invocations of symkeccak' we see
-                                     -- (similarly to sha3Crack), and simply assert that injectivity holds for these
-                                     -- particular invocations.
-
-                                     SymbolicBuffer bs -> do
-                                                   let hash' = symkeccak' bs
-                                                       previousUsed = view (env . keccakUsed) vm
-                                                   env . keccakUsed <>= [(bs, hash')]
-                                                   pathConditions <>= fmap (\(preimage, image) ->
-                                                                               image .== hash' .=> preimage .== bs)
-                                                                           previousUsed
-                                                   return (sw256 hash', mempty)
-
-                  burn (g_sha3 + g_sha3word * ceilDiv (num xSize) 32) $
-                    accessMemoryRange fees xOffset xSize $ do
-                      next
-                      assign (state . stack) (hash : xs)
-                      (env . sha3Crack) <>= invMap
+            (xOffset : xSize : xs) -> do
+
+               (hash, invMap) <- case readMemory xOffset xSize vm of
+
+                 DynamicSymBuffer bs -> error "currently unsupported: KECCAK of dynamic bytes"
+                 ConcreteBuffer bs -> pure (litWord $ keccakBlob bs, Map.singleton (keccakBlob bs) bs)
+
+                 -- Although we would like to simply assert that the uninterpreted function symkeccak'
+                 -- is injective, this proves to cause a lot of concern for our smt solvers, probably
+                 -- due to the introduction of universal quantifiers into the queries.
+
+                 -- Instead, we keep track of all of the particular invocations of symkeccak' we see
+                 -- (similarly to sha3Crack), and simply assert that injectivity holds for these
+                 -- particular invocations.
+
+                 StaticSymBuffer bs -> do
+                   let hash' = symkeccak' bs
+                       previousUsed = view (env . keccakUsed) vm
+                   env . keccakUsed <>= [(bs, hash')]
+                   pathConditions <>= flip fmap previousUsed (\(preimg, img) -> img .== hash' .=> preimg .== bs)
+                   return (sw256 hash', mempty)
+
+               burnSym (litWord g_sha3 + litWord g_sha3word * ceilSDiv xSize 32) $
+                 accessMemoryRange fees xOffset xSize $ do
+                   next
+                   assign (state . stack) (hash : xs)
+                   (env . sha3Crack) <>= invMap
             _ -> underrun
 
         -- op: ADDRESS
@@ -716,26 +721,24 @@ exec1 = do
 
         -- op: CALLDATALOAD
         0x35 -> stackOp1 (const g_verylow) $
-          \(S _ x) -> uncurry (readSWordWithBound (sFromIntegral x)) (the state calldata)
+          case the state calldata of
+            CalldataBuffer bf -> flip readSWord bf
+            CalldataDynamic bf -> flip readStaticWordWithBound bf
 
         -- op: CALLDATASIZE
         0x36 ->
           limitStack 1 . burn g_base $
-            next >> pushSym (sw256 . zeroExtend . snd $ (the state calldata))
+            next >> pushSym (cdlen $ the state calldata)
 
         -- op: CALLDATACOPY
         0x37 ->
           case stk of
-            (xTo' : xFrom' : xSize' : xs) -> forceConcrete3 (xTo',xFrom',xSize') $ \(xTo,xFrom,xSize) ->
-              burn (g_verylow + g_copy * ceilDiv xSize 32) $
+            (xTo : xFrom : xSize : xs) ->
+              burnSym (litWord g_verylow + litWord g_copy * ceilSDiv xSize 32) $
                 accessUnboundedMemoryRange fees xTo xSize $ do
                   next
                   assign (state . stack) xs
-                  case the state calldata of
-                    (SymbolicBuffer cd, cdlen) -> copyBytesToMemory (SymbolicBuffer [ite (i .<= cdlen) x 0 | (x, i) <- zip cd [1..]]) xSize xFrom xTo
-                    -- when calldata is concrete,
-                    -- the bound should always be equal to the bytestring length
-                    (cd, _) -> copyBytesToMemory cd xSize xFrom xTo
+                  copyCalldataToMemory (the state calldata) xSize xFrom xTo
             _ -> underrun
 
         -- op: CODESIZE
@@ -746,8 +749,8 @@ exec1 = do
         -- op: CODECOPY
         0x39 ->
           case stk of
-            (memOffset' : codeOffset' : n' : xs) -> forceConcrete3 (memOffset',codeOffset',n') $ \(memOffset,codeOffset,n) -> do
-              burn (g_verylow + g_copy * ceilDiv (num n) 32) $
+            (memOffset : codeOffset : n : xs) ->
+              burnSym (litWord g_verylow + litWord g_copy * ceilSDiv n 32) $
                 accessUnboundedMemoryRange fees memOffset n $ do
                   next
                   assign (state . stack) xs
@@ -782,38 +785,44 @@ exec1 = do
         0x3c ->
           case stk of
             ( extAccount'
-              : memOffset'
+              : memOffset
               : codeOffset'
               : codeSize'
               : xs ) ->
-              forceConcrete4 (extAccount', memOffset', codeOffset', codeSize') $
-                \(extAccount, memOffset, codeOffset, codeSize) ->
+              forceConcrete3 (extAccount', codeOffset', codeSize') $
+                \(extAccount, codeOffset, codeSize) ->
                   burn (g_extcode + g_copy * ceilDiv (num codeSize) 32) $
-                    accessUnboundedMemoryRange fees memOffset codeSize $
+                    accessUnboundedMemoryRange fees memOffset (litWord codeSize) $
                       fetchAccount (num extAccount) $ \c -> do
                         next
                         assign (state . stack) xs
                         copyBytesToMemory (ConcreteBuffer (view bytecode c))
-                          codeSize codeOffset memOffset
+                          (litWord codeSize) (litWord codeOffset) memOffset
             _ -> underrun
 
         -- op: RETURNDATASIZE
         0x3d ->
           limitStack 1 . burn g_base $
-            next >> push (num $ len (the state returndata))
+            next >> pushSym (len $ the state returndata)
 
         -- op: RETURNDATACOPY
         0x3e ->
           case stk of
-            (xTo' : xFrom' : xSize' :xs) -> forceConcrete3 (xTo', xFrom', xSize') $
-              \(xTo, xFrom, xSize) ->
-                burn (g_verylow + g_copy * ceilDiv xSize 32) $
+            (xTo : xFrom : xSize :xs) ->
+                burnSym (litWord g_verylow + litWord g_copy * ceilSDiv xSize 32) $
                   accessUnboundedMemoryRange fees xTo xSize $ do
                     next
                     assign (state . stack) xs
-                    if len (the state returndata) < num xFrom + num xSize
-                    then vmError InvalidMemoryAccess
-                    else copyBytesToMemory (the state returndata) xSize xFrom xTo
+                    case unliteral $ len (the state returndata) .< xFrom + xSize of
+                      Nothing ->
+                        --TODO: consult smt about possible failure here
+                        copyBytesToMemory (the state returndata) xSize xFrom xTo
+
+                      Just res ->
+                         if res
+                         then vmError InvalidMemoryAccess
+                         else copyBytesToMemory (the state returndata) xSize xFrom xTo
+
             _ -> underrun
 
         -- op: EXTCODEHASH
@@ -886,28 +895,28 @@ exec1 = do
         -- op: MLOAD
         0x51 ->
           case stk of
-            (x':xs) -> forceConcrete x' $ \x ->
+            (x:xs) ->
               burn g_verylow $
                 accessMemoryWord fees x $ do
                   next
-                  assign (state . stack) (view (word256At (num x)) mem : xs)
+                  assign (state . stack) (view (word256At x) mem : xs)
             _ -> underrun
 
         -- op: MSTORE
         0x52 ->
           case stk of
-            (x':y:xs) -> forceConcrete x' $ \x ->
+            (x:y:xs) ->
               burn g_verylow $
                 accessMemoryWord fees x $ do
                   next
-                  assign (state . memory . word256At (num x)) y
+                  assign (state . memory . word256At x) y
                   assign (state . stack) xs
             _ -> underrun
 
         -- op: MSTORE8
         0x53 ->
           case stk of
-            (x':(S _ y):xs) -> forceConcrete x' $ \x ->
+            (x:(S _ y):xs) ->
               burn g_verylow $
                 accessMemoryRange fees x 1 $ do
                   let yByte = bvExtract (Proxy :: Proxy 7) (Proxy :: Proxy 0) y
@@ -937,44 +946,35 @@ exec1 = do
                 if availableGas <= g_callstipend
                   then finishFrame (FrameErrored (OutOfGas availableGas g_callstipend))
                   else do
-                    let original = case view storage this of
-                                  Concrete _ -> fromMaybe 0 (Map.lookup (forceLit x) (view origStorage this))
-                                  Symbolic _ -> 0 -- we don't use this value anywhere anyway
-                        cost = case (maybeLitWord current, maybeLitWord new) of
-                                 (Just current', Just new') ->
-                                    if (current' == new') then g_sload
-                                    else if (current' == original) && (original == 0) then g_sset
-                                    else if (current' == original) then g_sreset
-                                    else g_sload
-
-                                 -- if any of the arguments are symbolic,
-                                 -- assume worst case scenario
-                                 _ -> g_sset
-
-                    burn cost $ do
+                    let original = fromMaybe 0 (readStorage (view origStorage this) x)
+                        pairPlus :: (SymWord, SymWord) -> (SymWord, SymWord) -> (SymWord, SymWord)
+                        pairPlus (a,b) (c,d) = (a + c, b + d)
+                        (cost, (anticost, unrefund)) =
+                           ite (current .== new) (litWord g_sload, (0, 0))
+                               (ite (original .== current)
+                                    (ite (original .== 0) (litWord g_sset, (0, 0))
+                                         (ite (new .== 0) (litWord g_sreset, (litWord r_sclear, 0))
+                                              (litWord g_sreset, (0, 0))))
+                                    -- cost always g_sload in this clause
+                                    (litWord g_sload, pairPlus
+                                                       (ite (original ./= 0)
+                                                          (pairPlus (ite (current .== 0) (0, litWord r_sclear) (0,0))
+                                                                    (ite (new .== 0)     (litWord r_sclear, 0) (0,0)))
+                                                       (0,0))
+                                                       (ite (original .== new)
+                                                            (ite (original .== 0) (litWord (g_sset   - g_sload), 0)
+                                                                                  (litWord (g_sreset - g_sload), 0))
+                                                            (0,0))))
+
+                    burnSym cost $ do
                       next
                       assign (state . stack) xs
                       modifying (env . contracts . ix self . storage)
                         (writeStorage x new)
 
-                      case (maybeLitWord current, maybeLitWord new) of
-                         (Just current', Just new') ->
-                            unless (current' == new') $
-                              if current' == original
-                              then when (original /= 0 && new' == 0) $
-                                      refund r_sclear
-                              else do
-                                      when (original /= 0) $
-                                        if new' == 0
-                                        then refund r_sclear
-                                        else unRefund r_sclear
-                                      when (original == new') $
-                                        if original == 0
-                                        then refund (g_sset - g_sload)
-                                        else refund (g_sreset - g_sload)
-                         -- if any of the arguments are symbolic,
-                         -- don't change the refund counter
-                         _ -> noop
+                      refundSym anticost
+                      unRefundSym unrefund
+
             _ -> underrun
 
         -- op: JUMP
@@ -1007,7 +1007,7 @@ exec1 = do
         -- op: MSIZE
         0x59 ->
           limitStack 1 . burn g_base $
-            next >> push (num (the state memorySize))
+            next >> pushSym (the state memorySize)
 
         -- op: GAS
         0x5a ->
@@ -1019,15 +1019,15 @@ exec1 = do
 
         -- op: EXP
         0x0a ->
-          let cost (_ ,(forceLit -> exponent)) =
-                if exponent == 0
-                then g_exp
-                else g_exp + g_expbyte * num (ceilDiv (1 + log2 exponent) 8)
+          let cost (_ ,exponent) =
+                ite (exponent .== 0)
+                    (litWord g_exp)
+                    (litWord g_exp + litWord g_expbyte * (ceilSDiv (litWord 1 + sw256 (sFromIntegral $ log2S exponent)) (litWord 8)))
           in stackOp2 cost $ \((S _ x),(S _ y)) -> sw256 $ x .^ y
 
         -- op: SIGNEXTEND
         0x0b ->
-          stackOp2 (const g_low) $ \((forceLit -> bytes), w@(S _ x)) ->
+          stackOp2 (const (litWord g_low)) $ \((forceLit -> bytes), w@(S _ x)) ->
             if bytes >= 32 then w
             else let n = num bytes * 8 + 7 in
               sw256 $ ite (sTestBit x n)
@@ -1038,15 +1038,14 @@ exec1 = do
         0xf0 ->
           notStatic $
           case stk of
-            (xValue' : xOffset' : xSize' : xs) -> forceConcrete3 (xValue', xOffset', xSize') $
-              \(xValue, xOffset, xSize) -> do
+            (xValue : xOffset : xSize : xs) -> forceConcrete xValue $ \xValue' ->
                 accessMemoryRange fees xOffset xSize $ do
                   availableGas <- use (state . gas)
                   let
                     newAddr = createAddress self (wordValue (view nonce this))
                     (cost, gas') = costOfCreate fees availableGas 0
-                  burn (cost - gas') $ forceConcreteBuffer (readMemory (num xOffset) (num xSize) vm) $ \initCode ->
-                    create self this gas' xValue xs newAddr initCode
+                  burn (cost - gas') $ forceConcreteBuffer (readMemory xOffset xSize vm) $ \initCode ->
+                    create self this gas' xValue' xs newAddr initCode
             _ -> underrun
 
         -- op: CALL
@@ -1054,14 +1053,14 @@ exec1 = do
           case stk of
             ( xGas'
               : xTo'
-              : (forceLit -> xValue)
-              : xInOffset'
-              : xInSize'
-              : xOutOffset'
-              : xOutSize'
+              : xValue'
+              : xInOffset
+              : xInSize
+              : xOutOffset
+              : xOutSize
               : xs
-             ) -> forceConcrete6 (xGas', xTo', xInOffset', xInSize', xOutOffset', xOutSize') $
-              \(xGas, (num -> xTo), xInOffset, xInSize, xOutOffset, xOutSize) ->
+             ) -> forceConcrete3 (xGas', xTo', xValue') $
+              \(xGas, (num -> xTo), xValue) ->
               (if xValue > 0 then notStatic else id) $
                 case xTo of
                   n | n > 0 && n <= 9 ->
@@ -1069,7 +1068,7 @@ exec1 = do
                   n | num n == cheatCode ->
                     do
                       assign (state . stack) xs
-                      cheat (xInOffset, xInSize) (xOutOffset, xOutSize)
+                      cheat xInOffset xInSize xOutOffset xOutSize
                   _ -> delegateCall this xGas xTo xTo xValue xInOffset xInSize xOutOffset xOutSize xs $ do
                             zoom state $ do
                               assign callvalue (litWord xValue)
@@ -1089,13 +1088,13 @@ exec1 = do
             ( xGas'
               : xTo'
               : (forceLit -> xValue)
-              : xInOffset'
-              : xInSize'
-              : xOutOffset'
-              : xOutSize'
+              : xInOffset
+              : xInSize
+              : xOutOffset
+              : xOutSize
               : xs
-              ) -> forceConcrete6 (xGas', xTo', xInOffset', xInSize', xOutOffset', xOutSize') $
-              \(xGas, (num -> xTo), xInOffset, xInSize, xOutOffset, xOutSize) ->
+              ) -> forceConcrete2 (xGas', xTo') $
+              \(xGas, (num -> xTo)) ->
                 case xTo of
                   n | n > 0 && n <= 9 ->
                     precompiledContract this xGas xTo self xValue xInOffset xInSize xOutOffset xOutSize xs
@@ -1110,35 +1109,37 @@ exec1 = do
         -- op: RETURN
         0xf3 ->
           case stk of
-            (xOffset' : xSize' :_) -> forceConcrete2 (xOffset', xSize') $ \(xOffset, xSize) ->
+            (xOffset : xSize :_) ->
               accessMemoryRange fees xOffset xSize $ do
                 let
                   output = readMemory xOffset xSize vm
-                  codesize = num (len output)
-                  maxsize = the block maxCodeSize
                 case view frames vm of
                   [] ->
                     case (the tx isCreate) of
-                      True ->
+                      True -> forceConcreteBuffer output $ \output' -> do
+                        let codesize = num $ BS.length output'
+                            maxsize = the block maxCodeSize
                         if codesize > maxsize
                         then
                           finishFrame (FrameErrored (MaxCodeSizeExceeded maxsize codesize))
                         else
                           burn (g_codedeposit * codesize) $
-                            finishFrame (FrameReturned output)
+                            finishFrame (FrameReturned $ ConcreteBuffer output')
                       False ->
                         finishFrame (FrameReturned output)
                   (frame: _) -> do
                     let
                       context = view frameContext frame
                     case context of
-                      CreationContext {} ->
+                      CreationContext {} -> forceConcreteBuffer output $ \output' -> do
+                        let codesize = num $ BS.length output'
+                            maxsize = the block maxCodeSize
                         if codesize > maxsize
                         then
                           finishFrame (FrameErrored (MaxCodeSizeExceeded maxsize codesize))
                         else
                           burn (g_codedeposit * codesize) $
-                            finishFrame (FrameReturned output)
+                            finishFrame (FrameReturned $ ConcreteBuffer output')
                       CallContext {} ->
                           finishFrame (FrameReturned output)
             _ -> underrun
@@ -1148,18 +1149,18 @@ exec1 = do
           case stk of
             (xGas'
              :xTo'
-             :xInOffset'
-             :xInSize'
-             :xOutOffset'
-             :xOutSize'
-             :xs) -> forceConcrete6 (xGas', xTo', xInOffset', xInSize', xOutOffset', xOutSize') $
-              \(xGas, (num -> xTo), xInOffset, xInSize, xOutOffset, xOutSize) ->
+             :xInOffset
+             :xInSize
+             :xOutOffset
+             :xOutSize
+             :xs) -> forceConcrete2 (xGas', xTo') $
+              \(xGas, (num -> xTo)) ->
                 case xTo of
                   n | n > 0 && n <= 9 ->
                     precompiledContract this xGas xTo self 0 xInOffset xInSize xOutOffset xOutSize xs
                   n | num n == cheatCode -> do
                         assign (state . stack) xs
-                        cheat (xInOffset, xInSize) (xOutOffset, xOutSize)
+                        cheat xInOffset xInSize xOutOffset xOutSize
                   _ -> do
                         delegateCall this xGas xTo self 0 xInOffset xInSize xOutOffset xOutSize xs $ do
                           touchAccount self
@@ -1169,14 +1170,14 @@ exec1 = do
         0xf5 -> notStatic $
           case stk of
             (xValue'
-             :xOffset'
+             :xOffset
              :xSize'
              :xSalt'
-             :xs) -> forceConcrete4 (xValue', xOffset', xSize', xSalt') $
-              \(xValue, xOffset, xSize, xSalt) ->
-                accessMemoryRange fees xOffset xSize $ do
+             :xs) -> forceConcrete3 (xValue', xSalt', xSize') $
+              \(xValue, xSalt, xSize) ->
+                accessMemoryRange fees xOffset (litWord xSize) $ do
                   availableGas <- use (state . gas)
-                  forceConcreteBuffer (readMemory (num xOffset) (num xSize) vm) $ \initCode ->
+                  forceConcreteBuffer (readMemory xOffset (litWord xSize) vm) $ \initCode ->
                    let
                     newAddr  = create2Address self (num xSalt) initCode
                     (cost, gas') = costOfCreate fees availableGas xSize
@@ -1189,12 +1190,12 @@ exec1 = do
           case stk of
             (xGas'
              :xTo'
-             :xInOffset'
-             :xInSize'
-             :xOutOffset'
-             :xOutSize'
-             :xs) -> forceConcrete6 (xGas', xTo', xInOffset', xInSize', xOutOffset', xOutSize') $
-              \(xGas, (num -> xTo), xInOffset, xInSize, xOutOffset, xOutSize) ->
+             :xInOffset
+             :xInSize
+             :xOutOffset
+             :xOutSize
+             :xs) -> forceConcrete2 (xGas', xTo') $
+              \(xGas, (num -> xTo)) -> 
                 case xTo of
                   n | n > 0 && n <= 9 ->
                     precompiledContract this xGas xTo xTo 0 xInOffset xInSize xOutOffset xOutSize xs
@@ -1237,19 +1238,18 @@ exec1 = do
         -- op: REVERT
         0xfd ->
           case stk of
-            (xOffset':xSize':_) -> forceConcrete2 (xOffset', xSize') $ \(xOffset, xSize) ->
+            (xOffset:xSize:_) ->
               accessMemoryRange fees xOffset xSize $ do
                 let output = readMemory xOffset xSize vm
                 finishFrame (FrameReverted output)
             _ -> underrun
 
-        xxx ->
-          vmError (UnrecognizedOpcode xxx)
+        xxx -> vmError (UnrecognizedOpcode xxx)
 
 -- | Checks a *CALL for failure; OOG, too many callframes, memory access etc.
 callChecks
   :: (?op :: Word8)
-  => Contract -> Word -> Addr -> Word -> Word -> Word -> Word -> Word -> [SymWord]
+  => Contract -> Word -> Addr -> Word -> SymWord -> SymWord -> SymWord -> SymWord -> [SymWord]
    -- continuation with gas avail for call
   -> (Word -> EVM ())
   -> EVM ()
@@ -1283,7 +1283,7 @@ precompiledContract
   -> Addr
   -> Addr
   -> Word
-  -> Word -> Word -> Word -> Word
+  -> SymWord -> SymWord -> SymWord -> SymWord
   -> [SymWord]
   -> EVM ()
 precompiledContract this xGas precompileAddr recipient xValue inOffset inSize outOffset outSize xs =
@@ -1311,11 +1311,11 @@ precompiledContract this xGas precompileAddr recipient xValue inOffset inSize ou
 executePrecompile
   :: (?op :: Word8)
   => Addr
-  -> Word -> Word -> Word -> Word -> Word -> [SymWord]
+  -> Word -> SymWord -> SymWord -> SymWord -> SymWord -> [SymWord]
   -> EVM ()
-executePrecompile preCompileAddr gasCap inOffset inSize outOffset outSize xs  = do
+executePrecompile preCompileAddr gasCap inOffset inSize outOffset outSize xs = do
   vm <- get
-  let input = readMemory (num inOffset) (num inSize) vm
+  let input = readMemory inOffset inSize vm
       fees = view (block . schedule) vm
       cost = costOfPrecompile fees preCompileAddr input
       notImplemented = error $ "precompile at address " <> show preCompileAddr <> " not yet implemented"
@@ -1351,7 +1351,7 @@ executePrecompile preCompileAddr gasCap inOffset inSize outOffset outSize xs  =
           let
             hash = case input of
                      ConcreteBuffer input' -> ConcreteBuffer $ BS.pack $ BA.unpack $ (Crypto.hash input' :: Digest SHA256)
-                     SymbolicBuffer input' -> SymbolicBuffer $ symSHA256 input'
+                     StaticSymBuffer input' -> StaticSymBuffer $ symSHA256 input'
           in do
             assign (state . stack) (1 : xs)
             assign (state . returndata) hash
@@ -1624,7 +1624,7 @@ finalize = do
   let
     burnRemainingGas = use (state . gas) >>= flip burn noop
     revertContracts  = use (tx . txReversion) >>= assign (env . contracts)
-    revertSubstate   = assign (tx . substate) (SubState mempty mempty mempty)
+    revertSubstate   = assign (tx . substate) (SubState mempty mempty 0)
 
   use result >>= \case
     Nothing ->
@@ -1647,7 +1647,7 @@ finalize = do
   -- compute and pay the refund to the caller and the
   -- corresponding payment to the miner
   txOrigin     <- use (tx . origin)
-  sumRefunds   <- (sum . (snd <$>)) <$> (use (tx . substate . refunds))
+  sumRefunds   <- use (tx . substate . refunds)
   miner        <- use (block . coinbase)
   blockReward  <- r_block <$> (use (block . schedule))
   gasPrice     <- use (tx . gasprice)
@@ -1721,8 +1721,13 @@ notStatic continue = do
     then vmError StateChangeWhileStatic
     else continue
 
+burnSym :: SymWord -> EVM () -> EVM ()
+burnSym n continue = case maybeLitWord n of
+  Nothing -> continue -- smt query (TODO: no gas mode)
+  Just n' -> burn n' continue
+
 -- | Burn gas, failing if insufficient gas is available
-burn :: Word -> EVM () -> EVM ()
+burn :: Word -> EVM () -> EVM()
 burn n continue = do
   available <- use (state . gas)
   if n <= available
@@ -1769,23 +1774,30 @@ forceConcrete6 (k,l,m,n,o,p) continue = case (maybeLitWord k, maybeLitWord l, ma
   _ -> vmError UnexpectedSymbolicArg
 
 forceConcreteBuffer :: Buffer -> (ByteString -> EVM ()) -> EVM ()
-forceConcreteBuffer (SymbolicBuffer b) continue = case maybeLitBytes b of
+forceConcreteBuffer (StaticSymBuffer b) continue = case maybeLitBytes b of
   Nothing -> vmError UnexpectedSymbolicArg
   Just bs -> continue bs
 forceConcreteBuffer (ConcreteBuffer b) continue = continue b
 
 -- * Substate manipulation
+refundSym :: SymWord -> EVM ()
+refundSym n = case maybeLitWord n of
+  Nothing -> refund 0 -- TODO: make refunds symbolic
+  Just n' -> refund n'
+
 refund :: Word -> EVM ()
 refund n = do
   self <- use (state . contract)
-  pushTo (tx . substate . refunds) (self, n)
+  tx . substate . refunds += n
+
+unRefundSym :: SymWord -> EVM ()
+unRefundSym n = case maybeLitWord n of
+  Nothing -> unRefund 0 --TODO: make refunds symbolic
+  Just n' -> unRefund n'  
 
 unRefund :: Word -> EVM ()
 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)
+  tx . substate . refunds -= n
 
 touchAccount :: Addr -> EVM()
 touchAccount = pushTo ((tx . substate) . touchedAccounts)
@@ -1804,39 +1816,37 @@ cheatCode = num (keccak "hevm cheat code")
 
 cheat
   :: (?op :: Word8)
-  => (Word, Word) -> (Word, Word)
+  => SymWord -> SymWord -> SymWord -> SymWord
   -> EVM ()
-cheat (inOffset, inSize) (outOffset, outSize) = do
-  mem <- use (state . memory)
-  vm <- get
-  let
-    abi = readMemoryWord32 inOffset mem
-    input = readMemory (inOffset + 4) (inSize - 4) vm
-  case fromSized <$> unliteral abi of
-    Nothing -> vmError UnexpectedSymbolicArg
-    Just abi ->
-              case Map.lookup abi cheatActions of
-                Nothing ->
+cheat inOffset' inSize' outOffset' outSize' =
+  case (maybeLitWord inOffset', maybeLitWord inSize', maybeLitWord outOffset', maybeLitWord outSize') of
+    (Just inOffset, Just inSize, Just outOffset, Just outSize) -> do
+      mem <- use (state . memory)
+      vm <- get
+      let
+        abi' = readMemoryWord32 inOffset' mem
+        input = readMemory (inOffset' + 4) (inSize' - 4) vm
+      forceConcrete (sw256 $ sFromIntegral abi') $ \(num -> abi) -> forceConcreteBuffer input $ \input' ->
+         case Map.lookup abi cheatActions of
+           Nothing ->
+             vmError (BadCheatCode (Just abi))
+           Just (argTypes, action) ->
+              case runGetOrFail
+                     (getAbiSeq (length argTypes) argTypes)
+                     (LS.fromStrict input') of
+                Right ("", _, args) ->
+                  action (toList args) >>= \case
+                    Nothing -> do
+                      next
+                      push 1
+                    Just (encodeAbiValue -> bs) -> do
+                      next
+                      modifying (state . memory)
+                        (writeMemory (ConcreteBuffer bs) outSize' 0 outOffset')
+                      push 1
+                _ ->
                   vmError (BadCheatCode (Just abi))
-                Just (argTypes, action) ->
-                  case input of
-                    SymbolicBuffer _ -> vmError UnexpectedSymbolicArg
-                    ConcreteBuffer input' ->
-                      case runGetOrFail
-                             (getAbiSeq (length argTypes) argTypes)
-                             (LS.fromStrict input') of
-                        Right ("", _, args) ->
-                          action (toList args) >>= \case
-                            Nothing -> do
-                              next
-                              push 1
-                            Just (encodeAbiValue -> bs) -> do
-                              next
-                              modifying (state . memory)
-                                (writeMemory (ConcreteBuffer bs) outSize 0 outOffset)
-                              push 1
-                        _ ->
-                          vmError (BadCheatCode (Just abi))
+    _ -> vmError UnexpectedSymbolicArg
 
 type CheatAction = ([AbiType], [AbiValue] -> EVM (Maybe AbiValue))
 
@@ -1865,7 +1875,7 @@ cheatActions =
 -- * General call implementation ("delegateCall")
 delegateCall
   :: (?op :: Word8)
-  => Contract -> Word -> Addr -> Addr -> Word -> Word -> Word -> Word -> Word -> [SymWord]
+  => Contract -> Word -> Addr -> Addr -> Word -> SymWord -> SymWord -> SymWord -> SymWord -> [SymWord]
   -> EVM ()
   -> EVM ()
 delegateCall this gasGiven xTo xContext xValue xInOffset xInSize xOutOffset xOutSize xs continue =
@@ -1885,12 +1895,11 @@ delegateCall this gasGiven xTo xContext xValue xInOffset xInSize xOutOffset xOut
                   , callContextReversion = view (env . contracts) vm0
                   , callContextSubState = view (tx . substate) vm0
                   , callContextAbi =
-                      if xInSize >= 4
-                      then case unliteral $ readMemoryWord32 xInOffset (view (state . memory) vm0)
-                           of Nothing -> Nothing
-                              Just abi -> Just . w256 $ num abi
+                      if maybe False (<= 4) $ maybeLitWord xInSize
+                      then do abi <- unliteral $ readMemoryWord32 xInOffset (view (state . memory) vm0)
+                              return $ w256 $ num abi
                       else Nothing
-                  , callContextData = (readMemory (num xInOffset) (num xInSize) vm0)
+                  , callContextData = (readMemory xInOffset xInSize vm0)
                   }
 
             pushTrace (FrameTrace newContext)
@@ -1911,11 +1920,11 @@ delegateCall this gasGiven xTo xContext xValue xInOffset xInSize xOutOffset xOut
               assign memory mempty
               assign memorySize 0
               assign returndata mempty
-              assign calldata (readMemory (num xInOffset) (num xInSize) vm0, literal (num xInSize))
+              assign calldata (CalldataBuffer $ readMemory xInOffset xInSize vm0)
 
             continue
 
--- -- * Contract creation
+-- * Contract creation
 
 -- EIP 684
 collision :: Maybe Contract -> Bool
@@ -2066,7 +2075,7 @@ finishFrame how = do
             ErrorTrace e
           FrameReverted (ConcreteBuffer output) ->
             ErrorTrace (Revert output)
-          FrameReverted (SymbolicBuffer output) ->
+          FrameReverted (StaticSymBuffer output) ->
             ErrorTrace (Revert (forceLitBytes output))
           FrameReturned output ->
             ReturnTrace output (view frameContext nextFrame)
@@ -2088,7 +2097,7 @@ finishFrame how = do
       case view frameContext nextFrame of
 
         -- Were we calling?
-        CallContext (num -> outOffset) (num -> outSize) _ _ _ reversion substate' -> do
+        CallContext outOffset outSize _ _ _ reversion substate' -> do
 
           let
             revertContracts = assign (env . contracts) reversion
@@ -2158,59 +2167,77 @@ finishFrame how = do
 
 accessUnboundedMemoryRange
   :: FeeSchedule Word
-  -> Word
-  -> Word
+  -> SymWord
+  -> SymWord
   -> EVM ()
   -> EVM ()
-accessUnboundedMemoryRange _ _ 0 continue = continue
-accessUnboundedMemoryRange fees f l continue = do
-  m0 <- num <$> use (state . memorySize)
-  do
-    let m1 = 32 * ceilDiv (max m0 (num f + num l)) 32
-    burn (memoryCost fees m1 - memoryCost fees m0) $ do
-      assign (state . memorySize) (num m1)
+accessUnboundedMemoryRange fees f l continue =
+  if maybe False ((==) 0) (maybeLitWord l) then continue
+  -- TODO: check for l .== 0 in the symbolic case as well
+  else do
+    m0 <- use (state . memorySize)
+    let m1 = 32 * ceilSDiv (smax m0 (f + l)) 32
+    burnSym (memoryCost fees m1 - memoryCost fees m0) $ do
+      assign (state . memorySize) m1
       continue
 
 accessMemoryRange
   :: FeeSchedule Word
-  -> Word
-  -> Word
+  -> SymWord
+  -> SymWord
   -> EVM ()
   -> EVM ()
-accessMemoryRange _ _ 0 continue = continue
 accessMemoryRange fees f l continue =
-  if f + l < l
-    then vmError IllegalOverflow
-    else accessUnboundedMemoryRange fees f l continue
+  case (maybeLitWord f, maybeLitWord l) of
+    (Just f', Just l') ->
+      if f' + l' < l'
+      then vmError IllegalOverflow
+      else accessUnboundedMemoryRange fees f l continue
+
+  -- todo: consult smt here
+    _ -> accessUnboundedMemoryRange fees f l continue
 
 accessMemoryWord
-  :: FeeSchedule Word -> Word -> EVM () -> EVM ()
+  :: FeeSchedule Word -> SymWord -> EVM () -> EVM ()
 accessMemoryWord fees x = accessMemoryRange fees x 32
 
+copyCalldataToMemory
+ :: Calldata -> SymWord -> SymWord -> SymWord -> EVM ()
+copyCalldataToMemory (CalldataBuffer bf) size xOffset yOffset =
+  copyBytesToMemory bf size xOffset yOffset
+copyCalldataToMemory (CalldataDynamic (b, (S _ l))) size xOffset yOffset =
+  case (maybeLitWord size, maybeLitWord xOffset, maybeLitWord yOffset) of
+    (Just size', Just xOffset', Just yOffset') ->
+      copyBytesToMemory (StaticSymBuffer [ite (i .<= l) x 0 | (x, i) <- zip b [1..]]) (litWord size') (litWord xOffset') (litWord yOffset')
+    _ ->
+      copyBytesToMemory (DynamicSymBuffer (subList (implode b) 0 (sFromIntegral l))) size xOffset yOffset
+
 copyBytesToMemory
-  :: Buffer -> Word -> Word -> Word -> EVM ()
+  :: Buffer -> SymWord -> SymWord -> SymWord -> EVM ()
 copyBytesToMemory bs size xOffset yOffset =
-  if size == 0 then noop
-  else do
-    mem <- use (state . memory)
-    assign (state . memory) $
-      writeMemory bs size xOffset yOffset mem
+  case maybeLitWord size of
+    Just size' -> 
+      if size' == 0 then noop
+      else copyBytes
+    Nothing -> copyBytes
+  where copyBytes = do
+          mem <- use (state . memory)
+          assign (state . memory) $
+            writeMemory bs size xOffset yOffset mem
 
 copyCallBytesToMemory
-  :: Buffer -> Word -> Word -> Word -> EVM ()
-copyCallBytesToMemory bs size xOffset yOffset =
-  if size == 0 then noop
-  else do
-    mem <- use (state . memory)
-    assign (state . memory) $
-      writeMemory bs (min size (num (len bs))) xOffset yOffset mem
+  :: Buffer -> SymWord -> SymWord -> SymWord -> EVM ()
+copyCallBytesToMemory bs size xOffset yOffset = do
+  mem <- use (state . memory)
+  assign (state . memory) $
+    writeMemory bs (smin size (len bs)) xOffset yOffset mem
 
-readMemory :: Word -> Word -> VM -> Buffer
-readMemory offset size vm = sliceWithZero (num offset) (num size) (view (state . memory) vm)
+readMemory :: SymWord -> SymWord -> VM -> Buffer
+readMemory offset size vm = sliceWithZero offset size (view (state . memory) vm)
 
 word256At
   :: Functor f
-  => Word -> (SymWord -> f (SymWord))
+  => SymWord -> (SymWord -> f (SymWord))
   -> Buffer -> f Buffer
 word256At i = lens getter setter where
   getter = readMemoryWord i
@@ -2291,13 +2318,13 @@ stackOp1 cost f =
 
 stackOp2
   :: (?op :: Word8)
-  => (((SymWord), (SymWord)) -> Word)
+  => (((SymWord), (SymWord)) -> SymWord)
   -> (((SymWord), (SymWord)) -> (SymWord))
   -> EVM ()
 stackOp2 cost f =
   use (state . stack) >>= \case
     (x:y:xs) ->
-      burn (cost (x, y)) $ do
+      burnSym (cost (x, y)) $ do
         next
         state . stack .= f (x, y) : xs
     _ ->
@@ -2536,16 +2563,19 @@ costOfPrecompile (FeeSchedule {..}) precompileAddr input =
     -- ECRECOVER
     0x1 -> 3000
     -- SHA2-256
-    0x2 -> num $ (((len input + 31) `div` 32) * 12) + 60
+    0x2 -> num $ (((l input + 31) `div` 32) * 12) + 60
+      where l i = fromMaybe (error "unsupported: dynamic data to SHA256") (maybeLitWord $ len i)
     -- RIPEMD-160
-    0x3 -> num $ (((len input + 31) `div` 32) * 120) + 600
+    0x3 -> num $ (((l input + 31) `div` 32) * 120) + 600
+      where l i = fromMaybe (error "unsupported: dynamic data to RIPEMD-160") (maybeLitWord $ len i)
     -- IDENTITY
-    0x4 -> num $ (((len input + 31) `div` 32) * 3) + 15
+    0x4 -> num $ (((l input + 31) `div` 32) * 3) + 15
+      where l i = fromMaybe (error "unsupported: dynamic data to IDENTITY") (maybeLitWord $ len i)
     -- MODEXP
     0x5 -> num $ (f (num (max lenm lenb)) * num (max lene' 1)) `div` (num g_quaddivisor)
       where input' = case input of
-              SymbolicBuffer _ -> error "unsupported: symbolic MODEXP gas cost calc"
               ConcreteBuffer b -> b
+              _ -> error "unsupported: symbolic MODEXP gas cost calc"
             (lenb, lene, lenm) = parseModexpLength input'
             lene' | lene <= 32 && ez = 0
                   | lene <= 32 = num (log2 e')
@@ -2565,21 +2595,23 @@ costOfPrecompile (FeeSchedule {..}) precompileAddr input =
     -- ECMUL
     0x7 -> g_ecmul
     -- ECPAIRING
-    0x8 -> num $ ((len input) `div` 192) * (num g_pairing_point) + (num g_pairing_base)
+    0x8 -> num $ ((l input) `div` 192) * (num g_pairing_point) + (num g_pairing_base)
+      where l i = fromMaybe (error "unsupported: dynamic data to ECPAIRING") (maybeLitWord $ len i)
     -- BLAKE2
     0x9 -> let input' = case input of
-                         SymbolicBuffer _ -> error "unsupported: symbolic BLAKE2B gas cost calc"
                          ConcreteBuffer b -> b
+                         _ -> error "unsupported: symbolic BLAKE2B gas cost calc"
+                         
            in g_fround * (num $ asInteger $ lazySlice 0 4 input')
     _ -> error ("unimplemented precompiled contract " ++ show precompileAddr)
 
 -- Gas cost of memory expansion
-memoryCost :: FeeSchedule Word -> Word -> Word
+memoryCost :: FeeSchedule Word -> SymWord -> SymWord
 memoryCost FeeSchedule{..} byteCount =
   let
-    wordCount = ceilDiv byteCount 32
-    linearCost = g_memory * wordCount
-    quadraticCost = div (wordCount * wordCount) 512
+    wordCount = ceilSDiv byteCount 32
+    linearCost = litWord g_memory * wordCount
+    quadraticCost = (wordCount * wordCount) `sDiv` 512
   in
     linearCost + quadraticCost
 
@@ -2614,12 +2646,18 @@ symSHA256 bytes = case length bytes of
 ceilDiv :: (Num a, Integral a) => a -> a -> a
 ceilDiv m n = div (m + n - 1) n
 
+ceilSDiv :: (Num a, SDivisible a) => a -> a -> a
+ceilSDiv m n = (m + n - 1) `sDiv` n
+
 allButOne64th :: (Num a, Integral a) => a -> a
 allButOne64th n = n - div n 64
 
 log2 :: FiniteBits b => b -> Int
 log2 x = finiteBitSize x - 1 - countLeadingZeros x
 
+log2S :: SymWord -> SWord8
+log2S (S _ x) = 255 - sCountLeadingZeros x
+
 
 -- * Emacs setup
 
diff --git a/src/hevm/src/EVM/Concrete.hs b/src/hevm/src/EVM/Concrete.hs
index 653e5593d..b07c9d69a 100644
--- a/src/hevm/src/EVM/Concrete.hs
+++ b/src/hevm/src/EVM/Concrete.hs
@@ -7,7 +7,7 @@ import Prelude hiding (Word)
 
 import EVM.Keccak (keccak)
 import EVM.RLP
-import EVM.Types (Addr, W256 (..), num, word, padRight, word160Bytes, word256Bytes, Buffer)
+import EVM.Types
 
 import Control.Lens    ((^?), ix)
 import Data.Bits       (Bits (..), FiniteBits (..), shiftL, shiftR)
@@ -36,21 +36,6 @@ byteStringSliceWithDefaultZeroes offset size bs =
     let bs' = BS.take size (BS.drop offset bs)
     in bs' <> BS.replicate (size - BS.length bs') 0
 
--- | This type can give insight into the provenance of a term
-data Whiff = Dull
-           | FromKeccak ByteString
-           | Var String
-           | FromBytes Buffer
-           | InfixBinOp String Whiff Whiff
-           | BinOp String Whiff Whiff
-           | UnOp String Whiff
-  deriving Show
-
-w256 :: W256 -> Word
-w256 = C Dull
-
-data Word = C Whiff W256 --maybe to remove completely in the future
-
 wordValue :: Word -> W256
 wordValue (C _ x) = x
 
@@ -112,70 +97,6 @@ blobSize x = w256 (num (BS.length x))
 keccakBlob :: ByteString -> Word
 keccakBlob x = C (FromKeccak x) (keccak x)
 
-instance Show Word where
-  show (C Dull x) = show x
-  show (C (Var var) x) = var ++ ": " ++ show x
-  show (C (InfixBinOp symbol x y) z) = show x ++ symbol ++ show y  ++ ": " ++ show z
-  show (C (BinOp symbol x y) z) = symbol ++ show x ++ show y  ++ ": " ++ show z
-  show (C (UnOp symbol x) z) = symbol ++ show x ++ ": " ++ show z
-  show (C whiff x) = show whiff ++ ": " ++ show x
-
-instance Read Word where
-  readsPrec n s =
-    case readsPrec n s of
-      [(x, r)] -> [(C Dull x, r)]
-      _ -> []
-
-instance Bits Word where
-  (C _ x) .&. (C _ y) = w256 (x .&. y)
-  (C _ x) .|. (C _ y) = w256 (x .|. y)
-  (C _ x) `xor` (C _ y) = w256 (x `xor` y)
-  complement (C _ x) = w256 (complement x)
-  shift (C _ x) i = w256 (shift x i)
-  rotate (C _ x) i = w256 (rotate x i)
-  bitSize (C _ x) = bitSize x
-  bitSizeMaybe (C _ x) = bitSizeMaybe x
-  isSigned (C _ x) = isSigned x
-  testBit (C _ x) = testBit x
-  bit i = w256 (bit i)
-  popCount (C _ x) = popCount x
-
-instance FiniteBits Word where
-  finiteBitSize (C _ x) = finiteBitSize x
-  countLeadingZeros (C _ x) = countLeadingZeros x
-  countTrailingZeros (C _ x) = countTrailingZeros x
-
-instance Bounded Word where
-  minBound = w256 minBound
-  maxBound = w256 maxBound
-
-instance Eq Word where
-  (C _ x) == (C _ y) = x == y
-
-instance Enum Word where
-  toEnum i = w256 (toEnum i)
-  fromEnum (C _ x) = fromEnum x
-
-instance Integral Word where
-  quotRem (C _ x) (C _ y) =
-    let (a, b) = quotRem x y
-    in (w256 a, w256 b)
-  toInteger (C _ x) = toInteger x
-
-instance Num Word where
-  (C _ x) + (C _ y) = w256 (x + y)
-  (C _ x) * (C _ y) = w256 (x * y)
-  abs (C _ x) = w256 (abs x)
-  signum (C _ x) = w256 (signum x)
-  fromInteger x = w256 (fromInteger x)
-  negate (C _ x) = w256 (negate x)
-
-instance Real Word where
-  toRational (C _ x) = toRational x
-
-instance Ord Word where
-  compare (C _ x) (C _ y) = compare x y
-
 -- Copied from the standard library just to get specialization.
 -- We also use bit operations instead of modulo and multiply.
 -- (This operation was significantly slow.)
diff --git a/src/hevm/src/EVM/Emacs.hs b/src/hevm/src/EVM/Emacs.hs
index 788f47e74..e348d11ae 100644
--- a/src/hevm/src/EVM/Emacs.hs
+++ b/src/hevm/src/EVM/Emacs.hs
@@ -42,6 +42,7 @@ import qualified Data.Set as Set
 import qualified Data.Vector as Vector
 import qualified EVM.Fetch as Fetch
 import qualified EVM.Stepper as Stepper
+import qualified Data.ByteString as BS
 
 data UiVmState = UiVmState
   { _uiVm             :: VM
@@ -462,7 +463,7 @@ instance SDisplay (SWord 8) where
 
 -- no idea what's going on here
 instance SDisplay Buffer where
-  sexp (SymbolicBuffer x) = sexp x
+  sexp (StaticSymBuffer x) = sexp x
   sexp (ConcreteBuffer x) = sexp x
 
 instance (SDisplay k, SDisplay v) => SDisplay (Map k v) where
@@ -509,10 +510,11 @@ instance SDisplay ByteString where
   sexp = A . txt . pack . show . ByteStringS
 
 sexpMemory :: Buffer -> SExpr Text
-sexpMemory bs =
-  if len bs > 1024
-  then L [A "large-memory", A (txt (len bs))]
-  else sexp bs
+sexpMemory (ConcreteBuffer bs) =
+  if BS.length bs > 1024
+  then L [A "large-memory", A (txt (BS.length bs))]
+  else sexp (ConcreteBuffer bs)
+sexpMemory bs = sexp bs
 
 defaultUnitTestOptions :: MonadIO m => m UnitTestOptions
 defaultUnitTestOptions = do
diff --git a/src/hevm/src/EVM/Exec.hs b/src/hevm/src/EVM/Exec.hs
index 20954dd06..0fede87b7 100644
--- a/src/hevm/src/EVM/Exec.hs
+++ b/src/hevm/src/EVM/Exec.hs
@@ -2,7 +2,7 @@ module EVM.Exec where
 
 import EVM
 import EVM.Concrete (createAddress)
-import EVM.Symbolic (litAddr)
+import EVM.Symbolic (litAddr, Calldata(..))
 import EVM.Types
 
 import qualified EVM.FeeSchedule as FeeSchedule
@@ -22,7 +22,7 @@ vmForEthrunCreation :: ByteString -> VM
 vmForEthrunCreation creationCode =
   (makeVm $ VMOpts
     { vmoptContract = initialContract (InitCode creationCode)
-    , vmoptCalldata = (mempty, 0)
+    , vmoptCalldata = CalldataBuffer mempty
     , vmoptValue = 0
     , vmoptAddress = createAddress ethrunAddress 1
     , vmoptCaller = litAddr ethrunAddress
diff --git a/src/hevm/src/EVM/Fetch.hs b/src/hevm/src/EVM/Fetch.hs
index 443940148..4050a3d14 100644
--- a/src/hevm/src/EVM/Fetch.hs
+++ b/src/hevm/src/EVM/Fetch.hs
@@ -152,15 +152,18 @@ oracle smtstate info model ensureConsistency q = do
           EVM.ConcreteS -> return $ continue x
           EVM.InitialS  -> return $ continue $ x
              & set EVM.storage (EVM.Symbolic $ SBV.sListArray 0 [])
+             & set EVM.origStorage (EVM.Symbolic $ SBV.sListArray 0 [])
           EVM.SymbolicS -> case smtstate of
             Nothing -> return (continue $ x
-                               & set EVM.storage (EVM.Symbolic $ SBV.sListArray 0 []))
+                               & set EVM.storage (EVM.Symbolic $ SBV.sListArray 0 [])
+                               & set EVM.origStorage (EVM.Symbolic $ SBV.sListArray 0 []))
 
-            Just state ->
+            Just state -> 
               flip runReaderT state $ SBV.runQueryT $ do
                 store <- freshArray_ Nothing
                 return $ continue $ x
                   & set EVM.storage (EVM.Symbolic store)
+                  & set EVM.origStorage (EVM.Symbolic store)
         Nothing -> error ("oracle error: " ++ show q)
 
     --- for other queries (there's only slot left right now) we default to zero or http
@@ -181,7 +184,11 @@ type Fetcher = EVM.Query -> IO (EVM ())
 checksat :: SBool -> Query CheckSatResult
 checksat b = do push 1
                 constrain b
-                m <- checkSat
+                b <- getInfo Name
+                m <- case b of
+                       -- some custom strategies for z3 which have proven to be quite useful (can still be tweaked)
+                       Resp_Name "Z3" -> checkSatUsing "(check-sat-using (then (using-params simplify :push_ite_bv true :ite_extra_rules true) smt))"
+                       _ -> checkSat
                 pop 1
                 return m
 
diff --git a/src/hevm/src/EVM/Format.hs b/src/hevm/src/EVM/Format.hs
index 393d42a6c..dcd08adae 100644
--- a/src/hevm/src/EVM/Format.hs
+++ b/src/hevm/src/EVM/Format.hs
@@ -114,7 +114,7 @@ formatBytes b =
     else formatBinary b
 
 formatSBytes :: Buffer -> Text
-formatSBytes (SymbolicBuffer b) = "<" <> pack (show (length b)) <> " symbolic bytes>"
+formatSBytes (StaticSymBuffer b) = "<" <> pack (show (length b)) <> " symbolic bytes>"
 formatSBytes (ConcreteBuffer b) = formatBytes b
 
 formatQString :: ByteString -> Text
@@ -124,7 +124,7 @@ formatString :: ByteString -> Text
 formatString bs = decodeUtf8 (fst (BS.spanEnd (== 0) bs))
 
 formatSString :: Buffer -> Text
-formatSString (SymbolicBuffer bs) = "<" <> pack (show (length bs)) <> " symbolic bytes (string)>"
+formatSString (StaticSymBuffer bs) = "<" <> pack (show (length bs)) <> " symbolic bytes (string)>"
 formatSString (ConcreteBuffer bs) = formatString bs
 
 formatBinary :: ByteString -> Text
@@ -132,7 +132,7 @@ formatBinary =
   (<>) "0x" . decodeUtf8 . toStrict . toLazyByteString . byteStringHex
 
 formatSBinary :: Buffer -> Text
-formatSBinary (SymbolicBuffer bs) = "<" <> pack (show (length bs)) <> " symbolic bytes>"
+formatSBinary (StaticSymBuffer bs) = "<" <> pack (show (length bs)) <> " symbolic bytes>"
 formatSBinary (ConcreteBuffer bs) = formatBinary bs
 
 showTraceTree :: DappInfo -> VM -> Text
@@ -250,7 +250,7 @@ getAbiTypes abi = map (parseTypeName mempty) types
         splitOn "," (dropEnd 1 (last (splitOn "(" abi)))
 
 showCall :: [AbiType] -> Buffer -> Text
-showCall ts (SymbolicBuffer bs) = showValues ts $ SymbolicBuffer (drop 4 bs)
+showCall ts (StaticSymBuffer bs) = showValues ts $ StaticSymBuffer (drop 4 bs)
 showCall ts (ConcreteBuffer bs) = showValues ts $ ConcreteBuffer (BS.drop 4 bs)
 
 showError :: ByteString -> Text
@@ -260,14 +260,14 @@ showError bs = case BS.take 4 bs of
   _             -> formatBinary bs
 
 showValues :: [AbiType] -> Buffer -> Text
-showValues ts (SymbolicBuffer sbs) = "symbolic: " <> (pack . show $ AbiTupleType (fromList ts))
+showValues ts (StaticSymBuffer sbs) = "symbolic: " <> (pack . show $ AbiTupleType (fromList ts))
 showValues ts (ConcreteBuffer bs) =
   case runGetOrFail (getAbiSeq (length ts) ts) (fromStrict bs) of
     Right (_, _, xs) -> showAbiValues xs
     Left (_, _, _)   -> formatBinary bs
 
 showValue :: AbiType -> Buffer -> Text
-showValue t (SymbolicBuffer _) = "symbolic: " <> (pack $ show t)
+showValue t (StaticSymBuffer _) = "symbolic: " <> (pack $ show t)
 showValue t (ConcreteBuffer bs) =
   case runGetOrFail (getAbi t) (fromStrict bs) of
     Right (_, _, x) -> showAbiValue x
diff --git a/src/hevm/src/EVM/SymExec.hs b/src/hevm/src/EVM/SymExec.hs
index dac85ad83..8c13bf8f7 100644
--- a/src/hevm/src/EVM/SymExec.hs
+++ b/src/hevm/src/EVM/SymExec.hs
@@ -16,10 +16,11 @@ import EVM.Stepper (Stepper)
 import qualified EVM.Stepper as Stepper
 import qualified Control.Monad.Operational as Operational
 import EVM.Types hiding (Word)
-import EVM.Symbolic (SymWord(..), sw256)
+import EVM.Symbolic (SymWord(..), sw256, Calldata(..))
 import EVM.Concrete (createAddress, Word)
 import qualified EVM.FeeSchedule as FeeSchedule
 import Data.SBV.Trans.Control
+import qualified Data.SBV.List as SList
 import Data.SBV.Trans hiding (distinct, Word)
 import Data.SBV hiding (runSMT, newArray_, addAxiom, distinct, sWord8s, Word)
 import Data.Vector (toList, fromList)
@@ -45,33 +46,31 @@ sbytes1024 = liftA2 (++) sbytes512 sbytes512
 -- We don't assume input types are restricted to their proper range here;
 -- such assumptions should instead be given as preconditions.
 -- This could catch some interesting calldata mismanagement errors.
-symAbiArg :: AbiType -> Query ([SWord 8], SWord 32)
-symAbiArg (AbiUIntType n) | n `mod` 8 == 0 && n <= 256 = do x <- sbytes32
-                                                            return (x, 32)
-                          | otherwise = error "bad type"
+symAbiArg :: AbiType -> Query [SWord 8]
+symAbiArg (AbiUIntType n)
+  | n `mod` 8 == 0 && n <= 256 = sbytes32
+  | otherwise = error "bad type"
 
-symAbiArg (AbiIntType n)  | n `mod` 8 == 0 && n <= 256 = do x <- sbytes32
-                                                            return (x, 32)
-                          | otherwise = error "bad type"
-symAbiArg AbiBoolType = do x <- sbytes32
-                           return (x, 32)
+symAbiArg (AbiIntType n)
+  | n `mod` 8 == 0 && n <= 256 = sbytes32
+  | otherwise = error "bad type"
 
-symAbiArg AbiAddressType = do x <- sbytes32
-                              return (x, 32)
+symAbiArg AbiBoolType = sbytes32
 
-symAbiArg (AbiBytesType n) | n <= 32 = do x <- sbytes32
-                                          return (x, 32)
-                           | otherwise = error "bad type"
+symAbiArg AbiAddressType = sbytes32
+
+symAbiArg (AbiBytesType n)
+  | n <= 32 = sbytes32
+  | otherwise = error "bad type"
 
 -- TODO: is this encoding correct?
 symAbiArg (AbiArrayType len typ) =
-  do args <- mapM symAbiArg (replicate len typ)
-     return (litBytes (encodeAbiValue (AbiUInt 256 (fromIntegral len))) <> (concat $ fst <$> args),
-             32 + (sum $ snd <$> args))
+  do args <- mconcat <$> mapM symAbiArg (replicate len typ)
+     return $ litBytes (encodeAbiValue (AbiUInt 256 (fromIntegral len))) <> args
 
 symAbiArg (AbiTupleType tuple) =
-  do args <- mapM symAbiArg (toList tuple)
-     return (concat $ fst <$> args, sum $ snd <$> args)
+  mconcat <$> mapM symAbiArg (toList tuple)
+
 symAbiArg n =
   error $ "Unsupported symbolic abiencoding for"
     <> show n
@@ -81,34 +80,52 @@ symAbiArg n =
 -- with concrete arguments.
 -- Any argument given as "<symbolic>" or omitted at the tail of the list are
 -- kept symbolic.
-symCalldata :: Text -> [AbiType] -> [String] -> Query ([SWord 8], SWord 32)
-symCalldata sig typesignature concreteArgs =
-  let args = concreteArgs <> replicate (length typesignature - length concreteArgs)  "<symbolic>"
-      mkArg typ "<symbolic>" = symAbiArg typ
-      mkArg typ arg = let n = litBytes . encodeAbiValue $ makeAbiValue typ arg
-                      in return (n, num (length n))
-      sig' = litBytes $ selector sig
-  in do calldatas <- zipWithM mkArg typesignature args
-        return (sig' <> concat (fst <$> calldatas), 4 + (sum $ snd <$> calldatas))
-
-abstractVM :: Maybe (Text, [AbiType]) -> [String] -> ByteString -> StorageModel -> Query VM
-abstractVM typesignature concreteArgs x storagemodel = do
-  (cd', cdlen, cdconstraint) <-
-    case typesignature of
-      Nothing -> do cd <- sbytes256
-                    len <- freshVar_
-                    return (cd, len, len .<= 256)
-      Just (name, typs) -> do (cd, cdlen) <- symCalldata name typs concreteArgs
-                              return (cd, cdlen, sTrue)
+staticCalldata :: Text -> [AbiType] -> [String] -> Query [SWord 8]
+staticCalldata sig typesignature concreteArgs =
+  fmap (sig' <>) $ concat <$> zipWithM mkArg typesignature args
+  where
+    -- ensure arg length is long enough
+    args = concreteArgs <> replicate (length typesignature - length concreteArgs)  "<symbolic>"
+
+    mkArg :: AbiType -> String -> Query [SWord 8]
+    mkArg typ "<symbolic>" = symAbiArg typ
+    mkArg typ arg = return $ litBytes . encodeAbiValue $ makeAbiValue typ arg
+
+    sig' = litBytes $ selector sig
+
+-- | Construct a VM out of a type signature, possibly with specialized concrete arguments
+-- ,bytecode, storagemodel and calldata structure.
+abstractVM :: Maybe (Text, [AbiType]) -> [String] -> ByteString -> StorageModel -> CalldataModel -> Query VM
+abstractVM typesignature concreteArgs x storagemodel calldatamodel = do
+  (cd',pathCond) <- case typesignature of
+           Nothing -> case calldatamodel of
+                        DynamicCD -> do
+                          list <- freshVar_
+                          return (CalldataBuffer (DynamicSymBuffer list),
+                            -- due to some current z3 shenanegans (possibly related to: https://github.com/Z3Prover/z3/issues/4635)
+                            -- we assume the list length to be shorter than max_length both as a bitvector and as an integer.
+                            -- The latter implies the former as long as max_length fits in a bitvector, but assuming it explitly
+                            -- improves z3 (4.8.8) performance.
+                            SList.length list .< 1000 .&&
+                             sw256 (sFromIntegral (SList.length list)) .< sw256 1000)
+
+                        BoundedCD -> do
+                           cd <- sbytes256
+                           len <- sw256 <$> freshVar_
+                           return (CalldataDynamic (cd, len), len .<= 256)
+           Just (name, typs) -> do symbytes <- staticCalldata name typs concreteArgs
+                                   return (CalldataBuffer (StaticSymBuffer symbytes), sTrue)
+
   symstore <- case storagemodel of
     SymbolicS -> Symbolic <$> freshArray_ Nothing
     InitialS -> Symbolic <$> freshArray_ (Just 0)
     ConcreteS -> return $ Concrete mempty
   c <- SAddr <$> freshVar_
   value' <- sw256 <$> freshVar_
-  return $ loadSymVM (RuntimeCode x) symstore storagemodel c value' (SymbolicBuffer cd', cdlen) & over pathConditions ((<>) [cdconstraint])
+  return $ loadSymVM (RuntimeCode x) symstore storagemodel c value' cd'
+    & over pathConditions (<> [pathCond])
 
-loadSymVM :: ContractCode -> Storage -> StorageModel -> SAddr -> SymWord -> (Buffer, SWord 32) -> VM
+loadSymVM :: ContractCode -> Storage -> StorageModel -> SAddr -> SymWord -> Calldata -> VM
 loadSymVM x initStore model addr callvalue' calldata' =
     (makeVm $ VMOpts
     { vmoptContract = contractWithStore x initStore
@@ -135,8 +152,8 @@ loadSymVM x initStore model addr callvalue' calldata' =
 
 
 -- | Interpreter which explores all paths at
--- | branching points.
--- | returns a list of possible final evm states
+-- branching points.
+-- returns a list of possible final evm states
 interpret
   :: Fetch.Fetcher
   -> Maybe Integer --max iterations
@@ -204,17 +221,21 @@ maxIterationsReached vm (Just maxIter) =
 type Precondition = VM -> SBool
 type Postcondition = (VM, VM) -> SBool
 
+checkAssertDynamic :: ByteString -> Query (Either (VM, [VM]) VM)
+checkAssertDynamic c = verifyContract c Nothing [] SymbolicS DynamicCD (const sTrue) (Just checkAssertions)
+
+
 checkAssert :: ByteString -> Maybe (Text, [AbiType]) -> [String] -> Query (Either (VM, [VM]) VM)
-checkAssert c signature' concreteArgs = verifyContract c signature' concreteArgs SymbolicS (const sTrue) (Just checkAssertions)
+checkAssert c signature' concreteArgs = verifyContract c signature' concreteArgs SymbolicS BoundedCD (const sTrue) (Just checkAssertions)
 
 checkAssertions :: Postcondition
 checkAssertions (_, out) = case view result out of
   Just (EVM.VMFailure (EVM.UnrecognizedOpcode 254)) -> sFalse
   _ -> sTrue
 
-verifyContract :: ByteString -> Maybe (Text, [AbiType]) -> [String] -> StorageModel -> Precondition -> Maybe Postcondition -> Query (Either (VM, [VM]) VM)
-verifyContract theCode signature' concreteArgs storagemodel pre maybepost = do
-    preStateRaw <- abstractVM signature' concreteArgs theCode  storagemodel
+verifyContract :: ByteString -> Maybe (Text, [AbiType]) -> [String] -> StorageModel -> CalldataModel -> Precondition -> Maybe Postcondition -> Query (Either (VM, [VM]) VM)
+verifyContract theCode signature' concreteArgs storagemodel calldatamodel pre maybepost = do
+    preStateRaw <- abstractVM signature' concreteArgs theCode  storagemodel calldatamodel
     -- add the pre condition to the pathconditions to ensure that we are only exploring valid paths
     let preState = over pathConditions ((++) [pre preStateRaw]) preStateRaw
     verify preState Nothing Nothing maybepost
@@ -256,15 +277,15 @@ verify preState maxIter rpcinfo maybepost = do
 -- | Compares two contract runtimes for trace equivalence by running two VMs and comparing the end states.
 equivalenceCheck :: ByteString -> ByteString -> Maybe Integer -> Maybe (Text, [AbiType]) -> Query (Either ([VM], [VM]) VM)
 equivalenceCheck bytecodeA bytecodeB maxiter signature' = do
-  preStateA <- abstractVM signature' [] bytecodeA SymbolicS
+  preStateA <- abstractVM signature' [] bytecodeA SymbolicS BoundedCD
 
   let preself = preStateA ^. state . contract
       precaller = preStateA ^. state . caller
       callvalue' = preStateA ^. state . callvalue
       prestorage = preStateA ^?! env . contracts . ix preself . storage
-      (calldata', cdlen) = view (state . calldata) preStateA
+      calldata' = view (state . calldata) preStateA
       pathconds = view pathConditions preStateA
-      preStateB = loadSymVM (RuntimeCode bytecodeB) prestorage SymbolicS precaller callvalue' (calldata', cdlen) & set pathConditions pathconds
+      preStateB = loadSymVM (RuntimeCode bytecodeB) prestorage SymbolicS precaller callvalue' calldata' & set pathConditions pathconds
 
   smtState <- queryState
   push 1
@@ -304,7 +325,8 @@ equivalenceCheck bytecodeA bytecodeB maxiter signature' = do
   constrain $ sOr differingEndStates
 
   checkSat >>= \case
-     Unk -> error "solver said unknown!"
+     Unk -> do io $ putStrLn "postcondition query timed out"
+               return $ Left (pruneDeadPaths aVMs, pruneDeadPaths bVMs)
      Sat -> return $ Right preStateA
      Unsat -> return $ Left (pruneDeadPaths aVMs, pruneDeadPaths bVMs)
 
@@ -313,13 +335,17 @@ both' f (x, y) = (f x, f y)
 
 showCounterexample :: VM -> Maybe (Text, [AbiType]) -> Query ()
 showCounterexample vm maybesig = do
-  let (calldata', cdlen) = view (EVM.state . EVM.calldata) vm
+  let calldata' = view (EVM.state . EVM.calldata) vm
       S _ cvalue = view (EVM.state . EVM.callvalue) vm
       SAddr caller' = view (EVM.state . EVM.caller) vm
-  cdlen' <- num <$> getValue cdlen
+--  cdlen' <- num <$> getValue cdlen
   calldatainput <- case calldata' of
-    SymbolicBuffer cd -> mapM (getValue.fromSized) (take cdlen' cd) >>= return . pack
-    ConcreteBuffer cd -> return $ BS.take cdlen' cd
+    CalldataDynamic (cd, (S _ cdlen)) -> do
+      cdlen' <- num <$> getValue cdlen
+      mapM (getValue.fromSized) (take cdlen' cd) >>= return . pack
+    CalldataBuffer (StaticSymBuffer cd) -> mapM (getValue.fromSized) cd >>= return . pack
+    CalldataBuffer (ConcreteBuffer cd)  -> return $ cd
+    CalldataBuffer (DynamicSymBuffer cd) -> (fmap fromSized) <$> getValue cd >>= return . pack
   callvalue' <- num <$> getValue cvalue
   caller'' <- num <$> getValue caller'
   io $ do
diff --git a/src/hevm/src/EVM/Symbolic.hs b/src/hevm/src/EVM/Symbolic.hs
index 606bc6438..cc5ea67a1 100644
--- a/src/hevm/src/EVM/Symbolic.hs
+++ b/src/hevm/src/EVM/Symbolic.hs
@@ -10,21 +10,20 @@ import qualified Data.ByteString as BS
 import Data.ByteString (ByteString)
 import Control.Lens hiding (op, (:<), (|>), (.>))
 import Data.Maybe                   (fromMaybe, fromJust)
-
 import EVM.Types
-import EVM.Concrete (Word (..), Whiff(..))
 import qualified EVM.Concrete as Concrete
 import Data.SBV hiding (runSMT, newArray_, addAxiom, Word)
-
-
--- | Symbolic words of 256 bits, possibly annotated with additional
---   "insightful" information
-data SymWord = S Whiff (SWord 256)
+import qualified Data.SBV.List as SL
+import Data.SBV.List ((.++), (.!!))
 
 -- | Convenience functions transporting between the concrete and symbolic realm
 sw256 :: SWord 256 -> SymWord
 sw256 = S Dull
 
+bv2int :: SymWord -> SInteger
+bv2int (S _ i) = sFromIntegral i
+--snum = sFromIntegral
+
 litWord :: Word -> (SymWord)
 litWord (C whiff a) = S whiff (literal $ toSizzle a)
 
@@ -34,9 +33,6 @@ w256lit = S Dull . literal . toSizzle
 litAddr :: Addr -> SAddr
 litAddr = SAddr . literal . toSizzle
 
-maybeLitWord :: SymWord -> Maybe Word
-maybeLitWord (S whiff a) = fmap (C whiff . fromSizzle) (unliteral a)
-
 maybeLitAddr :: SAddr -> Maybe Addr
 maybeLitAddr (SAddr a) = fmap fromSizzle (unliteral a)
 
@@ -58,7 +54,8 @@ forceLitBytes = BS.pack . fmap (fromSized . fromJust . unliteral)
 
 forceBuffer :: Buffer -> ByteString
 forceBuffer (ConcreteBuffer b) = b
-forceBuffer (SymbolicBuffer b) = forceLitBytes b
+forceBuffer (StaticSymBuffer b) = forceLitBytes b
+forceBuffer _ = error "unexpected symbolic argument"
 
 -- | Arithmetic operations on SymWord
 
@@ -94,153 +91,306 @@ sgt (S _ x) (S _ y) =
 
 shiftRight' :: SymWord -> SymWord -> SymWord
 shiftRight' (S _ a') b@(S _ b') = case (num <$> unliteral a', b) of
-  (Just n, (S (FromBytes (SymbolicBuffer a)) _)) | n `mod` 8 == 0 && n <= 256 ->
+  (Just n, (S (FromBytes (StaticSymBuffer a)) _)) | n `mod` 8 == 0 && n <= 256 ->
     let bs = replicate (n `div` 8) 0 <> (take ((256 - n) `div` 8) a)
-    in S (FromBytes (SymbolicBuffer bs)) (fromBytes bs)
+    in S (FromBytes (StaticSymBuffer bs)) (fromBytes bs)
   _ -> sw256 $ sShiftRight b' a'
 
--- | Operations over symbolic memory (list of symbolic bytes)
-swordAt :: Int -> [SWord 8] -> SymWord
-swordAt i bs = sw256 . fromBytes $ truncpad 32 $ drop i bs
-
-readByteOrZero' :: Int -> [SWord 8] -> SWord 8
-readByteOrZero' i bs = fromMaybe 0 (bs ^? ix i)
-
-sliceWithZero' :: Int -> Int -> [SWord 8] -> [SWord 8]
-sliceWithZero' o s m = truncpad s $ drop o m
-
-writeMemory' :: [SWord 8] -> Word -> Word -> Word -> [SWord 8] -> [SWord 8]
-writeMemory' bs1 (C _ n) (C _ src) (C _ dst) bs0 =
-  let
-    (a, b) = splitAt (num dst) bs0
-    a'     = replicate (num dst - length a) 0
-    c      = if src > num (length bs1)
-             then replicate (num n) 0
-             else sliceWithZero' (num src) (num n) bs1
-    b'     = drop (num (n)) b
-  in
-    a <> a' <> c <> b'
-
-readMemoryWord' :: Word -> [SWord 8] -> SymWord
-readMemoryWord' (C _ i) m = sw256 $ fromBytes $ truncpad 32 (drop (num i) m)
-
-readMemoryWord32' :: Word -> [SWord 8] -> SWord 32
-readMemoryWord32' (C _ i) m = fromBytes $ truncpad 4 (drop (num i) m)
-
-setMemoryWord' :: Word -> SymWord -> [SWord 8] -> [SWord 8]
-setMemoryWord' (C _ i) (S _ x) =
-  writeMemory' (toBytes x) 32 0 (num i)
-
-setMemoryByte' :: Word -> SWord 8 -> [SWord 8] -> [SWord 8]
-setMemoryByte' (C _ i) x =
-  writeMemory' [x] 1 0 (num i)
-
-readSWord' :: Word -> [SWord 8] -> SymWord
-readSWord' (C _ i) x =
-  if i > num (length x)
-  then 0
-  else swordAt (num i) x
-
-
-select' :: (Ord b, Num b, SymVal b, Mergeable a) => [a] -> a -> SBV b -> a
-select' xs err ind = walk xs ind err
-    where walk []     _ acc = acc
-          walk (e:es) i acc = walk es (i-1) (ite (i .== 0) e acc)
-
--- Generates a ridiculously large set of constraints (roughly 25k) when
--- the index is symbolic, but it still seems (kind of) manageable
--- for the solvers.
-readSWordWithBound :: SWord 32 -> Buffer -> SWord 32 -> SymWord
-readSWordWithBound ind (SymbolicBuffer xs) bound = case (num <$> fromSized <$> unliteral ind, num <$> fromSized <$> unliteral bound) of
-  (Just i, Just b) ->
-    let bs = truncpad 32 $ drop i (take b xs)
-    in S (FromBytes (SymbolicBuffer bs)) (fromBytes bs)
-  _ -> 
-    let boundedList = [ite (i .<= bound) x 0 | (x, i) <- zip xs [1..]]
-    in sw256 . fromBytes $ [select' boundedList 0 (ind + j) | j <- [0..31]]
-
-readSWordWithBound ind (ConcreteBuffer xs) bound =
-  case fromSized <$> unliteral ind of
-    Nothing -> readSWordWithBound ind (SymbolicBuffer (litBytes xs)) bound
-    Just x' ->                                       
-       -- INVARIANT: bound should always be length xs for concrete bytes
-       -- so we should be able to safely ignore it here
-         litWord $ Concrete.readMemoryWord (num x') xs
-
--- a whole foldable instance seems overkill, but length is always good to have!
-len :: Buffer -> Int
-len (SymbolicBuffer bs) = length bs
-len (ConcreteBuffer bs) = BS.length bs
-
-grab :: Int -> Buffer -> Buffer
-grab n (SymbolicBuffer bs) = SymbolicBuffer $ take n bs
-grab n (ConcreteBuffer bs) = ConcreteBuffer $ BS.take n bs
-
-ditch :: Int -> Buffer -> Buffer
-ditch n (SymbolicBuffer bs) = SymbolicBuffer $ drop n bs
-ditch n (ConcreteBuffer bs) = ConcreteBuffer $ BS.drop n bs
-
-readByteOrZero :: Int -> Buffer -> SWord 8
-readByteOrZero i (SymbolicBuffer bs) = readByteOrZero' i bs
-readByteOrZero i (ConcreteBuffer bs) = num $ Concrete.readByteOrZero i bs
-
-sliceWithZero :: Int -> Int -> Buffer -> Buffer
-sliceWithZero o s (SymbolicBuffer m) = SymbolicBuffer (sliceWithZero' o s m)
-sliceWithZero o s (ConcreteBuffer m) = ConcreteBuffer (Concrete.byteStringSliceWithDefaultZeroes o s m)
-
-writeMemory :: Buffer -> Word -> Word -> Word -> Buffer -> Buffer
-writeMemory (ConcreteBuffer bs1) n src dst (ConcreteBuffer bs0) =
-  ConcreteBuffer (Concrete.writeMemory bs1 n src dst bs0)
-writeMemory (ConcreteBuffer bs1) n src dst (SymbolicBuffer bs0) =
-  SymbolicBuffer (writeMemory' (litBytes bs1) n src dst bs0)
-writeMemory (SymbolicBuffer bs1) n src dst (ConcreteBuffer bs0) =
-  SymbolicBuffer (writeMemory' bs1 n src dst (litBytes bs0))
-writeMemory (SymbolicBuffer bs1) n src dst (SymbolicBuffer bs0) =
-  SymbolicBuffer (writeMemory' bs1 n src dst bs0)
-
-readMemoryWord :: Word -> Buffer -> SymWord
-readMemoryWord i (SymbolicBuffer m) = readMemoryWord' i m
-readMemoryWord i (ConcreteBuffer m) = litWord $ Concrete.readMemoryWord i m
-
-readMemoryWord32 :: Word -> Buffer -> SWord 32
-readMemoryWord32 i (SymbolicBuffer m) = readMemoryWord32' i m
-readMemoryWord32 i (ConcreteBuffer m) = num $ Concrete.readMemoryWord32 i m
-
-setMemoryWord :: Word -> SymWord -> Buffer -> Buffer
-setMemoryWord i x (SymbolicBuffer z) = SymbolicBuffer $ setMemoryWord' i x z
-setMemoryWord i x (ConcreteBuffer z) = case maybeLitWord x of
-  Just x' -> ConcreteBuffer $ Concrete.setMemoryWord i x' z
-  Nothing -> SymbolicBuffer $ setMemoryWord' i x (litBytes z)
-
-setMemoryByte :: Word -> SWord 8 -> Buffer -> Buffer
-setMemoryByte i x (SymbolicBuffer m) = SymbolicBuffer $ setMemoryByte' i x m
-setMemoryByte i x (ConcreteBuffer m) = case fromSized <$> unliteral x of
-  Nothing -> SymbolicBuffer $ setMemoryByte' i x (litBytes m)
-  Just x' -> ConcreteBuffer $ Concrete.setMemoryByte i x' m
-
-readSWord :: Word -> Buffer -> SymWord
-readSWord i (SymbolicBuffer x) = readSWord' i x
-readSWord i (ConcreteBuffer x) = num $ Concrete.readMemoryWord i x
+-- -- | Operations over static symbolic memory (list of symbolic bytes)
+-- truncpad :: Int -> [SWord 8] -> [SWord 8]
+-- truncpad n xs = if m > n then take n xs
+--                 else mappend xs (replicate (n - m) 0)
+--   where m = length xs
+
+-- -- | Is the list concretely known empty?
+-- isConcretelyEmpty :: SymVal a => SList a -> Bool
+-- isConcretelyEmpty sl | Just l <- unliteral sl = null l
+--                      | True                   = False
+
+-- -- WARNING: only works when (n <= list length)
+-- takeStatic :: (SymVal a) => Int -> SList a -> [SBV a]
+-- takeStatic 0 ls = []
+-- takeStatic n ls = 
+--   let (x, xs) = SL.uncons ls
+--   in x:(takeStatic (n - 1) xs)
+
+-- -- tries to create a static list whenever possible
+-- dropS :: SymWord -> SList (WordN 8) -> Buffer
+-- dropS n ls =
+--   if isConcretelyEmpty ls
+--   then mempty
+--   else case (maybeLitWord n, unliteral $ SL.length ls) of
+--     (Just n', Just l) ->
+--       if n' == 0
+--       then StaticSymBuffer $ takeStatic (num $ max n' (num l)) ls
+--       else let (_, xs) = SL.uncons ls
+--            in dropS (litWord $ n' - 1) xs
+--     _ -> DynamicSymBuffer $ SL.drop (bv2int n) ls
+
+-- -- special case of sliceWithZero when size is known
+-- truncpad' :: Int -> Buffer -> Buffer
+-- truncpad' n m = case m of
+--   ConcreteBuffer xs -> ConcreteBuffer $ Concrete.byteStringSliceWithDefaultZeroes 0 n xs
+--   StaticSymBuffer xs -> StaticSymBuffer $ truncpad n xs
+--   DynamicSymBuffer xs ->
+--     case unliteral $ SL.length xs of
+
+--       Just (num -> l) -> StaticSymBuffer $
+
+--         if n <= l
+--         then takeStatic n xs
+--         else takeStatic n (xs .++ literal (replicate (n - l) 0))
+
+--       Nothing -> StaticSymBuffer $ takeStatic n (xs .++ literal (replicate n 0))
+
+-- swordAt :: Int -> [SWord 8] -> SymWord
+-- swordAt i bs = let b = truncpad 32 $ drop i bs
+--                in S (FromBytes (StaticSymBuffer b)) (fromBytes b)
+
+-- swordAt' :: SymWord -> SList (WordN 8) -> SymWord
+-- swordAt' i@(S _ i') bs =
+--  ite (sFromIntegral (SL.length bs) .<= i')
+--  (sw256 0)
+--  (case truncpad' 32 $ dropS i bs of
+--    ConcreteBuffer s -> litWord $ Concrete.w256 $ Concrete.wordAt 0 s
+--    StaticSymBuffer s -> sw256 $ fromBytes s
+--    DynamicSymBuffer s -> sw256 $ fromBytes [s .!! literal i | i <- [0..31]])
+
+-- readByteOrZero' :: Int -> [SWord 8] -> SWord 8
+-- readByteOrZero' i bs = fromMaybe 0 (bs ^? ix i)
+
+-- sliceWithZero' :: Int -> Int -> [SWord 8] -> [SWord 8]
+-- sliceWithZero' o s m = truncpad s $ drop o m
+
+-- writeMemory' :: [SWord 8] -> Word -> Word -> Word -> [SWord 8] -> [SWord 8]
+-- writeMemory' bs1 (C _ n) (C _ src) (C _ dst) bs0 =
+--   let
+--     (a, b) = splitAt (num dst) bs0
+--     a'     = replicate (num dst - length a) 0
+--     c      = if src > num (length bs1)
+--              then replicate (num n) 0
+--              else sliceWithZero' (num src) (num n) bs1
+--     b'     = drop (num n) b
+--   in
+--     a <> a' <> c <> b'
+
+-- readMemoryWord' :: Word -> [SWord 8] -> SymWord
+-- readMemoryWord' (C _ i) m = sw256 $ fromBytes $ truncpad 32 (drop (num i) m)
+
+-- readMemoryWord32' :: Word -> [SWord 8] -> SymWord
+-- readMemoryWord32' (C _ i) m = sw256 $ fromBytes $ truncpad 4 (drop (num i) m)
+
+-- setMemoryWord' :: Word -> SymWord -> [SWord 8] -> [SWord 8]
+-- setMemoryWord' (C _ i) (S _ x) =
+--   writeMemory' (toBytes x) 32 0 (num i)
+
+-- setMemoryByte' :: Word -> SWord 8 -> [SWord 8] -> [SWord 8]
+-- setMemoryByte' (C _ i) x =
+--   writeMemory' [x] 1 0 (num i)
+
+-- setMemoryByte'' :: SymWord -> SWord 8 -> Buffer -> Buffer
+-- setMemoryByte'' i x = dynWriteMemory (StaticSymBuffer [x]) 1 0 i
+
+-- readSWord' :: Word -> [SWord 8] -> SymWord
+-- readSWord' (C _ i) x =
+--   if i > num (length x)
+--   then sw256 $ 0
+--   else swordAt (num i) x
+
+-- -- | Operations over dynamic symbolic memory (smt list of bytes)
+-- readByteOrZero'' :: SymWord -> SList (WordN 8) -> SWord 8
+-- readByteOrZero'' (S _ i) bs =
+--   ite (sFromIntegral (SL.length bs) .> i + 1)
+--   (bs .!! (sFromIntegral i))
+--   (literal 0)
+
+-- -- pad up to 1000 bytes
+-- sslice :: SymWord -> SymWord -> SList (WordN 8) -> SList (WordN 8)
+-- sslice (S _ o) (S _ l) bs = case (unliteral $ SL.length bs, unliteral (o + l)) of
+--   (Just le, Just (num -> max)) ->
+--     SL.subList (if le < max then bs .++ literal (replicate (num (max - le)) 0) else bs) o' l'
+--   _ -> SL.subList (bs .++ literal (replicate 10000 0)) o' l'
+--  where o' = sFromIntegral o
+--        l' = sFromIntegral l
+
+-- sdynWriteMemory :: SList (WordN 8) -> SymWord -> SymWord -> SymWord -> SList (WordN 8) -> SList (WordN 8)
+-- sdynWriteMemory bs1 n@(S _ n') src@(S _ src') dst@(S _ dst') bs0 =
+--   let
+--     a       = sslice 0 dst bs0
+--     b       = sslice src n bs1
+--     c       = SL.drop (sFromIntegral $ dst' + n') bs0
+
+--   in
+--     a .++ b .++ c
+
+-- dynWriteMemory :: Buffer -> SymWord -> SymWord -> SymWord -> Buffer -> Buffer
+-- dynWriteMemory bs1 n@(S _ n') src@(S _ src') dst@(S _ dst') bs0 =
+--   let
+--     a       = sliceWithZero 0 dst bs0
+--     b       = sliceWithZero src n bs1
+--     c       = ditchS (sFromIntegral $ dst' + n') bs0
+
+--   in
+--     a <> b <> c
+
+-- setMemoryWord'' :: SymWord -> SymWord -> Buffer -> Buffer
+-- setMemoryWord'' i (S _ x) =
+--   dynWriteMemory (StaticSymBuffer $ toBytes x) 32 0 i
+
+-- readSWord'' :: SymWord -> SList (WordN 8) -> SymWord
+-- readSWord'' i x = case (maybeLitWord i, unliteral (SL.length x)) of
+--   (Just i', Just l) ->
+--     if num l <= i'
+--     then 0
+--     else read32At (literal $ num $ Concrete.wordValue i') (x .++ literal (replicate (num $ l + 32 - num i') 0))
+--   _ -> altReadSWord i x
+
+-- altReadSWord :: SymWord -> SList (WordN 8) -> SymWord
+-- altReadSWord (S _ i) x =
+--   ite (i .< sFromIntegral (SL.length x))
+--     (read32At (sFromIntegral i) (x .++ literal (replicate 32 0)))
+--     (sw256 0)
+
+-- read32At :: SInteger -> SList (WordN 8) -> SymWord
+-- read32At i x = sw256 $ fromBytes $ [x .!! literal i | i <- [0..31]]
+
+-- -- | Although calldata can be modeled perfectly well directly as a Buffer,
+-- -- we allow for it to take on a special form; the pair ([SWord 8], SymWord)
+-- -- where the second argument is understood as the length of the list.
+-- -- This allows us to 'fake' dynamically sized calldata arrays in a way
+-- -- that has proven more efficient than `SList`.
+-- data Calldata
+--   = CalldataBuffer Buffer
+--   | CalldataDynamic ([SWord 8], SymWord)
+--   deriving Show
+
+-- -- a whole foldable instance seems overkill, but length is always good to have!
+-- len :: Buffer -> SymWord
+-- len (DynamicSymBuffer a) = sw256 $ sFromIntegral $ SL.length a
+-- len (StaticSymBuffer bs) = litWord . num $ length bs
+-- len (ConcreteBuffer bs) = litWord . num $ BS.length bs
+
+-- cdlen :: Calldata -> SymWord
+-- cdlen (CalldataBuffer bf) = len bf
+-- cdlen (CalldataDynamic (_, a)) = a
+
+-- grab :: Int -> Buffer -> Buffer
+-- grab n (StaticSymBuffer bs) = StaticSymBuffer $ take n bs
+-- grab n (ConcreteBuffer bs) = ConcreteBuffer $ BS.take n bs
+-- grab n (DynamicSymBuffer bs) =
+--   case unliteral $ SL.length bs of
+--     Nothing -> DynamicSymBuffer $ SL.take (literal $ num n) bs
+--     Just l' -> StaticSymBuffer $ takeStatic (num $ max n (num l')) bs
+
+-- ditch :: Int -> Buffer -> Buffer
+-- ditch n (StaticSymBuffer bs) = StaticSymBuffer $ drop n bs
+-- ditch n (ConcreteBuffer bs) = ConcreteBuffer $ BS.drop n bs
+-- ditch n (DynamicSymBuffer bs) = dropS (litWord $ num n) bs
+
+-- ditchS :: SInteger -> Buffer -> Buffer
+-- ditchS n bs = case unliteral n of
+--   Nothing -> dropS (sw256 $ sFromIntegral n) (dynamize bs)
+--   Just n' -> ditch (num n') bs
+
+-- grabS :: SInteger -> Buffer -> Buffer
+-- grabS n bs = case unliteral n of
+--   Nothing -> DynamicSymBuffer $ SL.take n (dynamize bs)
+--   Just n' -> grab (num n') bs
+
+-- readByteOrZero :: Int -> Buffer -> SWord 8
+-- readByteOrZero i (StaticSymBuffer bs) = readByteOrZero' i bs
+-- readByteOrZero i (ConcreteBuffer bs) = num $ Concrete.readByteOrZero i bs
+-- readByteOrZero i (DynamicSymBuffer bs) = readByteOrZero'' (litWord $ num i) bs
+
+-- -- pad up to 1000 bytes in the dynamic case
+-- sliceWithZero :: SymWord -> SymWord -> Buffer -> Buffer
+-- sliceWithZero (S _ o) (S _ s) bf = case (unliteral o, unliteral s, bf) of
+--   (Just o', Just s', StaticSymBuffer m) -> StaticSymBuffer (sliceWithZero' (num o') (num s') m)
+--   (Just o', Just s', ConcreteBuffer m)  -> ConcreteBuffer (Concrete.byteStringSliceWithDefaultZeroes (num o') (num s') m)
+--   (Just o', Just s', m)                 -> truncpad' (num s') (ditch (num o') m)
+--   _                                     -> DynamicSymBuffer $ SL.subList (dynamize bf .++ literal (replicate 1000 0)) (sFromIntegral o) (sFromIntegral s)
+
+-- writeMemory :: Buffer -> SymWord -> SymWord -> SymWord -> Buffer -> Buffer
+-- writeMemory bs1 n src dst bs0 =
+--   case (maybeLitWord n, maybeLitWord src, maybeLitWord dst, bs0, bs1) of
+--     (Just n', Just src', Just dst', ConcreteBuffer bs0', ConcreteBuffer bs1') ->
+--       ConcreteBuffer $ Concrete.writeMemory bs1' n' src' dst' bs0'
+--     (Just n', Just src', Just dst', StaticSymBuffer bs0', ConcreteBuffer bs1') ->
+--       StaticSymBuffer $ writeMemory' (litBytes bs1') n' src' dst' bs0'
+--     (Just n', Just src', Just dst', ConcreteBuffer bs0', StaticSymBuffer bs1') ->
+--       StaticSymBuffer $ writeMemory' bs1' n' src' dst' (litBytes bs0')
+--     (Just n', Just src', Just dst', StaticSymBuffer bs0', StaticSymBuffer bs1') ->
+--       StaticSymBuffer $ writeMemory' bs1' n' src' dst' bs0'
+-- -- TODO: figure whether dynWriteMemory or sdynWriteMemory is better
+--     _ -> dynWriteMemory bs1 n src dst bs0
+-- --    _ -> DynamicSymBuffer $ sdynWriteMemory (dynamize bs1) n src dst (dynamize bs0)
+
+-- readMemoryWord :: SymWord -> Buffer -> SymWord
+-- readMemoryWord i bf = case (maybeLitWord i, bf) of
+--   (Just i', StaticSymBuffer m) -> readMemoryWord' i' m
+--   (Just i',  ConcreteBuffer m) -> litWord $ Concrete.readMemoryWord i' m
+--   _ -> swordAt' i (dynamize bf)
+
+-- readMemoryWord32 :: SymWord -> Buffer -> SWord 32
+-- readMemoryWord32 i m = case (maybeLitWord i, m) of
+--   (Just i', StaticSymBuffer m') -> let S _ s = readMemoryWord32' i' m'
+--                                    in sFromIntegral s
+--   (Just i', ConcreteBuffer m') -> num $ Concrete.readMemoryWord32 i' m'
+--   (_, DynamicSymBuffer m') -> case truncpad' 4 $ dropS i m' of
+--     ConcreteBuffer s -> literal $ num $ Concrete.readMemoryWord32 0 s
+--     StaticSymBuffer s -> let S _ s' = readMemoryWord32' 0 s
+--                          in sFromIntegral s'
+--     DynamicSymBuffer s -> fromBytes [s .!! literal k | k <- [0..3]]
+    
+
+-- setMemoryWord :: SymWord -> SymWord -> Buffer -> Buffer
+-- setMemoryWord i x bf = case (maybeLitWord i, maybeLitWord x, bf) of
+--   (Just i', Just x', ConcreteBuffer z)  -> ConcreteBuffer $ Concrete.setMemoryWord i' x' z
+--   (Just i', _      , ConcreteBuffer z)  -> StaticSymBuffer $ setMemoryWord' i' x (litBytes z)
+--   (Just i', _      , StaticSymBuffer z) -> StaticSymBuffer $ setMemoryWord' i' x z
+--   _ -> setMemoryWord'' i x bf
+
+-- setMemoryByte :: SymWord -> SWord 8 -> Buffer -> Buffer
+-- setMemoryByte i x m = case (maybeLitWord i, m) of
+--   (Just i', StaticSymBuffer m) -> StaticSymBuffer $ setMemoryByte' i' x m
+--   (Just i', ConcreteBuffer m) -> case fromSized <$> unliteral x of
+--     Nothing -> StaticSymBuffer $ setMemoryByte' i' x (litBytes m)
+--     Just x' -> ConcreteBuffer $ Concrete.setMemoryByte i' x' m
+--   _ -> setMemoryByte'' i x m
+
+-- readSWord :: SymWord -> Buffer -> SymWord
+-- readSWord i bf = case (maybeLitWord i, bf) of
+--   (Just i', StaticSymBuffer x) -> readSWord' i' x
+--   (Just i', ConcreteBuffer x) -> litWord $ Concrete.readBlobWord i' x
+--   _  -> readSWord'' i (dynamize bf)
+
+
+-- select' :: (Ord b, Num b, SymVal b, Mergeable a) => [a] -> a -> SBV b -> a
+-- select' xs err ind = walk xs ind err
+--     where walk []     _ acc = acc
+--           walk (e:es) i acc = walk es (i-1) (ite (i .== 0) e acc)
+
+-- -- Generates a ridiculously large set of constraints (roughly 25k) when
+-- -- the index is symbolic, but it still seems (kind of) manageable
+-- -- for the solvers.
+-- readStaticWordWithBound :: SymWord -> ([SWord 8], SymWord) -> SymWord
+-- readStaticWordWithBound (S _ ind) (xs, S _ bound) =
+--   case (num <$> unliteral ind, num <$> unliteral bound) of
+--     (Just i, Just b) ->
+--       let bs = truncpad 32 $ drop i (take b xs)
+--       in S (FromBytes (StaticSymBuffer bs)) (fromBytes bs)
+--     _ -> 
+--       let boundedList = [ite (i .<= bound) x 0 | (x, i) <- zip xs [1..]]
+--       in sw256 $ fromBytes [select' boundedList 0 (ind + j) | j <- [0..31]]
 
 -- | Custom instances for SymWord, many of which have direct
 -- analogues for concrete words defined in Concrete.hs
-
-instance Show SymWord where
-  show s@(S Dull _) = case maybeLitWord s of
-    Nothing -> "<symbolic>"
-    Just w  -> show w
-  show (S (Var var) x) = var ++ ": " ++ show x
-  show (S (InfixBinOp symbol x y) z) = show x ++ symbol ++ show y  ++ ": " ++ show z
-  show (S (BinOp symbol x y) z) = symbol ++ show x ++ show y  ++ ": " ++ show z
-  show (S (UnOp symbol x) z) = symbol ++ show x ++ ": " ++ show z
-  show (S whiff x) = show whiff ++ ": " ++ show x
-
 instance EqSymbolic SymWord where
   (.==) (S _ x) (S _ y) = x .== y
 
 instance Num SymWord where
-  (S _ x) + (S _ y) = sw256 (x + y)
-  (S _ x) * (S _ y) = sw256 (x * y)
+  (S _ x) + (S _ y) = sw256 (x + y `mod` 2 ^ 256)
+  (S _ x) * (S _ y) = sw256 (x * y `mod ` 2 ^256)
   abs (S _ x) = sw256 (abs x)
   signum (S _ x) = sw256 (signum x)
   fromInteger x = sw256 (fromInteger x)
diff --git a/src/hevm/src/EVM/TTY.hs b/src/hevm/src/EVM/TTY.hs
index 8a606a26b..926f58436 100644
--- a/src/hevm/src/EVM/TTY.hs
+++ b/src/hevm/src/EVM/TTY.hs
@@ -12,7 +12,7 @@ import Brick.Widgets.List
 
 import EVM
 import EVM.ABI (abiTypeSolidity, decodeAbiValue, AbiType(..), emptyAbi)
-import EVM.Symbolic (SymWord(..))
+import EVM.Symbolic (SymWord(..), Calldata(..))
 import EVM.SymExec (maxIterationsReached)
 import EVM.Dapp (DappInfo, dappInfo)
 import EVM.Dapp (dappUnitTests, unitTestMethods, dappSolcByName, dappSolcByHash, dappSources)
@@ -778,7 +778,7 @@ updateUiVmState ui vm =
       case view result vm of
         Just (VMSuccess (ConcreteBuffer msg)) ->
           Just ("VMSuccess: " <> (show $ ByteStringS msg))
-        Just (VMSuccess (SymbolicBuffer msg)) ->
+        Just (VMSuccess (StaticSymBuffer msg)) ->
           Just ("VMSuccess: <symbolicbuffer> " <> (show msg))
         Just (VMFailure (Revert msg)) ->
           Just ("VMFailure: " <> (show . ByteStringS $ msg))
@@ -864,21 +864,28 @@ withHighlight False = withDefAttr dimAttr
 withHighlight True  = withDefAttr boldAttr
 
 prettyIfConcrete :: Buffer -> String
-prettyIfConcrete (SymbolicBuffer x) = show x
+prettyIfConcrete (StaticSymBuffer x) = show x
+prettyIfConcrete (DynamicSymBuffer x) = show x
 prettyIfConcrete (ConcreteBuffer x) = prettyHex 40 x
 
+prettyIfConcreteCd :: Calldata -> String
+prettyIfConcreteCd (CalldataBuffer bf) = prettyIfConcrete bf
+prettyIfConcreteCd (CalldataDynamic (x, l)) = show x
+
 drawTracePane :: UiVmState -> UiWidget
 drawTracePane s =
   case view uiShowMemory s of
     True ->
       hBorderWithLabel (txt "Calldata")
-      <=> str (prettyIfConcrete $ fst (view (uiVm . state . calldata) s))
+      <=> str (prettyIfConcreteCd $ view (uiVm . state . calldata) s)
       <=> hBorderWithLabel (txt "Returndata")
       <=> str (prettyIfConcrete (view (uiVm . state . returndata) s))
       <=> hBorderWithLabel (txt "Output")
       <=> str (maybe "" show (view (uiVm . result) s))
       <=> hBorderWithLabel (txt "Cache")
       <=> str (show (view (uiVm . cache . path) s))
+      <=> hBorderWithLabel (txt "refund")
+      <=> str (show (view (uiVm . tx . substate . refunds) s))
       <=> hBorderWithLabel (txt "Memory")
       <=> viewport TracePane Vertical
             (str (prettyIfConcrete (view (uiVm . state . memory) s)))
diff --git a/src/hevm/src/EVM/Types.hs b/src/hevm/src/EVM/Types.hs
index 7bfefeb14..a392bbc87 100644
--- a/src/hevm/src/EVM/Types.hs
+++ b/src/hevm/src/EVM/Types.hs
@@ -7,13 +7,16 @@
 
 module EVM.Types where
 
+import Prelude hiding (Word)
 import Data.Aeson (FromJSON (..), (.:))
 
 #if MIN_VERSION_aeson(1, 0, 0)
 import Data.Aeson (FromJSONKey (..), FromJSONKeyFunction (..))
 #endif
 
-import Data.SBV
+import Data.SBV hiding (Word)
+import Data.SBV.List ((.++))
+import qualified Data.SBV.List as SL
 import Data.Kind
 import Data.Monoid ((<>))
 import Data.Bifunctor (first)
@@ -88,29 +91,147 @@ instance (FromSizzleBV (WordN 160))
 litBytes :: ByteString -> [SWord 8]
 litBytes bs = fmap (toSized . literal) (BS.unpack bs)
 
--- | Operations over buffers (concrete or symbolic)
+-- * Operations over buffers (concrete or symbolic)
 
--- | A buffer is a list of bytes. For concrete execution, this is simply `ByteString`.
--- In symbolic settings, it is a list of symbolic bitvectors of size 8.
+-- | A buffer is a list of bytes, and is used to model EVM memory or calldata.
+-- During concrete execution, this is simply `ByteString`.
 data Buffer
-  = ConcreteBuffer ByteString
-  | SymbolicBuffer [SWord 8]
+  = ConcreteBuffer  ByteString
+  | StaticSymBuffer [SWord 8]
+  | Slice SymWord SymWord Buffer
+  | SymbolicBuffer BoundedArray
+  | Insert SymWord Buffer Buffer
   deriving (Show)
 
-instance Semigroup Buffer where
-  ConcreteBuffer a <> ConcreteBuffer b = ConcreteBuffer (a <> b)
-  ConcreteBuffer a <> SymbolicBuffer b = SymbolicBuffer (litBytes a <> b)
-  SymbolicBuffer a <> ConcreteBuffer b = SymbolicBuffer (a <> litBytes b)
-  SymbolicBuffer a <> SymbolicBuffer b = SymbolicBuffer (a <> b)
+type BoundedArray = (SArray (WordN 256) Word8, SWord 256)
+
+readBoundedArray :: SWord 256 -> BoundedArray -> SWord8
+readBoundedArray i (a,len) = ite (i .> len) 0 (readArray a i)
+
+-- | Symbolic words of 256 bits, possibly annotated with additional
+--   "insightful" information
+data SymWord = S Whiff (SWord 256)
+
+data Word = C Whiff W256 --maybe to remove completely in the future
+
+-- | This type can give insight into the provenance of a term
+data Whiff = Dull
+           | FromKeccak ByteString
+           | Var String
+           | FromBytes Buffer
+           | InfixBinOp String Whiff Whiff
+           | BinOp String Whiff Whiff
+           | UnOp String Whiff
+  deriving Show
+
+w256 :: W256 -> Word
+w256 = C Dull
+
+maybeLitWord :: SymWord -> Maybe Word
+maybeLitWord (S whiff a) = fmap (C whiff . fromSizzle) (unliteral a)
+
+instance Show SymWord where
+  show s@(S Dull _) = case maybeLitWord s of
+    Nothing -> "<symbolic>"
+    Just w  -> show w
+  show (S (Var var) x) = var ++ ": " ++ show x
+  show (S (InfixBinOp symbol x y) z) = show x ++ symbol ++ show y  ++ ": " ++ show z
+  show (S (BinOp symbol x y) z) = symbol ++ show x ++ show y  ++ ": " ++ show z
+  show (S (UnOp symbol x) z) = symbol ++ show x ++ ": " ++ show z
+  show (S whiff x) = show whiff ++ ": " ++ show x
+
+instance Show Word where
+  show (C Dull x) = show x
+  show (C (Var var) x) = var ++ ": " ++ show x
+  show (C (InfixBinOp symbol x y) z) = show x ++ symbol ++ show y  ++ ": " ++ show z
+  show (C (BinOp symbol x y) z) = symbol ++ show x ++ show y  ++ ": " ++ show z
+  show (C (UnOp symbol x) z) = symbol ++ show x ++ ": " ++ show z
+  show (C whiff x) = show whiff ++ ": " ++ show x
+
+instance Read Word where
+  readsPrec n s =
+    case readsPrec n s of
+      [(x, r)] -> [(C Dull x, r)]
+      _ -> []
+
+instance Bits Word where
+  (C _ x) .&. (C _ y) = w256 (x .&. y)
+  (C _ x) .|. (C _ y) = w256 (x .|. y)
+  (C _ x) `xor` (C _ y) = w256 (x `xor` y)
+  complement (C _ x) = w256 (complement x)
+  shift (C _ x) i = w256 (shift x i)
+  rotate (C _ x) i = w256 (rotate x i)
+  bitSize (C _ x) = bitSize x
+  bitSizeMaybe (C _ x) = bitSizeMaybe x
+  isSigned (C _ x) = isSigned x
+  testBit (C _ x) = testBit x
+  bit i = w256 (bit i)
+  popCount (C _ x) = popCount x
+
+instance FiniteBits Word where
+  finiteBitSize (C _ x) = finiteBitSize x
+  countLeadingZeros (C _ x) = countLeadingZeros x
+  countTrailingZeros (C _ x) = countTrailingZeros x
+
+instance Bounded Word where
+  minBound = w256 minBound
+  maxBound = w256 maxBound
+
+instance Eq Word where
+  (C _ x) == (C _ y) = x == y
+
+instance Enum Word where
+  toEnum i = w256 (toEnum i)
+  fromEnum (C _ x) = fromEnum x
+
+instance Integral Word where
+  quotRem (C _ x) (C _ y) =
+    let (a, b) = quotRem x y
+    in (w256 a, w256 b)
+  toInteger (C _ x) = toInteger x
+
+instance Num Word where
+  (C _ x) + (C _ y) = w256 (x + y)
+  (C _ x) * (C _ y) = w256 (x * y)
+  abs (C _ x) = w256 (abs x)
+  signum (C _ x) = w256 (signum x)
+  fromInteger x = w256 (fromInteger x)
+  negate (C _ x) = w256 (negate x)
+
+instance Real Word where
+  toRational (C _ x) = toRational x
+
+instance Ord Word where
+  compare (C _ x) (C _ y) = compare x y
+
+
+-- dynamize :: Buffer -> SList (WordN 8)
+-- dynamize (ConcreteBuffer a)  = SL.implode $ litBytes a
+-- dynamize (StaticSymBuffer a) = SL.implode a
+-- dynamize (DynamicSymBuffer a) = a
+
+-- instance EqSymbolic Buffer where
+--   ConcreteBuffer a .== ConcreteBuffer b = literal (a == b)
+--   ConcreteBuffer a .== StaticSymBuffer b = litBytes a .== b
+--   StaticSymBuffer a .== ConcreteBuffer b = a .== litBytes b
+--   StaticSymBuffer a .== StaticSymBuffer b = a .== b
+--   a .== b = dynamize a .== dynamize b
+
+
+-- instance Semigroup Buffer where
+--   ConcreteBuffer a     <> ConcreteBuffer b   = ConcreteBuffer (a <> b)
+--   ConcreteBuffer a     <> StaticSymBuffer b  = StaticSymBuffer (litBytes a <> b)
+--   c@(ConcreteBuffer a) <> DynamicSymBuffer b = DynamicSymBuffer (dynamize c .++ b)
+
+--   StaticSymBuffer a     <> ConcreteBuffer b   = StaticSymBuffer (a <> litBytes b)
+--   StaticSymBuffer a     <> StaticSymBuffer b  = StaticSymBuffer (a <> b)
+--   c@(StaticSymBuffer a) <> DynamicSymBuffer b = DynamicSymBuffer (dynamize c .++ b)
+
+--   a <> b = DynamicSymBuffer (dynamize a .++ dynamize b)
+
+-- instance Monoid Buffer where
+--   mempty = ConcreteBuffer mempty
 
-instance Monoid Buffer where
-  mempty = ConcreteBuffer mempty
-
-instance EqSymbolic Buffer where
-  ConcreteBuffer a .== ConcreteBuffer b = literal (a == b)
-  ConcreteBuffer a .== SymbolicBuffer b = litBytes a .== b
-  SymbolicBuffer a .== ConcreteBuffer b = a .== litBytes b
-  SymbolicBuffer a .== SymbolicBuffer b = a .== b
 
 newtype Addr = Addr { addressWord160 :: Word160 }
   deriving (Num, Integral, Real, Ord, Enum, Eq, Bits, Generic)
@@ -242,11 +363,6 @@ padLeft n xs = BS.replicate (n - BS.length xs) 0 <> xs
 padRight :: Int -> ByteString -> ByteString
 padRight n xs = xs <> BS.replicate (n - BS.length xs) 0
 
-truncpad :: Int -> [SWord 8] -> [SWord 8]
-truncpad n xs = if m > n then take n xs
-                else mappend xs (replicate (n - m) 0)
-  where m = length xs
-
 word256 :: ByteString -> Word256
 word256 xs = case Cereal.runGet m (padLeft 32 xs) of
                Left _ -> error "internal error"
diff --git a/src/hevm/src/EVM/UnitTest.hs b/src/hevm/src/EVM/UnitTest.hs
index 61fec4efb..9f85a34dc 100644
--- a/src/hevm/src/EVM/UnitTest.hs
+++ b/src/hevm/src/EVM/UnitTest.hs
@@ -106,36 +106,32 @@ type ABIMethod = Text
 
 -- | 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 -> Stepper ()
+initializeUnitTest :: UnitTestOptions -> EVM ()
 initializeUnitTest UnitTestOptions { .. } = do
 
   let addr = testAddress testParams
 
-  Stepper.evm $ do
-    -- Maybe modify the initial VM, e.g. to load library code
-    modify vmModifier
-    -- Make a trace entry for running the constructor
-    pushTrace (EntryTrace "constructor")
+  -- Maybe modify the initial VM, e.g. to load library code
+  modify vmModifier
+  -- Make a trace entry for running the constructor
+  pushTrace (EntryTrace "constructor")
 
   -- Constructor is loaded; run until it returns code
-  void Stepper.execFully
+  exec
 
   -- Give a balance to the test target
-  Stepper.evm $ do
-    env . contracts . ix addr . balance += w256 (testBalanceCreate testParams)
-
-    -- Initialize the test contract
-    setupCall testParams "setUp()" emptyAbi
-    popTrace
-    pushTrace (EntryTrace "initialize test")
+  env . contracts . ix addr . balance += w256 (testBalanceCreate testParams)
 
+  -- Initialize the test contract
+  setupCall testParams "setUp()" emptyAbi
+  popTrace
+  pushTrace (EntryTrace "initialize test")
   -- Let `setUp()' run to completion
-  res <- Stepper.execFully
-  Stepper.evm $ case res of
+  res <- exec
+  case res of
     Left e -> pushTrace (ErrorTrace e)
     _ -> popTrace
 
-
 -- | Assuming a test contract is loaded and initialized, this stepper
 -- will run the specified test method and return whether it succeeded.
 runUnitTest :: UnitTestOptions -> ABIMethod -> AbiValue -> Stepper Bool
@@ -553,7 +549,7 @@ setupCall TestVMParams{..} sig args  = do
   use (env . contracts) >>= assign (tx . txReversion)
   assign (tx . isCreate) False
   loadContract testAddress
-  assign (state . calldata) $ (ConcreteBuffer $ abiMethod sig args, literal . num . BS.length $ abiMethod sig args)
+  assign (state . calldata) (CalldataBuffer (ConcreteBuffer $ abiMethod sig args))
   assign (state . caller) (litAddr testCaller)
   assign (state . gas) (w256 testGasCall)
 
@@ -563,7 +559,7 @@ initialUnitTestVm (UnitTestOptions {..}) theContract =
     TestVMParams {..} = testParams
     vm = makeVm $ VMOpts
            { vmoptContract = initialContract (InitCode (view creationCode theContract))
-           , vmoptCalldata = (mempty, 0)
+           , vmoptCalldata = CalldataBuffer mempty
            , vmoptValue = 0
            , vmoptAddress = testAddress
            , vmoptCaller = litAddr testCaller
diff --git a/src/hevm/src/EVM/VMTest.hs b/src/hevm/src/EVM/VMTest.hs
index f087d4c50..6212e93ae 100644
--- a/src/hevm/src/EVM/VMTest.hs
+++ b/src/hevm/src/EVM/VMTest.hs
@@ -185,7 +185,7 @@ checkExpectedContracts vm expected =
      )
 
 clearOrigStorage :: EVM.Contract -> EVM.Contract
-clearOrigStorage = set EVM.origStorage mempty
+clearOrigStorage = set EVM.origStorage (EVM.Concrete mempty)
 
 clearZeroStorage :: EVM.Contract -> EVM.Contract
 clearZeroStorage c = case EVM._storage c of
@@ -255,7 +255,7 @@ parseVmOpts v =
        (JSON.Object env, JSON.Object exec) ->
          EVM.VMOpts
            <$> (dataField exec "code" >>= pure . EVM.initialContract . EVM.RuntimeCode)
-           <*> (dataField exec "data" >>= \a -> pure ( (ConcreteBuffer a), literal . num $ BS.length a))
+           <*> (dataField exec "data" >>= pure . CalldataBuffer . ConcreteBuffer)
            <*> (w256lit <$> wordField exec "value")
            <*> addrField exec "address"
            <*> (litAddr <$> addrField exec "caller")
@@ -325,16 +325,12 @@ realizeContract x =
   EVM.initialContract (x ^. code)
     & EVM.balance .~ EVM.w256 (x ^. balance)
     & EVM.nonce   .~ EVM.w256 (x ^. nonce)
-    & EVM.storage .~ EVM.Concrete (
-        Map.fromList .
-        map (bimap EVM.w256 (litWord . EVM.w256)) .
-        Map.toList $ x ^. storage
-        )
-    & EVM.origStorage .~ (
-        Map.fromList .
-        map (bimap EVM.w256 EVM.w256) .
-        Map.toList $ x ^. storage
-        )
+    & EVM.storage .~ store
+    & EVM.origStorage .~ store
+  where store = EVM.Concrete $
+          Map.fromList .
+          map (bimap EVM.w256 (litWord . EVM.w256)) .
+          Map.toList $ x ^. storage
 
 data BlockchainError
   = TooManyBlocks
@@ -380,7 +376,7 @@ fromCreateBlockchainCase block tx preState postState =
       in Right $ Case
          (EVM.VMOpts
           { vmoptContract      = EVM.initialContract (EVM.InitCode (txData tx))
-          , vmoptCalldata      = (mempty, 0)
+          , vmoptCalldata      = CalldataBuffer mempty
           , vmoptValue         = w256lit $ txValue tx
           , vmoptAddress       = createdAddr
           , vmoptCaller        = (litAddr origin)
@@ -419,7 +415,7 @@ fromNormalBlockchainCase block tx preState postState =
       (_, _, Just origin, Just checkState) -> Right $ Case
         (EVM.VMOpts
          { vmoptContract      = EVM.initialContract theCode
-         , vmoptCalldata      = (ConcreteBuffer $ txData tx, literal . num . BS.length $ txData tx)
+         , vmoptCalldata      = CalldataBuffer $ ConcreteBuffer $ txData tx
          , vmoptValue         = litWord (EVM.w256 $ txValue tx)
          , vmoptAddress       = toAddr
          , vmoptCaller        = (litAddr origin)
diff --git a/src/hevm/test/test.hs b/src/hevm/test/test.hs
index df7d20671..7dda52a8c 100644
--- a/src/hevm/test/test.hs
+++ b/src/hevm/test/test.hs
@@ -147,6 +147,109 @@ main = defaultMain $ testGroup "hevm"
                               (r, mempty), (s, mempty), (t, mempty)]
        === (Just $ Literal Patricia.Empty)
     ]
+  , testGroup "symbolic properties" [
+      -- testCase "calldata beyond length must be 0" $ runSMTWith z3
+      --   $ query $ do calldatalist <- freshVar_
+      --                -- works with length .< 10, but not 100...
+      --                constrain $ SL.length calldatalist .< 10
+      --                let cd = DynamicSymBuffer calldatalist
+      --                constrain $ 0 ./= readSWord (sw256 $ sFromIntegral $ len cd) cd
+      --                checkSat >>= \case
+      --                  Sat -> error "should be false"
+      --                  Unsat -> return ()
+      --                  Unk -> error "timed out!"
+
+--      ,
+        testCase "calldata beyond length must be 0" $ runSMTWith z3
+        $ query $ do calldatalist <- freshVar_
+                     -- works with length .< 100
+                     constrain $ SL.length calldatalist .< 100
+                     constrain $ sw256 (sFromIntegral $ SL.length calldatalist) .< sw256 100
+                     let cd = DynamicSymBuffer calldatalist
+                     constrain $ 0 ./= readSWord (len cd) cd
+                     checkSat >>= \case
+                       Sat -> error "should be false"
+                       Unsat -> return ()
+                       Unk -> error "timed out!"
+
+      ,
+        testCase "comparing function selector" $ runSMTWith z3{transcript=Just "sameno.smt2"} $ do
+          setTimeOut 5000
+          query $ do calldatalist <- freshVar_
+                     -- works with length .< 100
+                     constrain $ SL.length calldatalist .< 100
+                     constrain $ sw256 (sFromIntegral $ SL.length calldatalist) .< sw256 100
+                     let cd = DynamicSymBuffer calldatalist
+                     let S _ v = readSWord (sw256 0) cd
+                     constrain $ 1337 .== (sShiftRight v (224 :: SWord 256))
+                     checkSat >>= \case
+                       Sat -> return ()
+                       Unsat -> error "should be sat"
+                       Unk -> error "timed out!"
+
+    ]
+  , testGroup "Symbolic buffers"
+
+      [  testCase "dynWriteMemory works" $ runSMTWith z3 $ query $ do
+               cd  <- sbytes32
+               mem <- sbytes32
+
+               let
+                   staticWriting = writeMemory' cd 18 111 63 mem
+                   dynamicWriting =
+                     dynWriteMemory
+                      (DynamicSymBuffer (implode cd))
+                      (litWord 18)
+                      (litWord 111)
+                      (litWord 63)
+                      (DynamicSymBuffer (implode mem))
+               io $ print dynamicWriting
+               io (putStrLn "solving") >> checkSatAssuming [StaticSymBuffer staticWriting ./= dynamicWriting] >>= \case
+                 Unsat -> return ()
+                 Sat -> do getList dynamicWriting >>= io . print
+                           getList (StaticSymBuffer staticWriting) >>= io . print
+                           error "oh no!"
+                             where getList :: Buffer -> Query [WordN 8]
+                                   getList (StaticSymBuffer bf) = mapM getValue bf
+                                   getList (DynamicSymBuffer bf) = getValue bf
+
+      ,  testProperty "dynWriteMemory works like writeMemory" $
+--          withMaxSuccess 10000 $
+          forAll (genAbiValue (AbiTupleType $ Vector.fromList [AbiUIntType 16, AbiUIntType 16, AbiUIntType 16])) $ \(AbiTuple args) ->
+        let [AbiUInt 16 src', AbiUInt 16 dst', AbiUInt 16 len'] = Vector.toList args
+        in ioProperty $ when (len' < 1000) $ runSMTWith z3 $ do
+          setTimeOut 5000
+          query $ do
+               cd  <- sbytes32
+               mem <- sbytes32
+
+               let
+                   src = w256 $ W256 src'
+                   dst = w256 $ W256 dst'
+                   len = w256 $ W256 len'
+
+                   staticWriting = writeMemory' cd src len dst mem
+                   dynamicWriting =
+                     dynWriteMemory
+                      (DynamicSymBuffer (implode cd))
+                      (litWord src)
+                      (litWord len)
+                      (litWord dst)
+                      (DynamicSymBuffer (implode mem))
+
+               when (length staticWriting < 1000) $ do
+                 io $ putStrLn "solving..."
+                 checkSatAssuming [StaticSymBuffer staticWriting ./= dynamicWriting] >>= \case
+                   Unk -> io $ putStrLn "timeout"
+                   Unsat -> io $ putStrLn "Success!"
+                   Sat -> do getList dynamicWriting >>= io . print
+                             getList (StaticSymBuffer staticWriting) >>= io . print
+                             error "oh no!"
+                                where getList :: Buffer -> Query [WordN 8]
+                                      getList (StaticSymBuffer bf) = mapM getValue bf
+                                      getList (DynamicSymBuffer bf) = getValue bf                 
+               
+   ]
 
   , testGroup "Symbolic execution"
       [
@@ -162,15 +265,17 @@ main = defaultMain $ testGroup "hevm"
           }
           |]
         let pre preVM = let [x, y] = getStaticAbiArgs preVM
+                            z = x + y
                         in x .<= x + y
                            .&& view (state . callvalue) preVM .== 0
             post = Just $ \(prestate, poststate) ->
               let [x, y] = getStaticAbiArgs prestate
               in case view result poststate of
-                Just (VMSuccess (SymbolicBuffer out)) -> (fromBytes out) .== x + y
+                Just (VMSuccess (StaticSymBuffer out)) -> (fromBytes out) .== x + y
                 _ -> sFalse
-        Left (_, res) <- runSMT $ query $ verifyContract safeAdd (Just ("add(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] SymbolicS pre post
+        Left (_, res) <- runSMT $ query $ verifyContract safeAdd (Just ("add(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] SymbolicS BoundedCD pre post
         putStrLn $ "successfully explored: " <> show (length res) <> " paths"
+ 
      ,
 
       testCase "x == y => x + y == 2 * y" $ do
@@ -189,12 +294,14 @@ main = defaultMain $ testGroup "hevm"
             post (prestate, poststate) =
               let [_, y] = getStaticAbiArgs prestate
               in case view result poststate of
-                      Just (VMSuccess (SymbolicBuffer out)) -> fromBytes out .== 2 * y
+                      Just (VMSuccess (StaticSymBuffer out)) -> fromBytes out .== 2 * y
                       _ -> sFalse
         Left (_, res) <- runSMTWith z3 $ query $
-          verifyContract safeAdd (Just ("add(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] SymbolicS pre (Just post)
+          verifyContract safeAdd (Just ("add(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] SymbolicS BoundedCD pre (Just post)
         putStrLn $ "successfully explored: " <> show (length res) <> " paths"
+
       ,
+
         testCase "factorize 973013" $ do
         Just factor <- solcRuntime "PrimalityCheck"
           [i|
@@ -207,9 +314,9 @@ main = defaultMain $ testGroup "hevm"
           |]
         bs <- runSMTWith cvc4 $ query $ do
           Right vm <- checkAssert factor (Just ("factor(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) []
-          case view (state . calldata . _1) vm of
-            SymbolicBuffer bs -> BS.pack <$> mapM (getValue.fromSized) bs
-            ConcreteBuffer _ -> error "unexpected"
+          case view (state . calldata) vm of
+            CalldataBuffer (StaticSymBuffer bs) -> BS.pack <$> mapM (getValue.fromSized) bs
+            _ -> error "unexpected"
 
         let [AbiUInt 256 x, AbiUInt 256 y] = decodeAbiValues [AbiUIntType 256, AbiUIntType 256] bs
         assertEqual "" True (x == 953 && y == 1021 || x == 1021 && y == 953)
@@ -239,7 +346,7 @@ main = defaultMain $ testGroup "hevm"
               in case view result poststate of
                 Just (VMSuccess _) -> prex + 2 * y .== postx
                 _ -> sFalse
-        Left (_, res) <- runSMT $ query $ verifyContract c (Just ("f(uint256)", [AbiUIntType 256])) [] SymbolicS pre post
+        Left (_, res) <- runSMT $ query $ verifyContract c (Just ("f(uint256)", [AbiUIntType 256])) [] SymbolicS BoundedCD pre post
         putStrLn $ "successfully explored: " <> show (length res) <> " paths"
         ,
         -- Inspired by these `msg.sender == to` token bugs
@@ -271,10 +378,10 @@ main = defaultMain $ testGroup "hevm"
                 Just (VMSuccess _) -> prex + prey .== postx + (posty :: SWord 256)
                 _ -> sFalse
         bs <- runSMT $ query $ do
-          Right vm <- verifyContract c (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] SymbolicS pre (Just post)
-          case view (state . calldata . _1) vm of
-            SymbolicBuffer bs -> BS.pack <$> mapM (getValue.fromSized) bs
-            ConcreteBuffer bs -> error "unexpected"
+          Right vm <- verifyContract c (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] SymbolicS BoundedCD pre (Just post)
+          case view (state . calldata) vm of
+            CalldataBuffer (StaticSymBuffer bs) -> BS.pack <$> mapM (getValue.fromSized) bs
+            _ -> error "unexpected"
 
         let [AbiUInt 256 x, AbiUInt 256 y] = decodeAbiValues [AbiUIntType 256, AbiUIntType 256] bs
         assertEqual "Catch storage collisions" x y
@@ -344,9 +451,9 @@ main = defaultMain $ testGroup "hevm"
             |]
           bs <- runSMT $ query $ do
             Right vm <- checkAssert c (Just ("deposit(uint8)", [AbiUIntType 8])) []
-            case view (state . calldata . _1) vm of
-              SymbolicBuffer bs -> BS.pack <$> mapM (getValue.fromSized) bs
-              ConcreteBuffer _ -> error "unexpected"
+            case view (state . calldata) vm of
+              CalldataBuffer (StaticSymBuffer bs) -> BS.pack <$> mapM (getValue.fromSized) bs
+              _ -> error "unexpected"
 
           let [deposit] = decodeAbiValues [AbiUIntType 8] bs
           assertEqual "overflowing uint8" deposit (AbiUInt 8 255)
@@ -402,9 +509,9 @@ main = defaultMain $ testGroup "hevm"
             |]
           bs <- runSMTWith z3 $ query $ do
             Right vm <- checkAssert c (Just ("f(uint256,uint256,uint256,uint256)", replicate 4 (AbiUIntType 256))) []
-            case view (state . calldata . _1) vm of
-              SymbolicBuffer bs -> BS.pack <$> mapM (getValue.fromSized) bs
-              ConcreteBuffer _ -> error "unexpected"
+            case view (state . calldata) vm of
+              CalldataBuffer (StaticSymBuffer bs) -> BS.pack <$> mapM (getValue.fromSized) bs
+              _ -> error "unexpected"
               
           let [AbiUInt 256 x,
                AbiUInt 256 y,
@@ -431,9 +538,7 @@ main = defaultMain $ testGroup "hevm"
               }
             }
             |]
-          Left (_, res) <- runSMTWith z3 $ do
-            setTimeOut 5000
-            query $ checkAssert c Nothing []
+          Left (_, res) <- runSMTWith z3 $ query $ checkAssert c Nothing []
           putStrLn $ "successfully explored: " <> show (length res) <> " paths"
 
        ,
@@ -453,9 +558,9 @@ main = defaultMain $ testGroup "hevm"
           Right counterexample <- runSMTWith cvc4 $ query $ checkAssert c (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) []
           putStrLn $ "found counterexample:"
 
+       ,
 
-      ,
-         testCase "multiple contracts" $ do
+        testCase "multiple contracts" $ do
           let code =
                 [i|
                   contract C {
@@ -475,7 +580,7 @@ main = defaultMain $ testGroup "hevm"
           Just c <- solcRuntime "C" code
           Just a <- solcRuntime "A" code
           Right cex <- runSMT $ query $ do
-            vm0 <- abstractVM (Just ("call_A()", [])) [] c SymbolicS
+            vm0 <- abstractVM (Just ("call_A()", [])) [] c SymbolicS BoundedCD
             store <- freshArray (show aAddr) Nothing
             let vm = vm0
                   & set (state . callvalue) 0
@@ -484,6 +589,27 @@ main = defaultMain $ testGroup "hevm"
                                            set EVM.storage (Symbolic store)))
             verify vm Nothing Nothing (Just checkAssertions)
           putStrLn $ "found counterexample:"
+    ,
+         testCase "dynamic bytes (calldataload)" $ do
+          Just c <- solcRuntime "C"
+            [i|
+              contract C
+              {
+              function f() public pure {
+                uint y;
+                uint z;
+                assembly {
+                  y := calldataload(12)
+                  z := calldataload(31)
+                }
+                assert(y == z);
+              }
+              }
+            |]
+          -- should find a counterexample
+          Right cex <- runSMTWith z3 $ do
+            query $ checkAssert c Nothing []
+          putStrLn $ "found counterexample"
 
     ]
   , testGroup "Equivalence checking"
@@ -500,7 +626,7 @@ main = defaultMain $ testGroup "hevm"
         -- }                                 }
         let aPrgm = hex "602060006000376000805160008114601d5760018114602457fe6029565b8191506029565b600191505b50600160015250"
             bPrgm = hex "6020600060003760005160008114601c5760028114602057fe6021565b6021565b5b506001600152"
-        runSMTWith z3 $ query $ do
+        runSMTWith cvc4 $ query $ do
           Right counterexample <- equivalenceCheck aPrgm bPrgm Nothing Nothing
           return ()
 
@@ -512,11 +638,11 @@ main = defaultMain $ testGroup "hevm"
 
 runSimpleVM :: ByteString -> ByteString -> Maybe ByteString
 runSimpleVM x ins = case loadVM x of
-                      Nothing -> Nothing
-                      Just vm -> let calldata' = (ConcreteBuffer ins, literal . num $ BS.length ins)
-                       in case runState (assign (state.calldata) calldata' >> exec) vm of
-                            (VMSuccess (ConcreteBuffer bs), _) -> Just bs
-                            _ -> Nothing
+  Nothing -> Nothing
+  Just vm ->
+    case runState (assign (state.calldata) (CalldataBuffer $ ConcreteBuffer ins) >> exec) vm of
+      (VMSuccess (ConcreteBuffer bs), _) -> Just bs
+      _ -> Nothing
 
 loadVM :: ByteString -> Maybe VM
 loadVM x =
@@ -580,8 +706,8 @@ runStatements stmts args t = do
 
 getStaticAbiArgs :: VM -> [SWord 256]
 getStaticAbiArgs vm =
-  let SymbolicBuffer bs = ditch 4 $ view (state . calldata . _1) vm
-  in fmap (\i -> fromBytes $ take 32 (drop (i*32) bs)) [0..((length bs) `div` 32 - 1)]
+  let CalldataBuffer (StaticSymBuffer bs) = view (state . calldata) vm
+  in fmap (\i -> fromBytes $ take 32 (drop (i*32) (drop 4 bs))) [0..((length (drop 4 bs)) `div` 32 - 1)]
 
 -- includes shaving off 4 byte function sig
 decodeAbiValues :: [AbiType] -> ByteString -> [AbiValue]