From 29a28f544df0e71c82de58dec0d5f9f110a46bfc Mon Sep 17 00:00:00 2001
From: Nicola Mometto <me@bronsa.net>
Date: Tue, 27 Nov 2018 12:15:33 +0000
Subject: [PATCH 1/2] catch and print exceptions in Z3_mk_config instead of
 letting them bubble up the stack

---
 src/api/api_config_params.cpp | 15 +++++++++++----
 1 file changed, 11 insertions(+), 4 deletions(-)

diff --git a/src/api/api_config_params.cpp b/src/api/api_config_params.cpp
index 54b3c5795..60d5fa556 100644
--- a/src/api/api_config_params.cpp
+++ b/src/api/api_config_params.cpp
@@ -68,10 +68,17 @@ extern "C" {
     }
 
     Z3_config Z3_API Z3_mk_config(void) {
-        memory::initialize(UINT_MAX);
-        LOG_Z3_mk_config();
-        Z3_config r = reinterpret_cast<Z3_config>(alloc(context_params));
-        RETURN_Z3(r);
+        try {
+            memory::initialize(UINT_MAX);
+            LOG_Z3_mk_config();
+            Z3_config r = reinterpret_cast<Z3_config>(alloc(context_params));
+            RETURN_Z3(r);
+        } catch (z3_exception & ex) {
+            // The error handler is only available for contexts
+            // Just throw a warning.
+            warning_msg("%s", ex.msg());
+            return nullptr;
+        }
     }
     
     void Z3_API Z3_del_config(Z3_config c) {

From 21158d87e30a7c6683d8505254e4d10f53361a50 Mon Sep 17 00:00:00 2001
From: Nicola Mometto <me@bronsa.net>
Date: Tue, 27 Nov 2018 12:15:57 +0000
Subject: [PATCH 2/2] override n_mk_config in ml bindings to catch exception
 path

---
 scripts/update_api.py           |  8 ++++++++
 src/api/ml/z3native_stubs.c.pre | 18 ++++++++++++++++++
 2 files changed, 26 insertions(+)

diff --git a/scripts/update_api.py b/scripts/update_api.py
index 901ea4fda..65791399c 100755
--- a/scripts/update_api.py
+++ b/scripts/update_api.py
@@ -1335,6 +1335,10 @@ z3_long_funs = frozenset([
     'Z3_simplify_ex',
     ])
 
+z3_ml_overrides = frozenset([
+    'Z3_mk_config'
+    ])
+
 def mk_z3native_stubs_c(ml_src_dir, ml_output_dir): # C interface
     ml_wrapperf = os.path.join(ml_output_dir, 'z3native_stubs.c')
     ml_wrapper = open(ml_wrapperf, 'w')
@@ -1346,6 +1350,10 @@ def mk_z3native_stubs_c(ml_src_dir, ml_output_dir): # C interface
     ml_pref.close()
 
     for name, result, params in _dotnet_decls:
+
+        if name in z3_ml_overrides:
+            continue
+
         ip = inparams(params)
         op = outparams(params)
         ap = arrayparams(params)
diff --git a/src/api/ml/z3native_stubs.c.pre b/src/api/ml/z3native_stubs.c.pre
index 71ee18ce9..4d221aac3 100644
--- a/src/api/ml/z3native_stubs.c.pre
+++ b/src/api/ml/z3native_stubs.c.pre
@@ -448,3 +448,21 @@ CAMLprim value DLL_PUBLIC n_set_internal_error_handler(value ctx_v)
   Z3_set_error_handler(ctx_p->ctx, MLErrorHandler);
   CAMLreturn(Val_unit);
 }
+
+CAMLprim DLL_PUBLIC value n_mk_config() {
+  CAMLparam0();
+  CAMLlocal1(result);
+  Z3_config z3rv;
+
+  /* invoke Z3 function */
+  z3rv = Z3_mk_config();
+
+  if (z3rv == NULL) {
+    caml_raise_with_string(*caml_named_value("Z3EXCEPTION"), "internal error");
+  }
+
+  /* construct simple return value */
+  result = caml_alloc_custom(&default_custom_ops, sizeof(Z3_config), 0, 1); *(Z3_config*)Data_custom_val(result) = z3rv;
+  /* cleanup and return */
+  CAMLreturn(result);
+}