From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Sun, 16 Feb 2020 22:06:21 +0000 (-0600)
Subject: Fix simple issue with cache (#3762)
X-Git-Tag: cvc5-1.0.0~3642
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6b6290e89632108f35dd24924ac62bb0d69e462a;p=cvc5.git

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 63a61b818..551a9d225 100644
--- 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);