Fix issue related to higher-order purification in term database (#3157)

1 files changed, 15 insertions, 1 deletions

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 989609a76..84147bf6b 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -1039,7 +1039,21 @@ bool TermDb::reset( Theory::Effort effort ){
         }
         Trace("quant-ho") << "- assert purify equality : " << eq << std::endl;
         ee->assertEquality(eq, true, eq);
-        Assert(ee->consistent());
+        if (!ee->consistent())
+        {
+          // In some rare cases, purification functions (in the domain of
+          // d_ho_purify_to_term) may escape the term database. For example,
+          // matching algorithms may construct instantiations involving these
+          // functions. As a result, asserting these equalities internally may
+          // cause a conflict. In this case, we insist that the purification
+          // equality is sent out as a lemma here.
+          Trace("term-db-lemma")
+              << "Purify equality lemma: " << eq << std::endl;
+          d_quantEngine->addLemma(eq);
+          d_quantEngine->setConflict();
+          d_consistent_ee = false;
+          return false;
+        }
       }
     }
   }