diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp
index 5f916899b..74b9328e8 100644
--- a/src/smt/smt_setup.cpp
+++ b/src/smt/smt_setup.cpp
@@ -838,7 +838,7 @@ namespace smt {
                 m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));
             break;
         case AS_NEW_ARITH:
-            if (st.m_num_non_linear != 0) 
+            if (st.m_num_non_linear != 0 && st.m_has_int) 
                 m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));
             else 
                 setup_lra_arith();