mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 02:42:02 +00:00
Code Activity

remove debug code and improve printing

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-02-04 16:08:24 -08:00
parent 0d95c780d1
commit c562a1f883
2 changed files with 1 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/lp/core_solver_pretty_printer_def.h
View file

@ -53,7 +53,7 @@ core_solver_pretty_printer<T, X>::core_solver_pretty_printer(lp_core_solver_base
m_basis_heading_title = "heading"; m_basis_heading_title = "heading";
m_x_title = "x*"; 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_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() { template <typename T, typename X> void core_solver_pretty_printer<T, X>::init_costs() {

2
src/smt/smt_context_pp.cpp
View file

@ -497,8 +497,6 @@ namespace smt {
); );
display_lemma_as_smt_problem(out, num_antecedents, antecedents, num_eq_antecedents, eq_antecedents, consequent, logic); display_lemma_as_smt_problem(out, num_antecedents, antecedents, num_eq_antecedents, eq_antecedents, consequent, logic);
out.close(); out.close();
if (m_lemma_id == 1444)
exit(0);
return m_lemma_id; return m_lemma_id;
} }