build fixes

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Oct 14, 2023 · a39d4ad · a39d4ad
1 parent 47f1c86
commit a39d4ad
Showing 1 changed file with 3 additions and 4 deletions.
diff --git 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;