From 63003b5795b4188693b515cf06a5eb2b2bc084ee Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 26 Apr 2026 16:37:39 -0700 Subject: [PATCH] convert z3_exception to tactic exception in try_for Signed-off-by: Nikolaj Bjorner --- src/tactic/tactical.cpp | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp index a7024aeac..22e0f498b 100644 --- a/src/tactic/tactical.cpp +++ b/src/tactic/tactical.cpp @@ -1058,10 +1058,13 @@ public: scoped_timer timer(m_timeout, &eh); try { m_t->operator()(in, result); - } catch (z3_exception &) { - if (in->m().limit().is_canceled()) - return; + } catch (z3_error &ex) { + throw ex; + } catch (tactic_exception &) { throw; + } catch (z3_exception &ex) { + // convert all Z3 exceptions into tactic exceptions. + throw tactic_exception(ex.what()); } } }