mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
C API bugfix (Stackoverflow #22864146)
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
parent
4444eb361c
commit
9c052f589d
|
@ -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 {
|
||||
|
|
Loading…
Reference in a new issue