diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp
index f63b4fd8c..586c3a349 100644
--- a/src/tactic/portfolio/smt_strategic_solver.cpp
+++ b/src/tactic/portfolio/smt_strategic_solver.cpp
@@ -37,14 +37,11 @@ Notes:
 #include"horn_tactic.h"
 #include"smt_solver.h"
 
-#include"sls_tactic.h"
-
 tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const & logic) {
     if (logic=="QF_UF")
         return mk_qfuf_tactic(m, p);
     else if (logic=="QF_BV")
-   //     return mk_qfbv_tactic(m, p);
-        return mk_qfbv_sls_tactic(m, p);
+	    return mk_qfbv_tactic(m, p);
     else if (logic=="QF_IDL")
         return mk_qfidl_tactic(m, p);
     else if (logic=="QF_LIA")