diff --git a/src/tactic/portfolio/default_tactic.cpp b/src/tactic/portfolio/default_tactic.cpp
index 9ecc16ecf..5a5cbcf94 100644
--- a/src/tactic/portfolio/default_tactic.cpp
+++ b/src/tactic/portfolio/default_tactic.cpp
@@ -28,6 +28,7 @@ Notes:
 #include"probe_arith.h"
 #include"quant_tactics.h"
 #include"qffpa_tactic.h"
+#include"sls_tactic.h"
 
 tactic * mk_default_tactic(ast_manager & m, params_ref const & p) {
     tactic * st = using_params(and_then(mk_simplify_tactic(m),
diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp
index ae79446e3..f63b4fd8c 100644
--- a/src/tactic/portfolio/smt_strategic_solver.cpp
+++ b/src/tactic/portfolio/smt_strategic_solver.cpp
@@ -37,11 +37,14 @@ 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_tactic(m, p);
+        return mk_qfbv_sls_tactic(m, p);
     else if (logic=="QF_IDL")
         return mk_qfidl_tactic(m, p);
     else if (logic=="QF_LIA")
diff --git a/src/tactic/smtlogics/qfbv_tactic.cpp b/src/tactic/smtlogics/qfbv_tactic.cpp
index ac53ca0c8..3b4da2f2d 100644
--- a/src/tactic/smtlogics/qfbv_tactic.cpp
+++ b/src/tactic/smtlogics/qfbv_tactic.cpp
@@ -93,6 +93,32 @@ 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