more detailed tracing of where unmaterialized exceptions happen

Signed-off-by: Nikolaj Bjorner <[email protected]>

Author: NikolajBjorner

src/api/api_solver.cpp

@@ -628,6 +628,9 @@ extern "C" {
         Z3_CATCH_RETURN(nullptr);
     }
 
+#define STRINGIFY(x) #x
+#define TOSTRING(x) STRINGIFY(x)    
+
     static Z3_lbool _solver_check(Z3_context c, Z3_solver s, unsigned num_assumptions, Z3_ast const assumptions[]) {
         for (unsigned i = 0; i < num_assumptions; i++) {
             if (!is_expr(to_ast(assumptions[i]))) {
@@ -662,15 +665,15 @@ extern "C" {
                 }
                 return Z3_L_UNDEF;
             }
-            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);
                 return Z3_L_UNDEF;
             }
         }
         to_solver(s)->set_eh(nullptr);
         if (result == l_undef) {
-            to_solver_ref(s)->set_reason_unknown(eh);
+            to_solver_ref(s)->set_reason_unknown(eh, __FILE__ ":" TOSTRING(__LINE__));
         }
         return static_cast<Z3_lbool>(result);
     }
@@ -887,7 +890,7 @@ extern "C" {
         }
         to_solver(s)->set_eh(nullptr);
         if (result == l_undef) {
-            to_solver_ref(s)->set_reason_unknown(eh);
+            to_solver_ref(s)->set_reason_unknown(eh, __FILE__ ":" TOSTRING(__LINE__));
         }
         for (expr* e : _consequences) {
             to_ast_vector_ref(consequences).push_back(e);

src/cmd_context/cmd_context.cpp

@@ -1782,19 +1782,15 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
         try {
             r = m_solver->check_sat(num_assumptions, assumptions);
             if (r == l_undef && !m().inc()) {
-                m_solver->set_reason_unknown(eh);
+                m_solver->set_reason_unknown(eh, "canceled");
             }
         }
         catch (z3_error & ex) {
+            m_solver->set_reason_unknown(eh, ex);
             throw ex;
         }
         catch (z3_exception & ex) {
-            if (!m().inc()) {
-                m_solver->set_reason_unknown(eh);
-            }
-            else {
-                m_solver->set_reason_unknown(ex.what());
-            }
+            m_solver->set_reason_unknown(eh, ex);
             r = l_undef;
         }
         m_solver->set_status(r);

src/solver/check_sat_result.cpp

@@ -18,11 +18,11 @@ Module Name:
 --*/
 #include "solver/check_sat_result.h"
 
-void check_sat_result::set_reason_unknown(event_handler& eh) {
+void check_sat_result::set_reason_unknown(event_handler& eh, char const* what) {
     switch (eh.caller_id()) {
     case UNSET_EH_CALLER: 
         if (reason_unknown() == "")
-            set_reason_unknown("unclassified exception");
+            set_reason_unknown(what);
         break;
     case CTRL_C_EH_CALLER:
         set_reason_unknown("interrupted from keyboard");
@@ -46,7 +46,7 @@ void check_sat_result::set_reason_unknown(event_handler& eh, std::exception& ex)
             set_reason_unknown(ex.what());
         break;
     default:
-        set_reason_unknown(eh);
+        set_reason_unknown(eh, ex.what());
         break;
     }
 }

src/solver/check_sat_result.h

@@ -68,7 +68,7 @@ class check_sat_result {
     virtual proof * get_proof_core() = 0;
     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, char const* msg);
     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;