From 9c052f589d7a535ea46837f1feff095e57cfc878 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 4 Apr 2014 17:57:50 +0100 Subject: [PATCH] C API bugfix (Stackoverflow #22864146) Signed-off-by: Christoph M. Wintersteiger --- src/api/api_bv.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/api/api_bv.cpp b/src/api/api_bv.cpp index 07d4fda18..0109d6e6b 100644 --- a/src/api/api_bv.cpp +++ b/src/api/api_bv.cpp @@ -117,6 +117,7 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \ Z3_sort int_s = Z3_mk_int_sort(c); if (is_signed) { Z3_ast r = Z3_mk_bv2int(c, n, false); + Z3_inc_ref(c, r); Z3_sort s = Z3_get_sort(c, n); unsigned sz = Z3_get_bv_sort_size(c, s); rational max_bound = power(rational(2), sz); @@ -135,6 +136,7 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \ Z3_dec_ref(c, pred); Z3_dec_ref(c, sub); Z3_dec_ref(c, zero); + Z3_dec_ref(c, r); RETURN_Z3(res); } else {