diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 4cff79cf2..05aa33d13 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -656,8 +656,8 @@ namespace smt {
             m_asserted_qhead(0), 
             m_assume_eq_head(0),
             m_num_conflicts(0),
-            m_solver(0),
             m_model_eqs(DEFAULT_HASHTABLE_INITIAL_CAPACITY, var_value_hash(*this), var_value_eq(*this)),
+            m_solver(0),
             m_resource_limit(*this) {
         }
         
diff --git a/src/util/lp/lp_core_solver_base.h b/src/util/lp/lp_core_solver_base.h
index 03034b31d..4e9d3dfa3 100644
--- a/src/util/lp/lp_core_solver_base.h
+++ b/src/util/lp/lp_core_solver_base.h
@@ -18,6 +18,7 @@ namespace lean {
 template <typename T, typename X> // X represents the type of the x variable and the bounds
 class lp_core_solver_base {    
     unsigned m_total_iterations;
+    unsigned m_iters_with_no_cost_growing;
     unsigned inc_total_iterations() { ++m_settings.st().m_total_iterations; return m_total_iterations++; }
 private:
     lp_status m_status;
@@ -47,7 +48,6 @@ public:
     indexed_vector<T>     m_w; // the vector featuring in 24.3 of the Chvatal book
     vector<T>             m_d; // the vector of reduced costs
     indexed_vector<T>     m_ed; // the solution of B*m_ed = a
-    unsigned              m_iters_with_no_cost_growing;
     const vector<column_type> & m_column_types;
     const vector<X> &     m_low_bounds;
     const vector<X> &     m_upper_bounds;
@@ -678,6 +678,13 @@ public:
                 lean_assert(is_zero(this->m_costs[j]));
         }
         return true;
-}
+    }
+    unsigned & iters_with_no_cost_growing() {
+        return m_iters_with_no_cost_growing;
+    }
+
+    const unsigned & iters_with_no_cost_growing() const {
+        return m_iters_with_no_cost_growing;
+    }
 };
 }
diff --git a/src/util/lp/lp_core_solver_base.hpp b/src/util/lp/lp_core_solver_base.hpp
index 6bd1c807c..6407aec07 100644
--- a/src/util/lp/lp_core_solver_base.hpp
+++ b/src/util/lp/lp_core_solver_base.hpp
@@ -22,6 +22,8 @@ lp_core_solver_base(static_matrix<T, X> & A,
                     const vector<column_type> & column_types,
                     const vector<X> & low_bound_values,
                     const vector<X> & upper_bound_values):
+    m_total_iterations(0),
+    m_iters_with_no_cost_growing(0),
     m_status(FEASIBLE),
     m_inf_set(A.column_count()),
     m_using_infeas_costs(false),
@@ -50,10 +52,7 @@ lp_core_solver_base(static_matrix<T, X> & A,
     m_steepest_edge_coefficients(A.column_count()),
     m_tracing_basis_changes(false),
     m_pivoted_rows(nullptr),
-    m_look_for_feasible_solution_only(false),
-    m_total_iterations(0),
-    m_iters_with_no_cost_growing(0)
- {
+    m_look_for_feasible_solution_only(false) {
     lean_assert(bounds_for_boxed_are_set_correctly());    
     init();
     init_basis_heading_and_non_basic_columns_vector();
diff --git a/src/util/lp/lp_dual_core_solver.hpp b/src/util/lp/lp_dual_core_solver.hpp
index 92a84e238..918beb586 100644
--- a/src/util/lp/lp_dual_core_solver.hpp
+++ b/src/util/lp/lp_dual_core_solver.hpp
@@ -429,7 +429,7 @@ template <typename T, typename X> bool lp_dual_core_solver<T, X>::basis_change_a
     if (snap_runaway_nonbasic_column(m_p)) {
         if (!this->find_x_by_solving()) {
             revert_to_previous_basis();
-            this->m_iters_with_no_cost_growing++;
+            this->iters_with_no_cost_growing()++;
             return false;
         }
     }
@@ -437,7 +437,7 @@ template <typename T, typename X> bool lp_dual_core_solver<T, X>::basis_change_a
     if (!problem_is_dual_feasible()) {
         // todo : shift the costs!!!!
         revert_to_previous_basis();
-        this->m_iters_with_no_cost_growing++;
+        this->iters_with_no_cost_growing()++;
         return false;
     }
 
@@ -730,14 +730,14 @@ template <typename T, typename X> void lp_dual_core_solver<T, X>::solve() { // s
     lean_assert(problem_is_dual_feasible());
     lean_assert(this->basis_heading_is_correct());
     this->set_total_iterations(0);
-    this->m_iters_with_no_cost_growing = 0;
+    this->iters_with_no_cost_growing() = 0;
     do {
         if (this->print_statistics_with_iterations_and_nonzeroes_and_cost_and_check_that_the_time_is_over("", *this->m_settings.get_message_ostream())){
             return;
         }
         one_iteration();
     } while (this->get_status() != FLOATING_POINT_ERROR && this->get_status() != DUAL_UNBOUNDED && this->get_status() != OPTIMAL &&
-             this->m_iters_with_no_cost_growing <= this->m_settings.max_number_of_iterations_with_no_improvements
+             this->iters_with_no_cost_growing() <= this->m_settings.max_number_of_iterations_with_no_improvements
              && this->total_iterations() <= this->m_settings.max_total_number_of_iterations);
 }
 }
diff --git a/src/util/lp/lp_primal_core_solver.h b/src/util/lp/lp_primal_core_solver.h
index e1b7445b0..93ecd3c08 100644
--- a/src/util/lp/lp_primal_core_solver.h
+++ b/src/util/lp/lp_primal_core_solver.h
@@ -905,8 +905,8 @@ public:
                                   column_type_array,
                                   low_bound_values,
                                   upper_bound_values),
-        m_epsilon_of_reduced_cost(T(1)/T(10000000)),
         m_beta(A.row_count()),
+        m_epsilon_of_reduced_cost(T(1)/T(10000000)),
         m_bland_mode_threshold(1000) {
 
         if (!(numeric_traits<T>::precise())) {
diff --git a/src/util/lp/lp_primal_core_solver.hpp b/src/util/lp/lp_primal_core_solver.hpp
index 5bcbe317b..4299edb96 100644
--- a/src/util/lp/lp_primal_core_solver.hpp
+++ b/src/util/lp/lp_primal_core_solver.hpp
@@ -628,7 +628,7 @@ template <typename T, typename X>    void lp_primal_core_solver<T, X>::backup_an
 template <typename T, typename X>    void lp_primal_core_solver<T, X>::init_run() {
     this->m_basis_sort_counter = 0; // to initiate the sort of the basis
     this->set_total_iterations(0);
-    this->m_iters_with_no_cost_growing = 0;
+    this->iters_with_no_cost_growing() = 0;
     init_inf_set();
     if (this->current_x_is_feasible() && this->m_look_for_feasible_solution_only)
         return;
@@ -664,7 +664,7 @@ void lp_primal_core_solver<T, X>::advance_on_entering_equal_leaving(int entering
         this->init_lu();
         if (!this->find_x_by_solving()) {
             this->restore_x(entering, t * m_sign_of_entering_delta);
-            this->m_iters_with_no_cost_growing++;
+            this->iters_with_no_cost_growing()++;
             LP_OUT(this->m_settings, "failing in advance_on_entering_equal_leaving for entering = " << entering << std::endl);
             return;
         }
@@ -679,7 +679,7 @@ void lp_primal_core_solver<T, X>::advance_on_entering_equal_leaving(int entering
     if (need_to_switch_costs() ||!this->current_x_is_feasible()) {
         init_reduced_costs();
     }
-    this->m_iters_with_no_cost_growing = 0;
+    this->iters_with_no_cost_growing() = 0;
 }
 
 template <typename T, typename X>void lp_primal_core_solver<T, X>::advance_on_entering_and_leaving(int entering, int leaving, X & t) {
@@ -699,14 +699,14 @@ template <typename T, typename X>void lp_primal_core_solver<T, X>::advance_on_en
     if (!pivot_compare_result){;}
     else if (pivot_compare_result == 2) { // the sign is changed, cannot continue
         this->set_status(UNSTABLE);
-        this->m_iters_with_no_cost_growing++;
+        this->iters_with_no_cost_growing()++;
         return;
     } else {
         lean_assert(pivot_compare_result == 1);
         this->init_lu();
         if (this->m_factorization == nullptr || this->m_factorization->get_status() != LU_status::OK) {
             this->set_status(UNSTABLE);
-            this->m_iters_with_no_cost_growing++;
+            this->iters_with_no_cost_growing()++;
             return;
         }
     }
@@ -728,7 +728,7 @@ template <typename T, typename X>void lp_primal_core_solver<T, X>::advance_on_en
     }
 
     if (!is_zero(t)) {
-        this->m_iters_with_no_cost_growing = 0;
+        this->iters_with_no_cost_growing() = 0;
         init_infeasibility_after_update_x_if_inf(leaving);
     }
 
@@ -783,7 +783,7 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>::advance_on_e
         this->init_lu();
         init_reduced_costs();
         if (refresh_result == 2) {
-            this->m_iters_with_no_cost_growing++;
+            this->iters_with_no_cost_growing()++;
             return;
         }
     }
@@ -934,7 +934,7 @@ template <typename T, typename X> unsigned lp_primal_core_solver<T, X>::solve()
              &&
              this->get_status() != INFEASIBLE
              &&
-             this->m_iters_with_no_cost_growing <= this->m_settings.max_number_of_iterations_with_no_improvements
+             this->iters_with_no_cost_growing() <= this->m_settings.max_number_of_iterations_with_no_improvements
              &&
              this->total_iterations() <= this->m_settings.max_total_number_of_iterations
              &&
diff --git a/src/util/lp/lp_primal_core_solver_tableau.hpp b/src/util/lp/lp_primal_core_solver_tableau.hpp
index f0316cda3..6ce491960 100644
--- a/src/util/lp/lp_primal_core_solver_tableau.hpp
+++ b/src/util/lp/lp_primal_core_solver_tableau.hpp
@@ -169,7 +169,7 @@ unsigned lp_primal_core_solver<T, X>::solve_with_tableau() {
              &&
              this->get_status() != INFEASIBLE
              &&
-             this->m_iters_with_no_cost_growing <= this->m_settings.max_number_of_iterations_with_no_improvements
+             this->iters_with_no_cost_growing() <= this->m_settings.max_number_of_iterations_with_no_improvements
              &&
              this->total_iterations() <= this->m_settings.max_total_number_of_iterations
              &&
@@ -202,7 +202,7 @@ template <typename T, typename X>void lp_primal_core_solver<T, X>::advance_on_en
         }
         this->update_basis_and_x_tableau(entering, leaving, t);
         lean_assert(this->A_mult_x_is_off() == false);
-        this->m_iters_with_no_cost_growing = 0;
+        this->iters_with_no_cost_growing() = 0;
     } else {
         this->pivot_column_tableau(entering, this->m_basis_heading[leaving]);
         this->change_basis(entering, leaving);
@@ -233,7 +233,7 @@ void lp_primal_core_solver<T, X>::advance_on_entering_equal_leaving_tableau(int
     if (need_to_switch_costs()) {
         init_reduced_costs_tableau();
     }
-    this->m_iters_with_no_cost_growing = 0;
+    this->iters_with_no_cost_growing() = 0;
 }
 template <typename T, typename X> int lp_primal_core_solver<T, X>::find_leaving_and_t_tableau(unsigned entering, X & t) {
     unsigned k = 0;
@@ -302,7 +302,7 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>::init_run_tab
         lean_assert(basis_columns_are_set_correctly());
         this->m_basis_sort_counter = 0; // to initiate the sort of the basis
         this->set_total_iterations(0);
-        this->m_iters_with_no_cost_growing = 0;
+        this->iters_with_no_cost_growing() = 0;
 		lean_assert(this->inf_set_is_correct());
         if (this->current_x_is_feasible() && this->m_look_for_feasible_solution_only)
             return;
diff --git a/src/util/lp/mps_reader.h b/src/util/lp/mps_reader.h
index da5db6145..4c08ec8e6 100644
--- a/src/util/lp/mps_reader.h
+++ b/src/util/lp/mps_reader.h
@@ -122,12 +122,15 @@ class mps_reader {
         row_type m_type;
         std::string m_name;
         std::unordered_map<std::string, T> m_row_columns;
-        T m_right_side;
         unsigned m_index;
+        T m_right_side;
         T m_range;
-        row(row_type type, std::string name, unsigned index) : m_type(type), m_name(name), m_index(index),
-                                                               m_right_side(zero_of_type<T>()),
-                                                               m_range(zero_of_type<T>())
+        row(row_type type, std::string name, unsigned index) :
+            m_type(type),
+            m_name(name),
+            m_index(index),
+            m_right_side(zero_of_type<T>()),
+            m_range(zero_of_type<T>())
         {
         }
     };
diff --git a/src/util/lp/random_updater.h b/src/util/lp/random_updater.h
index 2d65e191d..8cb9740ea 100644
--- a/src/util/lp/random_updater.h
+++ b/src/util/lp/random_updater.h
@@ -16,7 +16,6 @@ namespace lean {
 template <typename T> struct numeric_pair; // forward definition
 class lar_core_solver; // forward definition
 class random_updater {
-    unsigned range ;
     struct interval {
         bool upper_bound_is_set;
         numeric_pair<mpq> upper_bound;
@@ -61,6 +60,7 @@ class random_updater {
     };
     std::set<var_index> m_var_set;
     lar_core_solver & m_core_solver;
+    unsigned range;
     linear_combination_iterator<mpq>* m_column_j; // the actual column
     interval find_shift_interval(unsigned j);
     interval get_interval_of_non_basic_var(unsigned j);