From 5e6ea4e5704babcf6502d8deb925f29134df3767 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 20 Jan 2015 19:03:49 +0000 Subject: [PATCH 1/5] added --x86 build flag --- scripts/mk_util.py | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 4641a7b1b..96bc1c273 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -59,6 +59,7 @@ VERBOSE=True DEBUG_MODE=False SHOW_CPPS = True VS_X64 = False +LINUX_X64 = True ONLY_MAKEFILES = False Z3PY_SRC_DIR=None VS_PROJ = False @@ -334,7 +335,8 @@ def check_java(): raise MKException("Failed to detect jni.h. Possible solution: set JNI_HOME with the path to JDK.") def is64(): - return sys.maxsize >= 2**32 + global LINUX_X64 + return LINUX_X64 and sys.maxsize >= 2**32 def check_ar(): if is_verbose(): @@ -450,6 +452,8 @@ def display_help(exit_code): print(" -t, --trace enable tracing in release mode.") if IS_WINDOWS: print(" -x, --x64 create 64 binary when using Visual Studio.") + else: + print(" --x86 force 32-bit x86 build on x64 systems.") print(" -m, --makefiles generate only makefiles.") if IS_WINDOWS: print(" -v, --vsproj generate Visual Studio Project Files.") @@ -477,12 +481,13 @@ def display_help(exit_code): def parse_options(): global VERBOSE, DEBUG_MODE, IS_WINDOWS, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE, VS_PAR, VS_PAR_NUM global DOTNET_ENABLED, JAVA_ENABLED, STATIC_LIB, PREFIX, GMP, FOCI2, FOCI2LIB, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH + global LINUX_X64 try: options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:df:sxhmcvtnp:gj', ['build=', 'debug', 'silent', 'x64', 'help', 'makefiles', 'showcpp', 'vsproj', 'trace', 'nodotnet', 'staticlib', 'prefix=', 'gmp', 'foci2=', 'java', 'parallel=', 'gprof', - 'githash=']) + 'githash=', 'x86']) except: print("ERROR: Invalid command line option") display_help(1) @@ -501,6 +506,8 @@ def parse_options(): if not IS_WINDOWS: raise MKException('x64 compilation mode can only be specified when using Visual Studio') VS_X64 = True + elif opt in ('--x86'): + LINUX_X64=False elif opt in ('-h', '--help'): display_help(0) elif opt in ('-m', '--onlymakefiles'): @@ -1593,6 +1600,10 @@ def mk_config(): CPPFLAGS = '%s -D_AMD64_' % CPPFLAGS if sysname == 'Linux': CPPFLAGS = '%s -D_USE_THREAD_LOCAL' % CPPFLAGS + elif not LINUX_X64: + CXXFLAGS = '%s -m32' % CXXFLAGS + LDFLAGS = '%s -m32' % LDFLAGS + SLIBFLAGS = '%s -m32' % SLIBFLAGS if DEBUG_MODE: CPPFLAGS = '%s -DZ3DEBUG' % CPPFLAGS if TRACE or DEBUG_MODE: From 145e0259590cb39bee591a02dd46b6a656a663c3 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 23 Jan 2015 18:14:49 +0000 Subject: [PATCH 2/5] FPA API naming consistency Signed-off-by: Christoph M. Wintersteiger --- src/api/api_fpa.cpp | 4 ++-- src/api/dotnet/Context.cs | 6 +++--- src/api/java/Context.java | 6 +++--- src/api/z3_fpa.h | 14 +++++++------- 4 files changed, 15 insertions(+), 15 deletions(-) diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp index 2d4529309..86166a5cf 100644 --- a/src/api/api_fpa.cpp +++ b/src/api/api_fpa.cpp @@ -773,9 +773,9 @@ extern "C" { Z3_CATCH_RETURN(0); } - Z3_ast Z3_API Z3_mk_fpa_to_fp_real_int(Z3_context c, Z3_ast rm, Z3_ast sig, Z3_ast exp, Z3_sort s) { + Z3_ast Z3_API Z3_mk_fpa_to_fp_int_real(Z3_context c, Z3_ast rm, Z3_ast exp, Z3_ast sig, Z3_sort s) { Z3_TRY; - LOG_Z3_mk_fpa_to_fp_real_int(c, rm, sig, exp, s); + LOG_Z3_mk_fpa_to_fp_int_real(c, rm, exp, sig, s); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); fpa_util & fu = ctx->fpautil(); diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index 96999d2d9..65ec87bc6 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -4227,13 +4227,13 @@ namespace Microsoft.Z3 /// according to rounding mode rm. /// /// RoundingMode term. - /// Significand term of Real sort. /// Exponent term of Int sort. + /// Significand term of Real sort. /// FloatingPoint sort. - public BitVecExpr MkFPToFP(FPRMExpr rm, RealExpr sig, IntExpr exp, FPSort s) + public BitVecExpr MkFPToFP(FPRMExpr rm, IntExpr exp, RealExpr sig, FPSort s) { Contract.Ensures(Contract.Result() != null); - return new BitVecExpr(this, Native.Z3_mk_fpa_to_fp_real_int(this.nCtx, rm.NativeObject, sig.NativeObject, exp.NativeObject, s.NativeObject)); + return new BitVecExpr(this, Native.Z3_mk_fpa_to_fp_int_real(this.nCtx, rm.NativeObject, exp.NativeObject, sig.NativeObject, s.NativeObject)); } #endregion #endregion // Floating-point Arithmetic diff --git a/src/api/java/Context.java b/src/api/java/Context.java index baa84f60a..294826f55 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -3542,8 +3542,8 @@ public class Context extends IDisposable /** * Conversion of a real-sorted significand and an integer-sorted exponent into a term of FloatingPoint sort. * @param rm RoundingMode term. - * @param sig Significand term of Real sort. * @param exp Exponent term of Int sort. + * @param sig Significand term of Real sort. * @param s FloatingPoint sort. * Remarks: * Produces a term that represents the conversion of sig * 2^exp into a @@ -3552,9 +3552,9 @@ public class Context extends IDisposable * @throws Z3Exception **/ - public BitVecExpr mkFPToFP(FPRMExpr rm, RealExpr sig, IntExpr exp, FPSort s) throws Z3Exception + public BitVecExpr mkFPToFP(FPRMExpr rm, IntExpr exp, RealExpr sig, FPSort s) throws Z3Exception { - return new BitVecExpr(this, Native.mkFpaToFpRealInt(nCtx(), rm.getNativeObject(), sig.getNativeObject(), exp.getNativeObject(), s.getNativeObject())); + return new BitVecExpr(this, Native.mkFpaToFpIntReal(nCtx(), rm.getNativeObject(), exp.getNativeObject(), sig.getNativeObject(), s.getNativeObject())); } diff --git a/src/api/z3_fpa.h b/src/api/z3_fpa.h index 275c30fe0..ca5ffebf7 100644 --- a/src/api/z3_fpa.h +++ b/src/api/z3_fpa.h @@ -501,10 +501,10 @@ extern "C" { t1, t2 must have the same FloatingPoint sort. def_API('Z3_mk_fpa_min', AST, (_in(CONTEXT),_in(AST),_in(AST))) - */ - Z3_ast Z3_API Z3_mk_fpa_min(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2); + */ + Z3_ast Z3_API Z3_mk_fpa_min(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2); - /** + /** \brief Maximum of floating-point numbers. \param c logical context @@ -905,15 +905,15 @@ extern "C" { \param c logical context \param rm term of RoundingMode sort - \param sig significand term of Real sort \param exp exponent term of Int sort + \param sig significand term of Real sort \param s FloatingPoint sort - s must be a FloatingPoint sort, rm must be of RoundingMode sort, t must be of real sort. + s must be a FloatingPoint sort, rm must be of RoundingMode sort, exp must be of int sort, sig must be of real sort. - def_API('Z3_mk_fpa_to_fp_real_int', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(AST),_in(SORT))) + def_API('Z3_mk_fpa_to_fp_int_real', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(AST),_in(SORT))) */ - Z3_ast Z3_API Z3_mk_fpa_to_fp_real_int(__in Z3_context c, __in Z3_ast rm, __in Z3_ast sig, __in Z3_ast exp, __in Z3_sort s); + Z3_ast Z3_API Z3_mk_fpa_to_fp_int_real(__in Z3_context c, __in Z3_ast rm, __in Z3_ast exp, __in Z3_ast sig, __in Z3_sort s); /*@}*/ From 48c72d2c38bc0d1da9d2627e9b933bb65f4de5a6 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 23 Jan 2015 18:18:26 +0000 Subject: [PATCH 3/5] FPA API: naming consistency Signed-off-by: Christoph M. Wintersteiger --- examples/c/test_capi.c | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/examples/c/test_capi.c b/examples/c/test_capi.c index 817ada98e..c0ea70453 100644 --- a/examples/c/test_capi.c +++ b/examples/c/test_capi.c @@ -2665,10 +2665,10 @@ void fpa_example() { c2 = Z3_mk_fpa_to_fp_bv(ctx, Z3_mk_numeral(ctx, "4619567317775286272", Z3_mk_bv_sort(ctx, 64)), Z3_mk_fpa_sort(ctx, 11, 53)); - c3 = Z3_mk_fpa_to_fp_real_int(ctx, + c3 = Z3_mk_fpa_to_fp_int_real(ctx, Z3_mk_fpa_rtz(ctx), - Z3_mk_numeral(ctx, "1.75", Z3_mk_real_sort(ctx)), - Z3_mk_numeral(ctx, "2", Z3_mk_int_sort(ctx)), + Z3_mk_numeral(ctx, "2", Z3_mk_int_sort(ctx)), + Z3_mk_numeral(ctx, "1.75", Z3_mk_real_sort(ctx)), Z3_mk_fpa_sort(ctx, 11, 53)); c4 = Z3_mk_fpa_to_fp_real(ctx, Z3_mk_fpa_rtz(ctx), From 5f527fa5626dd800db956267e089c782fd18f031 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 24 Jan 2015 15:54:32 +0000 Subject: [PATCH 4/5] documentation fixes Signed-off-by: Christoph M. Wintersteiger --- src/api/z3_fpa.h | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/src/api/z3_fpa.h b/src/api/z3_fpa.h index ca5ffebf7..e1bd67d66 100644 --- a/src/api/z3_fpa.h +++ b/src/api/z3_fpa.h @@ -274,7 +274,7 @@ extern "C" { Z3_ast Z3_API Z3_mk_fpa_fp(__in Z3_context c, __in Z3_ast sgn, __in Z3_ast exp, __in Z3_ast sig); /** - \brief Create a numeral of FloatingPoint sort from a float. + \brief Create a numeral of FloatingPoint sort from a float. This function is used to create numerals that fit in a float value. It is slightly faster than #Z3_mk_numeral since it is not necessary to parse a string. @@ -292,20 +292,20 @@ extern "C" { Z3_ast Z3_API Z3_mk_fpa_numeral_float(__in Z3_context c, __in float v, __in Z3_sort ty); /** - \brief Create a numeral of FloatingPoint sort from a double. + \brief Create a numeral of FloatingPoint sort from a double. - This function is used to create numerals that fit in a double value. - It is slightly faster than #Z3_mk_numeral since it is not necessary to parse a string. + This function is used to create numerals that fit in a double value. + It is slightly faster than #Z3_mk_numeral since it is not necessary to parse a string. - \param c logical context - \param v value - \param ty sort + \param c logical context + \param v value + \param ty sort - ty must be a FloatingPoint sort + ty must be a FloatingPoint sort - \sa Z3_mk_numeral + \sa Z3_mk_numeral - def_API('Z3_mk_fpa_numeral_double', AST, (_in(CONTEXT), _in(DOUBLE), _in(SORT))) + def_API('Z3_mk_fpa_numeral_double', AST, (_in(CONTEXT), _in(DOUBLE), _in(SORT))) */ Z3_ast Z3_API Z3_mk_fpa_numeral_double(__in Z3_context c, __in double v, __in Z3_sort ty); From 9cb50c9f2833a708b1da3c828f0781f6c600554c Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 24 Jan 2015 17:33:26 +0000 Subject: [PATCH 5/5] FPA API bugfixes Signed-off-by: Christoph M. Wintersteiger --- src/api/api_fpa.cpp | 384 +++++++++++++++++++++++++------------------- 1 file changed, 216 insertions(+), 168 deletions(-) diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp index 86166a5cf..e7ae685fc 100644 --- a/src/api/api_fpa.cpp +++ b/src/api/api_fpa.cpp @@ -14,7 +14,7 @@ Author: Christoph M. Wintersteiger (cwinter) 2013-06-05 Notes: - + --*/ #include #include"z3.h" @@ -27,21 +27,22 @@ extern "C" { Z3_sort Z3_API Z3_mk_fpa_rounding_mode_sort(Z3_context c) { Z3_TRY; LOG_Z3_mk_fpa_rounding_mode_sort(c); - RESET_ERROR_CODE(); - api::context * ctx = mk_c(c); - Z3_sort r = of_sort(ctx->fpautil().mk_rm_sort()); - RETURN_Z3(r); + RESET_ERROR_CODE(); + api::context * ctx = mk_c(c); + sort * s = ctx->fpautil().mk_rm_sort(); + mk_c(c)->save_ast_trail(s); + RETURN_Z3(of_sort(s)); Z3_CATCH_RETURN(0); } - Z3_ast Z3_API Z3_mk_fpa_round_nearest_ties_to_even(Z3_context c) - { + Z3_ast Z3_API Z3_mk_fpa_round_nearest_ties_to_even(Z3_context c) { Z3_TRY; LOG_Z3_mk_fpa_round_nearest_ties_to_even(c); - RESET_ERROR_CODE(); + RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->fpautil().mk_round_nearest_ties_to_even()); - RETURN_Z3(r); + expr * a = ctx->fpautil().mk_round_nearest_ties_to_even(); + ctx->save_ast_trail(a); + RETURN_Z3(of_expr(a)); Z3_CATCH_RETURN(0); } @@ -50,19 +51,20 @@ extern "C" { LOG_Z3_mk_fpa_rne(c); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->fpautil().mk_round_nearest_ties_to_even()); - RETURN_Z3(r); + expr * a = ctx->fpautil().mk_round_nearest_ties_to_even(); + ctx->save_ast_trail(a); + RETURN_Z3(of_expr(a)); Z3_CATCH_RETURN(0); } - Z3_ast Z3_API Z3_mk_fpa_round_nearest_ties_to_away(Z3_context c) - { + Z3_ast Z3_API Z3_mk_fpa_round_nearest_ties_to_away(Z3_context c) { Z3_TRY; LOG_Z3_mk_fpa_round_nearest_ties_to_away(c); - RESET_ERROR_CODE(); + RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->fpautil().mk_round_nearest_ties_to_away()); - RETURN_Z3(r); + expr * a = ctx->fpautil().mk_round_nearest_ties_to_away(); + ctx->save_ast_trail(a); + RETURN_Z3(of_expr(a)); Z3_CATCH_RETURN(0); } @@ -71,19 +73,20 @@ extern "C" { LOG_Z3_mk_fpa_rna(c); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->fpautil().mk_round_nearest_ties_to_away()); - RETURN_Z3(r); + expr * a = ctx->fpautil().mk_round_nearest_ties_to_away(); + ctx->save_ast_trail(a); + RETURN_Z3(of_expr(a)); Z3_CATCH_RETURN(0); } - Z3_ast Z3_API Z3_mk_fpa_round_toward_positive(Z3_context c) - { + Z3_ast Z3_API Z3_mk_fpa_round_toward_positive(Z3_context c) { Z3_TRY; LOG_Z3_mk_fpa_round_toward_positive(c); - RESET_ERROR_CODE(); + RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->fpautil().mk_round_toward_positive()); - RETURN_Z3(r); + expr * a = ctx->fpautil().mk_round_toward_positive(); + ctx->save_ast_trail(a); + RETURN_Z3(of_expr(a)); Z3_CATCH_RETURN(0); } @@ -92,19 +95,20 @@ extern "C" { LOG_Z3_mk_fpa_rtp(c); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->fpautil().mk_round_toward_positive()); - RETURN_Z3(r); + expr * a = ctx->fpautil().mk_round_toward_positive(); + ctx->save_ast_trail(a); + RETURN_Z3(of_expr(a)); Z3_CATCH_RETURN(0); } - Z3_ast Z3_API Z3_mk_fpa_round_toward_negative(Z3_context c) - { + Z3_ast Z3_API Z3_mk_fpa_round_toward_negative(Z3_context c) { Z3_TRY; LOG_Z3_mk_fpa_round_toward_negative(c); - RESET_ERROR_CODE(); + RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->fpautil().mk_round_toward_negative()); - RETURN_Z3(r); + expr * a = ctx->fpautil().mk_round_toward_negative(); + ctx->save_ast_trail(a); + RETURN_Z3(of_expr(a)); Z3_CATCH_RETURN(0); } @@ -113,19 +117,20 @@ extern "C" { LOG_Z3_mk_fpa_rtn(c); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->fpautil().mk_round_toward_negative()); - RETURN_Z3(r); + expr * a = ctx->fpautil().mk_round_toward_negative(); + ctx->save_ast_trail(a); + RETURN_Z3(of_expr(a)); Z3_CATCH_RETURN(0); } - Z3_ast Z3_API Z3_mk_fpa_round_toward_zero(Z3_context c) - { + Z3_ast Z3_API Z3_mk_fpa_round_toward_zero(Z3_context c) { Z3_TRY; LOG_Z3_mk_fpa_round_toward_zero(c); - RESET_ERROR_CODE(); + RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->fpautil().mk_round_toward_zero()); - RETURN_Z3(r); + expr * a = ctx->fpautil().mk_round_toward_zero(); + ctx->save_ast_trail(a); + RETURN_Z3(of_expr(a)); Z3_CATCH_RETURN(0); } @@ -134,8 +139,9 @@ extern "C" { LOG_Z3_mk_fpa_rtz(c); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->fpautil().mk_round_toward_zero()); - RETURN_Z3(r); + expr * a = ctx->fpautil().mk_round_toward_zero(); + ctx->save_ast_trail(a); + RETURN_Z3(of_expr(a)); Z3_CATCH_RETURN(0); } @@ -143,13 +149,14 @@ extern "C" { Z3_sort Z3_API Z3_mk_fpa_sort(Z3_context c, unsigned ebits, unsigned sbits) { Z3_TRY; LOG_Z3_mk_fpa_sort(c, ebits, sbits); - RESET_ERROR_CODE(); + RESET_ERROR_CODE(); if (ebits < 2 || sbits < 3) { SET_ERROR_CODE(Z3_INVALID_ARG); - } - api::context * ctx = mk_c(c); - Z3_sort r = of_sort(ctx->fpautil().mk_float_sort(ebits, sbits)); - RETURN_Z3(r); + } + api::context * ctx = mk_c(c); + sort * s = ctx->fpautil().mk_float_sort(ebits, sbits); + ctx->save_ast_trail(s); + RETURN_Z3(of_sort(s)); Z3_CATCH_RETURN(0); } @@ -188,21 +195,23 @@ extern "C" { Z3_ast Z3_API Z3_mk_fpa_nan(Z3_context c, Z3_sort s) { Z3_TRY; LOG_Z3_mk_fpa_nan(c, s); - RESET_ERROR_CODE(); + RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->fpautil().mk_nan(to_sort(s))); - RETURN_Z3(r); + expr * a = ctx->fpautil().mk_nan(to_sort(s)); + ctx->save_ast_trail(a); + RETURN_Z3(of_expr(a)); Z3_CATCH_RETURN(0); } - + Z3_ast Z3_API Z3_mk_fpa_inf(Z3_context c, Z3_sort s, Z3_bool negative) { Z3_TRY; LOG_Z3_mk_fpa_inf(c, s, negative); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(negative != 0 ? ctx->fpautil().mk_ninf(to_sort(s)) : - ctx->fpautil().mk_pinf(to_sort(s))); - RETURN_Z3(r); + expr * a = negative != 0 ? ctx->fpautil().mk_ninf(to_sort(s)) : + ctx->fpautil().mk_pinf(to_sort(s)); + ctx->save_ast_trail(a); + RETURN_Z3(of_expr(a)); Z3_CATCH_RETURN(0); } @@ -211,9 +220,10 @@ extern "C" { LOG_Z3_mk_fpa_inf(c, s, negative); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(negative != 0 ? ctx->fpautil().mk_nzero(to_sort(s)) : - ctx->fpautil().mk_pzero(to_sort(s))); - RETURN_Z3(r); + expr * a = negative != 0 ? ctx->fpautil().mk_nzero(to_sort(s)) : + ctx->fpautil().mk_pzero(to_sort(s)); + ctx->save_ast_trail(a); + RETURN_Z3(of_expr(a)); Z3_CATCH_RETURN(0); } @@ -222,8 +232,9 @@ extern "C" { LOG_Z3_mk_fpa_fp(c, sgn, sig, exp); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->fpautil().mk_fp(to_expr(sgn), to_expr(sig), to_expr(exp))); - RETURN_Z3(r); + expr * a = ctx->fpautil().mk_fp(to_expr(sgn), to_expr(sig), to_expr(exp)); + ctx->save_ast_trail(a); + RETURN_Z3(of_expr(a)); Z3_CATCH_RETURN(0); } @@ -233,12 +244,13 @@ extern "C" { RESET_ERROR_CODE(); api::context * ctx = mk_c(c); scoped_mpf tmp(ctx->fpautil().fm()); - ctx->fpautil().fm().set(tmp, - ctx->fpautil().get_ebits(to_sort(ty)), - ctx->fpautil().get_sbits(to_sort(ty)), - v); - Z3_ast r = of_ast(ctx->fpautil().mk_value(tmp)); - RETURN_Z3(r); + ctx->fpautil().fm().set(tmp, + ctx->fpautil().get_ebits(to_sort(ty)), + ctx->fpautil().get_sbits(to_sort(ty)), + v); + expr * a = ctx->fpautil().mk_value(tmp); + ctx->save_ast_trail(a); + RETURN_Z3(of_expr(a)); Z3_CATCH_RETURN(0); } @@ -249,8 +261,9 @@ extern "C" { api::context * ctx = mk_c(c); scoped_mpf tmp(ctx->fpautil().fm()); ctx->fpautil().fm().set(tmp, ctx->fpautil().get_ebits(to_sort(ty)), ctx->fpautil().get_sbits(to_sort(ty)), v); - Z3_ast r = of_ast(ctx->fpautil().mk_value(tmp)); - RETURN_Z3(r); + expr * a = ctx->fpautil().mk_value(tmp); + ctx->save_ast_trail(a); + RETURN_Z3(of_expr(a)); Z3_CATCH_RETURN(0); } @@ -261,11 +274,12 @@ extern "C" { api::context * ctx = mk_c(c); scoped_mpf tmp(ctx->fpautil().fm()); ctx->fpautil().fm().set(tmp, - ctx->fpautil().get_ebits(to_sort(ty)), - ctx->fpautil().get_sbits(to_sort(ty)), - v); - Z3_ast r = of_ast(ctx->fpautil().mk_value(tmp)); - RETURN_Z3(r); + ctx->fpautil().get_ebits(to_sort(ty)), + ctx->fpautil().get_sbits(to_sort(ty)), + v); + expr * a = ctx->fpautil().mk_value(tmp); + ctx->save_ast_trail(a); + RETURN_Z3(of_expr(a)); Z3_CATCH_RETURN(0); } @@ -275,12 +289,13 @@ extern "C" { RESET_ERROR_CODE(); api::context * ctx = mk_c(c); scoped_mpf tmp(ctx->fpautil().fm()); - ctx->fpautil().fm().set(tmp, - ctx->fpautil().get_ebits(to_sort(ty)), - ctx->fpautil().get_sbits(to_sort(ty)), - sgn != 0, sig, exp); - Z3_ast r = of_ast(ctx->fpautil().mk_value(tmp)); - RETURN_Z3(r); + ctx->fpautil().fm().set(tmp, + ctx->fpautil().get_ebits(to_sort(ty)), + ctx->fpautil().get_sbits(to_sort(ty)), + sgn != 0, sig, exp); + expr * a = ctx->fpautil().mk_value(tmp); + ctx->save_ast_trail(a); + RETURN_Z3(of_expr(a)); Z3_CATCH_RETURN(0); } @@ -291,111 +306,122 @@ extern "C" { api::context * ctx = mk_c(c); scoped_mpf tmp(ctx->fpautil().fm()); ctx->fpautil().fm().set(tmp, - ctx->fpautil().get_ebits(to_sort(ty)), - ctx->fpautil().get_sbits(to_sort(ty)), - sgn != 0, sig, exp); - Z3_ast r = of_ast(ctx->fpautil().mk_value(tmp)); - RETURN_Z3(r); + ctx->fpautil().get_ebits(to_sort(ty)), + ctx->fpautil().get_sbits(to_sort(ty)), + sgn != 0, sig, exp); + expr * a = ctx->fpautil().mk_value(tmp); + ctx->save_ast_trail(a); + RETURN_Z3(of_expr(a)); Z3_CATCH_RETURN(0); } - + Z3_ast Z3_API Z3_mk_fpa_abs(Z3_context c, Z3_ast t) { Z3_TRY; LOG_Z3_mk_fpa_abs(c, t); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->fpautil().mk_abs(to_expr(t))); - RETURN_Z3(r); + expr * a = ctx->fpautil().mk_abs(to_expr(t)); + ctx->save_ast_trail(a); + RETURN_Z3(of_expr(a)); Z3_CATCH_RETURN(0); } - + Z3_ast Z3_API Z3_mk_fpa_neg(Z3_context c, Z3_ast t) { Z3_TRY; LOG_Z3_mk_fpa_neg(c, t); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->fpautil().mk_neg(to_expr(t))); - RETURN_Z3(r); + expr * a = ctx->fpautil().mk_neg(to_expr(t)); + ctx->save_ast_trail(a); + RETURN_Z3(of_expr(a)); Z3_CATCH_RETURN(0); } - + Z3_ast Z3_API Z3_mk_fpa_add(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2) { Z3_TRY; LOG_Z3_mk_fpa_add(c, rm, t1, t2); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->fpautil().mk_add(to_expr(rm), to_expr(t1), to_expr(t2))); - RETURN_Z3(r); + expr * a = ctx->fpautil().mk_add(to_expr(rm), to_expr(t1), to_expr(t2)); + ctx->save_ast_trail(a); + RETURN_Z3(of_expr(a)); Z3_CATCH_RETURN(0); } - + Z3_ast Z3_API Z3_mk_fpa_sub(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2) { Z3_TRY; LOG_Z3_mk_fpa_add(c, rm, t1, t2); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->fpautil().mk_sub(to_expr(rm), to_expr(t1), to_expr(t2))); - RETURN_Z3(r); + expr * a = ctx->fpautil().mk_sub(to_expr(rm), to_expr(t1), to_expr(t2)); + ctx->save_ast_trail(a); + RETURN_Z3(of_expr(a)); Z3_CATCH_RETURN(0); } - + Z3_ast Z3_API Z3_mk_fpa_mul(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2) { Z3_TRY; LOG_Z3_mk_fpa_add(c, rm, t1, t2); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->fpautil().mk_mul(to_expr(rm), to_expr(t1), to_expr(t2))); - RETURN_Z3(r); + expr * a = ctx->fpautil().mk_mul(to_expr(rm), to_expr(t1), to_expr(t2)); + ctx->save_ast_trail(a); + RETURN_Z3(of_expr(a)); Z3_CATCH_RETURN(0); } - + Z3_ast Z3_API Z3_mk_fpa_div(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2) { Z3_TRY; LOG_Z3_mk_fpa_add(c, rm, t1, t2); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->fpautil().mk_div(to_expr(rm), to_expr(t1), to_expr(t2))); - RETURN_Z3(r); + expr * a = ctx->fpautil().mk_div(to_expr(rm), to_expr(t1), to_expr(t2)); + ctx->save_ast_trail(a); + RETURN_Z3(of_expr(a)); Z3_CATCH_RETURN(0); } - + Z3_ast Z3_API Z3_mk_fpa_fma(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2, Z3_ast t3) { Z3_TRY; LOG_Z3_mk_fpa_fma(c, rm, t1, t2, t3); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->fpautil().mk_fma(to_expr(rm), to_expr(t1), to_expr(t2), to_expr(t3))); - RETURN_Z3(r); + expr * a = ctx->fpautil().mk_fma(to_expr(rm), to_expr(t1), to_expr(t2), to_expr(t3)); + ctx->save_ast_trail(a); + RETURN_Z3(of_expr(a)); Z3_CATCH_RETURN(0); } - + Z3_ast Z3_API Z3_mk_fpa_sqrt(Z3_context c, Z3_ast rm, Z3_ast t) { Z3_TRY; LOG_Z3_mk_fpa_sqrt(c, rm, t); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->fpautil().mk_sqrt(to_expr(rm), to_expr(t))); - RETURN_Z3(r); + expr * a = ctx->fpautil().mk_sqrt(to_expr(rm), to_expr(t)); + ctx->save_ast_trail(a); + RETURN_Z3(of_expr(a)); Z3_CATCH_RETURN(0); } - + Z3_ast Z3_API Z3_mk_fpa_rem(Z3_context c, Z3_ast t1, Z3_ast t2) { Z3_TRY; LOG_Z3_mk_fpa_rem(c, t1, t2); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->fpautil().mk_rem(to_expr(t1), to_expr(t2))); - RETURN_Z3(r); + expr * a = ctx->fpautil().mk_rem(to_expr(t1), to_expr(t2)); + ctx->save_ast_trail(a); + RETURN_Z3(of_expr(a)); Z3_CATCH_RETURN(0); } - + Z3_ast Z3_API Z3_mk_fpa_round_to_integral(Z3_context c, Z3_ast rm, Z3_ast t) { Z3_TRY; LOG_Z3_mk_fpa_round_to_integral(c, rm, t); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->fpautil().mk_round_to_integral(to_expr(rm), to_expr(t))); - RETURN_Z3(r); + expr * a = ctx->fpautil().mk_round_to_integral(to_expr(rm), to_expr(t)); + ctx->save_ast_trail(a); + RETURN_Z3(of_expr(a)); Z3_CATCH_RETURN(0); } @@ -404,8 +430,9 @@ extern "C" { LOG_Z3_mk_fpa_min(c, t1, t2); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->fpautil().mk_min(to_expr(t1), to_expr(t2))); - RETURN_Z3(r); + expr * a = ctx->fpautil().mk_min(to_expr(t1), to_expr(t2)); + ctx->save_ast_trail(a); + RETURN_Z3(of_expr(a)); Z3_CATCH_RETURN(0); } @@ -418,14 +445,15 @@ extern "C" { RETURN_Z3(r); Z3_CATCH_RETURN(0); } - + Z3_ast Z3_API Z3_mk_fpa_leq(Z3_context c, Z3_ast t1, Z3_ast t2) { Z3_TRY; LOG_Z3_mk_fpa_leq(c, t1, t2); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->fpautil().mk_le(to_expr(t1), to_expr(t2))); - RETURN_Z3(r); + expr * a = ctx->fpautil().mk_le(to_expr(t1), to_expr(t2)); + ctx->save_ast_trail(a); + RETURN_Z3(of_expr(a)); Z3_CATCH_RETURN(0); } @@ -434,18 +462,20 @@ extern "C" { LOG_Z3_mk_fpa_lt(c, t1, t2); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->fpautil().mk_lt(to_expr(t1), to_expr(t2))); - RETURN_Z3(r); + expr * a = ctx->fpautil().mk_lt(to_expr(t1), to_expr(t2)); + ctx->save_ast_trail(a); + RETURN_Z3(of_expr(a)); Z3_CATCH_RETURN(0); } - + Z3_ast Z3_API Z3_mk_fpa_geq(Z3_context c, Z3_ast t1, Z3_ast t2) { Z3_TRY; LOG_Z3_mk_fpa_geq(c, t1, t2); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->fpautil().mk_ge(to_expr(t1), to_expr(t2))); - RETURN_Z3(r); + expr * a = ctx->fpautil().mk_ge(to_expr(t1), to_expr(t2)); + ctx->save_ast_trail(a); + RETURN_Z3(of_expr(a)); Z3_CATCH_RETURN(0); } @@ -454,8 +484,9 @@ extern "C" { LOG_Z3_mk_fpa_gt(c, t1, t2); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->fpautil().mk_gt(to_expr(t1), to_expr(t2))); - RETURN_Z3(r); + expr * a = ctx->fpautil().mk_gt(to_expr(t1), to_expr(t2)); + ctx->save_ast_trail(a); + RETURN_Z3(of_expr(a)); Z3_CATCH_RETURN(0); } @@ -464,18 +495,20 @@ extern "C" { LOG_Z3_mk_fpa_eq(c, t1, t2); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->fpautil().mk_float_eq(to_expr(t1), to_expr(t2))); - RETURN_Z3(r); + expr * a = ctx->fpautil().mk_float_eq(to_expr(t1), to_expr(t2)); + ctx->save_ast_trail(a); + RETURN_Z3(of_expr(a)); Z3_CATCH_RETURN(0); } - + Z3_ast Z3_API Z3_mk_fpa_is_normal(Z3_context c, Z3_ast t) { Z3_TRY; LOG_Z3_mk_fpa_is_normal(c, t); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->fpautil().mk_is_normal(to_expr(t))); - RETURN_Z3(r); + expr * a = ctx->fpautil().mk_is_normal(to_expr(t)); + ctx->save_ast_trail(a); + RETURN_Z3(of_expr(a)); Z3_CATCH_RETURN(0); } @@ -484,8 +517,9 @@ extern "C" { LOG_Z3_mk_fpa_is_subnormal(c, t); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->fpautil().mk_is_subnormal(to_expr(t))); - RETURN_Z3(r); + expr * a = ctx->fpautil().mk_is_subnormal(to_expr(t)); + ctx->save_ast_trail(a); + RETURN_Z3(of_expr(a)); Z3_CATCH_RETURN(0); } @@ -494,8 +528,9 @@ extern "C" { LOG_Z3_mk_fpa_is_zero(c, t); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->fpautil().mk_is_zero(to_expr(t))); - RETURN_Z3(r); + expr * a = ctx->fpautil().mk_is_zero(to_expr(t)); + ctx->save_ast_trail(a); + RETURN_Z3(of_expr(a)); Z3_CATCH_RETURN(0); } @@ -504,8 +539,9 @@ extern "C" { LOG_Z3_mk_fpa_is_infinite(c, t); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->fpautil().mk_is_inf(to_expr(t))); - RETURN_Z3(r); + expr * a = ctx->fpautil().mk_is_inf(to_expr(t)); + ctx->save_ast_trail(a); + RETURN_Z3(of_expr(a)); Z3_CATCH_RETURN(0); } @@ -514,8 +550,9 @@ extern "C" { LOG_Z3_mk_fpa_is_nan(c, t); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->fpautil().mk_is_nan(to_expr(t))); - RETURN_Z3(r); + expr * a = ctx->fpautil().mk_is_nan(to_expr(t)); + ctx->save_ast_trail(a); + RETURN_Z3(of_expr(a)); Z3_CATCH_RETURN(0); } @@ -524,8 +561,9 @@ extern "C" { LOG_Z3_mk_fpa_is_negative(c, t); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->fpautil().mk_is_negative(to_expr(t))); - RETURN_Z3(r); + expr * a = ctx->fpautil().mk_is_negative(to_expr(t)); + ctx->save_ast_trail(a); + RETURN_Z3(of_expr(a)); Z3_CATCH_RETURN(0); } @@ -534,8 +572,9 @@ extern "C" { LOG_Z3_mk_fpa_is_positive(c, t); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->fpautil().mk_is_positive(to_expr(t))); - RETURN_Z3(r); + expr * a = ctx->fpautil().mk_is_positive(to_expr(t)); + ctx->save_ast_trail(a); + RETURN_Z3(of_expr(a)); Z3_CATCH_RETURN(0); } @@ -551,8 +590,9 @@ extern "C" { SET_ERROR_CODE(Z3_INVALID_ARG); return 0; } - Z3_ast r = of_ast(fu.mk_to_fp(to_sort(s), to_expr(bv))); - RETURN_Z3(r); + expr * a = fu.mk_to_fp(to_sort(s), to_expr(bv)); + ctx->save_ast_trail(a); + RETURN_Z3(of_expr(a)); Z3_CATCH_RETURN(0); } @@ -562,14 +602,15 @@ extern "C" { RESET_ERROR_CODE(); api::context * ctx = mk_c(c); fpa_util & fu = ctx->fpautil(); - if (!fu.is_rm(to_expr(rm)) || + if (!fu.is_rm(to_expr(rm)) || !fu.is_float(to_expr(t)) || !fu.is_float(to_sort(s))) { SET_ERROR_CODE(Z3_INVALID_ARG); return 0; } - Z3_ast r = of_ast(fu.mk_to_fp(to_sort(s), to_expr(rm), to_expr(t))); - RETURN_Z3(r); + expr * a = fu.mk_to_fp(to_sort(s), to_expr(rm), to_expr(t)); + ctx->save_ast_trail(a); + RETURN_Z3(of_expr(a)); Z3_CATCH_RETURN(0); } @@ -585,8 +626,9 @@ extern "C" { SET_ERROR_CODE(Z3_INVALID_ARG); return 0; } - Z3_ast r = of_ast(fu.mk_to_fp(to_sort(s), to_expr(rm), to_expr(t))); - RETURN_Z3(r); + expr * a = fu.mk_to_fp(to_sort(s), to_expr(rm), to_expr(t)); + ctx->save_ast_trail(a); + RETURN_Z3(of_expr(a)); Z3_CATCH_RETURN(0); } @@ -602,8 +644,9 @@ extern "C" { SET_ERROR_CODE(Z3_INVALID_ARG); return 0; } - Z3_ast r = of_ast(fu.mk_to_fp(to_sort(s), to_expr(rm), to_expr(t))); - RETURN_Z3(r); + expr * a = fu.mk_to_fp(to_sort(s), to_expr(rm), to_expr(t)); + ctx->save_ast_trail(a); + RETURN_Z3(of_expr(a)); Z3_CATCH_RETURN(0); } @@ -613,14 +656,15 @@ extern "C" { RESET_ERROR_CODE(); api::context * ctx = mk_c(c); fpa_util & fu = ctx->fpautil(); - if (!fu.is_rm(to_expr(rm)) || + if (!fu.is_rm(to_expr(rm)) || !ctx->bvutil().is_bv(to_expr(t)) || !fu.is_float(to_sort(s))) { SET_ERROR_CODE(Z3_INVALID_ARG); return 0; } - Z3_ast r = of_ast(fu.mk_to_fp_unsigned(to_sort(s), to_expr(rm), to_expr(t))); - RETURN_Z3(r); + expr * a = fu.mk_to_fp_unsigned(to_sort(s), to_expr(rm), to_expr(t)); + ctx->save_ast_trail(a); + RETURN_Z3(of_expr(a)); Z3_CATCH_RETURN(0); } @@ -629,8 +673,9 @@ extern "C" { LOG_Z3_mk_fpa_to_ubv(c, rm, t, sz); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->fpautil().mk_to_ubv(to_expr(rm), to_expr(t), sz)); - RETURN_Z3(r); + expr * a = ctx->fpautil().mk_to_ubv(to_expr(rm), to_expr(t), sz); + ctx->save_ast_trail(a); + RETURN_Z3(of_expr(a)); Z3_CATCH_RETURN(0); } @@ -639,8 +684,9 @@ extern "C" { LOG_Z3_mk_fpa_to_sbv(c, rm, t, sz); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->fpautil().mk_to_sbv(to_expr(rm), to_expr(t), sz)); - RETURN_Z3(r); + expr * a = ctx->fpautil().mk_to_sbv(to_expr(rm), to_expr(t), sz); + ctx->save_ast_trail(a); + RETURN_Z3(of_expr(a)); Z3_CATCH_RETURN(0); } @@ -649,8 +695,9 @@ extern "C" { LOG_Z3_mk_fpa_to_real(c, t); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->fpautil().mk_to_real(to_expr(t))); - RETURN_Z3(r); + expr * a = ctx->fpautil().mk_to_real(to_expr(t)); + ctx->save_ast_trail(a); + RETURN_Z3(of_expr(a)); Z3_CATCH_RETURN(0); } @@ -689,7 +736,7 @@ extern "C" { return r; Z3_CATCH_RETURN(0); } - + Z3_string Z3_API Z3_fpa_get_numeral_significand_string(__in Z3_context c, __in Z3_ast t) { Z3_TRY; LOG_Z3_fpa_get_numeral_significand_string(c, t); @@ -699,14 +746,14 @@ extern "C" { unsynch_mpz_manager & mpzm = mpfm.mpz_manager(); unsynch_mpq_manager & mpqm = mpfm.mpq_manager(); fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid()); - scoped_mpf val(mpfm); - if (!plugin->is_numeral(to_expr(t), val)) { + scoped_mpf val(mpfm); + if (!plugin->is_numeral(to_expr(t), val)) { SET_ERROR_CODE(Z3_INVALID_ARG); return ""; } else if (!mpfm.is_regular(val)) { SET_ERROR_CODE(Z3_INVALID_ARG) - return ""; + return ""; } unsigned sbits = val.get().get_sbits(); scoped_mpq q(mpqm); @@ -726,7 +773,7 @@ extern "C" { LOG_Z3_fpa_get_numeral_exponent_string(c, t); RESET_ERROR_CODE(); ast_manager & m = mk_c(c)->m(); - mpf_manager & mpfm = mk_c(c)->fpautil().fm(); + mpf_manager & mpfm = mk_c(c)->fpautil().fm(); fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid()); scoped_mpf val(mpfm); bool r = plugin->is_numeral(to_expr(t), val); @@ -738,7 +785,7 @@ extern "C" { SET_ERROR_CODE(Z3_INVALID_ARG) return ""; } - mpf_exp_t exp = mpfm.exp_normalized(val); + mpf_exp_t exp = mpfm.exp_normalized(val); std::stringstream ss; ss << exp; return mk_c(c)->mk_external_string(ss.str()); @@ -753,7 +800,7 @@ extern "C" { mpf_manager & mpfm = mk_c(c)->fpautil().fm(); fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid()); scoped_mpf val(mpfm); - bool r = plugin->is_numeral(to_expr(t), val); + bool r = plugin->is_numeral(to_expr(t), val); if (!r) { SET_ERROR_CODE(Z3_INVALID_ARG); return 0; @@ -775,7 +822,7 @@ extern "C" { Z3_ast Z3_API Z3_mk_fpa_to_fp_int_real(Z3_context c, Z3_ast rm, Z3_ast exp, Z3_ast sig, Z3_sort s) { Z3_TRY; - LOG_Z3_mk_fpa_to_fp_int_real(c, rm, exp, sig, s); + LOG_Z3_mk_fpa_to_fp_int_real(c, rm, sig, exp, s); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); fpa_util & fu = ctx->fpautil(); @@ -786,8 +833,9 @@ extern "C" { SET_ERROR_CODE(Z3_INVALID_ARG); return 0; } - Z3_ast r = of_ast(fu.mk_to_fp(to_sort(s), to_expr(rm), to_expr(sig), to_expr(exp))); - RETURN_Z3(r); + expr * a = fu.mk_to_fp(to_sort(s), to_expr(rm), to_expr(sig), to_expr(exp)); + ctx->save_ast_trail(a); + RETURN_Z3(of_expr(a)); Z3_CATCH_RETURN(0); }