diff --git a/src/ast/euf/euf_mam.cpp b/src/ast/euf/euf_mam.cpp
index cce838c61..b9eb77e09 100644
--- a/src/ast/euf/euf_mam.cpp
+++ b/src/ast/euf/euf_mam.cpp
@@ -239,6 +239,7 @@ namespace euf {
         unsigned short m_num_args;
         unsigned       m_ireg;
         unsigned       m_oreg;
+        unsigned m_curr_generation;
     };
 
     struct get_cgr : public instruction {
@@ -1926,28 +1927,38 @@ namespace euf {
             m_max_generation = std::max(m_max_generation, n->generation());
         }
 
+        void get_f_app(func_decl* lbl, unsigned num_expected_args, enode* curr, enode*& matching_cgr, enode*& min_gen_match) {
+            if (curr->get_decl() == lbl && curr->num_args() == num_expected_args) {
+                if (curr->is_cgr() && !matching_cgr)
+                    matching_cgr = curr;
+                if (!min_gen_match || min_gen_match->generation() > curr->generation())
+                    min_gen_match = curr;
+            }
+        }
+
         // We have to provide the number of expected arguments because we have flat-assoc applications such as +.
         // Flat-assoc applications may have arbitrary number of arguments.
         enode * get_first_f_app(func_decl * lbl, unsigned num_expected_args, enode * first) {
+            enode *matching_cgr = nullptr, *min_gen_match = nullptr;
             for (enode* curr : euf::enode_class(first)) {
-                if (curr->get_decl() == lbl && curr->is_cgr() && curr->num_args() == num_expected_args) {
-                    update_max_generation(curr, first);
-                    return curr;
-                }
+                get_f_app(lbl, num_expected_args, curr, matching_cgr, min_gen_match);
+                curr = curr->get_next();
             }
-            return nullptr;
+            if (matching_cgr)
+                update_max_generation(min_gen_match, first);                          
+            return matching_cgr;
         }
 
         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) {
-                if (curr->get_decl() == lbl && curr->is_cgr() && curr->num_args() == num_expected_args) {
-                    update_max_generation(curr, first);
-                    return curr;
-                }
+                get_f_app(lbl, num_expected_args, curr, matching_cgr, min_gen_match);
                 curr = curr->get_next();
             }
-            return nullptr;
+            if (matching_cgr)
+                update_max_generation(min_gen_match, first);
+            return matching_cgr;
         }
 
         /**
@@ -2563,6 +2574,7 @@ namespace euf {
                  m_backtrack_stack[m_top].m_instr              = m_pc;                                                  \
                  m_backtrack_stack[m_top].m_old_max_generation = m_curr_max_generation;                                 \
                  m_backtrack_stack[m_top].m_curr               = m_app;                                                 \
+                 const_cast<bind*>(static_cast<bind const*>(m_pc))->m_curr_generation = m_max_generation;                \
                  m_top++;
 
             BIND_COMMON();
@@ -2829,7 +2841,8 @@ namespace euf {
                            goto backtrack;                                                                                      \
                        }                                                                                                        \
                        bp.m_curr = m_app;                                                                                       \
-                       TRACE(mam_int, tout << "bind next candidate:\n" << mk_ll_pp(m_app->get_expr(), m););      \
+                       m_max_generation = m_b->m_curr_generation;                                                               \
+                       TRACE(mam_int, tout << "bind next candidate:\n" << mk_ll_pp(m_app->get_expr(), m););                     \
                        m_oreg    = m_b->m_oreg
 
             BBIND_COMMON();
@@ -4059,4 +4072,4 @@ void euf::mam::ground_subterms(expr* e, ptr_vector<app>& ground) {
 
 euf::mam* euf::mam::mk(euf::mam_solver& ctx, euf::on_binding_callback& em) {
     return alloc(mam_impl, ctx, em, true);
-}
\ No newline at end of file
+}
diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp
index 006cb2697..d8c87eed6 100644
--- a/src/smt/mam.cpp
+++ b/src/smt/mam.cpp
@@ -215,6 +215,7 @@ namespace {
         unsigned short m_num_args;
         unsigned       m_ireg;
         unsigned       m_oreg;
+        unsigned       m_curr_max_generation = 0;
     };
 
     struct get_cgr : public instruction {
@@ -1887,33 +1888,43 @@ namespace {
                 m_used_enodes.push_back(std::make_tuple(prev, n));
         }
 
+        void get_f_app(func_decl* lbl, unsigned num_expected_args, enode* curr, enode*& matching_cgr, enode*& min_gen_match) {
+            if (curr->get_decl() == lbl && curr->get_num_args() == num_expected_args) {
+                if (curr->is_cgr() && !matching_cgr)
+                    matching_cgr = curr;
+
+                if (!min_gen_match || min_gen_match->get_generation() > curr->get_generation()) {
+                    min_gen_match = curr;
+                }
+            }
+        }
+
         // We have to provide the number of expected arguments because we have flat-assoc applications such as +.
         // Flat-assoc applications may have arbitrary number of arguments.
         enode * get_first_f_app(func_decl * lbl, unsigned num_expected_args, enode * curr) {
             enode * first = curr;
+            enode *matching_cgr = nullptr, *min_gen_match = nullptr;
             do {
-                if (curr->get_decl() == lbl && curr->is_cgr() && curr->get_num_args() == num_expected_args) {
-                    update_max_generation(curr, first);
-                    return curr;
-                }
+                get_f_app(lbl, num_expected_args, curr, matching_cgr, min_gen_match);
                 curr = curr->get_next();
             }
             while (curr != first);
-            return nullptr;
+            if (matching_cgr)
+                update_max_generation(min_gen_match, first);  
+            return matching_cgr;
         }
 
         enode * get_next_f_app(func_decl * lbl, unsigned num_expected_args, enode * first, enode * curr) {
             curr = curr->get_next();
             while (curr != first) {
-                if (curr->get_decl() == lbl && curr->is_cgr() && curr->get_num_args() == num_expected_args) {
-                    update_max_generation(curr, first);
+                if (curr->get_decl() == lbl && curr->get_num_args() == num_expected_args && curr->is_cgr())
                     return curr;
-                }
                 curr = curr->get_next();
             }
             return nullptr;
         }
 
+
         /**
            \brief Execute the is_cgr instruction.
            Return true if succeeded, and false if backtracking is needed.
@@ -2476,6 +2487,7 @@ namespace {
                  m_backtrack_stack[m_top].m_old_max_generation = m_curr_max_generation;                                 \
                  m_backtrack_stack[m_top].m_old_used_enodes_size = m_curr_used_enodes_size;                             \
                  m_backtrack_stack[m_top].m_curr               = m_app;                                                 \
+                 const_cast<bind*>(static_cast<const bind*>(m_pc))->m_curr_max_generation = m_max_generation;                                   \
                  m_top++;
 
             BIND_COMMON();
@@ -2743,7 +2755,8 @@ namespace {
 #define BBIND_COMMON() m_b   = static_cast<const bind*>(bp.m_instr);                                                            \
                        m_n1  = m_registers[m_b->m_ireg];                                                                        \
                        m_app = get_next_f_app(m_b->m_label, m_b->m_num_args, m_n1, bp.m_curr); \
-                       if (m_app == 0) {                                                                                        \
+                       m_max_generation = m_b->m_curr_max_generation;                                                            \
+                       if (!m_app) {                                                                                        \
                            m_top--;                                                                                             \
                            goto backtrack;                                                                                      \
                        }                                                                                                        \