mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
604e6b2705
commit
e17b43617c
|
@ -274,9 +274,8 @@ bool arith_rewriter::elim_to_real_pol(expr * p, expr_ref & new_p) {
|
|||
if (m_util.is_add(p)) {
|
||||
expr_ref_buffer new_monomials(m());
|
||||
expr_ref new_monomial(m());
|
||||
unsigned num = to_app(p)->get_num_args();
|
||||
for (unsigned i = 0; i < num; i++) {
|
||||
if (!elim_to_real_mon(to_app(p)->get_arg(i), new_monomial))
|
||||
for (expr* arg : *to_app(p)) {
|
||||
if (!elim_to_real_mon(arg, new_monomial))
|
||||
return false;
|
||||
new_monomials.push_back(new_monomial);
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue