diff --git a/.github/scripts/install-z3.sh b/.github/scripts/install-z3.sh
new file mode 100755
index 000000000..e67671bd4
--- /dev/null
+++ b/.github/scripts/install-z3.sh
@@ -0,0 +1,10 @@
+#!/bin/bash
+set -eux -o pipefail
+
+if [ "$HOST_OS" = "Linux" ]; then
+  sudo apt-get update
+  sudo apt-get install -y z3
+fi
+if [ "$HOST_OS" = "Windows" ]; then
+  choco install z3
+fi
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 4b17b4874..45dabc9db 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -216,6 +216,7 @@ jobs:
         run: |
           .github/scripts/install-solc.sh
           .github/scripts/install-crytic-compile.sh
+          .github/scripts/install-z3.sh
         env:
           HOST_OS: ${{ runner.os }}
           SOLC_VER: ${{ matrix.solc }}
diff --git a/lib/Echidna/Campaign.hs b/lib/Echidna/Campaign.hs
index 67b3f6b3e..c5505b269 100644
--- a/lib/Echidna/Campaign.hs
+++ b/lib/Echidna/Campaign.hs
@@ -5,7 +5,7 @@ module Echidna.Campaign where
 
 import Control.Concurrent
 import Control.DeepSeq (force)
-import Control.Monad (replicateM, when, void, forM_)
+import Control.Monad (replicateM, when, unless, void, forM_)
 import Control.Monad.Catch (MonadThrow(..))
 import Control.Monad.Random.Strict (MonadRandom, RandT, evalRandT)
 import Control.Monad.Reader (MonadReader, asks, liftIO, ask)
@@ -16,6 +16,7 @@ import Control.Monad.Trans (lift)
 import Data.Binary.Get (runGetOrFail)
 import Data.ByteString.Lazy qualified as LBS
 import Data.IORef (readIORef, atomicModifyIORef')
+import Data.Foldable (foldlM)
 import Data.List qualified as List
 import Data.Map qualified as Map
 import Data.Map (Map, (\\))
@@ -28,6 +29,7 @@ import System.Random (mkStdGen)
 
 import EVM (cheatCode)
 import EVM.ABI (getAbi, AbiType(AbiAddressType), AbiValue(AbiAddress))
+import EVM.Solidity (SolcContract)
 import EVM.Types hiding (Env, Frame(state), Gas)
 
 import Echidna.ABI
@@ -35,6 +37,7 @@ import Echidna.Exec
 import Echidna.Mutator.Corpus
 import Echidna.Shrink (shrinkTest)
 import Echidna.Symbolic (forceAddr)
+import Echidna.SymExec (createSymTx)
 import Echidna.Test
 import Echidna.Transaction
 import Echidna.Types (Gas)
@@ -78,10 +81,116 @@ replayCorpus vm txSeqs =
       Just faultyTx ->
         pushWorkerEvent (TxSequenceReplayFailed file faultyTx)
 
+runWorker
+  :: (MonadIO m, MonadThrow m, MonadReader Env m)
+  => WorkerType
+  -> StateT WorkerState m ()
+  -- ^ Callback to run after each state update (for instrumentation)
+  -> VM Concrete RealWorld -- ^ Initial VM state
+  -> World   -- ^ Initial world state
+  -> GenDict -- ^ Generation dictionary
+  -> Int     -- ^ Worker id starting from 0
+  -> [(FilePath, [Tx])]
+  -- ^ Initial corpus of transactions
+  -> Int     -- ^ Test limit for this worker
+  -> Maybe Text -- ^ Specified contract name
+  -> [SolcContract] -- ^ List of contracts
+  -> m (WorkerStopReason, WorkerState)
+runWorker SymbolicWorker callback vm _ dict workerId initialCorpus _ name cs = runSymWorker callback vm dict workerId initialCorpus name cs
+runWorker FuzzWorker callback vm world dict workerId initialCorpus testLimit _ _ = runFuzzWorker callback vm world dict workerId initialCorpus testLimit
+
+runSymWorker
+  :: (MonadIO m, MonadThrow m, MonadReader Env m)
+  => StateT WorkerState m ()
+  -- ^ Callback to run after each state update (for instrumentation)
+  -> VM Concrete RealWorld -- ^ Initial VM state
+  -> GenDict -- ^ Generation dictionary
+  -> Int     -- ^ Worker id starting from 0
+  -> [(FilePath, [Tx])]
+  -- ^ Initial corpus of transactions
+  -> Maybe Text -- ^ Specified contract name
+  -> [SolcContract] -- ^ List of contracts
+  -> m (WorkerStopReason, WorkerState)
+runSymWorker callback vm dict workerId initialCorpus name cs = do
+  cfg <- asks (.cfg)
+  let nworkers = getNFuzzWorkers cfg.campaignConf -- getNFuzzWorkers, NOT getNWorkers
+  eventQueue <- asks (.eventQueue)
+  chan <- liftIO $ dupChan eventQueue
+
+  flip runStateT initialState $
+    flip evalRandT (mkStdGen effectiveSeed) $ do -- unused but needed for callseq
+      lift callback
+      void $ replayCorpus vm initialCorpus
+      symexecTxs []
+      mapM_ (symexecTxs . snd) initialCorpus
+      listenerLoop listenerFunc chan nworkers
+      pure SymbolicDone
+
+  where
+
+  effectiveSeed = dict.defSeed + workerId
+  effectiveGenDict = dict { defSeed = effectiveSeed }
+  initialState =
+    WorkerState { workerId
+                , gasInfo = mempty
+                , genDict = effectiveGenDict
+                , newCoverage = False
+                , ncallseqs = 0
+                , ncalls = 0
+                , runningThreads = []
+                }
+
+  -- We could pattern match on workerType here to ignore WorkerEvents from SymbolicWorkers,
+  -- but it may be useful to symexec on top of symexec results to produce multi-transaction
+  -- chains where each transaction results in new coverage.
+  listenerFunc (_, WorkerEvent _ _ (NewCoverage {transactions})) = do
+    void $ callseq vm transactions
+    symexecTxs transactions
+  listenerFunc _ = pure ()
+
+  symexecTxs txs = mapM_ symexecTx =<< txsToTxAndVms txs
+
+  -- | Turn a list of transactions into inputs for symexecTx:
+  -- (maybe txn to concolic execute on, vm to symexec on, list of txns we're on top of)
+  txsToTxAndVms txs = do
+    isConc <- asks (.cfg.campaignConf.symExecConcolic)
+    if isConc
+      then txsToTxAndVmsConc txs vm []
+      else txsToTxAndVmsSym txs
+
+  txsToTxAndVmsConc [] _ _ = pure []
+  txsToTxAndVmsConc (h:t) vm' txsBase = do
+    (_, vm'') <- execTx vm' h
+    rest <- txsToTxAndVmsConc t vm'' (txsBase <> [h])
+    pure $ case h of
+             (Tx { call = SolCall _ }) -> (Just h,vm',txsBase):rest
+             _ -> rest
+
+  txsToTxAndVmsSym txs = do
+    vm' <- foldlM (\vm' tx -> snd <$> execTx vm' tx) vm txs
+    pure [(Nothing,vm',txs)]
+
+  symexecTx (tx, vm', txsBase) = do
+    cfg <- asks (.cfg)
+    (threadId, symTxsChan) <- liftIO $ createSymTx cfg name cs tx vm'
+
+    modify' (\ws -> ws { runningThreads = [threadId] })
+    lift callback
+
+    symTxs <- liftIO $ takeMVar symTxsChan
+
+    modify' (\ws -> ws { runningThreads = [] })
+    lift callback
+
+    -- We can't do callseq vm' [symTx] because callseq might post the full call sequence as an event
+    newCoverage <- or <$> mapM (\symTx -> snd <$> callseq vm (txsBase <> [symTx])) symTxs
+
+    unless newCoverage (pushWorkerEvent SymNoNewCoverage)
+
 -- | Run a fuzzing campaign given an initial universe state, some tests, and an
 -- optional dictionary to generate calls with. Return the 'Campaign' state once
 -- we can't solve or shrink anything.
-runWorker
+runFuzzWorker
   :: (MonadIO m, MonadThrow m, MonadReader Env m)
   => StateT WorkerState m ()
   -- ^ Callback to run after each state update (for instrumentation)
@@ -93,7 +202,7 @@ runWorker
   -- ^ Initial corpus of transactions
   -> Int     -- ^ Test limit for this worker
   -> m (WorkerStopReason, WorkerState)
-runWorker callback vm world dict workerId initialCorpus testLimit = do
+runFuzzWorker callback vm world dict workerId initialCorpus testLimit = do
   let
     effectiveSeed = dict.defSeed + workerId
     effectiveGenDict = dict { defSeed = effectiveSeed }
@@ -104,6 +213,7 @@ runWorker callback vm world dict workerId initialCorpus testLimit = do
                   , newCoverage = False
                   , ncallseqs = 0
                   , ncalls = 0
+                  , runningThreads = []
                   }
 
   flip runStateT initialState $ do
@@ -150,7 +260,7 @@ runWorker callback vm world dict workerId initialCorpus testLimit = do
        | otherwise ->
          lift callback >> pure TestLimitReached
 
-  fuzz = randseq vm.env.contracts world >>= callseq vm
+  fuzz = randseq vm.env.contracts world >>= fmap fst . callseq vm
 
   continue = runUpdate (shrinkTest vm) >> lift callback >> run
 
@@ -183,13 +293,16 @@ randseq deployedContracts world = do
     then pure randTxs -- Use the generated random transactions
     else mut seqLen corpus randTxs -- Apply the mutator
 
+-- TODO callseq ideally shouldn't need to be MonadRandom
+
 -- | Runs a transaction sequence and checks if any test got falsified or can be
 -- minimized. Stores any useful data in the campaign state if coverage increased.
+-- Returns resulting VM, as well as whether any new coverage was found.
 callseq
   :: (MonadIO m, MonadThrow m, MonadRandom m, MonadReader Env m, MonadState WorkerState m)
   => VM Concrete RealWorld
   -> [Tx]
-  -> m (VM Concrete RealWorld)
+  -> m (VM Concrete RealWorld, Bool)
 callseq vm txSeq = do
   env <- ask
   -- First, we figure out whether we need to execute with or without coverage
@@ -254,7 +367,7 @@ callseq vm txSeq = do
       , ncallseqs = workerState.ncallseqs + 1
       }
 
-  pure vm'
+  pure (vm', newCoverage)
 
   where
   -- Given a list of transactions and a return typing rule, checks whether we
@@ -402,7 +515,8 @@ pushWorkerEvent
 pushWorkerEvent event = do
   workerId <- gets (.workerId)
   env <- ask
-  liftIO $ pushCampaignEvent env (WorkerEvent workerId event)
+  let workerType = workerIDToType env.cfg.campaignConf workerId
+  liftIO $ pushCampaignEvent env (WorkerEvent workerId workerType event)
 
 pushCampaignEvent :: Env -> CampaignEvent -> IO ()
 pushCampaignEvent env event = do
@@ -424,17 +538,28 @@ spawnListener
   -> m (MVar ())
 spawnListener handler = do
   cfg <- asks (.cfg)
-  let nworkers = fromMaybe 1 cfg.campaignConf.workers
+  let nworkers = getNWorkers cfg.campaignConf
   eventQueue <- asks (.eventQueue)
   chan <- liftIO $ dupChan eventQueue
   stopVar <- liftIO newEmptyMVar
-  liftIO $ void $ forkFinally (loop chan nworkers) (const $ putMVar stopVar ())
+  liftIO $ void $ forkFinally (listenerLoop handler chan nworkers) (const $ putMVar stopVar ())
   pure stopVar
-  where
-  loop chan !workersAlive =
-    when (workersAlive > 0) $ do
-      event <- readChan chan
-      handler event
-      case event of
-        (_, WorkerEvent _ (WorkerStopped _)) -> loop chan (workersAlive - 1)
-        _                                    -> loop chan workersAlive
+
+-- | Repeatedly run 'handler' on events from 'chan'.
+-- Stops once 'workersAlive' workers stop.
+listenerLoop
+  :: (MonadIO m)
+  => ((LocalTime, CampaignEvent) -> m ())
+  -- ^ a function that handles the events
+  -> Chan (LocalTime, CampaignEvent)
+  -- ^ event channel
+  -> Int
+  -- ^ number of workers which have to stop before loop exits
+  -> m ()
+listenerLoop handler chan !workersAlive =
+  when (workersAlive > 0) $ do
+    event <- liftIO $ readChan chan
+    handler event
+    case event of
+      (_, WorkerEvent _ _ (WorkerStopped _)) -> listenerLoop handler chan (workersAlive - 1)
+      _                                      -> listenerLoop handler chan workersAlive
diff --git a/lib/Echidna/Config.hs b/lib/Echidna/Config.hs
index ce76b1c99..86b2441b9 100644
--- a/lib/Echidna/Config.hs
+++ b/lib/Echidna/Config.hs
@@ -97,6 +97,12 @@ instance FromJSON EConfigWithUsage where
         <*> v ..:? "coverageFormats" ..!= [Txt,Html,Lcov]
         <*> v ..:? "workers"
         <*> v ..:? "server"
+        <*> v ..:? "symExec"            ..!= False
+        <*> v ..:? "symExecConcolic"    ..!= True
+        <*> v ..:? "symExecTimeout"     ..!= defaultSymExecTimeout
+        <*> v ..:? "symExecNSolvers"    ..!= defaultSymExecNWorkers
+        <*> v ..:? "symExecMaxIters"    ..!= defaultSymExecMaxIters
+        <*> v ..:? "symExecAskSMTIters" ..!= defaultSymExecAskSMTIters
 
       solConfParser = SolConf
         <$> v ..:? "contractAddr"    ..!= defaultContractAddr
diff --git a/lib/Echidna/Output/Corpus.hs b/lib/Echidna/Output/Corpus.hs
index b13c022c8..258041197 100644
--- a/lib/Echidna/Output/Corpus.hs
+++ b/lib/Echidna/Output/Corpus.hs
@@ -42,7 +42,7 @@ saveCorpusEvent env (_time, campaignEvent) = do
     Just corpusDir -> saveEvent corpusDir campaignEvent
     Nothing -> pure ()
   where
-    saveEvent dir (WorkerEvent _workerId event) =
+    saveEvent dir (WorkerEvent _workerId _workerType event) =
       maybe (pure ()) (saveFile dir) $ getEventInfo event
     saveEvent _ _ = pure ()
 
diff --git a/lib/Echidna/Server.hs b/lib/Echidna/Server.hs
index 12ef22b8c..73d4592f6 100644
--- a/lib/Echidna/Server.hs
+++ b/lib/Echidna/Server.hs
@@ -16,11 +16,16 @@ import Echidna.Types.Config (Env(..))
 newtype SSE = SSE (LocalTime, CampaignEvent)
 
 instance ToJSON SSE where
-  toJSON (SSE (time, WorkerEvent workerId event)) =
+  toJSON (SSE (time, WorkerEvent workerId workerType event)) =
     object [ "worker" .= workerId
+           , "workerType" .= workerTypeString workerType
            , "timestamp" .= time
            , "data" .= event
            ]
+    where
+      workerTypeString :: WorkerType -> String
+      workerTypeString SymbolicWorker = "symbolic"
+      workerTypeString FuzzWorker = "fuzz"
   toJSON (SSE (time, Failure reason)) =
     object [ "timestamp" .= time
            , "data" .= reason
@@ -38,17 +43,18 @@ runSSEServer serverStopVar env port nworkers = do
         else do
           event@(_, campaignEvent) <- readChan sseChan
           let eventName = \case
-                WorkerEvent _ workerEvent ->
+                WorkerEvent _ _ workerEvent ->
                   case workerEvent of
                     TestFalsified _ -> "test_falsified"
                     TestOptimized _ -> "test_optimized"
                     NewCoverage {} -> "new_coverage"
+                    SymNoNewCoverage -> "sym_no_new_coverage"
                     TxSequenceReplayed {} -> "tx_sequence_replayed"
                     TxSequenceReplayFailed {} -> "tx_sequence_replay_failed"
                     WorkerStopped _ -> "worker_stopped"
                 Failure _err -> "failure"
           case campaignEvent of
-            WorkerEvent _ (WorkerStopped _) -> do
+            WorkerEvent _ _ (WorkerStopped _) -> do
               aliveAfter <- atomicModifyIORef' aliveRef (\n -> (n-1, n-1))
               when (aliveAfter == 0) $ putMVar serverStopVar ()
             _ -> pure ()
diff --git a/lib/Echidna/Solidity.hs b/lib/Echidna/Solidity.hs
index e124016ce..2e92c2d54 100644
--- a/lib/Echidna/Solidity.hs
+++ b/lib/Echidna/Solidity.hs
@@ -174,7 +174,7 @@ loadSpecified env name cs = do
   let solConf = env.cfg.solConf
 
   -- Pick contract to load
-  mainContract <- choose cs name
+  mainContract <- chooseContract cs name
   when (isNothing name && length cs > 1 && not solConf.quiet) $
     putStrLn "Multiple contracts found, only analyzing the first"
   unless solConf.quiet $
@@ -220,7 +220,7 @@ loadSpecified env name cs = do
     throwM $ ConstructorArgs (show mainContract.constructorInputs)
 
   -- Select libraries
-  ls <- mapM (choose cs . Just . T.pack) solConf.solcLibs
+  ls <- mapM (chooseContract cs . Just . T.pack) solConf.solcLibs
 
   -- Make sure everything is ready to use, then ship it
   when (null abi) $
@@ -241,7 +241,7 @@ loadSpecified env name cs = do
     vm0 <- deployContracts (zip [addrLibrary ..] ls) solConf.deployer blank
 
     -- additional contract deployment (by name)
-    cs' <- mapM ((choose cs . Just) . T.pack . snd) solConf.deployContracts
+    cs' <- mapM ((chooseContract cs . Just) . T.pack . snd) solConf.deployContracts
     vm1 <- deployContracts (zip (map fst solConf.deployContracts) cs') solConf.deployer vm0
 
     -- additional contract deployment (bytecode)
@@ -275,22 +275,28 @@ loadSpecified env name cs = do
       _ -> pure (vm4, neFuns, fst <$> tests, abiMapping)
 
   where
-    choose [] _ = throwM NoContracts
-    choose (c:_) Nothing = pure c
-    choose _ (Just n) =
-      maybe (throwM $ ContractNotFound n) pure $
-        find (isMatch n) cs
-    isMatch n s =
-      (Data.Text.isSuffixOf (contractId rewriteOsPathSeparators n) . (.contractName)) s ||
-      (Data.Text.isSuffixOf (contractId rewritePosixPathSeparators n) . (.contractName)) s
-    contractId rewrite n
+    setUpFunction = ("setUp", [])
+
+-- | Given a list of contracts and a requested contract name, pick a contract.
+-- See 'loadSpecified' for more information.
+chooseContract :: (MonadThrow m) => [SolcContract] -> Maybe Text -> m SolcContract
+chooseContract [] _ = throwM NoContracts
+chooseContract (c:_) Nothing = pure c
+chooseContract cs (Just n) =
+  maybe (throwM $ ContractNotFound n) pure $
+    find isMatch cs
+  where
+    isMatch s =
+      (Data.Text.isSuffixOf (contractId rewriteOsPathSeparators) . (.contractName)) s ||
+      (Data.Text.isSuffixOf (contractId rewritePosixPathSeparators) . (.contractName)) s
+    contractId rewrite
       | T.any (== ':') n =
         let (splitPath, splitName) = T.breakOn ":" n
         in rewrite splitPath `T.append` splitName
       | otherwise = ":" `append` n
+
     rewriteOsPathSeparators = T.pack . joinPath . splitDirectories . T.unpack
     rewritePosixPathSeparators = T.pack . FPP.joinPath . FPP.splitDirectories . T.unpack
-    setUpFunction = ("setUp", [])
 
 -- | Given the results of 'loadSolidity', assuming a single-contract test, get everything ready
 -- for running a 'Campaign' against the tests found.
diff --git a/lib/Echidna/SymExec.hs b/lib/Echidna/SymExec.hs
new file mode 100644
index 000000000..752dfcdfa
--- /dev/null
+++ b/lib/Echidna/SymExec.hs
@@ -0,0 +1,245 @@
+{-# OPTIONS_GHC -Wno-gadt-mono-local-binds #-}
+
+module Echidna.SymExec (createSymTx) where
+
+import Control.Applicative ((<|>))
+import Control.Concurrent.Async (mapConcurrently)
+import Control.Concurrent (ThreadId, forkIO)
+import Control.Concurrent.MVar (MVar, newEmptyMVar, putMVar, takeMVar)
+import Control.Monad (forM)
+import Control.Monad.IO.Class (liftIO)
+import Control.Monad.Reader (runReaderT)
+import Data.ByteString.Lazy qualified as BS
+import Data.Foldable (fold)
+import Data.Function ((&))
+import Data.List (singleton)
+import Data.Map qualified as Map
+import Data.Maybe (fromMaybe, mapMaybe, isJust, fromJust)
+import Data.Set (Set)
+import Data.Set qualified as Set
+import Data.Text (Text)
+import Data.Text qualified as T
+import Data.Vector (toList, fromList)
+import Optics.Core ((.~), (%))
+import Echidna.Solidity (chooseContract)
+import Echidna.Types (fromEVM)
+import Echidna.Types.Campaign (CampaignConf(..))
+import Echidna.Types.Config (EConfig(..))
+import Echidna.Types.Solidity (SolConf(..))
+import EVM.ABI (AbiValue(..), AbiType(..), Sig(..), decodeAbiValue)
+import EVM.Expr (simplify)
+import EVM.Fetch qualified as Fetch
+import EVM.SMT (SMTCex(..), SMT2, assertProps)
+import EVM (loadContract, resetState)
+import EVM.Effects (defaultEnv, defaultConfig)
+import EVM.Solidity (SolcContract(..), Method(..))
+import EVM.Solvers (withSolvers, Solver(Z3), CheckSatResult(Sat), SolverGroup, checkSat)
+import EVM.SymExec (interpret, runExpr, abstractVM, mkCalldata, LoopHeuristic (Naive), flattenExpr, extractProps)
+import EVM.Types (Addr, VM(..), Frame(..), FrameState(..), VMType(..), Env(..), Expr(..), EType(..), Query(..), Prop(..), BranchCondition(..), W256, word256Bytes, word)
+import EVM.Traversals (mapExpr)
+import Control.Monad.ST (stToIO, RealWorld)
+import Control.Monad.State.Strict (execState, runStateT)
+import Echidna.Types.Tx (Tx(..), TxCall(..), maxGasPerBlock)
+
+
+-- | Uses symbolic execution to find transactions which would increase coverage.
+-- Spawns a new thread; returns its thread ID as the first return value.
+-- The second return value is an MVar which is populated with transactions
+--   once the symbolic execution is finished.
+-- Also takes an optional Tx argument; this is used as the transaction
+--   to follow during concolic execution. If none is provided, we do full
+--   symbolic execution.
+--   The Tx argument, if present, must have a .call value of type SolCall.
+createSymTx :: EConfig -> Maybe Text -> [SolcContract] -> Maybe Tx -> VM Concrete RealWorld -> IO (ThreadId, MVar [Tx])
+createSymTx cfg name cs tx vm = do
+  mainContract <- chooseContract cs name
+  exploreContract cfg mainContract tx vm
+
+exploreContract :: EConfig -> SolcContract -> Maybe Tx -> VM Concrete RealWorld -> IO (ThreadId, MVar [Tx])
+exploreContract conf contract tx vm = do
+  let
+    isConc = isJust tx
+    allMethods = Map.elems contract.abiMap
+    concMethods (Tx { call = SolCall (methodName, _) }) = filter (\method -> method.name == methodName) allMethods
+    concMethods _ = error "`exploreContract` should only be called with Nothing or Just Tx{call=SolCall _} for its tx argument"
+    methods = maybe allMethods concMethods tx
+    timeout = Just (fromIntegral conf.campaignConf.symExecTimeout)
+    maxIters = if isConc then Nothing else Just conf.campaignConf.symExecMaxIters
+    askSmtIters = if isConc then 0 else conf.campaignConf.symExecAskSMTIters
+    rpcInfo = Nothing
+    defaultSender = fromJust $ fmap (.dst) tx <|> Set.lookupMin conf.solConf.sender <|> Just 0
+
+  threadIdChan <- newEmptyMVar
+  doneChan <- newEmptyMVar
+  resultChan <- newEmptyMVar
+
+  flip runReaderT defaultEnv $ withSolvers Z3 (fromIntegral conf.campaignConf.symExecNSolvers) timeout $ \solvers -> do
+    threadId <- liftIO $ forkIO $ flip runReaderT defaultEnv $ do
+      res <- forM methods $ \method -> do
+        let
+          fetcher = concOrSymFetcher tx solvers rpcInfo
+          dst = conf.solConf.contractAddr
+          calldata@(cd, constraints) = mkCalldata (Just (Sig method.methodSignature (snd <$> method.inputs))) []
+          vmSym = abstractVM calldata contract.runtimeCode Nothing False
+        vmSym' <- liftIO $ stToIO vmSym
+        vmReset <- liftIO $ snd <$> runStateT (fromEVM resetState) vm
+        let vm' = vmReset & execState (loadContract (LitAddr dst))
+                          & vmMakeSymbolic
+                          & #constraints .~ constraints
+                          & #state % #callvalue .~ TxValue
+                          & #state % #caller .~ SymAddr "caller"
+                          & #state % #calldata .~ cd
+                          & #env % #contracts .~ (Map.union vmSym'.env.contracts vm.env.contracts)
+        -- TODO we might want to switch vm's state.baseState value to to AbstractBase eventually.
+        -- Doing so might mess up concolic execution.
+        exprInter <- interpret fetcher maxIters askSmtIters Naive vm' runExpr
+        models <- liftIO $ mapConcurrently (checkSat solvers) $ manipulateExprInter isConc exprInter
+        pure $ mapMaybe (modelToTx dst method conf.solConf.sender defaultSender) models
+      liftIO $ putMVar resultChan $ concat res
+      liftIO $ putMVar doneChan ()
+    liftIO $ putMVar threadIdChan threadId
+    liftIO $ takeMVar doneChan
+
+  threadId <- takeMVar threadIdChan
+  pure (threadId, resultChan)
+
+-- | Turn the expression returned by `interpret` into into SMT2 values to feed into the solver
+manipulateExprInter :: Bool -> Expr End -> [SMT2]
+manipulateExprInter isConc = map (assertProps defaultConfig) . middleStep . map (extractProps . simplify) . flattenExpr . simplify where
+  middleStep = if isConc then middleStepConc else id
+  middleStepConc = map singleton . concatMap (go (PBool True))
+  go :: Prop -> [Prop] -> [Prop]
+  go _ [] = []
+  go acc (h:t) = (PNeg h `PAnd` acc) : go (h `PAnd` acc) t
+
+-- | Sets result to Nothing, and sets gas to ()
+vmMakeSymbolic :: VM Concrete s -> VM Symbolic s
+vmMakeSymbolic vm
+  = VM
+  { result         = Nothing
+  , state          = frameStateMakeSymbolic vm.state
+  , frames         = map frameMakeSymbolic vm.frames
+  , env            = vm.env
+  , block          = vm.block
+  , tx             = vm.tx
+  , logs           = vm.logs
+  , traces         = vm.traces
+  , cache          = vm.cache
+  , burned         = ()
+  , iterations     = vm.iterations
+  , constraints    = vm.constraints
+  , config         = vm.config
+  , forks          = vm.forks
+  , currentFork    = vm.currentFork
+  }
+
+frameStateMakeSymbolic :: FrameState Concrete s -> FrameState Symbolic s
+frameStateMakeSymbolic fs
+  = FrameState
+  { contract     = fs.contract
+  , codeContract = fs.codeContract
+  , code         = fs.code
+  , pc           = fs.pc
+  , stack        = fs.stack
+  , memory       = fs.memory
+  , memorySize   = fs.memorySize
+  , calldata     = fs.calldata
+  , callvalue    = fs.callvalue
+  , caller       = fs.caller
+  , gas          = ()
+  , returndata   = fs.returndata
+  , static       = fs.static
+  }
+
+frameMakeSymbolic :: Frame Concrete s -> Frame Symbolic s
+frameMakeSymbolic fr = Frame { context = fr.context, state = frameStateMakeSymbolic fr.state }
+
+modelToTx :: Addr -> Method -> Set Addr -> Addr -> CheckSatResult -> Maybe Tx
+modelToTx dst method senders fallbackSender result =
+  case result of
+    Sat cex ->
+      let
+        args = zipWith grabArg (snd <$> method.inputs) ["arg" <> T.pack (show n) | n <- [1..] :: [Int]]
+
+        grabArg t
+          = case t of
+              AbiUIntType _ -> grabNormalArg t
+              AbiIntType _ -> grabNormalArg t
+              AbiBoolType -> grabNormalArg t
+              AbiBytesType _ -> grabNormalArg t
+              AbiAddressType -> grabAddressArg
+              AbiArrayType n mt -> grabArrayArg n mt
+              _ -> error "Unexpected ABI type in `modelToTx`"
+
+        grabNormalArg argType name
+          = case Map.lookup (Var name) cex.vars of
+              Just w ->
+                decodeAbiValue argType (BS.fromStrict (word256Bytes w))
+              Nothing -> -- put a placeholder
+                decodeAbiValue argType (BS.repeat 0)
+
+        grabAddressArg name = AbiAddress $ fromMaybe 0 $ Map.lookup (SymAddr name) cex.addrs
+
+        grabArrayArg nElem memberType name = AbiArray nElem memberType $ fromList [grabArg memberType $ name <> T.pack (show n) | n <- [0..nElem] :: [Int]]
+
+        src_ = fromMaybe 0 $ Map.lookup (SymAddr "sender") cex.addrs
+        src = if Set.member src_ senders then src_ else fallbackSender
+
+        value = fromMaybe 0 $ Map.lookup TxValue cex.txContext
+
+      in Just Tx
+        { call = SolCall (method.name, args)
+        , src = src
+        , dst = dst
+        , gasprice = 0
+        , gas = maxGasPerBlock
+        , value = value
+        , delay = (0, 0)
+        }
+
+    _ -> Nothing
+
+-- | Symbolic variable -> concrete value mapping used during concolic execution.
+-- The third member in the tuple is the transaction value.
+type Substs = ([(Text, W256)], [(Text, Addr)], W256)
+
+-- | Mirrors hevm's `symAbiArg` function; whenever that changes, we need to change this too
+genSubsts :: Tx -> Substs
+genSubsts (Tx { call = SolCall (_, abiVals), src, value }) = addOnFinalValues $ fold $ zipWith genVal abiVals (T.pack . ("arg" <>) . show <$> ([1..] :: [Int])) where
+  addOnFinalValues (a, b) = (a, ("sender", src):b, value)
+  genVal (AbiUInt _ i) name = ([(name, fromIntegral i)], [])
+  genVal (AbiInt _ i) name = ([(name, fromIntegral i)], [])
+  genVal (AbiBool b) name = ([(name, if b then 1 else 0)], [])
+  genVal (AbiAddress addr) name = ([], [(name, addr)])
+  genVal (AbiBytes n b) name | n > 0 && n <= 32 = ([(name, word b)], [])
+  genVal (AbiArray _ _ vals) name = fold $ zipWith genVal (toList vals) [name <> T.pack (show n) | n <- [0..] :: [Int]]
+  genVal _ _ = error "`genSubsts` is not implemented for all API types, mirroring hevm's `symAbiArg` function"
+genSubsts _ = error "`genSubsts` should only be called with a `SolCall` transaction argument"
+
+-- | Apply substitutions into an expression
+substExpr :: Substs -> Expr a -> Expr a
+substExpr (sw, sa, val) = mapExpr go where
+  go v@(Var t) = maybe v Lit (lookup t sw)
+  go v@(SymAddr t) = maybe v LitAddr (lookup t sa)
+  go TxValue = Lit val
+  go e = e
+
+-- | Fetcher used during concolic exeuction.
+-- This is the most important function for concolic execution;
+-- it determines what branch `interpret` should take.
+-- We ensure that this fetcher is always used by setting askSMTIter to 0.
+-- We determine what branch to take by substituting concrete values into
+-- the provided `Prop`, and then simplifying.
+-- We fall back on `Fetch.oracle`.
+concFetcher :: Substs -> SolverGroup -> Fetch.RpcInfo -> Fetch.Fetcher t m s
+concFetcher substs s r (PleaseAskSMT branchcondition pathconditions continue) =
+  case simplify (substExpr substs branchcondition) of
+    Lit n -> pure (continue (Case (n/=0)))
+    simplifiedExpr -> Fetch.oracle s r (PleaseAskSMT simplifiedExpr pathconditions continue)
+concFetcher _ s r q = Fetch.oracle s r q
+
+-- | Depending on whether we're doing concolic or full symbolic execution,
+-- choose a fetcher to be used in `interpret` (either `concFetcher` or `Fetch.oracle`).
+concOrSymFetcher :: Maybe Tx -> SolverGroup -> Fetch.RpcInfo -> Fetch.Fetcher t m s
+concOrSymFetcher (Just c) = concFetcher $ genSubsts c
+concOrSymFetcher Nothing = Fetch.oracle
diff --git a/lib/Echidna/Types/Campaign.hs b/lib/Echidna/Types/Campaign.hs
index 240eeae32..c0b1e3351 100644
--- a/lib/Echidna/Types/Campaign.hs
+++ b/lib/Echidna/Types/Campaign.hs
@@ -1,7 +1,9 @@
 module Echidna.Types.Campaign where
 
+import Control.Concurrent (ThreadId)
 import Data.Aeson
 import Data.Map (Map)
+import Data.Maybe (fromMaybe)
 import Data.Text (Text)
 import Data.Text qualified as T
 import Data.Word (Word8, Word16)
@@ -14,46 +16,67 @@ import Echidna.Types.Tx (Tx)
 
 -- | Configuration for running an Echidna 'Campaign'.
 data CampaignConf = CampaignConf
-  { testLimit       :: Int
+  { testLimit          :: Int
     -- ^ Maximum number of function calls to execute while fuzzing
-  , stopOnFail      :: Bool
+  , stopOnFail         :: Bool
     -- ^ Whether to stop the campaign immediately if any property fails
-  , estimateGas     :: Bool
+  , estimateGas        :: Bool
     -- ^ Whether to collect gas usage statistics
-  , seqLen          :: Int
+  , seqLen             :: Int
     -- ^ Number of calls between state resets (e.g. \"every 10 calls,
     -- reset the state to avoid unrecoverable states/save memory\"
-  , shrinkLimit     :: Int
+  , shrinkLimit        :: Int
     -- ^ Maximum number of candidate sequences to evaluate while shrinking
-  , knownCoverage   :: Maybe CoverageMap
+  , knownCoverage      :: Maybe CoverageMap
     -- ^ If applicable, initially known coverage. If this is 'Nothing',
     -- Echidna won't collect coverage information (and will go faster)
-  , seed            :: Maybe Int
+  , seed               :: Maybe Int
     -- ^ Seed used for the generation of random transactions
-  , dictFreq        :: Float
+  , dictFreq           :: Float
     -- ^ Frequency for the use of dictionary values in the random transactions
-  , corpusDir       :: Maybe FilePath
+  , corpusDir          :: Maybe FilePath
     -- ^ Directory to load and save lists of transactions
-  , mutConsts       :: MutationConsts Integer
+  , mutConsts          :: MutationConsts Integer
     -- ^ Directory to load and save lists of transactions
-  , coverageFormats :: [CoverageFileType]
+  , coverageFormats    :: [CoverageFileType]
     -- ^ List of file formats to save coverage reports
-  , workers         :: Maybe Word8
+  , workers            :: Maybe Word8
     -- ^ Number of fuzzing workers
-  , serverPort      :: Maybe Word16
+  , serverPort         :: Maybe Word16
     -- ^ Server-Sent Events HTTP port number, if missing server is not ran
+  , symExec            :: Bool
+    -- ^ Whether to add an additional symbolic execution worker
+  , symExecConcolic    :: Bool
+    -- ^ Whether symbolic execution will be concolic (vs full symbolic execution)
+    -- Only relevant if symExec is True
+  , symExecTimeout     :: Int
+    -- ^ Timeout for symbolic execution SMT solver.
+    -- Only relevant if symExec is True
+  , symExecNSolvers    :: Int
+    -- ^ Number of SMT solvers used in symbolic execution.
+    -- Only relevant if symExec is True
+  , symExecMaxIters    :: Integer
+    -- ^ Number of times we may revisit a particular branching point.
+    -- Only relevant if symExec is True and symExecConcolic is False
+  , symExecAskSMTIters :: Integer
+    -- ^ Number of times we may revisit a particular branching point
+    -- before we consult the SMT solver to check reachability.
+    -- Only relevant if symExec is True and symExecConcolic is False
   }
 
+data WorkerType = FuzzWorker | SymbolicWorker deriving (Eq)
+
 type WorkerId = Int
 
 data CampaignEvent
-  = WorkerEvent WorkerId WorkerEvent
+  = WorkerEvent WorkerId WorkerType WorkerEvent
   | Failure String
 
 data WorkerEvent
   = TestFalsified !EchidnaTest
   | TestOptimized !EchidnaTest
   | NewCoverage { points :: !Int, numCodehashes :: !Int, corpusSize :: !Int, transactions :: [Tx] }
+  | SymNoNewCoverage
   | TxSequenceReplayed FilePath !Int !Int
   | TxSequenceReplayFailed FilePath Tx
   | WorkerStopped WorkerStopReason
@@ -67,6 +90,7 @@ instance ToJSON WorkerEvent where
     TestOptimized test -> toJSON test
     NewCoverage { points, numCodehashes, corpusSize } ->
       object [ "coverage" .= points, "contracts" .= numCodehashes, "corpus_size" .= corpusSize]
+    SymNoNewCoverage -> object []
     TxSequenceReplayed file current total ->
       object [ "file" .= file, "current" .= current, "total" .= total ]
     TxSequenceReplayFailed file tx ->
@@ -75,6 +99,7 @@ instance ToJSON WorkerEvent where
 
 data WorkerStopReason
   = TestLimitReached
+  | SymbolicDone
   | TimeLimitReached
   | FastFailed
   | Killed !String
@@ -83,7 +108,7 @@ data WorkerStopReason
 
 ppCampaignEvent :: CampaignEvent -> String
 ppCampaignEvent = \case
-  WorkerEvent _ e -> ppWorkerEvent e
+  WorkerEvent _ _ e -> ppWorkerEvent e
   Failure err -> err
 
 ppWorkerEvent :: WorkerEvent -> String
@@ -97,6 +122,8 @@ ppWorkerEvent = \case
     "New coverage: " <> show points <> " instr, "
       <> show numCodehashes <> " contracts, "
       <> show corpusSize <> " seqs in corpus"
+  SymNoNewCoverage ->
+    "Symbolic execution finished with no new coverage."
   TxSequenceReplayed file current total ->
     "Sequence replayed from corpus file " <> file <> " (" <> show current <> "/" <> show total <> ")"
   TxSequenceReplayFailed file tx ->
@@ -105,6 +132,8 @@ ppWorkerEvent = \case
     "Remove the file or the transaction to fix the issue."
   WorkerStopped TestLimitReached ->
     "Test limit reached. Stopping."
+  WorkerStopped SymbolicDone ->
+    "Symbolic worker ran out of transactions to work on. Stopping."
   WorkerStopped TimeLimitReached ->
     "Time limit reached. Stopping."
   WorkerStopped FastFailed ->
@@ -136,6 +165,9 @@ data WorkerState = WorkerState
     -- ^ Number of times the callseq is called
   , ncalls      :: !Int
     -- ^ Number of calls executed while fuzzing
+  , runningThreads :: [ThreadId]
+    -- ^ Extra threads currently being run,
+    --   aside from the main worker thread
   }
 
 initialWorkerState :: WorkerState
@@ -146,6 +178,7 @@ initialWorkerState =
               , newCoverage = False
               , ncallseqs = 0
               , ncalls = 0
+              , runningThreads = []
               }
 
 defaultTestLimit :: Int
@@ -156,3 +189,29 @@ defaultSequenceLength = 100
 
 defaultShrinkLimit :: Int
 defaultShrinkLimit = 5000
+
+defaultSymExecTimeout :: Int
+defaultSymExecTimeout = 30
+
+defaultSymExecNWorkers :: Int
+defaultSymExecNWorkers = 1
+
+defaultSymExecMaxIters :: Integer
+defaultSymExecMaxIters = 10
+
+-- | Same default as in hevm, "everything else is unsound"
+-- (https://github.com/ethereum/hevm/pull/252)
+defaultSymExecAskSMTIters :: Integer
+defaultSymExecAskSMTIters = 1
+
+-- | Get number of fuzzing workers (doesn't include sym exec worker)
+-- Defaults to 1 if set to Nothing
+getNFuzzWorkers :: CampaignConf -> Int
+getNFuzzWorkers conf = fromIntegral (fromMaybe 1 (conf.workers))
+
+-- | Number of workers, including SymExec worker if there is one
+getNWorkers :: CampaignConf -> Int
+getNWorkers conf = getNFuzzWorkers conf + (if conf.symExec then 1 else 0)
+
+workerIDToType :: CampaignConf -> WorkerId -> WorkerType
+workerIDToType conf wid = if conf.symExec && wid == (getNWorkers conf - 1) then SymbolicWorker else FuzzWorker
diff --git a/lib/Echidna/UI.hs b/lib/Echidna/UI.hs
index 257aaee9e..7ed7af724 100644
--- a/lib/Echidna/UI.hs
+++ b/lib/Echidna/UI.hs
@@ -25,11 +25,13 @@ import Data.ByteString.Lazy qualified as BS
 import Data.List.Split (chunksOf)
 import Data.Map (Map)
 import Data.Maybe (fromMaybe, isJust)
+import Data.Text (Text)
 import Data.Time
 import UnliftIO
-  ( MonadUnliftIO, newIORef, readIORef, hFlush, stdout , writeIORef, timeout)
+  ( MonadUnliftIO, IORef, newIORef, readIORef, hFlush, stdout , writeIORef, timeout)
 import UnliftIO.Concurrent hiding (killThread, threadDelay)
 
+import EVM.Solidity (SolcContract)
 import EVM.Types (Addr, Contract, VM, VMType(Concrete), W256)
 
 import Echidna.ABI
@@ -41,6 +43,7 @@ import Echidna.Types.Campaign
 import Echidna.Types.Config
 import Echidna.Types.Corpus qualified as Corpus
 import Echidna.Types.Coverage (scoveragePoints)
+import Echidna.Types.Solidity (SolConf(..))
 import Echidna.Types.Test (EchidnaTest(..), didFail, isOptimizationTest)
 import Echidna.Types.Tx (Tx)
 import Echidna.Types.World (World)
@@ -61,15 +64,17 @@ ui
   -> World   -- ^ Initial world state
   -> GenDict
   -> [(FilePath, [Tx])]
+  -> Maybe Text
+  -> [SolcContract]
   -> m [WorkerState]
-ui vm world dict initialCorpus = do
+ui vm world dict initialCorpus cliSelectedContract cs = do
   env <- ask
   conf <- asks (.cfg)
   terminalPresent <- liftIO isTerminal
 
   let
-    -- default to one worker if not configured
-    nworkers = fromIntegral $ fromMaybe 1 conf.campaignConf.workers
+    nFuzzWorkers = getNFuzzWorkers conf.campaignConf
+    nworkers = getNWorkers conf.campaignConf
 
     effectiveMode = case conf.uiConf.operationMode of
       Interactive | not terminalPresent -> NonInteractive Text
@@ -78,10 +83,10 @@ ui vm world dict initialCorpus = do
     -- Distribute over all workers, could be slightly bigger overall due to
     -- ceiling but this doesn't matter
     perWorkerTestLimit = ceiling
-      (fromIntegral conf.campaignConf.testLimit / fromIntegral nworkers :: Double)
+      (fromIntegral conf.campaignConf.testLimit / fromIntegral nFuzzWorkers :: Double)
 
     chunkSize = ceiling
-      (fromIntegral (length initialCorpus) / fromIntegral nworkers :: Double)
+      (fromIntegral (length initialCorpus) / fromIntegral nFuzzWorkers :: Double)
     corpusChunks = chunksOf chunkSize initialCorpus ++ repeat []
 
   corpusSaverStopVar <- spawnListener (saveCorpusEvent env)
@@ -217,11 +222,14 @@ ui vm world dict initialCorpus = do
 
     threadId <- forkIO $ do
       -- TODO: maybe figure this out with forkFinally?
+      let workerType = workerIDToType env.cfg.campaignConf workerId
       stopReason <- catches (do
-          let timeoutUsecs = maybe (-1) (*1_000_000) env.cfg.uiConf.maxTime
+          let
+            timeoutUsecs = maybe (-1) (*1_000_000) env.cfg.uiConf.maxTime
+            corpus = if workerType == SymbolicWorker then initialCorpus else corpusChunk
           maybeResult <- timeout timeoutUsecs $
-            runWorker (get >>= writeIORef stateRef)
-                      vm world dict workerId corpusChunk testLimit
+            runWorker workerType (get >>= writeIORef stateRef)
+                      vm world dict workerId corpus testLimit cliSelectedContract cs
           pure $ case maybeResult of
             Just (stopReason, _finalState) -> stopReason
             Nothing -> TimeLimitReached
@@ -231,7 +239,7 @@ ui vm world dict initialCorpus = do
         ]
 
       time <- liftIO getTimestamp
-      writeChan env.eventQueue (time, WorkerEvent workerId (WorkerStopped stopReason))
+      writeChan env.eventQueue (time, WorkerEvent workerId workerType (WorkerStopped stopReason))
 
     pure (threadId, stateRef)
 
@@ -241,9 +249,11 @@ ui vm world dict initialCorpus = do
 
 #ifdef INTERACTIVE_UI
  -- | Order the workers to stop immediately
-stopWorkers :: MonadIO m => [(ThreadId, a)] -> m ()
+stopWorkers :: MonadIO m => [(ThreadId, IORef WorkerState)] -> m ()
 stopWorkers workers =
-  forM_ workers $ \(threadId, _) -> liftIO $ killThread threadId
+  forM_ workers $ \(threadId, workerStateRef) -> do
+    workerState <- readIORef workerStateRef
+    liftIO $ mapM_ killThread (threadId : workerState.runningThreads)
 
 vtyConfig :: IO Config
 vtyConfig = do
@@ -274,14 +284,14 @@ monitor = do
         modify' $ \state -> state { events = state.events |> event }
 
         case campaignEvent of
-          WorkerEvent _ (NewCoverage { points, numCodehashes, corpusSize }) ->
+          WorkerEvent _ _ (NewCoverage { points, numCodehashes, corpusSize }) ->
             modify' $ \state ->
               state { coverage = max state.coverage points -- max not really needed
                     , corpusSize
                     , numCodehashes
                     , lastNewCov = time
                     }
-          WorkerEvent _ (WorkerStopped _) ->
+          WorkerEvent _ _ (WorkerStopped _) ->
             modify' $ \state ->
               state { workersAlive = state.workersAlive - 1
                     , timeStopped = if state.workersAlive == 1
diff --git a/lib/Echidna/UI/Report.hs b/lib/Echidna/UI/Report.hs
index 5c2dc564e..d35b31da9 100644
--- a/lib/Echidna/UI/Report.hs
+++ b/lib/Echidna/UI/Report.hs
@@ -30,8 +30,10 @@ import EVM.Solidity (SolcContract(..))
 import EVM.Types (W256, VM, VMType(Concrete), Addr, Expr (LitAddr))
 
 ppLogLine :: (LocalTime, CampaignEvent) -> String
-ppLogLine (time, event@(WorkerEvent workerId _)) =
+ppLogLine (time, event@(WorkerEvent workerId FuzzWorker _)) =
   timePrefix time <> "[Worker " <> show workerId <> "] " <> ppCampaignEvent event
+ppLogLine (time, event@(WorkerEvent workerId SymbolicWorker _)) =
+  timePrefix time <> "[Worker " <> show workerId <> ", symbolic] " <> ppCampaignEvent event
 ppLogLine (time, event) =
   timePrefix time <> " " <> ppCampaignEvent event
 
diff --git a/lib/Echidna/UI/Widgets.hs b/lib/Echidna/UI/Widgets.hs
index d648b01c9..906b1a3a6 100644
--- a/lib/Echidna/UI/Widgets.hs
+++ b/lib/Echidna/UI/Widgets.hs
@@ -146,9 +146,13 @@ logPane uiState =
   foldl (<=>) emptyWidget (showLogLine <$> Seq.reverse uiState.events)
 
 showLogLine :: (LocalTime, CampaignEvent) -> Widget Name
-showLogLine (time, event@(WorkerEvent workerId _)) =
-  (withAttr (attrName "time") $ str $ (timePrefix time) <> "[Worker " <> show workerId <> "] ")
+showLogLine (time, event@(WorkerEvent workerId workerType _)) =
+  (withAttr (attrName "time") $ str $ (timePrefix time) <> "[Worker " <> show workerId <> symSuffix <> "] ")
     <+> strBreak (ppCampaignEvent event)
+  where
+  symSuffix = case workerType of
+    SymbolicWorker -> ", symbolic"
+    _ -> ""
 showLogLine (time, event) =
   (withAttr (attrName "time") $ str $ (timePrefix time) <> " ") <+> strBreak (ppCampaignEvent event)
 
diff --git a/package.yaml b/package.yaml
index 657cef0d3..650cdce7b 100644
--- a/package.yaml
+++ b/package.yaml
@@ -17,6 +17,7 @@ ghc-options:
 dependencies:
   - base
   - aeson
+  - async
   - base16-bytestring
   - binary
   - bytestring
diff --git a/src/Main.hs b/src/Main.hs
index 5f5d12935..07a5ce7df 100644
--- a/src/Main.hs
+++ b/src/Main.hs
@@ -6,6 +6,7 @@ import Control.Monad (unless, forM_, when)
 import Control.Monad.Reader (runReaderT, liftIO)
 import Control.Monad.Random (getRandomR)
 import Data.Aeson.Key qualified as Aeson.Key
+import Data.Char (toLower)
 import Data.Function ((&))
 import Data.Hashable (hash)
 import Data.IORef (readIORef)
@@ -28,7 +29,7 @@ import System.IO (hPutStrLn, stderr)
 import System.IO.CodePage (withCP65001)
 
 import EVM.Dapp (DappInfo(..))
-import EVM.Solidity (BuildOutput(..))
+import EVM.Solidity (BuildOutput(..), Contracts(..))
 import EVM.Types (Addr)
 
 import Echidna
@@ -67,8 +68,9 @@ main = withUtf8 $ withCP65001 $ do
   (vm, world, dict) <- prepareContract env cliFilePath cliSelectedContract seed
 
   initialCorpus <- loadInitialCorpus env world
+  let (Contracts contractMap) = buildOutput.contracts
   -- start ui and run tests
-  _campaign <- runReaderT (ui vm world dict initialCorpus) env
+  _campaign <- runReaderT (ui vm world dict initialCorpus cliSelectedContract (Map.elems contractMap)) env
 
   tests <- readIORef env.testsRef
 
@@ -137,6 +139,9 @@ data Options = Options
   , cliSeed             :: Maybe Int
   , cliCryticArgs       :: Maybe String
   , cliSolcArgs         :: Maybe String
+  , cliSymExec          :: Maybe Bool
+  , cliSymExecTimeout   :: Maybe Int
+  , cliSymExecNSolvers  :: Maybe Int
   }
 
 optsParser :: ParserInfo Options
@@ -144,6 +149,12 @@ optsParser = info (helper <*> versionOption <*> options) $ fullDesc
   <> progDesc "EVM property-based testing framework"
   <> header "Echidna"
 
+bool :: ReadM Bool
+bool = maybeReader (f . map toLower) where
+  f "true" = Just True
+  f "false" = Just False
+  f _ = Nothing
+
 options :: Parser Options
 options = Options
   <$> (NE.fromList <$> some (argument str (metavar "FILES"
@@ -206,6 +217,15 @@ options = Options
   <*> optional (option str $ long "solc-args"
     <> metavar "ARGS"
     <> help "Additional arguments to use in solc for the compilation of the contract to test.")
+  <*> optional (option bool $ long "sym-exec"
+    <> metavar "BOOL"
+    <> help "Whether to enable the experimental symbolic execution feature.")
+  <*> optional (option auto $ long "sym-exec-timeout"
+    <> metavar "INTEGER"
+    <> help ("Timeout for each symbolic execution run, in seconds (assuming sym-exec is enabled). Default is " ++ show defaultSymExecTimeout))
+  <*> optional (option auto $ long "sym-exec-n-solvers"
+    <> metavar "INTEGER"
+    <> help ("Number of symbolic execution solvers to run in parallel for each task (assuming sym-exec is enabled). Default is " ++ show defaultSymExecNWorkers))
 
 versionOption :: Parser (a -> a)
 versionOption = infoOption
@@ -245,6 +265,9 @@ overrideConfig config Options{..} = do
       , seed = cliSeed <|> campaignConf.seed
       , workers = cliWorkers <|> campaignConf.workers
       , serverPort = cliServerPort <|> campaignConf.serverPort
+      , symExec = fromMaybe campaignConf.symExec cliSymExec
+      , symExecTimeout = fromMaybe campaignConf.symExecTimeout cliSymExecTimeout
+      , symExecNSolvers = fromMaybe campaignConf.symExecNSolvers cliSymExecNSolvers
       }
 
     overrideSolConf solConf = solConf
diff --git a/src/test/Common.hs b/src/test/Common.hs
index 5e240953b..ae658a76a 100644
--- a/src/test/Common.hs
+++ b/src/test/Common.hs
@@ -50,6 +50,8 @@ import Echidna.Types.Solidity (SolConf(..))
 import Echidna.Types.Test
 import Echidna.Types.Tx (Tx(..), TxCall(..), call)
 
+import EVM.Solidity (Contracts(..), BuildOutput(..))
+
 testConfig :: EConfig
 testConfig = defaultConfig & overrideQuiet
                            & overrideLimits
@@ -83,17 +85,18 @@ withSolcVersion (Just f) t = do
     Right v' -> if f v' then t else assertBool "skip" True
     Left e   -> error $ show e
 
-runContract :: FilePath -> Maybe ContractName -> EConfig -> IO (Env, WorkerState)
-runContract f selectedContract cfg = do
+runContract :: FilePath -> Maybe ContractName -> EConfig -> WorkerType -> IO (Env, WorkerState)
+runContract f selectedContract cfg workerType = do
   seed <- maybe (getRandomR (0, maxBound)) pure cfg.campaignConf.seed
   buildOutput <- compileContracts cfg.solConf (f :| [])
   env <- mkEnv cfg buildOutput
 
   (vm, world, dict) <- prepareContract env (f :| []) selectedContract seed
 
-  let corpus = []
+  let (Contracts contractMap) = buildOutput.contracts
+
   (_stopReason, finalState) <- flip runReaderT env $
-    runWorker (pure ()) vm world dict 0 corpus cfg.campaignConf.testLimit
+    runWorker workerType (pure ()) vm world dict 0 [] cfg.campaignConf.testLimit selectedContract (Map.elems contractMap)
 
   -- TODO: consider snapshotting the state so checking function don't need to
   -- be IO
@@ -104,7 +107,7 @@ testContract
   -> Maybe FilePath
   -> [(String, (Env, WorkerState) -> IO Bool)]
   -> TestTree
-testContract fp cfg = testContract' fp Nothing Nothing cfg True
+testContract fp cfg = testContract' fp Nothing Nothing cfg True FuzzWorker
 
 testContractV
   :: FilePath
@@ -112,7 +115,7 @@ testContractV
   -> Maybe FilePath
   -> [(String, (Env, WorkerState) -> IO Bool)]
   -> TestTree
-testContractV fp v cfg = testContract' fp Nothing v cfg True
+testContractV fp v cfg = testContract' fp Nothing v cfg True FuzzWorker
 
 testContract'
   :: FilePath
@@ -120,9 +123,10 @@ testContract'
   -> Maybe SolcVersionComp
   -> Maybe FilePath
   -> Bool
+  -> WorkerType
   -> [(String, (Env, WorkerState) -> IO Bool)]
   -> TestTree
-testContract' fp n v configPath s expectations = testCase fp $ withSolcVersion v $ do
+testContract' fp n v configPath s workerType expectations = testCase fp $ withSolcVersion v $ do
   c <- case configPath of
     Just path -> do
       parsed <- parseConfig path
@@ -130,7 +134,7 @@ testContract' fp n v configPath s expectations = testCase fp $ withSolcVersion v
     Nothing -> pure testConfig
   let c' = c & overrideQuiet
              & (if s then overrideLimits else id)
-  result <- runContract fp n c'
+  result <- runContract fp n c' workerType
   forM_ expectations $ \(message, assertion) -> do
     assertion result >>= assertBool message
 
diff --git a/src/test/Spec.hs b/src/test/Spec.hs
index dbc39b59d..bd01cf17b 100644
--- a/src/test/Spec.hs
+++ b/src/test/Spec.hs
@@ -14,6 +14,7 @@ import Tests.Values (valuesTests)
 import Tests.Seed (seedTests)
 import Tests.Dapptest (dapptestTests)
 import Tests.Cheat (cheatTests)
+import Tests.Symbolic (symbolicTests)
 
 main :: IO ()
 main = withCurrentDirectory "./tests/solidity" . defaultMain $
@@ -32,4 +33,5 @@ main = withCurrentDirectory "./tests/solidity" . defaultMain $
            , dapptestTests
            , encodingJSONTests
            , cheatTests
+           , symbolicTests
            ]
diff --git a/src/test/Tests/Assertion.hs b/src/test/Tests/Assertion.hs
index 4155d1123..089d55af9 100644
--- a/src/test/Tests/Assertion.hs
+++ b/src/test/Tests/Assertion.hs
@@ -4,6 +4,8 @@ import Test.Tasty (TestTree, testGroup)
 
 import Common (testContract, testContract', testContractV, solcV, solved, solvedUsing, passed)
 
+import Echidna.Types.Campaign (WorkerType(..))
+
 assertionTests :: TestTree
 assertionTests = testGroup "Assertion-based Integration Testing"
   [
@@ -34,10 +36,10 @@ assertionTests = testGroup "Assertion-based Integration Testing"
       [ ("fail passed",     solvedUsing "fail" "AssertionFailed(..)")
       , ("f failed",         passed     "f")
       ]
-    , testContract' "assert/conf.sol" (Just "A") Nothing (Just "assert/multi.yaml") True
+    , testContract' "assert/conf.sol" (Just "A") Nothing (Just "assert/multi.yaml") True FuzzWorker
       [ ("c failed", passed "c") ]
 
-    , testContract' "assert/fullmath.sol" (Just "FullMathEchidnaTest") (Just (\v -> v == solcV (0,7,5))) (Just "assert/config.yaml") False
+    , testContract' "assert/fullmath.sol" (Just "FullMathEchidnaTest") (Just (\v -> v == solcV (0,7,5))) (Just "assert/config.yaml") False FuzzWorker
       [ ("checkMulDivRoundingUp failed", solved "checkMulDivRoundingUp") ]
 
   ]
diff --git a/src/test/Tests/Cheat.hs b/src/test/Tests/Cheat.hs
index 1962fe8ab..8a11b8367 100644
--- a/src/test/Tests/Cheat.hs
+++ b/src/test/Tests/Cheat.hs
@@ -4,9 +4,11 @@ import Test.Tasty (TestTree, testGroup)
 
 import Common (testContract', solcV, solved)
 
+import Echidna.Types.Campaign (WorkerType(..))
+
 cheatTests :: TestTree
 cheatTests =
   testGroup "Cheatcodes Tests"
-    [ testContract' "cheat/ffi.sol" (Just "TestFFI") (Just (> solcV (0,6,0))) (Just "cheat/ffi.yaml") False
+    [ testContract' "cheat/ffi.sol" (Just "TestFFI") (Just (> solcV (0,6,0))) (Just "cheat/ffi.yaml") False FuzzWorker
         [ ("echidna_ffi passed", solved "echidna_ffi") ]
     ]
diff --git a/src/test/Tests/Coverage.hs b/src/test/Tests/Coverage.hs
index c56b54015..d1d29c2b9 100644
--- a/src/test/Tests/Coverage.hs
+++ b/src/test/Tests/Coverage.hs
@@ -10,7 +10,7 @@ coverageTests = testGroup "Coverage tests"
       -- single.sol is really slow and kind of unstable. it also messes up travis.
      -- testContract "coverage/single.sol"    (Just "coverage/test.yaml")
      -- [ ("echidna_state failed",                   solved      "echidna_state") ]
-     -- testContract' "coverage/multi.sol" Nothing Nothing (Just "coverage/test.yaml") False
+     -- testContract' "coverage/multi.sol" Nothing Nothing (Just "coverage/test.yaml") False False
      -- [ ("echidna_state3 failed",                  solved      "echidna_state3") ]
       testContract "coverage/boolean.sol"       (Just "coverage/boolean.yaml")
       [ ("echidna_true failed",                    passed     "echidna_true")
diff --git a/src/test/Tests/Dapptest.hs b/src/test/Tests/Dapptest.hs
index 7cf0dd8d2..ab4ad12e5 100644
--- a/src/test/Tests/Dapptest.hs
+++ b/src/test/Tests/Dapptest.hs
@@ -4,9 +4,11 @@ import Test.Tasty (TestTree, testGroup)
 
 import Common (testContract', solcV, solved, passed)
 
+import Echidna.Types.Campaign (WorkerType(..))
+
 dapptestTests :: TestTree
 dapptestTests = testGroup "Dapptest Integration Testing"
-  [ testContract' "dapptest/basic.sol" (Just "GreeterTest") (Just (\v -> v >= solcV (0,7,5))) (Just "dapptest/config.yaml") False
+  [ testContract' "dapptest/basic.sol" (Just "GreeterTest") (Just (\v -> v >= solcV (0,7,5))) (Just "dapptest/config.yaml") False FuzzWorker
      [ 
         ("testShrinking passed", solved "testShrinking"),
         ("testFuzzFixedArray passed", solved "testFuzzFixedArray"),
diff --git a/src/test/Tests/Integration.hs b/src/test/Tests/Integration.hs
index 287c17170..6abc27f79 100644
--- a/src/test/Tests/Integration.hs
+++ b/src/test/Tests/Integration.hs
@@ -5,6 +5,7 @@ import Test.Tasty (TestTree, testGroup)
 import Common (testContract, testContractV, solcV, testContract', checkConstructorConditions, passed, solved, solvedLen, solvedWith, solvedWithout, gasInRange)
 import Data.Functor ((<&>))
 import Data.Text (unpack)
+import Echidna.Types.Campaign (WorkerType(..))
 import Echidna.Types.Tx (TxCall(..))
 import EVM.ABI (AbiValue(..))
 
@@ -76,7 +77,7 @@ integrationTests = testGroup "Solidity Integration Testing"
       [ ("echidna_construct passed",               solved      "echidna_construct") ]
   , testContract "basic/gasprice.sol"     (Just "basic/gasprice.yaml")
       [ ("echidna_state passed",                   solved      "echidna_state") ]
-  , testContract' "basic/allContracts.sol" (Just "B") Nothing (Just "basic/allContracts.yaml") True
+  , testContract' "basic/allContracts.sol" (Just "B") Nothing (Just "basic/allContracts.yaml") True FuzzWorker
       [ ("echidna_test passed",                    solved      "echidna_test") ]
   , testContract "basic/array-mutation.sol"   Nothing
       [ ("echidna_mutated passed",                 solved      "echidna_mutated") ]
@@ -97,9 +98,9 @@ integrationTests = testGroup "Solidity Integration Testing"
       "invalid codesize"
   , testContractV "basic/eip-170.sol" (Just (>= solcV (0,5,0))) (Just "basic/eip-170.yaml")
       [ ("echidna_test passed",                    passed      "echidna_test") ]
-  , testContract' "basic/deploy.sol" (Just "Test") Nothing (Just "basic/deployContract.yaml") True
+  , testContract' "basic/deploy.sol" (Just "Test") Nothing (Just "basic/deployContract.yaml") True FuzzWorker
       [ ("test passed",                    solved     "test") ]
-  , testContract' "basic/deploy.sol" (Just "Test") Nothing (Just "basic/deployBytecode.yaml") True
+  , testContract' "basic/deploy.sol" (Just "Test") Nothing (Just "basic/deployBytecode.yaml") True FuzzWorker
       [ ("test passed",                    solved     "test") ]
   , testContract "basic/flags.sol" (Just "basic/etheno-query-error.yaml")
       [] -- Just check if the etheno config does not crash Echidna
diff --git a/src/test/Tests/Research.hs b/src/test/Tests/Research.hs
index ecb7cca88..86949f309 100644
--- a/src/test/Tests/Research.hs
+++ b/src/test/Tests/Research.hs
@@ -4,15 +4,17 @@ import Test.Tasty (TestTree, testGroup)
 
 import Common (testContract, testContract', solcV, solved)
 
+import Echidna.Types.Campaign (WorkerType(..))
+
 researchTests :: TestTree
 researchTests = testGroup "Research-based Integration Testing"
   [ testContract "research/harvey_foo.sol" Nothing
       [ ("echidna_assert failed",     solved "echidna_assert") ]
-  , testContract' "research/harvey_baz.sol" Nothing Nothing Nothing False
+  , testContract' "research/harvey_baz.sol" Nothing Nothing Nothing False FuzzWorker
       [ ("echidna_all_states failed", solved "echidna_all_states") ]
-  , testContract' "research/ilf_crowdsale.sol" Nothing (Just (\v -> v >= solcV (0,5,0) && v < solcV (0,6,0))) (Just "research/ilf_crowdsale.yaml") False
+  , testContract' "research/ilf_crowdsale.sol" Nothing (Just (\v -> v >= solcV (0,5,0) && v < solcV (0,6,0))) (Just "research/ilf_crowdsale.yaml") False FuzzWorker
       [ ("echidna_assert failed", solved "withdraw") ]
-  , testContract' "research/solcfuzz_funwithnumbers.sol" (Just "VerifyFunWithNumbers") (Just (< solcV (0,6,0))) (Just "research/solcfuzz_funwithnumbers.yaml") True
+  , testContract' "research/solcfuzz_funwithnumbers.sol" (Just "VerifyFunWithNumbers") (Just (< solcV (0,6,0))) (Just "research/solcfuzz_funwithnumbers.yaml") True FuzzWorker
       [ ("echidna_assert failed", solved "sellTokens"),
         ("echidna_assert failed", solved "buyTokens")
       ]
diff --git a/src/test/Tests/Seed.hs b/src/test/Tests/Seed.hs
index b609174fc..78897b921 100644
--- a/src/test/Tests/Seed.hs
+++ b/src/test/Tests/Seed.hs
@@ -21,7 +21,7 @@ seedTests =
     ]
     where
     cfg s = defaultConfig
-      { campaignConf = CampaignConf
+      { campaignConf = defaultConfig.campaignConf
         { testLimit = 600
         , stopOnFail = False
         , estimateGas = False
@@ -39,6 +39,6 @@ seedTests =
       }
       & overrideQuiet
     gen s = do
-      (env, _) <- runContract "basic/flags.sol" Nothing (cfg s)
+      (env, _) <- runContract "basic/flags.sol" Nothing (cfg s) FuzzWorker
       readIORef env.testsRef
     same s t = (\x y -> ((.reproducer) <$> x) == ((.reproducer) <$> y)) <$> gen s <*> gen t
diff --git a/src/test/Tests/Symbolic.hs b/src/test/Tests/Symbolic.hs
new file mode 100644
index 000000000..4ff86df8f
--- /dev/null
+++ b/src/test/Tests/Symbolic.hs
@@ -0,0 +1,15 @@
+module Tests.Symbolic (symbolicTests) where
+
+import Test.Tasty (TestTree, testGroup)
+import Common (testContract', solved, passed)
+import Echidna.Types.Campaign (WorkerType(..))
+
+symbolicTests :: TestTree
+symbolicTests = testGroup "Symbolic tests"
+  [ testContract' "symbolic/sym.sol" Nothing Nothing (Just "symbolic/sym.yaml") True SymbolicWorker
+      [ ("echidna_sym passed", passed "echidna_sym") ]
+
+  , testContract' "symbolic/sym-assert.sol" Nothing Nothing (Just "symbolic/sym-assert.yaml") True SymbolicWorker
+      [ ("func_one passed", solved "func_one")
+      , ("func_two passed", solved "func_two") ]
+  ]
diff --git a/src/test/Tests/Values.hs b/src/test/Tests/Values.hs
index 36c738bf9..58fa10cea 100644
--- a/src/test/Tests/Values.hs
+++ b/src/test/Tests/Values.hs
@@ -4,12 +4,14 @@ import Test.Tasty (TestTree, testGroup)
 
 import Common (testContract, testContract', solved, solvedLen)
 
+import Echidna.Types.Campaign (WorkerType(..))
+
 valuesTests :: TestTree
 valuesTests = testGroup "Value extraction tests"
   [ 
     testContract "values/nearbyMining.sol" Nothing
       [ ("echidna_findNearby passed", solved "echidna_findNearby") ]
-    , testContract' "values/smallValues.sol" Nothing Nothing (Just "coverage/test.yaml") False
+    , testContract' "values/smallValues.sol" Nothing Nothing (Just "coverage/test.yaml") False FuzzWorker
       [ ("echidna_findSmall passed", solved "echidna_findSmall") ]
     , testContract "values/constants.sol"    Nothing
       [ ("echidna_found failed",                   solved      "echidna_found")
@@ -20,15 +22,15 @@ valuesTests = testGroup "Value extraction tests"
       [ ("echidna_found_sender failed",            solved      "echidna_found_sender") ]
     , testContract "values/rconstants.sol"   Nothing
       [ ("echidna_found failed",                   solved      "echidna_found") ]
-    , testContract' "values/extreme.sol"   Nothing Nothing (Just "values/extreme.yaml") False
+    , testContract' "values/extreme.sol"   Nothing Nothing (Just "values/extreme.yaml") False FuzzWorker
       [ ("testMinInt8 passed",                   solved      "testMinInt8"),
         ("testMinInt16 passed",                  solved      "testMinInt16"),
         ("testMinInt64 passed",                  solved      "testMinInt32"),
         ("testMinInt128 passed",                 solved      "testMinInt128")
       ]
-    , testContract' "values/utf8.sol"   Nothing Nothing (Just "values/extreme.yaml") False
+    , testContract' "values/utf8.sol"   Nothing Nothing (Just "values/extreme.yaml") False FuzzWorker
       [ ("testNonUtf8 passed",                   solved      "testNonUTF8")]
-    , testContract' "values/create.sol" (Just "C") Nothing Nothing True
+    , testContract' "values/create.sol" (Just "C") Nothing Nothing True FuzzWorker
       [ ("echidna_state failed",                   solved      "echidna_state") ]
     , testContract "values/time.sol"         (Just "values/time.yaml")
       [ ("echidna_timepassed passed",              solved      "echidna_timepassed") ]
diff --git a/stack.yaml b/stack.yaml
index 7958d0c76..6480ae009 100644
--- a/stack.yaml
+++ b/stack.yaml
@@ -4,8 +4,8 @@ packages:
 - '.'
 
 extra-deps:
-- git: https://github.com/ethereum/hevm.git
-  commit: a39b1c07a3f643330f920042eb94a43d7e6454b5
+- git: https://github.com/samalws-tob/hevm.git
+  commit: 0a2a7f24303a727b0e65ad2bb3a33ffe4d780a7d
 
 - restless-git-0.7@sha256:346a5775a586f07ecb291036a8d3016c3484ccdc188b574bcdec0a82c12db293,968
 - s-cargot-0.1.4.0@sha256:61ea1833fbb4c80d93577144870e449d2007d311c34d74252850bb48aa8c31fb,3525
diff --git a/tests/solidity/basic/default.yaml b/tests/solidity/basic/default.yaml
index f07593d0a..957391f13 100644
--- a/tests/solidity/basic/default.yaml
+++ b/tests/solidity/basic/default.yaml
@@ -91,3 +91,20 @@ rpcBlock: null
 workers: 1
 # events server port
 server: null
+# whether to add an additional symbolic execution worker
+symExec: false
+# whether symbolic execution will be concolic (vs full symbolic execution)
+# only relevant if symExec is true
+symExecConcolic: true
+# number of SMT solvers used in symbolic execution
+# only relevant if symExec is true
+symExecNSolvers: 1
+# timeout for symbolic execution SMT solver
+# only relevant if symExec is true
+symExecTimeout: 30
+# Number of times we may revisit a particular branching point
+# only relevant if symExec is true and symExecConcolic is false
+symExecMaxIters: 10
+# Number of times we may revisit a particular branching point before we consult the smt solver to check reachability
+# only relevant if symExec is true and symExecConcolic is false
+symExecAskSMTIters: 1
diff --git a/tests/solidity/symbolic/sym-assert.sol b/tests/solidity/symbolic/sym-assert.sol
new file mode 100644
index 000000000..7b994d2a4
--- /dev/null
+++ b/tests/solidity/symbolic/sym-assert.sol
@@ -0,0 +1,15 @@
+contract VulnerableContract {
+    mapping (uint256 => uint256) a;
+    function func_one(uint256 x) public payable {
+        a[12323] = ((x >> 5) / 7777);
+        if (a[12323] == 2222) {
+            assert(false); // BUG
+        }
+    }
+
+    function func_two(uint256 x) public payable {
+        if ((x >> 5) / 7777 == 2222) {
+            assert(false); // BUG
+        }
+    }
+}
diff --git a/tests/solidity/symbolic/sym-assert.yaml b/tests/solidity/symbolic/sym-assert.yaml
new file mode 100644
index 000000000..d450b17e6
--- /dev/null
+++ b/tests/solidity/symbolic/sym-assert.yaml
@@ -0,0 +1,4 @@
+testMode: assertion
+symExec: true
+symExecConcolic: false
+workers: 0
diff --git a/tests/solidity/symbolic/sym.sol b/tests/solidity/symbolic/sym.sol
new file mode 100644
index 000000000..8b46a52a7
--- /dev/null
+++ b/tests/solidity/symbolic/sym.sol
@@ -0,0 +1,21 @@
+contract VulnerableContract {
+    mapping (uint256 => uint256) a;
+    bool y;
+    bool z;
+    function func_one(uint256 x) public payable {
+        a[12323] = ((x >> 5) / 7777);
+        if (a[12323] == 2222) {
+            y = true;
+        }
+    }
+
+    function func_two(uint256 x) public payable {
+        if ((x >> 5) / 7777 == 2222) {
+            z = true;
+        }
+    }
+
+    function echidna_sym() public returns (bool) {
+        return !(y && z);
+    }
+}
diff --git a/tests/solidity/symbolic/sym.yaml b/tests/solidity/symbolic/sym.yaml
new file mode 100644
index 000000000..03cecaf6f
--- /dev/null
+++ b/tests/solidity/symbolic/sym.yaml
@@ -0,0 +1,3 @@
+symExec: true
+workers: 0
+symExecConcolic: false