Revert "reject rows with columns with big numbers for lp bound propag…

…ation" This reverts commit c0b55d1.
Z3Prover · Sep 21, 2023 · 576309a · 576309a
1 parent c0b55d1
commit 576309a
Showing 1 changed file with 1 addition and 7 deletions.
diff --git 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;
     }