From 0f993e39779df1cbe053420cbdc1cb3568ec41d3 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Tue, 27 Sep 2022 17:56:26 +0200
Subject: [PATCH] New constraints need to be eval'd

---
 src/math/polysat/saturation.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/math/polysat/saturation.cpp b/src/math/polysat/saturation.cpp
index dd876549c..efa1317b9 100644
--- a/src/math/polysat/saturation.cpp
+++ b/src/math/polysat/saturation.cpp
@@ -99,7 +99,7 @@ namespace polysat {
 
         core.reset();
         for (auto d : m_new_constraints)
-            core.insert(d);
+            core.insert_eval(d);
         if (c.bvalue(s) != l_false)  // conflict is due to the evaluation of c, so it depends on the variable values
             core.insert_vars(c);
         core.insert(~c);