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

nit

Browse source
This commit is contained in:
Nikolaj Bjorner 2026-05-24 15:48:10 -07:00
parent bb73d5fc8e
commit 24bb93c3e4
1 changed files with 2 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -273,10 +273,9 @@ namespace euf {
unsigned arity = f->get_arity(); unsigned arity = f->get_arity();
SASSERT(is_lambda(lam)); SASSERT(is_lambda(lam));
if (arity == 0) { if (arity == 0)
// Constant lambda-def: just return the lambda expression // Constant lambda-def: just return the lambda expression
return expr_ref(lam, m); return expr_ref(lam, m);
}
var_subst subst(m, false); var_subst subst(m, false);
expr_ref r = subst(lam, to_app(e)->get_num_args(), to_app(e)->get_args()); expr_ref r = subst(lam, to_app(e)->get_num_args(), to_app(e)->get_args());