Fixes for relational triggers (#2967)

[cvc5.git] / src / theory / quantifiers / term_database.cpp

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index abb84ccd707e4869a66f5febdca41e2555c7f2a9..c4b10eb6f286ece6b684b417e6126cd556ca5bd7 100644 (file)
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -907,7 +907,8 @@ bool TermDb::hasTermCurrent( Node n, bool useMode ) {
   }
 }
 
-bool TermDb::isTermEligibleForInstantiation( TNode n, TNode f, bool print ) {
+bool TermDb::isTermEligibleForInstantiation(TNode n, TNode f)
+{
   if( options::lteRestrictInstClosure() ){
     //has to be both in inst closure and in ground assertions
     if( !isInstClosure( n ) ){
@@ -937,7 +938,9 @@ bool TermDb::isTermEligibleForInstantiation( TNode n, TNode f, bool print ) {
       }
     }
   }
-  return true;
+  // it cannot have instantiation constants, which originate from
+  // counterexample-guided instantiation strategies.
+  return !TermUtil::hasInstConstAttr(n);
 }
 
 Node TermDb::getEligibleTermInEqc( TNode r ) {
@@ -949,11 +952,14 @@ Node TermDb::getEligibleTermInEqc( TNode r ) {
       Node h;
       eq::EqualityEngine* ee = d_quantEngine->getActiveEqualityEngine();
       eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
-      while( h.isNull() && !eqc_i.isFinished() ){
+      while (!eqc_i.isFinished())
+      {
         TNode n = (*eqc_i);
         ++eqc_i;
-        if( hasTermCurrent( n ) ){
+        if (isTermEligibleForInstantiation(n, TNode::null()))
+        {
           h = n;
+          break;
         }
       }
       d_term_elig_eqc[r] = h;