diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 8215f7500..06881f343 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -1113,8 +1113,10 @@ namespace polysat {
 
     std::ostream& lit_pp::display(std::ostream& out) const {
         auto c = s.lit2cnstr(lit);
-        out << lpad(4, lit) << ": " << rpad(30, c) << "  [";
-        out << " " << s.m_bvars.value(lit);
+        out << lpad(4, lit) << ": " << rpad(30, c);
+        if (!c)
+            return out;
+        out << "  [ " << s.m_bvars.value(lit);
         if (s.m_bvars.is_assigned(lit)) {
             out << ' ';
             if (s.m_bvars.is_assumption(lit))
@@ -1123,6 +1125,8 @@ namespace polysat {
                 out << "bprop";
             else if (s.m_bvars.is_value_propagation(lit))
                 out << "eval";
+            else if (s.m_bvars.is_decision(lit))
+                out << "decide";
             out << '@' << s.m_bvars.level(lit);
         }
         if (c->is_pwatched())
diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h
index 9b2ae4fc6..f62dffe28 100644
--- a/src/math/polysat/solver.h
+++ b/src/math/polysat/solver.h
@@ -457,7 +457,7 @@ namespace polysat {
         solver const& s;
         sat::literal lit;
     public:
-        lit_pp(solver const& s, signed_constraint c): s(s), lit(c.blit()) {}
+        lit_pp(solver const& s, signed_constraint c): s(s), lit(c ? c.blit() : sat::null_literal) {}
         lit_pp(solver const& s, sat::literal lit): s(s), lit(lit) {}
         std::ostream& display(std::ostream& out) const;
     };