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 f226529de5a..41b53f97fff 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 944f717b998..0538991c9e8 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 b992d260da1..016c0533e97 100644
--- a/src/solver/check_sat_result.h
+++ b/src/solver/check_sat_result.h
@@ -69,6 +69,7 @@ class check_sat_result {
     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;