diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index 063626274..0514eefa5 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -64,6 +64,9 @@ jobs:
       # if we run this in nix build we often get killed due to oom in ci
       - name: run ethereum tests
         run: nix develop --command bash -c "cabal --active-repositories=:none run ethereum-tests"
+      # if we run this in nix build, it complains about running in a sandbox
+      - name: run cli tests
+        run: nix develop --command bash -c "cabal --active-repositories=:none run cli-test"
 
   build-windows-bitwuzla:
     name: bitwuzla-build (win64 target)
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 6b30e4f2a..129f8a113 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -45,6 +45,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - Allow user to change the verbosity level via `--verb`. For the moment, this is only to
   print some warnings related to zero-address dereference and to print `hemv test`'s
   output in case of failure
+- Simple test cases for the CLI
 
 ## Fixed
 - We now try to simplify expressions fully before trying to cast them to a concrete value
@@ -76,6 +77,8 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
   determining when (Eq a b) is true when a==b modulo commutativity
 - `hevm test`'s flag ` --verbose` is now `--verb`, which also increases verbosity
   for other elements of the system
+- We now use Options.Applicative and a rather different way of parsing CLI options.
+  This should give us much better control over the CLI options and their parsing.
 
 ## [0.54.2] - 2024-12-12
 
diff --git a/cli/cli.hs b/cli/cli.hs
index 0d567eb03..36cbcd091 100644
--- a/cli/cli.hs
+++ b/cli/cli.hs
@@ -3,6 +3,7 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE DeriveAnyClass #-}
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE OverloadedStrings #-}
 
 module Main where
 
@@ -14,7 +15,7 @@ import Data.ByteString (ByteString)
 import qualified Data.ByteString.Lazy as BS
 import qualified Data.ByteString.Char8 as BC
 import Data.DoubleWord (Word256)
-import Data.List (intersperse)
+import Data.List (intersperse, intercalate)
 import Data.Maybe (fromMaybe, mapMaybe, fromJust, isNothing, isJust)
 import Data.Text qualified as T
 import Data.Text.IO qualified as T
@@ -24,12 +25,14 @@ import GHC.Conc (getNumProcessors)
 import Numeric.Natural (Natural)
 import Optics.Core ((&), set)
 import Witch (unsafeInto)
-import Options.Generic as Options
+import Options.Generic as OptionsGeneric
+import Options.Applicative as Options
 import Paths_hevm qualified as Paths
 import System.Directory (withCurrentDirectory, getCurrentDirectory, doesDirectoryExist, makeAbsolute)
 import System.FilePath ((</>))
 import System.Exit (exitFailure, exitWith, ExitCode(..))
-import Main.Utf8 (withUtf8)
+import Data.List.Split (splitOn)
+import Text.Read (readMaybe)
 
 import EVM (initialContract, abstractContract, makeVm)
 import EVM.ABI (Sig(..))
@@ -52,170 +55,236 @@ import EVM.Effects
 import EVM.Expr (maybeLitWordSimp, maybeLitAddrSimp)
 
 data AssertionType = DSTest | Forge
-  deriving (Eq, Show, Read, ParseField)
-
--- This record defines the program's command-line options
--- automatically via the `optparse-generic` package.
-data Command w
-  = Symbolic -- Symbolically explore an abstract program, or specialized with specified env & calldata
-  -- vm opts
-      { code          :: w ::: Maybe ByteString <?> "Program bytecode"
-      , codeFile    :: w ::: Maybe String       <?> "Program bytecode in a file"
-      , calldata      :: w ::: Maybe ByteString <?> "Tx: calldata"
-      , address       :: w ::: Maybe Addr       <?> "Tx: address"
-      , caller        :: w ::: Maybe Addr       <?> "Tx: caller"
-      , origin        :: w ::: Maybe Addr       <?> "Tx: origin"
-      , coinbase      :: w ::: Maybe Addr       <?> "Block: coinbase"
-      , value         :: w ::: Maybe W256       <?> "Tx: Eth amount"
-      , nonce         :: w ::: Maybe Word64     <?> "Nonce of origin"
-      , gas           :: w ::: Maybe Word64     <?> "Tx: gas amount"
-      , number        :: w ::: Maybe W256       <?> "Block: number"
-      , timestamp     :: w ::: Maybe W256       <?> "Block: timestamp"
-      , basefee       :: w ::: Maybe W256       <?> "Block: base fee"
-      , priorityFee   :: w ::: Maybe W256       <?> "Tx: priority fee"
-      , gaslimit      :: w ::: Maybe Word64     <?> "Tx: gas limit"
-      , gasprice      :: w ::: Maybe W256       <?> "Tx: gas price"
-      , create        :: w ::: Bool             <?> "Tx: creation"
-      , maxcodesize   :: w ::: Maybe W256       <?> "Block: max code size"
-      , prevRandao    :: w ::: Maybe W256       <?> "Block: prevRandao"
-      , chainid       :: w ::: Maybe W256       <?> "Env: chainId"
-  -- remote state opts
-      , rpc           :: w ::: Maybe URL        <?> "Fetch state from a remote node"
-      , block         :: w ::: Maybe W256       <?> "Block state is be fetched from"
-
-  -- symbolic execution opts
-      , root          :: w ::: Maybe String       <?> "Path to  project root directory (default: . )"
-      , projectType   :: w ::: Maybe ProjectType  <?> "Is this a CombinedJSON or Foundry project (default: Foundry)"
-      , assertionType :: w ::: Maybe AssertionType <?> "Assertions as per Forge or DSTest (default: Forge)"
-      , initialStorage :: w ::: Maybe (InitialStorage) <?> "Starting state for storage: Empty, Abstract (default Abstract)"
-      , sig           :: w ::: Maybe Text         <?> "Signature of types to decode / encode"
-      , arg           :: w ::: [String]           <?> "Values to encode"
-      , getModels     :: w ::: Bool               <?> "Print example testcase for each execution path"
-      , showTree      :: w ::: Bool               <?> "Print branches explored in tree view"
-      , showReachableTree :: w ::: Bool           <?> "Print only reachable branches explored in tree view"
-      , smttimeout    :: w ::: Maybe Natural      <?> "Timeout given to SMT solver in seconds (default: 300)"
-      , maxIterations :: w ::: Maybe Integer      <?> "Number of times we may revisit a particular branching point. For no bound, set -1 (default: 5)"
-      , solver        :: w ::: Maybe Text         <?> "Used SMT solver: z3 (default), cvc5, or bitwuzla"
-      , smtdebug      :: w ::: Bool               <?> "Print smt queries sent to the solver"
-      , debug         :: w ::: Bool               <?> "Debug printing of internal behaviour, and dump internal expressions"
-      , trace         :: w ::: Bool               <?> "Dump trace"
-      , assertions    :: w ::: Maybe [Word256]    <?> "Comma separated list of solc panic codes to check for (default: user defined assertion violations only)"
-      , askSmtIterations :: w ::: Integer         <!> "1" <?> "Number of times we may revisit a particular branching point before we consult the smt solver to check reachability (default: 1)"
-      , numCexFuzz    :: w ::: Integer            <!> "3" <?> "Number of fuzzing tries to do to generate a counterexample (default: 3)"
-      , numSolvers    :: w ::: Maybe Natural      <?> "Number of solver instances to use (default: number of cpu cores)"
-      , solverThreads :: w ::: Maybe Natural      <?> "Number of threads for each solver instance. Only respected for Z3 (default: 1)"
-      , loopDetectionHeuristic :: w ::: LoopHeuristic <!> "StackBased" <?> "Which heuristic should be used to determine if we are in a loop: StackBased (default) or Naive"
-      , noDecompose   :: w ::: Bool               <?> "Don't decompose storage slots into separate arrays"
-      , maxBranch     :: w ::: Int                <!> "100" <?> "Max number of branches to explore when encountering a symbolic value (default: 100)"
-      , promiseNoReent:: w ::: Bool               <!> "Promise no reentrancy is possible into the contract(s) being examined"
-      , maxBufSize    :: w ::: Int                <!> "64" <?> "Maximum size of buffers such as calldata and returndata in exponents of 2 (default: 64, i.e. 2^64 bytes)"
-      , verb          :: w ::: Int                <!> "1" <?> "Verbosity level (default: 1)"
-      }
-  | Equivalence -- prove equivalence between two programs
-      { codeA         :: w ::: Maybe ByteString   <?> "Bytecode of the first program"
-      , codeB         :: w ::: Maybe ByteString   <?> "Bytecode of the second program"
-      , codeAFile     :: w ::: Maybe String     <?> "First program's bytecode in a file"
-      , codeBFile     :: w ::: Maybe String     <?> "Second program's bytecode in a file"
-      , sig           :: w ::: Maybe Text       <?> "Signature of types to decode / encode"
-      , arg           :: w ::: [String]         <?> "Values to encode"
-      , calldata      :: w ::: Maybe ByteString <?> "Tx: calldata"
-      , smttimeout    :: w ::: Maybe Natural    <?> "Timeout given to SMT solver in seconds (default: 300)"
-      , maxIterations :: w ::: Maybe Integer    <?> "Number of times we may revisit a particular branching point. For no bound, set -1 (default: 5)"
-      , solver        :: w ::: Maybe Text       <?> "Used SMT solver: z3 (default), cvc5, or bitwuzla"
-      , smtoutput     :: w ::: Bool             <?> "Print verbose smt output"
-      , smtdebug      :: w ::: Bool             <?> "Print smt queries sent to the solver"
-      , debug         :: w ::: Bool             <?> "Debug printing of internal behaviour, and dump internal expressions"
-      , trace         :: w ::: Bool             <?> "Dump trace"
-      , askSmtIterations :: w ::: Integer       <!> "1" <?> "Number of times we may revisit a particular branching point before we consult the smt solver to check reachability (default: 1)"
-      , numCexFuzz    :: w ::: Integer          <!> "3" <?> "Number of fuzzing tries to do to generate a counterexample (default: 3)"
-      , numSolvers    :: w ::: Maybe Natural    <?> "Number of solver instances to use (default: number of cpu cores)"
-      , solverThreads :: w ::: Maybe Natural    <?> "Number of threads for each solver instance. Only respected for Z3 (default: 1)"
-      , loopDetectionHeuristic :: w ::: LoopHeuristic <!> "StackBased" <?> "Which heuristic should be used to determine if we are in a loop: StackBased (default) or Naive"
-      , noDecompose   :: w ::: Bool             <?> "Don't decompose storage slots into separate arrays"
-      , maxBranch     :: w ::: Int              <!> "100" <?> "Max number of branches to explore when encountering a symbolic value (default: 100)"
-      , maxBufSize    :: w ::: Int              <!> "64" <?> "Maximum size of buffers such as calldata and returndata in exponents of 2 (default: 64, i.e. 2^64 bytes)"
-      , promiseNoReent:: w ::: Bool             <!> "Promise no reentrancy is possible into the contract(s) being examined"
-      , verb          :: w ::: Int              <!> "1" <?> "Verbosity level (default: 1)"
-      , create        :: w ::: Bool             <?> "Tx: creation"
-      }
-  | Exec -- Execute a given program with specified env & calldata
-      { code        :: w ::: Maybe ByteString  <?> "Program bytecode"
-      , codeFile    :: w ::: Maybe String      <?> "Program bytecode in a file"
-      , calldata    :: w ::: Maybe ByteString  <?> "Tx: calldata"
-      , address     :: w ::: Maybe Addr        <?> "Tx: address"
-      , caller      :: w ::: Maybe Addr        <?> "Tx: caller"
-      , origin      :: w ::: Maybe Addr        <?> "Tx: origin"
-      , coinbase    :: w ::: Maybe Addr        <?> "Block: coinbase"
-      , value       :: w ::: Maybe W256        <?> "Tx: Eth amount"
-      , nonce       :: w ::: Maybe Word64      <?> "Nonce of origin"
-      , gas         :: w ::: Maybe Word64      <?> "Tx: gas amount"
-      , number      :: w ::: Maybe W256        <?> "Block: number"
-      , timestamp   :: w ::: Maybe W256        <?> "Block: timestamp"
-      , basefee     :: w ::: Maybe W256        <?> "Block: base fee"
-      , priorityFee :: w ::: Maybe W256        <?> "Tx: priority fee"
-      , gaslimit    :: w ::: Maybe Word64      <?> "Tx: gas limit"
-      , gasprice    :: w ::: Maybe W256        <?> "Tx: gas price"
-      , create      :: w ::: Bool              <?> "Tx: creation"
-      , maxcodesize :: w ::: Maybe W256        <?> "Block: max code size"
-      , prevRandao  :: w ::: Maybe W256        <?> "Block: prevRandao"
-      , chainid     :: w ::: Maybe W256        <?> "Env: chainId"
-      , debug         :: w ::: Bool            <?> "Debug printing of internal behaviour, and dump internal expressions"
-      , trace       :: w ::: Bool              <?> "Dump trace"
-      , rpc         :: w ::: Maybe URL         <?> "Fetch state from a remote node"
-      , block       :: w ::: Maybe W256        <?> "Block state is be fetched from"
-      , root        :: w ::: Maybe String      <?> "Path to  project root directory (default: . )"
-      , projectType :: w ::: Maybe ProjectType <?> "Is this a CombinedJSON or Foundry project (default: Foundry)"
-      , assertionType :: w ::: Maybe AssertionType <?> "Assertions as per Forge or DSTest (default: Forge)"
-      , verb        :: w ::: Int               <!> "1" <?> "Verbosity level (default: 1)"
-      }
-  | Test -- Run Foundry unit tests
-      { root        :: w ::: Maybe String               <?> "Path to  project root directory (default: . )"
-      , projectType   :: w ::: Maybe ProjectType        <?> "Is this a CombinedJSON or Foundry project (default: Foundry)"
-      , assertionType :: w ::: Maybe AssertionType <?> "Assertions as per Forge or DSTest (default: Forge)"
-      , rpc           :: w ::: Maybe URL                <?> "Fetch state from a remote node"
-      , number        :: w ::: Maybe W256               <?> "Block: number"
-      , coverage      :: w ::: Bool                     <?> "Coverage analysis"
-      , match         :: w ::: Maybe String             <?> "Test case filter - only run methods matching regex"
-      , solver        :: w ::: Maybe Text               <?> "Used SMT solver: z3 (default), cvc5, or bitwuzla"
-      , numSolvers    :: w ::: Maybe Natural            <?> "Number of solver instances to use (default: number of cpu cores)"
-      , solverThreads :: w ::: Maybe Natural            <?> "Number of threads for each solver instance. Only respected for Z3 (default: 1)"
-      , smtdebug      :: w ::: Bool                     <?> "Print smt queries sent to the solver"
-      , debug         :: w ::: Bool                     <?> "Debug printing of internal behaviour, and dump internal expressions"
-      , trace         :: w ::: Bool                     <?> "Dump trace"
-      , ffi           :: w ::: Bool                     <?> "Allow the usage of the hevm.ffi() cheatcode (WARNING: this allows test authors to execute arbitrary code on your machine)"
-      , smttimeout    :: w ::: Maybe Natural            <?> "Timeout given to SMT solver in seconds (default: 300)"
-      , maxIterations :: w ::: Maybe Integer            <?> "Number of times we may revisit a particular branching point. For no bound, set -1 (default: 5)"
-      , loopDetectionHeuristic :: w ::: LoopHeuristic   <!> "StackBased" <?> "Which heuristic should be used to determine if we are in a loop: StackBased (default) or Naive"
-      , noDecompose   :: w ::: Bool                     <?> "Don't decompose storage slots into separate arrays"
-      , maxBranch     :: w ::: Int                      <!> "100" <?> "Max number of branches to explore when encountering a symbolic value (default: 100)"
-      , numCexFuzz    :: w ::: Integer                  <!> "3" <?> "Number of fuzzing tries to do to generate a counterexample (default: 3)"
-      , askSmtIterations :: w ::: Integer               <!> "1" <?> "Number of times we may revisit a particular branching point before we consult the smt solver to check reachability (default: 1)"
-      , maxBufSize    :: w ::: Int                      <!> "64" <?> "Maximum size of buffers such as calldata and returndata in exponents of 2 (default: 64, i.e. 2^64 bytes)"
-      , promiseNoReent:: w ::: Bool                     <!> "Promise no reentrancy is possible into the contract(s) being examined"
-      , verb          :: w ::: Int                      <!> "1" <?> "Verbosity level (default: 1)"
-      }
+  deriving (Eq, Show, Read)
+
+projectTypeParser :: Parser ProjectType
+projectTypeParser = option auto (long "project-type" <> showDefault <> value Foundry <> help "Is this a CombinedJSON or Foundry project")
+
+sigParser :: Parser (Maybe Text)
+sigParser = (optional $ strOption $ long "sig" <> help "Signature of types to decode/encode")
+
+argParser :: Parser [String]
+argParser = (many $ strOption $ long "arg" <> help "Value(s) to encode. Can be given multiple times, once for each argument")
+
+createParser :: Parser Bool
+createParser = switch $ long "create" <> help "Tx: creation"
+
+rpcParser :: Parser (Maybe URL)
+rpcParser = (optional $ strOption $ long "rpc" <> help "Fetch state from a remote node")
+
+data CommonOptions = CommonOptions
+  { askSmtIterations ::Integer
+  , loopDetectionHeuristic ::LoopHeuristic
+  , noDecompose   ::Bool
+  , maxBranch     ::Int
+  , solver        ::Text
+  , debug         ::Bool
+  , calldata      ::Maybe ByteString
+  , trace         ::Bool
+  , verb          ::Int
+  , root          ::Maybe String
+  , assertionType ::AssertionType
+  , solverThreads ::Natural
+  , smttimeout    ::Natural
+  , smtdebug      ::Bool
+  , smtoutput     ::Bool
+  , numSolvers    ::Maybe Natural
+  , numCexFuzz    ::Integer
+  , maxIterations ::Integer
+  , promiseNoReent::Bool
+  , maxBufSize    ::Int
+  }
+
+commonOptions :: Parser CommonOptions
+commonOptions = CommonOptions
+  <$> option auto ( long "ask-smt-iterations" <> value 1 <>
+    help "Number of times we may revisit a particular branching point before we consult the smt solver to check reachability")
+  <*> option auto (long "loop-detection-heuristic" <> showDefault <> value StackBased <>
+    help "Which heuristic should be used to determine if we are in a loop: StackBased or Naive")
+  <*> (switch $ long "no-decompose"         <> help "Don't decompose storage slots into separate arrays")
+  <*> (option auto $ long "max-branch"      <> showDefault <> value 100 <> help "Max number of branches to explore when encountering a symbolic value")
+  <*> (strOption $ long "solver"            <> value "z3" <> help "Used SMT solver: z3, cvc5, or bitwuzla")
+  <*> (switch $ long "debug"                <> help "Debug printing of internal behaviour, and dump internal expressions")
+  <*> (optional $ strOption $ long "calldata" <> help "Tx: calldata")
+  <*> (switch $ long "trace"                <> help "Dump trace")
+  <*> (option auto $ long "verb"            <> showDefault <> value 1 <> help "Append call trace: {1} failures {2} all")
+  <*> (optional $ strOption $ long "root"   <> help "Path to  project root directory")
+  <*> (option auto $ long "assertion-type"  <> showDefault <> value Forge <> help "Assertions as per Forge or DSTest")
+  <*> (option auto $ long "solver-threads"  <> showDefault <> value 1 <> help "Number of threads for each solver instance. Only respected for Z3")
+  <*> (option auto $ long "smttimeout"      <> value 300 <> help "Timeout given to SMT solver in seconds")
+  <*> (switch $ long "smtdebug"             <> help "Print smt queries sent to the solver")
+  <*> (switch $ long "smtoutput"            <> help "Print verbose smt output")
+  <*> (optional $ option auto $ long "num-solvers" <> help "Number of solver instances to use (default: number of cpu cores)")
+  <*> (option auto $ long "num-cex-fuzz"    <> showDefault <> value 3 <> help "Number of fuzzing tries to do to generate a counterexample")
+  <*> (option auto $ long "max-iterations"  <> showDefault <> value 5 <> help "Number of times we may revisit a particular branching point. For no bound, set -1")
+  <*> (switch $ long "promise-no-reent"     <> help "Promise no reentrancy is possible into the contract(s) being examined")
+  <*> (option auto $ long "max-buf-size"    <> value 64 <> help "Maximum size of buffers such as calldata and returndata in exponents of 2 (default: 64, i.e. 2^64 bytes)")
+
+data CommonExecOptions = CommonExecOptions
+  { address       ::Maybe Addr
+  , caller        ::Maybe Addr
+  , origin        ::Maybe Addr
+  , coinbase      ::Maybe Addr
+  , value         ::Maybe W256
+  , nonce         ::Maybe Word64
+  , gas           ::Maybe Word64
+  , number        ::Maybe W256
+  , timestamp     ::Maybe W256
+  , basefee       ::Maybe W256
+  , priorityFee   ::Maybe W256
+  , gaslimit      ::Maybe Word64
+  , gasprice      ::Maybe W256
+  , maxcodesize   ::Maybe W256
+  , prevRandao    ::Maybe W256
+  , chainid       ::Maybe W256
+  , rpc           ::Maybe URL
+  , block         ::Maybe W256
+}
+
+commonExecOptions :: Parser CommonExecOptions
+commonExecOptions = CommonExecOptions
+  <$> (optional $ option auto $ long "address"       <> help "Tx: address")
+  <*> (optional $ option auto $ long "caller"        <> help "Tx: caller")
+  <*> (optional $ option auto $ long "origin"        <> help "Tx: origin")
+  <*> (optional $ option auto $ long "coinbase"      <> help "Block: coinbase")
+  <*> (optional $ option auto $ long "value"         <> help "Tx: Eth amount")
+  <*> (optional $ option auto $ long "nonce"         <> help "Nonce of origin")
+  <*> (optional $ option auto $ long "gas"           <> help "Tx: gas amount")
+  <*> (optional $ option auto $ long "number"        <> help "Block: number")
+  <*> (optional $ option auto $ long "timestamp"     <> help "Block: timestamp")
+  <*> (optional $ option auto $ long "basefee"       <> help "Block: base fee")
+  <*> (optional $ option auto $ long "priority-fee"  <> help "Tx: priority fee")
+  <*> (optional $ option auto $ long "gaslimit"      <> help "Tx: gas limit")
+  <*> (optional $ option auto $ long "gasprice"      <> help "Tx: gas price")
+  <*> (optional $ option auto $ long "maxcodesize"   <> help "Block: max code size")
+  <*> (optional $ option auto $ long "prev-randao"   <> help "Block: prevRandao")
+  <*> (optional $ option auto $ long "chainid"       <> help "Env: chainId")
+  <*> rpcParser
+  <*> (optional $ option auto $ long "block"         <> help "Block state is be fetched from")
+
+data CommonFileOptions = CommonFileOptions
+ { code        ::Maybe ByteString
+ , codeFile    ::Maybe String
+ }
+
+commonFileOptions :: Parser CommonFileOptions
+commonFileOptions = CommonFileOptions
+  <$> (optional $ strOption $ long "code" <> help "Program bytecode")
+  <*> (optional $ strOption $ long "code-file" <> help "Program bytecode in a file")
+
+data TestOptions = TestOptions
+  { projectType   ::ProjectType
+  , rpc           ::Maybe URL
+  , number        ::Maybe W256
+  , coverage      ::Bool
+  , match         ::Maybe String
+  , ffi           ::Bool
+  }
+
+testOptions :: Parser TestOptions
+testOptions = TestOptions
+  <$> projectTypeParser
+  <*> rpcParser
+  <*> (optional $ option auto $ long "number" <> help "Block: number")
+  <*> (switch $ long "coverage" <> help "Coverage analysis")
+  <*> (optional $ strOption $ long "match" <> help "Test case filter - only run methods matching regex")
+  <*> (switch $ long "ffi" <> help "Allow the usage of the hevm.ffi() cheatcode (WARNING: this allows test authors to execute arbitrary code on your machine)")
+
+
+data EqOptions = EqOptions
+  { codeA         ::Maybe ByteString
+  , codeB         ::Maybe ByteString
+  , codeAFile     ::Maybe String
+  , codeBFile     ::Maybe String
+  , sig           ::Maybe Text
+  , arg           ::[String]
+  , create        ::Bool
+  }
+
+eqOptions :: Parser EqOptions
+eqOptions = EqOptions
+  <$> (optional $ strOption $ long "code-a"      <> help "Bytecode of the first program")
+  <*> (optional $ strOption $ long "code-b"      <> help "Bytecode of the second program")
+  <*> (optional $ strOption $ long "code-a-file" <> help "First program's bytecode in a file")
+  <*> (optional $ strOption $ long "code-b-file" <> help "Second program's bytecode in a file")
+  <*> sigParser
+  <*> argParser
+  <*> createParser
+
+data SymbolicOptions = SymbolicOptions
+  { projectType       ::ProjectType
+  , initialStorage    ::Maybe InitialStorage
+  , getModels         ::Bool
+  , showTree          ::Bool
+  , showReachableTree ::Bool
+  , assertions        ::Maybe String
+  , sig               ::Maybe Text
+  , arg               ::[String]
+  , create            ::Bool
+  }
+
+symbolicOptions :: Parser SymbolicOptions
+symbolicOptions = SymbolicOptions
+  <$> projectTypeParser
+  <*> (optional $ option auto $ long "initial-storage" <> help "Starting state for storage: Empty, Abstract (default Abstract)")
+  <*> (switch $ long "get-models" <> help "Print example testcase for each execution path")
+  <*> (switch $ long "show-tree" <> help "Print branches explored in tree view")
+  <*> (switch $ long "show-reachable-tree" <> showDefault <> help "Print only reachable branches explored in tree view")
+  <*> (optional $ strOption $ long "assertions" <> help "Comma separated list of solc panic codes to check for (default: user defined assertion violations only)")
+  <*> sigParser
+  <*> argParser
+  <*> createParser
+
+data ExecOptions = ExecOptions
+  { projectType   ::ProjectType
+  , create :: Bool
+  }
+execOptions :: Parser ExecOptions
+execOptions = ExecOptions
+  <$> projectTypeParser
+  <*> createParser
+
+-- Combined options data type
+data Command
+  = Symbolic   CommonFileOptions SymbolicOptions CommonExecOptions CommonOptions
+  | Equal      EqOptions CommonOptions
+  | Test       TestOptions  CommonOptions
+  | Exec       CommonFileOptions ExecOptions CommonExecOptions CommonOptions
   | Version
 
-  deriving (Options.Generic)
+-- Parser for the subcommands
+commandParser :: Parser Command
+commandParser = subparser
+  ( command "test"
+      (info (Test <$> testOptions <*> commonOptions <**> helper)
+        (progDesc "Prove Foundry unit tests marked with `prove_`"
+        <> footer "For more help: https://hevm.dev/std-test-tutorial.html" ))
+  <> command "equivalence"
+      (info (Equal <$> eqOptions <*> commonOptions <**> helper)
+        (progDesc "Prove equivalence between two programs"
+        <> footer "For more help: https://hevm.dev/equivalence-checking-tutorial.html" ))
+  <> command "symbolic"
+      (info (Symbolic <$> commonFileOptions <*> symbolicOptions <*> commonExecOptions <*> commonOptions <**> helper)
+        (progDesc "Symbolically explore an abstract program"
+        <> footer "For more help, see: https://hevm.dev/symbolic-execution-tutorial.html" ))
+  <> command "exec"
+      (info (Exec <$> commonFileOptions <*> execOptions <*> commonExecOptions <*> commonOptions <**> helper)
+        (progDesc "Concretely execute a given program"
+        <> footer "For more help, see https://hevm.dev/exec.html" ))
+  <> command "version"
+      (info (pure Version)
+        (progDesc "Show the version of the tool"))
+  )
 
 type URL = Text
 
-
--- For some reason haskell can't derive a
--- parseField instance for (Text, ByteString)
-instance Options.ParseField (Text, ByteString)
-
-deriving instance Options.ParseField Word256
-deriving instance Options.ParseField [Word256]
-
-instance Options.ParseRecord (Command Options.Wrapped) where
-  parseRecord =
-    Options.parseRecordWithModifiers Options.lispCaseModifiers
+deriving instance OptionsGeneric.ParseField Word256
+deriving instance OptionsGeneric.ParseField [Word256]
 
 data InitialStorage
   = Empty
   | Abstract
-  deriving (Show, Read, Options.ParseField)
+  deriving (Show, Read, OptionsGeneric.ParseField)
 
 getFullVersion :: [Char]
 getFullVersion = showVersion Paths.version <> " [" <> gitVersion <> "]"
@@ -225,56 +294,66 @@ getFullVersion = showVersion Paths.version <> " [" <> gitVersion <> "]"
       Right val -> "git rev " <> giBranch val <>  "@" <> giHash val
       Left _ -> "no git revision present"
 
-getMaxBufSize :: Int -> Command Options.Unwrapped -> Int
-getMaxBufSize def (Version {}) = def
-getMaxBufSize def (Exec {}) = def
-getMaxBufSize _ cmd = cmd.maxBufSize
-
 main :: IO ()
-main = withUtf8 $ do
-  cmd <- Options.unwrapRecord "hevm -- Ethereum evaluator"
-  when (getMaxBufSize 64 cmd > 64) $ do
-    putStrLn "Error: maxBufSize must be less than or equal to 64. That limits buffers to a size of 2^64, which is more than enough for practical purposes"
-    exitFailure
-  when (getMaxBufSize 64 cmd < 0) $ do
-    putStrLn "Error: maxBufSize must be at least 0. Negative values do not make sense. A value of zero means at most 1 byte long buffers"
-    exitFailure
-  let env = Env { config = defaultConfig
-    { dumpQueries = cmd.smtdebug
-    , debug = cmd.debug
-    , dumpEndStates = cmd.debug
-    , dumpExprs = cmd.debug
-    , numCexFuzz = cmd.numCexFuzz
-    , dumpTrace = cmd.trace
-    , decomposeStorage = Prelude.not cmd.noDecompose
-    , maxBranch = cmd.maxBranch
-    , promiseNoReent = cmd.promiseNoReent
-    , maxBufSize = getMaxBufSize 64 cmd
-    , verb = cmd.verb
-    } }
+main = do
+  cmd <- execParser $ info (commandParser <**> helper)
+    ( Options.fullDesc
+    <> progDesc "hevm, a symbolic and concrete EVM bytecode execution framework"
+    <> footer "See https://hevm.dev for more information"
+    )
+
   case cmd of
-    Version {} ->putStrLn getFullVersion
-    Symbolic {} -> do
-      root <- getRoot cmd
-      withCurrentDirectory root $ runEnv env $ assert cmd
-    Equivalence {} -> runEnv env $ equivalence cmd
-    Exec {} -> runEnv env $ launchExec cmd
-    Test {} -> do
-      root <- getRoot cmd
-      solver <- getSolver cmd
+    Symbolic cFileOpts symbOpts cExecOpts cOpts -> do
+      env <- makeEnv cOpts
+      root <- getRoot cOpts
+      withCurrentDirectory root $ runEnv env $ assert cFileOpts symbOpts cExecOpts cOpts
+    Equal eqOpts cOpts -> do
+      env <- makeEnv cOpts
+      runEnv env $ equivalence eqOpts cOpts
+    Test testOpts cOpts -> do
+      env <- makeEnv cOpts
+      root <- getRoot cOpts
+      solver <- getSolver cOpts.solver
       cores <- liftIO $ unsafeInto <$> getNumProcessors
-      let solverCount = fromMaybe cores cmd.numSolvers
-      runEnv env $ withSolvers solver solverCount (fromMaybe 1 cmd.solverThreads) cmd.smttimeout $ \solvers -> do
-        buildOut <- readBuildOutput root (getProjectType cmd)
+      let solverCount = fromMaybe cores cOpts.numSolvers
+      runEnv env $ withSolvers solver solverCount cOpts.solverThreads (Just cOpts.smttimeout) $ \solvers -> do
+        buildOut <- readBuildOutput root testOpts.projectType
         case buildOut of
           Left e -> liftIO $ do
             putStrLn $ "Error: " <> e
             exitFailure
           Right out -> do
             -- TODO: which functions here actually require a BuildOutput, and which can take it as a Maybe?
-            testOpts <- liftIO $ unitTestOptions cmd solvers (Just out)
-            res <- unitTest testOpts out.contracts
+            unitTestOpts <- liftIO $ unitTestOptions testOpts cOpts solvers (Just out)
+            res <- unitTest unitTestOpts out.contracts
             liftIO $ unless (uncurry (&&) res) exitFailure
+    Exec cFileOpts execOpts cExecOpts cOpts-> do
+      env <- makeEnv cOpts
+      runEnv env $ launchExec cFileOpts execOpts cExecOpts cOpts
+    Version {} ->putStrLn getFullVersion
+  where
+    makeEnv :: CommonOptions -> IO Env
+    makeEnv cOpts = do
+      when (cOpts.maxBufSize > 64) $ do
+        putStrLn "Error: maxBufSize must be less than or equal to 64. That limits buffers to a size of 2^64, which is more than enough for practical purposes"
+        exitFailure
+      when (cOpts.maxBufSize < 0) $ do
+        putStrLn "Error: maxBufSize must be at least 0. Negative values do not make sense. A value of zero means at most 1 byte long buffers"
+        exitFailure
+      pure Env { config = defaultConfig
+        { dumpQueries = cOpts.smtdebug
+        , debug = cOpts.debug
+        , dumpEndStates = cOpts.debug
+        , dumpExprs = cOpts.debug
+        , numCexFuzz = cOpts.numCexFuzz
+        , dumpTrace = cOpts.trace
+        , decomposeStorage = Prelude.not cOpts.noDecompose
+        , maxBranch = cOpts.maxBranch
+        , promiseNoReent = cOpts.promiseNoReent
+        , maxBufSize = cOpts.maxBufSize
+        , verb = cOpts.verb
+        } }
+
 
 getCode :: Maybe String -> Maybe ByteString -> IO (Maybe ByteString)
 getCode fname code = do
@@ -287,17 +366,17 @@ getCode fname code = do
       result <- try (BS.readFile f) :: IO (Either IOException BS.ByteString)
       case result of
         Left e -> do
-          putStrLn $ "Error reading file: " <> (show e)
+          putStrLn $ "Error reading file: " <> show e
           exitFailure
         Right content -> do
           pure $ Just $ strip (BS.toStrict content)
   where
     strip = BC.filter (\c -> c /= ' ' && c /= '\n' && c /= '\r' && c /= '\t' && c /= '"')
 
-equivalence :: App m => Command Options.Unwrapped -> m ()
-equivalence cmd = do
-  bytecodeA' <- liftIO $ getCode cmd.codeAFile cmd.codeA
-  bytecodeB' <- liftIO $ getCode cmd.codeBFile cmd.codeB
+equivalence :: App m => EqOptions -> CommonOptions -> m ()
+equivalence eqOpts cOpts = do
+  bytecodeA' <- liftIO $ getCode eqOpts.codeAFile eqOpts.codeA
+  bytecodeB' <- liftIO $ getCode eqOpts.codeBFile eqOpts.codeB
   let bytecodeA = decipher bytecodeA'
   let bytecodeB = decipher bytecodeB'
   when (isNothing bytecodeA) $ liftIO $ do
@@ -307,17 +386,17 @@ equivalence cmd = do
     putStrLn "Error: invalid or no bytecode for program B. Provide a valid one with --code-b or --code-b-file"
     exitFailure
   let veriOpts = VeriOpts { simp = True
-                          , maxIter = parseMaxIters cmd.maxIterations
-                          , askSmtIters = cmd.askSmtIterations
-                          , loopHeuristic = cmd.loopDetectionHeuristic
+                          , maxIter = parseMaxIters cOpts.maxIterations
+                          , askSmtIters = cOpts.askSmtIterations
+                          , loopHeuristic = cOpts.loopDetectionHeuristic
                           , rpcInfo = Nothing
                           }
-  calldata <- buildCalldata cmd
-  solver <- liftIO $ getSolver cmd
+  calldata <- buildCalldata cOpts eqOpts.sig eqOpts.arg
+  solver <- liftIO $ getSolver cOpts.solver
   cores <- liftIO $ unsafeInto <$> getNumProcessors
-  let solverCount = fromMaybe cores cmd.numSolvers
-  withSolvers solver solverCount (fromMaybe 1 cmd.solverThreads) cmd.smttimeout $ \s -> do
-    (res, e) <- equivalenceCheck s (fromJust bytecodeA) (fromJust bytecodeB) veriOpts calldata cmd.create
+  let solverCount = fromMaybe cores cOpts.numSolvers
+  withSolvers solver solverCount cOpts.solverThreads (Just cOpts.smttimeout) $ \s -> do
+    (res, e) <- equivalenceCheck s (fromJust bytecodeA) (fromJust bytecodeB) veriOpts calldata eqOpts.create
     liftIO $ case (any isCex res, any Expr.isPartial e || any isUnknown res) of
       (False, False) -> putStrLn "   \x1b[32m[PASS]\x1b[0m Contracts behave equivalently"
       (True, _)      -> putStrLn "   \x1b[31m[FAIL]\x1b[0m Contracts do not behave equivalently"
@@ -337,45 +416,38 @@ equivalence cmd = do
   where
     decipher = maybe Nothing (hexByteString . strip0x)
 
-getSolver :: Command Options.Unwrapped -> IO Solver
-getSolver cmd = case cmd.solver of
-                  Nothing -> pure Z3
-                  Just s -> case T.unpack s of
-                              "z3" -> pure Z3
-                              "cvc5" -> pure CVC5
-                              "bitwuzla" -> pure Bitwuzla
-                              input -> do
-                                putStrLn $ "unrecognised solver: " <> input
-                                exitFailure
-
-getSrcInfo :: App m => Command Options.Unwrapped -> m DappInfo
-getSrcInfo cmd = do
-  root <- liftIO $ getRoot cmd
+getSolver :: Text -> IO Solver
+getSolver s = case T.unpack s of
+  "z3" -> pure Z3
+  "cvc5" -> pure CVC5
+  "bitwuzla" -> pure Bitwuzla
+  input -> do
+    putStrLn $ "unrecognised solver: " <> input
+    exitFailure
+
+getSrcInfo :: App m => ExecOptions -> CommonOptions -> m DappInfo
+getSrcInfo execOpts cOpts = do
+  root <- liftIO $ getRoot cOpts
   conf <- readConfig
   liftIO $ withCurrentDirectory root $ do
-    outExists <- doesDirectoryExist (root </> "out")
+    outExists <- doesDirectoryExist (root System.FilePath.</> "out")
     if outExists
     then do
-      buildOutput <- runEnv Env {config = conf} $ readBuildOutput root (getProjectType cmd)
+      buildOutput <- runEnv Env {config = conf} $ readBuildOutput root execOpts.projectType
       case buildOutput of
         Left _ -> pure emptyDapp
         Right o -> pure $ dappInfo root o
     else pure emptyDapp
 
-getProjectType :: Command Options.Unwrapped -> ProjectType
-getProjectType cmd = fromMaybe Foundry cmd.projectType
-
-getRoot :: Command Options.Unwrapped -> IO FilePath
-getRoot cmd = maybe getCurrentDirectory makeAbsolute (cmd.root)
+getRoot :: CommonOptions -> IO FilePath
+getRoot cmd = maybe getCurrentDirectory makeAbsolute cmd.root
 
-parseMaxIters :: Maybe Integer -> Maybe Integer
-parseMaxIters i = if num < 0 then Nothing else Just num
-  where
-    num = fromMaybe (5::Integer) i
+parseMaxIters :: Integer -> Maybe Integer
+parseMaxIters num = if num < 0 then Nothing else Just num
 
 -- | Builds a buffer representing calldata based on the given cli arguments
-buildCalldata :: App m => Command Options.Unwrapped -> m (Expr Buf, [Prop])
-buildCalldata cmd = case (cmd.calldata, cmd.sig) of
+buildCalldata :: App m => CommonOptions -> Maybe Text -> [String] -> m (Expr Buf, [Prop])
+buildCalldata cOpts sig arg = case (cOpts.calldata, sig) of
   -- fully abstract calldata
   (Nothing, Nothing) -> mkCalldata Nothing []
   -- fully concrete calldata
@@ -388,7 +460,7 @@ buildCalldata cmd = case (cmd.calldata, cmd.sig) of
   -- calldata according to given abi with possible specializations from the `arg` list
   (Nothing, Just sig') -> do
     method' <- liftIO $ functionAbi sig'
-    mkCalldata (Just (Sig method'.methodSignature (snd <$> method'.inputs))) cmd.arg
+    mkCalldata (Just (Sig method'.methodSignature (snd <$> method'.inputs))) arg
   -- both args provided
   (_, _) -> liftIO $ do
     putStrLn "incompatible options provided: --calldata and --sig"
@@ -396,28 +468,35 @@ buildCalldata cmd = case (cmd.calldata, cmd.sig) of
 
 
 -- If function signatures are known, they should always be given for best results.
-assert :: App m => Command Options.Unwrapped -> m ()
-assert cmd = do
-  let block'  = maybe Fetch.Latest Fetch.BlockNumber cmd.block
-      rpcinfo = (,) block' <$> cmd.rpc
-  calldata <- buildCalldata cmd
-  preState <- liftIO $ symvmFromCommand cmd calldata
-  let errCodes = fromMaybe defaultPanicCodes cmd.assertions
+assert :: App m => CommonFileOptions -> SymbolicOptions -> CommonExecOptions -> CommonOptions -> m ()
+assert cFileOpts sOpts cExecOpts cOpts = do
+  let block' = maybe Fetch.Latest Fetch.BlockNumber cExecOpts.block
+      rpcinfo = (,) block' <$> cExecOpts.rpc
+  calldata <- buildCalldata cOpts sOpts.sig sOpts.arg
+  preState <- liftIO $ symvmFromCommand cExecOpts sOpts cFileOpts calldata
+  errCodes <- case sOpts.assertions of
+    Nothing -> pure defaultPanicCodes
+    Just s -> case (mapM readMaybe $ splitOn "," s) of
+      Nothing -> liftIO $ do
+        putStrLn $ "Error: invalid assertion codes: " <> s
+        exitFailure
+      Just codes -> pure codes
+  when (cOpts.verb > 0) $ liftIO $ putStrLn $ "Using assertion code(s): " <> intercalate "," (map show errCodes)
   cores <- liftIO $ unsafeInto <$> getNumProcessors
-  let solverCount = fromMaybe cores cmd.numSolvers
-  solver <- liftIO $ getSolver cmd
-  withSolvers solver solverCount (fromMaybe 1 cmd.solverThreads) cmd.smttimeout $ \solvers -> do
+  let solverCount = fromMaybe cores cOpts.numSolvers
+  solver <- liftIO $ getSolver cOpts.solver
+  withSolvers solver solverCount cOpts.solverThreads (Just cOpts.smttimeout) $ \solvers -> do
     let veriOpts = VeriOpts { simp = True
-                        , maxIter = parseMaxIters cmd.maxIterations
-                        , askSmtIters = cmd.askSmtIterations
-                        , loopHeuristic = cmd.loopDetectionHeuristic
+                        , maxIter = parseMaxIters cOpts.maxIterations
+                        , askSmtIters = cOpts.askSmtIterations
+                        , loopHeuristic = cOpts.loopDetectionHeuristic
                         , rpcInfo = rpcinfo
     }
     (expr, res) <- verify solvers veriOpts preState (Just $ checkAssertions errCodes)
     case res of
       [Qed _] -> do
         liftIO $ putStrLn "\nQED: No reachable property violations discovered\n"
-        showExtras solvers cmd calldata expr
+        showExtras solvers sOpts calldata expr
       _ -> do
         let cexs = snd <$> mapMaybe getCex res
             smtUnknowns = mapMaybe getUnknown res
@@ -436,22 +515,22 @@ assert cmd = do
                  , ""
                  ] <> fmap (formatExpr) smtUnknowns
         liftIO $ T.putStrLn $ T.unlines (counterexamples <> unknowns)
-        showExtras solvers cmd calldata expr
+        showExtras solvers sOpts calldata expr
         liftIO exitFailure
 
-showExtras :: App m => SolverGroup -> Command Options.Unwrapped -> (Expr Buf, [Prop]) -> Expr End -> m ()
-showExtras solvers cmd calldata expr = do
-  when cmd.showTree $ liftIO $ do
+showExtras :: App m => SolverGroup ->SymbolicOptions -> (Expr Buf, [Prop]) -> Expr End -> m ()
+showExtras solvers sOpts calldata expr = do
+  when sOpts.showTree $ liftIO $ do
     putStrLn "=== Expression ===\n"
     T.putStrLn $ formatExpr expr
     putStrLn ""
-  when cmd.showReachableTree $ do
+  when sOpts.showReachableTree $ do
     reached <- reachable solvers expr
     liftIO $ do
       putStrLn "=== Reachable Expression ===\n"
       T.putStrLn (formatExpr . snd $ reached)
       putStrLn ""
-  when cmd.getModels $ do
+  when sOpts.getModels $ do
     liftIO $ putStrLn $ "=== Models for " <> show (Expr.numBranches expr) <> " branches ==="
     ms <- produceModels solvers expr
     liftIO $ forM_ ms (showModel (fst calldata))
@@ -462,13 +541,13 @@ isTestOrLib file = T.isSuffixOf ".t.sol" file || areAnyPrefixOf ["src/test/", "s
 areAnyPrefixOf :: [Text] -> Text -> Bool
 areAnyPrefixOf prefixes t = any (flip T.isPrefixOf t) prefixes
 
-launchExec :: App m => Command Options.Unwrapped -> m ()
-launchExec cmd = do
-  dapp <- getSrcInfo cmd
-  vm <- liftIO $ vmFromCommand cmd
+launchExec :: App m => CommonFileOptions -> ExecOptions -> CommonExecOptions -> CommonOptions -> m ()
+launchExec cFileOpts execOpts cExecOpts cOpts = do
+  dapp <- getSrcInfo execOpts cOpts
+  vm <- liftIO $ vmFromCommand cOpts cExecOpts cFileOpts execOpts
   let
-    block = maybe Fetch.Latest Fetch.BlockNumber cmd.block
-    rpcinfo = (,) block <$> cmd.rpc
+    block = maybe Fetch.Latest Fetch.BlockNumber cExecOpts.block
+    rpcinfo = (,) block <$> cExecOpts.rpc
 
   -- TODO: we shouldn't need solvers to execute this code
   withSolvers Z3 0 1 Nothing $ \solvers -> do
@@ -493,9 +572,9 @@ launchExec cmd = do
         internalError "no EVM result"
 
 -- | Creates a (concrete) VM from command line options
-vmFromCommand :: Command Options.Unwrapped -> IO (VM Concrete RealWorld)
-vmFromCommand cmd = do
-  (miner,ts,baseFee,blockNum,prevRan) <- case cmd.rpc of
+vmFromCommand :: CommonOptions -> CommonExecOptions -> CommonFileOptions -> ExecOptions -> IO (VM Concrete RealWorld)
+vmFromCommand cOpts cExecOpts cFileOpts execOpts= do
+  (miner,ts,baseFee,blockNum,prevRan) <- case cExecOpts.rpc of
     Nothing -> pure (LitAddr 0,Lit 0,0,0,0)
     Just url -> Fetch.fetchBlockFrom block url >>= \case
       Nothing -> do
@@ -508,11 +587,11 @@ vmFromCommand cmd = do
                              , prevRandao
                              )
 
-  codeWrapped <- getCode cmd.codeFile cmd.code
-  contract <- case (cmd.rpc, cmd.address, codeWrapped) of
+  codeWrapped <- getCode cFileOpts.codeFile cFileOpts.code
+  contract <- case (cExecOpts.rpc, cExecOpts.address, codeWrapped) of
     (Just url, Just addr', Just c) -> do
       let code = hexByteString $ strip0x c
-      if (isNothing code) then do
+      if isNothing code then do
         putStrLn $ "Error, invalid code: " <> show c
         exitFailure
       else
@@ -559,16 +638,16 @@ vmFromCommand cmd = do
     pure $ EVM.Transaction.initTx vm
   where
         bsCallData = bytes (.calldata) (pure "")
-        block   = maybe Fetch.Latest Fetch.BlockNumber cmd.block
-        value   = word (.value) 0
+        block   = maybe Fetch.Latest Fetch.BlockNumber cExecOpts.block
+        val     = word (.value) 0
         caller  = addr (.caller) (LitAddr 0)
         origin  = addr (.origin) (LitAddr 0)
         calldata = ConcreteBuf $ fromJust bsCallData
         decipher = hexByteString . strip0x
-        mkCode bs = if cmd.create
+        mkCode bs = if execOpts.create
                     then InitCode bs mempty
                     else RuntimeCode (ConcreteRuntimeCode bs)
-        address = if cmd.create
+        address = if execOpts.create
                   then addr (.address) (Concrete.createAddress (fromJust $ maybeLitAddrSimp origin) (W64 $ word64 (.nonce) 0))
                   else addr (.address) (LitAddr 0xacab)
 
@@ -576,7 +655,7 @@ vmFromCommand cmd = do
           { contract       = c
           , otherContracts = []
           , calldata       = (calldata, [])
-          , value          = Lit value
+          , value          = Lit val
           , address        = address
           , caller         = caller
           , origin         = origin
@@ -593,21 +672,21 @@ vmFromCommand cmd = do
           , prevRandao     = word (.prevRandao) prevRan
           , schedule       = feeSchedule
           , chainId        = word (.chainid) 1
-          , create         = (.create) cmd
+          , create         = (.create) execOpts
           , baseState      = EmptyBase
           , txAccessList   = mempty -- TODO: support me soon
           , allowFFI       = False
           , freshAddresses = 0
           , beaconRoot     = 0
           }
-        word f def = fromMaybe def (f cmd)
-        word64 f def = fromMaybe def (f cmd)
-        addr f def = maybe def LitAddr (f cmd)
-        bytes f def = maybe def decipher (f cmd)
-
-symvmFromCommand :: Command Options.Unwrapped -> (Expr Buf, [Prop]) -> IO (VM EVM.Types.Symbolic RealWorld)
-symvmFromCommand cmd calldata = do
-  (miner,blockNum,baseFee,prevRan) <- case cmd.rpc of
+        word f def = fromMaybe def (f cExecOpts)
+        word64 f def = fromMaybe def (f cExecOpts)
+        addr f def = maybe def LitAddr (f cExecOpts)
+        bytes f def = maybe def decipher (f cOpts)
+
+symvmFromCommand :: CommonExecOptions -> SymbolicOptions -> CommonFileOptions -> (Expr Buf, [Prop]) -> IO (VM EVM.Types.Symbolic RealWorld)
+symvmFromCommand cExecOpts sOpts cFileOpts calldata = do
+  (miner,blockNum,baseFee,prevRan) <- case cExecOpts.rpc of
     Nothing -> pure (SymAddr "miner",0,0,0)
     Just url -> Fetch.fetchBlockFrom block url >>= \case
       Nothing -> do
@@ -620,13 +699,13 @@ symvmFromCommand cmd calldata = do
                              )
 
   let
-    caller = maybe (SymAddr "caller") LitAddr cmd.caller
-    ts = maybe Timestamp Lit cmd.timestamp
-    callvalue = maybe TxValue Lit cmd.value
-    storageBase = maybe AbstractBase parseInitialStorage (cmd.initialStorage)
+    caller = maybe (SymAddr "caller") LitAddr cExecOpts.caller
+    ts = maybe Timestamp Lit cExecOpts.timestamp
+    callvalue = maybe TxValue Lit cExecOpts.value
+    storageBase = maybe AbstractBase parseInitialStorage (sOpts.initialStorage)
 
-  codeWrapped <- getCode cmd.codeFile cmd.code
-  contract <- case (cmd.rpc, cmd.address, codeWrapped) of
+  codeWrapped <- getCode cFileOpts.codeFile cFileOpts.code
+  contract <- case (cExecOpts.rpc, cExecOpts.address, codeWrapped) of
     (Just url, Just addr', _) ->
       Fetch.fetchContractFrom block url addr' >>= \case
         Nothing -> do
@@ -666,9 +745,9 @@ symvmFromCommand cmd calldata = do
 
   where
     decipher = hexByteString . strip0x
-    block = maybe Fetch.Latest Fetch.BlockNumber cmd.block
+    block = maybe Fetch.Latest Fetch.BlockNumber cExecOpts.block
     origin = eaddr (.origin) (SymAddr "origin")
-    mkCode bs = if cmd.create
+    mkCode bs = if sOpts.create
                    then InitCode bs mempty
                    else RuntimeCode (ConcreteRuntimeCode bs)
     address = eaddr (.address) (SymAddr "entrypoint")
@@ -693,48 +772,43 @@ symvmFromCommand cmd calldata = do
       , prevRandao     = word (.prevRandao) prevRan
       , schedule       = feeSchedule
       , chainId        = word (.chainid) 1
-      , create         = (.create) cmd
+      , create         = (.create) sOpts
       , baseState      = baseState
       , txAccessList   = mempty
       , allowFFI       = False
       , freshAddresses = 0
       , beaconRoot     = 0
       }
-    word f def = fromMaybe def (f cmd)
-    word64 f def = fromMaybe def (f cmd)
-    eaddr f def = maybe def LitAddr (f cmd)
+    word f def = fromMaybe def (f cExecOpts)
+    word64 f def = fromMaybe def (f cExecOpts)
+    eaddr f def = maybe def LitAddr (f cExecOpts)
 
-unitTestOptions :: Command Options.Unwrapped -> SolverGroup -> Maybe BuildOutput -> IO (UnitTestOptions RealWorld)
-unitTestOptions cmd solvers buildOutput = do
-  root <- getRoot cmd
+unitTestOptions :: TestOptions -> CommonOptions -> SolverGroup -> Maybe BuildOutput -> IO (UnitTestOptions RealWorld)
+unitTestOptions testOpts cOpts solvers buildOutput = do
+  root <- getRoot cOpts
   let srcInfo = maybe emptyDapp (dappInfo root) buildOutput
-
-  let rpcinfo = case (cmd.number, cmd.rpc) of
+  let rpcinfo = case (testOpts.number, testOpts.rpc) of
           (Just block, Just url) -> Just (Fetch.BlockNumber block, url)
           (Nothing, Just url) -> Just (Fetch.Latest, url)
           _ -> Nothing
   params <- paramsFromRpc rpcinfo
-
-  let
-    testn = params.number
-    block' = if 0 == testn
+  let testn = params.number
+      block' = if 0 == testn
        then Fetch.Latest
        else Fetch.BlockNumber testn
-
   pure UnitTestOptions
     { solvers = solvers
-    , rpcInfo = case cmd.rpc of
+    , rpcInfo = case testOpts.rpc of
          Just url -> Just (block', url)
          Nothing  -> Nothing
-    , maxIter = parseMaxIters cmd.maxIterations
-    , askSmtIters = cmd.askSmtIterations
-    , smtTimeout = cmd.smttimeout
-    , solver = cmd.solver
-    , match = T.pack $ fromMaybe ".*" cmd.match
+    , maxIter = parseMaxIters cOpts.maxIterations
+    , askSmtIters = cOpts.askSmtIterations
+    , smtTimeout = Just cOpts.smttimeout
+    , match = T.pack $ fromMaybe ".*" testOpts.match
     , testParams = params
     , dapp = srcInfo
-    , ffiAllowed = cmd.ffi
-    , checkFailBit = (fromMaybe Forge cmd.assertionType) == DSTest
+    , ffiAllowed = testOpts.ffi
+    , checkFailBit = cOpts.assertionType == DSTest
     }
 parseInitialStorage :: InitialStorage -> BaseState
 parseInitialStorage Empty = EmptyBase
diff --git a/hevm.cabal b/hevm.cabal
index 2430b8349..932a51685 100644
--- a/hevm.cabal
+++ b/hevm.cabal
@@ -12,7 +12,7 @@ homepage:
 license:
   AGPL-3.0-only
 author:
-  dxo, Martin Lundfall, Mikael Brockman
+  dxo, Martin Lundfall, Mikael Brockman, Martin Blicha, Zoe Paraskevopoulou, Mate Soos
 maintainer:
   git@d-xo.org
 category:
@@ -89,6 +89,7 @@ common shared
 
 library
   import: shared
+  default-language: GHC2021
   exposed-modules:
     EVM,
     EVM.ABI,
@@ -190,6 +191,7 @@ library
 
 executable hevm
   import: shared
+  default-language: GHC2021
   hs-source-dirs:
     cli
   main-is:
@@ -203,21 +205,23 @@ executable hevm
     base,
     bytestring,
     data-dword,
-    directory,
+    directory                         >= 1.3.6 && < 1.4,
     filepath,
     hevm,
     optparse-generic,
+    optparse-applicative              >= 0.18.0.0 && < 0.20.0.0,
     text,
     optics-core,
-    githash,
+    githash                           >= 0.1.5 && < 0.2,
     witch,
     unliftio-core,
-    with-utf8,
+    split,
 
 --- Test Helpers ---
 
 common test-base
   import: shared
+  default-language: GHC2021
   hs-source-dirs:
     test
   other-modules:
@@ -254,6 +258,7 @@ common test-base
 
 library test-utils
   import: test-base
+  default-language: GHC2021
   exposed-modules:
     EVM.Test.Utils
     EVM.Test.Tracing
@@ -261,6 +266,7 @@ library test-utils
 
 common test-common
   import: test-base
+  default-language: GHC2021
   if flag(devel)
     ghc-options: -threaded -with-rtsopts=-N
   build-depends:
@@ -274,6 +280,7 @@ common test-common
 
 test-suite test
   import: test-common
+  default-language: GHC2021
   type:
     exitcode-stdio-1.0
   main-is:
@@ -291,6 +298,7 @@ test-suite test
 -- suite to make it easy to skip them when running nix-build
 test-suite rpc-tests
   import: test-common
+  default-language: GHC2021
   type:
     exitcode-stdio-1.0
   main-is:
@@ -298,15 +306,36 @@ test-suite rpc-tests
 
 test-suite ethereum-tests
   import: test-common
+  default-language: GHC2021
   type:
     exitcode-stdio-1.0
   main-is:
     BlockchainTests.hs
 
+test-suite cli-test
+  type:
+    exitcode-stdio-1.0
+  default-language: GHC2021
+  hs-source-dirs:
+    test
+  main-is:
+    clitest.hs
+  build-depends:
+    base,
+    hevm,
+    hspec,
+    process,
+    text,
+    bytestring,
+    filepath,
+    split,
+    here,
+
 --- Benchmarks ---
 
 benchmark bench
   import: shared
+  default-language: GHC2021
   type:
     exitcode-stdio-1.0
   main-is:
diff --git a/src/EVM/Solidity.hs b/src/EVM/Solidity.hs
index b2d98684c..4a9cdc379 100644
--- a/src/EVM/Solidity.hs
+++ b/src/EVM/Solidity.hs
@@ -399,8 +399,9 @@ functionAbi :: Text -> IO Method
 functionAbi f = do
   json <- solc Solidity ("contract ABI { function " <> f <> " public {}}")
   let (Contracts sol, _, _) = fromMaybe
-                                (internalError . T.unpack $ "unable to parse solc output:\n" <> json)
-                                (readStdJSON json)
+        (internalError . T.unpack $ "while trying to parse function signature `"
+          <> f <> "`, unable to parse solc output:\n" <> json)
+        (readStdJSON json)
   case Map.toList (fromJust (Map.lookup "hevm.sol:ABI" sol)).abiMap of
     [(_,b)] -> pure b
     _ -> internalError "unexpected abi format"
diff --git a/src/EVM/UnitTest.hs b/src/EVM/UnitTest.hs
index 96a03c3fd..3fcf443a3 100644
--- a/src/EVM/UnitTest.hs
+++ b/src/EVM/UnitTest.hs
@@ -51,7 +51,6 @@ data UnitTestOptions s = UnitTestOptions
   , maxIter     :: Maybe Integer
   , askSmtIters :: Integer
   , smtTimeout  :: Maybe Natural
-  , solver      :: Maybe Text
   , match       :: Text
   , dapp        :: DappInfo
   , testParams  :: TestVMParams
diff --git a/test/EVM/Test/Utils.hs b/test/EVM/Test/Utils.hs
index f5b0822ee..f3a68b0f1 100644
--- a/test/EVM/Test/Utils.hs
+++ b/test/EVM/Test/Utils.hs
@@ -58,7 +58,6 @@ testOpts solvers root buildOutput match maxIter allowFFI rpcinfo = do
     , maxIter = maxIter
     , askSmtIters = 1
     , smtTimeout = Nothing
-    , solver = Nothing
     , match = match
     , testParams = params
     , dapp = srcInfo
diff --git a/test/clitest.hs b/test/clitest.hs
new file mode 100644
index 000000000..f0f40cf78
--- /dev/null
+++ b/test/clitest.hs
@@ -0,0 +1,119 @@
+{-# LANGUAGE QuasiQuotes #-}
+
+module Main where
+
+{-|
+Description : CLI tests
+
+This module contains simple CLI test cases to make sure we don't accidentally
+break the hevm CLI interface.
+
+-}
+
+import Test.Hspec
+import System.Process (readProcess, readProcessWithExitCode)
+import System.FilePath ((</>))
+import System.Exit (ExitCode(..))
+import Data.List.Split (splitOn)
+import Data.Text qualified as T
+import Data.String.Here
+
+import EVM.Solidity
+import EVM.Effects
+import EVM.Types
+
+
+main :: IO ()
+main = do
+  hspec $
+    describe "CLI" $ do
+      it "hevm help works" $ do
+        (exitCode, stdout, stderr) <- readProcessWithExitCode "cabal" ["run", "exe:hevm", "--", "--help"] ""
+        stdout `shouldContain` "Usage: hevm"
+        stdout `shouldContain` "test"
+        stdout `shouldContain` "equivalence"
+        stdout `shouldContain` "symbolic"
+        stdout `shouldContain` "exec"
+        stdout `shouldContain` "version"
+
+      it "hevm symbolic tutorial works -- FAIL" $ do
+        Just symbBin <- runApp $ solcRuntime (T.pack "MyContract") (T.pack [i|
+          contract MyContract {
+            function simple_symb() public pure {
+              uint i;
+              i = 1;
+              assert(i == 2);
+            }
+          }
+        |])
+        let symbHex = bsToHex symbBin
+        (exitCode, stdout, stderr) <- readProcessWithExitCode "cabal" ["run", "exe:hevm", "--", "symbolic", "--code", symbHex] ""
+        stdout `shouldContain` "Discovered the following"
+        exitCode `shouldBe` ExitFailure 1
+
+        (exitCode, stdout, stderr) <- readProcessWithExitCode "cabal" ["run", "exe:hevm", "--", "symbolic", "--code", symbHex, "--sig", "nonexistent()"] ""
+        stdout `shouldContain` "QED"
+        exitCode `shouldBe` ExitSuccess
+
+      it "hevm equivalence tutorial works -- FAIL" $ do
+        let torun = splitOn " " "equivalence --code-a 60003560000260005260016000f3 --code-b 7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff60005260016000f3"
+        (exitCode, stdout, stderr) <- readProcessWithExitCode "cabal" (["run", "exe:hevm", "--" ] ++ torun) ""
+        stdout `shouldContain` "Not equivalent"
+        stdout `shouldContain` "FAIL"
+        exitCode `shouldBe` ExitFailure 1
+
+      it "hevm equivalence tutorial works -- PASS" $ do
+        Just a <- runApp $ solcRuntime (T.pack "MyContract") (T.pack [i|
+          contract MyContract {
+            mapping (address => uint) balances;
+            function my_adder(address recv, uint amt) public {
+              if (balances[recv] + amt >= 100) { revert(); }
+              balances[recv] += amt;
+            }
+          }
+        |])
+        let aHex = bsToHex a
+        Just b <- runApp $ solcRuntime (T.pack "MyContract") (T.pack [i|
+          contract MyContract {
+            mapping (address => uint) balances;
+            function my_adder(address recv, uint amt) public {
+              if (balances[recv] + amt >= 100) { revert(); }
+              balances[recv] += amt/2;
+              balances[recv] += amt/2;
+              if (amt % 2 != 0) balances[recv]++;
+            }
+          }
+        |])
+        let bHex = bsToHex b
+        (exitCode, stdout, stderr) <- readProcessWithExitCode "cabal" (["run", "exe:hevm", "--", "equivalence" , "--code-a", aHex, "--code-b", bHex ]) ""
+        stdout `shouldContain` "No discrepancies found"
+        stdout `shouldContain` "PASS"
+        exitCode `shouldBe` ExitSuccess
+
+      it "hevm concrete tutorial works" $ do
+        let torun = splitOn " " "exec --code 0x647175696e6550383480393834f3 --gas 0xff"
+        (exitCode, stdout, stderr) <- readProcessWithExitCode "cabal" (["run", "exe:hevm", "--" ] ++ torun) ""
+        stdout `shouldContain` "Return: 0x64"
+        exitCode `shouldBe` ExitSuccess
+
+      it "warning on zero address" $ do
+        Just c <- runApp $ solcRuntime (T.pack "C") (T.pack [i|
+           contract Target {
+             function get() external view returns (uint256) {
+                 return 55;
+             }
+           }
+           contract C {
+             Target mm;
+             function retFor() public returns (uint256) {
+                 Target target = Target(address(0));
+                 uint256 ret = target.get();
+                 assert(ret == 4);
+                 return ret;
+             }
+           }
+          |])
+        let hexStr = bsToHex c
+        (exitCode, stdout, stderr) <- readProcessWithExitCode "cabal" ["run", "exe:hevm", "--", "symbolic", "--code", hexStr] ""
+        stdout `shouldContain` "Warning: fetching contract at address 0"
+