From a39d4adf5b67ab77966eac8146c6c3dbc406f7df Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 14 Oct 2023 13:45:42 -0700 Subject: [PATCH] build fixes Signed-off-by: Nikolaj Bjorner --- src/math/lp/monomial_bounds.cpp | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/src/math/lp/monomial_bounds.cpp b/src/math/lp/monomial_bounds.cpp index 446bf4698..1acb56783 100644 --- a/src/math/lp/monomial_bounds.cpp +++ b/src/math/lp/monomial_bounds.cpp @@ -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;