From dda0c8ff4200faa6a441855716b47ec7f93e026e Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Sun, 20 Aug 2023 22:28:57 +0100 Subject: [PATCH] array theory: use expr_ref for mk_default() so it doesnt leak if internalize throws like on timeout/memout --- src/smt/theory_array_full.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/smt/theory_array_full.cpp b/src/smt/theory_array_full.cpp index 079c2f62e..345663b6b 100644 --- a/src/smt/theory_array_full.cpp +++ b/src/smt/theory_array_full.cpp @@ -546,7 +546,7 @@ namespace smt { expr_ref def2(m.mk_app(f, args2.size(), args2.data()), m); ctx.get_rewriter()(def2); - expr* def1 = mk_default(map); + expr_ref def1(mk_default(map), m); ctx.internalize(def1, false); ctx.internalize(def2, false); return try_assign_eq(def1, def2); @@ -561,7 +561,7 @@ namespace smt { SASSERT(is_const(cnst)); TRACE("array", tout << mk_bounded_pp(cnst->get_expr(), m) << "\n";); expr* val = cnst->get_arg(0)->get_expr(); - expr* def = mk_default(cnst->get_expr()); + expr_ref def(mk_default(cnst->get_expr()), m); ctx.internalize(def, false); return try_assign_eq(val, def); } @@ -598,7 +598,7 @@ namespace smt { return false; m_stats.m_num_default_lambda_axiom++; expr* e = arr->get_expr(); - expr* def = mk_default(e); + expr_ref def(mk_default(e), m); quantifier* lam = m.is_lambda_def(arr->get_decl()); TRACE("array", tout << mk_pp(lam, m) << "\n" << mk_pp(e, m) << "\n"); expr_ref_vector args(m);