diff --git a/src/math/polysat/forbidden_intervals.cpp b/src/math/polysat/forbidden_intervals.cpp
index cd5db069e..4aea096aa 100644
--- a/src/math/polysat/forbidden_intervals.cpp
+++ b/src/math/polysat/forbidden_intervals.cpp
@@ -40,9 +40,6 @@ namespace polysat {
     
     bool forbidden_intervals::get_interval_mul_ovfl(signed_constraint const& c, pvar v, fi_record& fi) {
 
-
-        std::cout << "FORBIDDEN v" << v << "\n";
-
         backtrack _backtrack(fi.side_cond);     
 
         fi.coeff = 1;
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index cce6eb318..3b1e78231 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -598,15 +598,15 @@ namespace polysat {
         while (search_it.next()) {
             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.contains_pvar(v) && !m_conflict.is_bailout()) {
                     m_search.pop_assignment();
                     continue;
                 }
+                LOG_H2("Working on " << search_item_pp(m_search, item));
+                LOG(m_justification[v]);
                 LOG("Conflict: " << m_conflict);
                 inc_activity(v);
                 justification& j = m_justification[v];
@@ -621,10 +621,12 @@ 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;
+
+                LOG_H2("Working on " << search_item_pp(m_search, item));
+                LOG(bool_justification_pp(m_bvars, lit));
+                LOG("Literal " << lit << " is " << lit2cnstr(lit));
                 LOG("Conflict: " << m_conflict);
                 if (m_bvars.is_assumption(var))
                     continue;
@@ -1000,7 +1002,10 @@ namespace polysat {
             if (item.is_assignment()) {
                 pvar v = item.var();
                 auto const& j = m_justification[v];
-                out << "\t" << assignment_pp(*this, v, get_value(v)) << " @" << j.level();   
+                out << "\t" << assignment_pp(*this, v, get_value(v)) << " @" << j.level() << " ";
+                if (j.is_propagation()) 
+                    for (auto const& c : m_viable.get_constraints(v))
+                        out << c << " ";
                 out << "\n";
             }
             else {
diff --git a/src/math/polysat/viable.h b/src/math/polysat/viable.h
index f64fe19ff..e64352b6e 100644
--- a/src/math/polysat/viable.h
+++ b/src/math/polysat/viable.h
@@ -156,15 +156,15 @@ namespace polysat {
         };
 
         class constraints {
-            viable& v;
+            viable const& v;
             pvar var;
         public:
-            constraints(viable& v, pvar var) : v(v), var(var) {}
+            constraints(viable const& v, pvar var) : v(v), var(var) {}
             iterator begin() const { return iterator(v.m_units[var], false); }
             iterator end() const { return iterator(v.m_units[var], true); }
         };
 
-        constraints get_constraints(pvar v) { 
+        constraints get_constraints(pvar v) const { 
             return constraints(*this, v); 
         }