diff options
| -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 = |