diff --git a/src/test/smt_reader.h b/src/test/smt_reader.h
index 714e734ad..41eb7472e 100644
--- a/src/test/smt_reader.h
+++ b/src/test/smt_reader.h
@@ -367,7 +367,7 @@ namespace lean {
             if (it!= m_name_to_var_index.end())
                 return it->second;
 
-            unsigned ret= m_name_to_var_index.size();
+            unsigned ret = static_cast<unsigned>(m_name_to_var_index.size());
             m_name_to_var_index[s] = ret;
             return ret;
         }
diff --git a/src/util/lp/conversion_helper.h b/src/util/lp/conversion_helper.h
index ea88a98bf..28b1a7838 100644
--- a/src/util/lp/conversion_helper.h
+++ b/src/util/lp/conversion_helper.h
@@ -1,6 +1,5 @@
 /*
   Copyright (c) 2013 Microsoft Corporation. All rights reserved.
-  Released under Apache 2.0 license as described in the file LICENSE.
 
   Author: Lev Nachmanson
 */
@@ -19,7 +18,7 @@ struct conversion_helper {
 
 template<>
 struct conversion_helper <double> {
-    static double conversion_helper <double>::get_upper_bound(const column_info<mpq> & ci) {
+    static double conversion_helper get_upper_bound(const column_info<mpq> & ci) {
         if (!ci.upper_bound_is_strict())
             return ci.get_upper_bound().get_double();
         double eps = 0.00001;
diff --git a/src/util/lp/init_lar_solver.h b/src/util/lp/init_lar_solver.h
index 3c74e622d..301516dee 100644
--- a/src/util/lp/init_lar_solver.h
+++ b/src/util/lp/init_lar_solver.h
@@ -29,7 +29,7 @@ var_index add_var(unsigned ext_j) {
 
 void register_new_ext_var_index(unsigned ext_v) {
     lean_assert(!contains(m_ext_vars_to_columns, ext_v));
-    unsigned j = m_ext_vars_to_columns.size();
+    unsigned j = static_cast<unsigned>(m_ext_vars_to_columns.size());
     m_ext_vars_to_columns[ext_v] = j;
     lean_assert(m_columns_to_ext_vars_or_term_indices.size() == j);
     m_columns_to_ext_vars_or_term_indices.push_back(ext_v);
@@ -104,7 +104,7 @@ var_index add_term(const vector<std::pair<mpq, var_index>> & coeffs,
     m_terms.push_back(new lar_term(coeffs, m_v));
     m_orig_terms.push_back(new lar_term(coeffs, m_v));
     unsigned adjusted_term_index = m_terms.size() - 1;
-	var_index ret = m_terms_start_index + adjusted_term_index;
+    var_index ret = m_terms_start_index + adjusted_term_index;
     if (use_tableau() && !coeffs.empty()) {
         add_row_for_term(m_orig_terms.back(), ret);
         if (m_settings.bound_propagation())
diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h
index b8609675a..173000fd1 100644
--- a/src/util/lp/lar_solver.h
+++ b/src/util/lp/lar_solver.h
@@ -37,7 +37,7 @@ class lar_solver : public column_namer {
     lp_settings m_settings;
     stacked_value<lp_status> m_status;
     stacked_value<simplex_strategy_enum> m_simplex_strategy;
-	std::unordered_map<unsigned, var_index> m_ext_vars_to_columns;
+    std::unordered_map<unsigned, var_index> m_ext_vars_to_columns;
     vector<unsigned> m_columns_to_ext_vars_or_term_indices;
     stacked_vector<ul_pair> m_vars_to_ul_pairs;
     vector<lar_base_constraint*> m_constraints;
@@ -45,7 +45,7 @@ class lar_solver : public column_namer {
     // the set of column indices j such that bounds have changed for j
     int_set m_columns_with_changed_bound;
     int_set m_rows_with_changed_bounds;
-	int_set m_basic_columns_with_changed_cost;
+    int_set m_basic_columns_with_changed_cost;
     stacked_value<int> m_infeasible_column_index; // such can be found at the initialization step
     stacked_value<unsigned> m_term_count;
     vector<lar_term*> m_terms;
@@ -55,12 +55,12 @@ class lar_solver : public column_namer {
     std::function<column_type (unsigned)> m_column_type_function;    
 public:
     lar_core_solver m_mpq_lar_core_solver;
-	unsigned constraint_count() const {
-		return m_constraints.size();
-	}
-	const lar_base_constraint& get_constraint(unsigned ci) const {
-		return *(m_constraints[ci]);
-	}
+    unsigned constraint_count() const {
+        return m_constraints.size();
+    }
+    const lar_base_constraint& get_constraint(unsigned ci) const {
+        return *(m_constraints[ci]);
+    }
 
     ////////////////// methods ////////////////////////////////
     static_matrix<mpq, numeric_pair<mpq>> & A_r() { return m_mpq_lar_core_solver.m_r_A;}
@@ -117,8 +117,8 @@ public:
     }
 
 
-	bool use_lu() const { return m_settings.simplex_strategy() == simplex_strategy_enum::lu; }
-
+    bool use_lu() const { return m_settings.simplex_strategy() == simplex_strategy_enum::lu; }
+    
     bool sizes_are_correct() const {
         lean_assert(strategy_is_undecided() || !m_mpq_lar_core_solver.need_to_presolve_with_double_solver() || A_r().column_count() == A_d().column_count());
         lean_assert(A_r().column_count() == m_mpq_lar_core_solver.m_r_solver.m_column_types.size());
@@ -348,10 +348,10 @@ public:
         //        new linear_combination_iterator_on_vector<mpq>(m_terms[adjust_term_index(term_index)]->coeffs_as_vector());
     }
 
-	unsigned adjust_column_index_to_term_index(unsigned j) const {
-		unsigned ext_var_or_term = m_columns_to_ext_vars_or_term_indices[j];
-		return ext_var_or_term < m_terms_start_index ? j : ext_var_or_term;
-	}
+    unsigned adjust_column_index_to_term_index(unsigned j) const {
+        unsigned ext_var_or_term = m_columns_to_ext_vars_or_term_indices[j];
+        return ext_var_or_term < m_terms_start_index ? j : ext_var_or_term;
+    }
     
     void propagate_bounds_on_a_term(const lar_term& t, bound_propagator & bp, unsigned term_offset) {
         lean_assert(false); // not implemented
diff --git a/src/util/lp/mps_reader.h b/src/util/lp/mps_reader.h
index 206220584..7a5c88f83 100644
--- a/src/util/lp/mps_reader.h
+++ b/src/util/lp/mps_reader.h
@@ -796,7 +796,7 @@ public:
         auto it = m_names_to_var_index.find(s);
         if (it != m_names_to_var_index.end())
             return it->second;
-        unsigned ret = m_names_to_var_index.size();
+        unsigned ret = static_cast<unsigned>(m_names_to_var_index.size());
         m_names_to_var_index[s] = ret;
         return ret;
     }