mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

fix user-after-free in smt_ctx test

Browse source
This commit is contained in:
Nuno Lopes 2021-02-20 16:20:32 +00:00
parent f59ff7c3a0
commit 7b6eff6967
1 changed files with 3 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/test/smt_context.cpp
View file

@ -21,7 +21,9 @@ void tst_smt_context()
app_ref c1(m.mk_const(symbol("c"), m.mk_bool_sort()), m);
app_ref na1(m.mk_not(a1), m);
ctx.assert_expr(na1);
ctx.assert_expr(m.mk_or(c1.get(), b1.get()));
app_ref b_or_c(m.mk_or(c1.get(), b1.get()), m);
ctx.assert_expr(b_or_c);
{
app_ref nc(m.mk_not(c1), m);