From c0b55d14352fa76f3a2eabf346a8d20fb93b4e9e Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 21 Sep 2023 15:53:53 -0700 Subject: [PATCH] reject rows with columns with big numbers for lp bound propagation Signed-off-by: Lev Nachmanson --- src/math/lp/lar_solver.cpp | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index 08ff3b0d4..dc114e9e0 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -135,9 +135,15 @@ namespace lp { bool lar_solver::row_has_a_big_num(unsigned i) const { - for (const auto& c : A_r().m_rows[i]) + for (const auto& c : A_r().m_rows[i]) { if (c.coeff().is_big()) return true; + if (column_has_lower_bound(c.var())&& get_lower_bound(c.var()).x.is_big()) + return true; + if (column_has_upper_bound(c.var())&& get_upper_bound(c.var()).x.is_big()) + return true; + } + return false; }