diff --git a/src/tactic/portfolio/default_tactic.cpp b/src/tactic/portfolio/default_tactic.cpp
index 53da9a159..5a5cbcf94 100644
--- a/src/tactic/portfolio/default_tactic.cpp
+++ b/src/tactic/portfolio/default_tactic.cpp
@@ -32,8 +32,7 @@ Notes:
 
 tactic * mk_default_tactic(ast_manager & m, params_ref const & p) {
     tactic * st = using_params(and_then(mk_simplify_tactic(m),
-                                        cond(mk_is_qfbv_probe(),  mk_qfbv_sls_tactic(m),
-  //                                      cond(mk_is_qfbv_probe(),  mk_qfbv_tactic(m),
+                                        cond(mk_is_qfbv_probe(),  mk_qfbv_tactic(m),
                                         cond(mk_is_qflia_probe(), mk_qflia_tactic(m),
                                         cond(mk_is_qflra_probe(), mk_qflra_tactic(m),
                                         cond(mk_is_qfnra_probe(), mk_qfnra_tactic(m),