mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 13:58:45 +00:00
Code Activity

always remove the tightened term

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-04-08 10:47:51 -07:00
parent dd1b2a294f
commit 019da2308e
1 changed files with 5 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/math/lp/dioph_eq.cpp
View file

@ -1543,10 +1543,13 @@ namespace lp {
// print_bounds(tout);
);
for (unsigned j : sorted_changed_terms) {
m_terms_to_tighten.remove(j);
if (ignore_big_nums() && term_has_big_number(lra.get_term(j)))
if (ignore_big_nums() && term_has_big_number(lra.get_term(j))) {
m_terms_to_tighten.remove(j);
continue;
}
auto ret = tighten_bounds_for_term_column(j);
m_terms_to_tighten.remove(j);
r = join(ret, r);
if (r == lia_move::conflict)
break;
@ -1892,7 +1895,6 @@ namespace lp {
if (lra.settings().get_cancel_flag())
return false;
lra.update_column_type_and_bound(j, kind, bound, dep);
lp_status st = lra.find_feasible_solution();
if (is_sat(st) || st == lp::lp_status::CANCELLED)
return false;