From 7f219e84de434d57631940b1d7ad1862dacd918a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 29 Aug 2015 15:51:58 -0700 Subject: [PATCH] check cancellation flag in min/max. Fixes issue #206 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_arith_aux.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index 60af00195..7e9baeebc 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -1530,7 +1530,7 @@ namespace smt { max_min_t result = OPTIMIZED; has_shared = false; unsigned max_efforts = 10 + (ctx.get_random_value() % 20); - while (best_efforts < max_efforts) { + while (best_efforts < max_efforts && !ctx.get_cancel_flag()) { theory_var x_j = null_theory_var; theory_var x_i = null_theory_var; max_gain.reset(); @@ -1692,7 +1692,7 @@ namespace smt { SASSERT(satisfy_bounds()); } TRACE("opt", display(tout);); - return (best_efforts>0)?BEST_EFFORT:result; + return (best_efforts>0 || ctx.get_cancel_flag())?BEST_EFFORT:result; } /**