From 43644fc2cbe8da8c74bdced967b8b9b9db50f677 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Fri, 4 Apr 2014 01:28:09 +0100 Subject: [PATCH 1/2] g++ pedantry --- src/interp/iz3hash.h | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) 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; } }; From 9c052f589d7a535ea46837f1feff095e57cfc878 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 4 Apr 2014 17:57:50 +0100 Subject: [PATCH 2/2] 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 {