mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
build fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
47f1c86f93
commit
a39d4adf5b
|
@ -143,7 +143,6 @@ namespace nla {
|
|||
return propagate_value(range, v);
|
||||
rational r;
|
||||
if (should_propagate_upper(range, v, p)) { // v.upper^p > range.upper
|
||||
SASSERT(c().has_upper_bound(v));
|
||||
lp::explanation ex;
|
||||
dep.get_upper_dep(range, ex);
|
||||
// p even, range.upper < 0, v^p >= 0 -> infeasible
|
||||
|
@ -154,16 +153,16 @@ namespace nla {
|
|||
return true;
|
||||
}
|
||||
// v.upper < 0, but v^p > range.upper -> infeasible.
|
||||
if (p % 2 == 0 && c().get_upper_bound(v) < 0) {
|
||||
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;
|
||||
}
|
||||
SASSERT(p % 2 == 1 || c().get_upper_bound(v) >= 0);
|
||||
|
||||
if (rational(dep.upper(range)).root(p, r)) {
|
||||
if (rational(dep.upper(range)).root(p, r) && (p % 2 == 1 || c().has_upper_bound(v))) {
|
||||
SASSERT(p % 2 == 1 || c().get_upper_bound(v) >= 0);
|
||||
// v = -2, [-4,-3]^3 < v^3 -> add bound v <= -3
|
||||
// v = -2, [-1,+1]^2 < v^2 -> add bound v >= -1
|
||||
++c().lra.settings().stats().m_nla_propagate_bounds;
|
||||
|
|
Loading…
Reference in a new issue