Work around an apparent bug in libc++ that was causing crashes on Mac..

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index fb1284d0dfd262acb2224d8e883c5320296cd11e..2b6feafa56e93fe06cf5176d35cc7ff54755cac3 100644 (file)
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -202,10 +202,21 @@ void NodeManager::reclaimZombies() {
                  NodeValueReferenceCountNonZero());
   d_zombies.clear();
 
+#ifdef _LIBCPP_VERSION
+  NodeValue* last = NULL;
+#endif
   for(vector<NodeValue*>::iterator i = zombies.begin();
       i != zombies.end();
       ++i) {
     NodeValue* nv = *i;
+#ifdef _LIBCPP_VERSION
+    // Work around an apparent bug in libc++'s hash_set<> which can
+    // (very occasionally) have an element repeated.
+    if(nv == last) {
+      continue;
+    }
+    last = nv;
+#endif
 
     // collect ONLY IF still zero
     if(nv->d_rc == 0) {