Fix simple issue with cache (#3762)

diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
index 63a61b818ddf4a48037ffde46aa27d1e0ebad315..551a9d225a86275895a2a0485098a2ca51ab353a 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_enumerator.cpp
+++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
@@ -338,6 +338,9 @@ bool SygusEnumerator::TermCache::addTerm(Node n)
       Trace("sygus-enum-exc") << "Exclude: " << bn << std::endl;
       return false;
     }
+    // insert to builtin term cache, regardless of whether it is redundant
+    // based on examples.
+    d_bterms.insert(bnr);
     // if we are doing PBE symmetry breaking
     if (d_eec != nullptr)
     {
@@ -356,7 +359,6 @@ bool SygusEnumerator::TermCache::addTerm(Node n)
       }
     }
     Trace("sygus-enum-terms") << "tc(" << d_tn << "): term " << bn << std::endl;
-    d_bterms.insert(bnr);
   }
   ++(d_stats->d_enumTerms);
   d_terms.push_back(n);