From 3dcfbb8347485a01413bc85b2491598eec163c9e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 25 Sep 2019 18:57:45 -0700 Subject: [PATCH] fix #2585 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/arith_rewriter.cpp | 2 +- src/smt/theory_arith_nl.h | 8 +++----- 2 files changed, 4 insertions(+), 6 deletions(-) diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index c6e8b9d62..c9df5bb37 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -478,7 +478,7 @@ br_status arith_rewriter::mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kin return BR_REWRITE_FULL; case EQ: result = m().mk_ite(is_zero, m().mk_eq(div0, arg2), m().mk_eq(e1, mul2)); - return BR_REWRITE2; + return BR_REWRITE_FULL; } } if ((m_arith_lhs || m_arith_ineq_lhs) && is_numeral(arg2, a2) && is_neg_poly(arg1, new_arg1)) { diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h index 14824c59e..78c3e2a39 100644 --- a/src/smt/theory_arith_nl.h +++ b/src/smt/theory_arith_nl.h @@ -811,15 +811,13 @@ namespace smt { bool theory_arith::is_monomial_linear(expr * m) const { SASSERT(is_pure_monomial(m)); unsigned num_nl_vars = 0; - for (unsigned i = 0; i < to_app(m)->get_num_args(); i++) { - expr * arg = to_app(m)->get_arg(i); + for (expr* arg : *to_app(m)) { theory_var _var = expr2var(arg); if (!is_fixed(_var)) { num_nl_vars++; } - else { - if (lower_bound(_var).is_zero()) - return true; + else if (lower_bound(_var).is_zero()) { + return true; } } return num_nl_vars <= 1;