mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-01 06:37:49 +00:00
Code Activity

convert z3_exception to tactic exception in try_for

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-04-26 16:37:39 -07:00
parent 7461103802
commit 63003b5795
1 changed files with 6 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/tactic/tactical.cpp
View file

@ -1058,10 +1058,13 @@ public:
scoped_timer timer(m_timeout, &eh); scoped_timer timer(m_timeout, &eh);
try { try {
m_t->operator()(in, result); m_t->operator()(in, result);
} catch (z3_exception &) { } catch (z3_error &ex) {
if (in->m().limit().is_canceled()) throw ex;
return; } catch (tactic_exception &) {
throw; throw;
} catch (z3_exception &ex) {
// convert all Z3 exceptions into tactic exceptions.
throw tactic_exception(ex.what());
} }
} }
} }