diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-05-24 19:55:47 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-05-24 19:55:47 -0500 |
| commit | 1589592be3c93ab2c3d42b9875535f950fe6b982 (patch) | |
| tree | 172095271a1fefec7081ed10813cb07ba0f25df1 | |
| parent | ce4493598547a9ef013b7bb8d554c83bae478b1b (diff) | |
Fix (#1979)
| -rw-r--r-- | src/theory/quantifiers/sygus/term_database_sygus.cpp | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index cd6c8bdec..8f20e2ffc 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -817,6 +817,7 @@ void TermDbSygus::registerEnumerator(Node e, d_enum_to_active_guard[e] = eg; } + d_enum_to_using_sym_cons[e] = useSymbolicCons; // depending on if we are using symbolic constructors, introduce symmetry // breaking lemma templates for each relevant subtype of the grammar std::map<TypeNode, std::map<TypeNode, unsigned> >::iterator it = |