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);