diff --git a/src/math/lp/core_solver_pretty_printer_def.h b/src/math/lp/core_solver_pretty_printer_def.h
index 697106183..2f1d99d22 100644
--- a/src/math/lp/core_solver_pretty_printer_def.h
+++ b/src/math/lp/core_solver_pretty_printer_def.h
@@ -88,7 +88,6 @@ template <typename T, typename X> T core_solver_pretty_printer<T, X>::current_co
 }
 
 template <typename T, typename X> void core_solver_pretty_printer<T, X>::init_m_A_and_signs() { 
-    if (numeric_traits<T>::precise() ) {
         for (unsigned column = 0; column < ncols(); column++) {
             vector<T> t(nrows(), zero_of_type<T>());
             for (const auto & c : m_core_solver.m_A.m_columns[column]){
@@ -115,8 +114,7 @@ template <typename T, typename X> void core_solver_pretty_printer<T, X>::init_m_
                           name);
                 m_rs[row] += t[row] * m_core_solver.m_x[column];
             }
-        }
-    } 
+        }     
 }
 
 template <typename T, typename X> void core_solver_pretty_printer<T, X>::init_column_widths() {
diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index 9bc850848..9b2361b74 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -281,9 +281,9 @@ namespace lp {
         unsigned m = A_r().row_count();
         clean_popped_elements(m, m_rows_with_changed_bounds);
         clean_inf_set_of_r_solver_after_pop();
-        lp_assert(m_settings.simplex_strategy() == simplex_strategy_enum::undecided ||
-            ( m_mpq_lar_core_solver.m_r_solver.reduced_costs_are_correct_tableau()));
-
+        lp_assert(
+            m_settings.simplex_strategy() == simplex_strategy_enum::undecided ||
+            m_mpq_lar_core_solver.m_r_solver.reduced_costs_are_correct_tableau());
 
         m_constraints.pop(k);
         m_term_count.pop(k);
@@ -627,10 +627,6 @@ namespace lp {
         m_rows_with_changed_bounds.insert(rid);
     }
 
-    void lar_solver::detect_rows_of_bound_change_column_for_nbasic_column(unsigned j) {
-       lp_assert(false);
-    }
-
 
 
     void lar_solver::detect_rows_of_bound_change_column_for_nbasic_column_tableau(unsigned j) {
@@ -676,20 +672,16 @@ namespace lp {
     }
 
     void lar_solver::change_basic_columns_dependend_on_a_given_nb_column(unsigned j, const numeric_pair<mpq>& delta) {
-         {
-            for (const auto& c : A_r().m_columns[j]) {
-                unsigned bj = m_mpq_lar_core_solver.m_r_basis[c.var()];
-                if (tableau_with_costs()) {
-                    m_basic_columns_with_changed_cost.insert(bj);
-                }
-                m_mpq_lar_core_solver.m_r_solver.add_delta_to_x_and_track_feasibility(bj, -A_r().get_val(c) * delta);
-                TRACE("change_x_del",
-                    tout << "changed basis column " << bj << ", it is " <<
-                    (m_mpq_lar_core_solver.m_r_solver.column_is_feasible(bj) ? "feas" : "inf") << std::endl;);
-
-            }
+        for (const auto& c : A_r().m_columns[j]) {
+           unsigned bj = m_mpq_lar_core_solver.m_r_basis[c.var()];
+           if (tableau_with_costs()) {
+              m_basic_columns_with_changed_cost.insert(bj);
+           }
+           m_mpq_lar_core_solver.m_r_solver.add_delta_to_x_and_track_feasibility(bj, -A_r().get_val(c) * delta);
+           TRACE("change_x_del",
+              tout << "changed basis column " << bj << ", it is " <<
+              (m_mpq_lar_core_solver.m_r_solver.column_is_feasible(bj) ? "feas" : "inf") << std::endl;);
         }
-        
     }
 
     void lar_solver::update_x_and_inf_costs_for_column_with_changed_bounds(unsigned j) {
@@ -819,19 +811,6 @@ namespace lp {
         A.set(last_row, basis_j, mpq(1));
     }
 
-    template <typename U, typename V>
-    void lar_solver::create_matrix_A(static_matrix<U, V>& matr) {
-        lp_assert(false); // not implemented
-        /*
-          unsigned m = number_or_nontrivial_left_sides();
-          unsigned n = m_vec_of_canonic_left_sides.size();
-          if (matr.row_count() == m && matr.column_count() == n)
-          return;
-          matr.init_empty_matrix(m, n);
-          copy_from_mpq_matrix(matr);
-        */
-    }
-
     template <typename U, typename V>
     void lar_solver::copy_from_mpq_matrix(static_matrix<U, V>& matr) {
         matr.m_rows.resize(A_r().row_count());
diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h
index b925b5ef0..356c86c2f 100644
--- a/src/math/lp/lar_solver.h
+++ b/src/math/lp/lar_solver.h
@@ -205,10 +205,9 @@ class lar_solver : public column_namer {
     void set_lower_bound_witness(var_index j, constraint_index ci);
     void substitute_terms_in_linear_expression( const vector<std::pair<mpq, var_index>>& left_side_with_terms,
                                                 vector<std::pair<mpq, var_index>> &left_side) const;
-    void detect_rows_of_bound_change_column_for_nbasic_column(unsigned j);
+    
     void detect_rows_of_bound_change_column_for_nbasic_column_tableau(unsigned j);
     bool use_tableau_costs() const;
-    void detect_rows_of_column_with_bound_change(unsigned j);
     bool tableau_with_costs() const;
     bool costs_are_used() const;
     void change_basic_columns_dependend_on_a_given_nb_column(unsigned j, const numeric_pair<mpq> & delta);
diff --git a/src/math/lp/lp_core_solver_base.cpp b/src/math/lp/lp_core_solver_base.cpp
index b76976d37..059d801a0 100644
--- a/src/math/lp/lp_core_solver_base.cpp
+++ b/src/math/lp/lp_core_solver_base.cpp
@@ -43,7 +43,6 @@ template bool lp::lp_core_solver_base<double, double>::print_statistics_with_ite
 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>::solve_Ax_eq_b();
 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;
@@ -51,7 +50,6 @@ template void lp::lp_core_solver_base<lp::mpq, lp::mpq>::fill_reduced_costs_from
 template bool lp::lp_core_solver_base<lp::mpq, 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<lp::mpq, lp::mpq>::restore_x(unsigned int, lp::mpq const&);
 template void lp::lp_core_solver_base<lp::mpq, lp::mpq>::set_non_basic_x_to_correct_bounds();
-template void lp::lp_core_solver_base<lp::mpq, lp::mpq>::solve_Ax_eq_b();
 template void lp::lp_core_solver_base<lp::mpq, lp::mpq>::add_delta_to_entering(unsigned int, const lp::mpq&);
 template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::init();
 template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::init_basis_heading_and_non_basic_columns_vector();
@@ -61,7 +59,6 @@ template lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::lp_core_s
                                                                                                    const vector<lp::numeric_pair<lp::mpq> >&,
                                                                                                    const vector<lp::numeric_pair<lp::mpq> >&);
 template bool lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::print_statistics_with_cost_and_check_that_the_time_is_over(lp::numeric_pair<lp::mpq>, std::ostream&);
-template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::solve_Ax_eq_b();
 
 template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::add_delta_to_entering(unsigned int, const lp::numeric_pair<lp::mpq>&);
 template lp::lp_core_solver_base<lp::mpq, lp::mpq>::lp_core_solver_base(
diff --git a/src/math/lp/lp_core_solver_base.h b/src/math/lp/lp_core_solver_base.h
index cb275ebc9..6fa2ddead 100644
--- a/src/math/lp/lp_core_solver_base.h
+++ b/src/math/lp/lp_core_solver_base.h
@@ -238,11 +238,11 @@ public:
     }
     
     bool below_bound(const X & x, const X & bound) const {
-        return precise()? x < bound : below_bound_numeric<X>(x, bound, m_settings.primal_feasibility_tolerance);
+        return x < bound ;
     }
 
     bool above_bound(const X & x, const X & bound) const {
-        return precise()? x > bound : above_bound_numeric<X>(x, bound, m_settings.primal_feasibility_tolerance);
+        return x > bound ;
     }
 
     bool x_below_low_bound(unsigned p) const {
@@ -323,9 +323,6 @@ public:
 
     void find_error_in_BxB(vector<X>& rs);
 
-    // recalculates the projection of x to B, such that Ax = b, whereab is the right side
-    void solve_Ax_eq_b();
-
     bool snap_non_basic_x_to_bound() {
         bool ret = false;
         for (unsigned j : non_basis())
@@ -628,8 +625,6 @@ public:
     bool pivot_column_tableau(unsigned j, unsigned row_index);
     bool divide_row_by_pivot(unsigned pivot_row, unsigned pivot_col);
     
-    bool precise() const { return numeric_traits<T>::precise(); }
-
     simplex_strategy_enum simplex_strategy() const { return
             m_settings.simplex_strategy();
     }
diff --git a/src/math/lp/lp_core_solver_base_def.h b/src/math/lp/lp_core_solver_base_def.h
index 474d39b57..213d67e6e 100644
--- a/src/math/lp/lp_core_solver_base_def.h
+++ b/src/math/lp/lp_core_solver_base_def.h
@@ -233,18 +233,12 @@ column_is_dual_feasible(unsigned j) const {
 }
 template <typename T, typename X> bool lp_core_solver_base<T, X>::
 d_is_not_negative(unsigned j) const {
-    if (numeric_traits<T>::precise()) {
-        return m_d[j] >= numeric_traits<T>::zero();
-    }
-    return m_d[j] > -T(0.00001);
+    return m_d[j] >= numeric_traits<T>::zero();
 }
 
 template <typename T, typename X> bool lp_core_solver_base<T, X>::
 d_is_not_positive(unsigned j) const {
-    if (numeric_traits<T>::precise()) {
-        return m_d[j] <= numeric_traits<T>::zero();
-    }
-    return m_d[j] < T(0.00001);
+    return m_d[j] <= numeric_traits<T>::zero();    
 }
 
 
@@ -319,7 +313,6 @@ template <typename T, typename X> bool lp_core_solver_base<T, X>::inf_set_is_cor
 
 template <typename T, typename X> bool lp_core_solver_base<T, X>::
 divide_row_by_pivot(unsigned pivot_row, unsigned pivot_col) {
-    lp_assert(numeric_traits<T>::precise());
     int pivot_index = -1;
     auto & row = m_A.m_rows[pivot_row];
     unsigned size = row.size();
@@ -517,13 +510,6 @@ find_error_in_BxB(vector<X>& rs){
     }
 }
 
-// recalculates the projection of x to B, such that Ax = b
-template <typename T, typename X> void lp_core_solver_base<T, X>::
-solve_Ax_eq_b() {
-    lp_assert(false);
-}
-
-
 template <typename T, typename X> non_basic_column_value_position lp_core_solver_base<T, X>::
 get_non_basic_column_value_position(unsigned j) const {
     switch (m_column_types[j]) {
diff --git a/src/math/lp/lp_primal_core_solver.h b/src/math/lp/lp_primal_core_solver.h
index 219cc2ad3..aa771d7ee 100644
--- a/src/math/lp/lp_primal_core_solver.h
+++ b/src/math/lp/lp_primal_core_solver.h
@@ -511,7 +511,6 @@ public:
     bool limit_inf_on_bound_m_neg(const T & m, const X & x, const X & bound, X & theta, bool & unlimited) {
         // x gets smaller
         lp_assert(m < 0);
-        if (numeric_traits<T>::precise()) {
             if (this->below_bound(x, bound)) return false;
             if (this->above_bound(x, bound)) {
                 limit_theta((bound - x) / m, theta, unlimited);
@@ -519,59 +518,30 @@ public:
                 theta = zero_of_type<X>();
                 unlimited = false;
             }
-        } else {
-            const X& eps = harris_eps_for_bound(bound);
-            if (this->below_bound(x, bound)) return false;
-            if (this->above_bound(x, bound)) {
-                limit_theta((bound - x - eps) / m, theta, unlimited);
-            } else {
-                theta = zero_of_type<X>();
-                unlimited = false;
-            }
-        }
         return true;
     }
 
     bool limit_inf_on_bound_m_pos(const T & m, const X & x, const X & bound, X & theta, bool & unlimited) {
         // x gets larger
         lp_assert(m > 0);
-        if (numeric_traits<T>::precise()) {
-            if (this->above_bound(x, bound)) return false;
-            if (this->below_bound(x, bound)) {
-                limit_theta((bound - x) / m, theta, unlimited);
-            } else {
-                theta = zero_of_type<X>();
-                unlimited = false;
-            }
+        if (this->above_bound(x, bound)) return false;
+        if (this->below_bound(x, bound)) {
+            limit_theta((bound - x) / m, theta, unlimited);
         } else {
-            const X& eps = harris_eps_for_bound(bound);
-            if (this->above_bound(x, bound)) return false;
-            if (this->below_bound(x, bound)) {
-                limit_theta((bound - x + eps) / m, theta, unlimited);
-            } else {
-                theta = zero_of_type<X>();
-                unlimited = false;
-            }
+            theta = zero_of_type<X>();
+            unlimited = false;
         }
+        
         return true;
     }
 
     void limit_inf_on_lower_bound_m_pos(const T & m, const X & x, const X & bound, X & theta, bool & unlimited) {
-        if (numeric_traits<T>::precise()) {
             // x gets larger
-            lp_assert(m > 0);
-            if (this->below_bound(x, bound)) {
-                limit_theta((bound - x) / m, theta, unlimited);
-            }
-        }
-        else {
-            // x gets larger
-            lp_assert(m > 0);
-            const X& eps = harris_eps_for_bound(bound);
-            if (this->below_bound(x, bound)) {
-                limit_theta((bound - x + eps) / m, theta, unlimited);
-            }
-        }
+      lp_assert(m > 0);
+      if (this->below_bound(x, bound)) {
+           limit_theta((bound - x) / m, theta, unlimited);
+      }
+        
     }
 
     void limit_inf_on_upper_bound_m_neg(const T & m, const X & x, const X & bound, X & theta, bool & unlimited) {
@@ -877,46 +847,13 @@ public:
         m_epsilon_of_reduced_cost(T(1)/T(10000000)),
         m_bland_mode_threshold(1000) {
 
-        if (!(numeric_traits<T>::precise())) {
-            m_converted_harris_eps = convert_struct<T, double>::convert(this->m_settings.harris_feasibility_tolerance);
-        } else {
-            m_converted_harris_eps = zero_of_type<T>();
-        }
+       
+        m_converted_harris_eps = zero_of_type<T>();
+        
         this->set_status(lp_status::UNKNOWN);
     }
 
-    // constructor
-    lp_primal_core_solver(static_matrix<T, X> & A,
-                          vector<X> & b, // the right side vector
-                          vector<X> & x, // the number of elements in x needs to be at least as large as the number of columns in A
-                          vector<unsigned> & basis,
-                          vector<unsigned> & nbasis,
-                          vector<int> & heading,
-                          vector<T> & costs,
-                          const vector<column_type> & column_type_array,
-                          const vector<X> & upper_bound_values,
-                          lp_settings & settings,
-                          const column_namer& column_names):
-        lp_core_solver_base<T, X>(A, // b,
-                                  basis,
-                                  nbasis,
-                                  heading,
-                                  x,
-                                  costs,
-                                  settings,
-                                  column_names,
-                                  column_type_array,
-                                  m_lower_bounds_dummy,
-                                  upper_bound_values),
-        m_beta(A.row_count()),
-        m_converted_harris_eps(convert_struct<T, double>::convert(this->m_settings.harris_feasibility_tolerance)) {
-        lp_assert(initial_x_is_correct());
-        m_lower_bounds_dummy.resize(A.column_count(), zero_of_type<T>());
-        m_enter_price_eps = numeric_traits<T>::precise() ? numeric_traits<T>::zero() : T(1e-5);
-#ifdef Z3DEBUG
-        lp_assert(false);
-#endif
-    }
+    
 
     bool initial_x_is_correct() {
         std::set<unsigned> basis_set;
diff --git a/src/math/lp/lp_primal_core_solver_def.h b/src/math/lp/lp_primal_core_solver_def.h
index dac1c15fa..fb62bbf54 100644
--- a/src/math/lp/lp_primal_core_solver_def.h
+++ b/src/math/lp/lp_primal_core_solver_def.h
@@ -33,9 +33,7 @@ namespace lp {
 
 template <typename T, typename X>
 void lp_primal_core_solver<T, X>::sort_non_basis_rational() {
-    lp_assert(numeric_traits<T>::precise());
-    
-        std::sort(this->m_nbasis.begin(), this->m_nbasis.end(), [this](unsigned a, unsigned b) {
+     std::sort(this->m_nbasis.begin(), this->m_nbasis.end(), [this](unsigned a, unsigned b) {
                 unsigned ca = this->m_A.number_of_non_zeroes_in_column(a);
                 unsigned cb = this->m_A.number_of_non_zeroes_in_column(b);
                 if (ca == 0 && cb != 0) return false;
@@ -54,57 +52,15 @@ void lp_primal_core_solver<T, X>::sort_non_basis_rational() {
 
 template <typename T, typename X>
 void lp_primal_core_solver<T, X>::sort_non_basis() {
-    if (numeric_traits<T>::precise()) {
-        sort_non_basis_rational();
-        return;
-    }
-    
-    
-    m_non_basis_list.clear();
-    // reinit m_basis_heading
-    for (unsigned j = 0; j < this->m_nbasis.size(); j++) {
-        unsigned col = this->m_nbasis[j];
-        this->m_basis_heading[col] = - static_cast<int>(j) - 1;
-        m_non_basis_list.push_back(col);
-    }
+     sort_non_basis_rational();   
 }
 
 template <typename T, typename X>
 bool lp_primal_core_solver<T, X>::column_is_benefitial_for_entering_basis(unsigned j) const {
-    if (numeric_traits<T>::precise())
-        return column_is_benefitial_for_entering_basis_precise(j);
-    const T& dj = this->m_d[j];
-    switch (this->m_column_types[j]) {
-    case column_type::fixed:  break;
-    case column_type::free_column:
-        if (dj > m_epsilon_of_reduced_cost || dj < -m_epsilon_of_reduced_cost)
-            return true;
-        break;
-    case column_type::lower_bound:
-        if (dj > m_epsilon_of_reduced_cost) return true;;
-        break;
-    case column_type::upper_bound:
-        if (dj < -m_epsilon_of_reduced_cost) return true;
-        break;
-    case column_type::boxed:
-        if (dj > m_epsilon_of_reduced_cost) {
-            if (this->m_x[j] < this->m_upper_bounds[j] - this->bound_span(j)/2)
-                return true;
-            break;
-        } else if (dj < - m_epsilon_of_reduced_cost) {
-            if (this->m_x[j] > this->m_lower_bounds[j] + this->bound_span(j)/2)
-                return true;
-        }
-        break;
-    default:
-        lp_unreachable();
-        break;
-    }
-    return false;
+    return column_is_benefitial_for_entering_basis_precise(j);    
 }
 template <typename T, typename X>
 bool lp_primal_core_solver<T, X>::column_is_benefitial_for_entering_basis_precise(unsigned j) const {
-    lp_assert (numeric_traits<T>::precise());
     const T& dj = this->m_d[j];
     TRACE("lar_solver", tout << "dj=" << dj << "\n";); 
     switch (this->m_column_types[j]) {
@@ -144,7 +100,6 @@ bool lp_primal_core_solver<T, X>::column_is_benefitial_for_entering_basis_precis
 
 template <typename T, typename X>
 int lp_primal_core_solver<T, X>::choose_entering_column_presize(unsigned number_of_benefitial_columns_to_go_over) { // at this moment m_y = cB * B(-1)
-    lp_assert(numeric_traits<T>::precise());
     if (number_of_benefitial_columns_to_go_over == 0)
         return -1;
     if (this->m_basis_sort_counter == 0) {
@@ -231,8 +186,6 @@ find_leaving_on_harris_theta(X const & harris_theta, X & t) {
         }
         if (++k == steps) k = 0;
     } while (k != initial_k);
-    if (!this->precise())
-        restore_harris_eps();
     return leaving;
 }
 
@@ -479,47 +432,14 @@ void lp_primal_core_solver<T, X>::update_reduced_costs_from_pivot_row(unsigned e
 // return 0 if the reduced cost at entering is close enough to the refreshed
 // 1 if it is way off, and 2 if it is unprofitable
 template <typename T, typename X>    int lp_primal_core_solver<T, X>::refresh_reduced_cost_at_entering_and_check_that_it_is_off(unsigned entering) {
-    if (numeric_traits<T>::precise()) return 0;
-    T reduced_at_entering_was = this->m_d[entering];  // can benefit from going over non-zeros of m_ed
-    lp_assert(abs(reduced_at_entering_was) > m_epsilon_of_reduced_cost);
-    T refreshed_cost = this->m_costs[entering];
-    unsigned i = this->m_m();
-    while (i--) refreshed_cost -= this->m_costs[this->m_basis[i]] * this->m_ed[i];
-    this->m_d[entering] = refreshed_cost;
-    T delta = abs(reduced_at_entering_was - refreshed_cost);
-    if (delta * 2 > abs(reduced_at_entering_was)) {
-        // this->m_status = UNSTABLE;
-        if (reduced_at_entering_was > m_epsilon_of_reduced_cost) {
-            if (refreshed_cost <= zero_of_type<T>())
-                return 2; // abort entering
-        } else {
-            if (refreshed_cost > -m_epsilon_of_reduced_cost)
-                return 2; // abort entering
-        }
-        return 1; // go on with this entering
-    } else {
-        if (reduced_at_entering_was > m_epsilon_of_reduced_cost) {
-            if (refreshed_cost <= zero_of_type<T>())
-                return 2; // abort entering
-        } else {
-            if (refreshed_cost > -m_epsilon_of_reduced_cost)
-                return 2; // abort entering
-        }
-    }
     return 0;
+    
 }
 
 template <typename T, typename X>    void lp_primal_core_solver<T, X>::backup_and_normalize_costs() {
     if (this->m_look_for_feasible_solution_only)
         return; // no need to backup cost, since we are going to use only feasibility costs
-    if (numeric_traits<T>::precise() ) {        
-        m_costs_backup = this->m_costs;
-    } else {
-        T cost_max = std::max(max_abs_in_vector(this->m_costs), T(1));
-        lp_assert(m_costs_backup.size() == 0);
-        for (unsigned j = 0; j < this->m_costs.size(); j++)
-            m_costs_backup.push_back(this->m_costs[j] /= cost_max);
-    }
+    m_costs_backup = this->m_costs;    
 }
 
 template <typename T, typename X>    void lp_primal_core_solver<T, X>::init_run() {
@@ -527,10 +447,6 @@ template <typename T, typename X>    void lp_primal_core_solver<T, X>::init_run(
 }
 
 
-template <typename T, typename X>    void lp_primal_core_solver<T, X>::calc_working_vector_beta_for_column_norms(){
-    lp_assert(false);
-}
-
 template <typename T, typename X>
 void lp_primal_core_solver<T, X>::advance_on_entering_equal_leaving(int entering, X & t) {
     
@@ -571,63 +487,7 @@ template <typename T, typename X>  unsigned lp_primal_core_solver<T, X>::get_num
 // returns the number of iterations
 template <typename T, typename X> unsigned lp_primal_core_solver<T, X>::solve() {
     TRACE("lar_solver", tout << "solve " << this->get_status() << "\n";);
-    if (numeric_traits<T>::precise())
-        return solve_with_tableau();
-
-    init_run();
-    if (this->current_x_is_feasible() && this->m_look_for_feasible_solution_only) {
-        this->set_status(lp_status::FEASIBLE);
-        return 0;
-    }
-        
-   
-    do {
-        if (this->print_statistics_with_iterations_and_nonzeroes_and_cost_and_check_that_the_time_is_over((this->using_infeas_costs()? "inf" : "feas"), * this->m_settings.get_message_ostream())) {
-            return this->total_iterations();
-        }
-        one_iteration();
-
-        TRACE("lar_solver", tout << "one iteration: " << this->get_status() << "\n";);
-        lp_assert(!this->using_infeas_costs() || this->costs_on_nbasis_are_zeros());
-        switch (this->get_status()) {
-        case lp_status::OPTIMAL:  // double check that we are at optimum
-        case lp_status::INFEASIBLE:
-            if (this->m_look_for_feasible_solution_only && this->current_x_is_feasible())
-                break;
-            { // precise case
-                
-            }
-            break;
-        case lp_status::TENTATIVE_UNBOUNDED:
-            lp_assert(false);
-            break;
-        case lp_status::UNBOUNDED:
-            lp_assert(false);
-            break;
-
-        case lp_status::UNSTABLE:
-            lp_assert(false);
-            break;
-
-        default:
-            break; // do nothing
-        }
-    } while (
-             this->get_status() != lp_status::UNBOUNDED
-             &&
-             this->get_status() != lp_status::OPTIMAL
-             &&
-             this->get_status() != lp_status::INFEASIBLE
-             &&
-             this->iters_with_no_cost_growing() <= this->m_settings.max_number_of_iterations_with_no_improvements
-             &&
-             !(this->current_x_is_feasible() && this->m_look_for_feasible_solution_only));
-
-    lp_assert(
-                this->current_x_is_feasible() == false
-                ||
-                this->calc_current_x_is_feasible_include_non_basis());
-    return this->total_iterations();
+    return solve_with_tableau();
 }
 
 // calling it stage1 is too cryptic
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 a63a6be17..96df997b1 100644
--- a/src/math/lp/lp_primal_core_solver_tableau_def.h
+++ b/src/math/lp/lp_primal_core_solver_tableau_def.h
@@ -43,19 +43,10 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>::advance_on_e
     }
     advance_on_entering_and_leaving_tableau(entering, leaving, t);
 }
-/*
-template <typename T, typename X> int lp_primal_core_solver<T, X>::choose_entering_column_tableau_rows() {
-    int i = find_inf_row();
-    if (i == -1)
-        return -1;
-    return find_shortest_beneficial_column_in_row(i);
- }
-*/
  template <typename T, typename X> int lp_primal_core_solver<T, X>::choose_entering_column_tableau() {
     //this moment m_y = cB * B(-1)
     unsigned number_of_benefitial_columns_to_go_over =  get_number_of_non_basic_column_to_try_for_enter();
     
-    lp_assert(numeric_traits<T>::precise());
     if (number_of_benefitial_columns_to_go_over == 0)
         return -1;
     if (this->m_basis_sort_counter == 0) {
@@ -294,7 +285,7 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>::init_run_tab
             return;
         if (this->m_settings.backup_costs)
             backup_and_normalize_costs();
-        m_epsilon_of_reduced_cost = numeric_traits<X>::precise() ? zero_of_type<T>() : T(1) / T(10000000);
+        m_epsilon_of_reduced_cost = zero_of_type<T>();
         
         if (this->m_settings.simplex_strategy() == simplex_strategy_enum::tableau_rows)
             init_tableau_rows();
diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h
index 38270230e..86a97e615 100644
--- a/src/math/lp/lp_settings.h
+++ b/src/math/lp/lp_settings.h
@@ -78,9 +78,8 @@ enum class lp_status {
 // when the ratio of the vector length to domain size to is greater than the return value we switch to solve_By_for_T_indexed_only
 template <typename X>
 unsigned ratio_of_index_size_to_all_size() {
-    if (numeric_traits<X>::precise())
         return 10;
-    return 120;
+    
 }
 
 const char* lp_status_to_string(lp_status status);
@@ -274,7 +273,7 @@ public:
     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>::precise())? is_epsilon_small<T>(t, eps) : numeric_traits<T>::is_zero(t);
+        return numeric_traits<T>::is_zero(t);
     }
 
     template <typename T>
@@ -373,9 +372,7 @@ inline std::string T_to_string(const mpq & t) {
 
 template <typename T>
 bool val_is_smaller_than_eps(T const & t, double const & eps) {
-    if (!numeric_traits<T>::precise()) {
-        return numeric_traits<T>::get_double(t) < eps;
-    }
+    
     return t <= numeric_traits<T>::zero();
 }
 
diff --git a/src/math/lp/lp_settings_def.h b/src/math/lp/lp_settings_def.h
index bb87109f6..a439466d1 100644
--- a/src/math/lp/lp_settings_def.h
+++ b/src/math/lp/lp_settings_def.h
@@ -70,19 +70,12 @@ lp_status lp_status_from_string(std::string status) {
 
 template <typename T>
 bool vectors_are_equal(T * a, vector<T>  &b, unsigned n) {
-    if (numeric_traits<T>::precise()) {
         for (unsigned i = 0; i < n; i ++){
             if (!numeric_traits<T>::is_zero(a[i] - b[i])) {
                 return false;
             }
         }
-    } else {
-        for (unsigned i = 0; i < n; i ++){
-            if (std::abs(numeric_traits<T>::get_double(a[i] - b[i])) > 0.000001) {
-                return false;
-            }
-        }
-    }
+    
     return true;
 }
 
@@ -91,27 +84,12 @@ template <typename T>
 bool vectors_are_equal(const vector<T> & a, const vector<T>  &b) {
     unsigned n = static_cast<unsigned>(a.size());
     if (n != b.size()) return false;
-    if (numeric_traits<T>::precise()) {
         for (unsigned i = 0; i < n; i ++){
             if (!numeric_traits<T>::is_zero(a[i] - b[i])) {
                 return false;
             }
         }
-    } else {
-        for (unsigned i = 0; i < n; i ++){
-            double da = numeric_traits<T>::get_double(a[i]);
-            double db = numeric_traits<T>::get_double(b[i]);
-            double amax = std::max(fabs(da), fabs(db));
-            if (amax > 1) {
-                da /= amax;
-                db /= amax;
-            }
-                
-            if (fabs(da - db) > 0.000001) {
-                return false;
-            }
-        }
-    }
+    
     return true;
 }
 #ifdef Z3DEBUG
diff --git a/src/math/lp/lp_utils.h b/src/math/lp/lp_utils.h
index 40c5f0632..ad5ba380d 100644
--- a/src/math/lp/lp_utils.h
+++ b/src/math/lp/lp_utils.h
@@ -153,9 +153,6 @@ template <typename X> inline X ceil_ratio(const X & a, const X & b) { return num
 template <typename X> inline X floor_ratio(const X & a, const X & b) { return numeric_traits<X>::floor_ratio(a, b); }
 
 
-template <typename X> inline bool precise() { return numeric_traits<X>::precise(); }
-
-
 // returns true if a factor of b
 template <typename T>
 bool is_proper_factor(const T & a, const T & b) {
diff --git a/src/math/lp/matrix_def.h b/src/math/lp/matrix_def.h
index 95810bd5a..e3ac08f7e 100644
--- a/src/math/lp/matrix_def.h
+++ b/src/math/lp/matrix_def.h
@@ -32,16 +32,9 @@ bool matrix<T, X>::is_equal(const matrix<T, X>& other) {
         for (unsigned j = 0; j < column_count(); j++) {
             auto a = get_elem(i, j);
             auto b = other.get_elem(i, j);
-            if (numeric_traits<T>::precise()) {
-                if (a != b) return false;
-            } else if (fabs(numeric_traits<T>::get_double(a - b)) > 0.000001) {
-                // cout << "returning false from operator== of matrix comparison" << endl;
-                // cout << "this matrix is " << endl;
-                // print_matrix(*this);
-                // cout << "other matrix is " << endl;
-                // print_matrix(other);
-                return false;
-            }
+            
+            if (a != b) return false;
+            
         }
     }
     return true;
diff --git a/src/math/lp/numeric_pair.h b/src/math/lp/numeric_pair.h
index 9f7e27c18..f59aa84ba 100644
--- a/src/math/lp/numeric_pair.h
+++ b/src/math/lp/numeric_pair.h
@@ -45,7 +45,6 @@ template <typename T> class numeric_traits {};
 
 template <>  class numeric_traits<unsigned> {
 public:
-    static bool precise() { return true; }
     static unsigned zero() { return 0; }
     static unsigned one() { return 1; }
     static bool is_zero(unsigned v) { return v == 0; }
@@ -56,7 +55,6 @@ public:
 
 template <>  class numeric_traits<int> {
 public:
-    static bool precise() { return true; }
     static int zero() { return 0; }
     static int one() { return 1; }
     static bool is_zero(int v) { return v == 0; }
@@ -71,7 +69,6 @@ public:
 
 template <>  class numeric_traits<double> {
 public:
-    static bool precise() { return false; }
     static double g_zero;
     static double const &zero() { return g_zero;  }
     static double g_one;
@@ -88,7 +85,6 @@ public:
 template<>
 class numeric_traits<rational> {
 public:
-    static bool precise() { return true; }
     static rational const & zero() { return rational::zero(); }
     static rational const & one() { return rational::one(); }
     static bool is_zero(const rational & v) { return v.is_zero(); }
@@ -251,8 +247,6 @@ struct numeric_pair {
         return numeric_pair(-x, -y);
     }
 
-    static bool precize() { return lp::numeric_traits<T>::precize();}
-
     bool is_zero() const { return x.is_zero() && y.is_zero(); }
 
     bool is_pos() const { return x.is_pos() || (x.is_zero() && y.is_pos());}
@@ -294,12 +288,10 @@ numeric_pair<T> operator/(const numeric_pair<T> & r, const X & a) {
     return numeric_pair<T>(r.x / a,  r.y / a);
 }
 
-// template <numeric_pair, typename T>  bool precise() { return numeric_traits<T>::precise();}
 template <typename T> double get_double(const lp::numeric_pair<T> & ) { /* lp_unreachable(); */ return 0;}
 template <typename T>
 class numeric_traits<lp::numeric_pair<T>> {
 public:
-    static bool precise() { return numeric_traits<T>::precise();}
     static lp::numeric_pair<T> zero() { return lp::numeric_pair<T>(numeric_traits<T>::zero(), numeric_traits<T>::zero()); }
     static bool is_zero(const lp::numeric_pair<T> & v) { return numeric_traits<T>::is_zero(v.x) && numeric_traits<T>::is_zero(v.y); }
     static double get_double(const lp::numeric_pair<T> & v){ return numeric_traits<T>::get_double(v.x); } // just return the double of the first coordinate
diff --git a/src/math/lp/static_matrix.h b/src/math/lp/static_matrix.h
index a42926853..7f81cae79 100644
--- a/src/math/lp/static_matrix.h
+++ b/src/math/lp/static_matrix.h
@@ -344,7 +344,6 @@ public:
     void fill_last_row_with_pivoting(const term& row,
                                      unsigned bj, // the index of the basis column
                                      const vector<int> & basis_heading) {
-        lp_assert(numeric_traits<T>::precise());
         lp_assert(row_count() > 0);
         m_work_vector.resize(column_count());
         T a;