diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp
index f8ea774cbb..485228f059 100644
--- a/src/smt/mam.cpp
+++ b/src/smt/mam.cpp
@@ -2541,7 +2541,7 @@ namespace {
         case YIELD1:
             m_bindings[0] = m_registers[static_cast<const yield *>(m_pc)->m_bindings[0]];
 #define ON_MATCH(NUM)                                                   \
-            m_max_generation = std::max(m_max_generation, get_max_generation(m_context, NUM, m_bindings.begin())); \
+            m_max_generation = std::max(m_max_generation, m_context.get_max_generation(NUM, m_bindings.begin())); \
             if (m_context.get_cancel_flag()) {                          \
                 return false;                                           \
             }                                                           \
diff --git a/src/smt/smt_enode.h b/src/smt/smt_enode.h
index 84da1756ad..07bb99219d 100644
--- a/src/smt/smt_enode.h
+++ b/src/smt/smt_enode.h
@@ -456,8 +456,6 @@ namespace smt {
         bool aux;
         return congruent(n1, n2, aux);
     }
-
-    unsigned get_max_generation(context & ctx, unsigned num_enodes, enode * const * enodes);
     
     void unmark_enodes(unsigned num_enodes, enode * const * enodes);
 
diff --git a/src/smt/smt_quick_checker.cpp b/src/smt/smt_quick_checker.cpp
index d1fca891c6..85f58cb2d0 100644
--- a/src/smt/smt_quick_checker.cpp
+++ b/src/smt/smt_quick_checker.cpp
@@ -235,7 +235,7 @@ namespace smt {
                     TRACE(quick_checker, tout << "found new candidate\n";);
                     TRACE(quick_checker_sizes, tout << "found new candidate\n"; 
                           for (unsigned i = 0; i < m_num_bindings; ++i) tout << "#" << m_bindings[i]->get_owner_id() << " "; tout << "\n";);
-                    unsigned max_generation = get_max_generation(m_context, m_num_bindings, m_bindings.data());
+                    unsigned max_generation = m_context.get_max_generation(m_num_bindings, m_bindings.data());
                     if (m_context.add_instance(q, nullptr /* no pattern was used */, m_num_bindings, m_bindings.data(),
                                                max_generation,
                                                0,  // min_top_generation is only available for instances created by the MAM