diff --git a/src/test/smt_context.cpp b/src/test/smt_context.cpp index d2ee858e5..c7bf22813 100644 --- a/src/test/smt_context.cpp +++ b/src/test/smt_context.cpp @@ -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);