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 { diff --git a/src/interp/iz3hash.h b/src/interp/iz3hash.h index 355c03817..a12cfb990 100644 --- a/src/interp/iz3hash.h +++ b/src/interp/iz3hash.h @@ -464,7 +464,9 @@ namespace hash_space { Value &operator[](const Key& key) { std::pair kvp(key,Value()); - return lookup(kvp,true)->val.second; + return + hashtable,Key,HashFun,proj1,EqFun>:: + lookup(kvp,true)->val.second; } };