From f678861aef8a49d53100d9d45fb28d04e49f81d5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 16 Oct 2023 08:43:08 -0700 Subject: [PATCH] fix #6947 --- src/math/lp/monomial_bounds.cpp | 8 -------- 1 file changed, 8 deletions(-) diff --git a/src/math/lp/monomial_bounds.cpp b/src/math/lp/monomial_bounds.cpp index 07028e001..e54f82682 100644 --- a/src/math/lp/monomial_bounds.cpp +++ b/src/math/lp/monomial_bounds.cpp @@ -152,14 +152,6 @@ namespace nla { lemma &= ex; 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)) { // v = -2, [-4,-3]^3 < v^3 -> add bound v <= -3