From 372bb4b25afeb3d727060a7063470e4a11b78983 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 6 Nov 2020 12:16:09 +0000 Subject: [PATCH] Fix reference counting in Z3_mk_fpa_to_ieee_bv --- src/api/api_fpa.cpp | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp index aa47079a9..100e0a082 100644 --- a/src/api/api_fpa.cpp +++ b/src/api/api_fpa.cpp @@ -1091,7 +1091,7 @@ extern "C" { if (biased) { exp = mpfm.is_zero(val) ? 0 : mpfm.is_inf(val) ? mpfm.mk_top_exp(ebits) : - mpfm.bias_exp(ebits, mpfm.exp(val)); + mpfm.bias_exp(ebits, mpfm.exp(val)); } else { exp = mpfm.is_zero(val) ? 0 : @@ -1200,8 +1200,9 @@ extern "C" { RETURN_Z3(nullptr); } api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->fpautil().mk_to_ieee_bv(to_expr(t))); - RETURN_Z3(r); + expr * r = ctx->fpautil().mk_to_ieee_bv(to_expr(t)); + ctx->save_ast_trail(r); + RETURN_Z3(of_expr(r)); Z3_CATCH_RETURN(nullptr); }