mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-02 02:48:47 +00:00
Code Activity

fix segfault

Browse source
This commit is contained in:
Jakob Rath 2022-12-19 14:25:58 +01:00
parent 59592754d8
commit 868a3710e0
1 changed files with 7 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/math/polysat/univariate/univariate_solver.cpp
View file

@ -133,12 +133,13 @@ namespace polysat {
} }
// [d,c,b,a] --> d + c*x + b*(x*x) + a*(x*x*x) // [d,c,b,a] --> d + c*x + b*(x*x) + a*(x*x*x)
expr* mk_poly(univariate const& p) const { expr_ref mk_poly(univariate const& p) {
if (p.empty()) { expr_ref e(m);
return mk_numeral(rational::zero()); if (p.empty())
} e = mk_numeral(rational::zero());
else { else {
expr* e = p[0] != 0 ? mk_numeral(p[0]) : nullptr; if (!p[0].is_zero())
e = mk_numeral(p[0]);
expr_ref xpow = x; expr_ref xpow = x;
for (unsigned i = 1; i < p.size(); ++i) { for (unsigned i = 1; i < p.size(); ++i) {
if (!p[i].is_zero()) { if (!p[i].is_zero()) {
@ -150,8 +151,8 @@ namespace polysat {
} }
if (!e) if (!e)
e = mk_numeral(p[0]); e = mk_numeral(p[0]);
return e;
} }
return e;
} }
#endif #endif