From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Tue, 3 Mar 2020 04:55:22 +0000 (-0800)
Subject: Fix `TheorySetsPrive::eqNotifyPostMerge()` (#3901)
X-Git-Tag: cvc5-1.0.0~3571
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1d44edf91762b837adf3db5ed40af9383e883b28;p=cvc5.git

Fix `TheorySetsPrive::eqNotifyPostMerge()` (#3901)

A local declaration of `s1` was shadowing `s1`, which meant that the
non-local definition of `s1` could never be not null. This meant that
parts of the code were never run. This commit fixes the issue by
removing the local declaration.
---

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index df6f76cbf..1a798414e 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -97,7 +97,6 @@ void TheorySetsPrivate::eqNotifyPostMerge(TNode t1, TNode t2)
     {
       s2 = e2->d_singleton;
       EqcInfo* e1 = getOrMakeEqcInfo(t1);
-      Node s1;
       Trace("sets-prop-debug") << "Merging singletons..." << std::endl;
       if (e1)
       {