From b2401b87db152fceff70340eb0bd029d19e198c9 Mon Sep 17 00:00:00 2001 From: Can Cebeci Date: Wed, 3 Jun 2026 13:36:51 -0700 Subject: [PATCH] Remove redundant min_gen_match search (#9696) 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 --- src/ast/euf/euf_mam.cpp | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/src/ast/euf/euf_mam.cpp b/src/ast/euf/euf_mam.cpp index d47eb087b..8148fe7d9 100644 --- a/src/ast/euf/euf_mam.cpp +++ b/src/ast/euf/euf_mam.cpp @@ -1951,14 +1951,12 @@ namespace euf { enode * get_next_f_app(func_decl * lbl, unsigned num_expected_args, enode * first, enode * curr) { curr = curr->get_next(); - enode *matching_cgr = nullptr, *min_gen_match = nullptr; 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(); } - if (matching_cgr) - update_max_generation(min_gen_match, first); - return matching_cgr; + return nullptr; } /**