diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp
index be6ab3064..4dd1e2510 100644
--- a/src/smt/smt_setup.cpp
+++ b/src/smt/smt_setup.cpp
@@ -725,8 +725,8 @@ namespace smt {
 
     void setup::setup_r_arith() {
         // to disable theory lra
-        m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));        
-        // m_context.register_plugin(alloc(smt::theory_lra, m_manager, m_params));
+        // m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));        
+        m_context.register_plugin(alloc(smt::theory_lra, m_manager, m_params));
     }
 
     void setup::setup_mi_arith() {
@@ -940,7 +940,7 @@ namespace smt {
         }
         
         if (st.num_theories() == 1 && is_arith(st)) {
-            if (st.m_has_int && st.m_has_real) 
+            if ((st.m_has_int && st.m_has_real) || (st.m_num_non_linear != 0)) 
                 setup_QF_LIRA(st);
             else if (st.m_has_real)
                 setup_QF_LRA(st);