mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-28 18:29:23 +00:00
Code Activity

swap signs of coefficients compared to sign of variables. They are on different sides of inequality

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-10-28 03:16:12 -07:00
parent ef500de2d2
commit e13e85c4ab
2 changed files with 3 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/math/lp/nla_stellensatz.cpp
View file

@ -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) {

1
src/math/lp/nra_solver.cpp
View file

@ -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);