diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp
index 3a02d76ce..7826ff18e 100644
--- a/src/math/polysat/conflict.cpp
+++ b/src/math/polysat/conflict.cpp
@@ -127,7 +127,7 @@ namespace polysat {
      */
     void conflict::insert(signed_constraint c) {
         if (c.is_always_true())
-            return;
+            return;        
         if (c->is_marked())
             return;
         LOG("inserting: " << c);
@@ -150,6 +150,7 @@ namespace polysat {
      */
     void conflict::insert(signed_constraint c, vector<signed_constraint> const& premises) {
         keep(c);
+
         clause_builder c_lemma(s);
         for (auto premise : premises) {
             LOG_H3("premise: " << premise);
@@ -162,7 +163,7 @@ namespace polysat {
         clause_ref lemma = c_lemma.build();
         SASSERT(lemma);
         cm().store(lemma.get(), s);
-        if (s.m_bvars.value(c.blit()) == l_undef)
+        if (c.bvalue(s) == l_undef)
             s.assign_propagate(c.blit(), *lemma);
     }
 
diff --git a/src/math/polysat/explain.cpp b/src/math/polysat/explain.cpp
index 6d09e59cf..34064d735 100644
--- a/src/math/polysat/explain.cpp
+++ b/src/math/polysat/explain.cpp
@@ -76,8 +76,12 @@ namespace polysat {
                 // Ensure that c is assigned and justified                    
                 premises.push_back(c1);
                 premises.push_back(c2);
+                // var dependency on c is lost
+                // c evaluates to false, when the clause ~c1 or ~c2 or c
+                // gets created, c is assigned to false by evaluation propagation
+                // It should have been assigned true by unit propagation.
                 core.replace(c2, c, premises);
-                // SASSERT_EQ(l_true, c.bvalue(s));  // TODO: currently violated, check this!
+                SASSERT_EQ(l_true, c.bvalue(s));  // TODO: currently violated, check this!
                 SASSERT(c.is_currently_false(s));
                 break;
             default:
@@ -88,6 +92,7 @@ namespace polysat {
             // c alone (+ variables) is now enough to represent the conflict.
             core.reset();
             core.set(c);
+            std::cout << "set c\n";
             return c->contains_var(v) ? l_undef : l_true;
         }
         return l_false;