From 4f3f21bff157152f0fa8927c57ec7dd1810c4f23 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 23 Oct 2016 21:45:35 -0700 Subject: [PATCH] disable local optimization in presence of non-linear constraints, addresses issue #758 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_arith_aux.h | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index d2db3a603..50bfee20e 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -1056,6 +1056,11 @@ namespace smt { inf_eps_rational theory_arith::maximize(theory_var v, expr_ref& blocker, bool& has_shared) { TRACE("bound_bug", display_var(tout, v); display(tout);); has_shared = false; + if (!m_nl_monomials.empty()) { + has_shared = true; + blocker = mk_gt(v); + return inf_eps_rational(get_value(v)); + } max_min_t r = max_min(v, true, true, has_shared); if (r == UNBOUNDED) { has_shared = false; @@ -1300,6 +1305,7 @@ namespace smt { */ + template bool theory_arith::pick_var_to_leave( @@ -1331,7 +1337,7 @@ namespace smt { if (update_gains(inc, s, coeff_ij, min_gain, max_gain) || (x_i == null_theory_var && !unbounded_gain(max_gain))) { x_i = s; - a_ij = coeff_ij; + a_ij = coeff_ij; } has_shared |= ctx.is_shared(get_enode(s)); }