reject rows with columns with big numbers for lp bound propagation

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Z3Prover · Sep 21, 2023 · c0b55d1 · c0b55d1
1 parent f423642
commit c0b55d1
Showing 1 changed file with 7 additions and 1 deletion.
diff --git 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;
     }