diff --git a/src/util/lp/lar_core_solver.cpp b/src/util/lp/lar_core_solver.cpp
index 820f0dec3..1a79de6ed 100644
--- a/src/util/lp/lar_core_solver.cpp
+++ b/src/util/lp/lar_core_solver.cpp
@@ -20,14 +20,12 @@ lar_core_solver<T, X>::lar_core_solver(std::vector<X> & x, std::vector<column_ty
                                        std::vector<unsigned> & basis,
                                        static_matrix<T, X> & A,
                                        lp_settings & settings,
-                                       std::unordered_map<unsigned, std::string> & column_names,
-                                       std::vector<X> & right_side,
-                                       std::vector<T> & costs) : // right_side and costs are redundant
+                                       std::unordered_map<unsigned, std::string> & column_names):
     lp_core_solver_base<T, X>(A,
-                              right_side,
+                              m_right_sides_dummy,
                               basis,
                               x,
-                              costs,
+                              m_costs_dummy,
                               settings,
                               column_names,
                               column_types,
diff --git a/src/util/lp/lar_core_solver.h b/src/util/lp/lar_core_solver.h
index 6222f7710..8c06610a6 100644
--- a/src/util/lp/lar_core_solver.h
+++ b/src/util/lp/lar_core_solver.h
@@ -26,16 +26,17 @@ class lar_core_solver : public lp_core_solver_base<T, X> {
     binary_heap_priority_queue<X> m_breakpoint_indices_queue;
     std::vector<std::pair<mpq, unsigned>> m_infeasible_row;
     int m_infeasible_row_sign = 0;
-    // with a breakpoint at this delta
+    std::vector<X> m_right_sides_dummy;
+    std::vector<T> m_costs_dummy;
 public:
-    lar_core_solver(std::vector<X> & x, std::vector<column_type> & column_types,
-                    std::vector<X> & low_bounds, std::vector<X> & upper_bounds,
+    lar_core_solver(std::vector<X> & x,
+                    std::vector<column_type> & column_types,
+                    std::vector<X> & low_bounds,
+                    std::vector<X> & upper_bounds,
                     std::vector<unsigned> & basis,
                     static_matrix<T, X> & A,
                     lp_settings & settings,
-                    std::unordered_map<unsigned, std::string> & column_names,
-                    std::vector<X> & right_side,
-                    std::vector<T> & costs);
+                    std::unordered_map<unsigned, std::string> & column_names);
 
     int get_infeasible_row_sign() const { return m_infeasible_row_sign;   }
 
diff --git a/src/util/lp/lar_core_solver_instances.cpp b/src/util/lp/lar_core_solver_instances.cpp
index c89328ec3..1c56d8fb1 100644
--- a/src/util/lp/lar_core_solver_instances.cpp
+++ b/src/util/lp/lar_core_solver_instances.cpp
@@ -10,7 +10,14 @@
 #include <vector>
 #include <functional>
 #include "util/lp/lar_core_solver.cpp"
-template lean::lar_core_solver<lean::mpq, lean::numeric_pair<lean::mpq> >::lar_core_solver(std::vector<lean::numeric_pair<lean::mpq>, std::allocator<lean::numeric_pair<lean::mpq> > >&, std::vector<lean::column_type, std::allocator<lean::column_type> >&, std::vector<lean::numeric_pair<lean::mpq>, std::allocator<lean::numeric_pair<lean::mpq> > >&, std::vector<lean::numeric_pair<lean::mpq>, std::allocator<lean::numeric_pair<lean::mpq> > >&, std::vector<unsigned int, std::allocator<unsigned int> >&, lean::static_matrix<lean::mpq, lean::numeric_pair<lean::mpq> >&, lean::lp_settings&, std::unordered_map<unsigned int, std::string, std::hash<unsigned int>, std::equal_to<unsigned int>, std::allocator<std::pair<unsigned int const, std::string> > >&, std::vector<lean::numeric_pair<lean::mpq>, std::allocator<lean::numeric_pair<lean::mpq> > >&, std::vector<lean::mpq, std::allocator<lean::mpq> >&);
+template lean::lar_core_solver<lean::mpq, lean::numeric_pair<lean::mpq> >::lar_core_solver(std::vector<lean::numeric_pair<lean::mpq>, std::allocator<lean::numeric_pair<lean::mpq> > >&,
+                                                                                           std::vector<lean::column_type, std::allocator<lean::column_type> >&,
+                                                                                           std::vector<lean::numeric_pair<lean::mpq>, std::allocator<lean::numeric_pair<lean::mpq> > >&,
+                                                                                           std::vector<lean::numeric_pair<lean::mpq>, std::allocator<lean::numeric_pair<lean::mpq> > >&,
+                                                                                           std::vector<unsigned int, std::allocator<unsigned int> >&,
+                                                                                           lean::static_matrix<lean::mpq, lean::numeric_pair<lean::mpq> >&,
+                                                                                           lean::lp_settings&,
+                                                                                           std::unordered_map<unsigned int, std::string, std::hash<unsigned int>, std::equal_to<unsigned int>, std::allocator<std::pair<unsigned int const, std::string> > >&);
 template void lean::lar_core_solver<lean::mpq, lean::numeric_pair<lean::mpq> >::solve();
 template void lean::lar_core_solver<lean::mpq, lean::numeric_pair<lean::mpq> >::prefix();
 template void lean::lar_core_solver<lean::mpq, lean::numeric_pair<lean::mpq> >::print_column_info(unsigned int, std::ostream & out);
diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp
index 5547349a8..0f30907cf 100644
--- a/src/util/lp/lar_solver.cpp
+++ b/src/util/lp/lar_solver.cpp
@@ -427,12 +427,6 @@ void lar_solver::update_column_info_of_normalized_constraints() {
         update_column_info_of_normalized_constraint(it.second);
 }
 
-template <typename V>
-void lar_solver::init_right_sides_with_zeros(std::vector<V> & rs) {
-    rs.clear();
-    rs.resize(m_basis.size(), zero_of_type<V>());
-}
-
 mpq lar_solver::sum_of_right_sides_of_evidence(const buffer<std::pair<mpq, unsigned>> & evidence) {
     mpq ret = numeric_traits<mpq>::zero();
     for (auto & it : evidence) {
@@ -464,7 +458,6 @@ void lar_solver::prepare_independently_of_numeric_type() {
 
 template <typename U, typename V>
 void lar_solver::prepare_core_solver_fields(static_matrix<U, V> & A, std::vector<V> & x,
-                                            std::vector<V> & right_side_vector,
                                             std::vector<V> & low_bound,
                                             std::vector<V> & upper_bound) {
     create_matrix_A(A);
@@ -472,14 +465,12 @@ void lar_solver::prepare_core_solver_fields(static_matrix<U, V> & A, std::vector
     if (m_status == INFEASIBLE) {
         lean_assert(false); // not implemented
     }
-    init_right_sides_with_zeros(right_side_vector);
     resize_x_and_init_with_zeros(x, A.column_count());
     lean_assert(m_basis.size() == A.row_count());
 }
 
 template <typename U, typename V>
 void lar_solver::prepare_core_solver_fields_with_signature(static_matrix<U, V> & A, std::vector<V> & x,
-                                                           std::vector<V> & right_side_vector,
                                                            std::vector<V> & low_bound,
                                                            std::vector<V> & upper_bound, const lar_solution_signature & signature) {
     create_matrix_A(A);
@@ -487,15 +478,16 @@ void lar_solver::prepare_core_solver_fields_with_signature(static_matrix<U, V> &
     if (m_status == INFEASIBLE) {
         lean_assert(false); // not implemented
     }
-    init_right_sides_with_zeros(right_side_vector);
     resize_x_and_init_with_signature(x, low_bound, upper_bound, signature);
 }
 
 void lar_solver::find_solution_signature_with_doubles(lar_solution_signature & signature) {
     static_matrix<double, double> A;
-    std::vector<double> x, right_side_vector, low_bounds, upper_bounds;
-    prepare_core_solver_fields<double, double>(A, x, right_side_vector, low_bounds, upper_bounds);
+    std::vector<double> x, low_bounds, upper_bounds;
+    prepare_core_solver_fields<double, double>(A, x, low_bounds, upper_bounds);
     std::vector<double> column_scale_vector;
+    std::vector<double> right_side_vector(A.row_count(), 0);
+
     scaler<double, double > scaler(right_side_vector, A, m_settings.scaling_minimum, m_settings.scaling_maximum, column_scale_vector, this->m_settings);
     if (!scaler.scale()) {
         // the scale did not succeed, unscaling
@@ -526,7 +518,7 @@ void lar_solver::extract_signature_from_lp_core_solver(lp_primal_core_solver<U,
 }
 
 void lar_solver::solve_on_signature(const lar_solution_signature & signature) {
-    prepare_core_solver_fields_with_signature(m_A, m_x, m_right_side_vector, m_low_bounds, m_upper_bounds, signature);
+    prepare_core_solver_fields_with_signature(m_A, m_x, m_low_bounds, m_upper_bounds, signature);
     solve_with_core_solver();
 }
 
@@ -539,7 +531,7 @@ void lar_solver::solve() {
         solve_on_signature(solution_signature);
         return;
     }
-    prepare_core_solver_fields(m_A, m_x, m_right_side_vector, m_low_bounds, m_upper_bounds);
+    prepare_core_solver_fields(m_A, m_x, m_low_bounds, m_upper_bounds);
     solve_with_core_solver();
 }
 
diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h
index 051f01f7c..104d9c522 100644
--- a/src/util/lp/lar_solver.h
+++ b/src/util/lp/lar_solver.h
@@ -66,8 +66,6 @@ class lar_solver {
     std::vector<unsigned> m_basis;
     std::vector<numeric_pair<mpq>> m_x; // the solution
     std::unordered_map<unsigned, std::string> m_column_names;
-    std::vector<numeric_pair<mpq>> m_right_side_vector; // this vector will be all zeroes, it might change when the optimization with fixed variables will used
-    std::vector<mpq> m_costs;
     canonic_left_side * m_infeasible_canonic_left_side = nullptr; // such can be found at the initialization step
     canonic_left_side * create_or_fetch_existing_left_side(const buffer<std::pair<mpq, var_index>>& left_side_par);
 
@@ -150,9 +148,7 @@ public:
                                      m_basis,
                                      m_A,
                                      m_settings,
-                                     m_column_names,
-                                     m_right_side_vector,
-                                     m_costs) {
+                                     m_column_names) {
     }
 
 
@@ -178,21 +174,16 @@ public:
 
     void update_column_info_of_normalized_constraints();
 
-    template <typename V>
-    void init_right_sides_with_zeros(std::vector<V> & rs);
-
     mpq sum_of_right_sides_of_evidence(const buffer<std::pair<mpq, unsigned>> & evidence);
     void prepare_independently_of_numeric_type();
 
     template <typename U, typename V>
     void prepare_core_solver_fields(static_matrix<U, V> & A, std::vector<V> & x,
-                                    std::vector<V> & right_side_vector,
                                     std::vector<V> & low_bound,
                                     std::vector<V> & upper_bound);
 
     template <typename U, typename V>
     void prepare_core_solver_fields_with_signature(static_matrix<U, V> & A, std::vector<V> & x,
-                                                   std::vector<V> & right_side_vector,
                                                    std::vector<V> & low_bound,
                                                    std::vector<V> & upper_bound, const lar_solution_signature & signature);