diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp
index 6b9402761..be6ab3064 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() {
diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h
index 173000fd1..e2b1eb682 100644
--- a/src/util/lp/lar_solver.h
+++ b/src/util/lp/lar_solver.h
@@ -80,14 +80,11 @@ public:
     }
 
 
-    lar_solver() : m_mpq_lar_core_solver(
-                                         m_settings,
-                                         *this
-                                         ),
-                   m_status(OPTIMAL),
+    lar_solver() : m_status(OPTIMAL),
                    m_infeasible_column_index(-1),
                    m_terms_start_index(1000000),
-                   m_column_type_function ([this] (unsigned j) {return m_mpq_lar_core_solver.m_column_types()[j];})    
+                   m_column_type_function ([this] (unsigned j) {return m_mpq_lar_core_solver.m_column_types()[j];}),
+                   m_mpq_lar_core_solver(m_settings, *this)
     {}
     
     void set_propagate_bounds_on_pivoted_rows_mode(bool v) {
diff --git a/src/util/lp/lp_primal_core_solver.h b/src/util/lp/lp_primal_core_solver.h
index e4d869289..e1b7445b0 100644
--- a/src/util/lp/lp_primal_core_solver.h
+++ b/src/util/lp/lp_primal_core_solver.h
@@ -32,21 +32,21 @@ class lp_primal_core_solver:public lp_core_solver_base<T, X> {
 public:
     // m_sign_of_entering is set to 1 if the entering variable needs
     // to grow and is set to -1  otherwise
-    unsigned m_column_norm_update_counter;
-    T m_enter_price_eps;
-    int m_sign_of_entering_delta;
+    unsigned       m_column_norm_update_counter;
+    T              m_enter_price_eps;
+    int            m_sign_of_entering_delta;
     vector<breakpoint<X>> m_breakpoints;
     binary_heap_priority_queue<X> m_breakpoint_indices_queue;
     indexed_vector<T> m_beta; // see Swietanowski working vector beta for column norms
-    T m_epsilon_of_reduced_cost;
-    vector<T> m_costs_backup;
-    T m_converted_harris_eps;
-    unsigned m_inf_row_index_for_tableau;
-    bool m_bland_mode_tableau;
-    int_set m_left_basis_tableau;
-    unsigned m_bland_mode_threshold;
-    unsigned m_left_basis_repeated;
-    vector<unsigned> m_leaving_candidates;
+    T                 m_epsilon_of_reduced_cost;
+    vector<T>         m_costs_backup;
+    T                 m_converted_harris_eps;
+    unsigned          m_inf_row_index_for_tableau;
+    bool              m_bland_mode_tableau;
+    int_set           m_left_basis_tableau;
+    unsigned          m_bland_mode_threshold;
+    unsigned          m_left_basis_repeated;
+    vector<unsigned>  m_leaving_candidates;
     //    T m_converted_harris_eps = convert_struct<T, double>::convert(this->m_settings.harris_feasibility_tolerance);
     std::list<unsigned> m_non_basis_list;
     void sort_non_basis();
@@ -906,8 +906,8 @@ public:
                                   low_bound_values,
                                   upper_bound_values),
         m_epsilon_of_reduced_cost(T(1)/T(10000000)),
-        m_bland_mode_threshold(1000),
-        m_beta(A.row_count()) {
+        m_beta(A.row_count()),
+        m_bland_mode_threshold(1000) {
 
         if (!(numeric_traits<T>::precise())) {
             m_converted_harris_eps = convert_struct<T, double>::convert(this->m_settings.harris_feasibility_tolerance);
diff --git a/src/util/lp/mps_reader.h b/src/util/lp/mps_reader.h
index 7a5c88f83..da5db6145 100644
--- a/src/util/lp/mps_reader.h
+++ b/src/util/lp/mps_reader.h
@@ -93,12 +93,12 @@ template <typename T, typename X>
 class mps_reader {
     enum row_type { Cost, Less_or_equal, Greater_or_equal, Equal };
     struct bound {
+        T    m_low;
+        T    m_upper;
         bool m_low_is_set;
-        T m_low;
         bool m_upper_is_set;
-        T m_upper;
         bool m_value_is_fixed;
-        T m_fixed_value;
+        T    m_fixed_value;
         bool m_free;
         // constructor
         bound() : m_low(numeric_traits<T>::zero()),
@@ -132,8 +132,8 @@ class mps_reader {
         }
     };
 
-    std::string m_file_name;
     bool m_is_OK;
+    std::string m_file_name;
     std::unordered_map<std::string, row *> m_rows;
     std::unordered_map<std::string, column *> m_columns;
     std::unordered_map<std::string, unsigned> m_names_to_var_index;
@@ -747,7 +747,8 @@ public:
 
     mps_reader(std::string file_name):
         m_is_OK(true),
-        m_file_name(file_name), m_file_stream(file_name),
+        m_file_name(file_name), 
+        m_file_stream(file_name),
         m_cost_line_count(0),
         m_line_number(0),
         m_message_stream(& std::cout) {}