msooseth · Oct 26, 2026 · Oct 26, 2026 · Oct 26, 2026 · Oct 26, 2026 · Oct 26, 2026
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -8,11 +8,50 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 ## [Unreleased]
 
 ## Added
+- A memory offset or size that depends on a subterm with at most
+  `--max-mem-arg-split` values (default 8), such as the length of a short dynamic
+  argument, forks the path on those values, each substituted into the state, so
+  memory stays concrete.
+- Dynamic arrays of static types (e.g. `uint16[]`) can be symbolic arguments, with
+  a symbolic length of at most `--max-dyn-size` elements, under the same caveat as
+  `bytes` and `string`. They used to stop the run with an internal error.
+- With `--check-static-branches`, a branch that simplification keeps both ways but
+  the solver decides is logged as a `static-missed` event in the progress log, with
+  its condition and path conditions under `--progress-exprs`, and counted per
+  location in the summary.
+- Bounds from path conditions carry through `c + x`, `c - x` and `~x`, also when
+  they wrap past 2^256 as signed range checks do, and through small signed values
+  such as `-k + y % n`. The simplifier drops `m & x` to 0 when the bound of `x`
+  leaves it none of the bits of `m`, and to `x` when it leaves only bits of `m`, and
+  props whose bounds contradict, or exclude every value a term can have, such as a
+  sign-extended value, simplify to false.
+- The simplifier folds `c + ~x` to `(c - 1) - x` and `c - ~x` to `(c + 1) + x`.
+- The simplifier folds arithmetic, comparisons and bit operations through nested
+  ITEs whose leaves are literals, as merged branches build them, up to 128 leaves.
+- `test/scripts/fuzz-coverage.sh` reports which source lines a fuzz run never
+  reaches, using HPC.
+- Abstract arithmetic lemmas for dividends a literal apart over one divisor,
+  `(x-k)/z <= x/z <= (x-k)/z + k`, as in a `ceilDiv` next to a round-down, and
+  for `(r + c*q)/c == q` when `r < c`.
+- Abstract arithmetic lemmas relating `a/c` to `x` when `a` is bounded by `c*x`,
+  bounding `ceilDiv(c1*x, c2)` by `x/(c2/c1)` when `c1` divides `c2`, and bounding
+  remainders: `a%b <= a` and `a%b < b`.
+- The simplifier drops an `ITE c t k` whose literal `k` is what `t` is when `c` is 0,
+  such as the product a short-circuited overflow check leaves after a merge.
+- The simplifier splits `b ** ITE c x y` with literal `b`, `x` and `y` into two
+  constants, and folds `x < x - x % c`, also masked to `uintN`, to false.
+- A memory offset or size that depends on a merged condition, such as an array
+  length picked by a ternary, forks on that condition, so memory stays concrete.
+- `test` takes `--run-log FILE`, appending a line when each test starts and ends,
+  and `--yul-verbosity N`. Tests time out after 10 minutes by default.
+- The progress log gives the source location of forks and of the locations in
+  its summaries, when there is debug info.
 - Invariant testing: `hevm test` checks `invariant_` functions after every
   sequence of at most `--invariant-depth` calls to the target contracts, with
   symbolic arguments, callers and timestamps. States reached before are not
   explored again. Assertion failures in the calls fail the test, and minimal
   proxies (EIP-1167 clones) can be targets.
+- An invariant testing tutorial in the docs.
 - A worked example in the docs: finding the Abracadabra `cook()` exploit on a mainnet fork.
 - `--smt-branch-timeout`, 20 seconds by default, for the queries that decide which
   branches to explore.
@@ -128,6 +167,42 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
   writes of zero.
 
 ## Changed
+- A word subterm that a solver query uses more than once is defined once with
+  `define-fun` and referred to by name, instead of being written out at every use.
+- `mapExpr` visits each hash-consed node once per call, and the simplifier's
+  searches for subterms fold over each node once, instead of over every path to it.
+  So do common subexpression elimination and the collection of variables, buffers,
+  storage reads and keccak values before a query is encoded.
+- Deciding a branch without the solver reuses the simplified path conditions
+  of the earlier branches on the path, kept in the new `VM` field
+  `simpConstraints`, and first tries the branch condition alone, which
+  simplification can decide where it cannot with the path conditions.
+- State merging also merges if/else branches and ternaries, where the two
+  sides meet after the jump target, and follows the branches inside a merged
+  side that its own condition decides, such as the overflow check of `a - b`
+  under `a > b`. A branch reached again in a loop is not merged, so the loop
+  bound applies. `MergeState` has `msAssume` instead of `msRemainingBudget`.
+- Invariant testing merges the states after a call that differ only in their
+  path conditions into one state with the disjunction of those conditions, and
+  drops the logs of earlier calls. The disjunction drops conditions whose
+  negation is the only difference between two of its parts.
+- Symbolic execution explores the newest pending path first, depth-first,
+  which keeps fewer paths pending.
+- The Solidity ASTs are no longer kept after reading the build output:
+  `SourceCache` has no `asts`, `DappInfo` no `astIdMap` and `astSrcMap`.
+- Invariant testing keeps only the states of feasible calls, checked by the
+  solver, and drops the states seen before as soon as they are reached. It keeps
+  the state after a call without that call's memory and traces.
+- The default number of solvers is at most half of the available memory divided
+  by `--smt-memory`, so that the solvers running at once fit in memory.
+- Solidity's overflow check of a multiplication by a literal, `y == 0 || (y * c) / y == c`,
+  also once simplification has distributed `y * c` or dropped `y == 0`,
+  simplifies to a bound on `y`, and the overflow checks of multiplications use bounds that hold
+  through comparisons with other bounded values.
+- Constant propagation substitutes any term that the props fix to a constant,
+  not only variables.
+- Invariant tests print the paths they only partially explored grouped by
+  source location, as `prove` tests do, instead of printing their expressions.
 - `EVM.SymExec` is split: concrete replay of counterexamples moves to
   `EVM.CexReplay`, and equivalence checking to `EVM.Equivalence`. Symbolic
   calldata (`EVM.SymExec.Calldata`) and counterexample models and printing
@@ -193,6 +268,24 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
   instead of simplifying an ITE of them.
 
 ## Fixed
+- An account whose balance is a term equal to 0, e.g. after a transfer of `x & 0`,
+  counted as non-empty, so `EXTCODEHASH` gave the hash of the empty code instead
+  of 0, and the account was not cleared at the end of the transaction.
+- A memory instruction with fewer stack items than it takes could fork on a merged
+  memory offset before underrunning the stack, so the path went on where it should
+  have halted.
+- `CREATE` and `CREATE2` compared a symbolic init code size with the maximum
+  structurally, so every symbolic size failed as too large and the path was
+  dropped. The size is now simplified and compared as a number, and one that stays
+  symbolic ends the path as partial.
+- Symbolic execution leaked memory: every trace kept the whole VM it was made
+  in, and memory size and loop visit counters kept the earlier frame states.
+- Memory snapshots at forks no longer copy the unused zeros of the memory buffer.
+- Source locations of contracts with immutables are found in Foundry projects.
+- Source locations are right after an incremental `forge build`, whose
+  build-infos number the source files independently.
+- `prank` and `startPrank` with a symbolic address, e.g. one picked from a list
+  by a symbolic index, explore each possible address instead of failing.
 - SMT queries skip assumptions between concrete keccak hashes, whose values
   are already known, avoiding unnecessary quadratic growth.
 - Constant propagation checks disequalities and disjunctions against the

diff --git a/cli/cli.hs b/cli/cli.hs
@@ -23,11 +23,9 @@ import Data.Text qualified as T
 import Data.Text.IO qualified as T
 import Data.Version (showVersion)
 import Data.Word (Word64)
-import GHC.Conc (getNumProcessors)
 import GitHash
 import Numeric.Natural (Natural)
 import Optics.Core ((&), set)
-import Witch (unsafeInto)
 import Options.Generic as OptionsGeneric
 import Options.Applicative as Options
 import Paths_hevm qualified as Paths
@@ -104,6 +102,7 @@ data CommonOptions = CommonOptions
   , promiseNoReent::Bool
   , maxBufSize    ::Int
   , maxWidth      ::Int
+  , maxMemArgSplit ::Int
   , maxDepth      ::Maybe Int
   , noSimplify    ::Bool
   , onlyDeployed  ::Bool
@@ -143,20 +142,21 @@ commonOptions = CommonOptions
   <*> (option auto $ long "smt-memory"      <> value defMemLimit <> help "Maximum memory limit for SMT solver in MB. Only available on Linux")
   <*> (switch $ long "smt-debug"            <> help "Print smt queries sent to the solver")
   <*> (optional $ strOption $ long "dump-unsolved" <> help "Dump unsolved SMT queries to this (relative) path")
-  <*> (optional $ option auto $ long "num-solvers" <> help "Number of solver instances to use (default: number of cpu cores)")
+  <*> (optional $ option auto $ long "num-solvers" <> help "Number of solver instances to use (default: number of cpu cores, at most half the available memory divided by --smt-memory)")
   <*> (option auto $ long "max-iterations"  <> showDefault <> value 5 <> help "Number of times we may revisit a particular branching point. For no bound, set -1")
   <*> (option auto $ long "max-concrete-iterations" <> showDefault <> value 10000 <> help "Number of times we may revisit a branching point whose condition is concrete, e.g. in a loop over fetched state. Gas is not tracked, so this stops loops that never end. 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 24 <> help "Maximum size of buffers such as calldata and returndata in exponents of 2 (default: 24, i.e. 16 MB, more than gas limits allow)")
   <*> (option auto $ long "max-width"      <> showDefault <> value 100 <> help "Max number of concrete values to explore when encountering a symbolic value. This is a form of branch width limitation per symbolic value")
+  <*> (option auto $ long "max-mem-arg-split" <> showDefault <> value 8 <> help "Max number of values of a subterm that a memory offset or size depends on, e.g. a short dynamic argument's length, to explore one path each with that value substituted, so memory stays concrete. 0 disables it")
   <*> (optional $ option auto $ long "max-depth" <> help "Limit maximum depth of branching during exploration (default: unlimited)")
   <*> (switch $ long "no-simplify" <> help "Don't perform simplification of expressions")
   <*> (switch $ long "only-deployed" <> help "When trying to resolve unknown addresses, only use addresses of deployed contracts")
   <*> (optional $ strOption $ long "cache-dir" <> help "Directory to save and load the RPC cache in (default: the user's cache directory, for runs at a fixed block)")
   <*> (switch $ long "no-rpc-cache" <> help "Don't save or load fetched state in the user's cache directory")
   <*> (switch $  long "no-early-abort" <> help "Keep exploring after the first counterexample, to find all of them. By default, exploration stops at the first one")
   <*> (option auto $ long "merge-max-budget" <> showDefault <> value 100 <> help "Max instructions for speculative merge exploration during path merging")
-  <*> (option auto $ long "max-dyn-size" <> showDefault <> value 64 <> help "Max byte length for concretized dynamic types (bytes, string) in symbolic arguments")
+  <*> (option auto $ long "max-dyn-size" <> showDefault <> value 64 <> help "Max length of dynamic symbolic arguments: bytes for bytes and string, elements for arrays")
   <*> (switch $  long "no-abstract-arith" <> help "Don't abstract symbolic multiplication and division as uninterpreted functions with sound lemmas; use native bitvector arithmetic instead")
   <*> (switch $ long "no-hash-cons" <> help "Don't hash-cons (share equal subterms of) the symbolic VM state during exploration")
   <*> (optional $ strOption $ long "progress-log" <> help "Write a JSONL log of interpreter and solver progress to this file (default with --verb 3: hevm-progress.jsonl)")
@@ -166,7 +166,7 @@ commonOptions = CommonOptions
   <*> (switch $ long "serve" <> help "Serve the progress of the run over HTTP on localhost, at /progress")
   <*> (option auto $ long "port" <> showDefault <> value defaultDebuggerPort <> help "Port for --interactive and --serve, 0 picks a free one")
   <*> (option auto $ long "interactive-snapshot-every" <> showDefault <> value snapshotInterval <> help "Steps between the debugger's snapshots: fewer make going back faster and use more memory")
-  <*> (switch $ long "check-static-branches" <> help "Internal check, slow: ask the solver to confirm every branch side that exploration drops by simplification alone")
+  <*> (switch $ long "check-static-branches" <> help "Slow: ask the solver about every branch that exploration decides by simplification alone. A dropped side that is reachable is an error; a side kept that the solver rules out is logged as a static-missed event in the progress log, and counted per location in its summary")
 
 data CommonExecOptions = CommonExecOptions
   { address       ::Maybe Addr
@@ -368,8 +368,7 @@ main = do
       env <- makeEnv cOpts
       root <- getRoot cOpts
       solver <- getSolver cOpts.solver
-      cores <- liftIO $ unsafeInto <$> getNumProcessors
-      let solverCount = fromMaybe cores cOpts.numSolvers
+      solverCount <- liftIO $ maybe (defaultSolverCount cOpts.smtMemory) pure cOpts.numSolvers
       runEnv env $ withProgress (progressOpts env cOpts) $ serving cOpts $ withSolvers solver solverCount (Just cOpts.smtTimeout) cOpts.smtMemory $ \solvers -> do
         buildOut <- readBuildOutput root testOpts.projectType
         case buildOut of
@@ -420,6 +419,7 @@ main = do
         , promiseNoReent = cOpts.promiseNoReent
         , maxBufSize = cOpts.maxBufSize
         , maxWidth = cOpts.maxWidth
+        , maxMemArgSplit = cOpts.maxMemArgSplit
         , maxDepth = cOpts.maxDepth
         , verb = cOpts.verb
         , simp = Prelude.not cOpts.noSimplify
@@ -483,8 +483,7 @@ equivalence eqOpts cOpts = do
                           }
   (calldata, _caveats) <- buildCalldata cOpts eqOpts.sig eqOpts.arg
   solver <- liftIO $ getSolver cOpts.solver
-  cores <- liftIO $ unsafeInto <$> getNumProcessors
-  let solverCount = fromMaybe cores cOpts.numSolvers
+  solverCount <- liftIO $ maybe (defaultSolverCount cOpts.smtMemory) pure cOpts.numSolvers
   withSolvers solver solverCount (Just cOpts.smtTimeout) cOpts.smtMemory $ \s -> do
     sess <- Fetch.mkSession cOpts.cacheDir Nothing
     eq <- equivalenceCheck s (Just sess) (fromJust bytecodeA) (fromJust bytecodeB) veriOpts calldata eqOpts.create
@@ -603,8 +602,7 @@ symbCheck cFileOpts sOpts cExecOpts cOpts = withRpcSession cOpts cExecOpts.rpc c
         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 cOpts.numSolvers
+  solverCount <- liftIO $ maybe (defaultSolverCount cOpts.smtMemory) pure cOpts.numSolvers
   solver <- liftIO $ getSolver cOpts.solver
   withSolvers solver solverCount (Just cOpts.smtTimeout) cOpts.smtMemory $ \solvers -> do
     let veriOpts = VeriOpts { iterConf = IterConfig {

diff --git a/doc/src/SUMMARY.md b/doc/src/SUMMARY.md
@@ -7,6 +7,7 @@
 # Tutorials
 
 - [Forge std-test tutorial](./std-test-tutorial.md)
+- [Invariant testing tutorial](./invariant-testing-tutorial.md)
 - [Equivalence checking tutorial](./equivalence-checking-tutorial.md)
 - [Symbolic execution tutorial](./symbolic-execution-tutorial.md)
 - [Example: Truebit exploit](./exploit-tutorial.md)