From aeee44398d1b70471afdcbe8e7733a672499b325 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 30 Mar 2020 12:40:15 -0700 Subject: [PATCH] fix #3594 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_arith_nl.h | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h index fe23240d2..34297c172 100644 --- a/src/smt/theory_arith_nl.h +++ b/src/smt/theory_arith_nl.h @@ -794,7 +794,7 @@ bool theory_arith::branch_nl_int_var(theory_var v) { TRACE("non_linear", tout << "BRANCHING on v" << v << "\n";); m_stats.m_nl_branching++; SASSERT(is_int(v)); - expr * bound = nullptr; + expr_ref bound(get_manager()); if (lower(v)) bound = m_util.mk_le(var2expr(v), m_util.mk_numeral(lower_bound(v).get_rational().to_rational(), true)); else if (upper(v)) @@ -825,8 +825,7 @@ template 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++;