mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

#5223

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-05-01 16:43:54 -07:00
parent 7835388361
commit 323e0e6270
1 changed files with 5 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/ast/arith_decl_plugin.cpp
View file

@ -898,7 +898,8 @@ bool arith_util::is_extended_numeral(expr* term, rational& r) const {
continue; continue;
} }
if (is_mul(term)) { if (is_mul(term)) {
rational r(mul), n(0); r = mul;
rational n(0);
for (expr* arg : *to_app(term)) { for (expr* arg : *to_app(term)) {
if (!is_extended_numeral(arg, n)) if (!is_extended_numeral(arg, n))
return false; return false;
@ -907,7 +908,8 @@ bool arith_util::is_extended_numeral(expr* term, rational& r) const {
return true; return true;
} }
if (is_add(term)) { if (is_add(term)) {
rational r(0), n(0); rational n(0);
r = 0;
for (expr* arg : *to_app(term)) { for (expr* arg : *to_app(term)) {
if (!is_extended_numeral(arg, n)) if (!is_extended_numeral(arg, n))
return false; return false;
@ -921,8 +923,7 @@ bool arith_util::is_extended_numeral(expr* term, rational& r) const {
if (is_sub(term, t1, t2) && if (is_sub(term, t1, t2) &&
is_extended_numeral(t1, k1) && is_extended_numeral(t1, k1) &&
is_extended_numeral(t2, k2)) { is_extended_numeral(t2, k2)) {
r = k1 - k2; r = (k1 - k2) * mul;
r *= mul;
return true; return true;
} }
return false; return false;