mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-09 10:30:59 +00:00
Code Activity

Remove redundant min_gen_match search (#9696)

Browse source 
While working on https://github.com/Z3Prover/z3/pull/9405, I noticed
that euf_mam.cpp code was slightly out of sync with mam.cpp and did some
redundant work.

Co-authored-by: Can Cebeci <t-cancebeci@microsoft.com>
This commit is contained in:
Can Cebeci 2026-06-03 13:36:51 -07:00 • committed by GitHub
parent 14746d7fb6
commit b2401b87db
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 3 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/ast/euf/euf_mam.cpp
View file

@ -1951,14 +1951,12 @@ namespace euf {
enode * get_next_f_app(func_decl * lbl, unsigned num_expected_args, enode * first, enode * curr) { enode * get_next_f_app(func_decl * lbl, unsigned num_expected_args, enode * first, enode * curr) {
curr = curr->get_next(); curr = curr->get_next();
enode *matching_cgr = nullptr, *min_gen_match = nullptr;
while (curr != first) { while (curr != first) {
get_f_app(lbl, num_expected_args, curr, matching_cgr, min_gen_match); if (curr->get_decl() == lbl && curr->num_args() == num_expected_args && curr->is_cgr())
return curr;
curr = curr->get_next(); curr = curr->get_next();
} }
if (matching_cgr) return nullptr;
update_max_generation(min_gen_match, first);
return matching_cgr;
} }
/** /**