diff --git a/src/math/lp/core_solver_pretty_printer_def.h b/src/math/lp/core_solver_pretty_printer_def.h
index 8d2cef125..db50ea0df 100644
--- a/src/math/lp/core_solver_pretty_printer_def.h
+++ b/src/math/lp/core_solver_pretty_printer_def.h
@@ -53,7 +53,7 @@ core_solver_pretty_printer<T, X>::core_solver_pretty_printer(lp_core_solver_base
     m_basis_heading_title = "heading";
     m_x_title = "x*";
     m_title_width = static_cast<unsigned>(std::max(std::max(m_cost_title.size(), std::max(m_basis_heading_title.size(), m_x_title.size())), m_approx_norm_title.size()));
-    m_squash_blanks = nrows() > 10 && ncols() > 10;
+    m_squash_blanks = nrows() > 10 && ncols() > 5;
 }
 
 template <typename T, typename X> void core_solver_pretty_printer<T, X>::init_costs() {
diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp
index aaa249b2a..a5ec36466 100644
--- a/src/smt/smt_context_pp.cpp
+++ b/src/smt/smt_context_pp.cpp
@@ -497,8 +497,6 @@ namespace smt {
 );
         display_lemma_as_smt_problem(out, num_antecedents, antecedents, num_eq_antecedents, eq_antecedents, consequent, logic);
         out.close();
-        if (m_lemma_id == 1444)
-            exit(0);
         return m_lemma_id;
     }