diff options
| author | Tim King <taking@google.com> | 2016-11-06 16:05:29 -0800 |
|---|---|---|
| committer | Tim King <taking@google.com> | 2016-11-06 16:06:53 -0800 |
| commit | 8be2d02f510e329d88e38889720334c277bf268c (patch) | |
| tree | 60ffaa576d6a63beafc8ac8c5ea3d66f59f67b0b /src/expr/node_manager.h | |
| parent | 4961abfa9bec88a2e15fc3078e2bd8a5bb258f93 (diff) | |
This switches the ZombieSet in the NodeManager to use NodeValue's id for equality comparison. The previously used function NodeValueEq incorrectly identified VARIABLE nodes as being equal. This meant that on hash collisions these nodes could leak memory.
Diffstat (limited to 'src/expr/node_manager.h')
| -rw-r--r-- | src/expr/node_manager.h | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 0b3830f4b..aaffeb322 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -96,7 +96,7 @@ class NodeManager { expr::NodeValuePoolEq> NodeValuePool; typedef __gnu_cxx::hash_set<expr::NodeValue*, expr::NodeValueIDHashFunction, - expr::NodeValueEq> ZombieSet; + expr::NodeValueIDEquality> ZombieSet; static CVC4_THREADLOCAL(NodeManager*) s_current; @@ -268,7 +268,7 @@ class NodeManager { Debug("gc") << (d_inReclaimZombies ? " [CURRENTLY-RECLAIMING]" : "") << std::endl; } - d_zombies.insert(nv);// FIXME multithreading + d_zombies.insert(nv); // FIXME multithreading if(safeToReclaimZombies()) { if(d_zombies.size() > 5000) { |