From 88707f37e75c3c1d8fd54570af8da7135b3bfa2d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 2 Jan 2022 11:31:50 -0800 Subject: [PATCH] Better error reporting #5746 --- src/api/api_solver.cpp | 5 ++++- src/tactic/tactical.cpp | 4 ++++ 2 files changed, 8 insertions(+), 1 deletion(-) diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 8e8360cd3..43093d749 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -607,7 +607,10 @@ extern "C" { return Z3_L_UNDEF; } catch (...) { - to_solver_ref(s)->set_reason_unknown(eh); + if (eh.caller_id() == event_handler_caller_t::UNSET_EH_CALLER) + to_solver_ref(s)->set_reason_unknown("unclassified exception"); + else + to_solver_ref(s)->set_reason_unknown(eh); to_solver(s)->set_eh(nullptr); return Z3_L_UNDEF; } diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp index e6a3a024e..c5a9e6984 100644 --- a/src/tactic/tactical.cpp +++ b/src/tactic/tactical.cpp @@ -344,6 +344,10 @@ public: IF_VERBOSE(10, verbose_stream() << ex.msg() << " in or-else\n"); throw; } + catch (const std::exception &ex) { + IF_VERBOSE(10, verbose_stream() << ex.what() << " in or-else\n"); + throw; + } catch (...) { IF_VERBOSE(10, verbose_stream() << " unclassified exception in or-else\n"); // std::current_exception returns a std::exception_ptr, which apparently