mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

is_linear does not check for is_big

Browse source
This commit is contained in:
Lev Nachmanson 2023-09-15 17:44:10 -07:00
parent b621c9fa1c
commit c240f62ca8
1 changed files with 2 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/math/lp/lp_bound_propagator.h
View file

@ -121,7 +121,6 @@ private:
bool is_linear(const svector<lpvar>& m, lpvar& zero_var, lpvar& non_fixed) { bool is_linear(const svector<lpvar>& m, lpvar& zero_var, lpvar& non_fixed) {
zero_var = non_fixed = null_lpvar; zero_var = non_fixed = null_lpvar;
unsigned n_of_non_fixed = 0; unsigned n_of_non_fixed = 0;
bool big_bound = false;
for (lpvar v : m) { for (lpvar v : m) {
if (!this->column_is_fixed(v)) { if (!this->column_is_fixed(v)) {
n_of_non_fixed++; n_of_non_fixed++;
@ -133,11 +132,9 @@ private:
zero_var = v; zero_var = v;
return true; return true;
} }
if (b.is_big()) {
big_bound |= true;
}
} }
return n_of_non_fixed <= 1 && !big_bound; return n_of_non_fixed <= 1;
} }