diff --git a/src/sat/smt/arith_axioms.cpp b/src/sat/smt/arith_axioms.cpp
index 71e992c0e..f014da9fa 100644
--- a/src/sat/smt/arith_axioms.cpp
+++ b/src/sat/smt/arith_axioms.cpp
@@ -405,9 +405,13 @@ namespace arith {
             expr* n = m_idiv_terms[i];
             expr* p = nullptr, * q = nullptr;
             VERIFY(a.is_idiv(n, p, q));
-            theory_var v = mk_evar(n);
+            euf::enode* np = ctx.get_enode(p);
+            euf::enode* nn = ctx.get_enode(n);
+            if (!np || !np->is_attached_to(get_id()))
+                continue;
+            if (!nn || !nn->is_attached_to(get_id()))
+                continue;
             theory_var v1 = mk_evar(p);
-
             if (!is_registered_var(v1))
                 continue;
             lp::impq r1 = get_ivalue(v1);
@@ -428,6 +432,7 @@ namespace arith {
                     TRACE("arith", tout << "unbounded " << expr_ref(n, m) << "\n";);
                     continue;
                 }
+                theory_var v = mk_evar(n);
                 if (!is_registered_var(v))
                     continue;
                 lp::impq val_v = get_ivalue(v);
diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp
index f85dbca15..52df38247 100644
--- a/src/tactic/portfolio/smt_strategic_solver.cpp
+++ b/src/tactic/portfolio/smt_strategic_solver.cpp
@@ -116,8 +116,11 @@ static solver* mk_special_solver_for_logic(ast_manager & m, params_ref const & p
 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);
+    tactic_params tp;
     if (!s && logic == "QF_BV" && rw.hi_div0()) 
         s = mk_inc_sat_solver(m, p);
+    if (!s && tp.default_tactic() == "sat")
+        s = mk_inc_sat_solver(m, p);
     if (!s) 
         s = mk_smt_solver(m, p, logic);
     return s;