diff --git a/contrib/cmake/src/test/CMakeLists.txt b/contrib/cmake/src/test/CMakeLists.txt
index b395c09e6..f92525069 100644
--- a/contrib/cmake/src/test/CMakeLists.txt
+++ b/contrib/cmake/src/test/CMakeLists.txt
@@ -1,4 +1,5 @@
 add_subdirectory(fuzzing)
+add_subdirectory(lp)
 ################################################################################
 # z3-test executable
 ################################################################################
@@ -117,7 +118,7 @@ add_executable(test-z3
   upolynomial.cpp
   var_subst.cpp
   vector.cpp
-  lp.cpp
+  lp/lp.cpp
   ${z3_test_extra_object_files}
 )
 z3_add_install_tactic_rule(${z3_test_deps})
diff --git a/contrib/cmake/src/test/lp/CMakeLists.txt b/contrib/cmake/src/test/lp/CMakeLists.txt
new file mode 100644
index 000000000..99f8747b1
--- /dev/null
+++ b/contrib/cmake/src/test/lp/CMakeLists.txt
@@ -0,0 +1,6 @@
+add_executable(lp_tst lp_main.cpp lp.cpp $<TARGET_OBJECTS:util>   $<TARGET_OBJECTS:lp>)
+target_compile_definitions(lp_tst PRIVATE ${Z3_COMPONENT_CXX_DEFINES})
+target_compile_options(lp_tst PRIVATE ${Z3_COMPONENT_CXX_FLAGS})
+target_include_directories(lp_tst PRIVATE ${Z3_COMPONENT_EXTRA_INCLUDE_DIRS})
+target_link_libraries(lp_tst PRIVATE ${Z3_DEPENDENT_LIBS})
+z3_append_linker_flag_list_to_target(lp_tst ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS})
diff --git a/src/test/argument_parser.h b/src/test/lp/argument_parser.h
similarity index 100%
rename from src/test/argument_parser.h
rename to src/test/lp/argument_parser.h
diff --git a/src/test/lp.cpp b/src/test/lp/lp.cpp
similarity index 99%
rename from src/test/lp.cpp
rename to src/test/lp/lp.cpp
index 235dab960..1acf4ba2a 100644
--- a/src/test/lp.cpp
+++ b/src/test/lp/lp.cpp
@@ -2691,8 +2691,8 @@ void test_term() {
     lar_solver solver;
     unsigned _x = 0;
     unsigned _y = 1;
-    var_index x = solver.add_var(_x);
-    var_index y = solver.add_var(_y);
+    var_index x = solver.add_var(_x, false);
+    var_index y = solver.add_var(_y, false);
 
     vector<std::pair<mpq, var_index>> term_ls;
     term_ls.push_back(std::pair<mpq, var_index>((int)1, x));
@@ -2719,8 +2719,8 @@ void test_term() {
 
 void test_evidence_for_total_inf_simple(argument_parser & args_parser) {
     lar_solver solver;
-    var_index x = solver.add_var(0);
-    var_index y = solver.add_var(1);
+    var_index x = solver.add_var(0, false);
+    var_index y = solver.add_var(1, false);
     solver.add_var_bound(x, LE, -mpq(1));
     solver.add_var_bound(y, GE, mpq(0));
     vector<std::pair<mpq, var_index>> ls;
@@ -2754,9 +2754,9 @@ If b becomes basic variable, then it is likely the old solver ends up with a row
             return true; 
         };   
     lar_solver ls;
-    unsigned a = ls.add_var(0);
-    unsigned b = ls.add_var(1);
-    unsigned c = ls.add_var(2);
+    unsigned a = ls.add_var(0, false);
+    unsigned b = ls.add_var(1, false);
+    unsigned c = ls.add_var(2, false);
     vector<std::pair<mpq, var_index>> coeffs;
     coeffs.push_back(std::pair<mpq, var_index>(1, a));
     coeffs.push_back(std::pair<mpq, var_index>(-1, c));
@@ -2819,8 +2819,8 @@ If x9 becomes basic variable, then it is likely the old solver ends up with a ro
 }
 void test_bound_propagation_one_row() {
     lar_solver ls;
-    unsigned x0 = ls.add_var(0);
-    unsigned x1 = ls.add_var(1);
+    unsigned x0 = ls.add_var(0, false);
+    unsigned x1 = ls.add_var(1, false);
     vector<std::pair<mpq, var_index>> c;
     c.push_back(std::pair<mpq, var_index>(1, x0));
     c.push_back(std::pair<mpq, var_index>(-1, x1));
@@ -2833,8 +2833,8 @@ void test_bound_propagation_one_row() {
 } 
 void test_bound_propagation_one_row_with_bounded_vars() {
     lar_solver ls;
-    unsigned x0 = ls.add_var(0);
-    unsigned x1 = ls.add_var(1);
+    unsigned x0 = ls.add_var(0, false);
+    unsigned x1 = ls.add_var(1, false);
     vector<std::pair<mpq, var_index>> c;
     c.push_back(std::pair<mpq, var_index>(1, x0));
     c.push_back(std::pair<mpq, var_index>(-1, x1));
@@ -2849,8 +2849,8 @@ void test_bound_propagation_one_row_with_bounded_vars() {
 }
 void test_bound_propagation_one_row_mixed() {
     lar_solver ls;
-    unsigned x0 = ls.add_var(0);
-    unsigned x1 = ls.add_var(1);
+    unsigned x0 = ls.add_var(0, false);
+    unsigned x1 = ls.add_var(1, false);
     vector<std::pair<mpq, var_index>> c;
     c.push_back(std::pair<mpq, var_index>(1, x0));
     c.push_back(std::pair<mpq, var_index>(-1, x1));
@@ -2864,9 +2864,9 @@ void test_bound_propagation_one_row_mixed() {
 
 void test_bound_propagation_two_rows() {
     lar_solver ls;
-    unsigned x = ls.add_var(0);
-    unsigned y = ls.add_var(1);
-    unsigned z = ls.add_var(2);
+    unsigned x = ls.add_var(0, false);
+    unsigned y = ls.add_var(1, false);
+    unsigned z = ls.add_var(2, false);
     vector<std::pair<mpq, var_index>> c;
     c.push_back(std::pair<mpq, var_index>(1, x));
     c.push_back(std::pair<mpq, var_index>(2, y));
@@ -2888,9 +2888,9 @@ void test_bound_propagation_two_rows() {
 void test_total_case_u() {
     std::cout << "test_total_case_u\n";
     lar_solver ls;
-    unsigned x = ls.add_var(0);
-    unsigned y = ls.add_var(1);
-    unsigned z = ls.add_var(2);
+    unsigned x = ls.add_var(0, false);
+    unsigned y = ls.add_var(1, false);
+    unsigned z = ls.add_var(2, false);
     vector<std::pair<mpq, var_index>> c;
     c.push_back(std::pair<mpq, var_index>(1, x));
     c.push_back(std::pair<mpq, var_index>(2, y));
@@ -2914,9 +2914,9 @@ bool contains_j_kind(unsigned j, lconstraint_kind kind, const mpq & rs, const ve
 void test_total_case_l(){
     std::cout << "test_total_case_l\n";
     lar_solver ls;
-    unsigned x = ls.add_var(0);
-    unsigned y = ls.add_var(1);
-    unsigned z = ls.add_var(2);
+    unsigned x = ls.add_var(0, false);
+    unsigned y = ls.add_var(1, false);
+    unsigned z = ls.add_var(2, false);
     vector<std::pair<mpq, var_index>> c;
     c.push_back(std::pair<mpq, var_index>(1, x));
     c.push_back(std::pair<mpq, var_index>(2, y));
diff --git a/src/test/smt_reader.h b/src/test/lp/smt_reader.h
similarity index 99%
rename from src/test/smt_reader.h
rename to src/test/lp/smt_reader.h
index 38e3f4157..dd38c6bcd 100644
--- a/src/test/smt_reader.h
+++ b/src/test/lp/smt_reader.h
@@ -376,7 +376,7 @@ namespace lean {
         void add_constraint_to_solver(lar_solver * solver, formula_constraint & fc) {
             vector<std::pair<mpq, var_index>> ls;
             for (auto & it : fc.m_coeffs) {
-                ls.push_back(std::make_pair(it.first, solver->add_var(register_name(it.second))));
+                ls.push_back(std::make_pair(it.first, solver->add_var(register_name(it.second), false)));
             }
             solver->add_constraint(ls, fc.m_kind, fc.m_right_side);
         }
diff --git a/src/test/test_file_reader.h b/src/test/lp/test_file_reader.h
similarity index 100%
rename from src/test/test_file_reader.h
rename to src/test/lp/test_file_reader.h
diff --git a/src/util/lp/init_lar_solver.cpp b/src/util/lp/init_lar_solver.cpp
index a84d791d5..5efa24a48 100644
--- a/src/util/lp/init_lar_solver.cpp
+++ b/src/util/lp/init_lar_solver.cpp
@@ -2,8 +2,10 @@
   Copyright (c) 2017 Microsoft Corporation
   Author: Lev Nachmanson
 */
-#include "util/lp/lar_solver.h"
+// this file represents the intiialization functionality of lar_solver
 
+
+#include "util/lp/lar_solver.h"
 namespace lean {
 
 bool lar_solver::strategy_is_undecided() const {
diff --git a/src/util/lp/mps_reader.h b/src/util/lp/mps_reader.h
index 4c08ec8e6..6b80c2257 100644
--- a/src/util/lp/mps_reader.h
+++ b/src/util/lp/mps_reader.h
@@ -810,7 +810,7 @@ public:
             auto kind = get_lar_relation_from_row(row->m_type);
             vector<std::pair<mpq, var_index>> ls;
             for (auto s : row->m_row_columns) {
-                var_index i = solver->add_var(get_var_index(s.first));
+                var_index i = solver->add_var(get_var_index(s.first), false);
                 ls.push_back(std::make_pair(s.second, i));
             }
             solver->add_constraint(ls, kind, row->m_right_side);
@@ -828,20 +828,20 @@ public:
 
     void create_low_constraint_for_var(column* col, bound * b, lar_solver *solver) {
         vector<std::pair<mpq, var_index>> ls;
-        var_index i = solver->add_var(col->m_index);
+        var_index i = solver->add_var(col->m_index, false);
         ls.push_back(std::make_pair(numeric_traits<T>::one(), i));
         solver->add_constraint(ls, GE, b->m_low);
     }
 
     void create_upper_constraint_for_var(column* col, bound * b, lar_solver *solver) {
-        var_index i = solver->add_var(col->m_index);
+        var_index i = solver->add_var(col->m_index, false);
         vector<std::pair<mpq, var_index>> ls;
         ls.push_back(std::make_pair(numeric_traits<T>::one(), i));
         solver->add_constraint(ls, LE, b->m_upper);
     }
 
     void create_equality_contraint_for_var(column* col, bound * b, lar_solver *solver) {
-        var_index i = solver->add_var(col->m_index);
+        var_index i = solver->add_var(col->m_index, false);
         vector<std::pair<mpq, var_index>> ls;
         ls.push_back(std::make_pair(numeric_traits<T>::one(), i));
         solver->add_constraint(ls, EQ, b->m_fixed_value);
@@ -850,7 +850,7 @@ public:
     void fill_lar_solver_on_columns(lar_solver * solver) {
         for (auto s : m_columns) {
             mps_reader::column * col = s.second;
-            solver->add_var(col->m_index);
+            solver->add_var(col->m_index, false);
             auto b = col->m_bound;
             if (b == nullptr) return;