diff --git a/src/smt/smt_case_split_queue.cpp b/src/smt/smt_case_split_queue.cpp
index d43dd0fb8..029758b85 100644
--- a/src/smt/smt_case_split_queue.cpp
+++ b/src/smt/smt_case_split_queue.cpp
@@ -1046,7 +1046,7 @@ namespace {
             void operator()(expr * e) {
                 if (m_context.e_internalized(e)) {
                     enode * n = m_context.get_enode(e);
-                    n->set_generation(m_context, m_generation);
+                    n->set_generation(&m_context, m_generation);
                 }
             }
         };
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index 02da5d15f..6b84e8d6a 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -785,6 +785,13 @@ namespace smt {
             return get_bdata(get_bool_var(n));
         }
 
+        void update_generation(enode * n);
+
+        void update_generation(expr * e) {
+            if (is_app(e) && e_internalized(e))
+                update_generation(get_enode(to_app(e)));
+        }
+
         typedef std::pair<expr *, bool> expr_bool_pair;
 
         void ts_visit_child(expr * n, bool gate_ctx, svector<expr_bool_pair> & todo, bool & visited);
diff --git a/src/smt/smt_enode.cpp b/src/smt/smt_enode.cpp
index 99424c8ed..b1965c2f3 100644
--- a/src/smt/smt_enode.cpp
+++ b/src/smt/smt_enode.cpp
@@ -136,10 +136,11 @@ namespace smt {
        \brief Push old value of generation on the context trail stack
        and update the generation.       
     */
-    void enode::set_generation(context & ctx, unsigned generation) {
+    void enode::set_generation(context * ctx, unsigned generation) {
         if (m_generation == generation)
             return;
-        ctx.push_trail(value_trail<unsigned>(m_generation));
+        if (ctx)
+            ctx->push_trail(value_trail<unsigned>(m_generation));
         m_generation = generation;
     }
 
diff --git a/src/smt/smt_enode.h b/src/smt/smt_enode.h
index 3f488a3b7..ab3dcd141 100644
--- a/src/smt/smt_enode.h
+++ b/src/smt/smt_enode.h
@@ -386,7 +386,7 @@ namespace smt {
             return m_generation;
         }
 
-        void set_generation(context & ctx, unsigned generation);
+        void set_generation(context * ctx, unsigned generation);
         
         /**
            \brief Return the enode n that is in the eqc of *this, and has the minimal generation.
diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
index d742aadf1..7e32eaaf6 100644
--- a/src/smt/smt_internalizer.cpp
+++ b/src/smt/smt_internalizer.cpp
@@ -101,6 +101,11 @@ namespace smt {
         }
     }
 
+    void context::update_generation(enode * e) {
+        if (0 < m_generation && m_generation < e->get_generation())
+            e->set_generation(nullptr, m_generation);
+    }
+
     void context::ts_visit_child(expr * n, bool gate_ctx, svector<expr_bool_pair> & todo, bool & visited) {
         if (get_color(tcolors, fcolors, n, gate_ctx) == White) {
             todo.push_back(expr_bool_pair(n, gate_ctx));
@@ -115,12 +120,16 @@ namespace smt {
             return true;
         SASSERT(is_app(n));
         if (m.is_bool(n)) {
-            if (b_internalized(n))
+            if (b_internalized(n)) {
+                update_generation(n);                
                 return true;
+            }
         }
         else {
-            if (e_internalized(n))
+            update_generation(n);
+            if (e_internalized(n))                 
                 return true;
+            
         }
 
         bool visited  = true;
@@ -404,6 +413,8 @@ namespace smt {
             bool_var v = get_bool_var(n);
             TRACE(internalize_bug, tout << "#" << n->get_id() << " already has bool_var v" << v << "\n";);
             
+            update_generation(n);            
+            
             // n was already internalized as boolean, but an enode was
             // not associated with it.  So, an enode is necessary, if
             // n is not in the context of a gate and is an application.
@@ -810,6 +821,8 @@ namespace smt {
     */
     void context::internalize_term(app * n) {
         if (e_internalized(n)) {
+            enode * e = get_enode(n);
+            update_generation(e);
             theory * th = m_theories.get_plugin(n->get_family_id());
             if (th != nullptr) {
                 // This code is necessary because some theories may decide
@@ -822,7 +835,6 @@ namespace smt {
                 //   Later, the core tries to internalize (f (* 2 x)).
                 //   Now, (* 2 x) is not internal to arithmetic anymore,
                 //   and a theory variable must be created for it.
-                enode * e = get_enode(n);
                 if (!th->is_attached_to_var(e))
                     th->internalize_term(n);
             }