diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-10 00:35:31 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-03-09 22:35:31 -0700 |
| commit | 426469ee6b6e5f9e0f4f720d62ec3798b7badff7 (patch) | |
| tree | 4f3cbf6d20fb0aaea251b7700bf764eacffd87ff | |
| parent | ccca2e76be3412fc24e1bb0a4eccae1133e519f4 (diff) | |
Only register sygus terms to unfold if option is set (#3978)
Fixes #3953.
| -rw-r--r-- | src/theory/quantifiers_engine.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index f6c17ebf9..ed4a79808 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -990,7 +990,7 @@ void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant, bool within if (!withinQuant) { - if (d_sygus_tdb) + if (d_sygus_tdb && options::sygusEvalUnfold()) { d_sygus_tdb->getEvalUnfold()->registerEvalTerm(n); } |