diff options
Diffstat (limited to 'src/smt/sygus_solver.cpp')
| -rw-r--r-- | src/smt/sygus_solver.cpp | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp index 0976442e1..317bb2646 100644 --- a/src/smt/sygus_solver.cpp +++ b/src/smt/sygus_solver.cpp @@ -31,6 +31,7 @@ #include "theory/quantifiers/sygus/sygus_grammar_cons.h" #include "theory/quantifiers/sygus/sygus_utils.h" #include "theory/quantifiers_engine.h" +#include "theory/rewriter.h" #include "theory/smt_engine_subsolver.h" using namespace cvc5::theory; @@ -384,7 +385,12 @@ void SygusSolver::checkSynthSolution(Assertions& as) // definitions that were added as assertions to the sygus problem. for (Node a : auxAssertions) { - solChecker->assertFormula(a); + // We require rewriting here, e.g. so that define-fun from the original + // problem are rewritten to true. If this is not the case, then the + // assertions module of the subsolver will complain about assertions + // with free variables. + Node ar = theory::Rewriter::rewrite(a); + solChecker->assertFormula(ar); } Result r = solChecker->checkSat(); Notice() << "SygusSolver::checkSynthSolution(): result is " << r |