From 6b6290e89632108f35dd24924ac62bb0d69e462a Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sun, 16 Feb 2020 16:06:21 -0600 Subject: [PATCH] Fix simple issue with cache (#3762) --- src/theory/quantifiers/sygus/sygus_enumerator.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) 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); -- 2.30.2