diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp
index 16e59302b..a4a579ddd 100644
--- a/src/tactic/portfolio/smt_strategic_solver.cpp
+++ b/src/tactic/portfolio/smt_strategic_solver.cpp
@@ -99,17 +99,18 @@ tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const
 }
 
 static solver* mk_special_solver_for_logic(ast_manager & m, params_ref const & p, symbol const& logic) {
-    bv_rewriter rw(m);
-    if (logic == "QF_BV" && rw.hi_div0()) 
-        return mk_inc_sat_solver(m, p);
     if (logic == "QF_FD") 
         return mk_fd_solver(m, p);
     return 0;
 }
 
 static solver* mk_solver_for_logic(ast_manager & m, params_ref const & p, symbol const& logic) {
+    bv_rewriter rw(m);
     solver* s = mk_special_solver_for_logic(m, p, logic);
-    if (!s) s = mk_smt_solver(m, p, logic);
+    if (!s && logic == "QF_BV" && rw.hi_div0()) 
+        s = mk_inc_sat_solver(m, p);
+    if (!s) 
+        s = mk_smt_solver(m, p, logic);
     return s;
 }