diff --git a/src/smt/smt_enode.cpp b/src/smt/smt_enode.cpp
index 8be9384039..362bc81726 100644
--- a/src/smt/smt_enode.cpp
+++ b/src/smt/smt_enode.cpp
@@ -26,7 +26,7 @@ namespace smt {
        \brief Initialize an enode in the given memory position.
     */
     enode * enode::init(ast_manager & m, void * mem, app2enode_t const & app2enode, expr * owner, 
-                        bool suppress_args, bool merge_tf, unsigned iscope_lvl,
+                        unsigned generation, bool suppress_args, bool merge_tf, unsigned iscope_lvl,
                         bool cgc_enabled, bool update_children_parent) {
         SASSERT(m.is_bool(owner) || !merge_tf);
         enode * n             = new (mem) enode();
@@ -35,7 +35,7 @@ namespace smt {
         n->m_next             = n;
         n->m_cg               = nullptr;
         n->m_class_size       = 1;
-        n->m_generation       = 0;
+        n->m_generation       = generation;
         n->m_func_decl_id     = UINT_MAX;
         n->m_mark             = false;
         n->m_mark2            = false;
@@ -65,18 +65,18 @@ namespace smt {
     }
 
     enode * enode::mk(ast_manager & m, region & r, app2enode_t const & app2enode, expr * owner, 
-                        bool suppress_args, bool merge_tf, unsigned iscope_lvl,
-                           bool cgc_enabled, bool update_children_parent) {
+                        unsigned generation, bool suppress_args, bool merge_tf, unsigned iscope_lvl,
+                        bool cgc_enabled, bool update_children_parent) {
         SASSERT(m.is_bool(owner) || !merge_tf);
         unsigned sz           = get_enode_size(suppress_args || !::is_app(owner) ? 0 : to_app(owner)->get_num_args());
         void * mem            = r.allocate(sz);
-        return init(m, mem, app2enode, owner, suppress_args, merge_tf, iscope_lvl, cgc_enabled, update_children_parent);
+        return init(m, mem, app2enode, owner, generation, suppress_args, merge_tf, iscope_lvl, cgc_enabled, update_children_parent);
     }
 
     enode * enode::mk_dummy(ast_manager & m, app2enode_t const & app2enode, app * owner) {
         unsigned sz           = get_enode_size(owner->get_num_args());
         void * mem            = alloc_svect(char, sz);
-        return init(m, mem, app2enode, owner, false, false, 0, true, false);
+        return init(m, mem, app2enode, owner, 0, false, false, 0, true, false);
     }
 
     void enode::del_eh(ast_manager & m, bool update_children_parent) {
diff --git a/src/smt/smt_enode.h b/src/smt/smt_enode.h
index 1b1faeedbd..b860c35aaf 100644
--- a/src/smt/smt_enode.h
+++ b/src/smt/smt_enode.h
@@ -133,7 +133,7 @@ namespace smt {
         friend class tmp_enode;
 
         static enode * init(ast_manager & m, void * mem, app2enode_t const & app2enode, expr * owner, 
-                            bool suppress_args, bool merge_tf, unsigned iscope_lvl,
+                            unsigned generation, bool suppress_args, bool merge_tf, unsigned iscope_lvl,
                             bool cgc_enabled, bool update_children_parent);
     public:
 
@@ -142,7 +142,7 @@ namespace smt {
         }
         
         static enode * mk(ast_manager & m, region & r, app2enode_t const & app2enode, expr * owner, 
-                            bool suppress_args, bool merge_tf, unsigned iscope_lvl,
+                            unsigned generation, bool suppress_args, bool merge_tf, unsigned iscope_lvl,
                             bool cgc_enabled, bool update_children_parent);
 
         static enode * mk_dummy(ast_manager & m, app2enode_t const & app2enode, app * owner);
diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
index a0a7db122d..5a2eadbafc 100644
--- a/src/smt/smt_internalizer.cpp
+++ b/src/smt/smt_internalizer.cpp
@@ -1054,7 +1054,7 @@ namespace smt {
             CTRACE(cached_generation, generation != m_generation,
                    tout << "cached_generation: #" << n->get_id() << " " << generation << " " << m_generation << "\n";);
         }
-        enode *e = enode::mk(m, get_region(), m_app2enode, n, suppress_args, merge_tf, m_scope_lvl,
+        enode *e = enode::mk(m, get_region(), m_app2enode, n, generation, suppress_args, merge_tf, m_scope_lvl,
                              cgc_enabled, true);
         TRACE(mk_enode_detail, tout << "e.get_num_args() = " << e->get_num_args() << "\n";);
         if (m.is_unique_value(n))
@@ -1084,13 +1084,9 @@ namespace smt {
                     }
                     else {
                         e->m_cg = e;
-                        // e is the congruence root: cache its class generation on the enode.
-                        e->m_generation = generation;
                     }
                 }
                 else {
-                    SASSERT(!e->uses_cg_table());
-                    e->m_generation = generation;
                     e->m_cg = e;
                 }
             }
@@ -1100,8 +1096,6 @@ namespace smt {
                     m_decl2enodes.resize(decl_id+1);
                 m_decl2enodes[decl_id].push_back(e);
             }
-        } else {
-            e->m_generation = generation;
         }
 
         SASSERT(e_internalized(n));