bug fix (unreported on bugzilla): skolem variables failing removal from pool

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 247348497320537158dde37b774f37f6967c8a3c..b67f42dfaa8af817eef939e6196578a3fdd5eda0 100644 (file)
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -161,7 +161,7 @@ void NodeManager::reclaimZombies() {
                   << " [" << nv->d_id << "]: " << *nv << "\n";
 
       // remove from the pool
-      if(nv->getKind() != kind::VARIABLE) {
+      if(nv->getMetaKind() != kind::metakind::VARIABLE) {
         poolRemove(nv);
       }