diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h index 79337f4fe..025ec76d1 100644 --- a/src/smt/theory_arith_nl.h +++ b/src/smt/theory_arith_nl.h @@ -166,6 +166,8 @@ std::pair theory_arith::analyze_monomial(expr * m) const { int idx = 0; for (unsigned i = 0; i < to_app(m)->get_num_args(); i++) { expr * arg = to_app(m)->get_arg(i); + if (m_util.is_numeral(arg)) + continue; if (var == nullptr) { var = arg; power = 1;