mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 01:24:08 +00:00
Code Activity

fix #3241

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-03-12 07:55:16 -07:00
parent 67d19cba4a
commit 4e9005ac3d
1 changed files with 10 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/nlsat/nlsat_solver.cpp
View file

@ -642,13 +642,18 @@ namespace nlsat {
SASSERT(k == atom::LT || k == atom::GT || k == atom::EQ);
bool is_const = true;
polynomial::manager::scoped_numeral cnst(m_pm.m());
m_pm.m().set(cnst, 1);
for (unsigned i = 0; is_const && i < sz; ++i) {
m_pm.m().set(cnst, 1);
for (unsigned i = 0; i < sz; ++i) {
if (m_pm.is_const(ps[i])) {
if (m_pm.is_zero(ps[i])) {
m_pm.m().set(cnst, 0);
is_const = true;
break;
}
auto const& c = m_pm.coeff(ps[i], 0);
m_pm.m().mul(cnst, c, cnst);
if (is_even[i]) {
m_pm.m().mul(cnst, c, cnst);
if (is_even[i] && m_pm.m().is_neg(c)) {
m_pm.m().neg(cnst);
}
}
else {
@ -2707,8 +2712,8 @@ namespace nlsat {
if (m_pm.is_zero(pr)) {
ps.reset();
even.reset();
even.push_back(false);
ps.push_back(pr);
even.push_back(false);
break;
}
if (m_pm.is_const(pr)) {