From 576309a16fe8e6d30dd19bebaeaa1bc0b4856b6a Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 21 Sep 2023 16:30:43 -0700 Subject: [PATCH] Revert "reject rows with columns with big numbers for lp bound propagation" This reverts commit c0b55d14352fa76f3a2eabf346a8d20fb93b4e9e. --- src/math/lp/lar_solver.cpp | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index dc114e9e0..08ff3b0d4 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -135,15 +135,9 @@ 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; }