diff --git a/src/tests/util/lp/lp.cpp b/src/tests/util/lp/lp.cpp
index 7766c7a415..96e5378944 100644
--- a/src/tests/util/lp/lp.cpp
+++ b/src/tests/util/lp/lp.cpp
@@ -221,7 +221,7 @@ void test_small_lu(lp_settings & settings) {
     l.change_basis(3, 2);
     cout << "we were factoring " << std::endl;
 #ifdef LEAN_DEBUG
-    print_matrix(get_B(l),std::cout);
+    print_matrix(get_B(l), std::cout);
 #endif
     lean_assert(l.is_correct());
 }
@@ -2082,7 +2082,7 @@ int my_readdir(DIR *dirp, struct dirent *
 #endif
                , struct dirent **result) {
 #ifdef LEAN_WINDOWS
-    *result = readdir(dirp);
+    *result = readdir(dirp); // NOLINT
     return *result != nullptr? 0 : 1;
 #else
     return readdir_r(dirp, entry, result);
diff --git a/src/util/lp/binary_heap_priority_queue.cpp b/src/util/lp/binary_heap_priority_queue.cpp
index 7cf693b790..4659f24b34 100644
--- a/src/util/lp/binary_heap_priority_queue.cpp
+++ b/src/util/lp/binary_heap_priority_queue.cpp
@@ -4,6 +4,7 @@
 
   Author: Lev Nachmanson
 */
+#include <vector>
 #include "util/lp/binary_heap_priority_queue.h"
 namespace lean {
 // is is the child place in heap
@@ -190,5 +191,5 @@ template <typename T> void binary_heap_priority_queue<T>::print(std::ostream & o
     for (int i = 0; i < index.size(); i++)
         enqueue(index[i], prs[i]);
 }
-#endif 
+#endif
 }
diff --git a/src/util/lp/binary_heap_priority_queue.h b/src/util/lp/binary_heap_priority_queue.h
index f581c909da..0ff18fcaf9 100644
--- a/src/util/lp/binary_heap_priority_queue.h
+++ b/src/util/lp/binary_heap_priority_queue.h
@@ -40,7 +40,7 @@ public:
     void put_to_heap(unsigned i, unsigned o);
 
     void enqueue_new(unsigned o, const T& priority);
-    
+
     // This method can work with an element that is already in the queue.
     // In this case the priority will be changed and the queue adjusted.
     void enqueue(unsigned o, const T & priority);
diff --git a/src/util/lp/binary_heap_upair_queue.cpp b/src/util/lp/binary_heap_upair_queue.cpp
index c012b99ce9..a2d22fa046 100644
--- a/src/util/lp/binary_heap_upair_queue.cpp
+++ b/src/util/lp/binary_heap_upair_queue.cpp
@@ -5,7 +5,7 @@
   Author: Lev Nachmanson
 */
 
-
+#include <set>
 #include "util/lp/binary_heap_upair_queue.h"
 namespace lean {
 template <typename T> binary_heap_upair_queue<T>::binary_heap_upair_queue(unsigned size) : m_q(size), m_pairs(size) {
diff --git a/src/util/lp/core_solver_pretty_printer.cpp b/src/util/lp/core_solver_pretty_printer.cpp
index 8b4c9ee0ad..f1bc65cc9e 100644
--- a/src/util/lp/core_solver_pretty_printer.cpp
+++ b/src/util/lp/core_solver_pretty_printer.cpp
@@ -4,6 +4,8 @@
 
   Author: Lev Nachmanson
 */
+#include <string>
+#include <algorithm>
 #include "util/lp/lp_core_solver_base.h"
 #include "util/lp/core_solver_pretty_printer.h"
 namespace lean {
diff --git a/src/util/lp/dense_matrix.cpp b/src/util/lp/dense_matrix.cpp
index bcb67edc17..e1186bc9b4 100644
--- a/src/util/lp/dense_matrix.cpp
+++ b/src/util/lp/dense_matrix.cpp
@@ -5,15 +5,16 @@
   Author: Lev Nachmanson
 */
 #ifdef LEAN_DEBUG
+#include <vector>
 #include "util/lp/dense_matrix.h"
 namespace lean {
-template <typename T, typename X> dense_matrix<T,X>::dense_matrix(unsigned m, unsigned n) : m_m(m), m_n(n) {
+template <typename T, typename X> dense_matrix<T, X>::dense_matrix(unsigned m, unsigned n) : m_m(m), m_n(n) {
     m_values = new T[m * n];
     for (unsigned i = 0; i < m * n; i ++)
         m_values[i] = numeric_traits<T>::zero();
 }
 
-template <typename T, typename X> dense_matrix<T,X> dense_matrix<T,X>::operator*=(matrix<T, X> const & a){
+template <typename T, typename X> dense_matrix<T, X> dense_matrix<T, X>::operator*=(matrix<T, X> const & a) {
     lean_assert(column_count() == a.row_count());
     dense_matrix c(row_count(), a.column_count());
     for (unsigned i = 0; i < row_count(); i++) {
@@ -28,8 +29,8 @@ template <typename T, typename X> dense_matrix<T,X> dense_matrix<T,X>::operator*
     *this = c;
     return *this;
 }
-template <typename T, typename X> dense_matrix<T,X>&
-dense_matrix<T,X>::operator=(matrix<T, X> const & other){
+template <typename T, typename X> dense_matrix<T, X>&
+dense_matrix<T, X>::operator=(matrix<T, X> const & other){
     if ( this == & other)
         return *this;
     m_values = new T[m_m * m_n];
@@ -39,8 +40,8 @@ dense_matrix<T,X>::operator=(matrix<T, X> const & other){
     return *this;
 }
 
-template <typename T, typename X> dense_matrix<T,X>&
-dense_matrix<T,X>::operator=(dense_matrix const & other){
+template <typename T, typename X> dense_matrix<T, X>&
+dense_matrix<T, X>::operator=(dense_matrix const & other){
     if ( this == & other)
         return *this;
     m_m = other.m_m;
@@ -53,14 +54,14 @@ dense_matrix<T,X>::operator=(dense_matrix const & other){
     return *this;
 }
 
-template <typename T, typename X> dense_matrix<T,X>::dense_matrix(dense_matrix<T, X> const & other) : m_m(other.row_count()), m_n(other.column_count()) {
+template <typename T, typename X> dense_matrix<T, X>::dense_matrix(dense_matrix<T, X> const & other) : m_m(other.row_count()), m_n(other.column_count()) {
     m_values = new T[m_m * m_n];
     for (unsigned i = 0; i < m_m; i ++)
         for (unsigned j = 0; j < m_n; j++)
             m_values[i * m_n + j] = other.get_elem(i, j);
 }
 
-template <typename T, typename X> dense_matrix<T,X>::dense_matrix(matrix<T, X> const & other) :
+template <typename T, typename X> dense_matrix<T, X>::dense_matrix(matrix<T, X> const & other) :
     m_m(other.row_count()),
     m_n(other.column_count()) {
     m_values = new T[m_m * m_n];
diff --git a/src/util/lp/dense_matrix.h b/src/util/lp/dense_matrix.h
index fc358a34ae..3e2f47bee8 100644
--- a/src/util/lp/dense_matrix.h
+++ b/src/util/lp/dense_matrix.h
@@ -6,6 +6,7 @@
 */
 #pragma once
 #ifdef LEAN_DEBUG
+#include <vector>
 #include "util/numerics/double.h"
 #include "util/lp/matrix.h"
 namespace lean {
diff --git a/src/util/lp/dense_matrix_instances.cpp b/src/util/lp/dense_matrix_instances.cpp
index f4907d268f..0c8e9ff38c 100644
--- a/src/util/lp/dense_matrix_instances.cpp
+++ b/src/util/lp/dense_matrix_instances.cpp
@@ -5,9 +5,10 @@
   Author: Lev Nachmanson
 */
 #ifdef LEAN_DEBUG
+#include <vector>
 #include "util/lp/dense_matrix.cpp"
 template lean::dense_matrix<double, double> lean::operator*<double, double>(lean::matrix<double, double>&, lean::matrix<double, double>&);
-template void lean::dense_matrix<double, double>::apply_from_left(std::vector<double, std::allocator<double> >&);
+template void lean::dense_matrix<double, double>::apply_from_left(std::vector<double> &);
 template lean::dense_matrix<double, double>::dense_matrix(lean::matrix<double, double> const&);
 template lean::dense_matrix<double, double>::dense_matrix(unsigned int, unsigned int);
 template lean::dense_matrix<double, double>& lean::dense_matrix<double, double>::operator=(lean::dense_matrix<double, double> const&);
diff --git a/src/util/lp/eta_matrix.cpp b/src/util/lp/eta_matrix.cpp
index c8e1de612b..28088c7fca 100644
--- a/src/util/lp/eta_matrix.cpp
+++ b/src/util/lp/eta_matrix.cpp
@@ -15,7 +15,7 @@ template <typename T, typename X>
 void eta_matrix<T, X>::apply_from_left(std::vector<X> & w, lp_settings & ) {
     auto w_at_column_index = w[m_column_index];
     w[m_column_index] /= m_diagonal_element;
-    for (auto & it: m_column_vector.m_data) {
+    for (auto & it : m_column_vector.m_data) {
         w[it.first] += w_at_column_index * it.second;
     }
 }
@@ -57,7 +57,7 @@ void eta_matrix<T, X>::apply_from_right(std::vector<T> & w) {
     // deb.apply_from_right(clone_w);
 #endif
     T t = w[m_column_index] / m_diagonal_element;
-    for (auto & it :m_column_vector.m_data) {
+    for (auto & it : m_column_vector.m_data) {
         t += w[it.first] * it.second;
     }
     w[m_column_index] = t;
diff --git a/src/util/lp/eta_matrix_instances.cpp b/src/util/lp/eta_matrix_instances.cpp
index e59d28d4de..61b25b0011 100644
--- a/src/util/lp/eta_matrix_instances.cpp
+++ b/src/util/lp/eta_matrix_instances.cpp
@@ -4,6 +4,8 @@
 
   Author: Lev Nachmanson
 */
+#include <memory>
+#include <vector>
 #include "util/lp/numeric_pair.h"
 #include "util/lp/eta_matrix.cpp"
 #ifdef LEAN_DEBUG
@@ -18,7 +20,7 @@ template void lean::eta_matrix<lean::mpq, lean::mpq>::apply_from_left(std::vecto
 template void lean::eta_matrix<lean::mpq, lean::mpq>::apply_from_right(std::vector<lean::mpq, std::allocator<lean::mpq> >&);
 template void lean::eta_matrix<lean::mpq, lean::mpq>::conjugate_by_permutation(lean::permutation_matrix<lean::mpq, lean::mpq>&);
 template void lean::eta_matrix<lean::mpq, lean::numeric_pair<lean::mpq> >::apply_from_left(std::vector<lean::numeric_pair<lean::mpq>, std::allocator<lean::numeric_pair<lean::mpq> > >&, lean::lp_settings&);
-template void lean::eta_matrix<lean::mpq, lean::numeric_pair<lean::mpq> >::apply_from_right(std::vector<lean::mpq, std::allocator<lean::mpq> >&);
+template void lean::eta_matrix<lean::mpq, lean::numeric_pair<lean::mpq> >::apply_from_right(std::vector<lean::mpq>&);
 template void lean::eta_matrix<lean::mpq, lean::numeric_pair<lean::mpq> >::conjugate_by_permutation(lean::permutation_matrix<lean::mpq, lean::numeric_pair<lean::mpq> >&);
 template void lean::eta_matrix<double, double>::apply_from_left_local<double>(lean::indexed_vector<double>&, lean::lp_settings&);
 template void lean::eta_matrix<lean::mpq, lean::mpq>::apply_from_left_local<lean::mpq>(lean::indexed_vector<lean::mpq>&, lean::lp_settings&);
diff --git a/src/util/lp/indexed_vector.cpp b/src/util/lp/indexed_vector.cpp
index 60b3f17ab4..e264f85998 100644
--- a/src/util/lp/indexed_vector.cpp
+++ b/src/util/lp/indexed_vector.cpp
@@ -4,7 +4,7 @@
 
   Author: Lev Nachmanson
 */
-
+#include <vector>
 #include "util/lp/indexed_vector.h"
 namespace lean {
 
@@ -37,38 +37,38 @@ void print_vector(const std::vector<mpq> & t, std::ostream & out) {
     out << std::endl;
 }
 
-template <typename T> 
+template <typename T>
 void indexed_vector<T>::resize(unsigned data_size) {
     m_index.clear();
     m_data.resize(data_size, numeric_traits<T>::zero());
 }
 
-template <typename T> 
+template <typename T>
 void indexed_vector<T>::set_value(T value, unsigned index) {
     m_data[index] = value;
     m_index.push_back(index);
 }
 
-template <typename T> 
+template <typename T>
 void indexed_vector<T>::clear() {
     for (unsigned i : m_index)
         m_data[i] = numeric_traits<T>::zero();
     m_index.clear();
 }
-template <typename T> 
+template <typename T>
 void indexed_vector<T>::clear_all() {
     unsigned i = m_data.size();
     while (i--)  m_data[i] = numeric_traits<T>::zero();
     m_index.clear();
 }
-template <typename T> 
+template <typename T>
 void indexed_vector<T>::erase_from_index(unsigned j) {
     auto it = std::find(m_index.begin(), m_index.end(), j);
     if (it != m_index.end()) m_index.erase(it);
 }
 
 #ifdef LEAN_DEBUG
-template <typename T> 
+template <typename T>
 bool indexed_vector<T>::is_OK() const {
     int size = 0;
     for (unsigned i = 0; i < m_data.size(); i++) {
@@ -80,7 +80,7 @@ bool indexed_vector<T>::is_OK() const {
     }
     return size == m_index.size();
 }
-template <typename T> 
+template <typename T>
 void indexed_vector<T>::print(std::ostream & out) {
     out << "m_index " << std::endl;
     for (unsigned i = 0; i < m_index.size(); i++) {
diff --git a/src/util/lp/indexed_vector.h b/src/util/lp/indexed_vector.h
index b06ea919e2..28398b10a1 100644
--- a/src/util/lp/indexed_vector.h
+++ b/src/util/lp/indexed_vector.h
@@ -24,7 +24,7 @@ namespace lean {
 template <typename T> void print_vector(const std::vector<T> & t, std::ostream & out);
 template <typename T> void print_vector(const buffer<T> & t, std::ostream & out);
 template <typename T> void print_sparse_vector(const std::vector<T> & t, std::ostream & out);
-    
+
 void print_vector(const std::vector<mpq> & t, std::ostream & out);
 template <typename T>
 class indexed_vector {
diff --git a/src/util/lp/lar_constraints.cpp b/src/util/lp/lar_constraints.cpp
index 7ad8c9a4b0..e9d3bedd02 100644
--- a/src/util/lp/lar_constraints.cpp
+++ b/src/util/lp/lar_constraints.cpp
@@ -4,7 +4,7 @@
 
   Author: Lev Nachmanson
 */
-
+#include <utility>
 #include "util/lp/lar_constraints.h"
 namespace lean {
 
@@ -18,7 +18,7 @@ lar_constraint::lar_constraint(const buffer<std::pair<mpq, var_index>> & left_si
         }
     }
 }
-    
+
 lar_constraint::lar_constraint(const lar_base_constraint & c): lar_base_constraint(c.m_kind, c.m_right_side, c.m_index) {
     for (auto t : c.get_left_side_coefficients())
         m_left_side.insert(std::make_pair(t.second, t.first));
@@ -44,4 +44,4 @@ buffer<std::pair<mpq, var_index>> lar_normalized_constraint::get_left_side_coeff
 
 
 
-    
+
diff --git a/src/util/lp/lar_constraints.h b/src/util/lp/lar_constraints.h
index 7c1f9eafbf..1b0323deef 100644
--- a/src/util/lp/lar_constraints.h
+++ b/src/util/lp/lar_constraints.h
@@ -7,6 +7,7 @@
 
 #pragma once
 #include <vector>
+#include <utility>
 #include "util/debug.h"
 #include "util/buffer.h"
 #include "util/numerics/numeric_traits.h"
diff --git a/src/util/lp/lar_core_solver.cpp b/src/util/lp/lar_core_solver.cpp
index d5c8b206ba..af1a52b10e 100644
--- a/src/util/lp/lar_core_solver.cpp
+++ b/src/util/lp/lar_core_solver.cpp
@@ -10,6 +10,8 @@
 
   Author: Lev Nachmanson
 */
+#include <string>
+#include <vector>
 #include "util/lp/lar_core_solver.h"
 namespace lean {
 template <typename T, typename X>
@@ -322,7 +324,7 @@ template <typename T, typename X>    void lar_core_solver<T, X>::try_add_breakpo
     }
 }
 
-template <typename T, typename X>  std::string  lar_core_solver<T, X>::break_type_to_string(breakpoint_type type) {
+template <typename T, typename X> std::string lar_core_solver<T, X>::break_type_to_string(breakpoint_type type) {
     switch (type){
     case low_break: return "low_break";
     case upper_break: return "upper_break";
diff --git a/src/util/lp/lar_core_solver.h b/src/util/lp/lar_core_solver.h
index f74a85f430..da5e8b76c8 100644
--- a/src/util/lp/lar_core_solver.h
+++ b/src/util/lp/lar_core_solver.h
@@ -46,7 +46,7 @@ public:
     void init_costs();
 
     void init_cost_for_column(unsigned j);
-    
+
     void init_local();
 
     // returns m_sign_of_alpha_r
@@ -120,7 +120,7 @@ public:
     void prefix();
 
     bool is_tiny() const { return this->m_m < 10 && this->m_n < 20; }
-    
+
     bool is_empty() const { return this->m_m == 0 || this->m_n == 0; }
 
     void feasibility_loop();
diff --git a/src/util/lp/lar_core_solver_instances.cpp b/src/util/lp/lar_core_solver_instances.cpp
index e3852483a0..c89328ec3e 100644
--- a/src/util/lp/lar_core_solver_instances.cpp
+++ b/src/util/lp/lar_core_solver_instances.cpp
@@ -4,6 +4,11 @@
 
   Author: Lev Nachmanson
 */
+#include <utility>
+#include <memory>
+#include <string>
+#include <vector>
+#include <functional>
 #include "util/lp/lar_core_solver.cpp"
 template lean::lar_core_solver<lean::mpq, lean::numeric_pair<lean::mpq> >::lar_core_solver(std::vector<lean::numeric_pair<lean::mpq>, std::allocator<lean::numeric_pair<lean::mpq> > >&, std::vector<lean::column_type, std::allocator<lean::column_type> >&, std::vector<lean::numeric_pair<lean::mpq>, std::allocator<lean::numeric_pair<lean::mpq> > >&, std::vector<lean::numeric_pair<lean::mpq>, std::allocator<lean::numeric_pair<lean::mpq> > >&, std::vector<unsigned int, std::allocator<unsigned int> >&, lean::static_matrix<lean::mpq, lean::numeric_pair<lean::mpq> >&, lean::lp_settings&, std::unordered_map<unsigned int, std::string, std::hash<unsigned int>, std::equal_to<unsigned int>, std::allocator<std::pair<unsigned int const, std::string> > >&, std::vector<lean::numeric_pair<lean::mpq>, std::allocator<lean::numeric_pair<lean::mpq> > >&, std::vector<lean::mpq, std::allocator<lean::mpq> >&);
 template void lean::lar_core_solver<lean::mpq, lean::numeric_pair<lean::mpq> >::solve();
diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp
index 585fd7e55a..1e8f50f01e 100644
--- a/src/util/lp/lar_solver.cpp
+++ b/src/util/lp/lar_solver.cpp
@@ -4,7 +4,9 @@
 
   Author: Lev Nachmanson
 */
-
+#include <string>
+#include <algorithm>
+#include <vector>
 #include "util/lp/lar_solver.h"
 namespace lean {
 double conversion_helper <double>::get_low_bound(const column_info<mpq> & ci) {
diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h
index d72f13f6ef..4020441e16 100644
--- a/src/util/lp/lar_solver.h
+++ b/src/util/lp/lar_solver.h
@@ -170,7 +170,7 @@ public:
     bool the_righ_sides_do_not_sum_to_zero(const buffer<pair<mpq, unsigned>> & evidence);
 
     bool the_evidence_is_correct();
-    
+
     void update_column_info_of_normalized_constraints();
 
     template <typename V>
diff --git a/src/util/lp/lp_core_solver_base.cpp b/src/util/lp/lp_core_solver_base.cpp
index d995aa3007..1ddd65d572 100644
--- a/src/util/lp/lp_core_solver_base.cpp
+++ b/src/util/lp/lp_core_solver_base.cpp
@@ -4,6 +4,9 @@
 
   Author: Lev Nachmanson
 */
+#include <set>
+#include <string>
+#include <vector>
 #include "util/lp/lp_core_solver_base.h"
 namespace lean {
 void init_basic_part_of_basis_heading(std::vector<unsigned> & basis, unsigned m, std::vector<int> & basis_heading) {
@@ -63,7 +66,8 @@ lp_core_solver_base(static_matrix<T, X> & A,
     m_low_bound_values(low_bound_values),
     m_upper_bound_values(upper_bound_values),
     m_column_norms(m_n, T(1)),
-    m_copy_of_xB(m_m) {
+    m_copy_of_xB(m_m),
+    m_steepest_edge_coefficients(A.column_count()) {
     if (m_m) {
         lean_assert(m_A.col_val_equal_to_row_val());
         init();
diff --git a/src/util/lp/lp_core_solver_base.h b/src/util/lp/lp_core_solver_base.h
index cc0c634d63..697a797b2e 100644
--- a/src/util/lp/lp_core_solver_base.h
+++ b/src/util/lp/lp_core_solver_base.h
@@ -59,6 +59,9 @@ public:
     std::vector<T> m_column_norms; // the approximate squares of column norms that help choosing a profitable column
     std::vector<X> m_copy_of_xB;
     unsigned m_refactor_counter = 200;
+    unsigned m_sort_counter = 0;
+    std::vector<T> m_steepest_edge_coefficients;
+
     lp_core_solver_base(static_matrix<T, X> & A,
                         std::vector<X> & b, // the right side vector
                         std::vector<unsigned> & basis,
@@ -69,7 +72,7 @@ public:
                         std::vector<column_type> & column_types,
                         std::vector<X> & low_bound_values,
                         std::vector<X> & upper_bound_values);
-    
+
     void allocate_basis_heading();
     void init();
 
@@ -144,7 +147,7 @@ public:
     bool print_statistics_and_check_that_the_time_is_over(unsigned total_iterations);
 
     void set_non_basic_x_to_correct_bounds();
-    
+
     bool at_bound(const X &x, const X & bound) const {
         return !below_bound(x, bound) && !above_bound(x, bound);
     }
@@ -171,7 +174,7 @@ public:
         return below_bound(m_x[p], m_upper_bound_values[p]);
     }
 
-    
+
     bool x_above_upper_bound(unsigned p) {
         return above_bound(m_x[p], m_upper_bound_values[p]);
     }
diff --git a/src/util/lp/lp_core_solver_base_instances.cpp b/src/util/lp/lp_core_solver_base_instances.cpp
index a3ec83e663..dbf5c93b61 100644
--- a/src/util/lp/lp_core_solver_base_instances.cpp
+++ b/src/util/lp/lp_core_solver_base_instances.cpp
@@ -4,6 +4,11 @@
 
   Author: Lev Nachmanson
 */
+#include <utility>
+#include <memory>
+#include <string>
+#include <vector>
+#include <functional>
 #include "util/lp/lp_core_solver_base.cpp"
 template bool lean::lp_core_solver_base<double, double>::A_mult_x_is_off();
 template bool lean::lp_core_solver_base<double, double>::basis_heading_is_correct();
diff --git a/src/util/lp/lp_dual_core_solver.cpp b/src/util/lp/lp_dual_core_solver.cpp
index bf70d4d76c..65177c2181 100644
--- a/src/util/lp/lp_dual_core_solver.cpp
+++ b/src/util/lp/lp_dual_core_solver.cpp
@@ -4,6 +4,9 @@
 
   Author: Lev Nachmanson
 */
+#include <algorithm>
+#include <string>
+#include <vector>
 #include "util/lp/lp_dual_core_solver.h"
 
 namespace lean {
@@ -243,7 +246,7 @@ template <typename T, typename X> bool lp_dual_core_solver<T, X>::advance_on_kno
         return true;
     }
     calculate_beta_r_precisely();
-    this->solve_Bd(m_q); //FTRAN
+    this->solve_Bd(m_q); // FTRAN
     int pivot_compare_result = this->pivots_in_column_and_row_are_different(m_q, m_p);
     if (!pivot_compare_result){;}
     else if (pivot_compare_result == 2) { // the sign is changed, cannot continue
@@ -461,20 +464,20 @@ 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()) {
+        if (!this->find_x_by_solving()) {
             revert_to_previous_basis();
             this->m_iters_with_no_cost_growing++;
             return false;
         }
     }
 
-    if (!problem_is_dual_feasible() ) {
+    if (!problem_is_dual_feasible()) {
         // todo : shift the costs!!!!
         revert_to_previous_basis();
         this->m_iters_with_no_cost_growing++;
         return false;
     }
-    
+
     lean_assert(d_is_correct());
     return true;
 }
@@ -517,7 +520,7 @@ template <typename T, typename X> bool lp_dual_core_solver<T, X>::snap_runaway_n
     switch (this->m_column_type[j]) {
     case fixed:
     case low_bound:
-        if (! this->x_is_at_low_bound(j)) { 
+        if (!this->x_is_at_low_bound(j)) {
             this->m_x[j] = this->m_low_bound_values[j];
             return true;
         }
@@ -526,12 +529,12 @@ template <typename T, typename X> bool lp_dual_core_solver<T, X>::snap_runaway_n
         {
             bool closer_to_low_bound = abs(this->m_low_bound_values[j] - this->m_x[j]) < abs(this->m_upper_bound_values[j] - this->m_x[j]);
             if (closer_to_low_bound) {
-                if (! this->x_is_at_low_bound(j)) { 
+                if (!this->x_is_at_low_bound(j)) {
                     this->m_x[j] = this->m_low_bound_values[j];
                     return true;
                 }
             } else {
-                if (! this->x_is_at_upper_bound(j)) { 
+                if (!this->x_is_at_upper_bound(j)) {
                     this->m_x[j] = this->m_low_bound_values[j];
                     return true;
                 }
@@ -539,7 +542,7 @@ template <typename T, typename X> bool lp_dual_core_solver<T, X>::snap_runaway_n
         }
         break;
     case upper_bound:
-        if (! this->x_is_at_upper_bound(j)) { 
+        if (!this->x_is_at_upper_bound(j)) {
             this->m_x[j] = this->m_upper_bound_values[j];
             return true;
         }
diff --git a/src/util/lp/lp_dual_core_solver.h b/src/util/lp/lp_dual_core_solver.h
index 0484d7f9de..f41abf33d7 100644
--- a/src/util/lp/lp_dual_core_solver.h
+++ b/src/util/lp/lp_dual_core_solver.h
@@ -118,7 +118,7 @@ public:
     bool snap_runaway_nonbasic_column(unsigned);
 
     bool snap_runaway_nonbasic_columns();
-    
+
     unsigned get_number_of_rows_to_try_for_leaving();
 
     void update_a_wave(const T & del, unsigned j) {
diff --git a/src/util/lp/lp_dual_core_solver_instances.cpp b/src/util/lp/lp_dual_core_solver_instances.cpp
index 378b21962f..5f656c43fd 100644
--- a/src/util/lp/lp_dual_core_solver_instances.cpp
+++ b/src/util/lp/lp_dual_core_solver_instances.cpp
@@ -4,6 +4,11 @@
 
   Author: Lev Nachmanson
 */
+#include <utility>
+#include <memory>
+#include <string>
+#include <vector>
+#include <functional>
 #include "util/lp/lp_dual_core_solver.cpp"
 template lean::lp_dual_core_solver<lean::mpq, lean::mpq>::lp_dual_core_solver(lean::static_matrix<lean::mpq, lean::mpq>&, std::vector<bool, std::allocator<bool> >&, std::vector<lean::mpq, std::allocator<lean::mpq> >&, std::vector<lean::mpq, std::allocator<lean::mpq> >&, std::vector<unsigned int, std::allocator<unsigned int> >&, std::vector<lean::mpq, std::allocator<lean::mpq> >&, std::vector<lean::column_type, std::allocator<lean::column_type> >&, std::vector<lean::mpq, std::allocator<lean::mpq> >&, std::vector<lean::mpq, std::allocator<lean::mpq> >&, lean::lp_settings&, std::unordered_map<unsigned int, std::string, std::hash<unsigned int>, std::equal_to<unsigned int>, std::allocator<std::pair<unsigned int const, std::string> > > const&);
 template void lean::lp_dual_core_solver<lean::mpq, lean::mpq>::start_with_initial_basis_and_make_it_dual_feasible();
diff --git a/src/util/lp/lp_primal_core_solver.cpp b/src/util/lp/lp_primal_core_solver.cpp
index 0bf48e73a6..07972b96ee 100644
--- a/src/util/lp/lp_primal_core_solver.cpp
+++ b/src/util/lp/lp_primal_core_solver.cpp
@@ -4,7 +4,12 @@
 
   Author: Lev Nachmanson
 */
+#include <list>
+#include <vector>
 #include <fstream>
+#include <algorithm>
+#include <set>
+#include <string>
 #include "util/lp/lp_primal_core_solver.h"
 namespace lean {
 
@@ -15,35 +20,37 @@ template <typename T, typename X>
 void lp_primal_core_solver<T, X>::sort_non_basis() {
     for (unsigned j : this->m_non_basic_columns) {
         T const & da = this->m_d[j];
-        m_steepest_edge_coefficients[j] = da * da / this->m_column_norms[j];
+        this->m_steepest_edge_coefficients[j] = da * da / this->m_column_norms[j];
     }
-    
+
     std::sort(this->m_non_basic_columns.begin(), this->m_non_basic_columns.end(), [this](unsigned a, unsigned b) {
-            return m_steepest_edge_coefficients[a] > m_steepest_edge_coefficients[b];
+            return this->m_steepest_edge_coefficients[a] > this->m_steepest_edge_coefficients[b];
     });
+
+    m_non_basis_list.clear();
     // reinit m_basis_heading
-    for (int j = 0; j < this->m_non_basic_columns.size(); j++)
-        this->m_basis_heading[this->m_non_basic_columns[j]] = - j - 1;
+    for (int j = 0; j < this->m_non_basic_columns.size(); j++) {
+        unsigned col = this->m_non_basic_columns[j];
+        this->m_basis_heading[col] = - j - 1;
+        m_non_basis_list.push_back(col);
+    }
 }
 
 
 template <typename T, typename X>
 int lp_primal_core_solver<T, X>::choose_entering_column(unsigned number_of_benefitial_columns_to_go_over) { // at this moment m_y = cB * B(-1)
     lean_assert(number_of_benefitial_columns_to_go_over);
-    if (m_sort_columns_counter == 0) {
+    if (this->m_sort_counter == 0) {
         sort_non_basis();
-        m_sort_columns_counter = 20;
+        this->m_sort_counter = 20;
     } else {
-        m_sort_columns_counter--;
+        this->m_sort_counter--;
     }
-    lean_assert(m_sort_columns_counter>=0);
-    unsigned offset_in_nb = 0;
-    unsigned initial_offset_in_non_basis = offset_in_nb;
+    lean_assert(this->m_sort_counter >=0);
     T steepest_edge = zero_of_type<T>();
-    int entering = -1;
-    do {
-        unsigned j = this->m_non_basic_columns[offset_in_nb];
-        push_forward_offset_in_non_basis(offset_in_nb);
+    std::list<unsigned>::iterator entering_iter = m_non_basis_list.end();
+    for (auto non_basis_iter= m_non_basis_list.begin(); number_of_benefitial_columns_to_go_over && non_basis_iter != m_non_basis_list.end(); ++non_basis_iter) {
+        unsigned j = *non_basis_iter;
         if (m_forbidden_enterings.find(j) != m_forbidden_enterings.end()) {
             continue;
         }
@@ -76,14 +83,19 @@ int lp_primal_core_solver<T, X>::choose_entering_column(unsigned number_of_benef
         T t = dj * dj / this->m_column_norms[j];
         if (t > steepest_edge) {
             steepest_edge = t;
-            entering = j;
+            entering_iter = non_basis_iter;
             if (number_of_benefitial_columns_to_go_over)
                 number_of_benefitial_columns_to_go_over--;
         }
-    } while (number_of_benefitial_columns_to_go_over && initial_offset_in_non_basis != offset_in_nb);
-    if (entering != -1)
+    }// while (number_of_benefitial_columns_to_go_over && initial_offset_in_non_basis != offset_in_nb);
+    if (entering_iter != m_non_basis_list.end()) {
+        unsigned entering = *entering_iter;
         m_sign_of_entering_delta = this->m_d[entering] > 0? 1 : -1;
-    return entering;
+        m_non_basis_list.erase(entering_iter);
+        m_non_basis_list.push_back(entering);
+        return entering;
+    }
+    return -1;
 }
 
 
@@ -249,8 +261,7 @@ template <typename T, typename X> lp_primal_core_solver<T, X>::   lp_primal_core
                               column_type_array,
                               low_bound_values,
                               upper_bound_values),
-    m_beta(A.row_count()),
-    m_steepest_edge_coefficients(A.column_count()) {
+    m_beta(A.row_count()) {
     this->m_status = UNKNOWN;
     this->m_column_norm_update_counter = settings.column_norms_update_frequency;
 }
@@ -275,8 +286,7 @@ lp_primal_core_solver(static_matrix<T, X> & A,
                               column_type_array,
                               m_low_bound_values_dummy,
                               upper_bound_values),
-    m_beta(A.row_count()),
-    m_steepest_edge_coefficients(A.column_count()) {
+    m_beta(A.row_count()) {
     m_converted_harris_eps = convert_struct<T, double>::convert(this->m_settings.harris_feasibility_tolerance);
     lean_assert(initial_x_is_correct());
     m_low_bound_values_dummy.resize(A.column_count(), zero_of_type<T>());
@@ -426,6 +436,7 @@ template <typename T, typename X>    void lp_primal_core_solver<T, X>::calc_work
 }
 
 template <typename T, typename X>void lp_primal_core_solver<T, X>::advance_on_entering_and_leaving(int entering, int leaving, X & t) {
+    lean_assert(m_non_basis_list.back() == entering);
     lean_assert(t >= zero_of_type<X>());
     lean_assert(leaving >= 0 && entering >= 0);
     lean_assert(entering != leaving || !is_zero(t)); // otherwise nothing changes
@@ -482,6 +493,9 @@ template <typename T, typename X>void lp_primal_core_solver<T, X>::advance_on_en
         update_reduced_costs_from_pivot_row(entering, leaving);
     lean_assert(!need_to_switch_costs());
     m_forbidden_enterings.clear();
+    std::list<unsigned>::iterator it = m_non_basis_list.end();
+    it--;
+    * it = static_cast<unsigned>(leaving);
 }
 
 // void recalc_reduced_costs() {
diff --git a/src/util/lp/lp_primal_core_solver.h b/src/util/lp/lp_primal_core_solver.h
index 1528e731a8..075e422619 100644
--- a/src/util/lp/lp_primal_core_solver.h
+++ b/src/util/lp/lp_primal_core_solver.h
@@ -6,7 +6,7 @@
 */
 
 #pragma once
-
+#include <list>
 #include "util/numerics/double.h"
 #include "util/lp/lu.h"
 #include "util/lp/lp_solver.h"
@@ -30,7 +30,7 @@ namespace lean {
 // The right side b is given implicitly by x and the basis
 template <typename T, typename X>
 class lp_primal_core_solver:public lp_core_solver_base<T, X> {
-public: 
+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;
@@ -48,8 +48,7 @@ public:
     std::vector<T> m_costs_backup;
     bool m_current_x_is_feasible;
     T m_converted_harris_eps = convert_struct<T, double>::convert(this->m_settings.harris_feasibility_tolerance);
-    unsigned m_sort_columns_counter = 0;
-    std::vector<T> m_steepest_edge_coefficients;
+    std::list<unsigned> m_non_basis_list;
     void sort_non_basis();
     int choose_entering_column(unsigned number_of_benefitial_columns_to_go_over);
 
@@ -72,7 +71,7 @@ public:
     void limit_theta_on_basis_column_for_inf_case_m_neg_upper_bound(unsigned j, const T & m, X & theta) {
         lean_assert(m < 0 && this->m_column_type[j] == upper_bound);
         limit_inf_on_upper_bound_m_neg(m, this->m_x[j], this->m_upper_bound_values[j], theta);
-    }   
+    }
 
 
     void limit_theta_on_basis_column_for_inf_case_m_neg_low_bound(unsigned j, const T & m, X & theta) {
diff --git a/src/util/lp/lp_primal_core_solver_instances.cpp b/src/util/lp/lp_primal_core_solver_instances.cpp
index ef5afc832d..fc7ce3da20 100644
--- a/src/util/lp/lp_primal_core_solver_instances.cpp
+++ b/src/util/lp/lp_primal_core_solver_instances.cpp
@@ -4,10 +4,14 @@
 
   Author: Lev Nachmanson
 */
+#include <utility>
+#include <memory>
+#include <string>
+#include <vector>
+#include <functional>
 #include "util/lp/lar_solver.h"
 #include "util/lp/lp_primal_core_solver.cpp"
 namespace lean {
-//template void lar_solver::find_solution_signature_with_doubles(lar_solution_signature&);
 template void lp_primal_core_solver<double, double>::find_feasible_solution();
 template lp_primal_core_solver<double, double>::lp_primal_core_solver(static_matrix<double, double>&, std::vector<double, std::allocator<double> >&, std::vector<double, std::allocator<double> >&, std::vector<unsigned int, std::allocator<unsigned int> >&, std::vector<double, std::allocator<double> >&, std::vector<column_type, std::allocator<column_type> >&, std::vector<double, std::allocator<double> >&, lp_settings&, std::unordered_map<unsigned int, std::string, std::hash<unsigned int>, std::equal_to<unsigned int>, std::allocator<std::pair<unsigned int const, std::string> > > const&);
 template lp_primal_core_solver<double, double>::lp_primal_core_solver(static_matrix<double, double>&, std::vector<double, std::allocator<double> >&, std::vector<double, std::allocator<double> >&, std::vector<unsigned int, std::allocator<unsigned int> >&, std::vector<double, std::allocator<double> >&, std::vector<column_type, std::allocator<column_type> >&, std::vector<double, std::allocator<double> >&, std::vector<double, std::allocator<double> >&, lp_settings&, std::unordered_map<unsigned int, std::string, std::hash<unsigned int>, std::equal_to<unsigned int>, std::allocator<std::pair<unsigned int const, std::string> > > const&);
@@ -15,6 +19,4 @@ template lp_primal_core_solver<double, double>::lp_primal_core_solver(static_mat
 template unsigned lp_primal_core_solver<double, double>::solve();
 template lp_primal_core_solver<mpq, mpq>::lp_primal_core_solver(static_matrix<mpq, mpq>&, std::vector<mpq, std::allocator<mpq> >&, std::vector<mpq, std::allocator<mpq> >&, std::vector<unsigned int, std::allocator<unsigned int> >&, std::vector<mpq, std::allocator<mpq> >&, std::vector<column_type, std::allocator<column_type> >&, std::vector<mpq, std::allocator<mpq> >&, std::vector<mpq, std::allocator<mpq> >&, lp_settings&, std::unordered_map<unsigned int, std::string, std::hash<unsigned int>, std::equal_to<unsigned int>, std::allocator<std::pair<unsigned int const, std::string> > > const&);
 template unsigned lp_primal_core_solver<mpq, mpq>::solve();
-//template void lp_primal_simplex<double, double>::solve_with_total_inf();
-//template void lp_primal_simplex<mpq, mpq>::solve_with_total_inf();
 }
diff --git a/src/util/lp/lp_primal_simplex.cpp b/src/util/lp/lp_primal_simplex.cpp
index 831b1fdc4e..ab907c240d 100644
--- a/src/util/lp/lp_primal_simplex.cpp
+++ b/src/util/lp/lp_primal_simplex.cpp
@@ -4,6 +4,8 @@
 
   Author: Lev Nachmanson
 */
+#include <string>
+#include <vector>
 #include "util/lp/lp_primal_simplex.h"
 
 namespace lean {
diff --git a/src/util/lp/lp_primal_simplex_instances.cpp b/src/util/lp/lp_primal_simplex_instances.cpp
index c56dfd6ea8..b725732c87 100644
--- a/src/util/lp/lp_primal_simplex_instances.cpp
+++ b/src/util/lp/lp_primal_simplex_instances.cpp
@@ -4,6 +4,11 @@
 
   Author: Lev Nachmanson
 */
+#include <utility>
+#include <memory>
+#include <string>
+#include <vector>
+#include <functional>
 #include "util/lp/lp_primal_simplex.cpp"
 template bool lean::lp_primal_simplex<double, double>::bounds_hold(std::unordered_map<std::string, double, std::hash<std::string>, std::equal_to<std::string>, std::allocator<std::pair<std::string const, double> > > const&);
 template bool lean::lp_primal_simplex<double, double>::row_constraints_hold(std::unordered_map<std::string, double, std::hash<std::string>, std::equal_to<std::string>, std::allocator<std::pair<std::string const, double> > > const&);
diff --git a/src/util/lp/lp_settings.cpp b/src/util/lp/lp_settings.cpp
index 50ff025c87..4e0210d25d 100644
--- a/src/util/lp/lp_settings.cpp
+++ b/src/util/lp/lp_settings.cpp
@@ -5,6 +5,8 @@
   Author: Lev Nachmanson
 */
 #include <cmath>
+#include <string>
+#include <vector>
 #include "util/numerics/double.h"
 #include "util/lp/lp_settings.h"
 namespace lean {
@@ -77,7 +79,7 @@ void my_random_init(unsigned * seed) {
 }
 unsigned my_random() {
 #ifdef LEAN_WINDOWS
-    return rand();
+    return rand(); // NOLINT
 #else
     return lrand48();
 #endif
diff --git a/src/util/lp/lp_settings.h b/src/util/lp/lp_settings.h
index 02d265065e..dc27a8f332 100644
--- a/src/util/lp/lp_settings.h
+++ b/src/util/lp/lp_settings.h
@@ -6,6 +6,7 @@
 */
 
 #pragma once
+#include <vector>
 #include <string>
 #include <algorithm>
 #include <limits>
diff --git a/src/util/lp/lp_settings_instances.cpp b/src/util/lp/lp_settings_instances.cpp
index 3c5eb4a1b4..bd780d5fc2 100644
--- a/src/util/lp/lp_settings_instances.cpp
+++ b/src/util/lp/lp_settings_instances.cpp
@@ -4,5 +4,7 @@
 
   Author: Lev Nachmanson
 */
+#include <vector>
+#include <memory>
 #include "util/lp/lp_settings.cpp"
 template bool lean::vectors_are_equal<double>(std::vector<double, std::allocator<double> > const&, std::vector<double, std::allocator<double> > const&);
diff --git a/src/util/lp/lp_solver.cpp b/src/util/lp/lp_solver.cpp
index 620a207f74..a7783bf225 100644
--- a/src/util/lp/lp_solver.cpp
+++ b/src/util/lp/lp_solver.cpp
@@ -4,7 +4,9 @@
 
   Author: Lev Nachmanson
 */
-
+#include <string>
+#include <algorithm>
+#include <vector>
 #include "util/lp/lp_solver.h"
 namespace lean {
 template <typename T, typename X> column_info<T> * lp_solver<T, X>::get_or_create_column_info(unsigned column) {
@@ -373,10 +375,10 @@ template <typename T, typename X> void lp_solver<T, X>::cleanup() {
     while ((d = try_to_remove_some_rows()))
         n += d;
 
-    if (n == 1)
-        std::cout << "deleted one row" << std::endl;
-    else if (n)
-        std::cout << "deleted " << n << " rows" << std::endl;
+    // if (n == 1)
+    //     std::cout << "deleted one row" << std::endl;
+    // else if (n)
+    //     std::cout << "deleted " << n << " rows" << std::endl;
 }
 
 template <typename T, typename X> void lp_solver<T, X>::map_external_rows_to_core_solver_rows() {
@@ -532,7 +534,7 @@ template <typename T, typename X>    T lp_solver<T, X>::get_column_value_with_co
 
     return numeric_traits<T>::zero(); // returns zero for out of boundary columns
 }
-    
+
 template <typename T, typename X> void lp_solver<T, X>::set_scaled_cost(unsigned j) {
     // grab original costs but modify it with the column scales
     lean_assert(j < this->m_column_scale.size());
diff --git a/src/util/lp/lp_solver_instances.cpp b/src/util/lp/lp_solver_instances.cpp
index 2244ca9f39..42ddb9e4ca 100644
--- a/src/util/lp/lp_solver_instances.cpp
+++ b/src/util/lp/lp_solver_instances.cpp
@@ -4,7 +4,7 @@
 
   Author: Lev Nachmanson
 */
-
+#include <string>
 #include "util/lp/lp_solver.cpp"
 template void lean::lp_solver<double, double>::add_constraint(lean::lp_relation, double, unsigned int);
 template void lean::lp_solver<double, double>::cleanup();
diff --git a/src/util/lp/lu.cpp b/src/util/lp/lu.cpp
index 6761b9d5f1..edd2b0734b 100644
--- a/src/util/lp/lu.cpp
+++ b/src/util/lp/lu.cpp
@@ -4,7 +4,10 @@
 
   Author: Lev Nachmanson
 */
-
+#include <string>
+#include <algorithm>
+#include <set>
+#include <vector>
 #include "util/lp/lu.h"
 namespace lean {
 #ifdef LEAN_DEBUG
@@ -75,7 +78,7 @@ X dot_product(const std::vector<T> & a, const std::vector<X> & b, unsigned l) {
 
 
 template <typename T, typename X>
-one_elem_on_diag<T,X>::one_elem_on_diag(const one_elem_on_diag & o) {
+one_elem_on_diag<T, X>::one_elem_on_diag(const one_elem_on_diag & o) {
     m_i = o.m_i;
     m_val = o.m_val;
 #ifdef LEAN_DEBUG
@@ -710,7 +713,7 @@ void lu<T, X>::calculate_Lwave_Pwave_for_bump(unsigned replaced_column, unsigned
     calculate_Lwave_Pwave_for_last_row(lowest_row_of_the_bump, diagonal_elem);
     //         lean_assert(m_U.is_upper_triangular_and_maximums_are_set_correctly_in_rows(m_settings));
 }
-    
+
 template <typename T, typename X>
 void lu<T, X>::calculate_Lwave_Pwave_for_last_row(unsigned lowest_row_of_the_bump, T diagonal_element) {
     auto l = new one_elem_on_diag<T, X>(lowest_row_of_the_bump, diagonal_element);
diff --git a/src/util/lp/lu.h b/src/util/lp/lu.h
index 2876503e54..1abf31a270 100644
--- a/src/util/lp/lu.h
+++ b/src/util/lp/lu.h
@@ -132,7 +132,7 @@ public:
     template <typename L>
     void solve_By_when_y_is_ready(std::vector<L> & y);
     void print_indexed_vector(indexed_vector<T> & w, std::ofstream & f);
-    
+
     void print_basis(std::ostream & f);
     void print_matrix_compact(std::ostream & f);
 
@@ -275,7 +275,7 @@ public:
         init_vector_w(entering, w);
     }
 }; // end of lu
-    
+
 template <typename T, typename X>
 void init_factorization(lu<T, X>* & factorization, static_matrix<T, X> & m_A, std::vector<unsigned> & m_basis, std::vector<int> & m_basis_heading, lp_settings &m_settings, std::vector<unsigned> & non_basic_columns);
 
diff --git a/src/util/lp/lu_instances.cpp b/src/util/lp/lu_instances.cpp
index 840fd11a5c..2a4d07ac4d 100644
--- a/src/util/lp/lu_instances.cpp
+++ b/src/util/lp/lu_instances.cpp
@@ -4,7 +4,10 @@
 
   Author: Lev Nachmanson
 */
-
+#include <utility>
+#include <memory>
+#include <string>
+#include <vector>
 #include "util/lp/lu.cpp"
 template double lean::dot_product<double, double>(std::vector<double, std::allocator<double> > const&, std::vector<double, std::allocator<double> > const&, unsigned int);
 template void lean::lu<double, double>::change_basis(unsigned int, unsigned int);
@@ -45,4 +48,4 @@ template void lean::lu<lean::mpq, lean::numeric_pair<lean::mpq> >::solve_yB(std:
 template void lean::lu<lean::mpq, lean::numeric_pair<lean::mpq> >::solve_By(std::vector<lean::numeric_pair<lean::mpq>, std::allocator<lean::numeric_pair<lean::mpq> > >&);
 template void lean::lu<double, double>::init_vector_w(unsigned int, lean::indexed_vector<double>&);
 template lean::numeric_pair<lean::mpq> lean::dot_product<lean::mpq, lean::numeric_pair<lean::mpq> >(std::vector<lean::mpq, std::allocator<lean::mpq> > const&, std::vector<lean::numeric_pair<lean::mpq>, std::allocator<lean::numeric_pair<lean::mpq> > > const&, unsigned int);
-template bool lean::lu<double, double>::pivot_the_row(int);
+template bool lean::lu<double, double>::pivot_the_row(int); // NOLINT
diff --git a/src/util/lp/matrix.cpp b/src/util/lp/matrix.cpp
index d75d2d23c9..36ef385c49 100644
--- a/src/util/lp/matrix.cpp
+++ b/src/util/lp/matrix.cpp
@@ -5,6 +5,8 @@
   Author: Lev Nachmanson
 */
 #ifdef LEAN_DEBUG
+#include <vector>
+#include <string>
 #include "util/lp/matrix.h"
 namespace lean {
 template <typename T, typename X>
diff --git a/src/util/lp/matrix.h b/src/util/lp/matrix.h
index cd1a6410ad..ed0dc7e721 100644
--- a/src/util/lp/matrix.h
+++ b/src/util/lp/matrix.h
@@ -39,7 +39,6 @@ void apply_to_vector(matrix<T, X> & m, T * w);
 unsigned get_width_of_column(unsigned j, std::vector<std::vector<std::string>> & A);
 void print_matrix_with_widths(std::vector<std::vector<std::string>> & A, std::vector<unsigned> & ws, std::ostream & out);
 void print_string_matrix(std::vector<std::vector<std::string>> & A);
-    
 
 template <typename T, typename X>
 void print_matrix(matrix<T, X> const & m, std::ostream & out);
diff --git a/src/util/lp/permutation_matrix.cpp b/src/util/lp/permutation_matrix.cpp
index 58b421ce5c..e180769552 100644
--- a/src/util/lp/permutation_matrix.cpp
+++ b/src/util/lp/permutation_matrix.cpp
@@ -4,6 +4,7 @@
 
   Author: Lev Nachmanson
 */
+#include <vector>
 #include "util/lp/permutation_matrix.h"
 namespace lean {
 template <typename T, typename X> permutation_matrix<T, X>::permutation_matrix(unsigned length): m_length(length), m_permutation(length), m_rev(length) {
diff --git a/src/util/lp/permutation_matrix.h b/src/util/lp/permutation_matrix.h
index ebbdff07b6..361c2956f7 100644
--- a/src/util/lp/permutation_matrix.h
+++ b/src/util/lp/permutation_matrix.h
@@ -96,7 +96,7 @@ namespace lean {
         template <typename L>
         void apply_reverse_from_left(std::vector<L> & w);
         template <typename L>
-        void apply_reverse_from_right(std::vector<L> & w) ;
+        void apply_reverse_from_right(std::vector<L> & w);
 
         void set_val(unsigned i, unsigned pi) {
             lean_assert(i < m_length && pi < m_length);  m_permutation[i] = pi;  m_rev[pi] = i;  }
@@ -144,16 +144,16 @@ namespace lean {
         permutation_matrix<T, X> m_current;
         unsigned m_last;
     public:
-        permutation_generator(unsigned n); 
+        permutation_generator(unsigned n);
         permutation_generator(const permutation_generator & o);
         bool move_next();
-        
+
         ~permutation_generator() {
         if (m_lower != nullptr) {
         delete m_lower;
     }
     }
-        
+
     permutation_matrix<T, X> *current() {
         return &m_current;
     }
@@ -161,12 +161,12 @@ namespace lean {
 
         template <typename T, typename X>
         inline unsigned number_of_inversions(permutation_matrix<T, X> & p);
-    
+
         template <typename T, typename X>
         int sign(permutation_matrix<T, X> & p) {
         return is_even(number_of_inversions(p))? 1: -1;
     }
-    
+
         template <typename T, typename X>
         T det_val_on_perm(permutation_matrix<T, X>* u, const matrix<T, X>& m);
 
diff --git a/src/util/lp/permutation_matrix_instances.cpp b/src/util/lp/permutation_matrix_instances.cpp
index 4832c0cb27..f8a0d9bacc 100644
--- a/src/util/lp/permutation_matrix_instances.cpp
+++ b/src/util/lp/permutation_matrix_instances.cpp
@@ -4,6 +4,8 @@
 
   Author: Lev Nachmanson
 */
+#include <memory>
+#include <vector>
 #include "util/lp/permutation_matrix.cpp"
 #include "util/lp/numeric_pair.h"
 template void lean::permutation_matrix<double, double>::apply_from_right(std::vector<double, std::allocator<double> >&);
diff --git a/src/util/lp/row_eta_matrix.cpp b/src/util/lp/row_eta_matrix.cpp
index e84ce96e0e..f00884627e 100644
--- a/src/util/lp/row_eta_matrix.cpp
+++ b/src/util/lp/row_eta_matrix.cpp
@@ -4,7 +4,7 @@
 
   Author: Lev Nachmanson
 */
-
+#include <vector>
 #include "util/lp/row_eta_matrix.h"
 namespace lean {
 template <typename T, typename X>
@@ -15,7 +15,7 @@ void row_eta_matrix<T, X>::apply_from_left(std::vector<X> & w, lp_settings &) {
     //         deb.apply_from_left(clone_w, settings);
     // #endif
     auto w_at_row = w[m_row];
-    for (auto & it :m_row_vector.m_data) {
+    for (auto & it : m_row_vector.m_data) {
         w_at_row += w[it.first] * it.second;
     }
     w[m_row] = w_at_row;
diff --git a/src/util/lp/row_eta_matrix_instances.cpp b/src/util/lp/row_eta_matrix_instances.cpp
index de5e25aeb8..70d9691d75 100644
--- a/src/util/lp/row_eta_matrix_instances.cpp
+++ b/src/util/lp/row_eta_matrix_instances.cpp
@@ -4,7 +4,8 @@
 
   Author: Lev Nachmanson
 */
-
+#include <vector>
+#include <memory>
 #include "util/lp/row_eta_matrix.cpp"
 #include "util/lp/lu.h"
 namespace lean {
diff --git a/src/util/lp/scaler.cpp b/src/util/lp/scaler.cpp
index 4fc0cc879b..e36dd69815 100644
--- a/src/util/lp/scaler.cpp
+++ b/src/util/lp/scaler.cpp
@@ -4,7 +4,7 @@
 
   Author: Lev Nachmanson
 */
-
+#include <algorithm>
 #include "util/lp/scaler.h"
 #include "util/lp/numeric_pair.h"
 namespace lean {
diff --git a/src/util/lp/sparse_matrix.cpp b/src/util/lp/sparse_matrix.cpp
index fdee736d58..e9b02d43ec 100644
--- a/src/util/lp/sparse_matrix.cpp
+++ b/src/util/lp/sparse_matrix.cpp
@@ -5,7 +5,7 @@
   Author: Lev Nachmanson
 */
 
-
+#include <vector>
 #include "util/lp/sparse_matrix.h"
 namespace lean {
 template <typename T, typename X>
@@ -798,7 +798,7 @@ bool sparse_matrix<T, X>::shorten_active_matrix(unsigned row, eta_matrix<T, X> *
     if (eta_matrix == nullptr) return true;
     // it looks like double work, but the pivot scores have changed for all rows
     // touched by eta_matrix
-    for (auto & it: eta_matrix->m_column_vector.m_data) {
+    for (auto & it : eta_matrix->m_column_vector.m_data) {
         unsigned row = adjust_row(it.first);
         auto & row_values = m_rows[row];
         unsigned rnz = row_values.size();
diff --git a/src/util/lp/sparse_matrix.h b/src/util/lp/sparse_matrix.h
index 2e1511c9bf..5aa72122b9 100644
--- a/src/util/lp/sparse_matrix.h
+++ b/src/util/lp/sparse_matrix.h
@@ -109,7 +109,7 @@ public:
     void set_with_no_adjusting(unsigned row, unsigned col, T val);
 
     void set(unsigned row, unsigned col, T val);
-    
+
     T const & get_not_adjusted(unsigned row, unsigned col) const;
     T const & get(unsigned row, unsigned col) const;
 
diff --git a/src/util/lp/sparse_matrix_instances.cpp b/src/util/lp/sparse_matrix_instances.cpp
index 49ec3db7f6..b8cf51a35f 100644
--- a/src/util/lp/sparse_matrix_instances.cpp
+++ b/src/util/lp/sparse_matrix_instances.cpp
@@ -4,6 +4,8 @@
 
   Author: Lev Nachmanson
 */
+#include <vector>
+#include <memory>
 #include "util/lp/lu.h"
 #include "util/lp/sparse_matrix.cpp"
 namespace lean {
diff --git a/src/util/lp/square_dense_submatrix.cpp b/src/util/lp/square_dense_submatrix.cpp
index 81d174c9de..c94c7a525e 100644
--- a/src/util/lp/square_dense_submatrix.cpp
+++ b/src/util/lp/square_dense_submatrix.cpp
@@ -4,7 +4,7 @@
 
   Author: Lev Nachmanson
 */
-
+#include <vector>
 #include "util/lp/square_dense_submatrix.h"
 namespace lean {
 template <typename T, typename X>
@@ -157,7 +157,7 @@ template <typename T, typename X>    void square_dense_submatrix<T, X>::push_new
         }
     }
 }
-template <typename T, typename X> 
+template <typename T, typename X>
 template <typename L>
 L square_dense_submatrix<T, X>::row_by_vector_product(unsigned i, const std::vector<L> & v) {
     lean_assert(i >= m_index_start);
@@ -170,7 +170,7 @@ L square_dense_submatrix<T, X>::row_by_vector_product(unsigned i, const std::vec
     return r;
 }
 
-template <typename T, typename X> 
+template <typename T, typename X>
 template <typename L>
 L square_dense_submatrix<T, X>::column_by_vector_product(unsigned j, const std::vector<L> & v) {
     lean_assert(j >= m_index_start);
@@ -181,7 +181,7 @@ L square_dense_submatrix<T, X>::column_by_vector_product(unsigned j, const std::
         r += m_v[offset] * v[adjust_row_inverse(m_index_start + i)];
     return r;
 }
-template <typename T, typename X> 
+template <typename T, typename X>
 template <typename L>
 L square_dense_submatrix<T, X>::row_by_indexed_vector_product(unsigned i, const indexed_vector<L> & v) {
     lean_assert(i >= m_index_start);
@@ -193,7 +193,7 @@ L square_dense_submatrix<T, X>::row_by_indexed_vector_product(unsigned i, const
         r += m_v[row_offset + j] * v[adjust_column_inverse(m_index_start + j)];
     return r;
 }
-template <typename T, typename X> 
+template <typename T, typename X>
 template <typename L>
 void square_dense_submatrix<T, X>::apply_from_left_local(indexed_vector<L> & w, lp_settings & settings) {
 #ifdef LEAN_DEBUG
diff --git a/src/util/lp/square_dense_submatrix.h b/src/util/lp/square_dense_submatrix.h
index 8ea8d81fda..8373044c1a 100644
--- a/src/util/lp/square_dense_submatrix.h
+++ b/src/util/lp/square_dense_submatrix.h
@@ -96,7 +96,7 @@ public:
     void update_existing_or_delete_in_parent_matrix_for_row(unsigned i, lp_settings & settings);
 
     void push_new_elements_to_parent_matrix(lp_settings & settings);
-    
+
     template <typename L>
     L row_by_vector_product(unsigned i, const std::vector<L> & v);
 
diff --git a/src/util/lp/square_dense_submatrix_instances.cpp b/src/util/lp/square_dense_submatrix_instances.cpp
index 6c942d3106..25cc4cdee8 100644
--- a/src/util/lp/square_dense_submatrix_instances.cpp
+++ b/src/util/lp/square_dense_submatrix_instances.cpp
@@ -4,6 +4,8 @@
 
   Author: Lev Nachmanson
 */
+#include <memory>
+#include <vector>
 #include "util/lp/square_dense_submatrix.cpp"
 template void lean::square_dense_submatrix<double, double>::init(lean::sparse_matrix<double, double>*, unsigned int);
 template lean::square_dense_submatrix<double, double>::square_dense_submatrix(lean::sparse_matrix<double, double>*, unsigned int);
diff --git a/src/util/lp/static_matrix.cpp b/src/util/lp/static_matrix.cpp
index 2ca7578eb5..226ee25661 100644
--- a/src/util/lp/static_matrix.cpp
+++ b/src/util/lp/static_matrix.cpp
@@ -4,7 +4,9 @@
 
   Author: Lev Nachmanson
 */
-
+#include <vector>
+#include <utility>
+#include <set>
 #include "util/lp/static_matrix.h"
 
 namespace lean {
@@ -19,7 +21,7 @@ void  static_matrix<T, X>::init_row_columns(unsigned m, unsigned n) {
         m_columns.push_back(column_strip());
     }
 }
-    
+
 // constructor that copies columns of the basis from A
 template <typename T, typename X>
 static_matrix<T, X>::static_matrix(static_matrix const &A, unsigned * basis) :
@@ -32,7 +34,7 @@ static_matrix<T, X>::static_matrix(static_matrix const &A, unsigned * basis) :
         }
     }
 }
-    
+
 template <typename T, typename X>    void static_matrix<T, X>::clear() {
     m_work_pivot_vector.clear();
     m_rows.clear();
@@ -45,12 +47,12 @@ template <typename T, typename X>    void static_matrix<T, X>::clear() {
 template <typename T, typename X>    void static_matrix<T, X>::init_work_pivot_vector(unsigned m) {
     while (m--) m_work_pivot_vector.push_back(numeric_traits<T>::zero());
 }
-    
+
 template <typename T, typename X>    void static_matrix<T, X>::init_empty_matrix(unsigned m, unsigned n) {
     init_work_pivot_vector(m);
     init_row_columns(m, n);
 }
-template <typename T, typename X>  
+template <typename T, typename X>
 template <typename L>
 L static_matrix<T, X>::dot_product_with_row(unsigned row, const std::vector<L> & w) {
     L ret = zero_of_type<L>();
@@ -127,7 +129,7 @@ void static_matrix<T, X>::divide_row_by_constant(unsigned row, T const & alpha)
         m_columns[t.m_j][t.m_offset].m_value /= alpha;
     }
 }
-    
+
 template <typename T, typename X>
 void static_matrix<T, X>::scale_column(unsigned column, T const & alpha) {
     for (auto & t : m_columns[column]) {
@@ -181,7 +183,7 @@ template <typename T, typename X>    void static_matrix<T, X>::copy_column_to_ve
             v.set_value(it.m_value, it.m_i);
     }
 }
-    
+
 template <typename T, typename X>    void static_matrix<T, X>::copy_column_to_vector (unsigned j, std::vector<T> & v) const {
     v.resize(row_count(), numeric_traits<T>::zero());
     for (auto & it : m_columns[j]) {
@@ -195,7 +197,7 @@ template <typename T, typename X>    void static_matrix<T, X>::add_column_to_vec
         v[it.m_i] += a * it.m_value;
     }
 }
-    
+
 template <typename T, typename X>    T static_matrix<T, X>::get_max_abs_in_row(unsigned row) const {
     T ret = numeric_traits<T>::zero();
     for (auto & t : m_rows[row]) {
@@ -206,7 +208,7 @@ template <typename T, typename X>    T static_matrix<T, X>::get_max_abs_in_row(u
     }
     return ret;
 }
-    
+
 template <typename T, typename X>    T static_matrix<T, X>::get_min_abs_in_row(unsigned row) const {
     bool first_time = true;
     T ret = numeric_traits<T>::zero();
@@ -248,7 +250,7 @@ template <typename T, typename X>     T static_matrix<T, X>::get_min_abs_in_colu
     }
     return ret;
 }
-    
+
 #ifdef LEAN_DEBUG
 template <typename T, typename X>    void static_matrix<T, X>::check_consistency() {
     std::unordered_map<std::pair<unsigned, unsigned>, T> by_rows;
@@ -312,7 +314,7 @@ template <typename T, typename X>    void static_matrix<T, X>::cross_out_row_fro
         cross_out_row_from_column(t.m_j, k);
     }
 }
-    
+
 template <typename T, typename X>    void static_matrix<T, X>::cross_out_row_from_column(unsigned col, unsigned k) {
     auto & s = m_columns[col];
     for (unsigned i = 0; i < s.size(); i++) {
@@ -338,13 +340,13 @@ template <typename T, typename X>    void static_matrix<T, X>::scan_row_to_work_
         m_work_pivot_vector[rc.m_j] = rc.get_val();
     }
 }
-    
+
 template <typename T, typename X>    void static_matrix<T, X>::clean_row_work_vector(unsigned i) {
     for (auto & rc : m_rows[i]) {
         m_work_pivot_vector[rc.m_j] = numeric_traits<T>::zero();
     }
 }
-    
+
 
 template <typename T, typename X>    T static_matrix<T, X>::get_balance() const {
     T ret = zero_of_type<T>();
diff --git a/src/util/lp/static_matrix.h b/src/util/lp/static_matrix.h
index 33f6121881..7a4850e079 100644
--- a/src/util/lp/static_matrix.h
+++ b/src/util/lp/static_matrix.h
@@ -147,9 +147,9 @@ public:
     std::set<pair<unsigned, unsigned>>  get_domain();
 
     void copy_column_to_vector (unsigned j, indexed_vector<T> & v) const;
-    
+
     void copy_column_to_vector (unsigned j, std::vector<T> & v) const;
-    
+
     void add_column_to_vector (const T & a, unsigned j, T * v) const;
     T get_max_abs_in_row(unsigned row) const;
 
@@ -172,7 +172,7 @@ public:
 
     void cross_out_row_from_column(unsigned col, unsigned k);
 
-    T get_elem(unsigned i, unsigned j) const; 
+    T get_elem(unsigned i, unsigned j) const;
 
 
     unsigned number_of_non_zeroes_in_column(unsigned j) const { return m_columns[j].size(); }
diff --git a/src/util/lp/static_matrix_instances.cpp b/src/util/lp/static_matrix_instances.cpp
index ef296e9e42..ba6d3030e8 100644
--- a/src/util/lp/static_matrix_instances.cpp
+++ b/src/util/lp/static_matrix_instances.cpp
@@ -4,7 +4,9 @@
 
   Author: Lev Nachmanson
 */
-
+#include <vector>
+#include <memory>
+#include <set>
 #include "util/lp/static_matrix.cpp"
 #include "util/lp/lp_core_solver_base.h"
 #include "util/lp/lp_dual_core_solver.h"
@@ -63,10 +65,10 @@ template void static_matrix<mpq, mpq>::set(unsigned int, unsigned int, mpq const
 template static_matrix<mpq, mpq>::static_matrix(unsigned int, unsigned int);
 #ifdef LEAN_DEBUG
 template bool static_matrix<mpq, numeric_pair<mpq> >::col_val_equal_to_row_val() const;
-#endif    
+#endif
 template void static_matrix<mpq, numeric_pair<mpq> >::copy_column_to_vector(unsigned int, indexed_vector<mpq>&) const;
 template mpq static_matrix<mpq, numeric_pair<mpq> >::dot_product_with_column(std::vector<mpq, std::allocator<mpq> > const&, unsigned int) const;
 template mpq static_matrix<mpq, numeric_pair<mpq> >::get_elem(unsigned int, unsigned int) const;
 template void static_matrix<mpq, numeric_pair<mpq> >::init_empty_matrix(unsigned int, unsigned int);
 template void static_matrix<mpq, numeric_pair<mpq> >::set(unsigned int, unsigned int, mpq const&);
- }
+}
diff --git a/src/util/lp/tail_matrix.h b/src/util/lp/tail_matrix.h
index 35214395b3..4809195613 100644
--- a/src/util/lp/tail_matrix.h
+++ b/src/util/lp/tail_matrix.h
@@ -6,6 +6,7 @@
 */
 
 #pragma once
+#include <vector>
 #include "util/lp/indexed_vector.h"
 #include "util/lp/matrix.h"
 // These matrices appear at the end of the list