From f831e2116c210bee79aeae7d26527ac62e3dd92d Mon Sep 17 00:00:00 2001
From: mudathirmahgoub <mudathirmahgoub@gmail.com>
Date: Sat, 23 May 2020 10:28:50 -0500
Subject: [PATCH] remove unused field d_emp_exp in TheorySetsPrivate (#4521)

Remove unused field d_emp_exp in TheorySetsPrivate
---
 src/theory/sets/theory_sets_private.cpp | 2 +-
 src/theory/sets/theory_sets_private.h   | 1 -
 2 files changed, 1 insertion(+), 2 deletions(-)

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
-- 
2.30.2