diff options
Diffstat (limited to 'src/expr/node_manager.cpp')
-rw-r--r-- | src/expr/node_manager.cpp | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 5c24699b8..4e872ad5c 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -164,7 +164,8 @@ void NodeManager::reclaimZombies() { << " [" << nv->d_id << "]: " << *nv << "\n"; // remove from the pool - if(nv->getMetaKind() != kind::metakind::VARIABLE) { + kind::MetaKind mk = nv->getMetaKind(); + if(mk != kind::metakind::VARIABLE) { poolRemove(nv); } @@ -179,6 +180,16 @@ void NodeManager::reclaimZombies() { // decr ref counts of children nv->decrRefCounts(); + if(mk == kind::metakind::CONSTANT) { + // Destroy (call the destructor for) the C++ type representing + // the constant in this NodeValue. This is needed for + // e.g. CVC4::Rational, since it has a gmp internal + // representation that mallocs memory and should be cleaned + // up. (This won't delete a pointer value if used as a + // constant, but then, you should probably use a smart-pointer + // type for a constant payload.) + kind::metakind::deleteNodeValueConstant(nv); + } free(nv); } } |