From d7da64f94632e30fee3870c3daa95424c08cdda2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 8 Sep 2015 16:27:57 -0700 Subject: [PATCH] fix crash with incorrect bound computation Signed-off-by: Nikolaj Bjorner --- src/smt/theory_arith_aux.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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++; }