diff --git a/src/math/simplex/sparse_matrix_def.h b/src/math/simplex/sparse_matrix_def.h
index 0b48e0049..c68116190 100644
--- a/src/math/simplex/sparse_matrix_def.h
+++ b/src/math/simplex/sparse_matrix_def.h
@@ -468,6 +468,10 @@ namespace simplex {
         g.reset();
         row_iterator it = row_begin(r), end = row_end(r); 
         for (; it != end && !m.is_one(g); ++it) {
+            if (!m.is_int(it->m_coeff)) {
+                g = numeral(1);  
+                break;
+            }
             if (m.is_zero(g)) g = it->m_coeff;
             else m.gcd(g, it->m_coeff, g);
         }   
diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp
index 44f03d99c..d42176280 100644
--- a/src/opt/opt_solver.cpp
+++ b/src/opt/opt_solver.cpp
@@ -52,6 +52,7 @@ namespace opt {
         if (m_params.m_case_split_strategy == CS_ACTIVITY_DELAY_NEW) {            
             m_params.m_relevancy_lvl = 0;
         }
+        m_params.m_arith_auto_config_simplex = false;
         // m_params.m_auto_config = false;
     }
 
@@ -65,6 +66,7 @@ namespace opt {
         m_dump_benchmarks = p.dump_benchmarks();
         m_params.updt_params(_p);
         m_context.updt_params(_p);
+        m_params.m_arith_auto_config_simplex = false;
     }
 
     solver* opt_solver::translate(ast_manager& m, params_ref const& p) {
@@ -437,6 +439,11 @@ namespace opt {
             smt::theory_dense_smi& th = dynamic_cast<smt::theory_dense_smi&>(opt);
             return th.mk_ge(m_fm, v, val);
         }
+
+        if (typeid(smt::theory_dense_mi) == typeid(opt)) {
+            smt::theory_dense_mi& th = dynamic_cast<smt::theory_dense_mi&>(opt);
+            return th.mk_ge(m_fm, v, val);
+        }
         
         IF_VERBOSE(0, verbose_stream() << "WARNING: unhandled theory " << typeid(opt).name() << "\n";);
         return expr_ref(m.mk_true(), m);
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 860105583..c484808ec 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -473,7 +473,7 @@ namespace sat {
         VERIFY(ENABLE_TERNARY);
         bool reinit = false;
         if (m_config.m_drat) m_drat.add(c, c.is_learned());
-        TRACE("sat", tout << c << "\n";);
+        TRACE("sat_verbose", tout << c << "\n";);
         SASSERT(!c.was_removed());
         m_watches[(~c[0]).index()].push_back(watched(c[1], c[2]));
         m_watches[(~c[1]).index()].push_back(watched(c[0], c[2]));
diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp
index 6931203e7..9aec90e32 100644
--- a/src/smt/smt_setup.cpp
+++ b/src/smt/smt_setup.cpp
@@ -302,12 +302,6 @@ namespace smt {
         if (m_manager.proofs_enabled()) {
             m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));
         }
-        else if (!m_params.m_arith_auto_config_simplex && is_dense(st)) {
-            if (!st.m_has_rational && !m_params.m_model && st.arith_k_sum_is_small())
-                m_context.register_plugin(alloc(smt::theory_dense_smi, m_manager, m_params));
-            else
-                m_context.register_plugin(alloc(smt::theory_dense_mi, m_manager, m_params));
-        }
         else {
             if (m_params.m_arith_auto_config_simplex || st.m_num_uninterpreted_constants > 4 * st.m_num_bool_constants 
                 || st.m_num_ite_terms > 0 /* theory_rdl and theory_frdl do not support ite-terms */) {