remove unused field d_emp_exp in TheorySetsPrivate (#4521)
authormudathirmahgoub <mudathirmahgoub@gmail.com>
Sat, 23 May 2020 15:28:50 +0000 (10:28 -0500)
committerGitHub <noreply@github.com>
Sat, 23 May 2020 15:28:50 +0000 (10:28 -0500)
Remove unused field d_emp_exp in TheorySetsPrivate

src/theory/sets/theory_sets_private.cpp
src/theory/sets/theory_sets_private.h

index 78f6fa8b5603170fce05068c5aa1db3fcc1c8363..bbe46b2a6d65f0acad0c859e06210ef1bf0ec53c 100644 (file)
@@ -912,7 +912,7 @@ void TheorySetsPrivate::checkDisequalities()
     Node mem2 = nm->mkNode(MEMBER, x, deq[1]);
     Node lem = nm->mkNode(OR, deq, nm->mkNode(EQUAL, mem1, mem2).negate());
     lem = Rewriter::rewrite(lem);
-    d_im.assertInference(lem, d_emp_exp, "diseq", 1);
+    d_im.assertInference(lem, d_true, "diseq", 1);
     d_im.flushPendingLemmas();
     if (d_im.hasProcessed())
     {
index da42ad1fe50daba4312dcc5f2d4303fa52719688..fc965020499ddf47b1c5002e462a1af4121caf95 100644 (file)
@@ -124,7 +124,6 @@ class TheorySetsPrivate {
    */
   NodeSet d_termProcessed;
   NodeSet d_keep;
-  std::vector< Node > d_emp_exp;
   
   //propagation
   class EqcInfo