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

change some TRACE statements

Browse source
This commit is contained in:
Lev Nachmanson 2023-12-20 06:49:55 -10:00
parent db5a1a7604
commit d6365610d5
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/math/lp/int_solver.cpp
View file

@ -670,11 +670,11 @@ namespace lp {
if (abs(value.x) < small_value || if (abs(value.x) < small_value ||
(has_upper(j) && small_value > upper_bound(j).x - value.x) || (has_upper(j) && small_value > upper_bound(j).x - value.x) ||
(has_lower(j) && small_value > value.x - lower_bound(j).x)) { (has_lower(j) && small_value > value.x - lower_bound(j).x)) {
TRACE("gomory_cut", tout << "small j" << j << "\n"); TRACE("int_solver", tout << "small j" << j << "\n");
add_column(true, r_small_value, n_small_value, j); add_column(true, r_small_value, n_small_value, j);
continue; continue;
} }
TRACE("gomory_cut", tout << "any j" << j << "\n"); TRACE("int_solver", tout << "any j" << j << "\n");
add_column(usage >= prev_usage, r_any_value, n_any_value, j); add_column(usage >= prev_usage, r_any_value, n_any_value, j);
if (usage > prev_usage) if (usage > prev_usage)
prev_usage = usage; prev_usage = usage;