diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 0e9f50828..9cd6f6add 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -685,8 +685,8 @@ namespace sat {
     // Search
     //
     // -----------------------
-    lbool solver::check() {
-        IF_VERBOSE(2, verbose_stream() << "(sat.sat-solver using the new SAT solver)\n";);
+    lbool solver::check(unsigned num_lits, literal const* lits) {
+        IF_VERBOSE(2, verbose_stream() << "(sat.sat-solver using the efficient SAT solver)\n";);
         SASSERT(scope_lvl() == 0);
 #ifdef CLONE_BEFORE_SOLVING
         if (m_mc.empty()) {
diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h
index b18bae06a..9cd62a47f 100644
--- a/src/sat/sat_solver.h
+++ b/src/sat/sat_solver.h
@@ -250,7 +250,7 @@ namespace sat {
         //
         // -----------------------
     public:
-        lbool check();
+        lbool check(unsigned num_lits = 0, literal const* lits = 0);
         model const & get_model() const { return m_model; }
         model_converter const & get_model_converter() const { return m_mc; }