From 74611038028b01dd329cd6f9ba974f2dccbd7b89 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 26 Apr 2026 15:58:12 -0700 Subject: [PATCH] making try-for tactic exception resilient on cancelation Signed-off-by: Nikolaj Bjorner --- src/nlsat/tactic/nlsat_tactic.cpp | 18 +----------------- src/tactic/tactical.cpp | 8 +++++++- 2 files changed, 8 insertions(+), 18 deletions(-) diff --git a/src/nlsat/tactic/nlsat_tactic.cpp b/src/nlsat/tactic/nlsat_tactic.cpp index 563f830fd..c12c29570 100644 --- a/src/nlsat/tactic/nlsat_tactic.cpp +++ b/src/nlsat/tactic/nlsat_tactic.cpp @@ -133,23 +133,7 @@ class nlsat_tactic : public tactic { return ok; } - void operator()(goal_ref const &g, goal_ref_buffer &result) { - try { - check(g, result); - } - catch (z3_exception &ex) { - if (m.limit().is_canceled()) { - if (result.empty()) { - g->inc_depth(); - result.push_back(g.get()); - } - return; - } - throw; - } - } - - void check(goal_ref const & g, goal_ref_buffer & result) { + void operator()(goal_ref const & g, goal_ref_buffer & result) { tactic_report report("nlsat", *g); if (g->is_decided()) { diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp index 148873c03..a7024aeac 100644 --- a/src/tactic/tactical.cpp +++ b/src/tactic/tactical.cpp @@ -1056,7 +1056,13 @@ public: cancel_eh eh(in->m().limit()); { scoped_timer timer(m_timeout, &eh); - m_t->operator()(in, result); + try { + m_t->operator()(in, result); + } catch (z3_exception &) { + if (in->m().limit().is_canceled()) + return; + throw; + } } }