diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 5d4eb3fc5..b1296f71e 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -1084,11 +1084,7 @@ namespace opt { } term = m_arith.mk_add(args.size(), args.c_ptr()); } - else if (m_arith.is_arith_expr(term) && !is_mul_const(term)) { - TRACE("opt", tout << "Purifying " << term << "\n";); - term = purify(fm, term); - } - else if (m.is_ite(term)) { + else if (m.is_ite(term) || !is_mul_const(term)) { TRACE("opt", tout << "Purifying " << term << "\n";); term = purify(fm, term); }