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 bedab16f1c8f0dbcf57ef33cd02535e065b84d18..523b84e6590d61ba3690c0035cde205430c923a2 100644 (file)
--- 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