From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Sat, 8 Nov 2014 20:13:24 +0000 (-0500)
Subject: Work around an apparent bug in libc++ that was causing crashes on Mac..
X-Git-Tag: cvc5-1.0.0~6509^2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5c99a9b0fb5f8c0f0aabc8ddcee1cbb93d493eca;p=cvc5.git

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 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) {