From 73a8f9960f264163978ab76355a978eccb35577e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 7 Sep 2015 20:17:46 -0700 Subject: [PATCH] fix regressions exposed in Internal Signed-off-by: Nikolaj Bjorner --- src/smt/theory_arith_aux.h | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index 565181877..886791fec 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -1310,17 +1310,17 @@ namespace smt { inf_numeral& max_gain, // maximal possible gain on x_j bool& has_shared, // determine if pivot involves shared variable theory_var& x_i) { // base variable to pivot with x_j - + + context& ctx = get_context(); + x_i = null_theory_var; + init_gains(x_j, inc, min_gain, max_gain); + has_shared |= ctx.is_shared(get_enode(x_j)); if (is_int(x_j) && !get_value(x_j).is_int()) { return false; - } - x_i = null_theory_var; - context& ctx = get_context(); + } column & c = m_columns[x_j]; typename svector::iterator it = c.begin_entries(); typename svector::iterator end = c.end_entries(); - init_gains(x_j, inc, min_gain, max_gain); - has_shared |= ctx.is_shared(get_enode(x_j)); bool empty_column = true; for (; it != end; ++it) { if (it->is_dead()) continue; @@ -1407,7 +1407,6 @@ namespace smt { SASSERT(max_gain.is_minus_one() || !max_gain.is_neg()); SASSERT(min_gain.is_minus_one() || min_gain.is_one()); - SASSERT(!is_int(x) || max_gain.is_int()); SASSERT(is_int(x) == min_gain.is_one()); } @@ -1556,7 +1555,7 @@ namespace smt { SASSERT(!picked_var || safe_gain(curr_min_gain, curr_max_gain)); - if (!picked_var && r.size() > 1) { + if (!picked_var && (r.size() > 1 || !safe_gain(curr_min_gain, curr_max_gain))) { TRACE("opt", tout << "no variable picked\n";); best_efforts++; }