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;