From 2122fdee4557c22720be03b88645e8e2c379f65f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 19 Nov 2015 08:33:27 -0800 Subject: [PATCH] fix build script for update to name of get_error_msg Signed-off-by: Nikolaj Bjorner --- scripts/update_api.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/update_api.py b/scripts/update_api.py index a4a8faab2..ae0761056 100644 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -632,7 +632,7 @@ def mk_java(): 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') + java_native.write(' throw new Z3Exception(INTERNALgetErrorMsg(a0, err.toInt()));\n') if result != VOID: java_native.write(' return res;\n') java_native.write(' }\n\n')