diff --git a/src/math/polysat/boolean.cpp b/src/math/polysat/boolean.cpp
index 5b15448cf..c465bcb77 100644
--- a/src/math/polysat/boolean.cpp
+++ b/src/math/polysat/boolean.cpp
@@ -122,4 +122,13 @@ namespace polysat {
         }
         return out;
     }
+
+    std::ostream& bool_var_manager::display_justification(sat::literal lit, std::ostream& out) const {
+        out << m_kind[lit.var()];
+        if (is_assigned(lit))
+            out << " @ " << level(lit);
+        if (is_bool_propagation(lit))
+            out << " by " << show_deref(reason(lit));
+        return out;
+    }
 }
diff --git a/src/math/polysat/boolean.h b/src/math/polysat/boolean.h
index b7e8a2118..23b9384f8 100644
--- a/src/math/polysat/boolean.h
+++ b/src/math/polysat/boolean.h
@@ -92,6 +92,7 @@ namespace polysat {
         void unassign(sat::literal lit);
 
         std::ostream& display(std::ostream& out) const;
+        std::ostream& display_justification(sat::literal lit, std::ostream& out) const;
 
         friend std::ostream& operator<<(std::ostream& out, kind_t const& k) {
             switch (k) {
@@ -104,6 +105,14 @@ namespace polysat {
          }
     };
 
+    struct bool_justification_pp {
+        bool_var_manager const& b;
+        sat::literal lit;
+        bool_justification_pp(bool_var_manager const& b, sat::literal lit) : b(b), lit(lit) {}
+    };
+
     inline std::ostream& operator<<(std::ostream& out, bool_var_manager const& m) { return m.display(out); }
 
+    inline std::ostream& operator<<(std::ostream& out, bool_justification_pp const& p) { return p.b.display_justification(p.lit, out); }
+
 }
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 88ead7623..52da561c6 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -502,7 +502,8 @@ namespace polysat {
     void solver::resolve_conflict() {        
         LOG_H2("Resolve conflict");
         LOG("\n" << *this);
-        LOG("search state: " << m_search);
+        LOG("Search state: " << m_search);
+        LOG("Assignment: " << assignments_pp(*this));
         for (pvar v = 0; v < m_justification.size(); ++v)
             LOG("v" << v << " " << viable::var_pp(m_viable, v));
         ++m_stats.m_num_conflicts;
@@ -527,13 +528,13 @@ namespace polysat {
         
         search_iterator search_it(m_search);
         while (search_it.next()) {
-            // LOG("search state: " << m_search);
             auto& item = *search_it;
             search_it.set_resolved();
             LOG_H2("Working on " << search_item_pp(m_search, item));
             if (item.is_assignment()) {
                 // Resolve over variable assignment
                 pvar v = item.var();
+                LOG(m_justification[v]);
                 if (!m_conflict.is_pmarked(v) && !m_conflict.is_bailout()) {
                     m_search.pop_assignment();
                     continue;
@@ -552,6 +553,8 @@ namespace polysat {
                 SASSERT(item.is_boolean());
                 sat::literal const lit = item.lit();
                 sat::bool_var const var = lit.var();
+                LOG(bool_justification_pp(m_bvars, lit));
+                LOG("Literal " << lit << " is " << lit2cnstr(lit));
                 if (!m_conflict.is_bmarked(var))
                     continue;
                 if (m_bvars.level(var) <= base_level())