mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 13:29:11 +00:00
Code Activity

check cancellation flag in min/max. Fixes issue #206

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-08-29 15:51:58 -07:00
parent dd01f6be46
commit 7f219e84de
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/smt/theory_arith_aux.h
View file

@ -1530,7 +1530,7 @@ namespace smt {
max_min_t result = OPTIMIZED; max_min_t result = OPTIMIZED;
has_shared = false; has_shared = false;
unsigned max_efforts = 10 + (ctx.get_random_value() % 20); 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_j = null_theory_var;
theory_var x_i = null_theory_var; theory_var x_i = null_theory_var;
max_gain.reset(); max_gain.reset();
@ -1692,7 +1692,7 @@ namespace smt {
SASSERT(satisfy_bounds()); SASSERT(satisfy_bounds());
} }
TRACE("opt", display(tout);); TRACE("opt", display(tout););
return (best_efforts>0)?BEST_EFFORT:result; return (best_efforts>0 || ctx.get_cancel_flag())?BEST_EFFORT:result;
} }
/** /**