diff --git a/src/tactic/sls/sls_engine.cpp b/src/tactic/sls/sls_engine.cpp
index 9fa2cc263..cc06e4f78 100644
--- a/src/tactic/sls/sls_engine.cpp
+++ b/src/tactic/sls/sls_engine.cpp
@@ -868,6 +868,7 @@ bailout:
     return res;
 }
 
+#if 0 // Old code.
 // main search loop
 lbool sls_engine::search_old() {
     lbool res = l_undef;
@@ -1060,6 +1061,7 @@ lbool sls_engine::search_old() {
             }
         }
     }
+#endif
 
 bailout:
     m_mpz_manager.del(new_value);
@@ -1190,4 +1192,4 @@ unsigned sls_engine::check_restart(unsigned curr_value)
         return 0;
     }
     return 1;
-}
\ No newline at end of file
+}
diff --git a/src/tactic/sls/sls_engine.h b/src/tactic/sls/sls_engine.h
index 8458817b6..5d4c9a0fc 100644
--- a/src/tactic/sls/sls_engine.h
+++ b/src/tactic/sls/sls_engine.h
@@ -114,7 +114,6 @@ public:
 
 protected:
     void checkpoint();
-    lbool search_old(void);
     double get_restart_armin(unsigned cnt_restarts);    
 
     bool what_if(func_decl * fd, const unsigned & fd_inx, const mpz & temp,
@@ -148,4 +147,4 @@ protected:
     inline unsigned check_restart(unsigned curr_value);
 };
 
-#endif
\ No newline at end of file
+#endif