diff --git a/examples/java/JavaExample.java b/examples/java/JavaExample.java
index a26c21d65..c2743ece8 100644
--- a/examples/java/JavaExample.java
+++ b/examples/java/JavaExample.java
@@ -2155,7 +2155,7 @@ class JavaExample
// But you cannot mix numerals of different sorts
// even if the size of their domains are the same:
// System.out.println(ctx.mkEq(s1, t1));
- }
+ }
public static void main(String[] args)
{
@@ -2226,7 +2226,7 @@ class JavaExample
Context ctx = new Context(cfg);
p.quantifierExample3(ctx);
p.quantifierExample4(ctx);
- }
+ }
Log.close();
if (Log.isOpen())
diff --git a/scripts/update_api.py b/scripts/update_api.py
index 08dd012e3..fa6111482 100644
--- a/scripts/update_api.py
+++ b/scripts/update_api.py
@@ -395,8 +395,7 @@ def mk_dotnet():
dotnet.write(' public delegate void Z3_error_handler(Z3_context c, Z3_error_code e);\n\n')
dotnet.write(' public unsafe class LIB\n')
dotnet.write(' {\n')
- dotnet.write(' '
- ' const string Z3_DLL_NAME = \"libz3.dll\";\n'
+ dotnet.write(' const string Z3_DLL_NAME = \"libz3.dll\";\n'
' \n');
dotnet.write(' [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]\n')
dotnet.write(' public extern static void Z3_set_error_handler(Z3_context a0, Z3_error_handler a1);\n\n')
@@ -420,7 +419,8 @@ def mk_dotnet():
dotnet.write(' }\n')
-DotnetUnwrapped = [ 'Z3_del_context' ]
+NULLWrapped = [ 'Z3_mk_context', 'Z3_mk_context_rc' ]
+Unwrapped = [ 'Z3_del_context' ]
def mk_dotnet_wrappers():
global Type2Str
@@ -469,11 +469,15 @@ def mk_dotnet_wrappers():
dotnet.write('a%d' % i)
i = i + 1
dotnet.write(');\n');
- if name not in DotnetUnwrapped:
- if len(params) > 0 and param_type(params[0]) == CONTEXT:
- dotnet.write(" Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);\n")
- dotnet.write(" if (err != Z3_error_code.Z3_OK)\n")
- dotnet.write(" throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));\n")
+ if name not in Unwrapped:
+ if name in NULLWrapped:
+ dotnet.write(" if (r == IntPtr.Zero)\n")
+ dotnet.write(" throw new Z3Exception(\"Object allocation failed.\");\n")
+ else:
+ if len(params) > 0 and param_type(params[0]) == CONTEXT:
+ dotnet.write(" Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);\n")
+ dotnet.write(" if (err != Z3_error_code.Z3_OK)\n")
+ dotnet.write(" throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));\n")
if result == STRING:
dotnet.write(" return Marshal.PtrToStringAnsi(r);\n")
elif result != VOID:
@@ -550,7 +554,7 @@ def mk_java():
java_native.write('%s a%d' % (param2java(param), i))
i = i + 1
java_native.write(')')
- if len(params) > 0 and param_type(params[0]) == CONTEXT:
+ if (len(params) > 0 and param_type(params[0]) == CONTEXT) or name in NULLWrapped:
java_native.write(' throws Z3Exception')
java_native.write('\n')
java_native.write(' {\n')
@@ -568,10 +572,15 @@ def mk_java():
java_native.write('a%d' % i)
i = i + 1
java_native.write(');\n')
- if len(params) > 0 and param_type(params[0]) == CONTEXT:
- java_native.write(' Z3_error_code err = Z3_error_code.fromInt(INTERNALgetErrorCode(a0));\n')
- java_native.write(' if (err != Z3_error_code.Z3_OK)\n')
- java_native.write(' throw new Z3Exception(INTERNALgetErrorMsgEx(a0, err.toInt()));\n')
+ if name not in Unwrapped:
+ if name in NULLWrapped:
+ java_native.write(" if (res == 0)\n")
+ java_native.write(" throw new Z3Exception(\"Object allocation failed.\");\n")
+ else:
+ if len(params) > 0 and param_type(params[0]) == CONTEXT:
+ java_native.write(' Z3_error_code err = Z3_error_code.fromInt(INTERNALgetErrorCode(a0));\n')
+ java_native.write(' if (err != Z3_error_code.Z3_OK)\n')
+ java_native.write(' throw new Z3Exception(INTERNALgetErrorMsgEx(a0, err.toInt()));\n')
if result != VOID:
java_native.write(' return res;\n')
java_native.write(' }\n\n')
diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp
index 6106cb6c7..cf179332a 100644
--- a/src/api/api_context.cpp
+++ b/src/api/api_context.cpp
@@ -419,17 +419,21 @@ namespace api {
extern "C" {
Z3_context Z3_API Z3_mk_context(Z3_config c) {
+ Z3_TRY;
LOG_Z3_mk_context(c);
memory::initialize(UINT_MAX);
Z3_context r = reinterpret_cast<Z3_context>(alloc(api::context, reinterpret_cast<context_params*>(c), false));
RETURN_Z3(r);
+ Z3_CATCH_RETURN_NO_HANDLE(0);
}
Z3_context Z3_API Z3_mk_context_rc(Z3_config c) {
+ Z3_TRY;
LOG_Z3_mk_context_rc(c);
memory::initialize(UINT_MAX);
Z3_context r = reinterpret_cast<Z3_context>(alloc(api::context, reinterpret_cast<context_params*>(c), true));
RETURN_Z3(r);
+ Z3_CATCH_RETURN_NO_HANDLE(0);
}
void Z3_API Z3_del_context(Z3_context c) {
diff --git a/src/api/api_util.h b/src/api/api_util.h
index c81384f2f..58abf97bf 100644
--- a/src/api/api_util.h
+++ b/src/api/api_util.h
@@ -26,6 +26,7 @@ Revision History:
#define Z3_CATCH_CORE(CODE) } catch (z3_exception & ex) { mk_c(c)->handle_exception(ex); CODE }
#define Z3_CATCH Z3_CATCH_CORE(return;)
#define Z3_CATCH_RETURN(VAL) Z3_CATCH_CORE(return VAL;)
+#define Z3_CATCH_RETURN_NO_HANDLE(VAL) } catch (z3_exception &) { return VAL; }
#define CHECK_REF_COUNT(a) (reinterpret_cast<ast const*>(a)->get_ref_count() > 0)
#define VALIDATE(a) SASSERT(!a || CHECK_REF_COUNT(a))
diff --git a/src/api/java/Context.java b/src/api/java/Context.java
index 7a1a404af..3ad136f12 100644
--- a/src/api/java/Context.java
+++ b/src/api/java/Context.java
@@ -3053,10 +3053,10 @@ public class Context extends IDisposable
// OK.
}
m_ctx = 0;
- } else
- /* re-queue the finalizer */
- /* BUG: DRQ's need to be taken over too! */
- new Context(m_ctx, m_refCount);
+ }
+ /*
+ else
+ CMW: re-queue the finalizer? */
}
/**