diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index 31e7722102..64b2189963 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -635,6 +635,16 @@ namespace smt {
             return *generation;
         }
 
+        unsigned get_max_generation(unsigned num_enodes, enode * const * enodes) {
+            unsigned max = 0;
+            for (unsigned i = 0; i < num_enodes; ++i) {
+                unsigned curr = get_generation(enodes[i]);
+                if (curr > max)
+                    max = curr;
+            }
+            return max;
+        }
+
         void set_generation(enode * e, unsigned generation);
 
         /**
diff --git a/src/smt/smt_enode.cpp b/src/smt/smt_enode.cpp
index e5dd01d24e..87b9c64283 100644
--- a/src/smt/smt_enode.cpp
+++ b/src/smt/smt_enode.cpp
@@ -293,16 +293,6 @@ namespace smt {
         }
     }
 
-    unsigned get_max_generation(context & ctx, unsigned num_enodes, enode * const * enodes) {
-        unsigned max = 0;
-        for (unsigned i = 0; i < num_enodes; ++i) {
-            unsigned curr = ctx.get_generation(enodes[i]);
-            if (curr > max)
-                max = curr;
-        }
-        return max;
-    }
-
     void unmark_enodes(unsigned num_enodes, enode * const * enodes) {
         for (unsigned i = 0; i < num_enodes; ++i)
             enodes[i]->unset_mark();