diff --git a/flake.lock b/flake.lock
index 990584087..5d3bfb046 100644
--- a/flake.lock
+++ b/flake.lock
@@ -49,11 +49,11 @@
     },
     "nixpkgs": {
       "locked": {
-        "lastModified": 1669063728,
-        "narHash": "sha256-xkaGi5mXSfRUjNCzbyBX2AOuweg14sNMRqawpO/GJCU=",
+        "lastModified": 1672485841,
+        "narHash": "sha256-4Ibn06cyIsV+jS7qjh0tIw670DJRbzCxhLuPJeC46o0=",
         "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "aee7510bf1c4942b3ce0f73ed69476c21b896fc4",
+        "rev": "a73f033cc7e5e1c6ac8bbadbbe28e9625cf9ec47",
         "type": "github"
       },
       "original": {
diff --git a/flake.nix b/flake.nix
index f0ca47547..554d6770e 100644
--- a/flake.nix
+++ b/flake.nix
@@ -42,8 +42,17 @@
             chmod +x $out/bin/solc
           '';
         };
+
+        hevm = pkgs.haskell.lib.dontCheck (
+          pkgs.haskellPackages.callCabal2nix "hevm" (pkgs.fetchFromGitHub {
+            owner = "ethereum";
+            repo = "hevm";
+            rev = "0.50.1";
+            sha256 = "sha256-fgseeQNxWh13PVLsfvyAdZZwtqzELbTivPOiRc6cox8=";
+        }) { secp256k1 = pkgs.secp256k1; });
+
         echidna = with pkgs; lib.pipe
-          (haskellPackages.callCabal2nix "echidna" ./. {})
+          (haskellPackages.callCabal2nix "echidna" ./. { inherit hevm; })
           [
             (haskell.lib.compose.addTestToolDepends [ haskellPackages.hpack slither-analyzer solc ])
             (haskell.lib.compose.disableCabalFlag "static")
diff --git a/lib/Echidna/ABI.hs b/lib/Echidna/ABI.hs
index 8ec1877ca..06f6aad12 100644
--- a/lib/Echidna/ABI.hs
+++ b/lib/Echidna/ABI.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE DerivingStrategies #-}
 {-# LANGUAGE TemplateHaskell #-}
 
 module Echidna.ABI where
@@ -18,10 +19,11 @@ import Data.Hashable (Hashable(..))
 import Data.HashMap.Strict (HashMap)
 import Data.HashMap.Strict qualified as M
 import Data.HashSet (HashSet, fromList, union)
-import Data.HashSet qualified as H
+import Data.Set (Set)
+import Data.Set qualified as Set
 import Data.List (intercalate)
 import Data.List.NonEmpty qualified as NE
-import Data.Maybe (fromMaybe, catMaybes)
+import Data.Maybe (fromMaybe, catMaybes, mapMaybe)
 import Data.Text (Text)
 import Data.Text qualified as T
 import Data.Text.Encoding (encodeUtf8)
@@ -33,7 +35,7 @@ import Data.Word (Word8)
 import Numeric (showHex)
 
 import EVM.ABI hiding (genAbiValue)
-import EVM.Types (Addr, abiKeccak)
+import EVM.Types (Addr, abiKeccak, W256)
 
 import Echidna.Mutator.Array (mutateLL, replaceAt)
 import Echidna.Types.Random
@@ -107,6 +109,8 @@ data GenDict = GenDict { _pSynthA    :: Float
                          -- ^ Default seed to use if one is not provided in EConfig
                        , _rTypes     :: Text -> Maybe AbiType
                          -- ^ Return types of any methods we scrape return values from
+                       , _dictValues :: Set W256
+                         -- ^ A set of int/uint constants for better performance
                        }
 
 makeLenses 'GenDict
@@ -114,27 +118,15 @@ makeLenses 'GenDict
 hashMapBy :: (Hashable k, Hashable a, Eq k, Ord a) => (a -> k) -> [a] -> HashMap k (HashSet a)
 hashMapBy f = M.fromListWith union . fmap (\v -> (f v, fromList [v]))
 
-gaddConstants :: [AbiValue] -> GenDict -> GenDict
-gaddConstants l = constants <>~ hashMapBy abiValueType l
-
 gaddCalls :: [SolCall] -> GenDict -> GenDict
 gaddCalls c = wholeCalls <>~ hashMapBy (fmap $ fmap abiValueType) c
 
 defaultDict :: GenDict
 defaultDict = mkGenDict 0 [] [] 0 (const Nothing)
 
-dictValues :: GenDict -> [Integer]
-dictValues g = catMaybes $ concatMap (\(_,h) -> map fromValue $ H.toList h) $ M.toList $ g ^. constants
-  where fromValue (AbiUInt _ n) = Just (toInteger n)
-        fromValue (AbiInt  _ n) = Just (toInteger n)
-        fromValue _             = Nothing
-
--- This instance is the only way for mkConf to work nicely, and is well-formed.
-{-# ANN module ("HLint: ignore Unused LANGUAGE pragma" :: String) #-}
--- We need the above since hlint doesn't notice DeriveAnyClass in StandaloneDeriving.
-deriving instance Hashable AbiType
-deriving instance Hashable AbiValue
-deriving instance Hashable Addr
+deriving anyclass instance Hashable AbiType
+deriving anyclass instance Hashable AbiValue
+deriving anyclass instance Hashable Addr
 
 -- | Construct a 'GenDict' from some dictionaries, a 'Float', a default seed, and a typing rule for
 -- return values
@@ -145,7 +137,14 @@ mkGenDict :: Float      -- ^ Percentage of time to mutate instead of synthesize.
           -> (Text -> Maybe AbiType)
           -- ^ A return value typing rule
           -> GenDict
-mkGenDict p vs cs = GenDict p (hashMapBy abiValueType vs) (hashMapBy (fmap $ fmap abiValueType) cs)
+mkGenDict p vs cs s tr =
+  GenDict p (hashMapBy abiValueType vs) (hashMapBy (fmap $ fmap abiValueType) cs) s tr (mkDictValues vs)
+
+mkDictValues :: [AbiValue] -> Set W256
+mkDictValues vs = Set.fromList $ mapMaybe fromValue vs
+  where fromValue (AbiUInt _ n) = Just (fromIntegral n)
+        fromValue (AbiInt  _ n) = Just (fromIntegral n)
+        fromValue _             = Nothing
 
 -- Generation (synthesis)
 
diff --git a/lib/Echidna/Campaign.hs b/lib/Echidna/Campaign.hs
index 8dcc42f02..db1eec694 100644
--- a/lib/Echidna/Campaign.hs
+++ b/lib/Echidna/Campaign.hs
@@ -1,6 +1,7 @@
 {-# LANGUAGE MultiWayIf #-}
 {-# LANGUAGE NoMonomorphismRestriction #-}
 {-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE GADTs #-}
 
 module Echidna.Campaign where
 
@@ -28,7 +29,7 @@ import System.Random (mkStdGen)
 import EVM
 import EVM.Dapp (DappInfo)
 import EVM.ABI (getAbi, AbiType(AbiAddressType), AbiValue(AbiAddress))
-import EVM.Types (Addr, Buffer(..))
+import EVM.Types (Addr, Expr(ConcreteBuf))
 
 import Echidna.ABI
 import Echidna.Exec
@@ -252,12 +253,13 @@ callseq ic v w ql = do
       additions = H.unionWith S.union diffs results
   -- append to the constants dictionary
   modifying (hasLens . genDict . constants) . H.unionWith S.union $ additions
+  modifying (hasLens . genDict . dictValues) . DS.union $ mkDictValues $ S.toList $ S.unions $ H.elems additions
   where
     -- Given a list of transactions and a return typing rule, this checks whether we know the return
     -- type for each function called, and if we do, tries to parse the return value as a value of that
     -- type. It returns a 'GenDict' style HashMap.
     parse l rt = H.fromList . flip mapMaybe l $ \(x, r) -> case (rt =<< x ^? call . _SolCall . _1, r) of
-      (Just ty, VMSuccess (ConcreteBuffer b)) ->
+      (Just ty, VMSuccess (ConcreteBuf b)) ->
         (ty,) . S.fromList . pure <$> runGetOrFail (getAbi ty) (b ^. lazy) ^? _Right . _3
       _ -> Nothing
 
diff --git a/lib/Echidna/Config.hs b/lib/Echidna/Config.hs
index 0bb7a2563..cc77ad0f1 100644
--- a/lib/Echidna/Config.hs
+++ b/lib/Echidna/Config.hs
@@ -19,7 +19,6 @@ import Data.Text (isPrefixOf)
 import Data.Yaml qualified as Y
 
 import EVM (result)
-import EVM.Types (w256)
 
 import Echidna.Test
 import Echidna.Types.Campaign
@@ -57,7 +56,7 @@ instance FromJSON EConfigWithUsage where
             let useKey k = hasLens %= insert k
                 x ..:? k = useKey k >> lift (x .:? k)
                 x ..!= y = fromMaybe y <$> x
-                getWord s d = w256 . fromIntegral <$> v ..:? s ..!= (d :: Integer)
+                getWord s d = fromIntegral <$> v ..:? s ..!= (d :: Integer)
 
                 -- TxConf
                 xc = TxConf <$> getWord "propMaxGas" maxGasPerBlock
diff --git a/lib/Echidna/Events.hs b/lib/Echidna/Events.hs
index dc9255e86..b8b1461b3 100644
--- a/lib/Echidna/Events.hs
+++ b/lib/Echidna/Events.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE ImplicitParams #-}
+{-# LANGUAGE GADTs #-}
 
 module Echidna.Events where
 
@@ -8,16 +9,15 @@ import Data.Tree (flatten)
 import Data.Tree.Zipper (fromForest, TreePos, Empty)
 import Data.Text (pack, Text)
 import Data.Map qualified as M
-import Data.Maybe (listToMaybe)
+import Data.Maybe (listToMaybe, fromJust)
 import Data.Vector (fromList)
 import Control.Lens
 
 import EVM
 import EVM.ABI (Event(..), Indexed(..), decodeAbiValue, AbiType(AbiUIntType, AbiTupleType, AbiStringType))
-import EVM.Concrete (wordValue)
 import EVM.Dapp
 import EVM.Format (showValues, showError, contractNamePart)
-import EVM.Types (W256, maybeLitWord)
+import EVM.Types (Expr(ConcreteBuf), W256, maybeLitWord)
 import EVM.Solidity (contractName)
 
 type EventMap = M.Map W256 Event
@@ -37,14 +37,14 @@ extractEvents decodeErrors dappInfo' vm =
       forest = traceForest vm
       showTrace trace =
         let ?context = DappContext { _contextInfo = dappInfo', _contextEnv = vm ^?! EVM.env . EVM.contracts } in
-        let codehash' = trace ^. traceContract . codehash
+        let codehash' = fromJust $ maybeLitWord (trace ^. traceContract . codehash)
             maybeContractName = maybeContractNameFromCodeHash codehash'
         in
         case trace ^. traceData of
-          EventTrace (Log addr bytes topics) ->
+          EventTrace addr bytes topics ->
             case maybeLitWord =<< listToMaybe topics of
               Nothing   -> []
-              Just word -> case M.lookup (wordValue word) eventMap of
+              Just word -> case M.lookup word eventMap of
                              Just (Event name _ types) ->
                                -- TODO this is where indexed types are filtered out
                                -- they are filtered out for a reason as they only contain
@@ -67,7 +67,7 @@ extractEvents decodeErrors dappInfo' vm =
 decodeRevert :: Bool -> VM -> Events
 decodeRevert decodeErrors vm =
   case vm ^. result of
-    Just (VMFailure (Revert bs)) -> decodeRevertMsg decodeErrors bs
+    Just (VMFailure (Revert (ConcreteBuf bs))) -> decodeRevertMsg decodeErrors bs
     _                            -> []
 
 decodeRevertMsg :: Bool -> BS.ByteString -> Events
diff --git a/lib/Echidna/Exec.hs b/lib/Echidna/Exec.hs
index 3744e898f..c270e43a2 100644
--- a/lib/Echidna/Exec.hs
+++ b/lib/Echidna/Exec.hs
@@ -1,5 +1,6 @@
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE GADTs #-}
 
 module Echidna.Exec where
 
@@ -10,11 +11,11 @@ import Data.Has (Has(..))
 import Data.Map qualified as M
 import Data.Maybe (fromMaybe)
 import Data.Set qualified as S
+import Data.Word (Word64)
 
 import EVM
 import EVM.Exec (exec, vmForEthrunCreation)
-import EVM.Types (Buffer(..), Word)
-import EVM.Symbolic (litWord)
+import EVM.Types (Expr(ConcreteBuf, Lit))
 
 import Echidna.Events (emptyEvents)
 import Echidna.Transaction
@@ -43,7 +44,7 @@ getQuery (VMFailure (Query q)) = Just q
 getQuery _                     = Nothing
 
 emptyAccount :: Contract
-emptyAccount = initialContract (RuntimeCode mempty)
+emptyAccount = initialContract (RuntimeCode (ConcreteRuntimeCode mempty))
 
 -- | Matches execution errors that just cause a reversion.
 pattern Reversion :: VMResult
@@ -72,7 +73,7 @@ vmExcept e = throwM $ case VMFailure e of {Illegal -> IllegalExec e; _ -> Unknow
 execTxWith :: (MonadState x m, Has VM x) => (Error -> m ()) -> m VMResult -> Tx -> m (VMResult, Int)
 execTxWith onErr executeTx tx' = do
   isSelfDestruct <- hasSelfdestructed (tx' ^. dst)
-  if isSelfDestruct then pure (VMFailure (Revert ""), 0)
+  if isSelfDestruct then pure (VMFailure (Revert (ConcreteBuf "")), 0)
   else do
     hasLens . traces .= emptyEvents
     vmBeforeTx <- use hasLens
@@ -82,7 +83,7 @@ execTxWith onErr executeTx tx' = do
     gasLeftAfterTx <- use $ hasLens . state . gas
     checkAndHandleQuery vmBeforeTx vmResult' onErr executeTx tx' gasLeftBeforeTx gasLeftAfterTx
 
-checkAndHandleQuery :: (MonadState x m, Has VM x) => VM -> VMResult -> (Error -> m ()) -> m VMResult -> Tx -> EVM.Types.Word -> EVM.Types.Word -> m (VMResult, Int)
+checkAndHandleQuery :: (MonadState x m, Has VM x) => VM -> VMResult -> (Error -> m ()) -> m VMResult -> Tx -> Word64 -> Word64 -> m (VMResult, Int)
 checkAndHandleQuery vmBeforeTx vmResult' onErr executeTx tx' gasLeftBeforeTx gasLeftAfterTx =
         -- Continue transaction whose execution queried a contract or slot
     let continueAfterQuery = do
@@ -94,7 +95,7 @@ checkAndHandleQuery vmBeforeTx vmResult' onErr executeTx tx' gasLeftBeforeTx gas
 
     in case getQuery vmResult' of
       -- A previously unknown contract is required
-      Just (PleaseFetchContract _ _ continuation) -> do
+      Just (PleaseFetchContract _ continuation) -> do
         -- Use the empty contract
         hasLens %= execState (continuation emptyAccount)
         continueAfterQuery
@@ -135,11 +136,11 @@ handleErrorsAndConstruction onErr vmResult' vmBeforeTx tx' = case (vmResult', tx
     hasLens . traces .= tracesBeforeVMReset
     hasLens . state . codeContract .= codeContractBeforeVMReset
   (VMFailure x, _) -> onErr x
-  (VMSuccess (ConcreteBuffer bytecode'), SolCreate _) ->
+  (VMSuccess (ConcreteBuf bytecode'), SolCreate _) ->
     -- Handle contract creation.
     hasLens %= execState (do
-      env . contracts . at (tx' ^. dst) . _Just . contractcode .= InitCode (ConcreteBuffer "")
-      replaceCodeOfSelf (RuntimeCode (ConcreteBuffer bytecode'))
+      env . contracts . at (tx' ^. dst) . _Just . contractcode .= InitCode mempty mempty
+      replaceCodeOfSelf (RuntimeCode (ConcreteRuntimeCode bytecode'))
       loadContract (tx' ^. dst))
   _ -> pure ()
 
@@ -183,6 +184,6 @@ execTxWithCov memo l = do
       pure $ lookupBytecodeMetadata memo bc
 
 initialVM :: VM
-initialVM = vmForEthrunCreation mempty & block . timestamp .~ litWord initialTimestamp
+initialVM = vmForEthrunCreation mempty & block . timestamp .~ Lit initialTimestamp
                                        & block . number .~ initialBlockNumber
                                        & env . contracts .~ mempty       -- fixes weird nonce issues
diff --git a/lib/Echidna/Orphans/JSON.hs b/lib/Echidna/Orphans/JSON.hs
index 678314af6..3c06ea890 100644
--- a/lib/Echidna/Orphans/JSON.hs
+++ b/lib/Echidna/Orphans/JSON.hs
@@ -14,7 +14,7 @@ import Data.ByteString (ByteString)
 import Data.DoubleWord (Word256, Int256, Word160)
 import Data.Text (Text, unpack)
 import EVM.ABI (AbiValue, AbiType)
-import EVM.Types (Addr, Word)
+import EVM.Types (Addr)
 import Text.Read (readMaybe)
 
 readT :: Read a => Text -> Maybe a
@@ -47,8 +47,5 @@ instance FromJSON ByteString where
 instance ToJSON Addr where
   toJSON = toJSON . show
 
-instance FromJSON Word where
-  parseJSON = withText "Word" $ maybe (fail "could not parse Word") pure . readT
-
 $(deriveJSON defaultOptions ''AbiType)
 $(deriveJSON defaultOptions ''AbiValue)
diff --git a/lib/Echidna/Output/JSON.hs b/lib/Echidna/Output/JSON.hs
index d43ae64b0..b3778f19a 100644
--- a/lib/Echidna/Output/JSON.hs
+++ b/lib/Echidna/Output/JSON.hs
@@ -13,7 +13,7 @@ import Data.Text
 import Data.Text.Encoding (decodeUtf8)
 import Numeric (showHex)
 
-import EVM.Types (keccak)
+import EVM.Types (keccak')
 
 import Echidna.ABI (ppAbiValue, GenDict(..))
 import Echidna.Types.Coverage (CoverageInfo)
@@ -99,7 +99,7 @@ encodeCampaign C.Campaign{..} = encode
            , _error = Nothing
            , _tests = mapTest <$> _tests
            , seed = _defSeed _genDict
-           , coverage = mapKeys (("0x" ++) . (`showHex` "") . keccak) $ DF.toList <$> _coverage
+           , coverage = mapKeys (("0x" ++) . (`showHex` "") . keccak') $ DF.toList <$>_coverage
            , gasInfo = toList _gasInfo
            }
 
diff --git a/lib/Echidna/Output/Source.hs b/lib/Echidna/Output/Source.hs
index 48c29146f..1fbc37b7b 100644
--- a/lib/Echidna/Output/Source.hs
+++ b/lib/Echidna/Output/Source.hs
@@ -4,7 +4,7 @@ import Prelude hiding (writeFile)
 
 import Control.Lens
 import Data.Foldable
-import Data.Maybe (catMaybes, fromMaybe, mapMaybe)
+import Data.Maybe (fromMaybe, mapMaybe)
 import Data.List (nub, sort)
 import Data.Map qualified as M
 import Data.Set qualified as S
@@ -140,7 +140,7 @@ srcMapForOpLocation contract (_,n,_,r) =
 buildRuntimeLinesMap :: SourceCache -> [SolcContract] -> M.Map Text (S.Set Int)
 buildRuntimeLinesMap sc contracts =
   M.fromListWith (<>)
-    [(k, S.singleton v) | (k, v) <- catMaybes $ srcMapCodePos sc <$> srcMaps]
+    [(k, S.singleton v) | (k, v) <- mapMaybe (srcMapCodePos sc) srcMaps]
   where
   srcMaps = concatMap
     (\c -> toList $ c ^. runtimeSrcmap <> c ^. creationSrcmap) contracts
diff --git a/lib/Echidna/RPC.hs b/lib/Echidna/RPC.hs
index ee61efeda..0d515ae45 100644
--- a/lib/Echidna/RPC.hs
+++ b/lib/Echidna/RPC.hs
@@ -1,3 +1,5 @@
+{-# LANGUAGE GADTs #-}
+
 module Echidna.RPC where
 
 import Prelude hiding (Word)
@@ -23,7 +25,7 @@ import Text.Read (readMaybe)
 import EVM
 import EVM.ABI (AbiType(..), AbiValue(..), decodeAbiValue, selector)
 import EVM.Exec (exec)
-import EVM.Types (Addr, Buffer(..), W256, w256)
+import EVM.Types (Addr, W256, Expr(ConcreteBuf))
 
 import Echidna.Exec
 import Echidna.Transaction
@@ -122,14 +124,14 @@ initAddress addr = do
   cs <- use (env . EVM.contracts)
   if addr `member` cs then pure ()
   else env . EVM.contracts . at addr .= Just account
- where account = initialContract (RuntimeCode mempty) & set nonce 0 & set balance (w256 100000000000000000000) -- default balance for EOAs in etheno
+ where account = initialContract (RuntimeCode (ConcreteRuntimeCode mempty)) & set nonce 0 & set balance 100000000000000000000 -- default balance for EOAs in etheno
 
 crashWithQueryError :: (MonadState VM m, MonadFail m, MonadThrow m) => Query -> Etheno -> m ()
 crashWithQueryError q et =
   case (q, et) of
-    (PleaseFetchContract addr _ _, FunctionCall f t _ _ _ _) ->
+    (PleaseFetchContract addr _, FunctionCall f t _ _ _ _) ->
       error ("Address " ++ show addr ++ " was used during function call from " ++ show f ++ " to " ++ show t ++ " but it was never defined as EOA or deployed as a contract")
-    (PleaseFetchContract addr _ _, ContractCreated f t _ _ _ _) ->
+    (PleaseFetchContract addr _, ContractCreated f t _ _ _ _) ->
       error ("Address " ++ show addr ++ " was used during the contract creation of " ++ show t ++ " from " ++ show f ++ " but it was never defined as EOA or deployed as a contract")
     (PleaseFetchSlot slot _ _, FunctionCall f t _ _ _ _) ->
       error ("Slot " ++ show slot ++ " was used during function call from " ++ show f ++ " to " ++ show t ++ " but it was never loaded")
@@ -149,16 +151,16 @@ execEthenoTxs et = do
        (Reversion,   _)               -> void $ put vm
        (VMFailure (Query q), _)       -> crashWithQueryError q et
        (VMFailure x, _)               -> vmExcept x >> M.fail "impossible"
-       (VMSuccess (ConcreteBuffer bc),
+       (VMSuccess (ConcreteBuf bc),
         ContractCreated _ ca _ _ _ _) -> do
-          env . contracts . at ca . _Just . contractcode .= InitCode (ConcreteBuffer "")
-          liftSH (replaceCodeOfSelf (RuntimeCode (ConcreteBuffer bc)) >> loadContract ca)
+          env . contracts . at ca . _Just . contractcode .= InitCode mempty mempty
+          liftSH (replaceCodeOfSelf (RuntimeCode (ConcreteRuntimeCode bc)) >> loadContract ca)
           return ()
        _                              -> return ()
 
 -- | For an etheno txn, set up VM to execute txn
 setupEthenoTx :: MonadState VM m => Etheno -> m ()
 setupEthenoTx (AccountCreated f) = initAddress f -- TODO: improve etheno to include initial balance
-setupEthenoTx (ContractCreated f c _ _ d v) = setupTx $ createTxWithValue d f c (fromInteger unlimitedGasPerBlock) (w256 v) (1, 1)
-setupEthenoTx (FunctionCall f t _ _ d v) = setupTx $ Tx (SolCalldata d) f t (fromInteger unlimitedGasPerBlock) 0 (w256 v) (1, 1)
+setupEthenoTx (ContractCreated f c _ _ d v) = setupTx $ createTxWithValue d f c (fromInteger unlimitedGasPerBlock) v (1, 1)
+setupEthenoTx (FunctionCall f t _ _ d v) = setupTx $ Tx (SolCalldata d) f t (fromInteger unlimitedGasPerBlock) 0 v (1, 1)
 setupEthenoTx (BlockMined n t) = setupTx $ Tx NoCall 0 0 0 0 0 (fromInteger t, fromInteger n)
diff --git a/lib/Echidna/Solidity.hs b/lib/Echidna/Solidity.hs
index f2ddbeae1..258558eee 100644
--- a/lib/Echidna/Solidity.hs
+++ b/lib/Echidna/Solidity.hs
@@ -30,7 +30,7 @@ import EVM hiding (contracts, path)
 import EVM qualified (contracts)
 import EVM.ABI
 import EVM.Solidity
-import EVM.Types (Addr, w256)
+import EVM.Types (Addr)
 import EVM.Dapp (dappInfo)
 
 import Echidna.ABI (encodeSig, encodeSigWithName, hashSig, fallback, commonTypeSizes, mkValidAbiInt, mkValidAbiUInt)
@@ -119,7 +119,7 @@ addresses = do
 populateAddresses :: [Addr] -> Integer -> VM -> VM
 populateAddresses []     _ vm = vm
 populateAddresses (a:as) b vm = if deployed then populateAddresses as b vm else populateAddresses as b (vm & set (env . EVM.contracts . at a) (Just account))
-  where account   = initialContract (RuntimeCode mempty) & set nonce 0 & set balance (w256 $ fromInteger b)
+  where account   = initialContract (RuntimeCode (ConcreteRuntimeCode mempty)) & set nonce 0 & set balance (fromInteger b)
         deployed = a `member` (vm ^. env . EVM.contracts)
 
 -- | Address to load the first library
@@ -189,7 +189,7 @@ loadSpecified name cs = do
   -- Set up initial VM, either with chosen contract or Etheno initialization file
   -- need to use snd to add to ABI dict
   let vm = initialVM & block . gaslimit .~ fromInteger unlimitedGasPerBlock
-                     & block . maxCodeSize .~ w256 (fromInteger mcs)
+                     & block . maxCodeSize .~ fromInteger mcs
   blank' <- liftIO $ maybe (pure vm) loadEthenoBatch fp
   let blank = populateAddresses (NE.toList ads |> d) bala blank'
 
@@ -221,7 +221,7 @@ loadSpecified name cs = do
       vm2 <- deployBytecodes di dpb d vm1
 
       -- main contract deployment
-      let deployment = execTx $ createTxWithValue bc d ca (fromInteger unlimitedGasPerBlock) (w256 $ fromInteger balc) (0, 0)
+      let deployment = execTx $ createTxWithValue bc d ca (fromInteger unlimitedGasPerBlock) (fromInteger balc) (0, 0)
       vm3 <- execStateT deployment vm2
       when (isNothing $ currentContract vm3) (throwM $ DeploymentFailed ca $ T.unlines $ extractEvents True di vm3)
 
diff --git a/lib/Echidna/Test.hs b/lib/Echidna/Test.hs
index b69e00ec1..cd38a2c07 100644
--- a/lib/Echidna/Test.hs
+++ b/lib/Echidna/Test.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE GADTs #-}
 module Echidna.Test where
 
 import Prelude hiding (Word)
@@ -15,8 +16,7 @@ import Data.Text qualified as T
 import EVM (Error(..), VMResult(..), VM, calldata, callvalue, codeContract, result, tx, state, substate, selfdestructs)
 import EVM.ABI (AbiValue(..), AbiType(..), encodeAbiValue, decodeAbiValue, )
 import EVM.Dapp (DappInfo)
-import EVM.Types (Addr)
-import EVM.Symbolic (forceLit)
+import EVM.Types (Addr, Expr (ConcreteBuf, Lit))
 
 import Echidna.ABI
 import Echidna.Events (Events, extractEvents)
@@ -176,7 +176,7 @@ checkStatefullAssertion (sig, addr) = do
   dappInfo <- view hasLens
   vm <- use hasLens
       -- Whether the last transaction called the function `sig`.
-  let isCorrectFn = case viewBuffer $ vm ^. state . calldata . _1 of
+  let isCorrectFn = case viewBuffer $ vm ^. state . calldata of
         Just cd -> BS.isPrefixOf (BS.take 4 (abiCalldata (encodeSig sig) mempty)) cd
         Nothing -> False
       -- Whether the last transaction executed a function on the contract `addr`.
@@ -202,13 +202,13 @@ checkDapptestAssertion (sig, addr) = do
   dappInfo <- view hasLens
   vm <- use hasLens
   -- Whether the last transaction has any value
-  let hasValue = forceLit (vm ^. state . callvalue) /= 0
+  let hasValue = vm ^. state . callvalue /= Lit 0
       -- Whether the last transaction called the function `sig`.
-  let isCorrectFn = case viewBuffer $ vm ^. state . calldata . _1 of
+  let isCorrectFn = case viewBuffer $ vm ^. state . calldata of
         Just cd -> BS.isPrefixOf (BS.take 4 (abiCalldata (encodeSig sig) mempty)) cd
         Nothing -> False
       isAssertionFailure = case vm ^. result of
-        Just (VMFailure (Revert bs)) -> not $ BS.isSuffixOf assumeMagicReturnCode bs
+        Just (VMFailure (Revert (ConcreteBuf bs))) -> not $ BS.isSuffixOf assumeMagicReturnCode bs
         Just (VMFailure _)           -> True
         _                            -> False
       isCorrectAddr = addr == vm ^. state . codeContract
diff --git a/lib/Echidna/Transaction.hs b/lib/Echidna/Transaction.hs
index e7dd9b301..fc19c4998 100644
--- a/lib/Echidna/Transaction.hs
+++ b/lib/Echidna/Transaction.hs
@@ -1,25 +1,24 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
 {-# LANGUAGE ViewPatterns #-}
 
 module Echidna.Transaction where
 
-import Prelude hiding (Word)
-
 import Control.Lens
 import Control.Monad (join, liftM2)
 import Control.Monad.Random.Strict (MonadRandom, getRandomR, uniform)
 import Control.Monad.Reader.Class (MonadReader)
 import Control.Monad.State.Strict (MonadState, State, runState, get, put)
-import Data.ByteString qualified as BS
 import Data.List.NonEmpty qualified as NE
 import Data.Has (Has(..))
 import Data.HashMap.Strict qualified as M
 import Data.Map (Map, toList)
-import Data.Maybe (catMaybes)
+import Data.Maybe (mapMaybe)
+import Data.Set (Set)
 import Data.Vector qualified as V
 import EVM hiding (value)
 import EVM.ABI (abiValueType)
-import EVM.Symbolic (litWord, litAddr)
-import EVM.Types (Addr, Buffer(..), Word(..), w256, w256lit, SymWord)
+import EVM.Types (Expr(ConcreteBuf, Lit), EType(EWord), Addr, W256)
 
 import Echidna.ABI
 import Echidna.Types.Random
@@ -54,9 +53,9 @@ genTxM memo m = do
   World ss hmm lmm ps _ <- view hasLens
   genDict <- use hasLens
   mm <- getSignatures hmm lmm
-  let ns = dictValues genDict
+  let ns = _dictValues genDict
   s' <- rElem ss
-  r' <- rElem $ NE.fromList . catMaybes $ toContractA mm <$> toList m
+  r' <- rElem $ NE.fromList (mapMaybe (toContractA mm) (toList m))
   c' <- genInteractionsM genDict (snd r')
   v' <- genValue mv ns ps c'
   t' <- (,) <$> genDelay t ns <*> genDelay b ns
@@ -68,24 +67,21 @@ genTxM memo m = do
       let metadata = lookupBytecodeMetadata memo bc
       (addr,) <$> M.lookup metadata mm
 
-genDelay :: MonadRandom m => Word -> [Integer] -> m Word
+genDelay :: MonadRandom m => W256 -> Set W256 -> m W256
 genDelay mv ds = do
-  let ds' = map (`mod` (fromIntegral mv + 1)) ds
-  g <- oftenUsually randValue $ rElem (0 NE.:| ds')
-  w256 . fromIntegral <$> g
-  where randValue = getRandomR (1 :: Integer, fromIntegral mv)
+  join $ oftenUsually fromDict randValue
+  where randValue = fromIntegral <$> getRandomR (1 :: Integer, fromIntegral mv)
+        fromDict = (`mod` (mv + 1)) <$> rElem' ds
 
-genValue :: MonadRandom m => Word -> [Integer] -> [FunctionHash] -> SolCall -> m Word
+genValue :: MonadRandom m => W256 -> Set W256 -> [FunctionHash] -> SolCall -> m W256
 genValue mv ds ps sc =
-  if sig `elem` ps then do
-    let ds' = map (`mod` (fromIntegral mv + 1)) ds
-    g <- oftenUsually randValue $ rElem (0 NE.:| ds')
-    fromIntegral <$> g
+  if sig `elem` ps then
+    join $ oftenUsually fromDict randValue
   else do
-    g <- usuallyVeryRarely (pure 0) randValue -- once in a while, this will generate value in a non-payable function
-    fromIntegral <$> g
-  where randValue = getRandomR (0 :: Integer, fromIntegral mv)
+    join $ usuallyVeryRarely (pure 0) randValue -- once in a while, this will generate value in a non-payable function
+  where randValue = fromIntegral <$> getRandomR (0 :: Integer, fromIntegral mv)
         sig = (hashSig . encodeSig . signatureCall) sc
+        fromDict = (`mod` (mv + 1)) <$> rElem' ds
 
 -- | Check if a 'Transaction' is as \"small\" (simple) as possible (using ad-hoc heuristics).
 canShrinkTx :: Tx -> Bool
@@ -101,13 +97,13 @@ removeCallTx (Tx _ _ r _ _ _ d) = Tx NoCall 0 r 0 0 0 d
 -- | Given a 'Transaction', generate a random \"smaller\" 'Transaction', preserving origin,
 -- destination, value, and call signature.
 shrinkTx :: MonadRandom m => Tx -> m Tx
-shrinkTx tx'@(Tx c _ _ _ gp (C _ v) (C _ t, C _ b)) = let
+shrinkTx tx'@(Tx c _ _ _ gp v (t, b)) = let
   c' = case c of
          SolCall sc -> SolCall <$> shrinkAbiCall sc
          _ -> pure c
-  lower 0 = pure $ w256 0
+  lower 0 = pure 0
   lower x = (getRandomR (0 :: Integer, fromIntegral x)
-              >>= (\r -> uniform [0, r]) . w256 . fromIntegral)  -- try 0 quicker
+              >>= (\r -> uniform [0, r]) . fromIntegral)  -- try 0 quicker
   possibilities =
     [ set call      <$> c'
     , set value     <$> lower v
@@ -139,20 +135,21 @@ liftSH = stateST . runState . zoom hasLens
 setupTx :: (MonadState x m, Has VM x) => Tx -> m ()
 setupTx (Tx NoCall _ r _ _ _ (t, b)) = liftSH . sequence_ $
   [ state . pc .= 0, state . stack .= mempty, state . memory .= mempty
-  , block . timestamp += litWord t, block . number += b, loadContract r]
+  , block . timestamp %= (\x -> Lit (forceLit x + t)), block . number += b, loadContract r]
 
 setupTx (Tx c s r g gp v (t, b)) = liftSH . sequence_ $
   [ result .= Nothing, state . pc .= 0, state . stack .= mempty, state . memory .= mempty, state . gas .= g
-  , tx . gasprice .= gp, tx . origin .= s, state . caller .= litAddr s, state . callvalue .= litWord v
-  , block . timestamp += litWord t, block . number += b, setup] where
+  , tx . gasprice .= gp, tx . origin .= s, state . caller .= Lit (fromIntegral s), state . callvalue .= Lit v
+  , block . timestamp %= (\x -> Lit (forceLit x + t)), block . number += b, setup] where
     setup = case c of
-      SolCreate bc   -> assign (env . contracts . at r) (Just $ initialContract (InitCode (ConcreteBuffer bc)) & set balance v) >> loadContract r >> state . code .= ConcreteBuffer bc
-      SolCall cd     -> incrementBalance >> loadContract r >> state . calldata .= concreteCalldata (encode cd)
-      SolCalldata cd -> incrementBalance >> loadContract r >> state . calldata .= concreteCalldata cd
-      NoCall         -> error "NoCall"
+      SolCreate bc   -> assign (env . contracts . at r) (Just $ initialContract (InitCode bc mempty) & set balance v) >> loadContract r >> state . code .= RuntimeCode (ConcreteRuntimeCode bc)
+      SolCall cd     -> incrementBalance >> loadContract r >> state . calldata .= ConcreteBuf (encode cd)
+      SolCalldata cd -> incrementBalance >> loadContract r >> state . calldata .= ConcreteBuf cd
     incrementBalance = (env . contracts . ix r . balance) += v
     encode (n, vs) = abiCalldata
       (encodeSig (n, abiValueType <$> vs)) $ V.fromList vs
 
-concreteCalldata :: BS.ByteString -> (Buffer, SymWord)
-concreteCalldata cd = (ConcreteBuffer cd, w256lit . fromIntegral . BS.length $ cd)
+forceLit :: Expr 'EWord -> W256
+forceLit x = case x of
+  Lit x' -> x'
+  _ -> error "expected Lit"
diff --git a/lib/Echidna/Types/Buffer.hs b/lib/Echidna/Types/Buffer.hs
index ee694174d..bf7f585c0 100644
--- a/lib/Echidna/Types/Buffer.hs
+++ b/lib/Echidna/Types/Buffer.hs
@@ -1,9 +1,10 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
 module Echidna.Types.Buffer where
 
 import Data.ByteString (ByteString)
-import EVM.Types (Buffer(..))
-import EVM.Symbolic (maybeLitBytes)
+import EVM.Types (Expr(ConcreteBuf), EType(Buf))
 
-viewBuffer :: Buffer -> Maybe ByteString
-viewBuffer (ConcreteBuffer b) = Just b
-viewBuffer (SymbolicBuffer b) = maybeLitBytes b
+viewBuffer :: Expr 'Buf -> Maybe ByteString
+viewBuffer (ConcreteBuf b) = Just b
+viewBuffer _ = Nothing
diff --git a/lib/Echidna/Types/Campaign.hs b/lib/Echidna/Types/Campaign.hs
index 82484795d..f7ee8a790 100644
--- a/lib/Echidna/Types/Campaign.hs
+++ b/lib/Echidna/Types/Campaign.hs
@@ -8,7 +8,7 @@ import Data.Foldable (toList)
 import Data.Has (Has(..))
 import Data.Map (Map, mapKeys)
 import Data.Text (Text)
-import EVM.Types (keccak)
+import EVM.Types (keccak')
 import Numeric (showHex)
 
 import Echidna.ABI (GenDict, defaultDict)
@@ -66,7 +66,7 @@ makeLenses ''Campaign
 
 instance ToJSON Campaign where
   toJSON (Campaign ts co gi _ _ _ _ _) = object $ ("tests", toJSON $ map format ts)
-    : [("coverage",) . toJSON . mapKeys (("0x" <>) . (`showHex` "") . keccak) $ toList <$> co | co /= mempty] ++
+    : [("coverage",) . toJSON . mapKeys (("0x" <>) . (`showHex` "") . keccak') $ toList <$> co | co /= mempty] ++
       [(("maxgas",) . toJSON . toList) gi | gi /= mempty] where
         format _ = "" :: String -- TODO: complete this format string
 
diff --git a/lib/Echidna/Types/Random.hs b/lib/Echidna/Types/Random.hs
index 396ba3d6b..bd6db7a56 100644
--- a/lib/Echidna/Types/Random.hs
+++ b/lib/Echidna/Types/Random.hs
@@ -3,6 +3,8 @@ module Echidna.Types.Random where
 import Prelude hiding ((!!))
 import Control.Monad.Random.Strict (MonadRandom, getRandomR, weighted)
 import Data.List.NonEmpty ((!!), NonEmpty(..))
+import Data.Set (Set)
+import Data.Set qualified as S
 
 type Seed = Int
 
@@ -10,6 +12,10 @@ type Seed = Int
 rElem :: MonadRandom m => NonEmpty a -> m a
 rElem l  = (l !!) <$> getRandomR (0, length l - 1)
 
+-- | Get a random element of a Set
+rElem' :: MonadRandom m => Set a -> m a
+rElem' v = (`S.elemAt` v) <$> getRandomR (0, length v - 1)
+
 oftenUsually :: MonadRandom m => a -> a -> m a
 oftenUsually u r = weighted [(u, 10), (r, 1)]
 
diff --git a/lib/Echidna/Types/Signature.hs b/lib/Echidna/Types/Signature.hs
index d88f042b8..508109bfd 100644
--- a/lib/Echidna/Types/Signature.hs
+++ b/lib/Echidna/Types/Signature.hs
@@ -1,3 +1,5 @@
+{-# LANGUAGE GADTs #-}
+
 module Echidna.Types.Signature where
 
 import Data.ByteString (ByteString)
diff --git a/lib/Echidna/Types/Tx.hs b/lib/Echidna/Types/Tx.hs
index 7ab28a2c0..90a32c973 100644
--- a/lib/Echidna/Types/Tx.hs
+++ b/lib/Echidna/Types/Tx.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE GADTs #-}
 
 module Echidna.Types.Tx where
 
@@ -8,13 +9,14 @@ import Control.Lens.TH (makePrisms, makeLenses)
 import Data.Aeson.TH (deriveJSON, defaultOptions)
 import Data.ByteString (ByteString)
 import Data.Text (Text)
+import Data.Word (Word64)
 
 import EVM (VMResult(..), Error(..))
 import EVM.ABI (encodeAbiValue, AbiValue(..))
-import EVM.Types (Addr, W256, Word, w256)
+import EVM.Types (Addr, W256)
 
-import Echidna.Types.Buffer (viewBuffer)
 import Echidna.Orphans.JSON ()
+import Echidna.Types.Buffer (viewBuffer)
 import Echidna.Types.Signature (SolCall)
 
 -- | A transaction call is either a @CREATE@, a fully instrumented 'SolCall', or
@@ -39,10 +41,10 @@ defaultTimeDelay = 604800
 defaultBlockDelay :: Integer
 defaultBlockDelay = 60480
 
-initialTimestamp :: Word
+initialTimestamp :: W256
 initialTimestamp = 1524785992 -- Thu Apr 26 23:39:52 UTC 2018
 
-initialBlockNumber :: Word
+initialBlockNumber :: W256
 initialBlockNumber = 4370000  -- Initial byzantium block
 
 -- | A transaction is either a @CREATE@ or a regular call with an origin, destination, and value.
@@ -50,10 +52,10 @@ initialBlockNumber = 4370000  -- Initial byzantium block
 data Tx = Tx { _call  :: TxCall       -- | Call
              , _src   :: Addr         -- | Origin
              , _dst   :: Addr         -- | Destination
-             , _gas'  :: Word         -- | Gas
-             , _gasprice' :: Word     -- | Gas price
-             , _value :: Word         -- | Value
-             , _delay :: (Word, Word) -- | (Time, # of blocks since last call)
+             , _gas'  :: Word64       -- | Gas
+             , _gasprice' :: W256     -- | Gas price
+             , _value :: W256         -- | Value
+             , _delay :: (W256, W256) -- | (Time, # of blocks since last call)
              } deriving (Eq, Ord, Show)
 makeLenses ''Tx
 $(deriveJSON defaultOptions ''Tx)
@@ -62,8 +64,8 @@ basicTx :: Text         -- | Function name
         -> [AbiValue]   -- | Function args
         -> Addr         -- | Sender
         -> Addr         -- | Destination contract
-        -> Word         -- | Gas limit
-        -> (Word, Word) -- | Block increment
+        -> Word64       -- | Gas limit
+        -> (W256, W256) -- | Block increment
         -> Tx
 basicTx f a s d g = basicTxWithValue f a s d g 0
 
@@ -71,26 +73,26 @@ basicTxWithValue :: Text         -- | Function name
                  -> [AbiValue]   -- | Function args
                  -> Addr         -- | Sender
                  -> Addr         -- | Destination contract
-                 -> Word         -- | Gas limit
-                 -> Word         -- | Value
-                 -> (Word, Word) -- | Block increment
+                 -> Word64       -- | Gas limit
+                 -> W256         -- | Value
+                 -> (W256, W256) -- | Block increment
                  -> Tx
 basicTxWithValue f a s d g = Tx (SolCall (f, a)) s d g 0
 
 createTx :: ByteString   -- | Constructor bytecode
          -> Addr         -- | Creator
          -> Addr         -- | Destination address
-         -> Word         -- | Gas limit
-         -> (Word, Word) -- | Block increment
+         -> Word64       -- | Gas limit
+         -> (W256, W256) -- | Block increment
          -> Tx
 createTx bc s d g = createTxWithValue bc s d g 0
 
 createTxWithValue :: ByteString   -- | Constructor bytecode
                   -> Addr         -- | Creator
                   -> Addr         -- | Destination address
-                  -> Word         -- | Gas limit
-                  -> Word         -- | Value
-                  -> (Word, Word) -- | Block increment
+                  -> Word64       -- | Gas limit
+                  -> W256         -- | Value
+                  -> (W256, W256) -- | Block increment
                   -> Tx
 createTxWithValue bc s d g = Tx (SolCreate bc) s d g 0
 
@@ -120,20 +122,21 @@ data TxResult = ReturnTrue
               | ErrorWhiffNotUnique
               | ErrorSMTTimeout
               | ErrorFFI
+              | ErrorNonceOverflow
   deriving (Eq, Ord, Show)
 $(deriveJSON defaultOptions ''TxResult)
 
-data TxConf = TxConf { _propGas       :: Word
+data TxConf = TxConf { _propGas       :: Word64
                      -- ^ Gas to use evaluating echidna properties
-                     , _txGas         :: Word
+                     , _txGas         :: Word64
                      -- ^ Gas to use in generated transactions
-                     , _maxGasprice   :: Word
+                     , _maxGasprice   :: W256
                      -- ^ Maximum gasprice to be checked for a transaction
-                     , _maxTimeDelay  :: Word
+                     , _maxTimeDelay  :: W256
                      -- ^ Maximum time delay between transactions (seconds)
-                     , _maxBlockDelay :: Word
+                     , _maxBlockDelay :: W256
                      -- ^ Maximum block delay between transactions
-                     , _maxValue      :: Word
+                     , _maxValue      :: W256
                      -- ^ Maximum value to use in transactions
                      }
 makeLenses 'TxConf
@@ -160,13 +163,14 @@ getResult (VMFailure InvalidMemoryAccess)       = ErrorInvalidMemoryAccess
 getResult (VMFailure CallDepthLimitReached)     = ErrorCallDepthLimitReached
 getResult (VMFailure (MaxCodeSizeExceeded _ _)) = ErrorMaxCodeSizeExceeded
 getResult (VMFailure PrecompileFailure)         = ErrorPrecompileFailure
-getResult (VMFailure UnexpectedSymbolicArg)     = ErrorUnexpectedSymbolic
+getResult (VMFailure (UnexpectedSymbolicArg{})) = ErrorUnexpectedSymbolic
 getResult (VMFailure DeadPath)                  = ErrorDeadPath
 getResult (VMFailure (Choose _))                = ErrorChoose -- not entirely sure what this is
 getResult (VMFailure (NotUnique _))             = ErrorWhiffNotUnique
 getResult (VMFailure SMTTimeout)                = ErrorSMTTimeout
 getResult (VMFailure (FFI _))                   = ErrorFFI
+getResult (VMFailure NonceOverflow)             = ErrorNonceOverflow
 
 makeSingleTx :: Addr -> Addr -> W256 -> TxCall -> [Tx]
-makeSingleTx a d v (SolCall c) = [Tx (SolCall c) a d (fromInteger maxGasPerBlock) 0 (w256 v) (0, 0)]
+makeSingleTx a d v (SolCall c) = [Tx (SolCall c) a d (fromInteger maxGasPerBlock) 0 v (0, 0)]
 makeSingleTx _ _ _ _           = error "invalid usage of makeSingleTx"
diff --git a/lib/Echidna/UI.hs b/lib/Echidna/UI.hs
index f7ffbe974..f63e3476b 100644
--- a/lib/Echidna/UI.hs
+++ b/lib/Echidna/UI.hs
@@ -125,13 +125,13 @@ monitor = do
   let cs :: (CampaignConf, Names, TxConf) -> (Campaign, UIState) -> Widget ()
       cs s c = runReader (campaignStatus c) s
 
-      se _ (AppEvent (CampaignUpdated c')) = continue (c', Running)
-      se _ (AppEvent (CampaignTimedout c')) = continue (c', Timedout)
-      se c (VtyEvent (EvKey KEsc _))                         = halt c
-      se c (VtyEvent (EvKey (KChar 'c') l)) | MCtrl `elem` l = halt c
-      se c _                                                 = continue c
+      se (AppEvent (CampaignUpdated c')) = put (c', Running)
+      se (AppEvent (CampaignTimedout c')) = put (c', Timedout)
+      se (VtyEvent (EvKey KEsc _))                         = halt
+      se (VtyEvent (EvKey (KChar 'c') l)) | MCtrl `elem` l = halt
+      se _                                                 = pure ()
   s <- (,,) <$> view hasLens <*> view hasLens <*> view hasLens
-  pure $ App (pure . cs s) neverShowCursor se pure (const attrs)
+  pure $ App (pure . cs s) neverShowCursor se (pure ()) (const attrs)
 
 -- | Heuristic check that we're in a sensible terminal (not a pipe)
 isTerminal :: MonadIO m => m Bool
diff --git a/lib/Echidna/UI/Widgets.hs b/lib/Echidna/UI/Widgets.hs
index 1fc565bbb..189c6b394 100644
--- a/lib/Echidna/UI/Widgets.hs
+++ b/lib/Echidna/UI/Widgets.hs
@@ -27,12 +27,12 @@ data UIState = Uninitialized | Running | Timedout
 
 attrs :: A.AttrMap
 attrs = A.attrMap (V.white `on` V.black)
-  [ ("failure", fg V.brightRed)
-  , ("maximum", fg V.brightBlue)
-  , ("bold", fg V.white `V.withStyle` V.bold)
-  , ("tx", fg V.brightWhite)
-  , ("working", fg V.brightBlue)
-  , ("success", fg V.brightGreen)
+  [ (attrName "failure", fg V.brightRed)
+  , (attrName "maximum", fg V.brightBlue)
+  , (attrName "bold", fg V.white `V.withStyle` V.bold)
+  , (attrName "tx", fg V.brightWhite)
+  , (attrName "working", fg V.brightBlue)
+  , (attrName "success", fg V.brightGreen)
   ]
 
 -- | Render 'Campaign' progress as a 'Widget'.
@@ -53,7 +53,7 @@ campaignStatus (c@Campaign{_tests, _coverage, _ncallseqs}, uiState) = do
       <=>
       hCenter underneath
     wrapInner inner =
-      borderWithLabel (withAttr "bold" $ str title) $
+      borderWithLabel (withAttr (attrName "bold") $ str title) $
       summaryWidget c
       <=>
       hBorderWithLabel (str "Tests")
@@ -96,19 +96,19 @@ testWidget etest =
     pure $ padLeft (Pad 1) $
       str infront <+> name n <+> str ": " <+> status
       <=> padTop (Pad 1) details
-  name n = withAttr "bold" $ str (T.unpack n)
+  name n = withAttr (attrName "bold") $ str (T.unpack n)
 
 tsWidget :: (MonadReader x m, Has CampaignConf x, Has Names x, Has TxConf x)
          => TestState -> EchidnaTest -> m (Widget (), Widget ())
 tsWidget (Failed e) _ = pure (str "could not evaluate", str $ show e)
 tsWidget Solved     t = failWidget Nothing (t ^. testReproducer) (t ^. testEvents) (t ^. testValue) (t  ^. testResult)
-tsWidget Passed     _ = pure (withAttr "success" $ str "PASSED!", emptyWidget)
+tsWidget Passed     _ = pure (withAttr (attrName "success") $ str "PASSED!", emptyWidget)
 tsWidget (Open i)   t = do
   n <- view (hasLens . testLimit)
   if i >= n then
     tsWidget Passed t
   else
-    pure (withAttr "working" $ str $ "fuzzing " ++ progress i n, emptyWidget)
+    pure (withAttr (attrName "working") $ str $ "fuzzing " ++ progress i n, emptyWidget)
 tsWidget (Large n)  t = do
   m <- view (hasLens . shrinkLimit)
   failWidget (if n < m then Just (n,m) else Nothing) (t ^. testReproducer) (t ^. testEvents) (t ^. testValue) (t  ^. testResult)
@@ -131,7 +131,7 @@ failWidget b xs es _ r = do
   where
   status = case b of
     Nothing    -> emptyWidget
-    Just (n,m) -> str "Current action: " <+> withAttr "working" (str ("shrinking " ++ progress n m))
+    Just (n,m) -> str "Current action: " <+> withAttr (attrName "working") (str ("shrinking " ++ progress n m))
 
 
 optWidget :: (MonadReader x m, Has CampaignConf x, Has Names x, Has TxConf x)
@@ -144,7 +144,7 @@ optWidget (Open i)   t = do
   if i >= n then
     optWidget Passed t
   else
-    pure (withAttr "working" $ str $ "optimizing " ++ progress i n ++ ", current max value: " ++ show (t ^. testValue), emptyWidget)
+    pure (withAttr (attrName "working") $ str $ "optimizing " ++ progress i n ++ ", current max value: " ++ show (t ^. testValue), emptyWidget)
 optWidget (Large n)  t = do
   m <- view (hasLens . shrinkLimit)
   maxWidget (if n < m then Just (n,m) else Nothing) (t ^. testReproducer) (t ^. testEvents) (t ^. testValue)
@@ -158,7 +158,7 @@ maxWidget b xs es v = do
   where
   status = case b of
     Nothing    -> emptyWidget
-    Just (n,m) -> str "Current action: " <+> withAttr "working" (str ("shrinking " ++ progress n m))
+    Just (n,m) -> str "Current action: " <+> withAttr (attrName "working") (str ("shrinking " ++ progress n m))
 
 
 seqWidget :: (MonadReader x m, Has Names x, Has TxConf x) => [Tx] -> m (Widget ())
@@ -167,13 +167,13 @@ seqWidget xs = do
     let ordinals = str . printf "%d." <$> [1 :: Int ..]
     pure $
       foldl (<=>) emptyWidget $
-        zipWith (<+>) ordinals (withAttr "tx" . strWrapWith wrapSettings <$> ppTxs)
+        zipWith (<+>) ordinals (withAttr (attrName "tx") . strWrapWith wrapSettings <$> ppTxs)
 
 failureBadge :: Widget ()
-failureBadge = withAttr "failure" $ str "FAILED!"
+failureBadge = withAttr (attrName "failure") $ str "FAILED!"
 
 maximumBadge :: Widget ()
-maximumBadge = withAttr "maximum" $ str "OPTIMIZED!"
+maximumBadge = withAttr (attrName "maximum") $ str "OPTIMIZED!"
 
 wrapSettings :: WrapSettings
 wrapSettings = defaultWrapSettings { breakLongWords = True }
diff --git a/package.yaml b/package.yaml
index 187a95c13..1c838d1c7 100644
--- a/package.yaml
+++ b/package.yaml
@@ -47,23 +47,20 @@ dependencies:
   - word-wrap
   - yaml
 
+language: GHC2021
+
 default-extensions:
   - LambdaCase
   - OverloadedStrings
-  # GHC2021 default extensions from 9.2
-  - FlexibleContexts
-  - FlexibleInstances
-  - ImportQualifiedPost
-  - MultiParamTypeClasses
-  - NamedFieldPuns
-  - RankNTypes
-  - ScopedTypeVariables
-  - StandaloneDeriving
-  - TupleSections
 
 library:
   source-dirs: lib/
 
+when:
+  - condition: os(darwin)
+    extra-libraries: c++
+    ld-options: -Wl,-keep_dwarf_unwind
+
 executables:
   echidna-test:
     main: Main.hs
diff --git a/src/test/Common.hs b/src/test/Common.hs
index 246928286..735aed607 100644
--- a/src/test/Common.hs
+++ b/src/test/Common.hs
@@ -69,14 +69,18 @@ withSolcVersion :: Maybe SolcVersionComp -> IO () -> IO ()
 withSolcVersion Nothing t = t
 withSolcVersion (Just f) t = do
   sv <- readProcess "solc" ["--version"] ""
-  let (_:sv':_) = splitOn "Version: " sv
-  let (sv'':_) = splitOn "+" sv'
+  let sv' = case splitOn "Version: " sv of
+              _:x:_ -> x
+              _ -> error "unexpected output"
+  let sv'' = case splitOn "+" sv' of
+               x:_ -> x
+               _ -> error "unexpected output"
   case fromText $ pack sv'' of
     Right v' -> if f v' then t else assertBool "skip" True
     Left e   -> error $ show e
 
 runContract :: FilePath -> Maybe ContractName -> EConfig -> IO Campaign
-runContract f mc cfg = 
+runContract f mc cfg =
   flip runReaderT cfg $ do
     g <- getRandom
     (v, sc, cs, w, ts, d, txs) <- prepareContract cfg (f :| []) mc g
@@ -109,11 +113,13 @@ checkConstructorConditions fp as = testCase fp $ do
     let env = Env { _cfg = testConfig, _dapp = emptyDapp }
     flip runReaderT env $
       mapM (\u -> evalStateT (checkETest u) v) t
-  mapM_ (\(BoolValue b,_,_) -> assertBool as b) r
+  mapM_ (\(x,_,_) -> assertBool as (forceBool x)) r
+  where forceBool (BoolValue b) = b
+        forceBool _ = error "BoolValue expected"
 
 
 getResult :: Text -> Campaign -> Maybe EchidnaTest
-getResult n c = 
+getResult n c =
   case filter findTest $ view tests c of
     []  -> Nothing
     [x] -> Just x
@@ -124,7 +130,7 @@ getResult n c =
                           AssertionTest _ (t,_) _ -> t == n
                           CallTest t _            -> t == n
                           OptimizationTest t _    -> t == n
-                          _                       -> False 
+                          _                       -> False
 
 optnFor :: Text -> Campaign -> Maybe TestValue
 optnFor n c = case getResult n c of
@@ -139,7 +145,7 @@ optimized n v c = case optnFor n c of
 
 solnFor :: Text -> Campaign -> Maybe [Tx]
 solnFor n c = case getResult n c of
-  Just t -> if null $ t ^. testReproducer then Nothing else Just $ t ^. testReproducer 
+  Just t -> if null $ t ^. testReproducer then Nothing else Just $ t ^. testReproducer
   _      -> Nothing
 
 solved :: Text -> Campaign -> Bool
diff --git a/src/test/Tests/Compile.hs b/src/test/Tests/Compile.hs
index 2353f5934..008cda4d6 100644
--- a/src/test/Tests/Compile.hs
+++ b/src/test/Tests/Compile.hs
@@ -5,6 +5,7 @@ import Test.Tasty.HUnit (testCase, assertBool)
 
 import Common (testConfig)
 import Control.Lens (Prism', preview)
+import Control.Monad (void)
 import Control.Monad.Catch (catch)
 import Control.Monad.Reader (runReaderT)
 import Data.List.NonEmpty (NonEmpty(..))
@@ -37,7 +38,7 @@ compilationTests = testGroup "Compilation and loading tests"
 
 loadFails :: FilePath -> Maybe Text -> String -> (SolException -> Bool) -> TestTree
 loadFails fp c e p = testCase fp . catch tryLoad $ assertBool e . p where
-  tryLoad = runReaderT (loadWithCryticCompile (fp :| []) c >> pure ()) testConfig
+  tryLoad = runReaderT (void (loadWithCryticCompile (fp :| []) c)) testConfig
 
 pmatch :: Prism' s a -> s -> Bool
 pmatch p = isJust . preview p
diff --git a/src/test/Tests/Encoding.hs b/src/test/Tests/Encoding.hs
index 49441af1f..b5476a61a 100644
--- a/src/test/Tests/Encoding.hs
+++ b/src/test/Tests/Encoding.hs
@@ -1,19 +1,17 @@
 module Tests.Encoding (encodingJSONTests) where
 
-import Prelude hiding (Word)
-
 import Test.Tasty (TestTree, testGroup)
 import Test.Tasty.QuickCheck (Arbitrary(..), Gen, (===), property, testProperty, resize)
 
 import Data.Aeson (encode, decode)
 import Data.Text (pack)
 import Echidna.Types.Tx (TxCall(..), Tx(..))
-import EVM.Types (Addr, Word)
+import EVM.Types (Addr, W256)
 
 instance Arbitrary Addr where
   arbitrary = fromInteger <$> arbitrary
 
-instance Arbitrary Word where
+instance Arbitrary W256 where
   arbitrary = fromInteger <$> arbitrary
 
 instance Arbitrary TxCall where
diff --git a/stack.yaml b/stack.yaml
index fa7c2b915..89cf9c4e8 100644
--- a/stack.yaml
+++ b/stack.yaml
@@ -1,18 +1,18 @@
-resolver: lts-19.33
+resolver: lts-20.05
 
 packages:
 - '.'
 
 extra-deps:
-- git: https://github.com/crytic/dapptools.git
-  commit: f1ccf43e466b4fdfee4b18d137bd393632d5afda
-  subdirs:
-  - src/hevm
+- git: https://github.com/ethereum/hevm.git
+  commit: 021d6355df0778638054fb4742cd9b110ea3b314
 
 - restless-git-0.7@sha256:346a5775a586f07ecb291036a8d3016c3484ccdc188b574bcdec0a82c12db293,968
 - s-cargot-0.1.4.0@sha256:61ea1833fbb4c80d93577144870e449d2007d311c34d74252850bb48aa8c31fb,3525
 - semver-range-0.2.8@sha256:44918080c220cf67b6e7c8ad16f01f3cfe1ac69d4f72e528e84d566348bb23c3,1941
 - HSH-2.1.3@sha256:71ded11b224f5066373ce985ec63b10c87129850b33916736dd64fa2bea9ea0a,1705
+- spool-0.1@sha256:77780cbfc2c0be23ff2ea9e474062f3df97fcd9db946ee0b3508280a923b83e2,1461
+- smt2-parser-0.1.0.1@sha256:1e1a4565915ed851c13d1e6b8bb5185cf5d454da3b43170825d53e221f753d77,1421
 
 extra-include-dirs:
 - /usr/local/opt/readline/include