mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-05-13 10:44:43 +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 • committed by Lev Nachmanson
parent dc7185d0a4
commit 436eefbce2
1 changed files with 5 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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

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