From e855a50d9bc4d9c321836bad98b9a89cb2b88cf6 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 19 Nov 2024 11:46:54 -0800
Subject: [PATCH] add exception handling to easier diagnose #7418
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/api/api_solver.cpp | 8 ++++----
src/solver/check_sat_result.cpp | 12 ++++++++++++
src/solver/check_sat_result.h | 1 +
3 files changed, 17 insertions(+), 4 deletions(-)
diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp
index f226529de..41b53f97f 100644
--- a/src/api/api_solver.cpp
+++ b/src/api/api_solver.cpp
@@ -655,7 +655,7 @@ extern "C" {
result = to_solver_ref(s)->check_sat(num_assumptions, _assumptions);
}
catch (z3_exception & ex) {
- to_solver_ref(s)->set_reason_unknown(eh);
+ to_solver_ref(s)->set_reason_unknown(eh, ex);
to_solver(s)->set_eh(nullptr);
if (mk_c(c)->m().inc()) {
mk_c(c)->handle_exception(ex);
@@ -751,8 +751,8 @@ extern "C" {
try {
to_solver_ref(s)->get_unsat_core(core);
}
- catch (...) {
- to_solver_ref(s)->set_reason_unknown(eh);
+ catch (std::exception& ex) {
+ to_solver_ref(s)->set_reason_unknown(eh, ex);
to_solver(s)->set_eh(nullptr);
if (core.empty())
throw;
@@ -877,7 +877,7 @@ extern "C" {
}
catch (z3_exception & ex) {
to_solver(s)->set_eh(nullptr);
- to_solver_ref(s)->set_reason_unknown(eh);
+ to_solver_ref(s)->set_reason_unknown(eh, ex);
_assumptions.finalize(); _consequences.finalize(); _variables.finalize();
mk_c(c)->handle_exception(ex);
return Z3_L_UNDEF;
diff --git a/src/solver/check_sat_result.cpp b/src/solver/check_sat_result.cpp
index 944f717b9..0538991c9 100644
--- a/src/solver/check_sat_result.cpp
+++ b/src/solver/check_sat_result.cpp
@@ -39,6 +39,18 @@ void check_sat_result::set_reason_unknown(event_handler& eh) {
}
}
+void check_sat_result::set_reason_unknown(event_handler& eh, std::exception& ex) {
+ switch (eh.caller_id()) {
+ case UNSET_EH_CALLER:
+ if (reason_unknown() == "")
+ set_reason_unknown(ex.what());
+ break;
+ default:
+ set_reason_unknown(eh);
+ break;
+ }
+}
+
proof* check_sat_result::get_proof() {
if (!m_log.empty() && !m_proof) {
SASSERT(is_app(m_log.back()));
diff --git a/src/solver/check_sat_result.h b/src/solver/check_sat_result.h
index b992d260d..016c0533e 100644
--- a/src/solver/check_sat_result.h
+++ b/src/solver/check_sat_result.h
@@ -69,6 +69,7 @@ public:
virtual std::string reason_unknown() const = 0;
virtual void set_reason_unknown(char const* msg) = 0;
void set_reason_unknown(event_handler& eh);
+ void set_reason_unknown(event_handler& eh, std::exception& ex);
virtual void get_labels(svector<symbol> & r) = 0;
virtual ast_manager& get_manager() const = 0;