diff options
Diffstat (limited to 'src/smt/sygus_solver.cpp')
-rw-r--r-- | src/smt/sygus_solver.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp index 2a1d4e6c6..5db9804c6 100644 --- a/src/smt/sygus_solver.cpp +++ b/src/smt/sygus_solver.cpp @@ -377,7 +377,7 @@ void SygusSolver::checkSynthSolution(Assertions& as) // 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); + Node ar = rewrite(a); solChecker->assertFormula(ar); } Result r = solChecker->checkSat(); |