diff --git a/src/math/polysat/constraint.h b/src/math/polysat/constraint.h
index e484571d1..1b7414886 100644
--- a/src/math/polysat/constraint.h
+++ b/src/math/polysat/constraint.h
@@ -217,7 +217,7 @@ namespace polysat {
         constraint_literal& operator=(nullptr_t) { m_literal = sat::null_literal; m_constraint = nullptr; return *this; }
     private:
         friend class constraint_manager;
-        explicit constraint_literal(polysat::constraint* c): constraint_literal(sat::literal(c->bvar()), c) {}
+        explicit constraint_literal(constraint* c): constraint_literal(sat::literal(c->bvar()), c) {}
     };
 
 
diff --git a/src/math/polysat/eq_constraint.cpp b/src/math/polysat/eq_constraint.cpp
index dec682819..daf4b0193 100644
--- a/src/math/polysat/eq_constraint.cpp
+++ b/src/math/polysat/eq_constraint.cpp
@@ -19,7 +19,7 @@ Author:
 namespace polysat {
 
     std::ostream& eq_constraint::display(std::ostream& out) const {
-        out << p() << (is_positive() ? " == 0 " : " != 0");
+        out << p() << " == 0";
         return display_extra(out);
     }
 
diff --git a/src/math/polysat/explain.cpp b/src/math/polysat/explain.cpp
index 5ca8775c2..7626aa179 100644
--- a/src/math/polysat/explain.cpp
+++ b/src/math/polysat/explain.cpp
@@ -91,6 +91,7 @@ namespace polysat {
     clause_ref conflict_explainer::by_polynomial_superposition() {
         LOG_H3("units-size: " << m_conflict.units().size() << " conflict-clauses " << m_conflict.clauses().size());
         constraint* c1 = nullptr, *c2 = nullptr;
+
         if (m_conflict.units().size() == 2 && m_conflict.clauses().size() == 0) {
             c1 = m_conflict.units()[0];
             c2 = m_conflict.units()[1];
@@ -111,6 +112,8 @@ namespace polysat {
                     if (lit.sign())
                         continue;
                     constraint* c = m_solver.m_constraints.lookup(lit.var());                    
+                    c->assign(true);
+                    // this clause is really a unit.
                     LOG("unit clause: " << *c);
                     if (c->is_eq() && c->is_positive()) {
                         c1 = c;
@@ -127,7 +130,6 @@ namespace polysat {
                     break;
                 }
             }
-            std::cout << c1 << " " << c2 << "\n";
 #endif
         }
         if (!c1 || !c2 || c1 == c2)