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; }