diff options
Diffstat (limited to 'src/theory/quantifiers/sygus/cegis.cpp')
-rw-r--r-- | src/theory/quantifiers/sygus/cegis.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index 7a9a9ca21..a4dc241b8 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -309,8 +309,9 @@ bool Cegis::constructCandidates(const std::vector<Node>& enums, { // if we didn't add a lemma, trying sampling to add a refinement lemma // that immediately refutes the candidate we just constructed - if (sampleAddRefinementLemma(enums, enum_values, lems)) + if (sampleAddRefinementLemma(candidates, candidate_values, lems)) { + candidate_values.clear(); // restart (should be guaranteed to add evaluation lemmas on this call) return constructCandidates( enums, enum_values, candidates, candidate_values, lems); |