diff --git a/src/smt/smt_enode.cpp b/src/smt/smt_enode.cpp
index e26ac1aa3..86b83af4c 100644
--- a/src/smt/smt_enode.cpp
+++ b/src/smt/smt_enode.cpp
@@ -340,7 +340,8 @@ namespace smt {
 
     void tmp_enode::set_capacity(unsigned new_capacity) {
         SASSERT(new_capacity > m_capacity);
-        dealloc_svect(m_enode_data);
+        if (m_enode_data)
+            dealloc_svect(m_enode_data);
         m_capacity   = new_capacity;
         unsigned sz  = sizeof(enode) + m_capacity * sizeof(enode*);
         m_enode_data = alloc_svect(char, sz);
@@ -358,6 +359,9 @@ namespace smt {
         if (num_args > m_capacity)
             set_capacity(num_args * 2);
         enode * r = get_enode();
+        if (m_app.get_app()->get_decl() != f) {
+            r->m_func_decl_id = UINT_MAX;
+        }
         m_app.set_decl(f);
         m_app.set_num_args(num_args);
         r->m_commutative  = num_args == 2 && f->is_commutative();
@@ -365,5 +369,9 @@ namespace smt {
         return r;
     }
 
+    void tmp_enode::reset() {
+        get_enode()->m_func_decl_id = UINT_MAX;
+    }
+
 };
 
diff --git a/src/smt/smt_enode.h b/src/smt/smt_enode.h
index c07576f38..92902ea0b 100644
--- a/src/smt/smt_enode.h
+++ b/src/smt/smt_enode.h
@@ -465,6 +465,7 @@ namespace smt {
         tmp_enode();
         ~tmp_enode();
         enode * set(func_decl * f, unsigned num_args, enode * const * args);
+        void reset();
     };
 
     inline mk_pp pp(enode* n, ast_manager& m) { return mk_pp(n->get_expr(), m); }