From d7718623a4a8c0039eefd5da778b9514cca12ee7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 4 Sep 2025 12:58:03 -0700 Subject: [PATCH] handle case where all variables are bounded Signed-off-by: Nikolaj Bjorner --- src/math/lp/nla_core.cpp | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index e821e26bd..b4efae222 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1555,7 +1555,12 @@ void core::refine_pseudo_linear(monic const& m) { lemma_builder lemma(*this, "nla-pseudo-linear"); lpvar nlvar = null_lpvar; rational prod(1); - for (auto v : m.vars()) { + for (unsigned i = 0; i < m.vars().size(); ++i) { + auto v = m.vars()[i]; + if (i == m.vars().size() - 1 && nlvar == null_lpvar) { + nlvar = v; + break; + } if (lra.column_is_bounded(v) && lra.var_is_int(v)) { auto lb = lra.get_lower_bound(v); auto ub = lra.get_upper_bound(v); @@ -1568,6 +1573,7 @@ void core::refine_pseudo_linear(monic const& m) { SASSERT(nlvar == null_lpvar); nlvar = v; } + SASSERT(nlvar != null_lpvar); lemma |= ineq(lp::lar_term(m.var(), rational(-prod), nlvar), llc::EQ, rational(0)); // lemma.display(verbose_stream() << "pseudo-linear lemma\n"); }