mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 21:03:39 +00:00
Code Activity

fix #6330

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-09-09 08:18:30 -07:00
parent 058ed3de56
commit 660bdc33e3
1 changed files with 8 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/smt/theory_array_full.cpp
View file

@ -604,6 +604,14 @@ namespace smt {
for (unsigned i = 0; i < lam->get_num_decls(); ++i) for (unsigned i = 0; i < lam->get_num_decls(); ++i)
args.push_back(mk_epsilon(lam->get_decl_sort(i)).first); args.push_back(mk_epsilon(lam->get_decl_sort(i)).first);
expr_ref val(mk_select(args), m); expr_ref val(mk_select(args), m);
ctx.get_rewriter()(val);
if (has_quantifiers(val)) {
expr_ref fn(m.mk_fresh_const("lambda-body", m.mk_bool_sort()), m);
expr_ref eq(m.mk_eq(fn, val), m);
ctx.assert_expr(eq);
ctx.internalize_assertions();
val = fn;
}
ctx.internalize(def, false); ctx.internalize(def, false);
ctx.internalize(val.get(), false); ctx.internalize(val.get(), false);
return try_assign_eq(val.get(), def); return try_assign_eq(val.get(), def);