Merge pull request #268 from ethereum/propogate-constraints

SymExec: propogate constraints from vm to output expression
ethereum · Jun 1, 2023 · 886c11f · 886c11f
2 parents 7ba1d97 + 7aed063
commit 886c11f
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 1 deletion.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -10,6 +10,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 ## Fixed
 
 - hevm now gracefully handles missing `out` directories
+- Constraints are correctly propogated to the final output expression during symbolic execution
 
 ## Changed
 

diff --git a/src/EVM/SymExec.hs b/src/EVM/SymExec.hs
@@ -442,7 +442,7 @@ verifyContract solvers theCode signature' concreteArgs opts initStore maybepre m
 runExpr :: Stepper.Stepper (Expr End)
 runExpr = do
  vm <- Stepper.runFully
- let asserts = vm.keccakEqs
+ let asserts = vm.keccakEqs <> vm.constraints
  pure $ case vm.result of
  Just (VMSuccess buf) -> Success asserts buf vm.env.storage
  Just (VMFailure e) -> Failure asserts e