From ecfbdbbd2318ea60c6feb6be7ffb03241f00d4ea Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 12 Mar 2025 17:31:34 -0700 Subject: [PATCH] allow bounds tightening on fixed columns Signed-off-by: Lev Nachmanson --- src/math/lp/dioph_eq.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp index 88d7cd997..989cb2aa3 100644 --- a/src/math/lp/dioph_eq.cpp +++ b/src/math/lp/dioph_eq.cpp @@ -1028,8 +1028,8 @@ namespace lp { eliminate_substituted_in_changed_rows(); m_changed_columns.reset(); - SASSERT(m_changed_columns.size() == 0); m_changed_rows.reset(); + // do not clean up m_changed_terms as they are used in tighten_terms_with_S() SASSERT(entries_are_ok()); } @@ -1372,7 +1372,7 @@ namespace lp { if (j >= lra.column_count() || !lra.column_has_term(j) || lra.column_is_free(j) || - is_fixed(j) || !lia.column_is_int(j)) { + !lia.column_is_int(j)) { cleanup.push_back(j); continue; }