diff --git a/src/test/smt_reader.h b/src/test/smt_reader.h
index 41eb7472e..38e3f4157 100644
--- a/src/test/smt_reader.h
+++ b/src/test/smt_reader.h
@@ -66,16 +66,17 @@ namespace lean {
         lisp_elem m_formula_lisp_elem;
 
         std::unordered_map<std::string, unsigned> m_name_to_var_index;
-        std::vector<formula_constraint> m_constraints;
-        std::string m_file_name;
-        std::ifstream m_file_stream;
-        std::string m_line;
-        bool m_is_OK;
-        unsigned m_line_number;
+        std::vector<formula_constraint>           m_constraints;
+        bool                                      m_is_OK;
+        unsigned                                  m_line_number;
+        std::string                               m_file_name;
+        std::ifstream                             m_file_stream;
+        std::string                               m_line;
         smt_reader(std::string file_name):
             m_is_OK(true),
             m_line_number(0),
-            m_file_name(file_name), m_file_stream(file_name) {
+            m_file_name(file_name), 
+            m_file_stream(file_name) {
         }
 
         void set_error() {
diff --git a/src/util/lp/bound_analyzer_on_row.h b/src/util/lp/bound_analyzer_on_row.h
index bc0b72eee..b6c3c4ef2 100644
--- a/src/util/lp/bound_analyzer_on_row.h
+++ b/src/util/lp/bound_analyzer_on_row.h
@@ -18,12 +18,13 @@ namespace lean {
 class bound_analyzer_on_row {
     
     linear_combination_iterator<mpq> & m_it;
-    unsigned m_row_or_term_index;
-    int m_column_of_u; // index of an unlimited from above monoid
-    // -1 means that such a value is not found, -2 means that at least two of such monoids were found
-    int m_column_of_l; // index of an unlimited from below monoid
-    impq m_rs;
-    bound_propagator & m_bp;
+    bound_propagator &                 m_bp;
+    unsigned           m_row_or_term_index;
+    int                m_column_of_u; // index of an unlimited from above monoid
+                               // -1 means that such a value is not found, -2 means that at least two of such monoids were found
+    int                m_column_of_l; // index of an unlimited from below monoid
+    impq               m_rs;
+
 public :
     // constructor
     bound_analyzer_on_row(
@@ -34,11 +35,11 @@ public :
                           )
         :
         m_it(it),
-        m_row_or_term_index(row_or_term_index),
-        m_rs(rs),
         m_bp(bp),
+        m_row_or_term_index(row_or_term_index),
         m_column_of_u(-1),
-        m_column_of_l(-1)
+        m_column_of_l(-1),
+        m_rs(rs)
     {}
 
 
diff --git a/src/util/lp/iterator_on_term_with_basis_var.h b/src/util/lp/iterator_on_term_with_basis_var.h
index 74a2c4038..3dd217103 100644
--- a/src/util/lp/iterator_on_term_with_basis_var.h
+++ b/src/util/lp/iterator_on_term_with_basis_var.h
@@ -8,15 +8,15 @@
 #include "util/lp/lar_term.h"
 namespace lean {
 struct iterator_on_term_with_basis_var:linear_combination_iterator<mpq> {
-    std::unordered_map<unsigned, mpq>::const_iterator m_i; // the offset in term coeffs
-    bool m_term_j_returned;
     const lar_term & m_term;
-    unsigned m_term_j;
+    std::unordered_map<unsigned, mpq>::const_iterator m_i; // the offset in term coeffs
+    bool             m_term_j_returned;
+    unsigned         m_term_j;
     unsigned size() const {return static_cast<unsigned>(m_term.m_coeffs.size() + 1);}
     iterator_on_term_with_basis_var(const lar_term & t, unsigned term_j) :
-        m_term_j_returned(false),
-        m_i(t.m_coeffs.begin()),
         m_term(t),
+        m_i(t.m_coeffs.begin()),
+        m_term_j_returned(false),
         m_term_j(term_j) {}
 
     bool next(mpq & a, unsigned & i) {