From e13e85c4abc7e59c4541eff0130bbf6fcedcebfc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 28 Oct 2025 03:16:12 -0700 Subject: [PATCH] swap signs of coefficients compared to sign of variables. They are on different sides of inequality Signed-off-by: Nikolaj Bjorner --- src/math/lp/nla_stellensatz.cpp | 4 ++-- src/math/lp/nra_solver.cpp | 1 + 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/src/math/lp/nla_stellensatz.cpp b/src/math/lp/nla_stellensatz.cpp index 1a6e6fb30..9a7b2e2c4 100644 --- a/src/math/lp/nla_stellensatz.cpp +++ b/src/math/lp/nla_stellensatz.cpp @@ -702,7 +702,7 @@ namespace nla { lhs.add_monomial(coeff, j); } if (quot_lo.empty()) { - auto coeff = -lo_sign * con_lo.rhs() / coeff_lo; + auto coeff = lo_sign * con_lo.rhs() / coeff_lo; rhs += coeff; } else if (con_lo.rhs() != 0) { @@ -716,7 +716,7 @@ namespace nla { lhs.add_monomial(coeff, j); } if (quot_hi.empty()) { - auto coeff = -hi_sign * con_hi.rhs() / coeff_hi; + auto coeff = hi_sign * con_hi.rhs() / coeff_hi; rhs += coeff; } else if (con_hi.rhs() != 0) { diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp index c8346d0b7..ceff0e4bb 100644 --- a/src/math/lp/nra_solver.cpp +++ b/src/math/lp/nra_solver.cpp @@ -120,6 +120,7 @@ struct solver::imp { } } m_nlsat->collect_statistics(st); + TRACE(nra, tout << "nra result " << r << "\n"); CTRACE(nra, false, m_nlsat->display(tout << r << "\n"); display(tout);