diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp
index 955b295a4..f2eba6ac5 100644
--- a/src/math/polysat/conflict.cpp
+++ b/src/math/polysat/conflict.cpp
@@ -68,7 +68,7 @@ namespace polysat {
         m_conflict_var = null_var;
         m_saturation_premises.reset();
         m_bailout = false;
-        SASSERT(empty());
+        SASSERT(empty());        
     }
 
     /**
@@ -163,8 +163,6 @@ namespace polysat {
         SASSERT(std::all_of(m_constraints.begin(), m_constraints.end(), [](auto c){ return !c->has_bvar(); }));
         bool core_has_pos = contains_literal(sat::literal(var));
         bool core_has_neg = contains_literal(~sat::literal(var));
-        std::cout << cl << "\n";
-        std::cout << *this << "\n";
         DEBUG_CODE({
             bool clause_has_pos = std::count(cl.begin(), cl.end(), sat::literal(var)) > 0;
             bool clause_has_neg = std::count(cl.begin(), cl.end(), ~sat::literal(var)) > 0;
@@ -173,12 +171,14 @@ namespace polysat {
             SASSERT((core_has_pos && clause_has_pos) || (core_has_neg && clause_has_neg));
         });
 
+        sat::literal var_lit(var);
         if (core_has_pos)
-            remove_literal(sat::literal(var));
+            remove_literal(var_lit);
         if (core_has_neg)
-            remove_literal(~sat::literal(var));
-        unset_bmark(var);
-
+            remove_literal(~var_lit);
+        
+        unset_mark(m.lookup(var_lit));
+        
         for (sat::literal lit : cl)
             if (lit.var() != var)
                 insert(m.lookup(~lit));
diff --git a/src/math/polysat/explain.cpp b/src/math/polysat/explain.cpp
index 55af07c83..901a8635b 100644
--- a/src/math/polysat/explain.cpp
+++ b/src/math/polysat/explain.cpp
@@ -98,7 +98,7 @@ namespace polysat {
         while (progress) {
             progress = false;
             for (auto c : core) {
-                if (is_positive_equality_over(v, c) && reduce_by(v, c, core)) {
+                if (is_positive_equality_over(v, c) && c.is_currently_true(s()) && reduce_by(v, c, core)) {
                     progress = true;
                     break;
                 }
@@ -125,10 +125,16 @@ namespace polysat {
                 auto c2 = s().ule(a, b);
                 if (!c.is_positive())
                     c2 = ~c2;
-                SASSERT(c2.is_currently_false(s()));
+                SASSERT(c2.is_currently_false(s()));                
                 if (!c2->has_bvar() || l_undef == c2.bvalue(s()))
                     core.keep(c2);  // adds propagation of c to the search stack
                 core.reset();
+                if (c2.bvalue(s()) == l_false) {
+                    core.insert(eq);
+                    core.insert(c);
+                    core.insert(~c2);
+                    return false;
+                }
                 core.set(c2);                
                 return true;
             }