diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index be6b0e6a4..27465aaf5 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -307,7 +307,7 @@ namespace smt {
 
     void context::assign_core(literal l, b_justification j, bool decision) {
         TRACE("assign_core", tout << (decision?"decision: ":"propagating: ") << l << " ";
-              display_literal_verbose(tout, l); tout << " level: " << m_scope_lvl << "\n";
+              display_literal_smt2(tout, l); tout << " level: " << m_scope_lvl << "\n";
               display(tout, j););
         m_assigned_literals.push_back(l);
         m_assignment[l.index()]    = l_true;
diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp
index f85b803f4..a698d94a0 100644
--- a/src/smt/smt_context_pp.cpp
+++ b/src/smt/smt_context_pp.cpp
@@ -103,9 +103,9 @@ namespace smt {
 
     std::ostream& context::display_literal_smt2(std::ostream& out, literal l) const {
         if (l.sign())
-            out << "  (not " << mk_bounded_pp(bool_var2expr(l.var()), m, 10) << ") ";
+            out << "  (not " << mk_pp(bool_var2expr(l.var()), m) << ") ";
         else
-            out << "  " << mk_bounded_pp(bool_var2expr(l.var()), m, 10) << " ";
+            out << "  " << mk_pp(bool_var2expr(l.var()), m) << " ";
         return out;
     }
 
diff --git a/src/smt/smt_literal.cpp b/src/smt/smt_literal.cpp
index a52293aab..67afbe962 100644
--- a/src/smt/smt_literal.cpp
+++ b/src/smt/smt_literal.cpp
@@ -30,9 +30,9 @@ namespace smt {
         else if (*this == null_literal)
             out << "null";
         else if (sign())
-            out << "(not " << mk_bounded_pp(bool_var2expr_map[var()], m) << ")";
+            out << "(not " << mk_bounded_pp(bool_var2expr_map[var()], m, 3) << ")";
         else
-            out << mk_bounded_pp(bool_var2expr_map[var()], m);
+            out << mk_bounded_pp(bool_var2expr_map[var()], m, 3);
     }
 
     void literal::display_compact(std::ostream & out, expr * const * bool_var2expr_map) const {