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;
         }
 
         /**