diff --git a/src/math/lp/binary_heap_priority_queue.cpp b/src/math/lp/binary_heap_priority_queue.cpp
index bbe735e58..ec6630b1d 100644
--- a/src/math/lp/binary_heap_priority_queue.cpp
+++ b/src/math/lp/binary_heap_priority_queue.cpp
@@ -23,15 +23,12 @@ namespace lp {
 template binary_heap_priority_queue<int>::binary_heap_priority_queue(unsigned int);
 template unsigned binary_heap_priority_queue<int>::dequeue();
 template void binary_heap_priority_queue<int>::enqueue(unsigned int, int const&);
-template void binary_heap_priority_queue<double>::enqueue(unsigned int, double const&);
 template void binary_heap_priority_queue<mpq>::enqueue(unsigned int, mpq const&);
 template void binary_heap_priority_queue<int>::remove(unsigned int);
 template unsigned binary_heap_priority_queue<numeric_pair<mpq> >::dequeue();
-template unsigned binary_heap_priority_queue<double>::dequeue();
 template unsigned binary_heap_priority_queue<mpq>::dequeue();
 template void binary_heap_priority_queue<numeric_pair<mpq> >::enqueue(unsigned int, numeric_pair<mpq> const&);
 template void binary_heap_priority_queue<numeric_pair<mpq> >::resize(unsigned int);
-template void lp::binary_heap_priority_queue<double>::resize(unsigned int);
 template binary_heap_priority_queue<unsigned int>::binary_heap_priority_queue(unsigned int);
 template void binary_heap_priority_queue<unsigned>::resize(unsigned int);
 template unsigned binary_heap_priority_queue<unsigned int>::dequeue();
diff --git a/src/math/lp/conversion_helper.h b/src/math/lp/conversion_helper.h
index feb999743..ba8b6a983 100644
--- a/src/math/lp/conversion_helper.h
+++ b/src/math/lp/conversion_helper.h
@@ -31,28 +31,5 @@ struct conversion_helper {
     }
 };
 
-template<>
-struct conversion_helper <double> {
-    static double 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;
-        if (!ci.lower_bound_is_set())
-            return ci.get_upper_bound().get_double() - eps;
-        eps = std::min((ci.get_upper_bound() - ci.get_lower_bound()).get_double() / 1000, eps);
-        return ci.get_upper_bound().get_double() - eps;
-    }
-
-    static double get_lower_bound(const column_info<mpq> & ci) {
-        if (!ci.lower_bound_is_strict())
-            return ci.get_lower_bound().get_double();
-        double eps = 0.00001;
-        if (!ci.upper_bound_is_set())
-            return ci.get_lower_bound().get_double() + eps;
-        eps = std::min((ci.get_upper_bound() - ci.get_lower_bound()).get_double() / 1000, eps);
-        return ci.get_lower_bound().get_double() + eps;
-    }
-
-};
 
 }
diff --git a/src/math/lp/core_solver_pretty_printer.cpp b/src/math/lp/core_solver_pretty_printer.cpp
index 74d2f6048..18bef8303 100644
--- a/src/math/lp/core_solver_pretty_printer.cpp
+++ b/src/math/lp/core_solver_pretty_printer.cpp
@@ -19,9 +19,6 @@ Revision History:
 --*/
 #include "math/lp/numeric_pair.h"
 #include "math/lp/core_solver_pretty_printer_def.h"
-template lp::core_solver_pretty_printer<double, double>::core_solver_pretty_printer(const lp::lp_core_solver_base<double, double> &, std::ostream & out);
-template void lp::core_solver_pretty_printer<double, double>::print();
-template lp::core_solver_pretty_printer<double, double>::~core_solver_pretty_printer();
 template lp::core_solver_pretty_printer<lp::mpq, lp::mpq>::core_solver_pretty_printer(const lp::lp_core_solver_base<lp::mpq, lp::mpq> &, std::ostream & out);
 template void lp::core_solver_pretty_printer<lp::mpq, lp::mpq>::print();
 template lp::core_solver_pretty_printer<lp::mpq, lp::mpq>::~core_solver_pretty_printer();
diff --git a/src/math/lp/dense_matrix.cpp b/src/math/lp/dense_matrix.cpp
index f12e688d3..25fc65a5d 100644
--- a/src/math/lp/dense_matrix.cpp
+++ b/src/math/lp/dense_matrix.cpp
@@ -21,11 +21,6 @@ Revision History:
 #include "math/lp/dense_matrix_def.h"
 #ifdef Z3DEBUG
 #include "util/vector.h"
-template lp::dense_matrix<double, double> lp::operator*<double, double>(lp::matrix<double, double>&, lp::matrix<double, double>&);
-template void lp::dense_matrix<double, double>::apply_from_left(vector<double> &);
-template lp::dense_matrix<double, double>::dense_matrix(lp::matrix<double, double> const*);
-template lp::dense_matrix<double, double>::dense_matrix(unsigned int, unsigned int);
-template lp::dense_matrix<double, double>& lp::dense_matrix<double, double>::operator=(lp::dense_matrix<double, double> const&);
 template lp::dense_matrix<lp::mpq, lp::mpq>::dense_matrix(unsigned int, unsigned int);
 template lp::dense_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::dense_matrix(lp::matrix<lp::mpq, lp::numeric_pair<lp::mpq> > const*);
 template void lp::dense_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::apply_from_left(vector<lp::mpq>&);
@@ -35,6 +30,5 @@ template lp::dense_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::dense_matrix(uns
 template lp::dense_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >& lp::dense_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::operator=(lp::dense_matrix<lp::mpq, lp::numeric_pair<lp::mpq> > const&);
 template lp::dense_matrix<lp::mpq, lp::numeric_pair<lp::mpq> > lp::operator*<lp::mpq, lp::numeric_pair<lp::mpq> >(lp::matrix<lp::mpq, lp::numeric_pair<lp::mpq> >&, lp::matrix<lp::mpq, lp::numeric_pair<lp::mpq> >&);
 template void lp::dense_matrix<lp::mpq, lp::numeric_pair< lp::mpq> >::apply_from_right( vector< lp::mpq> &);
-template void lp::dense_matrix<double,double>::apply_from_right(vector<double> &);
 template void lp::dense_matrix<lp::mpq, lp::mpq>::apply_from_left(vector<lp::mpq>&);
 #endif
diff --git a/src/math/lp/dense_matrix.h b/src/math/lp/dense_matrix.h
index 342fc7aeb..fcc85cdd1 100644
--- a/src/math/lp/dense_matrix.h
+++ b/src/math/lp/dense_matrix.h
@@ -90,11 +90,7 @@ public:
 
     void set_elem(unsigned i, unsigned j, const T& val) {  m_values[i * m_n + j] = val;  }
 
-    // This method pivots row i to row i0 by muliplying row i by
-    //   alpha and adding it to row i0.
-    void pivot_row_to_row(unsigned i, const T& alpha, unsigned i0,
-                          const double & pivot_epsilon);
-
+    // This method pivots
     void swap_columns(unsigned a, unsigned b);
 
     void swap_rows(unsigned a, unsigned b);
diff --git a/src/math/lp/dense_matrix_def.h b/src/math/lp/dense_matrix_def.h
index 8eb9ad5dd..e850a9acd 100644
--- a/src/math/lp/dense_matrix_def.h
+++ b/src/math/lp/dense_matrix_def.h
@@ -150,17 +150,6 @@ template <typename T, typename X> void dense_matrix<T, X>::apply_from_left_to_X(
     }
 }
 
-// This method pivots row i to row i0 by muliplying row i by
-//   alpha and adding it to row i0.
-template <typename T, typename X> void dense_matrix<T, X>::pivot_row_to_row(unsigned i, const T& alpha, unsigned i0,
-                                                                            const double & pivot_epsilon) {
-    for (unsigned j = 0; j < m_n; j++) {
-        m_values[i0 * m_n + j] += m_values[i * m_n + j] * alpha;
-        if (fabs(m_values[i0 + m_n + j]) < pivot_epsilon) {
-            m_values[i0 + m_n + j] = numeric_traits<T>::zero();;
-        }
-    }
-}
 
 template <typename T, typename X> void dense_matrix<T, X>::swap_columns(unsigned a, unsigned b) {
     for (unsigned i = 0; i < m_m; i++) {
diff --git a/src/math/lp/indexed_vector.cpp b/src/math/lp/indexed_vector.cpp
index d7cde2e1d..fe0892541 100644
--- a/src/math/lp/indexed_vector.cpp
+++ b/src/math/lp/indexed_vector.cpp
@@ -20,10 +20,6 @@ Revision History:
 #include "util/vector.h"
 #include "math/lp/indexed_vector_def.h"
 namespace lp {
-template void indexed_vector<double>::clear();
-template void indexed_vector<double>::clear_all();
-template void indexed_vector<double>::erase_from_index(unsigned int);
-template void indexed_vector<double>::set_value(const double&, unsigned int);
 template void indexed_vector<mpq>::clear();
 template void indexed_vector<unsigned>::clear();
 template void indexed_vector<mpq>::clear_all();
@@ -32,22 +28,8 @@ template void indexed_vector<mpq>::resize(unsigned int);
 template void indexed_vector<unsigned>::resize(unsigned int);
 template void indexed_vector<mpq>::set_value(const mpq&, unsigned int);
 template void indexed_vector<unsigned>::set_value(const unsigned&, unsigned int);
-#ifdef Z3DEBUG
-template bool indexed_vector<unsigned>::is_OK() const;
-template bool indexed_vector<double>::is_OK() const;
-template bool indexed_vector<mpq>::is_OK() const;
-template bool indexed_vector<lp::numeric_pair<mpq> >::is_OK() const;
-#endif
 template void lp::indexed_vector< lp::mpq>::print(std::basic_ostream<char,struct std::char_traits<char> > &);
-template void lp::indexed_vector<double>::print(std::basic_ostream<char,struct std::char_traits<char> > &);
 template void lp::indexed_vector<lp::numeric_pair<lp::mpq> >::print(std::ostream&);
 }
-// template void lp::print_vector<double, vectro>(vector<double> const&, std::ostream&);
-// template void lp::print_vector<unsigned int>(vector<unsigned int> const&, std::ostream&);
-// template void lp::print_vector<std::string>(vector<std::string> const&, std::ostream&);
-// template void lp::print_vector<lp::numeric_pair<lp::mpq> >(vector<lp::numeric_pair<lp::mpq>> const&, std::ostream&);
-template void lp::indexed_vector<double>::resize(unsigned int);
-// template void lp::print_vector< lp::mpq>(vector< lp::mpq> const &, std::basic_ostream<char, std::char_traits<char> > &);
-// template void lp::print_vector<std::pair<lp::mpq, unsigned int> >(vector<std::pair<lp::mpq, unsigned int>> const&, std::ostream&);
 template void lp::indexed_vector<lp::numeric_pair<lp::mpq> >::erase_from_index(unsigned int);
 
diff --git a/src/math/lp/indexed_vector.h b/src/math/lp/indexed_vector.h
index 017a25f6b..9f3119e9a 100644
--- a/src/math/lp/indexed_vector.h
+++ b/src/math/lp/indexed_vector.h
@@ -99,47 +99,9 @@ public:
         return m_data[i];
     }
 
-    void clean_up() {
-#if 0==1
-        for (unsigned k = 0; k < m_index.size(); k++) {
-            unsigned i = m_index[k];
-            T & v = m_data[i];
-            if (lp_settings::is_eps_small_general(v, 1e-14)) {
-                v = zero_of_type<T>();
-                m_index.erase(m_index.begin() + k--);
-            }
-        }
-#endif
-       vector<unsigned> index_copy;
-       for (unsigned i : m_index) {
-           T & v = m_data[i];
-           if (!lp_settings::is_eps_small_general(v, 1e-14)) {
-               index_copy.push_back(i);
-           } else if (!numeric_traits<T>::is_zero(v)) {
-               v = zero_of_type<T>();
-           }
-       }
-       m_index = index_copy;
-    }
-
     
     void erase_from_index(unsigned j);
-
-    void add_value_at_index_with_drop_tolerance(unsigned j, const T& val_to_add) {
-        T & v = m_data[j];
-        bool was_zero = is_zero(v);
-        v += val_to_add;
-        if (lp_settings::is_eps_small_general(v, 1e-14)) {
-            v = zero_of_type<T>();
-            if (!was_zero) {
-                erase_from_index(j);
-            }
-        } else {
-            if (was_zero)
-                m_index.push_back(j);
-        }
-    }
-
+    
     void add_value_at_index(unsigned j, const T& val_to_add) {
         T & v = m_data[j];
         bool was_zero = is_zero(v);
@@ -153,18 +115,6 @@ public:
         }
     }
 
-    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];
-            if (lp_settings::is_eps_small_general(v, 1e-14)) {
-                v = zero_of_type<T>();
-            } else {
-                m_index.push_back(i);
-            }
-        }
-    }
-
     struct ival {
         unsigned m_var;
         const T & m_coeff;
@@ -215,9 +165,6 @@ public:
     }
 
     
-#ifdef Z3DEBUG
-    bool is_OK() const;
-#endif
     void print(std::ostream & out);
 };
 }
diff --git a/src/math/lp/indexed_vector_def.h b/src/math/lp/indexed_vector_def.h
index 0e25ee271..1b904e14a 100644
--- a/src/math/lp/indexed_vector_def.h
+++ b/src/math/lp/indexed_vector_def.h
@@ -43,7 +43,7 @@ template <typename T>
 void indexed_vector<T>::resize(unsigned data_size) {
     clear();
     m_data.resize(data_size, numeric_traits<T>::zero());
-    lp_assert(is_OK());
+
 }
 
 template <typename T>
@@ -72,33 +72,6 @@ void indexed_vector<T>::erase_from_index(unsigned j) {
         m_index.erase(it);
 }
 
-#ifdef Z3DEBUG
-template <typename T>
-bool indexed_vector<T>::is_OK() const {
-    return true;
-    const double drop_eps = 1e-14;
-    for (unsigned i = 0; i < m_data.size(); i++) {
-        if (!is_zero(m_data[i]) && lp_settings::is_eps_small_general(m_data[i], drop_eps)) {
-            return false;
-        }
-        if (lp_settings::is_eps_small_general(m_data[i], drop_eps) != (std::find(m_index.begin(), m_index.end(), i) == m_index.end())) {
-            return false;
-        }
-    }
-
-    std::unordered_set<unsigned> s;
-    for (unsigned i : m_index) {
-        //no duplicates!!!
-        if (s.find(i) != s.end())
-            return false;
-        s.insert(i);
-        if (i >= m_data.size())
-            return false;
-    }
-
-    return true;
-}
-#endif
 template <typename T>
 void indexed_vector<T>::print(std::ostream & out) {
     out << "m_index " << std::endl;
diff --git a/src/math/lp/lar_core_solver.h b/src/math/lp/lar_core_solver.h
index d40572b9e..e024b199c 100644
--- a/src/math/lp/lar_core_solver.h
+++ b/src/math/lp/lar_core_solver.h
@@ -27,8 +27,7 @@ class lar_core_solver  {
     int m_infeasible_sum_sign; // todo: get rid of this field
     vector<numeric_pair<mpq>> m_right_sides_dummy;
     vector<mpq> m_costs_dummy;
-    vector<double> m_d_right_sides_dummy;
-    vector<double> m_d_costs_dummy;
+    
 public:
     stacked_value<simplex_strategy_enum> m_stacked_simplex_strategy;
     stacked_vector<column_type> m_column_types;
@@ -45,10 +44,6 @@ public:
     stacked_vector<unsigned> m_r_rows_nz;
     
     // d - solver fields, for doubles
-    vector<double> m_d_x; // the solution in doubles
-    vector<double> m_d_lower_bounds;
-    vector<double> m_d_upper_bounds;
-    static_matrix<double, double> m_d_A;
     stacked_vector<unsigned> m_d_pushed_basis;
     vector<unsigned> m_d_basis;
     vector<unsigned> m_d_nbasis;
@@ -146,7 +141,7 @@ public:
         m_r_lower_bounds.push();
         m_r_upper_bounds.push();
         
-        m_d_A.push();
+        
         
     }
 
@@ -185,10 +180,6 @@ public:
         m_r_solver.m_costs.resize(m_r_A.column_count());
         m_r_solver.m_d.resize(m_r_A.column_count());
         
-        m_d_A.pop(k);
-        // doubles
-        
-        m_d_x.resize(m_d_A.column_count());
         pop_basis(k);
         m_stacked_simplex_strategy.pop(k);
         settings().set_simplex_strategy(m_stacked_simplex_strategy);
@@ -279,15 +270,7 @@ public:
     }
     
    
-    void create_double_matrix(static_matrix<double, double> & A) {
-        for (unsigned i = 0; i < m_r_A.row_count(); i++) {
-            auto & row = m_r_A.m_rows[i];
-            for (row_cell<mpq> & c : row) {
-                A.add_new_element(i, c.var(), c.coeff().get_double());
-            }
-        }
-    }
-
+    
     void fill_basis_d(
                       vector<unsigned>& basis_d,
                       vector<int>& heading_d,
@@ -308,27 +291,6 @@ public:
         }
     }
 
-    void get_bounds_for_double_solver() {
-        unsigned n = m_n();
-        m_d_lower_bounds.resize(n);
-        m_d_upper_bounds.resize(n);
-        double delta = find_delta_for_strict_boxed_bounds().get_double();
-        if (delta > 0.000001)
-            delta = 0.000001;
-        for (unsigned j = 0; j < n; j++) {
-            if (lower_bound_is_set(j)) {
-                const auto & lb = m_r_solver.m_lower_bounds[j];
-                m_d_lower_bounds[j] = lb.x.get_double() + delta * lb.y.get_double();
-            }
-            if (upper_bound_is_set(j)) {
-                const auto & ub = m_r_solver.m_upper_bounds[j];
-                m_d_upper_bounds[j] = ub.x.get_double() + delta * ub.y.get_double();
-                lp_assert(!lower_bound_is_set(j) || (m_d_upper_bounds[j] >= m_d_lower_bounds[j]));
-            }
-        }
-    }
-
-    
     
     bool lower_bound_is_set(unsigned j) const {
         switch (m_column_types[j]) {
diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index 9b2361b74..67cf90bd0 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -8,10 +8,6 @@
 
 namespace lp {
 
-    static_matrix<double, double>& lar_solver::A_d() { return m_mpq_lar_core_solver.m_d_A; }
-
-    static_matrix<double, double > const& lar_solver::A_d() const { return m_mpq_lar_core_solver.m_d_A; }
-
     lp_settings& lar_solver::settings() { return m_settings; }
 
     lp_settings const& lar_solver::settings() const { return m_settings; }
@@ -574,7 +570,6 @@ namespace lp {
 
     void lar_solver::pop_core_solver_params(unsigned k) {
         A_r().pop(k);
-        A_d().pop(k);
     }
 
 
@@ -1544,27 +1539,7 @@ namespace lp {
         add_new_var_to_core_fields_for_mpq(false); // false for not adding a row
         
     }
-
-    void lar_solver::add_new_var_to_core_fields_for_doubles(bool register_in_basis) {
-        unsigned j = A_d().column_count();
-        A_d().add_column();
-        lp_assert(m_mpq_lar_core_solver.m_d_x.size() == j);
-        //        lp_assert(m_mpq_lar_core_solver.m_d_lower_bounds.size() == j && m_mpq_lar_core_solver.m_d_upper_bounds.size() == j);  // restore later
-        m_mpq_lar_core_solver.m_d_x.resize(j + 1);
-        m_mpq_lar_core_solver.m_d_lower_bounds.resize(j + 1);
-        m_mpq_lar_core_solver.m_d_upper_bounds.resize(j + 1);
-        lp_assert(m_mpq_lar_core_solver.m_d_heading.size() == j); // as A().column_count() on the entry to the method
-        if (register_in_basis) {
-            A_d().add_row();
-            m_mpq_lar_core_solver.m_d_heading.push_back(m_mpq_lar_core_solver.m_d_basis.size());
-            m_mpq_lar_core_solver.m_d_basis.push_back(j);
-        }
-        else {
-            m_mpq_lar_core_solver.m_d_heading.push_back(-static_cast<int>(m_mpq_lar_core_solver.m_d_nbasis.size()) - 1);
-            m_mpq_lar_core_solver.m_d_nbasis.push_back(j);
-        }
-    }
-
+    
     void lar_solver::add_new_var_to_core_fields_for_mpq(bool register_in_basis) {
         unsigned j = A_r().column_count();
         TRACE("add_var", tout << "j = " << j << std::endl;);
@@ -1927,34 +1902,7 @@ namespace lp {
         }
     }
 
-    void lar_solver::adjust_initial_state_for_lu() {
-        copy_from_mpq_matrix(A_d());
-        unsigned n = A_d().column_count();
-        m_mpq_lar_core_solver.m_d_x.resize(n);
-        m_mpq_lar_core_solver.m_d_lower_bounds.resize(n);
-        m_mpq_lar_core_solver.m_d_upper_bounds.resize(n);
-        m_mpq_lar_core_solver.m_d_heading = m_mpq_lar_core_solver.m_r_heading;
-        m_mpq_lar_core_solver.m_d_basis = m_mpq_lar_core_solver.m_r_basis;
-
-        /*
-          unsigned j = A_d().column_count();
-          A_d().add_column();
-          lp_assert(m_mpq_lar_core_solver.m_d_x.size() == j);
-          //        lp_assert(m_mpq_lar_core_solver.m_d_lower_bounds.size() == j && m_mpq_lar_core_solver.m_d_upper_bounds.size() == j);  // restore later
-          m_mpq_lar_core_solver.m_d_x.resize(j + 1 );
-          m_mpq_lar_core_solver.m_d_lower_bounds.resize(j + 1);
-          m_mpq_lar_core_solver.m_d_upper_bounds.resize(j + 1);
-          lp_assert(m_mpq_lar_core_solver.m_d_heading.size() == j); // as A().column_count() on the entry to the method
-          if (register_in_basis) {
-          A_d().add_row();
-          m_mpq_lar_core_solver.m_d_heading.push_back(m_mpq_lar_core_solver.m_d_basis.size());
-          m_mpq_lar_core_solver.m_d_basis.push_back(j);
-          }else {
-          m_mpq_lar_core_solver.m_d_heading.push_back(- static_cast<int>(m_mpq_lar_core_solver.m_d_nbasis.size()) - 1);
-          m_mpq_lar_core_solver.m_d_nbasis.push_back(j);
-          }*/
-    }
-
+    
     void lar_solver::adjust_initial_state_for_tableau_rows() {
         for (unsigned i = 0; i < m_terms.size(); i++) {
             if (m_var_register.external_is_used(tv::mask_term(i)))
@@ -1963,24 +1911,7 @@ namespace lp {
         }
     }
 
-    // this fills the last row of A_d and sets the basis column: -1 in the last column of the row
-    void lar_solver::fill_last_row_of_A_d(static_matrix<double, double>& A, const lar_term* ls) {
-        lp_assert(A.row_count() > 0);
-        lp_assert(A.column_count() > 0);
-        unsigned last_row = A.row_count() - 1;
-        lp_assert(A.m_rows[last_row].empty());
-
-        for (auto t : *ls) {
-            lp_assert(!is_zero(t.coeff()));
-            var_index j = t.column();
-            A.set(last_row, j, -t.coeff().get_double());
-        }
-
-        unsigned basis_j = A.column_count() - 1;
-        A.set(last_row, basis_j, -1);
-        lp_assert(A.is_correct());
-    }
-
+    
     void lar_solver::update_column_type_and_bound_with_ub(unsigned j, lp::lconstraint_kind kind, const mpq& right_side, unsigned constraint_index) {
         SASSERT(column_has_upper_bound(j));
         if (column_has_lower_bound(j)) {
diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h
index 356c86c2f..237b9de81 100644
--- a/src/math/lp/lar_solver.h
+++ b/src/math/lp/lar_solver.h
@@ -112,8 +112,6 @@ class lar_solver : public column_namer {
     // end of fields
 
     ////////////////// methods ////////////////////////////////
-    static_matrix<double, double> & A_d();
-    static_matrix<double, double > const & A_d() const;
     
     static bool valid_index(unsigned j) { return static_cast<int>(j) >= 0;}
     const lar_term & get_term(unsigned j) const;
@@ -162,9 +160,7 @@ class lar_solver : public column_namer {
     unsigned row_of_basic_column(unsigned) const;
     void decide_on_strategy_and_adjust_initial_state();
     void adjust_initial_state();
-    void adjust_initial_state_for_lu();
     void adjust_initial_state_for_tableau_rows();
-    void fill_last_row_of_A_d(static_matrix<double, double> & A, const lar_term* ls);
     bool sizes_are_correct() const;
     bool implied_bound_is_correctly_explained(implied_bound const & be, const vector<std::pair<mpq, unsigned>> & explanation) const;
     
diff --git a/src/math/lp/lp_core_solver_base.cpp b/src/math/lp/lp_core_solver_base.cpp
index 059d801a0..14c454d6f 100644
--- a/src/math/lp/lp_core_solver_base.cpp
+++ b/src/math/lp/lp_core_solver_base.cpp
@@ -23,27 +23,10 @@ Revision History:
 #include "util/vector.h"
 #include <functional>
 #include "math/lp/lp_core_solver_base_def.h"
-template bool lp::lp_core_solver_base<double, double>::basis_heading_is_correct() const;
-template bool lp::lp_core_solver_base<double, double>::column_is_dual_feasible(unsigned int) const;
-template void lp::lp_core_solver_base<double, double>::fill_reduced_costs_from_m_y_by_rows();
-template lp::non_basic_column_value_position lp::lp_core_solver_base<double, double>::get_non_basic_column_value_position(unsigned int) const;
 template lp::non_basic_column_value_position lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::get_non_basic_column_value_position(unsigned int) const;
 template lp::non_basic_column_value_position lp::lp_core_solver_base<lp::mpq, lp::mpq>::get_non_basic_column_value_position(unsigned int) const;
-template lp::lp_core_solver_base<double, double>::lp_core_solver_base(
-    lp::static_matrix<double, double>&, // vector<double>&, 
-    vector<unsigned>&,
-    vector<unsigned> &, vector<int> &,
-    vector<double >&, 
-    vector<double >&, 
-    lp::lp_settings&, const column_namer&, const vector<lp::column_type >&,
-    const vector<double >&,
-    const vector<double >&);
 
-template bool lp::lp_core_solver_base<double, double>::print_statistics_with_iterations_and_nonzeroes_and_cost_and_check_that_the_time_is_over(char const*, std::ostream &);
 template bool lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::print_statistics_with_iterations_and_nonzeroes_and_cost_and_check_that_the_time_is_over(char const*, std::ostream &);
-template void lp::lp_core_solver_base<double, double>::restore_x(unsigned int, double const&);
-template void lp::lp_core_solver_base<double, double>::set_non_basic_x_to_correct_bounds();
-template void lp::lp_core_solver_base<double, double>::add_delta_to_entering(unsigned int, const double&);
 template bool lp::lp_core_solver_base<lp::mpq, lp::mpq>::basis_heading_is_correct() const ;
 template bool lp::lp_core_solver_base<lp::mpq, lp::mpq>::column_is_dual_feasible(unsigned int) const;
 template void lp::lp_core_solver_base<lp::mpq, lp::mpq>::fill_reduced_costs_from_m_y_by_rows();
@@ -74,35 +57,25 @@ template lp::lp_core_solver_base<lp::mpq, lp::mpq>::lp_core_solver_base(
                                                                               const vector<lp::mpq>&,
                                                                               const vector<lp::mpq>&);
 template bool lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::print_statistics_with_iterations_and_check_that_the_time_is_over(std::ostream &);
-template std::string lp::lp_core_solver_base<double, double>::column_name(unsigned int) const;
-template void lp::lp_core_solver_base<double, double>::pretty_print(std::ostream & out);
 template std::string lp::lp_core_solver_base<lp::mpq, lp::mpq>::column_name(unsigned int) const;
 template void lp::lp_core_solver_base<lp::mpq, lp::mpq>::pretty_print(std::ostream & out);
 template std::string lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::column_name(unsigned int) const;
 template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::pretty_print(std::ostream & out);
-template int lp::lp_core_solver_base<double, double>::pivots_in_column_and_row_are_different(int, int) const;
-template int lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::pivots_in_column_and_row_are_different(int, int) const;
-template int lp::lp_core_solver_base<lp::mpq, lp::mpq>::pivots_in_column_and_row_are_different(int, int) const;
-template bool lp::lp_core_solver_base<double, double>::calc_current_x_is_feasible_include_non_basis(void)const;
 template bool lp::lp_core_solver_base<lp::mpq, lp::mpq>::calc_current_x_is_feasible_include_non_basis(void)const;
 template bool lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::calc_current_x_is_feasible_include_non_basis() const;
 template void  lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::pivot_fixed_vars_from_basis();
-template bool lp::lp_core_solver_base<double, double>::column_is_feasible(unsigned int) const;
 template bool lp::lp_core_solver_base<lp::mpq, lp::mpq>::column_is_feasible(unsigned int) const;
 // template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::print_linear_combination_of_column_indices(vector<std::pair<lp::mpq, unsigned int>, std::allocator<std::pair<lp::mpq, unsigned int> > > const&, std::ostream&) const;
 template bool lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::column_is_feasible(unsigned int) const;
 template bool lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::snap_non_basic_x_to_bound();
 template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::restore_x(unsigned int, lp::numeric_pair<lp::mpq> const&);
 template bool lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq>>::pivot_column_tableau(unsigned int, unsigned int);
-template bool lp::lp_core_solver_base<double, double>::pivot_column_tableau(unsigned int, unsigned int);
 template bool lp::lp_core_solver_base<lp::mpq, lp::mpq>::pivot_column_tableau(unsigned int, unsigned int);
 template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::transpose_rows_tableau(unsigned int, unsigned int);
 template bool lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::inf_set_is_correct() const;
-template bool lp::lp_core_solver_base<double, double>::inf_set_is_correct() const;
 template bool lp::lp_core_solver_base<lp::mpq, lp::mpq>::inf_set_is_correct() const;
 template bool lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::infeasibility_costs_are_correct() const;
 template bool lp::lp_core_solver_base<lp::mpq, lp::mpq >::infeasibility_costs_are_correct() const;
-template bool lp::lp_core_solver_base<double, double >::infeasibility_costs_are_correct() const;
 template bool lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::remove_from_basis(unsigned int);
 template bool lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::remove_from_basis(unsigned int, lp::numeric_pair<lp::mpq> const&);
 
diff --git a/src/math/lp/lp_core_solver_base.h b/src/math/lp/lp_core_solver_base.h
index 6fa2ddead..14cb60ebf 100644
--- a/src/math/lp/lp_core_solver_base.h
+++ b/src/math/lp/lp_core_solver_base.h
@@ -309,10 +309,7 @@ public:
 
     column_type get_column_type(unsigned j) const {return m_column_types[j]; }
 
-    bool pivot_row_element_is_too_small_for_ratio_test(unsigned j) {
-        return m_settings.abs_val_is_smaller_than_pivot_tolerance(m_pivot_row[j]);
-    }
-
+    
     X bound_span(unsigned j) const {
         return m_upper_bounds[j] - m_lower_bounds[j];
     }
@@ -410,7 +407,6 @@ public:
     
     non_basic_column_value_position get_non_basic_column_value_position(unsigned j) const;
 
-    int pivots_in_column_and_row_are_different(int entering, int leaving) const;
     void pivot_fixed_vars_from_basis();
     bool remove_from_basis(unsigned j);
     bool remove_from_basis(unsigned j, const impq&);
diff --git a/src/math/lp/lp_core_solver_base_def.h b/src/math/lp/lp_core_solver_base_def.h
index 213d67e6e..16f56bade 100644
--- a/src/math/lp/lp_core_solver_base_def.h
+++ b/src/math/lp/lp_core_solver_base_def.h
@@ -533,23 +533,6 @@ get_non_basic_column_value_position(unsigned j) const {
     return at_lower_bound;
 }
 
-template <typename T, typename X> int lp_core_solver_base<T, X>::pivots_in_column_and_row_are_different(int entering, int leaving) const {
-    const T & column_p = this->m_ed[this->m_basis_heading[leaving]];
-    const T & row_p = this->m_pivot_row[entering];
-    if (is_zero(column_p) || is_zero(row_p)) return true; // pivots cannot be zero
-    // the pivots have to have the same sign
-    if (column_p < 0) {
-        if (row_p > 0)
-            return 2;
-    } else { // column_p > 0
-        if (row_p < 0)
-            return 2;
-    }
-    T diff_normalized = abs((column_p - row_p) / (numeric_traits<T>::one() + abs(row_p)));
-    if ( !this->m_settings.abs_val_is_smaller_than_harris_tolerance(diff_normalized / T(10)))
-        return 1;
-    return 0;
-}
 template <typename T, typename X>  void lp_core_solver_base<T, X>::transpose_rows_tableau(unsigned i, unsigned j) {
     transpose_basis(i, j);
     m_A.transpose_rows(i, j);
diff --git a/src/math/lp/lp_primal_core_solver.cpp b/src/math/lp/lp_primal_core_solver.cpp
index f4597da76..22042668d 100644
--- a/src/math/lp/lp_primal_core_solver.cpp
+++ b/src/math/lp/lp_primal_core_solver.cpp
@@ -27,15 +27,11 @@ Revision History:
 #include "math/lp/lp_primal_core_solver_tableau_def.h"
 namespace lp {
 
-template void lp_primal_core_solver<double, double>::find_feasible_solution();
 template void lp::lp_primal_core_solver<lp::mpq, lp::numeric_pair<lp::mpq> >::find_feasible_solution();
 
-template unsigned lp_primal_core_solver<double, double>::solve();
-template unsigned lp_primal_core_solver<double, double>::solve_with_tableau();
 template unsigned lp_primal_core_solver<mpq, mpq>::solve();
 template unsigned lp_primal_core_solver<mpq, numeric_pair<mpq> >::solve();
 template bool lp::lp_primal_core_solver<lp::mpq, lp::mpq>::update_basis_and_x_tableau(int, int, lp::mpq const&);
-template bool lp::lp_primal_core_solver<double, double>::update_basis_and_x_tableau(int, int, double const&);
 template bool lp::lp_primal_core_solver<lp::mpq, lp::numeric_pair<lp::mpq> >::update_basis_and_x_tableau(int, int, lp::numeric_pair<lp::mpq> const&);
 template void lp::lp_primal_core_solver<rational, lp::numeric_pair<rational> >::update_inf_cost_for_column_tableau(unsigned);
 
diff --git a/src/math/lp/lp_primal_core_solver.h b/src/math/lp/lp_primal_core_solver.h
index aa771d7ee..aacabf944 100644
--- a/src/math/lp/lp_primal_core_solver.h
+++ b/src/math/lp/lp_primal_core_solver.h
@@ -56,7 +56,7 @@ public:
     unsigned          m_bland_mode_threshold;
     unsigned          m_left_basis_repeated;
     vector<unsigned>  m_leaving_candidates;
-    //    T m_converted_harris_eps = convert_struct<T, double>::convert(this->m_settings.harris_feasibility_tolerance);
+    
     std::list<unsigned> m_non_basis_list;
     void sort_non_basis();
     void sort_non_basis_rational();
@@ -279,12 +279,10 @@ public:
 
     bool get_harris_theta(X & theta);
 
-    void restore_harris_eps() { m_converted_harris_eps = convert_struct<T, double>::convert(this->m_settings.harris_feasibility_tolerance); }
     void zero_harris_eps() { m_converted_harris_eps = zero_of_type<T>(); }
     int find_leaving_on_harris_theta(X const & harris_theta, X & t);
     bool try_jump_to_another_bound_on_entering(unsigned entering, const X & theta, X & t, bool & unlimited);
     bool try_jump_to_another_bound_on_entering_unlimited(unsigned entering, X & t);
-    int find_leaving_and_t(unsigned entering, X & t);
     int find_leaving_and_t_precise(unsigned entering, X & t);
     int find_leaving_and_t_tableau(unsigned entering, X & t);
  
diff --git a/src/math/lp/lp_primal_core_solver_def.h b/src/math/lp/lp_primal_core_solver_def.h
index fb62bbf54..cfd8fc947 100644
--- a/src/math/lp/lp_primal_core_solver_def.h
+++ b/src/math/lp/lp_primal_core_solver_def.h
@@ -144,7 +144,6 @@ int lp_primal_core_solver<T, X>::choose_entering_column(unsigned number_of_benef
 
 
 template <typename T, typename X> bool lp_primal_core_solver<T, X>::get_harris_theta(X & theta) {
-    lp_assert(this->m_ed.is_OK());
     bool unlimited = true;
     for (unsigned i : this->m_ed.m_index) {
         if (this->m_settings.abs_val_is_smaller_than_pivot_tolerance(this->m_ed[i])) continue;
@@ -311,17 +310,6 @@ template <typename T, typename X> int lp_primal_core_solver<T, X>::find_leaving_
 }
 
 
-template <typename T, typename X>    int lp_primal_core_solver<T, X>::find_leaving_and_t(unsigned entering, X & t) {
-    X theta = zero_of_type<X>();
-    bool unlimited = get_harris_theta(theta);
-    lp_assert(unlimited || theta >= zero_of_type<X>());
-    if (try_jump_to_another_bound_on_entering(entering, theta, t, unlimited)) return entering;
-    if (unlimited)
-        return -1;
-    return find_leaving_on_harris_theta(theta, t);
-}
-
-
 
 // m is the multiplier. updating t in a way that holds the following
 // x[j] + t * m >= m_lower_bounds[j] ( if m < 0 )
diff --git a/src/math/lp/lp_primal_core_solver_tableau_def.h b/src/math/lp/lp_primal_core_solver_tableau_def.h
index 96df997b1..256853be7 100644
--- a/src/math/lp/lp_primal_core_solver_tableau_def.h
+++ b/src/math/lp/lp_primal_core_solver_tableau_def.h
@@ -107,7 +107,7 @@ unsigned lp_primal_core_solver<T, X>::solve_with_tableau() {
         }
         TRACE("lar_solver", tout << "one iteration tableau " << this->get_status() << "\n";);
         switch (this->get_status()) {
-        case lp_status::OPTIMAL:  // double check that we are at optimum
+        case lp_status::OPTIMAL:  // check again that we are at optimum
         case lp_status::INFEASIBLE:
             if (this->m_look_for_feasible_solution_only && this->current_x_is_feasible())
                 break;
diff --git a/src/math/lp/lp_settings.cpp b/src/math/lp/lp_settings.cpp
index 592a98983..b72b837fd 100644
--- a/src/math/lp/lp_settings.cpp
+++ b/src/math/lp/lp_settings.cpp
@@ -21,7 +21,6 @@ Revision History:
 #include "util/vector.h"
 #include "smt/params/smt_params_helper.hpp"
 #include "math/lp/lp_settings_def.h"
-template bool lp::vectors_are_equal<double>(vector<double> const&, vector<double> const&);
 template bool lp::vectors_are_equal<lp::mpq>(vector<lp::mpq > const&, vector<lp::mpq> const&);
 
 void lp::lp_settings::updt_params(params_ref const& _p) {
diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h
index 86a97e615..197b7c04f 100644
--- a/src/math/lp/lp_settings.h
+++ b/src/math/lp/lp_settings.h
@@ -92,7 +92,6 @@ lp_status lp_status_from_string(std::string status);
 
 enum non_basic_column_value_position { at_lower_bound, at_upper_bound, at_fixed, free_of_bounds, not_at_bound };
 
-template <typename X> bool is_epsilon_small(const X & v, const double& eps);    // forward definition
 
 class lp_resource_limit {
 public:
@@ -182,36 +181,18 @@ public:
     unsigned      reps_in_scaler { 20 };
     // when the absolute value of an element is less than pivot_epsilon
     // in pivoting, we treat it as a zero
-    double        pivot_epsilon { 0.00000001 };
-    // see Chatal, page 115
-    double        positive_price_epsilon { 1e-7 };
     // a quotation "if some choice of the entering variable leads to an eta matrix
     // whose diagonal element in the eta column is less than e2 (entering_diag_epsilon) in magnitude, the this choice is rejected ...
-    double        entering_diag_epsilon { 1e-8 };
     int           c_partial_pivoting { 10 }; // this is the constant c from page 410
     unsigned      depth_of_rook_search { 4 };
     bool          using_partial_pivoting { true };
     // dissertation of Achim Koberstein
     // if Bx - b is different at any component more that refactor_epsilon then we refactor
-    double       refactor_tolerance { 1e-4 };
-    double       pivot_tolerance { 1e-6 };
-    double       zero_tolerance { 1e-12 };
-    double       drop_tolerance { 1e-14 };
-    double       tolerance_for_artificials { 1e-4 };
-    double       can_be_taken_to_basis_tolerance { 0.00001 };
-
+    
     unsigned     percent_of_entering_to_check { 5 }; // we try to find a profitable column in a percentage of the columns
     bool         use_scaling { true };
-    double       scaling_maximum { 1.0 };
-    double       scaling_minimum { 0.5 };
-    double       harris_feasibility_tolerance { 1e-7 };         // page 179 of Istvan Maros
-    double       ignore_epsilon_of_harris { 10e-5 };
     unsigned     max_number_of_iterations_with_no_improvements { 2000000 };
-    double       time_limit; // the maximum time limit of the total run time in seconds
-    // dual section
-    double       dual_feasibility_tolerance { 1e-7 };            // page 71 of the PhD thesis of Achim Koberstein
-    double       primal_feasibility_tolerance { 1e-7 };          // page 71 of the PhD thesis of Achim Koberstein
-    double       relative_primal_feasibility_tolerance { 1e-9 }; // page 71 of the PhD thesis of Achim Koberstein
+ double       time_limit; // the maximum time limit of the total run time in seconds
     // end of dual section
     bool                   m_bound_propagation { true };
     bool                   presolve_with_double_solver_for_lar { true };
@@ -221,7 +202,6 @@ public:
     bool             print_statistics { false };
     unsigned         column_norms_update_frequency { 12000 };
     bool             scale_with_ratio { true };
-    double           density_threshold { 0.7 };
     unsigned         max_row_length_for_bound_propagation { 300 };
     bool             backup_costs { true };
     unsigned         column_number_threshold_for_using_lu_in_lar_solver { 4000 };
@@ -272,61 +252,10 @@ public:
     statistics& stats() { return m_stats; }
     statistics const& stats() const { return m_stats; }
 
-    template <typename T> static bool is_eps_small_general(const T & t, const double & eps) {
-        return numeric_traits<T>::is_zero(t);
-    }
+    
 
-    template <typename T>
-    bool abs_val_is_smaller_than_dual_feasibility_tolerance(T const & t) {
-        return is_eps_small_general<T>(t, dual_feasibility_tolerance);
-    }
-
-    template <typename T>
-    bool abs_val_is_smaller_than_primal_feasibility_tolerance(T const & t) {
-        return is_eps_small_general<T>(t, primal_feasibility_tolerance);
-    }
-
-    template <typename T>
-    bool abs_val_is_smaller_than_can_be_taken_to_basis_tolerance(T const & t) {
-        return is_eps_small_general<T>(t, can_be_taken_to_basis_tolerance);
-    }
-
-    template <typename T>
-    bool abs_val_is_smaller_than_drop_tolerance(T const & t) const {
-        return is_eps_small_general<T>(t, drop_tolerance);
-    }
-
-
-    template <typename T>
-    bool abs_val_is_smaller_than_zero_tolerance(T const & t) {
-        return is_eps_small_general<T>(t, zero_tolerance);
-    }
-
-    template <typename T>
-    bool abs_val_is_smaller_than_refactor_tolerance(T const & t) {
-        return is_eps_small_general<T>(t, refactor_tolerance);
-    }
-
-
-    template <typename T>
-    bool abs_val_is_smaller_than_pivot_tolerance(T const & t) {
-        return is_eps_small_general<T>(t, pivot_tolerance);
-    }
-
-    template <typename T>
-    bool abs_val_is_smaller_than_harris_tolerance(T const & t) {
-        return is_eps_small_general<T>(t, harris_feasibility_tolerance);
-    }
-
-    template <typename T>
-    bool abs_val_is_smaller_than_ignore_epslilon_for_harris(T const & t) {
-        return is_eps_small_general<T>(t, ignore_epsilon_of_harris);
-    }
-
-    template <typename T>
-    bool abs_val_is_smaller_than_artificial_tolerance(T const & t) {
-        return is_eps_small_general<T>(t, tolerance_for_artificials);
-    }
+    
+    
     // the method of lar solver to use
     simplex_strategy_enum simplex_strategy() const {
         return m_simplex_strategy;
@@ -370,11 +299,6 @@ inline std::string T_to_string(const mpq & t) {
     return strs.str();
 }
 
-template <typename T>
-bool val_is_smaller_than_eps(T const & t, double const & eps) {
-    
-    return t <= numeric_traits<T>::zero();
-}
 
 template <typename T>
 bool vectors_are_equal(T * a, vector<T>  &b, unsigned n);
diff --git a/src/math/lp/lp_utils.cpp b/src/math/lp/lp_utils.cpp
index 9ce3b9894..b909a0389 100644
--- a/src/math/lp/lp_utils.cpp
+++ b/src/math/lp/lp_utils.cpp
@@ -20,8 +20,7 @@ Revision History:
 #include "math/lp/lp_utils.h"
 #ifdef lp_for_z3
 namespace lp {
-double numeric_traits<double>::g_zero = 0.0;
-double numeric_traits<double>::g_one = 1.0;
+
 }
 #endif
 
diff --git a/src/math/lp/matrix.cpp b/src/math/lp/matrix.cpp
index 5367c74d0..1ea2da263 100644
--- a/src/math/lp/matrix.cpp
+++ b/src/math/lp/matrix.cpp
@@ -22,10 +22,8 @@ Revision History:
 #include "math/lp/static_matrix.h"
 #include <string>
 #ifdef Z3DEBUG
-template bool lp::matrix<double, double>::is_equal(lp::matrix<double, double> const&);
 template bool lp::matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::is_equal(lp::matrix<lp::mpq, lp::numeric_pair<lp::mpq> > const&);
 template bool lp::matrix<lp::mpq, lp::mpq>::is_equal(lp::matrix<lp::mpq, lp::mpq> const&);
 #endif
-template void lp::print_matrix<double, double>(lp::matrix<double, double> const*, std::ostream & out);
 template void lp::print_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >(lp::matrix<lp::mpq, lp::numeric_pair<lp::mpq> > const *, std::basic_ostream<char, std::char_traits<char> > &);
 template void lp::print_matrix<lp::mpq, lp::mpq>(lp::matrix<lp::mpq, lp::mpq> const*, std::ostream&);
diff --git a/src/math/lp/permutation_matrix.cpp b/src/math/lp/permutation_matrix.cpp
index 28319c2ee..762b85d63 100644
--- a/src/math/lp/permutation_matrix.cpp
+++ b/src/math/lp/permutation_matrix.cpp
@@ -21,16 +21,8 @@ Revision History:
 #include "util/vector.h"
 #include "math/lp/permutation_matrix_def.h"
 #include "math/lp/numeric_pair.h"
-template void lp::permutation_matrix<double, double>::apply_from_right(vector<double>&);
-template void lp::permutation_matrix<double, double>::init(unsigned int);
 template void lp::permutation_matrix<lp::mpq, lp::mpq>::init(unsigned int);
 template void lp::permutation_matrix<lp::mpq, lp::numeric_pair<lp::mpq>>::init(unsigned int);
-template bool lp::permutation_matrix<double, double>::is_identity() const;
-template void lp::permutation_matrix<double, double>::multiply_by_permutation_from_left(lp::permutation_matrix<double, double>&);
-template void lp::permutation_matrix<double, double>::multiply_by_permutation_reverse_from_left(lp::permutation_matrix<double, double>&);
-template void lp::permutation_matrix<double, double>::multiply_by_reverse_from_right(lp::permutation_matrix<double, double>&);
-template lp::permutation_matrix<double, double>::permutation_matrix(unsigned int, vector<unsigned int> const&);
-template void lp::permutation_matrix<double, double>::transpose_from_left(unsigned int, unsigned int);
 
 template void lp::permutation_matrix<lp::mpq, lp::mpq>::apply_from_right(vector<lp::mpq>&);
 template bool lp::permutation_matrix<lp::mpq, lp::mpq>::is_identity() const;
@@ -50,21 +42,13 @@ template void lp::permutation_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::multi
 template lp::permutation_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::permutation_matrix(unsigned int);
 template void lp::permutation_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::transpose_from_left(unsigned int, unsigned int);
 template void lp::permutation_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::transpose_from_right(unsigned int, unsigned int);
-template void lp::permutation_matrix<double, double>::apply_reverse_from_left<double>(lp::indexed_vector<double>&);
-template void lp::permutation_matrix<double, double>::apply_reverse_from_left_to_T(vector<double>&);
-template void lp::permutation_matrix<double, double>::apply_reverse_from_right_to_T(vector<double>&);
-template void lp::permutation_matrix<double, double>::transpose_from_right(unsigned int, unsigned int);
 template void lp::permutation_matrix<lp::mpq, lp::mpq>::apply_reverse_from_left<lp::mpq>(lp::indexed_vector<lp::mpq>&);
 template void lp::permutation_matrix<lp::mpq, lp::mpq>::apply_reverse_from_left_to_T(vector<lp::mpq>&);
 template void lp::permutation_matrix<lp::mpq, lp::mpq>::apply_reverse_from_right_to_T(vector<lp::mpq>&);
 template void lp::permutation_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::apply_reverse_from_left<lp::mpq>(lp::indexed_vector<lp::mpq>&);
 template void lp::permutation_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::apply_reverse_from_left_to_T(vector<lp::mpq>&);
 template void lp::permutation_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::apply_reverse_from_right_to_T(vector<lp::mpq >&);
-template void lp::permutation_matrix<double, double>::multiply_by_permutation_from_right(lp::permutation_matrix<double, double>&);
-template lp::permutation_matrix<double, double>::permutation_matrix(unsigned int);
-template void lp::permutation_matrix<double, double>::apply_reverse_from_left_to_X(vector<double> &);
 template void  lp::permutation_matrix< lp::mpq, lp::mpq>::apply_reverse_from_left_to_X(vector<lp::mpq> &);
 template void lp::permutation_matrix< lp::mpq, lp::numeric_pair< lp::mpq> >::apply_reverse_from_left_to_X(vector<lp::numeric_pair< lp::mpq>> &);
-template void lp::permutation_matrix<double, double>::apply_reverse_from_right_to_T(lp::indexed_vector<double>&);
 template void lp::permutation_matrix<lp::mpq, lp::mpq>::apply_reverse_from_right_to_T(lp::indexed_vector<lp::mpq>&);
 template void lp::permutation_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::apply_reverse_from_right_to_T(lp::indexed_vector<lp::mpq>&);
diff --git a/src/math/lp/permutation_matrix_def.h b/src/math/lp/permutation_matrix_def.h
index 703830ffc..b6f9924ff 100644
--- a/src/math/lp/permutation_matrix_def.h
+++ b/src/math/lp/permutation_matrix_def.h
@@ -133,7 +133,7 @@ template <typename T, typename X> void permutation_matrix<T, X>::apply_from_righ
         unsigned pj = m_permutation[j];
         w.set_value(buffer[i], pj);
     }
-    lp_assert(w.is_OK());
+    
 #ifdef Z3DEBUG
     lp_assert(vectors_are_equal(wcopy, w.m_data));
 #endif
@@ -235,7 +235,6 @@ void permutation_matrix<T, X>::apply_reverse_from_right_to_T(indexed_vector<T> &
     // vector<T> wcopy(w.m_data);
     // apply_reverse_from_right_to_T(wcopy);
 #endif
-    lp_assert(w.is_OK());
     vector<T> tmp;
     vector<unsigned> tmp_index(w.m_index);
     for (auto i : w.m_index) {
@@ -248,8 +247,7 @@ void permutation_matrix<T, X>::apply_reverse_from_right_to_T(indexed_vector<T> &
         w.set_value(tmp[k], m_rev[j]);
     }
 
-    // lp_assert(w.is_OK());    
-    // lp_assert(vectors_are_equal(w.m_data, wcopy));
+    
 }
 
 
diff --git a/src/math/lp/sparse_vector.h b/src/math/lp/sparse_vector.h
index 1c27a8d96..3de701e10 100644
--- a/src/math/lp/sparse_vector.h
+++ b/src/math/lp/sparse_vector.h
@@ -42,7 +42,6 @@ public:
     }
 #endif
     void divide(T const & a) {
-        lp_assert(!lp_settings::is_eps_small_general(a, 1e-12));
         for (auto & t : m_data) {  t.second /= a; }
     }
 
diff --git a/src/math/lp/static_matrix.cpp b/src/math/lp/static_matrix.cpp
index 12d2f9f0d..28a23b0c3 100644
--- a/src/math/lp/static_matrix.cpp
+++ b/src/math/lp/static_matrix.cpp
@@ -26,26 +26,8 @@ Revision History:
 #include "math/lp/lp_primal_core_solver.h"
 #include "math/lp/lar_solver.h"
 namespace lp {
-template void static_matrix<double, double>::add_columns_at_the_end(unsigned int);
-template void static_matrix<double, double>::clear();
-#ifdef Z3DEBUG
-template bool static_matrix<double, double>::is_correct() const;
-#endif
-template void static_matrix<double, double>::copy_column_to_indexed_vector(unsigned int, indexed_vector<double>&) const;
-
-template double static_matrix<double, double>::get_balance() const;
-template std::set<std::pair<unsigned, unsigned>> static_matrix<double, double>::get_domain();
 template std::set<std::pair<unsigned, unsigned>> lp::static_matrix<lp::mpq, lp::mpq>::get_domain();
 template std::set<std::pair<unsigned, unsigned>> lp::static_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::get_domain();
-template double static_matrix<double, double>::get_elem(unsigned int, unsigned int) const;
-template double static_matrix<double, double>::get_max_abs_in_column(unsigned int) const;
-template double static_matrix<double, double>::get_min_abs_in_column(unsigned int) const;
-template double static_matrix<double, double>::get_min_abs_in_row(unsigned int) const;
-template void static_matrix<double, double>::init_empty_matrix(unsigned int, unsigned int);
-template void static_matrix<double, double>::init_row_columns(unsigned int, unsigned int);
-template static_matrix<double, double>::ref & static_matrix<double, double>::ref::operator=(double const&);
-template void static_matrix<double, double>::set(unsigned int, unsigned int, double const&);
-template static_matrix<double, double>::static_matrix(unsigned int, unsigned int);
 template void static_matrix<mpq, mpq>::add_column_to_vector(mpq const&, unsigned int, mpq*) const;
 template void static_matrix<mpq, mpq>::add_columns_at_the_end(unsigned int);
 template bool static_matrix<mpq, mpq>::is_correct() const;
@@ -55,7 +37,6 @@ template mpq static_matrix<mpq, mpq>::get_balance() const;
 template mpq static_matrix<mpq, mpq>::get_elem(unsigned int, unsigned int) const;
 template mpq static_matrix<mpq, mpq>::get_max_abs_in_column(unsigned int) const;
 template mpq static_matrix<mpq, mpq>::get_max_abs_in_row(unsigned int) const;
-template double static_matrix<double, double>::get_max_abs_in_row(unsigned int) const;
 template mpq static_matrix<mpq, mpq>::get_min_abs_in_column(unsigned int) const;
 template mpq static_matrix<mpq, mpq>::get_min_abs_in_row(unsigned int) const;
 template void static_matrix<mpq, mpq>::init_row_columns(unsigned int, unsigned int);
@@ -72,7 +53,6 @@ template void static_matrix<mpq, numeric_pair<mpq> >::init_empty_matrix(unsigned
 template void static_matrix<mpq, numeric_pair<mpq> >::set(unsigned int, unsigned int, mpq const&);
 
 
-template bool lp::static_matrix<double, double>::pivot_row_to_row_given_cell(unsigned int, column_cell &, unsigned int);
 template bool lp::static_matrix<lp::mpq, lp::mpq>::pivot_row_to_row_given_cell(unsigned int, column_cell& , unsigned int);
 template bool lp::static_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::pivot_row_to_row_given_cell(unsigned int, column_cell&, unsigned int);
 template void lp::static_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::remove_element(vector<lp::row_cell<lp::mpq>, true, unsigned int>&, lp::row_cell<lp::mpq>&);
diff --git a/src/math/lp/static_matrix.h b/src/math/lp/static_matrix.h
index 7f81cae79..b9870ceb5 100644
--- a/src/math/lp/static_matrix.h
+++ b/src/math/lp/static_matrix.h
@@ -359,7 +359,6 @@ public:
         for (auto p : row) {
             fill_last_row_with_pivoting_loop_block(p.column().index(), basis_heading);
         }
-        lp_assert(m_work_vector.is_OK());
         unsigned last_row = row_count() - 1;
     
         for (unsigned j : m_work_vector.m_index) {