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

fix crash when propagating equalities over arrays with lambdas

Browse source
This commit is contained in:
Nuno Lopes 2020-01-10 16:04:58 +00:00
parent 9064e58665
commit 0b14f1b6f6
1 changed files with 3 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/smt/theory_array_base.cpp
View file

@ -371,10 +371,8 @@ namespace smt {
literal n1_eq_n2 = mk_eq(e1, e2, true); literal n1_eq_n2 = mk_eq(e1, e2, true);
ctx.mark_as_relevant(n1_eq_n2); ctx.mark_as_relevant(n1_eq_n2);
expr_ref_vector args1(m), args2(m); expr_ref_vector args1(m), args2(m);
expr_ref f1 = instantiate_lambda(e1); args1.push_back(instantiate_lambda(e1));
expr_ref f2 = instantiate_lambda(e2); args2.push_back(instantiate_lambda(e2));
args1.push_back(f1);
args2.push_back(f2);
svector<symbol> names; svector<symbol> names;
sort_ref_vector sorts(m); sort_ref_vector sorts(m);
for (unsigned i = 0; i < dimension; i++) { for (unsigned i = 0; i < dimension; i++) {
@ -403,7 +401,7 @@ namespace smt {
quantifier * q = m.is_lambda_def(e->get_decl()); quantifier * q = m.is_lambda_def(e->get_decl());
expr_ref f(e, m); expr_ref f(e, m);
if (q) { if (q) {
var_subst sub(m, false); var_subst sub(m);
f = sub(q, e->get_num_args(), e->get_args()); f = sub(q, e->get_num_args(), e->get_args());
} }
return f; return f;