From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 27 Jul 2021 14:24:20 +0000 (-0500)
Subject: Minor fix for term database + central equality engine (#6928)
X-Git-Tag: cvc5-1.0.0~1442
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2bb47a96e61babeedfd717104a9ec80b559017a9;p=cvc5.git

Minor fix for term database + central equality engine (#6928)

Previously we provided a bogus (self) explanation in a rare case of setting up the term database for higher order. This is incompatible with cases where central equality engine = master equality engine.
---

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index bedab16f1..523b84e65 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -480,9 +480,8 @@ void TermDb::addTermHo(Node n)
       Node psk;
       if (itp == d_ho_fun_op_purify.end())
       {
-        psk = sm->mkDummySkolem("pfun",
-                                curr.getType(),
-                                "purify for function operator term indexing");
+        psk = sm->mkPurifySkolem(
+            curr, "pfun", "purify for function operator term indexing");
         d_ho_fun_op_purify[curr] = psk;
         // we do not add it to d_ops since it is an internal operator
       }
@@ -1034,7 +1033,10 @@ bool TermDb::reset( Theory::Effort effort ){
           eq = itpe->second;
         }
         Trace("quant-ho") << "- assert purify equality : " << eq << std::endl;
-        ee->assertEquality(eq, true, eq);
+        // Note that ee may be the central equality engine, in which case this
+        // equality is explained trivially with "true", since both sides of
+        // eq are HOL and FOL encodings of the same thing.
+        ee->assertEquality(eq, true, d_true);
         if (!ee->consistent())
         {
           // In some rare cases, purification functions (in the domain of