diff --git a/src/math/polysat/search_state.cpp b/src/math/polysat/search_state.cpp
index 0bfbcfd62..742941a9d 100644
--- a/src/math/polysat/search_state.cpp
+++ b/src/math/polysat/search_state.cpp
@@ -38,24 +38,12 @@ namespace polysat {
         }
         case search_item_k::boolean: {
             sat::literal const lit = item.lit();
-            out << rpad(4, lit);
-            out << ": " << rpad(32, s.lit2cnstr(lit));
-            out << " @" << s.m_bvars.level(lit);
-            if (s.m_bvars.is_assumption(lit))
-                out << " assumption";
-            else if (s.m_bvars.is_bool_propagation(lit)) {
+            out << lit_pp(s, lit);
+            if (s.m_bvars.is_bool_propagation(lit)) {
                 clause* reason = s.m_bvars.reason(lit);
-                out << " bool propagation " << show_deref(reason);
-                for (auto l2 : *reason) {
-                    out << "\n\t" << rpad(4, l2) << ": " << rpad(16, s.lit2cnstr(l2)) << "   " << bool_justification_pp(s.m_bvars, l2);
-                }
-            }
-            else if (s.m_bvars.is_evaluation(lit)) {
-                out << " evaluated";
-            }
-            else {
-                SASSERT(s.m_bvars.is_decision(lit));
-                out << " decision";
+                out << "\n\treason " << show_deref(reason);
+                for (auto l2 : *reason)
+                    out << "\n\t" << lit_pp(s, l2);
             }
             return out;
         }
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 2a06bfcae..f87026f6c 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -1529,15 +1529,17 @@ namespace polysat {
             }
         );
 #if ENABLE_LEMMA_VALIDITY_CHECK
-        clause_builder clauseBuilder(*this);
+        clause_builder cb(*this, "unsat core check");
         for (auto d : deps) {
             for (sat::bool_var b = 0; b < m_bvars.size(); ++b) {
                 if (m_bvars.dep(b) != d)
                     continue;
-                clauseBuilder.insert(sat::literal(b, m_bvars.value(b) != l_false));
+                sat::literal lit(b, m_bvars.value(b) == l_false);
+                VERIFY(m_bvars.is_true(lit));
+                cb.insert(~lit);
             }
         }
-        log_lemma_smt2(*clauseBuilder.build()); // check the unsat-core
+        log_lemma_smt2(*cb.build());  // check the unsat core
 #endif
     }