add exception handling to easier diagnose #7418

Signed-off-by: Nikolaj Bjorner <[email protected]>
Z3Prover · Nov 19, 2024 · e855a50 · e855a50
1 parent 5168a13
commit e855a50
Show file tree

Hide file tree

Showing 3 changed files with 17 additions and 4 deletions.
diff --git 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
@@ -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
@@ -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;