From 0b1d5645097d41eec4c43946407e08d57b41ad64 Mon Sep 17 00:00:00 2001
From: hume <hume@hmz.local>
Date: Tue, 14 Mar 2017 18:11:00 +0800
Subject: [PATCH] added no exception support to z3++.h

---
 src/api/c++/z3++.h | 22 ++++++++++++++--------
 1 file changed, 14 insertions(+), 8 deletions(-)

diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index bfd4eb2c4..ac0e2c84a 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -86,7 +86,13 @@ namespace z3 {
     };
     inline std::ostream & operator<<(std::ostream & out, exception const & e) { out << e.msg(); return out; }
 
-
+#if !defined(Z3_THROW)
+#if __cpp_exceptions || _CPPUNWIND
+#define Z3_THROW(x) throw x
+#else
+#define Z3_THROW(x) {}
+#endif
+#endif // !defined(Z3_THROW)
 
     /**
        \brief Z3 global configuration object.
@@ -165,7 +171,7 @@ namespace z3 {
         Z3_error_code check_error() const {
             Z3_error_code e = Z3_get_error_code(m_ctx);
             if (e != Z3_OK && enable_exceptions())
-                throw exception(Z3_get_error_msg(m_ctx, e));
+                Z3_THROW(exception(Z3_get_error_msg(m_ctx, e)));
             return e;
         }
 
@@ -701,7 +707,7 @@ namespace z3 {
             if (!is_numeral_i(result)) {
                 assert(ctx().enable_exceptions());
                 if (!ctx().enable_exceptions()) return 0;
-                throw exception("numeral does not fit in machine int");
+                Z3_THROW(exception("numeral does not fit in machine int"));
             }
             return result;
         }
@@ -721,7 +727,7 @@ namespace z3 {
             if (!is_numeral_u(result)) {
                 assert(ctx().enable_exceptions());
                 if (!ctx().enable_exceptions()) return 0;
-                throw exception("numeral does not fit in machine uint");
+                Z3_THROW(exception("numeral does not fit in machine uint"));
             }
             return result;
         }
@@ -738,7 +744,7 @@ namespace z3 {
             if (!is_numeral_i64(result)) {
                 assert(ctx().enable_exceptions());
                 if (!ctx().enable_exceptions()) return 0;
-                throw exception("numeral does not fit in machine __int64");
+                Z3_THROW(exception("numeral does not fit in machine __int64"));
             }
             return result;
         }
@@ -755,7 +761,7 @@ namespace z3 {
             if (!is_numeral_u64(result)) {
                 assert(ctx().enable_exceptions());
                 if (!ctx().enable_exceptions()) return 0;
-                throw exception("numeral does not fit in machine __uint64");
+                Z3_THROW(exception("numeral does not fit in machine __uint64"));
             }
             return result;
         }
@@ -1699,7 +1705,7 @@ namespace z3 {
             Z3_bool status = Z3_model_eval(ctx(), m_model, n, model_completion, &r);
             check_error();
             if (status == Z3_FALSE && ctx().enable_exceptions())
-                throw exception("failed to evaluate expression");
+                Z3_THROW(exception("failed to evaluate expression"));
             return expr(ctx(), r);
         }
 
@@ -2023,7 +2029,7 @@ namespace z3 {
     }
     inline tactic par_or(unsigned n, tactic const* tactics) {
         if (n == 0) {
-            throw exception("a non-zero number of tactics need to be passed to par_or");
+            Z3_THROW(exception("a non-zero number of tactics need to be passed to par_or"));
         }
         array<Z3_tactic> buffer(n);
         for (unsigned i = 0; i < n; ++i) buffer[i] = tactics[i];