diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-02-16 16:06:21 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-02-16 16:06:21 -0600 |
| commit | 6b6290e89632108f35dd24924ac62bb0d69e462a (patch) | |
| tree | 53f998af22d96a322a2ba828cd0765b54a50fb6f /src/theory | |
| parent | f5c8fa4f2edf773d1942110b7fee6411894c6961 (diff) | |
Fix simple issue with cache (#3762)
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_enumerator.cpp | 4 |
1 files changed, 3 insertions, 1 deletions
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); |