From 6e03c7a54216f9da0a5cdbfb29a3a131a2b1ae09 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 3 May 2018 03:23:54 -0700 Subject: [PATCH] fix #1607 by filtering exceptions when the context is canceled Signed-off-by: Nikolaj Bjorner --- src/api/api_opt.cpp | 4 +++- src/api/api_solver.cpp | 4 +++- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/src/api/api_opt.cpp b/src/api/api_opt.cpp index 2712eef6f..7b8866b59 100644 --- a/src/api/api_opt.cpp +++ b/src/api/api_opt.cpp @@ -139,7 +139,9 @@ extern "C" { r = to_optimize_ptr(o)->optimize(); } catch (z3_exception& ex) { - mk_c(c)->handle_exception(ex); + if (!mk_c(c)->m().canceled()) { + mk_c(c)->handle_exception(ex); + } r = l_undef; } // to_optimize_ref(d).cleanup(); diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 1b2e9dcc3..88ce8b144 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -361,7 +361,9 @@ extern "C" { } catch (z3_exception & ex) { to_solver_ref(s)->set_reason_unknown(eh); - mk_c(c)->handle_exception(ex); + if (!mk_c(c)->m().canceled()) { + mk_c(c)->handle_exception(ex); + } return Z3_L_UNDEF; } }