mirror of
https://github.com/Z3Prover/z3
synced 2025-04-15 13:28:47 +00:00
Merge branch 'master' of https://github.com/Z3Prover/z3
This commit is contained in:
commit
0da8160716
|
@ -2557,7 +2557,7 @@ void reference_counter_example() {
|
||||||
ty = Z3_mk_bool_sort(ctx);
|
ty = Z3_mk_bool_sort(ctx);
|
||||||
Z3_inc_ref(ctx, Z3_sort_to_ast(ctx, ty)); // Z3_sort_to_ast(ty) is just syntax sugar for ((Z3_ast) ty)
|
Z3_inc_ref(ctx, Z3_sort_to_ast(ctx, ty)); // Z3_sort_to_ast(ty) is just syntax sugar for ((Z3_ast) ty)
|
||||||
sx = Z3_mk_string_symbol(ctx, "x");
|
sx = Z3_mk_string_symbol(ctx, "x");
|
||||||
// Z3_symbol is not a Z3_ast. No reference counting is not needed.
|
// Z3_symbol is not a Z3_ast. No reference counting is needed.
|
||||||
x = Z3_mk_const(ctx, sx, ty);
|
x = Z3_mk_const(ctx, sx, ty);
|
||||||
Z3_inc_ref(ctx, x);
|
Z3_inc_ref(ctx, x);
|
||||||
sy = Z3_mk_string_symbol(ctx, "y");
|
sy = Z3_mk_string_symbol(ctx, "y");
|
||||||
|
|
Loading…
Reference in a new issue