From 8a59a76773caae0d24ada780a4192c6002422125 Mon Sep 17 00:00:00 2001
From: David Terry <me@xwvvvvwx.com>
Date: Wed, 31 May 2023 16:29:00 +0200
Subject: [PATCH] SymExec: propogate constraints from vm to output expression

---
 CHANGELOG.md       | 1 +
 src/EVM/SymExec.hs | 2 +-
 2 files changed, 2 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index dc5eca06f..3376e09d7 100644
--- 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
 
 ## [0.51.0] - 2023-04-27
 
diff --git a/src/EVM/SymExec.hs b/src/EVM/SymExec.hs
index 04005bedc..33730655d 100644
--- 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