From 436eefbce20a494ee5eb36d7e3dac940e01c65c3 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 8 Apr 2025 10:47:51 -0700 Subject: [PATCH] always remove the tightened term Signed-off-by: Lev Nachmanson --- src/math/lp/dioph_eq.cpp | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp index 6ba0d8cc7..1458a7054 100644 --- a/src/math/lp/dioph_eq.cpp +++ b/src/math/lp/dioph_eq.cpp @@ -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;