From: mudathirmahgoub <mudathirmahgoub@gmail.com>
Date: Sat, 23 May 2020 15:28:50 +0000 (-0500)
Subject: remove unused field d_emp_exp in TheorySetsPrivate (#4521)
X-Git-Tag: cvc5-1.0.0~3292
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f831e2116c210bee79aeae7d26527ac62e3dd92d;p=cvc5.git

remove unused field d_emp_exp in TheorySetsPrivate (#4521)

Remove unused field d_emp_exp in TheorySetsPrivate
---

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 78f6fa8b5..bbe46b2a6 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -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())
     {
diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index da42ad1fe..fc9650204 100644
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -124,7 +124,6 @@ class TheorySetsPrivate {
    */
   NodeSet d_termProcessed;
   NodeSet d_keep;
-  std::vector< Node > d_emp_exp;
   
   //propagation
   class EqcInfo