diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index e8f5e9dddb..f647cab383 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -683,7 +683,7 @@ namespace smt {
                     if (parent->is_cgc_enabled()) {
                         auto [p, parent_generation] = m_r1_parent_generations[cgc_enabled_idx++];
                         SASSERT(p == parent);
-                        m_constant_generations.insert(parent, parent_generation);
+                        parent->m_generation = parent_generation;
                     }
                     // It is not necessary to reinsert the equality to the congruence table
                     // (because the only congruence propagations that could lead to are already handled by the assign() here).
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index ad6d2cd7b2..cece66fad5 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -161,7 +161,6 @@ namespace smt {
         enode_vector                m_empty_vector;
         cg_table                    m_cg_table;
         enode_generation_table      m_sticky_generation_updates;
-        enode_generation_table      m_constant_generations;  // generations for enodes with !e->uses_cg_table()
         vector<std::pair<enode*, unsigned>>      m_r1_parent_generations; // generations of parents removed from m_cg_table while merging r1
 
         struct new_eq {
@@ -628,7 +627,7 @@ namespace smt {
                 return 0;
 
             if (!e->uses_cg_table())
-                return m_constant_generations.find(e);
+                return e->m_generation;
 
             // The class generation is cached on the congruence root's m_generation field.
             // Fast path: if e is already the congruence root, read it directly. Otherwise
diff --git a/src/smt/smt_enode.h b/src/smt/smt_enode.h
index 4dfec95cb2..1b1faeedbd 100644
--- a/src/smt/smt_enode.h
+++ b/src/smt/smt_enode.h
@@ -64,7 +64,7 @@ namespace smt {
         enode *             m_next;     //!< Next element in the equivalence class.
         enode *             m_cg;       
         unsigned            m_class_size;    //!< Size of the equivalence class if the enode is the root.
-        unsigned            m_generation;    //!< Cached generation of the congruence class. Only valid when is_cgr() (or for enodes that do not use the cg_table, where the generation is kept in context::m_constant_generations).
+        unsigned            m_generation;    //!< Cached generation of the congruence class. Valid when is_cgr(), or when the enode does not use the cg_table (constants/leaves/true-eq nodes), where it directly stores the enode's generation.
 
         unsigned            m_func_decl_id; //!< Id generated by the congruence table for fast indexing.
 
diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
index afe948e49e..05b458c544 100644
--- a/src/smt/smt_internalizer.cpp
+++ b/src/smt/smt_internalizer.cpp
@@ -111,7 +111,7 @@ namespace smt {
             if (e->uses_cg_table())
                 set_generation_sticky(e, m_generation);
             else
-                m_constant_generations[e] = m_generation; // Sticky by default. Won't unmerge
+                e->m_generation = m_generation; // Sticky by default. Won't unmerge
         }
     }
 
@@ -126,7 +126,7 @@ namespace smt {
             SASSERT(cgr);
             cgr->m_generation = generation;
         } else {
-            m_constant_generations[e] = generation;
+            e->m_generation = generation;
         }
     }
 
@@ -1098,7 +1098,7 @@ namespace smt {
                 }
                 else {
                     SASSERT(!e->uses_cg_table());
-                    m_constant_generations.insert(e, generation);
+                    e->m_generation = generation;
                     e->m_cg = e;
                 }
             }
@@ -1109,7 +1109,7 @@ namespace smt {
                 m_decl2enodes[decl_id].push_back(e);
             }
         } else {
-            m_constant_generations.insert(e, generation);
+            e->m_generation = generation;
         }
 
         SASSERT(e_internalized(n));
@@ -1152,8 +1152,6 @@ namespace smt {
         m_enodes.pop_back();
         m_e_internalized_stack.pop_back();
         m_sticky_generation_updates.erase(e);
-        if (!e->uses_cg_table()) 
-            m_constant_generations.erase(e);
     }
 
     /**