diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp
index b128b9b1f..f9334bcb2 100644
--- a/src/tactic/portfolio/smt_strategic_solver.cpp
+++ b/src/tactic/portfolio/smt_strategic_solver.cpp
@@ -38,6 +38,8 @@ Notes:
 #include"horn_tactic.h"
 #include"smt_solver.h"
 #include"inc_sat_solver.h"
+#include"bv_rewriter.h"
+
 
 tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const & logic) {
     if (logic=="QF_UF")
@@ -93,7 +95,8 @@ tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const
 }
 
 static solver* mk_solver_for_logic(ast_manager & m, params_ref const & p, symbol const& logic) {
-    if (logic == "QF_BV") 
+    bv_rewriter rw(m);
+    if (logic == "QF_BV" && rw.hi_div0()) 
         return mk_inc_sat_solver(m, p);
     return mk_smt_solver(m, p, logic);
 }