From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 19 Apr 2022 20:36:54 +0000 (-0500)
Subject: Avoid trivial equalities in explanation of SETS_CARD_CYCLE (#8635)
X-Git-Tag: cvc5-1.0.1~244
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6a9a932b5e1f96b911bac1a95cb622ea04f57ec6;p=cvc5.git

Avoid trivial equalities in explanation of SETS_CARD_CYCLE (#8635)

This was the root cause of cvc5/cvc5-projects#178.
---

diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp
index eed014ea5..78658f7bd 100644
--- a/src/theory/sets/cardinality_extension.cpp
+++ b/src/theory/sets/cardinality_extension.cpp
@@ -639,7 +639,11 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc,
     }
     // now recurse on parents (to ensure their normal will be computed after
     // this eqc)
-    exp.push_back(eqc.eqNode(n));
+    bool needExp = (eqc != n);
+    if (needExp)
+    {
+      exp.push_back(eqc.eqNode(n));
+    }
     for (const std::pair<Node, Node>& cpnc : d_cardParent[n])
     {
       Trace("sets-cycle-debug") << "Traverse card parent " << eqc << " -> "
@@ -650,7 +654,10 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc,
         return;
       }
     }
-    exp.pop_back();
+    if (needExp)
+    {
+      exp.pop_back();
+    }
   }
   curr.pop_back();
   // parents now processed, can add to ordered list