mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 03:07:07 +00:00
Code Activity

move a TRACE statement

Browse source
This commit is contained in:
Lev Nachmanson 2023-12-31 20:58:26 -10:00 committed by Lev Nachmanson
parent fd2b6c62d1
commit 84997f8b21
1 changed files with 0 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/math/lp/gomory.cpp
View file

@ -322,7 +322,6 @@ public:
for (auto c : *m_ex)
m_dep = lia.lra.join_deps(lia.lra.dep_manager().mk_leaf(c.ci()), m_dep);
TRACE("gomory_cut", print_linear_combination_of_column_indices_only(m_t.coeffs_as_vector(), tout << "gomory cut: "); tout << " >= " << m_k << std::endl;);
TRACE("gomory_cut_detail", dump_cut_and_constraints_as_smt_lemma(tout);
lia.lra.display(tout));
SASSERT(lia.current_solution_is_inf_on_cut());