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

#5518

Browse source 
regression from adding lambdas in model
This commit is contained in:
Nikolaj Bjorner 2021-08-31 12:13:27 -07:00
parent cd2701da0c
commit 535f442655
2 changed files with 3 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/normal_forms/defined_names.cpp
View file

@ -114,6 +114,8 @@ app * defined_names::impl::gen_name(expr * e, sort_ref_buffer & var_sorts, buffe
var_sorts.push_back(s);
}
else {
domain.push_back(m.mk_bool_sort());
new_args.push_back(m.mk_true());
var_sorts.push_back(m.mk_bool_sort()); // could be any sort.
}
var_names.push_back(symbol(i));

14
src/smt/theory_array_base.cpp
View file

@ -389,19 +389,7 @@ namespace smt {
if (q) {
// the variables in q are maybe not consecutive.
var_subst sub(m, false);
expr_free_vars fv;
fv(q);
expr_ref_vector es(m);
es.resize(fv.size());
for (unsigned i = 0, j = 0; i < e->get_num_args(); ++i) {
SASSERT(j < es.size());
while (!fv[j]) {
++j;
SASSERT(j < es.size());
}
es[j++] = e->get_arg(i);
}
f = sub(q, es.size(), es.data());
f = sub(q, e->get_num_args(), e->get_args());
}
return f;
}