diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index 886791fec..106a038e4 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -1555,7 +1555,7 @@ namespace smt { SASSERT(!picked_var || safe_gain(curr_min_gain, curr_max_gain)); - if (!picked_var && (r.size() > 1 || !safe_gain(curr_min_gain, curr_max_gain))) { + if (!picked_var) { // && (r.size() > 1 || !safe_gain(curr_min_gain, curr_max_gain)) TRACE("opt", tout << "no variable picked\n";); best_efforts++; }