From c591a7a3e78dfd5f7b9923f2e95cf5922a475236 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 17 Jan 2024 13:53:59 -1000 Subject: [PATCH] force int bound on int columns, call term_is_int() after subst Signed-off-by: Lev Nachmanson --- src/math/lp/lar_solver.cpp | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index a55edfe35fc..5762cbc9a53 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -1641,12 +1641,12 @@ namespace lp { var_index lar_solver::add_term(const vector>& coeffs, unsigned ext_i) { TRACE("lar_solver_terms", print_linear_combination_of_column_indices_only(coeffs, tout) << ", ext_i =" << ext_i << "\n";); SASSERT(!m_var_register.external_is_used(ext_i)); - m_term_register.add_var(ext_i, term_is_int(coeffs)); - lp_assert(all_vars_are_registered(coeffs)); - if (strategy_is_undecided()) - return add_term_undecided(coeffs); + SASSERT(all_vars_are_registered(coeffs)); lar_term* t = new lar_term(coeffs); subst_known_terms(t); + m_term_register.add_var(ext_i, term_is_int(t)); + if (strategy_is_undecided()) + return add_term_undecided(coeffs); push_term(t); SASSERT(m_terms.size() == m_term_register.size()); unsigned adjusted_term_index = m_terms.size() - 1; @@ -1938,10 +1938,11 @@ namespace lp { tout << std::endl; } }); + mpq rs = adjust_bound_for_int(j, kind, right_side); if (column_has_upper_bound(j)) - update_column_type_and_bound_with_ub(j, kind, right_side, dep); + update_column_type_and_bound_with_ub(j, kind, rs, dep); else - update_column_type_and_bound_with_no_ub(j, kind, right_side, dep); + update_column_type_and_bound_with_no_ub(j, kind, rs, dep); if (is_base(j) && column_is_fixed(j)) m_fixed_base_var_set.insert(j);