diff options
Diffstat (limited to 'src/theory/quantifiers/sygus/cegis.cpp')
| -rw-r--r-- | src/theory/quantifiers/sygus/cegis.cpp | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index 78ea5b22f..2d27878fd 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -79,7 +79,6 @@ bool Cegis::processInitialize(Node conj, Trace("cegis") << "...register enumerator " << candidates[i]; // We use symbolic constants if we are doing repair constants or if the // grammar construction was not simple. - bool useSymCons = false; if (options::sygusRepairConst() || options::sygusGrammarConsMode() != options::SygusGrammarConsMode::SIMPLE) @@ -89,15 +88,13 @@ bool Cegis::processInitialize(Node conj, SygusTypeInfo& cti = d_tds->getTypeInfo(ctn); if (cti.hasSubtermSymbolicCons()) { - useSymCons = true; // remember that we are using symbolic constructors d_usingSymCons = true; Trace("cegis") << " (using symbolic constructors)"; } } Trace("cegis") << std::endl; - d_tds->registerEnumerator( - candidates[i], candidates[i], d_parent, erole, useSymCons); + d_tds->registerEnumerator(candidates[i], candidates[i], d_parent, erole); } return true; } |