Merge branch '1.4.x'

2 files changed, 13 insertions, 2 deletions

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 31b17ccda..5c2b81645 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) {
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index c59d87d40..dc80d65e3 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -3760,8 +3760,8 @@ CVC4::SExpr SmtEngine::getAssignment() throw(ModalException) {
   vector<SExpr> sexprs;
   TypeNode boolType = d_nodeManager->booleanType();
   TheoryModel* m = d_theoryEngine->getModel();
-  for(AssignmentSet::const_iterator i = d_assignments->begin(),
-        iend = d_assignments->end();
+  for(AssignmentSet::key_iterator i = d_assignments->key_begin(),
+        iend = d_assignments->key_end();
       i != iend;
       ++i) {
     Assert((*i).getType() == boolType);