diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp
index 0a13bfe31..6b9402761 100644
--- a/src/smt/smt_setup.cpp
+++ b/src/smt/smt_setup.cpp
@@ -471,12 +471,16 @@ namespace smt {
         setup_r_arith();
     }
 
+    void setup::setup_QF_LIRA(static_features const& st) {
+        setup_mi_arith();
+    }
+
     void setup::setup_QF_LIA() {
         TRACE("setup", tout << "setup_QF_LIA(st)\n";);
         m_params.m_relevancy_lvl       = 0;
         m_params.m_arith_expand_eqs    = true;
         m_params.m_arith_reflect       = false; 
-        m_params.m_arith_propagate_eqs = false;
+        m_params.m_arith_propagate_eqs = false; 
         m_params.m_nnf_cnf             = false;
         setup_i_arith();
     }
@@ -721,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() {
@@ -936,7 +940,9 @@ namespace smt {
         }
         
         if (st.num_theories() == 1 && is_arith(st)) {
-            if (st.m_has_real)
+            if (st.m_has_int && st.m_has_real) 
+                setup_QF_LIRA(st);
+            else if (st.m_has_real)
                 setup_QF_LRA(st);
             else
                 setup_QF_LIA(st);
diff --git a/src/smt/smt_setup.h b/src/smt/smt_setup.h
index cffc96bb8..f12cc5e09 100644
--- a/src/smt/smt_setup.h
+++ b/src/smt/smt_setup.h
@@ -65,6 +65,7 @@ namespace smt {
         void setup_QF_LRA();
         void setup_QF_LRA(static_features const & st);
         void setup_QF_LIA();
+        void setup_QF_LIRA(static_features const& st);
         void setup_QF_LIA(static_features const & st);
         void setup_QF_UFLIA();
         void setup_QF_UFLIA(static_features & st);
diff --git a/src/tactic/smtlogics/qflra_tactic.cpp b/src/tactic/smtlogics/qflra_tactic.cpp
index 41f0e16f3..1fbecef2d 100644
--- a/src/tactic/smtlogics/qflra_tactic.cpp
+++ b/src/tactic/smtlogics/qflra_tactic.cpp
@@ -72,5 +72,17 @@ tactic * mk_qflra_tactic(ast_manager & m, params_ref const & p) {
     //                            using_params(mk_smt_tactic(), pivot_p)),
     //                    p);
 
+#if 0
+
+    params_ref simplex_0, simplex_1, simplex_2;
+    simplex_0.set("lp.simplex_strategy", 0);    
+    simplex_1.set("lp.simplex_strategy", 1);    
+    simplex_2.set("lp.simplex_strategy", 1);
+    
+    tactic* lp_par = par_or(using_params(mk_smt_tactic(), simplex_0), 
+                            using_params(mk_smt_tactic(), simplex_1), 
+                            using_params(mk_smt_tactic(), simplex_2));
+                            
+#endif
     return using_params(using_params(mk_smt_tactic(), pivot_p), p);
 }