Merge pull request #31 from kbansal/sets

Sets

2 files changed, 5 insertions, 7 deletions

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 9b628ede2..f768bd62d 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -90,7 +90,9 @@ void TheorySetsPrivate::check(Theory::Effort level) {
     finishPropagation();
 
     Debug("sets") << "[sets]  in conflict = " << d_conflict << std::endl;
-    Assert( d_conflict ^ d_equalityEngine.consistent() );
+    // Assert( d_conflict ^ d_equalityEngine.consistent() );
+    // ^ doesn't hold when we propagate equality/disequality between shared terms
+    // and that leads to conflict (externally).
     if(d_conflict) { return; }
     Debug("sets") << "[sets]  is complete = " << isComplete() << std::endl;
   }
@@ -831,8 +833,8 @@ TheorySetsPrivate::TheorySetsPrivate(TheorySets& external,
   d_propagationQueue(c),
   d_settermPropagationQueue(c),
   d_nodeSaver(c),
-  d_pending(u),
-  d_pendingDisequal(u),
+  d_pending(c),
+  d_pendingDisequal(c),
   d_pendingEverInserted(u),
   d_scrutinize(NULL)
 {
diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp
index bcfbc46ae..7b02c1bfb 100644
--- a/src/theory/sets/theory_sets_rewriter.cpp
+++ b/src/theory/sets/theory_sets_rewriter.cpp
@@ -117,10 +117,6 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
               node[1].getKind() == kind::EMPTYSET) {
       Trace("sets-postrewrite") << "Sets::postRewrite returning " << node[0] << std::endl;
       return RewriteResponse(REWRITE_DONE, node[0]);
-    } else if (node[0] > node[1]) {
-      Node newNode = nm->mkNode(node.getKind(), node[1], node[0]);
-      Trace("sets-postrewrite") << "Sets::postRewrite returning " << newNode << std::endl;
-      return RewriteResponse(REWRITE_DONE, newNode);
     }
     break;
   }//kind::INTERSECION