From 447af0f5480aafb56adbb4ba74c47df57cb603a8 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 24 Feb 2025 13:07:40 -0800 Subject: [PATCH] allow fixed variables is term tightening Signed-off-by: Lev Nachmanson --- src/math/lp/dioph_eq.cpp | 10 +++------- 1 file changed, 3 insertions(+), 7 deletions(-) diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp index d6e551a0c..12d508672 100644 --- a/src/math/lp/dioph_eq.cpp +++ b/src/math/lp/dioph_eq.cpp @@ -1377,15 +1377,11 @@ namespace lp { std_vector cleanup; m_tightened_columns.reset(); for (unsigned j : m_changed_terms) { - if ( - j >= lra.column_count() || + if (j >= lra.column_count() || !lra.column_has_term(j) || lra.column_is_free(j) || - is_fixed(j) || - !lia.column_is_int(j) - || - !term_has_int_inv_vars(j) - ) { + !lia.column_is_int(j) || + !term_has_int_inv_vars(j)) { cleanup.push_back(j); continue; }