From 5c99a9b0fb5f8c0f0aabc8ddcee1cbb93d493eca Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Sat, 8 Nov 2014 15:13:24 -0500
Subject: [PATCH] Work around an apparent bug in libc++ that was causing
 crashes on Mac..

---
 src/expr/node_manager.cpp | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index fb1284d0d..2b6feafa5 100644
--- 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) {
-- 
2.30.2