From 6e852762baf568af2aad1e35019fdf41189e4e12 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 6 Oct 2015 19:07:47 -0700 Subject: [PATCH] patch for issue #232 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_arith_aux.h | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index 106a038e4..bad141e94 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -1593,6 +1593,13 @@ namespace smt { TRACE("opt", tout << "after traversing row:\nx_i: v" << x_i << ", x_j: v" << x_j << ", gain: " << max_gain << "\n"; tout << "best efforts: " << best_efforts << " has shared: " << has_shared << "\n";); + if (x_j == null_theory_var && x_i == null_theory_var) { + has_shared = false; + best_efforts = 0; + result = UNBOUNDED; + break; + } + if (x_j == null_theory_var) { TRACE("opt", tout << "row is " << (max ? "maximized" : "minimized") << "\n"; display_row(tout, r, true););