Consider substitution as constraints in evaluatePattern

runtimeverification · Oct 16, 2024 · abf0354 · abf0354
1 parent 77c8c57
commit abf0354
Showing 1 changed file with 8 additions and 1 deletion.
diff --git a/booster/library/Booster/Pattern/ApplyEquations.hs b/booster/library/Booster/Pattern/ApplyEquations.hs
@@ -455,7 +455,14 @@ evaluatePattern ::
     Pattern ->
     io (Either EquationFailure Pattern, SimplifierCache)
 evaluatePattern def mLlvmLibrary smtSolver cache pat =
-    runEquationT def mLlvmLibrary smtSolver cache pat.constraints . evaluatePattern' $ pat
+    runEquationT
+        def
+        mLlvmLibrary
+        smtSolver
+        cache
+        (pat.constraints <> (Set.fromList . asEquations $ pat.substitution))
+        . evaluatePattern'
+        $ pat
 
 -- version for internal nested evaluation
 evaluatePattern' ::