mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-29 13:26:29 +00:00
Code Activity

code nits

Browse source
This commit is contained in:
Nikolaj Bjorner 2026-05-24 13:14:25 -07:00
parent 459629c662
commit 24248b3300
1 changed files with 3 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/ast/euf/ho_matcher.cpp
View file

@ -544,8 +544,7 @@ namespace euf {
uint_set vars; uint_set vars;
while (m_array.is_select(p)) { while (m_array.is_select(p)) {
auto a = to_app(p); auto a = to_app(p);
for (unsigned i = 1; i < a->get_num_args(); ++i) { for (auto arg : *a) {
auto arg = a->get_arg(i);
if (!is_bound_var(arg, offset)) if (!is_bound_var(arg, offset))
return false; return false;
auto idx = to_var(arg)->get_idx(); auto idx = to_var(arg)->get_idx();
@ -605,15 +604,12 @@ namespace euf {
} }
expr_ref_vector pat2bound(m); expr_ref_vector pat2bound(m);
for (auto a : pats) { for (auto a : pats) {
unsigned sz = a->get_num_args(); for (auto arg : *a) {
for (unsigned i = 1; i < sz; ++i) {
auto arg = a->get_arg(i);
SASSERT(is_bound_var(arg, offset)); SASSERT(is_bound_var(arg, offset));
auto idx = to_var(arg)->get_idx(); auto idx = to_var(arg)->get_idx();
pat2bound.reserve(idx + 1); pat2bound.reserve(idx + 1);
pat2bound[idx] = m.mk_var(--num_bound, arg->get_sort()); pat2bound[idx] = m.mk_var(--num_bound, arg->get_sort());
} }
p1 = a->get_arg(0);
} }
var_subst sub(m, false); var_subst sub(m, false);
expr_ref lam = sub(t, pat2bound); expr_ref lam = sub(t, pat2bound);