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();