mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

array theory: use expr_ref for mk_default() so it doesnt leak if internalize throws

Browse source 
like on timeout/memout
This commit is contained in:
Nuno Lopes 2023-08-20 22:28:57 +01:00
parent 57c667e355
commit dda0c8ff42
1 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/smt/theory_array_full.cpp
View file

@ -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);