diff --git a/src/util/lp/indexed_vector.h b/src/util/lp/indexed_vector.h
index 080ec2e71..4de827e10 100644
--- a/src/util/lp/indexed_vector.h
+++ b/src/util/lp/indexed_vector.h
@@ -110,7 +110,7 @@ public:
         return m_data[i];
     }
 
-    void clp_up() {
+    void clean_up() {
 #if 0==1
         for (unsigned k = 0; k < m_index.size(); k++) {
             unsigned i = m_index[k];
@@ -164,7 +164,7 @@ public:
         }
     }
 
-    void restore_index_and_clp_from_data() {
+    void restore_index_and_clean_from_data() {
         m_index.resize(0);
         for (unsigned i = 0; i < m_data.size(); i++) {
             T & v = m_data[i];
diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp
index 3e7c994e6..93cd6a118 100644
--- a/src/util/lp/lar_solver.cpp
+++ b/src/util/lp/lar_solver.cpp
@@ -316,9 +316,6 @@ void lar_solver::fill_explanation_from_infeasible_column(vector<std::pair<mpq, c
 
     
 unsigned lar_solver::get_total_iterations() const { return m_mpq_lar_core_solver.m_r_solver.total_iterations(); }
-// see http://research.microsoft.com/projects/z3/smt07.pdf
-// This method searches for a feasible solution with as many different values of variables, reverenced in vars, as it can find
-// Attention, after a call to this method the non-basic variables don't necesserarly stick to their bounds anymore
 vector<unsigned> lar_solver::get_list_of_all_var_indices() const {
     vector<unsigned> ret;
     for (unsigned j = 0; j < m_mpq_lar_core_solver.m_r_heading.size(); j++)
@@ -338,7 +335,7 @@ void lar_solver::push() {
     m_constraint_count.push();
 }
 
-void lar_solver::clp_large_elements_after_pop(unsigned n, int_set& set) {
+void lar_solver::clean_large_elements_after_pop(unsigned n, int_set& set) {
     vector<int> to_remove;
     for (unsigned j: set.m_index)
         if (j >= n)
@@ -348,7 +345,7 @@ void lar_solver::clp_large_elements_after_pop(unsigned n, int_set& set) {
 }
 
 void lar_solver::shrink_inf_set_after_pop(unsigned n, int_set & set) {
-    clp_large_elements_after_pop(n, set);
+    clean_large_elements_after_pop(n, set);
     set.resize(n);
 }
 
@@ -367,10 +364,10 @@ void lar_solver::pop(unsigned k) {
     m_vars_to_ul_pairs.pop(k);
 
     m_mpq_lar_core_solver.pop(k);
-    clp_large_elements_after_pop(n, m_columns_with_changed_bound);
+    clean_large_elements_after_pop(n, m_columns_with_changed_bound);
     unsigned m = A_r().row_count();
-    clp_large_elements_after_pop(m, m_rows_with_changed_bounds);
-    clp_inf_set_of_r_solver_after_pop();
+    clean_large_elements_after_pop(m, m_rows_with_changed_bounds);
+    clean_inf_set_of_r_solver_after_pop();
     lp_assert(m_settings.simplex_strategy() == simplex_strategy_enum::undecided ||
                 (!use_tableau()) || m_mpq_lar_core_solver.m_r_solver.reduced_costs_are_correct_tableau());
         
@@ -1346,9 +1343,9 @@ void lar_solver::pop_tableau() {
     lp_assert(m_mpq_lar_core_solver.m_r_solver.basis_heading_is_correct());
 }
 
-void lar_solver::clp_inf_set_of_r_solver_after_pop() {
+void lar_solver::clean_inf_set_of_r_solver_after_pop() {
     vector<unsigned> became_feas;
-    clp_large_elements_after_pop(A_r().column_count(), m_mpq_lar_core_solver.m_r_solver.m_inf_set);
+    clean_large_elements_after_pop(A_r().column_count(), m_mpq_lar_core_solver.m_r_solver.m_inf_set);
     std::unordered_set<unsigned> basic_columns_with_changed_cost;
     auto inf_index_copy = m_mpq_lar_core_solver.m_r_solver.m_inf_set.m_index;
     for (auto j: inf_index_copy) {
diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h
index 7c689fc4d..ed8d03fc1 100644
--- a/src/util/lp/lar_solver.h
+++ b/src/util/lp/lar_solver.h
@@ -462,7 +462,7 @@ public:
     vector<unsigned> get_list_of_all_var_indices() const;
     void push();
 
-    static void clp_large_elements_after_pop(unsigned n, int_set& set);
+    static void clean_large_elements_after_pop(unsigned n, int_set& set);
 
     static void shrink_inf_set_after_pop(unsigned n, int_set & set);
 
@@ -1275,7 +1275,7 @@ public:
     void remove_last_column_from_basis_tableau(unsigned j);
     void remove_column_from_tableau(unsigned j);
     void pop_tableau();
-    void clp_inf_set_of_r_solver_after_pop();
+    void clean_inf_set_of_r_solver_after_pop();
     void shrink_explanation_to_minimum(vector<std::pair<mpq, constraint_index>> & explanation) const;
 
     bool column_represents_row_in_tableau(unsigned j) {
diff --git a/src/util/lp/lp_dual_simplex.hpp b/src/util/lp/lp_dual_simplex.hpp
index 92df8c92f..e334ded90 100644
--- a/src/util/lp/lp_dual_simplex.hpp
+++ b/src/util/lp/lp_dual_simplex.hpp
@@ -350,7 +350,7 @@ template <typename T, typename X> void lp_dual_simplex<T, X>::find_maximal_solut
 
     this->flip_costs(); // do it for now, todo ( remove the flipping)
 
-    this->clpup();
+    this->cleanup();
     if (this->m_status == INFEASIBLE) {
         return;
     }
diff --git a/src/util/lp/lp_primal_simplex.hpp b/src/util/lp/lp_primal_simplex.hpp
index c4d2fa377..63ccd469d 100644
--- a/src/util/lp/lp_primal_simplex.hpp
+++ b/src/util/lp/lp_primal_simplex.hpp
@@ -172,7 +172,7 @@ template <typename T, typename X> void lp_primal_simplex<T, X>::find_maximal_sol
         return;
     }
 
-    this->clpup();
+    this->cleanup();
     this->fill_matrix_A_and_init_right_side();
     if (this->m_status == lp_status::INFEASIBLE) {
         return;
diff --git a/src/util/lp/lp_solver.h b/src/util/lp/lp_solver.h
index be0d23bbe..c447b1870 100644
--- a/src/util/lp/lp_solver.h
+++ b/src/util/lp/lp_solver.h
@@ -220,7 +220,7 @@ protected:
 
     unsigned try_to_remove_some_rows();
 
-    void clpup();
+    void cleanup();
 
     void map_external_rows_to_core_solver_rows();
 
diff --git a/src/util/lp/lp_solver.hpp b/src/util/lp/lp_solver.hpp
index 75bef74e7..bfa69c5fc 100644
--- a/src/util/lp/lp_solver.hpp
+++ b/src/util/lp/lp_solver.hpp
@@ -396,7 +396,7 @@ template <typename T, typename X> unsigned lp_solver<T, X>::try_to_remove_some_r
     return static_cast<unsigned>(rows_to_delete.size());
 }
 
-template <typename T, typename X> void lp_solver<T, X>::clpup() {
+template <typename T, typename X> void lp_solver<T, X>::cleanup() {
     int n = 0; // number of deleted rows
     int d;
     while ((d = try_to_remove_some_rows() > 0))
diff --git a/src/util/lp/lp_solver_instances.cpp b/src/util/lp/lp_solver_instances.cpp
index 2db52ff54..4fe04c05f 100644
--- a/src/util/lp/lp_solver_instances.cpp
+++ b/src/util/lp/lp_solver_instances.cpp
@@ -20,7 +20,7 @@ Revision History:
 #include <string>
 #include "util/lp/lp_solver.hpp"
 template void lp::lp_solver<double, double>::add_constraint(lp::lp_relation, double, unsigned int);
-template void lp::lp_solver<double, double>::clpup();
+template void lp::lp_solver<double, double>::cleanup();
 template void lp::lp_solver<double, double>::count_slacks_and_artificials();
 template void lp::lp_solver<double, double>::fill_m_b();
 template void lp::lp_solver<double, double>::fill_matrix_A_and_init_right_side();
@@ -36,7 +36,7 @@ template void lp::lp_solver<double, double>::scale();
 template void lp::lp_solver<double, double>::set_scaled_cost(unsigned int);
 template lp::lp_solver<double, double>::~lp_solver();
 template void lp::lp_solver<lp::mpq, lp::mpq>::add_constraint(lp::lp_relation, lp::mpq, unsigned int);
-template void lp::lp_solver<lp::mpq, lp::mpq>::clpup();
+template void lp::lp_solver<lp::mpq, lp::mpq>::cleanup();
 template void lp::lp_solver<lp::mpq, lp::mpq>::count_slacks_and_artificials();
 template void lp::lp_solver<lp::mpq, lp::mpq>::fill_m_b();
 template void lp::lp_solver<lp::mpq, lp::mpq>::fill_matrix_A_and_init_right_side();
diff --git a/src/util/lp/lu.hpp b/src/util/lp/lu.hpp
index c20fb855d..e42d2e050 100644
--- a/src/util/lp/lu.hpp
+++ b/src/util/lp/lu.hpp
@@ -430,7 +430,7 @@ void lu<T, X>::solve_yB_with_error_check_indexed(indexed_vector<T> & y, const ve
             solve_yB_indexed(y);
         } else {
             solve_yB(y.m_data);
-            y.restore_index_and_clp_from_data();
+            y.restore_index_and_clean_from_data();
         }
         return;
     }
@@ -444,7 +444,7 @@ void lu<T, X>::solve_yB_with_error_check_indexed(indexed_vector<T> & y, const ve
             find_error_of_yB(m_y_copy.m_data, y.m_data, basis);
             solve_yB(m_y_copy.m_data);
             add_delta_to_solution(m_y_copy.m_data, y.m_data);
-            y.restore_index_and_clp_from_data();
+            y.restore_index_and_clean_from_data();
             m_y_copy.clear_all();
         } else {
             find_error_of_yB_indexed(y, heading, settings); // this works with m_y_copy
@@ -454,7 +454,7 @@ void lu<T, X>::solve_yB_with_error_check_indexed(indexed_vector<T> & y, const ve
         lp_assert(m_y_copy.is_OK());
     } else {
         solve_yB_with_error_check(y.m_data, basis);
-        y.restore_index_and_clp_from_data();
+        y.restore_index_and_clean_from_data();
     }
 }
 
@@ -909,7 +909,7 @@ void lu<T, X>::calculate_Lwave_Pwave_for_bump(unsigned replaced_column, unsigned
     if (replaced_column < lowest_row_of_the_bump) {
         diagonal_elem = m_row_eta_work_vector[lowest_row_of_the_bump];
         //          lp_assert(m_row_eta_work_vector.is_OK());
-        m_U.set_row_from_work_vector_and_clp_work_vector_not_adjusted(m_U.adjust_row(lowest_row_of_the_bump), m_row_eta_work_vector, m_settings);
+        m_U.set_row_from_work_vector_and_clean_work_vector_not_adjusted(m_U.adjust_row(lowest_row_of_the_bump), m_row_eta_work_vector, m_settings);
     } else {
         diagonal_elem = m_U(lowest_row_of_the_bump, lowest_row_of_the_bump); // todo - get it more efficiently
     }
diff --git a/src/util/lp/sparse_matrix.h b/src/util/lp/sparse_matrix.h
index ae332a537..3ca6d3fa8 100644
--- a/src/util/lp/sparse_matrix.h
+++ b/src/util/lp/sparse_matrix.h
@@ -205,13 +205,13 @@ public:
 
     // set the max val as well
     // returns false if the resulting row is all zeroes, and true otherwise
-    bool set_row_from_work_vector_and_clp_work_vector_not_adjusted(unsigned i0, indexed_vector<T> & work_vec,
+    bool set_row_from_work_vector_and_clean_work_vector_not_adjusted(unsigned i0, indexed_vector<T> & work_vec,
                                                                      lp_settings & settings);
 
 
     // set the max val as well
     // returns false if the resulting row is all zeroes, and true otherwise
-    bool set_row_from_work_vector_and_clp_work_vector(unsigned i0);
+    bool set_row_from_work_vector_and_clean_work_vector(unsigned i0);
 
     void remove_zero_elements_and_set_data_on_existing_elements(unsigned row);
 
diff --git a/src/util/lp/sparse_matrix.hpp b/src/util/lp/sparse_matrix.hpp
index f2c8f28a8..8892e5b14 100644
--- a/src/util/lp/sparse_matrix.hpp
+++ b/src/util/lp/sparse_matrix.hpp
@@ -311,7 +311,7 @@ bool sparse_matrix<T, X>::pivot_row_to_row(unsigned i, const T& alpha, unsigned
     }
     
     
-    // clp the work vector
+    // clean the work vector
     for (unsigned k = 0; k < prev_size_i0; k++) {
         m_work_pivot_vector[i0_row_vals[k].m_index] = -1;
     }
@@ -334,7 +334,7 @@ bool sparse_matrix<T, X>::pivot_row_to_row(unsigned i, const T& alpha, unsigned
 // set the max val as well
 // returns false if the resulting row is all zeroes, and true otherwise
 template <typename T, typename X>
-bool sparse_matrix<T, X>::set_row_from_work_vector_and_clp_work_vector_not_adjusted(unsigned i0, indexed_vector<T> & work_vec,
+bool sparse_matrix<T, X>::set_row_from_work_vector_and_clean_work_vector_not_adjusted(unsigned i0, indexed_vector<T> & work_vec,
                                                                                       lp_settings & settings) {
     remove_zero_elements_and_set_data_on_existing_elements_not_adjusted(i0, work_vec, settings);
     // all non-zero elements in m_work_pivot_vector are new
@@ -572,11 +572,11 @@ void sparse_matrix<T, X>::double_solve_U_y(indexed_vector<L>& y, const lp_settin
         active_rows.clear();
         solve_U_y_indexed_only(y_orig, settings, active_rows);
         add_delta_to_solution(y_orig, y);
-        y.clp_up();
+        y.clean_up();
     } else { // the dense version
         solve_U_y(y_orig.m_data);
         add_delta_to_solution(y_orig.m_data, y.m_data);
-        y.restore_index_and_clp_from_data();
+        y.restore_index_and_clean_from_data();
     }
     lp_assert(y.is_OK());
 }
diff --git a/src/util/lp/sparse_matrix_instances.cpp b/src/util/lp/sparse_matrix_instances.cpp
index b45c6faa8..a5b2fc90a 100644
--- a/src/util/lp/sparse_matrix_instances.cpp
+++ b/src/util/lp/sparse_matrix_instances.cpp
@@ -39,7 +39,7 @@ template void sparse_matrix<double, double>::remove_element(vector<indexed_value
 template void     sparse_matrix<double, double>::replace_column(unsigned int, indexed_vector<double>&, lp_settings&);
 template void     sparse_matrix<double, double>::set(unsigned int, unsigned int, double);
 template void     sparse_matrix<double, double>::set_max_in_row(vector<indexed_value<double> >&);
-template bool sparse_matrix<double, double>::set_row_from_work_vector_and_clp_work_vector_not_adjusted(unsigned int, indexed_vector<double>&, lp_settings&);
+template bool sparse_matrix<double, double>::set_row_from_work_vector_and_clean_work_vector_not_adjusted(unsigned int, indexed_vector<double>&, lp_settings&);
 template bool sparse_matrix<double, double>::shorten_active_matrix(unsigned int, eta_matrix<double, double>*);
 template void sparse_matrix<double, double>::solve_y_U(vector<double>&) const;
 template sparse_matrix<double, double>::sparse_matrix(static_matrix<double, double> const&, vector<unsigned int>&);
@@ -56,7 +56,7 @@ template void  sparse_matrix<mpq, mpq>::prepare_for_factorization();
 template void   sparse_matrix<mpq, mpq>::remove_element(vector<indexed_value<mpq>> &, indexed_value<mpq>&);
 template void     sparse_matrix<mpq, mpq>::replace_column(unsigned int, indexed_vector<mpq>&, lp_settings&);
 template void     sparse_matrix<mpq, mpq>::set_max_in_row(vector<indexed_value<mpq>>&);
-template bool sparse_matrix<mpq, mpq>::set_row_from_work_vector_and_clp_work_vector_not_adjusted(unsigned int, indexed_vector<mpq>&, lp_settings&);
+template bool sparse_matrix<mpq, mpq>::set_row_from_work_vector_and_clean_work_vector_not_adjusted(unsigned int, indexed_vector<mpq>&, lp_settings&);
 template bool sparse_matrix<mpq, mpq>::shorten_active_matrix(unsigned int, eta_matrix<mpq, mpq>*);
 template void     sparse_matrix<mpq, mpq>::solve_y_U(vector<mpq>&) const;
 template sparse_matrix<mpq, mpq>::sparse_matrix(static_matrix<mpq, mpq> const&, vector<unsigned int>&);
@@ -72,7 +72,7 @@ template void     sparse_matrix<mpq, numeric_pair<mpq>>::prepare_for_factorizati
 template void     sparse_matrix<mpq, numeric_pair<mpq>>::remove_element(vector<indexed_value<mpq>>&, indexed_value<mpq>&);
 template void     sparse_matrix<mpq, numeric_pair<mpq>>::replace_column(unsigned int, indexed_vector<mpq>&, lp_settings&);
 template void     sparse_matrix<mpq, numeric_pair<mpq>>::set_max_in_row(vector<indexed_value<mpq>>&);
-template bool sparse_matrix<mpq, numeric_pair<mpq>>::set_row_from_work_vector_and_clp_work_vector_not_adjusted(unsigned int, indexed_vector<mpq>&, lp_settings&);
+template bool sparse_matrix<mpq, numeric_pair<mpq>>::set_row_from_work_vector_and_clean_work_vector_not_adjusted(unsigned int, indexed_vector<mpq>&, lp_settings&);
 template bool     sparse_matrix<mpq, numeric_pair<mpq>>::shorten_active_matrix(unsigned int, eta_matrix<mpq, numeric_pair<mpq> >*);
 template void     sparse_matrix<mpq, numeric_pair<mpq>>::solve_y_U(vector<mpq>&) const;
 template sparse_matrix<mpq, numeric_pair<mpq>>::sparse_matrix(static_matrix<mpq, numeric_pair<mpq> > const&, vector<unsigned int>&);
diff --git a/src/util/lp/square_dense_submatrix.h b/src/util/lp/square_dense_submatrix.h
index 5227cc1b4..266610516 100644
--- a/src/util/lp/square_dense_submatrix.h
+++ b/src/util/lp/square_dense_submatrix.h
@@ -202,7 +202,7 @@ public:
                 }
             }
         }
-        m_work_vector.clp_up();
+        m_work_vector.clean_up();
         lp_assert(m_work_vector.is_OK());
         w = m_work_vector;
 #endif
diff --git a/src/util/lp/static_matrix.h b/src/util/lp/static_matrix.h
index 78c634641..6833352ba 100644
--- a/src/util/lp/static_matrix.h
+++ b/src/util/lp/static_matrix.h
@@ -208,7 +208,7 @@ public:
     
     void scan_row_to_work_vector(unsigned i);
 
-    void clp_row_work_vector(unsigned i);
+    void clean_row_work_vector(unsigned i);
 
 
 #ifdef Z3DEBUG
diff --git a/src/util/lp/static_matrix.hpp b/src/util/lp/static_matrix.hpp
index d885c067b..4e05c669c 100644
--- a/src/util/lp/static_matrix.hpp
+++ b/src/util/lp/static_matrix.hpp
@@ -76,7 +76,7 @@ template <typename T, typename X> bool static_matrix<T, X>::pivot_row_to_row_giv
         }
     }
     
-    // clp the work vector
+    // clean the work vector
     for (unsigned k = 0; k < prev_size_ii; k++) {
         m_vector_of_row_offsets[ii_row_vals[k].m_j] = -1;
     }