From 9743c188da732ccdb775ba04e7061f08811c43b2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 8 Mar 2016 17:00:12 -0800 Subject: [PATCH] add exception handling for making solver-1 discontinuation transparent, thanks to Martin, #497 Signed-off-by: Nikolaj Bjorner --- src/solver/combined_solver.cpp | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp index 338a4a7da..858885d9d 100644 --- a/src/solver/combined_solver.cpp +++ b/src/solver/combined_solver.cpp @@ -212,11 +212,16 @@ public: else { IF_VERBOSE(PS_VB_LVL, verbose_stream() << "(combined-solver \"using solver 2 (with timeout)\")\n";); aux_timeout_eh eh(m_solver2.get()); - lbool r; - { + lbool r = l_undef; + try { scoped_timer timer(m_inc_timeout, &eh); r = m_solver2->check_sat(0, 0); } + catch (z3_exception&) { + if (!eh.m_canceled) { + throw; + } + } if ((r != l_undef || !use_solver1_when_undef()) && !eh.m_canceled) { return r; }