diff options
Diffstat (limited to 'src/theory/quantifiers/sygus/sygus_unif.cpp')
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif.cpp | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_unif.cpp b/src/theory/quantifiers/sygus/sygus_unif.cpp index 15606c9a4..76ca94e05 100644 --- a/src/theory/quantifiers/sygus/sygus_unif.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif.cpp @@ -42,7 +42,8 @@ void SygusUnif::initializeCandidate( d_strategy[f].initialize(qe, f, enums); } -bool SygusUnif::constructSolution(std::vector<Node>& sols) +bool SygusUnif::constructSolution(std::vector<Node>& sols, + std::vector<Node>& lemmas) { // initialize a call to construct solution initializeConstructSol(); @@ -52,7 +53,7 @@ bool SygusUnif::constructSolution(std::vector<Node>& sols) initializeConstructSolFor(f); // call the virtual construct solution method Node e = d_strategy[f].getRootEnumerator(); - Node sol = constructSol(f, e, role_equal, 1); + Node sol = constructSol(f, e, role_equal, 1, lemmas); if (sol.isNull()) { return false; |