From cb1818f4b87dcea22d1e0f189926aa613fb102d4 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 7 Apr 2025 11:49:39 -0700 Subject: [PATCH] reject more terms with big numbers Signed-off-by: Lev Nachmanson --- src/math/lp/dioph_eq.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp index 2864650d3..4ae49787b 100644 --- a/src/math/lp/dioph_eq.cpp +++ b/src/math/lp/dioph_eq.cpp @@ -1065,9 +1065,11 @@ namespace lp { void process_changed_columns(std_vector &f_vector) { find_changed_terms_and_more_changed_rows(); for (unsigned j: m_changed_terms) { - if (j >= lra.column_count()) + if (j >= lra.column_count() || + !lra.column_has_term(j) || + (ignore_big_nums() && term_has_big_number(lra.get_term(j))) + ) continue; - SASSERT(!ignore_big_nums() || !term_has_big_number(lra.get_term(j))); m_terms_to_tighten.insert(j); if (j < m_l_matrix.column_count()) { for (const auto& cs : m_l_matrix.column(j)) {