is_linear does not check for is_big

Z3Prover · Sep 16, 2023 · c240f62 · c240f62
1 parent b621c9f
commit c240f62
Showing 1 changed file with 2 additions and 5 deletions.
diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h
@@ -121,7 +121,6 @@ class lp_bound_propagator {
     bool is_linear(const svector<lpvar>& m, lpvar& zero_var, lpvar& non_fixed) {
         zero_var = non_fixed = null_lpvar;
         unsigned n_of_non_fixed = 0;
-        bool big_bound = false;
         for (lpvar v : m) {
             if (!this->column_is_fixed(v)) {
                 n_of_non_fixed++;
@@ -133,11 +132,9 @@ class lp_bound_propagator {
                 zero_var = v;
                 return true;
             } 
-            if (b.is_big()) {
-                big_bound |= true;
-            }
+
         }
-        return n_of_non_fixed <= 1 && !big_bound;
+        return n_of_non_fixed <= 1;
     }