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")
diff --git a/src/tactic/sls/sls_tactic.cpp b/src/tactic/sls/sls_tactic.cpp
index 9bbed20bb..b06a047f7 100644
--- a/src/tactic/sls/sls_tactic.cpp
+++ b/src/tactic/sls/sls_tactic.cpp
@@ -158,8 +158,7 @@ tactic * mk_preamble(ast_manager & m, params_ref const & p) {
 }
 
 tactic * mk_qfbv_sls_tactic(ast_manager & m, params_ref const & p) {
-    tactic * t = and_then(mk_preamble(m, p), mk_sls_tactic(m));    
-    //tactic * t = and_then(mk_simplify_tactic(m), mk_nnf_tactic(m, p), mk_sls_tactic(m));    
+    tactic * t = and_then(mk_preamble(m, p), mk_sls_tactic(m, p));
     t->updt_params(p);
     return t;
 }
diff --git a/src/tactic/sls/sls_tactic.h b/src/tactic/sls/sls_tactic.h
index 50b8f0d5b..82ac1ce88 100644
--- a/src/tactic/sls/sls_tactic.h
+++ b/src/tactic/sls/sls_tactic.h
@@ -23,8 +23,8 @@ Notes:
 class ast_manager;
 class tactic;
 
-tactic * mk_sls_tactic(ast_manager & m, params_ref const & p = params_ref());
 tactic * mk_qfbv_sls_tactic(ast_manager & m, params_ref const & p = params_ref());
+
 /*
   ADD_TACTIC("qfbv-sls", "(try to) solve using stochastic local search for QF_BV.", "mk_qfbv_sls_tactic(m, p)")
 */
diff --git a/src/tactic/smtlogics/qfbv_tactic.cpp b/src/tactic/smtlogics/qfbv_tactic.cpp
index 3b4da2f2d..ac53ca0c8 100644
--- a/src/tactic/smtlogics/qfbv_tactic.cpp
+++ b/src/tactic/smtlogics/qfbv_tactic.cpp
@@ -93,32 +93,6 @@ tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p) {
                             mk_sat_tactic(m));
 #endif    
     
-    /* use full sls
-    tactic * st = using_params(and_then(preamble_st,
-                                        cond(mk_is_qfbv_probe(),
-                                             cond(mk_is_qfbv_eq_probe(),
-                                                  and_then(mk_bv1_blaster_tactic(m),
-                                                           using_params(mk_smt_tactic(), solver_p)),
-                                                  and_then(mk_nnf_tactic(m, p), mk_sls_tactic(m))),
-                                             mk_smt_tactic())),
-                               main_p);*/
-
-    /* use pure dpll
-    tactic * st = using_params(and_then(mk_simplify_tactic(m),
-                                        cond(mk_is_qfbv_probe(),
-                                                  and_then(mk_bit_blaster_tactic(m),
-                                                           when(mk_lt(mk_memory_probe(), mk_const_probe(MEMLIMIT)),
-                                                                and_then(using_params(and_then(mk_simplify_tactic(m),
-                                                                                               mk_solve_eqs_tactic(m)),
-                                                                                      local_ctx_p),
-                                                                         if_no_proofs(cond(mk_produce_unsat_cores_probe(),
-                                                                                           mk_aig_tactic(),
-                                                                                           using_params(mk_aig_tactic(),
-                                                                                                        big_aig_p))))),
-                                                           new_sat),
-                                             mk_smt_tactic())),
-                               main_p);*/
-
     tactic * st = using_params(and_then(preamble_st,
                                         // If the user sets HI_DIV0=false, then the formula may contain uninterpreted function
                                         // symbols. In this case, we should not use