Implement API to set exit action to exception

src/api/CMakeLists.txt

@@ -44,6 +44,7 @@ z3_add_component(api
     api_context.cpp
     api_datalog.cpp
     api_datatype.cpp
+    api_debug.cpp
     api_fpa.cpp
     api_goal.cpp
     api_log.cpp

src/api/api_debug.cpp

@@ -0,0 +1,8 @@
+#include "api/z3.h"
+#include "util/util.h"
+
+extern "C" {
+    void Z3_API Z3_set_exit_action_to_throw_exception() {
+        set_default_exit_action(exit_action::throw_exception);
+    }
+}

src/api/python/z3/z3.py

@@ -316,6 +316,11 @@ def get_param(name):
         return r
     raise Z3Exception("failed to retrieve value for '%s'" % name)
 
+
+def set_exit_action_to_throw_exception():
+    """Set the debug exit action to throw exception"""
+    Z3_set_exit_action_to_throw_exception()
+
 #########################################
 #
 # ASTs base class

src/api/z3_api.h

@@ -7455,6 +7455,13 @@ extern "C" {
 
     /**@}*/
 
+    /**
+    \brief Set exit action to throw exception.
+
+    def_API('Z3_set_exit_action_to_throw_exception', VOID, ())
+    */
+    void Z3_API Z3_set_exit_action_to_throw_exception();
+
 #ifdef __cplusplus
 }
 #endif // __cplusplus

src/util/debug.cpp

@@ -75,6 +75,37 @@ bool is_debug_enabled(const char * tag) {
     return g_enabled_debug_tags->contains(tag);
 }
 
+atomic<exit_action> g_default_exit_action(exit_action::exit);
+
+exit_action get_default_exit_action() {
+    return g_default_exit_action;
+}
+
+void set_default_exit_action(exit_action a) {
+    g_default_exit_action = a;
+}
+
+void invoke_exit_action(unsigned int code) {
+    exit_action a = get_default_exit_action();
+    switch (a) {
+    case exit_action::exit:
+        exit(code);
+    case exit_action::throw_exception:
+        switch (code) {
+            case ERR_INTERNAL_FATAL:
+                throw default_exception("internal fatal");
+            case ERR_UNREACHABLE:
+                throw default_exception("unreachable");
+            case ERR_NOT_IMPLEMENTED_YET:
+                throw default_exception("not implemented yet");
+            default:
+                throw default_exception("unknown");
+        }
+    default:
+        exit(code);
+    }
+}
+
 atomic<debug_action> g_default_debug_action(debug_action::ask);
 
 debug_action get_default_debug_action() {

src/util/debug.h

@@ -35,6 +35,14 @@ enum class debug_action {
 debug_action get_default_debug_action();
 void set_default_debug_action(debug_action a);
 
+enum class exit_action {
+    exit,
+    throw_exception,
+};
+exit_action get_default_exit_action();
+void set_default_exit_action(exit_action a);
+void invoke_exit_action(unsigned int code);
+
 #include "util/error_codes.h"
 #include "util/warning.h"
 
@@ -56,7 +64,7 @@ void set_default_debug_action(debug_action a);
 #endif
 
 #ifdef NO_Z3_DEBUGGER
-#define INVOKE_DEBUGGER() exit(ERR_INTERNAL_FATAL)
+#define INVOKE_DEBUGGER() invoke_exit_action(ERR_INTERNAL_FATAL)
 #else
 #ifdef _WINDOWS
 #define INVOKE_DEBUGGER() __debugbreak()
@@ -71,6 +79,7 @@ void enable_debug(const char * tag);
 void disable_debug(const char * tag);
 bool is_debug_enabled(const char * tag);
 
+
 #define SASSERT(COND) DEBUG_CODE(if (assertions_enabled() && !(COND)) { notify_assertion_violation(__FILE__, __LINE__, #COND); INVOKE_DEBUGGER(); })
 #define CASSERT(TAG, COND) DEBUG_CODE(if (assertions_enabled() && is_debug_enabled(TAG) && !(COND)) { notify_assertion_violation(__FILE__, __LINE__, #COND); INVOKE_DEBUGGER(); })
 #define XASSERT(COND, EXTRA_CODE) DEBUG_CODE(if (assertions_enabled() && !(COND)) { notify_assertion_violation(__FILE__, __LINE__, #COND); { EXTRA_CODE } INVOKE_DEBUGGER(); })
@@ -85,25 +94,25 @@ bool is_debug_enabled(const char * tag);
 #ifdef Z3DEBUG
 # define UNREACHABLE() DEBUG_CODE(notify_assertion_violation(__FILE__, __LINE__, "UNEXPECTED CODE WAS REACHED."); INVOKE_DEBUGGER();)
 #else
-# define UNREACHABLE() { notify_assertion_violation(__FILE__, __LINE__, "UNEXPECTED CODE WAS REACHED."); exit(ERR_UNREACHABLE); } ((void) 0)
+# define UNREACHABLE() { notify_assertion_violation(__FILE__, __LINE__, "UNEXPECTED CODE WAS REACHED."); invoke_exit_action(ERR_UNREACHABLE); } ((void) 0)
 #endif
 
 #ifdef Z3DEBUG
 # define NOT_IMPLEMENTED_YET() DEBUG_CODE(notify_assertion_violation(__FILE__, __LINE__, "NOT IMPLEMENTED YET!"); INVOKE_DEBUGGER();)
 #else
-# define NOT_IMPLEMENTED_YET() { notify_assertion_violation(__FILE__, __LINE__, "NOT IMPLEMENTED YET!"); exit(ERR_NOT_IMPLEMENTED_YET); } ((void) 0)
+# define NOT_IMPLEMENTED_YET() { notify_assertion_violation(__FILE__, __LINE__, "NOT IMPLEMENTED YET!"); invoke_exit_action(ERR_NOT_IMPLEMENTED_YET); } ((void) 0)
 #endif
 
 #define VERIFY(_x_) if (!(_x_)) {                                                       \
         notify_assertion_violation(__FILE__, __LINE__, "Failed to verify: " #_x_ "\n"); \
-        exit(ERR_UNREACHABLE);                                                          \
+        invoke_exit_action(ERR_UNREACHABLE);                                                          \
     }
 
 #define VERIFY_EQ(LHS, RHS)                                                                         \
     if (!((LHS) == (RHS))) {                                                                        \
         notify_assertion_violation(__FILE__, __LINE__, "Failed to verify: " #LHS " == " #RHS "\n"); \
         std::cerr << "LHS value: " << (LHS) << "\nRHS value: " << (RHS) << "\n";                    \
-        exit(ERR_UNREACHABLE);                                                                      \
+        invoke_exit_action(ERR_UNREACHABLE);                                                                      \
     }
 
 #define ENSURE(_x_) VERIFY(_x_)