diff options
Diffstat (limited to 'src/theory/quantifiers/sygus/cegis.cpp')
| -rw-r--r-- | src/theory/quantifiers/sygus/cegis.cpp | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index 3ef3a3edc..57fe40517 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -136,8 +136,7 @@ bool Cegis::addEvalLemmas(const std::vector<Node>& candidates, bool addedEvalLemmas = false; // Refinement evaluation should not be done for grammars with symbolic // constructors. - bool doRefEval = options::sygusRefEval() && !d_usingSymCons; - if (doRefEval) + if (!d_usingSymCons) { Trace("cegqi-engine") << " *** Do refinement lemma evaluation" << (doGen ? " with conjecture-specific refinement" |