mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

fix #6947

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-10-16 08:43:08 -07:00
parent ba881d9c9b
commit f678861aef
1 changed files with 0 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/math/lp/monomial_bounds.cpp
View file

@ -152,14 +152,6 @@ namespace nla {
lemma &= ex; lemma &= ex;
return true; return true;
} }
// v.upper < 0, but v^p > range.upper -> infeasible.
if (p % 2 == 0 && c().has_upper_bound(v) && c().get_upper_bound(v) < 0) {
++c().lra.settings().stats().m_nla_propagate_bounds;
new_lemma lemma(c(), "range requires a non-negative upper bound");
lemma &= ex;
lemma.explain_existing_upper_bound(v);
return true;
}
if (rational(dep.upper(range)).root(p, r)) { if (rational(dep.upper(range)).root(p, r)) {
// v = -2, [-4,-3]^3 < v^3 -> add bound v <= -3 // v = -2, [-4,-3]^3 < v^3 -> add bound v <= -3