summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/sygus/cegis.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/sygus/cegis.cpp')
-rw-r--r--src/theory/quantifiers/sygus/cegis.cpp3
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);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback