diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3bba8b0b2..c25499598 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
 
 ## Changed
 
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