From 0e07b218bc05b5681aa70565b6b4a6a076be094a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 26 Apr 2026 13:11:59 -0700 Subject: [PATCH] exception protection for nlsat_tactic Signed-off-by: Nikolaj Bjorner --- src/nlsat/tactic/nlsat_tactic.cpp | 19 +++++++++++++++++-- 1 file changed, 17 insertions(+), 2 deletions(-) diff --git a/src/nlsat/tactic/nlsat_tactic.cpp b/src/nlsat/tactic/nlsat_tactic.cpp index c47a586f8..563f830fd 100644 --- a/src/nlsat/tactic/nlsat_tactic.cpp +++ b/src/nlsat/tactic/nlsat_tactic.cpp @@ -133,8 +133,23 @@ class nlsat_tactic : public tactic { return ok; } - void operator()(goal_ref const & g, - goal_ref_buffer & result) { + 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) { tactic_report report("nlsat", *g); if (g->is_decided()) {