diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 4677c7cd1..256f2c1f3 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -920,7 +920,7 @@ namespace polysat {
     void solver::add_clause(clause& clause) {
         LOG((clause.is_redundant() ? "Lemma: ": "Aux: ") << clause);
         for (sat::literal lit : clause) {
-            LOG("   Literal " << lit << " is: " << lit2cnstr(lit));
+            LOG("   Literal " << lit << " is: " << lit_pp(*this, lit));
             // SASSERT(m_bvars.value(lit) != l_true);
             // it could be that such a literal has been created previously but we don't detect it when e.g. narrowing a mul_ovfl_constraint
             if (m_bvars.value(lit) == l_true) {
@@ -1046,6 +1046,17 @@ namespace polysat {
         return out;
     }
 
+    std::ostream& lit_pp::display(std::ostream& out) const {
+        auto c = s.lit2cnstr(lit);
+        out << lit << ": " << c << "  [";
+        out << " bvalue=" << s.m_bvars.value(lit);
+        if (s.m_bvars.is_assigned(lit))
+            out << " @" << s.m_bvars.level(lit);
+        out << " pwatched=" << c->is_pwatched();
+        out << "  ]";
+        return out;
+    }
+
     std::ostream& num_pp::display(std::ostream& out) const {
         rational const& p = rational::power_of_two(s.size(var));
         if (val > mod(-val, p))
diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h
index 7a238febf..5cec5a360 100644
--- a/src/math/polysat/solver.h
+++ b/src/math/polysat/solver.h
@@ -80,6 +80,7 @@ namespace polysat {
         friend class viable_fallback;
         friend class search_state;
         friend class num_pp;
+        friend class lit_pp;
         friend class assignment_pp;
         friend class assignments_pp;
         friend class ex_polynomial_superposition;
@@ -420,6 +421,14 @@ namespace polysat {
         std::ostream& display(std::ostream& out) const;
     };
 
+    class lit_pp {
+        solver const& s;
+        sat::literal lit;
+    public:
+        lit_pp(solver const& s, sat::literal lit): s(s), lit(lit) {}
+        std::ostream& display(std::ostream& out) const;
+    };
+
     /** Format value 'val' as member of the domain of 'var' */
     class num_pp {
         solver const& s;
@@ -434,6 +443,8 @@ namespace polysat {
 
     inline std::ostream& operator<<(std::ostream& out, num_pp const& v) { return v.display(out); }
 
+    inline std::ostream& operator<<(std::ostream& out, lit_pp const& l) { return l.display(out); }
+
     inline std::ostream& operator<<(std::ostream& out, assignment_pp const& p) { return p.display(out); }
 
     inline std::ostream& operator<<(std::ostream& out, assignments_pp const& a) { return a.display(out); }