projects
/
cvc5.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
36ff166
)
Work around an apparent bug in libc++ that was causing crashes on Mac..
author
Morgan Deters
<mdeters@cs.nyu.edu>
Sat, 8 Nov 2014 20:13:24 +0000
(15:13 -0500)
committer
Morgan Deters
<mdeters@cs.nyu.edu>
Sun, 9 Nov 2014 23:53:29 +0000
(18:53 -0500)
src/expr/node_manager.cpp
patch
|
blob
|
history
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();
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;
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) {
// collect ONLY IF still zero
if(nv->d_rc == 0) {