diff --git a/src/math/lp/CMakeLists.txt b/src/math/lp/CMakeLists.txt
index 98241bf60..4ca8cb1d2 100644
--- a/src/math/lp/CMakeLists.txt
+++ b/src/math/lp/CMakeLists.txt
@@ -20,7 +20,6 @@ z3_add_component(lp
     lp_core_solver_base.cpp
     lp_primal_core_solver.cpp
     lp_settings.cpp
-    lp_utils.cpp
     matrix.cpp
     mon_eq.cpp
     monomial_bounds.cpp
diff --git a/src/math/lp/lp_primal_core_solver.h b/src/math/lp/lp_primal_core_solver.h
index 17b1ea494..1719f9c55 100644
--- a/src/math/lp/lp_primal_core_solver.h
+++ b/src/math/lp/lp_primal_core_solver.h
@@ -618,8 +618,6 @@ public:
     
     void print_bound_info_and_x(unsigned j, std::ostream & out);
     
-    unsigned solve_with_tableau();
-
     bool basis_column_is_set_correctly(unsigned j) const {
         return this->m_A.m_columns[j].size() == 1;
             
diff --git a/src/math/lp/lp_primal_core_solver_def.h b/src/math/lp/lp_primal_core_solver_def.h
index 1c48f1163..cc8ad88b3 100644
--- a/src/math/lp/lp_primal_core_solver_def.h
+++ b/src/math/lp/lp_primal_core_solver_def.h
@@ -315,11 +315,6 @@ 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";);
-    return solve_with_tableau();
-}
 
 // calling it stage1 is too cryptic
 template <typename T, typename X>    void lp_primal_core_solver<T, X>::find_feasible_solution() {
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 de2f1c208..c7b604b95 100644
--- a/src/math/lp/lp_primal_core_solver_tableau_def.h
+++ b/src/math/lp/lp_primal_core_solver_tableau_def.h
@@ -87,7 +87,8 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>::advance_on_e
 }
 
 template <typename T, typename X>
-unsigned lp_primal_core_solver<T, X>::solve_with_tableau() {
+unsigned lp_primal_core_solver<T, X>::solve() {
+    TRACE("lar_solver", tout << "solve " << this->get_status() << "\n";);
     init_run_tableau();
     if (this->current_x_is_feasible() && this->m_look_for_feasible_solution_only) {
         this->set_status(lp_status::FEASIBLE);
diff --git a/src/math/lp/lp_utils.cpp b/src/math/lp/lp_utils.cpp
deleted file mode 100644
index b909a0389..000000000
--- a/src/math/lp/lp_utils.cpp
+++ /dev/null
@@ -1,26 +0,0 @@
-/*++
-Copyright (c) 2017 Microsoft Corporation
-
-Module Name:
-
-    <name>
-
-Abstract:
-
-    <abstract>
-
-Author:
-
-    Lev Nachmanson (levnach)
-
-Revision History:
-
-
---*/
-#include "math/lp/lp_utils.h"
-#ifdef lp_for_z3
-namespace lp {
-
-}
-#endif
-