diff --git a/src/test/argument_parser.h b/src/test/argument_parser.h
index 706167f49..c8566ce34 100644
--- a/src/test/argument_parser.h
+++ b/src/test/argument_parser.h
@@ -1,9 +1,22 @@
-/*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
+/*++
+Copyright (c) 2017 Microsoft Corporation
 
-Author: Lev Nachmanson
-*/
+Module Name:
+
+    <name>
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Lev Nachmanson (levnach)
+
+Revision History:
+
+
+--*/
 
 #include <unordered_map>
 #include <vector>
@@ -11,7 +24,7 @@ Author: Lev Nachmanson
 #include <set>
 #include <iostream>
 
-namespace lean {
+namespace lp {
 class argument_parser {
     std::unordered_map<std::string, std::string> m_options;
     std::unordered_map<std::string, std::string> m_options_with_after_string;
diff --git a/src/test/lp.cpp b/src/test/lp.cpp
index 695a31cf4..0f4186252 100644
--- a/src/test/lp.cpp
+++ b/src/test/lp.cpp
@@ -1,7 +1,23 @@
-/*
-Copyright (c) 2017 Microsoft Corporation. All rights reserved.
-Author: Lev Nachmanson
-*/
+/*++
+Copyright (c) 2017 Microsoft Corporation
+
+Module Name:
+
+    <name>
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Lev Nachmanson (levnach)
+
+Revision History:
+
+
+--*/
+
 #include <limits>
 #if _LINUX_
 #include <dirent.h>
@@ -31,8 +47,9 @@ Author: Lev Nachmanson
 #include "util/lp/stacked_unordered_set.h"
 #include "util/lp/int_set.h"
 #include "util/stopwatch.h"
-namespace lean {
-unsigned seed = 1;
+
+namespace lp {
+    unsigned seed = 1;
 
     random_gen g_rand;
     static unsigned my_random() {
@@ -78,7 +95,7 @@ void test_matrix(sparse_matrix<T, X> & a) {
 
     a.set(i, j, t);
 
-    lean_assert(a.get(i, j) == t);
+    SASSERT(a.get(i, j) == t);
 
     unsigned j1;
     if (j < m - 1) {
@@ -155,7 +172,7 @@ void tst1() {
 
     test_matrix(m10by9);
     std::cout <<"zeroing m10by9\n";
-#ifdef LEAN_DEBUG
+#ifdef Z3DEBUG
     for (unsigned int i = 0; i < m10by9.dimension(); i++)
         for (unsigned int j = 0; j < m10by9.column_count(); j++)
             m10by9.set(i, j, 0);
@@ -170,7 +187,7 @@ vector<int> allocate_basis_heading(unsigned count) { // the rest of initilizatio
 
 
 void init_basic_part_of_basis_heading(vector<unsigned> & basis, vector<int> & basis_heading) {
-    lean_assert(basis_heading.size() >= basis.size());
+    SASSERT(basis_heading.size() >= basis.size());
     unsigned m = basis.size();
     for (unsigned i = 0; i < m; i++) {
         unsigned column = basis[i];
@@ -205,7 +222,7 @@ void change_basis(unsigned entering, unsigned leaving, vector<unsigned>& basis,
 }
 
 
-#ifdef LEAN_DEBUG
+#ifdef Z3DEBUG
 void test_small_lu(lp_settings & settings) {
     std::cout << " test_small_lu" << std::endl;
     static_matrix<double, double> m(3, 6);
@@ -218,61 +235,61 @@ void test_small_lu(lp_settings & settings) {
     m(1, 1) = 4; m(1, 4) = 7;
     m(2, 0) = 1.8; m(2, 2) = 5; m(2, 4) = 2; m(2, 5) = 8;
 
-#ifdef LEAN_DEBUG
+#ifdef Z3DEBUG
     print_matrix(m, std::cout);
 #endif
     vector<int> heading = allocate_basis_heading(m.column_count());
     vector<unsigned> non_basic_columns;
     init_basis_heading_and_non_basic_columns_vector(basis, heading, non_basic_columns);
     lu<double, double> l(m, basis, settings);
-    lean_assert(l.is_correct(basis));
+    SASSERT(l.is_correct(basis));
     indexed_vector<double> w(m.row_count());
     std::cout << "entering 2, leaving 0" << std::endl;
     l.prepare_entering(2, w); // to init vector w
     l.replace_column(0, w, heading[0]);
     change_basis(2, 0, basis, non_basic_columns, heading);
-    // #ifdef LEAN_DEBUG
+    // #ifdef Z3DEBUG
     // std::cout << "we were factoring " << std::endl;
     // print_matrix(get_B(l));
     // #endif
-    lean_assert(l.is_correct(basis));
+    SASSERT(l.is_correct(basis));
     std::cout << "entering 4, leaving 3" << std::endl;
     l.prepare_entering(4, w); // to init vector w
     l.replace_column(0, w, heading[3]);
     change_basis(4, 3, basis, non_basic_columns, heading);
     std::cout << "we were factoring " << std::endl;
-#ifdef LEAN_DEBUG
+#ifdef Z3DEBUG
     {
         auto bl = get_B(l, basis);
         print_matrix(&bl, std::cout);
     }
 #endif
-    lean_assert(l.is_correct(basis));
+    SASSERT(l.is_correct(basis));
 
     std::cout << "entering 5, leaving 1" << std::endl;
     l.prepare_entering(5, w); // to init vector w
     l.replace_column(0, w, heading[1]);
     change_basis(5, 1, basis, non_basic_columns, heading);
     std::cout << "we were factoring " << std::endl;
-#ifdef LEAN_DEBUG
+#ifdef Z3DEBUG
     {
         auto bl = get_B(l, basis);
         print_matrix(&bl, std::cout);
     }
 #endif
-    lean_assert(l.is_correct(basis));
+    SASSERT(l.is_correct(basis));
     std::cout << "entering 3, leaving 2" << std::endl;
     l.prepare_entering(3, w); // to init vector w
     l.replace_column(0, w, heading[2]);
     change_basis(3, 2, basis, non_basic_columns, heading);
     std::cout << "we were factoring " << std::endl;
-#ifdef LEAN_DEBUG
+#ifdef Z3DEBUG
     {
         auto bl = get_B(l, basis);
         print_matrix(&bl, std::cout);
     }
 #endif
-    lean_assert(l.is_correct(basis));
+    SASSERT(l.is_correct(basis));
 
     m.add_row();
     m.add_column();
@@ -291,7 +308,7 @@ void test_small_lu(lp_settings & settings) {
     auto columns_to_replace = l.get_set_of_columns_to_replace_for_add_last_rows(heading);
     l.add_last_rows_to_B(heading, columns_to_replace);
     std::cout << "here" << std::endl;
-    lean_assert(l.is_correct(basis));
+    SASSERT(l.is_correct(basis));
 }
 
 #endif
@@ -351,7 +368,7 @@ void fill_larger_sparse_matrix(static_matrix<double, double> & m){
 
 int perm_id = 0;
 
-#ifdef LEAN_DEBUG
+#ifdef Z3DEBUG
 void test_larger_lu_exp(lp_settings & settings) {
     std::cout << " test_larger_lu_exp" << std::endl;
     static_matrix<double, double> m(6, 12);
@@ -373,7 +390,7 @@ void test_larger_lu_exp(lp_settings & settings) {
 
     dense_matrix<double, double> left_side = l.get_left_side(basis);
     dense_matrix<double, double> right_side = l.get_right_side();
-    lean_assert(left_side == right_side);
+    SASSERT(left_side == right_side);
     int leaving = 3;
     int entering = 8;
     for (unsigned i = 0; i < m.row_count(); i++) {
@@ -385,12 +402,12 @@ void test_larger_lu_exp(lp_settings & settings) {
     l.prepare_entering(entering, w);
     l.replace_column(0, w, heading[leaving]);
     change_basis(entering, leaving, basis, non_basic_columns, heading);
-    lean_assert(l.is_correct(basis));
+    SASSERT(l.is_correct(basis));
 
     l.prepare_entering(11, w); // to init vector w
     l.replace_column(0, w, heading[0]);
     change_basis(11, 0, basis, non_basic_columns, heading);
-    lean_assert(l.is_correct(basis));
+    SASSERT(l.is_correct(basis));
 }
 
 void test_larger_lu_with_holes(lp_settings & settings) {
@@ -432,7 +449,7 @@ void test_larger_lu_with_holes(lp_settings & settings) {
     l.prepare_entering(8, w); // to init vector w
     l.replace_column(0, w, heading[0]);
     change_basis(8, 0, basis, non_basic_columns, heading);
-    lean_assert(l.is_correct(basis));
+    SASSERT(l.is_correct(basis));
 }
 
 
@@ -479,7 +496,7 @@ void test_larger_lu(lp_settings& settings) {
     l.prepare_entering(9, w); // to init vector w
     l.replace_column(0, w, heading[0]);
     change_basis(9, 0, basis, non_basic_columns, heading);
-    lean_assert(l.is_correct(basis));
+    SASSERT(l.is_correct(basis));
 }
 
 
@@ -550,7 +567,7 @@ void test_lp_1() {
     m(1, 0) = -1;                m(1, 2) = 3;  m(1, 4) = 1;
     m(2, 0) =  2;  m(2, 1) = -1; m(2, 2) = 2;  m(2, 5) = 1;
     m(3, 0) =  2;  m(3, 1) =  3; m(3, 2) = -1; m(3, 6) = 1;
-#ifdef LEAN_DEBUG
+#ifdef Z3DEBUG
     print_matrix(m, std::cout);
 #endif
     vector<double> x_star(7);
@@ -604,7 +621,7 @@ void test_lp_primal_core_solver() {
 }
 
 
-#ifdef LEAN_DEBUG
+#ifdef Z3DEBUG
 template <typename T, typename X>
 void test_swap_rows_with_permutation(sparse_matrix<T, X>& m){
     std::cout << "testing swaps" << std::endl;
@@ -612,7 +629,7 @@ void test_swap_rows_with_permutation(sparse_matrix<T, X>& m){
     dense_matrix<double, double> original(&m);
     permutation_matrix<double, double> q(dim);
     print_matrix(m, std::cout);
-    lean_assert(original == q * m);
+    SASSERT(original == q * m);
     for (int i = 0; i < 100; i++) {
         unsigned row1 = my_random() % dim;
         unsigned row2 = my_random() % dim;
@@ -620,7 +637,7 @@ void test_swap_rows_with_permutation(sparse_matrix<T, X>& m){
         std::cout << "swap " << row1 << " " << row2 << std::endl;
         m.swap_rows(row1, row2);
         q.transpose_from_left(row1, row2);
-        lean_assert(original == q * m);
+        SASSERT(original == q * m);
         print_matrix(m, std::cout);
         std::cout << std::endl;
     }
@@ -628,7 +645,7 @@ void test_swap_rows_with_permutation(sparse_matrix<T, X>& m){
 #endif
 template <typename T, typename X>
 void fill_matrix(sparse_matrix<T, X>& m); // forward definition
-#ifdef LEAN_DEBUG
+#ifdef Z3DEBUG
 template <typename T, typename X>
 void test_swap_cols_with_permutation(sparse_matrix<T, X>& m){
     std::cout << "testing swaps" << std::endl;
@@ -636,7 +653,7 @@ void test_swap_cols_with_permutation(sparse_matrix<T, X>& m){
     dense_matrix<double, double> original(&m);
     permutation_matrix<double, double> q(dim);
     print_matrix(m, std::cout);
-    lean_assert(original == q * m);
+    SASSERT(original == q * m);
     for (int i = 0; i < 100; i++) {
         unsigned row1 = my_random() % dim;
         unsigned row2 = my_random() % dim;
@@ -644,7 +661,7 @@ void test_swap_cols_with_permutation(sparse_matrix<T, X>& m){
         std::cout << "swap " << row1 << " " << row2 << std::endl;
         m.swap_rows(row1, row2);
         q.transpose_from_right(row1, row2);
-        lean_assert(original == q * m);
+        SASSERT(original == q * m);
         print_matrix(m, std::cout);
         std::cout << std::endl;
     }
@@ -663,8 +680,8 @@ void test_swap_rows(sparse_matrix<T, X>& m, unsigned i0, unsigned i1){
     m.swap_rows(i0, i1);
 
     for (unsigned j = 0; j < m.dimension(); j++) {
-        lean_assert(mcopy(i0, j) == m(i1, j));
-        lean_assert(mcopy(i1, j) == m(i0, j));
+        SASSERT(mcopy(i0, j) == m(i1, j));
+        SASSERT(mcopy(i1, j) == m(i0, j));
     }
 }
 template <typename T, typename X>
@@ -678,15 +695,15 @@ void test_swap_columns(sparse_matrix<T, X>& m, unsigned i0, unsigned i1){
     m.swap_columns(i0, i1);
 
     for (unsigned j = 0; j < m.dimension(); j++) {
-        lean_assert(mcopy(j, i0) == m(j, i1));
-        lean_assert(mcopy(j, i1) == m(j, i0));
+        SASSERT(mcopy(j, i0) == m(j, i1));
+        SASSERT(mcopy(j, i1) == m(j, i0));
     }
 
     for (unsigned i = 0; i  < m.dimension(); i++) {
         if (i == i0 || i == i1)
             continue;
         for (unsigned j = 0; j < m.dimension(); j++) {
-            lean_assert(mcopy(j, i)== m(j, i));
+            SASSERT(mcopy(j, i)== m(j, i));
         }
     }
 }
@@ -731,7 +748,7 @@ void test_pivot_like_swaps_and_pivot(){
     m(target_row, 3) = 0;
     m(target_row, 5) = 0;
     m(pivot_row, 6) = 0;
-#ifdef LEAN_DEBUG
+#ifdef Z3DEBUG
     print_matrix(m, std::cout);
 #endif
 
@@ -748,11 +765,11 @@ void test_pivot_like_swaps_and_pivot(){
     m.pivot_row_to_row(pivot_row_0, beta, target_row, settings);
     //  print_matrix(m);
     for (unsigned j = 0; j < m.dimension(); j++) {
-        lean_assert(abs(row[j] - m(target_row, j)) < 0.00000001);
+        SASSERT(abs(row[j] - m(target_row, j)) < 0.00000001);
     }
 }
 
-#ifdef LEAN_DEBUG
+#ifdef Z3DEBUG
 void test_swap_rows() {
     sparse_matrix<double, double> m(10);
     fill_matrix(m);
@@ -853,57 +870,57 @@ void sparse_matrix_with_permutaions_test() {
     m.multiply_from_left(q0);
     for (unsigned i = 0; i < dim; i++) {
         for (unsigned j = 0; j < dim; j++) {
-            lean_assert(m(i, j) == dm0.get_elem(q0[i], j));
+            SASSERT(m(i, j) == dm0.get_elem(q0[i], j));
         }
     }
 
     auto q0_dm = q0 * dm;
-    lean_assert(m == q0_dm);
+    SASSERT(m == q0_dm);
 
     m.multiply_from_left(q1);
     for (unsigned i = 0; i < dim; i++) {
         for (unsigned j = 0; j < dim; j++) {
-            lean_assert(m(i, j) == dm0.get_elem(q0[q1[i]], j));
+            SASSERT(m(i, j) == dm0.get_elem(q0[q1[i]], j));
         }
     }
 
 
     auto q1_q0_dm = q1 * q0_dm;
 
-    lean_assert(m == q1_q0_dm);
+    SASSERT(m == q1_q0_dm);
 
     m.multiply_from_right(p0);
 
     for (unsigned i = 0; i < dim; i++) {
         for (unsigned j = 0; j < dim; j++) {
-            lean_assert(m(i, j) == dm0.get_elem(q0[q1[i]], p0[j]));
+            SASSERT(m(i, j) == dm0.get_elem(q0[q1[i]], p0[j]));
         }
     }
 
     auto q1_q0_dm_p0 = q1_q0_dm * p0;
 
-    lean_assert(m == q1_q0_dm_p0);
+    SASSERT(m == q1_q0_dm_p0);
 
     m.multiply_from_right(p1);
 
     for (unsigned i = 0; i < dim; i++) {
         for (unsigned j = 0; j < dim; j++) {
-            lean_assert(m(i, j) == dm0.get_elem(q0[q1[i]], p1[p0[j]]));
+            SASSERT(m(i, j) == dm0.get_elem(q0[q1[i]], p1[p0[j]]));
         }
     }
 
     auto q1_q0_dm_p0_p1 = q1_q0_dm_p0 * p1;
-    lean_assert(m == q1_q0_dm_p0_p1);
+    SASSERT(m == q1_q0_dm_p0_p1);
 
     m.multiply_from_right(p1);
     for (unsigned i = 0; i < dim; i++) {
         for (unsigned j = 0; j < dim; j++) {
-            lean_assert(m(i, j) == dm0.get_elem(q0[q1[i]], p1[p1[p0[j]]]));
+            SASSERT(m(i, j) == dm0.get_elem(q0[q1[i]], p1[p1[p0[j]]]));
         }
     }
     auto q1_q0_dm_p0_p1_p1 = q1_q0_dm_p0_p1 * p1;
 
-    lean_assert(m == q1_q0_dm_p0_p1_p1);
+    SASSERT(m == q1_q0_dm_p0_p1_p1);
 }
 
 void test_swap_columns() {
@@ -1021,10 +1038,10 @@ void test_apply_reverse_from_right_to_perm(permutation_matrix<double, double> &
     pclone[4] = 1;
 
     p.multiply_by_reverse_from_right(l);
-#ifdef LEAN_DEBUG
+#ifdef Z3DEBUG
     auto rev = l.get_inverse();
     auto rs = pclone * rev;
-    lean_assert(p == rs)
+    SASSERT(p == rs);
 #endif
 }
 
@@ -1051,8 +1068,8 @@ void test_permutations() {
 
     p.apply_reverse_from_right_to_T(v);
     p.apply_reverse_from_right_to_T(vi);
-    lean_assert(vectors_are_equal(v, vi.m_data));
-    lean_assert(vi.is_OK());
+    SASSERT(vectors_are_equal(v, vi.m_data));
+    SASSERT(vi.is_OK());
 }
 
 void lp_solver_test() {
@@ -1200,7 +1217,7 @@ void solve_mps_double(std::string file_name, bool look_for_min, unsigned max_ite
                     compare_solutions(reader, primal_solver, solver);
                     print_x(reader, primal_solver);
                     std::cout << "dual cost is " << cost << ", but primal cost is " << primal_cost << std::endl;
-                    lean_assert(false);
+                    SASSERT(false);
                 }
             }
         }
@@ -1210,7 +1227,7 @@ void solve_mps_double(std::string file_name, bool look_for_min, unsigned max_ite
 }
 
 void solve_mps_rational(std::string file_name, bool look_for_min, unsigned max_iterations, unsigned time_limit, bool dual, argument_parser & args_parser) {
-    mps_reader<lean::mpq, lean::mpq> reader(file_name);
+    mps_reader<lp::mpq, lp::mpq> reader(file_name);
     reader.read();
     if (reader.is_ok()) {
         auto * solver =  reader.create_solver(dual);
@@ -1224,7 +1241,7 @@ void solve_mps_rational(std::string file_name, bool look_for_min, unsigned max_i
             // for (auto name: reader.column_names()) {
             //  std::cout << name << "=" << solver->get_column_value_by_name(name) << ' ';
             // }
-            lean::mpq cost = solver->get_current_cost();
+            lp::mpq cost = solver->get_current_cost();
             if (look_for_min) {
                 cost = -cost;
             }
@@ -1262,7 +1279,7 @@ void solve_mps(std::string file_name, argument_parser & args_parser) {
 void solve_mps_in_rational(std::string file_name, bool dual, argument_parser & /*args_parser*/) {
     std::cout << "solving " << file_name << std::endl;
 
-    mps_reader<lean::mpq, lean::mpq> reader(file_name);
+    mps_reader<lp::mpq, lp::mpq> reader(file_name);
     reader.read();
     if (reader.is_ok()) {
         auto * solver =  reader.create_solver(dual);
@@ -1274,7 +1291,7 @@ void solve_mps_in_rational(std::string file_name, bool dual, argument_parser & /
                     std::cout << name << "=" << solver->get_column_value_by_name(name).get_double() << ' ';
                 }
             }
-            std::cout << std::endl << "cost = " << numeric_traits<lean::mpq>::get_double(solver->get_current_cost()) << std::endl;
+            std::cout << std::endl << "cost = " << numeric_traits<lp::mpq>::get_double(solver->get_current_cost()) << std::endl;
         }
         delete solver;
     } else {
@@ -1318,7 +1335,7 @@ void test_binary_priority_queue() {
 
     for (unsigned i = 0; i < 10; i++) {
         unsigned de = q.dequeue();
-        lean_assert(i == de);
+        SASSERT(i == de);
         std::cout << de << std::endl;
     }
     q.enqueue(2, 2);
@@ -1337,11 +1354,11 @@ void test_binary_priority_queue() {
     q.dequeue();
     q.remove(33);
     q.enqueue(0, 0);
-#ifdef LEAN_DEBUG
+#ifdef Z3DEBUG
     unsigned t = 0;
     while (q.size() > 0) {
         unsigned d =q.dequeue();
-        lean_assert(t++ == d);
+        SASSERT(t++ == d);
         std::cout << d << std::endl;
     }
 #endif
@@ -1370,7 +1387,7 @@ void solve_mps_with_known_solution(std::string file_name, std::unordered_map<std
         std::cout << "status is " << lp_status_to_string(solver->get_status()) << std::endl;
         if (status != solver->get_status()){
             std::cout << "status should be " << lp_status_to_string(status) << std::endl;
-            lean_assert(status == solver->get_status());
+            SASSERT(status == solver->get_status());
             throw "status is wrong";
         }
         if (solver->get_status() == lp_status::OPTIMAL) {
@@ -1381,7 +1398,7 @@ void solve_mps_with_known_solution(std::string file_name, std::unordered_map<std
                         std::cout << "expected:" << it.first << "=" <<
                             it.second <<", got " << solver->get_column_value_by_name(it.first) << std::endl;
                     }
-                    lean_assert(fabs(it.second - solver->get_column_value_by_name(it.first)) < 0.000001);
+                    SASSERT(fabs(it.second - solver->get_column_value_by_name(it.first)) < 0.000001);
                 }
             }
             if (reader.column_names().size() < 20) {
@@ -1706,48 +1723,48 @@ void solve_some_mps(argument_parser & args_parser) {
 #endif
 
 void solve_rational() {
-    lp_primal_simplex<lean::mpq, lean::mpq> solver;
-    solver.add_constraint(lp_relation::Equal, lean::mpq(7), 0);
-    solver.add_constraint(lp_relation::Equal, lean::mpq(-3), 1);
+    lp_primal_simplex<lp::mpq, lp::mpq> solver;
+    solver.add_constraint(lp_relation::Equal, lp::mpq(7), 0);
+    solver.add_constraint(lp_relation::Equal, lp::mpq(-3), 1);
 
     // setting the cost
     int cost[] = {-3, -1, -1, 2, -1, 1, 1, -4};
     std::string var_names[8] = {"x1", "x2", "x3", "x4", "x5", "x6", "x7", "x8"};
 
     for (unsigned i = 0; i < 8; i++) {
-        solver.set_cost_for_column(i, lean::mpq(cost[i]));
+        solver.set_cost_for_column(i, lp::mpq(cost[i]));
         solver.give_symbolic_name_to_column(var_names[i], i);
     }
 
     int row0[] = {1, 0, 3, 1, -5, -2 , 4, -6};
     for (unsigned i = 0; i < 8; i++) {
-        solver.set_row_column_coefficient(0, i, lean::mpq(row0[i]));
+        solver.set_row_column_coefficient(0, i, lp::mpq(row0[i]));
     }
 
     int row1[] = {0, 1, -2, -1, 4, 1, -3, 5};
     for (unsigned i = 0; i < 8; i++) {
-        solver.set_row_column_coefficient(1, i, lean::mpq(row1[i]));
+        solver.set_row_column_coefficient(1, i, lp::mpq(row1[i]));
     }
 
     int bounds[] = {8, 6, 4, 15, 2, 10, 10, 3};
     for (unsigned i = 0; i < 8; i++) {
-        solver.set_low_bound(i, lean::mpq(0));
-        solver.set_upper_bound(i, lean::mpq(bounds[i]));
+        solver.set_low_bound(i, lp::mpq(0));
+        solver.set_upper_bound(i, lp::mpq(bounds[i]));
     }
 
-    std::unordered_map<std::string, lean::mpq>  expected_sol;
-    expected_sol["x1"] = lean::mpq(0);
-    expected_sol["x2"] = lean::mpq(6);
-    expected_sol["x3"] = lean::mpq(0);
-    expected_sol["x4"] = lean::mpq(15);
-    expected_sol["x5"] = lean::mpq(2);
-    expected_sol["x6"] = lean::mpq(1);
-    expected_sol["x7"] = lean::mpq(1);
-    expected_sol["x8"] = lean::mpq(0);
+    std::unordered_map<std::string, lp::mpq>  expected_sol;
+    expected_sol["x1"] = lp::mpq(0);
+    expected_sol["x2"] = lp::mpq(6);
+    expected_sol["x3"] = lp::mpq(0);
+    expected_sol["x4"] = lp::mpq(15);
+    expected_sol["x5"] = lp::mpq(2);
+    expected_sol["x6"] = lp::mpq(1);
+    expected_sol["x7"] = lp::mpq(1);
+    expected_sol["x8"] = lp::mpq(0);
     solver.find_maximal_solution();
-    lean_assert(solver.get_status() == OPTIMAL);
+    SASSERT(solver.get_status() == OPTIMAL);
     for (auto it : expected_sol) {
-        lean_assert(it.second == solver.get_column_value_by_name(it.first));
+        SASSERT(it.second == solver.get_column_value_by_name(it.first));
     }
 }
 
@@ -1805,7 +1822,7 @@ std::unordered_map<std::string, double> * get_solution_from_glpsol_output(std::s
            return ret;
         }
 
-        lean_assert(split.size() > 3);
+        SASSERT(split.size() > 3);
         (*ret)[split[1]] = atof(split[3].c_str());
     } while (true);
 }
@@ -1817,7 +1834,7 @@ void test_init_U() {
     m(0, 0) = 10; m(0, 1) = 11; m(0, 2) = 12; m(0, 3) = 13; m(0, 4) = 14;
     m(1, 0) = 20; m(1, 1) = 21; m(1, 2) = 22; m(1, 3) = 23; m(1, 5) = 24;
     m(2, 0) = 30; m(2, 1) = 31; m(2, 2) = 32; m(2, 3) = 33; m(2, 6) = 34;
-#ifdef LEAN_DEBUG
+#ifdef Z3DEBUG
     print_matrix(m, std::cout);
 #endif
     vector<unsigned> basis(3);
@@ -1829,7 +1846,7 @@ void test_init_U() {
 
     for (unsigned i = 0; i < 3; i++) {
         for (unsigned j = 0; j < 3; j ++) {
-            lean_assert(m(i, basis[j]) == u(i, j));
+            SASSERT(m(i, basis[j]) == u(i, j));
         }
     }
 
@@ -1857,7 +1874,7 @@ void test_replace_column() {
     for (unsigned column_to_replace = 0;  column_to_replace < m.dimension(); column_to_replace ++) {
         m.replace_column(column_to_replace, w, settings);
         for (unsigned i = 0; i < m.dimension(); i++) {
-            lean_assert(abs(w[i] - m(i, column_to_replace)) < 0.00000001);
+            SASSERT(abs(w[i] - m(i, column_to_replace)) < 0.00000001);
         }
     }
 }
@@ -1961,7 +1978,7 @@ void test_stacked_unsigned() {
     v = 3;
     v = 4;
     v.pop();
-    lean_assert(v == 2);
+    SASSERT(v == 2);
     v ++;
     v++;
     std::cout << "before push v=" << v << std::endl;
@@ -1971,7 +1988,7 @@ void test_stacked_unsigned() {
     v+=1;
     std::cout << "v = " << v << std::endl;
     v.pop(2);
-    lean_assert(v == 4);
+    SASSERT(v == 4);
     const unsigned & rr = v;
     std::cout << rr << std:: endl;
     
@@ -2010,7 +2027,7 @@ void test_stacked_vector() {
 }
 
 void test_stacked_set() {
-#ifdef LEAN_DEBUG
+#ifdef Z3DEBUG
     std::cout << "test_stacked_set" << std::endl;
     stacked_unordered_set<int> s;
     s.insert(1);
@@ -2020,7 +2037,7 @@ void test_stacked_set() {
     s.push();
     s.insert(4);
     s.pop();
-    lean_assert(s() == scopy);
+    SASSERT(s() == scopy);
     s.push();
     s.push();
     s.insert(4);
@@ -2028,7 +2045,7 @@ void test_stacked_set() {
     s.push();
     s.insert(4);
     s.pop(3);
-    lean_assert(s() == scopy);
+    SASSERT(s() == scopy);
 #endif
 }
 
@@ -2397,15 +2414,15 @@ void test_files_from_directory(std::string test_file_dir, argument_parser & args
 }
 
 
-std::unordered_map<std::string, lean::mpq> get_solution_map(lp_solver<lean::mpq, lean::mpq> * lps, mps_reader<lean::mpq, lean::mpq> & reader) {
-    std::unordered_map<std::string, lean::mpq> ret;
+std::unordered_map<std::string, lp::mpq> get_solution_map(lp_solver<lp::mpq, lp::mpq> * lps, mps_reader<lp::mpq, lp::mpq> & reader) {
+    std::unordered_map<std::string, lp::mpq> ret;
     for (auto it : reader.column_names()) {
         ret[it] = lps->get_column_value_by_name(it);
     }
     return ret;
 }
 
-void run_lar_solver(argument_parser & args_parser, lar_solver * solver, mps_reader<lean::mpq, lean::mpq> * reader) {
+void run_lar_solver(argument_parser & args_parser, lar_solver * solver, mps_reader<lp::mpq, lp::mpq> * reader) {
     std::string maxng = args_parser.get_option_value("--maxng");
     if (maxng.size() > 0) {
         solver->settings().max_number_of_iterations_with_no_improvements = atoi(maxng.c_str());
@@ -2425,7 +2442,7 @@ void run_lar_solver(argument_parser & args_parser, lar_solver * solver, mps_read
         }
         auto * lps = reader->create_solver(false);
         lps->find_maximal_solution();
-        std::unordered_map<std::string, lean::mpq> sol = get_solution_map(lps, *reader);
+        std::unordered_map<std::string, lp::mpq> sol = get_solution_map(lps, *reader);
         std::cout << "status = " << lp_status_to_string(solver->get_status()) <<  std::endl;
         return;
     }
@@ -2434,7 +2451,7 @@ void run_lar_solver(argument_parser & args_parser, lar_solver * solver, mps_read
     lp_status status = solver->solve();
     std::cout << "status is " <<  lp_status_to_string(status) << ", processed for " << sw.get_current_seconds() <<" seconds, and " << solver->get_total_iterations() << " iterations" << std::endl;
     if (solver->get_status() == INFEASIBLE) {
-        vector<std::pair<lean::mpq, constraint_index>> evidence;
+        vector<std::pair<lp::mpq, constraint_index>> evidence;
         solver->get_infeasibility_explanation(evidence);
     }
     if (args_parser.option_is_used("--randomize_lar")) {
@@ -2467,7 +2484,7 @@ lar_solver * create_lar_solver_from_file(std::string file_name, argument_parser
         }
         return reader.create_lar_solver();
     }
-    mps_reader<lean::mpq, lean::mpq> reader(file_name);
+    mps_reader<lp::mpq, lp::mpq> reader(file_name);
     reader.read();
     if (!reader.is_ok()) {
         std::cout << "cannot process " << file_name << std::endl;
@@ -2478,8 +2495,8 @@ lar_solver * create_lar_solver_from_file(std::string file_name, argument_parser
 
 void test_lar_on_file(std::string file_name, argument_parser & args_parser) {
     lar_solver * solver = create_lar_solver_from_file(file_name, args_parser);
-    mps_reader<lean::mpq, lean::mpq> reader(file_name);
-    mps_reader<lean::mpq, lean::mpq> * mps_reader = nullptr;
+    mps_reader<lp::mpq, lp::mpq> reader(file_name);
+    mps_reader<lp::mpq, lp::mpq> * mps_reader = nullptr;
     reader.read();
     if (reader.is_ok()) {
         mps_reader = & reader;
@@ -2524,28 +2541,28 @@ void test_lar_solver(argument_parser & args_parser) {
 }
 
 void test_numeric_pair() {
-    numeric_pair<lean::mpq> a;
-    numeric_pair<lean::mpq> b(2, lean::mpq(6, 2));
+    numeric_pair<lp::mpq> a;
+    numeric_pair<lp::mpq> b(2, lp::mpq(6, 2));
     a = b;
-    numeric_pair<lean::mpq> c(0.1, 0.5);
+    numeric_pair<lp::mpq> c(0.1, 0.5);
     a += 2*c;
     a -= c;
-    lean_assert (a == b + c);
-    numeric_pair<lean::mpq> d = a * 2;
+    SASSERT (a == b + c);
+    numeric_pair<lp::mpq> d = a * 2;
     std::cout << a  << std::endl;
-    lean_assert(b == b);
-    lean_assert(b < a);
-    lean_assert(b <= a);
-    lean_assert(a > b);
-    lean_assert(a != b);
-    lean_assert(a >= b);
-    lean_assert(-a < b);
-    lean_assert(a < 2 * b);
-    lean_assert(b + b > a);
-    lean_assert(lean::mpq(2.1) * b + b > a);
-    lean_assert(-b * lean::mpq(2.1) - b < lean::mpq(0.99)  * a);
-    std::cout << - b * lean::mpq(2.1) - b << std::endl;
-    lean_assert(-b *(lean::mpq(2.1) + 1) == - b * lean::mpq(2.1) - b);
+    SASSERT(b == b);
+    SASSERT(b < a);
+    SASSERT(b <= a);
+    SASSERT(a > b);
+    SASSERT(a != b);
+    SASSERT(a >= b);
+    SASSERT(-a < b);
+    SASSERT(a < 2 * b);
+    SASSERT(b + b > a);
+    SASSERT(lp::mpq(2.1) * b + b > a);
+    SASSERT(-b * lp::mpq(2.1) - b < lp::mpq(0.99)  * a);
+    std::cout << - b * lp::mpq(2.1) - b << std::endl;
+    SASSERT(-b *(lp::mpq(2.1) + 1) == - b * lp::mpq(2.1) - b);
 }
 
 void get_matrix_dimensions(std::ifstream & f, unsigned & m, unsigned & n) {
@@ -2566,7 +2583,7 @@ void read_row_cols(unsigned i, static_matrix<double, double>& A, std::ifstream &
         if (line== "row_end")
             break;
         auto r = split_and_trim(line);
-        lean_assert(r.size() == 4);
+        SASSERT(r.size() == 4);
         unsigned j = atoi(r[1].c_str());
         double v = atof(r[3].c_str());
         A.set(i, j, v);
@@ -2594,7 +2611,7 @@ void read_basis(vector<unsigned> & basis, std::ifstream & f) {
     std::cout << "reading basis" << std::endl;
     std::string line;
     getline(f, line);
-    lean_assert(line == "basis_start");
+    SASSERT(line == "basis_start");
     do {
         getline(f, line);
         if (line == "basis_end")
@@ -2607,7 +2624,7 @@ void read_basis(vector<unsigned> & basis, std::ifstream & f) {
 void read_indexed_vector(indexed_vector<double> & v, std::ifstream & f) {
     std::string line;
     getline(f, line);
-    lean_assert(line == "vector_start");
+    SASSERT(line == "vector_start");
     do {
         getline(f, line);
         if (line == "vector_end") break;
@@ -2641,13 +2658,13 @@ void check_lu_from_file(std::string lufile_name) {
      indexed_vector<double>  d(A.row_count());
     unsigned entering = 26;
     lsuhl.solve_Bd(entering, d, v);
-#ifdef LEAN_DEBUG
+#ifdef Z3DEBUG
     auto B = get_B(lsuhl, basis);
     vector<double>  a(m);
     A.copy_column_to_vector(entering, a);
     indexed_vector<double> cd(d);
     B.apply_from_left(cd.m_data, settings);
-    lean_assert(vectors_are_equal(cd.m_data , a));
+    SASSERT(vectors_are_equal(cd.m_data , a));
 #endif
 }
 
@@ -2662,7 +2679,7 @@ void test_square_dense_submatrix() {
     for (unsigned i = index_start; i < parent_dim; i++)
         for (unsigned j = index_start; j < parent_dim; j++)
             d[i][j] = i*3+j*2;
-#ifdef LEAN_DEBUG
+#ifdef Z3DEBUG
     unsigned dim = parent_dim - index_start;
     dense_matrix<double, double> m(dim, dim);
     for (unsigned i = index_start; i < parent_dim; i++)
@@ -2673,7 +2690,7 @@ void test_square_dense_submatrix() {
     for (unsigned i = index_start; i < parent_dim; i++)
         for (unsigned j = index_start; j < parent_dim; j++)
             d[i][j] = d[j][i];
-#ifdef LEAN_DEBUG
+#ifdef Z3DEBUG
     for (unsigned i = index_start; i < parent_dim; i++)
         for (unsigned j = index_start; j < parent_dim; j++)
             m[i-index_start][j-index_start] = d[i][j];
@@ -2738,7 +2755,7 @@ void test_evidence_for_total_inf_simple(argument_parser & args_parser) {
     auto status = solver.solve();
     std::cout << lp_status_to_string(status) << std::endl;
     std::unordered_map<var_index, mpq> model;
-    lean_assert(solver.get_status() == INFEASIBLE);
+    SASSERT(solver.get_status() == INFEASIBLE);
 }
 void test_bound_propagation_one_small_sample1() {
     /*
@@ -2934,8 +2951,8 @@ void test_total_case_l(){
     ls.solve();
     lp_bound_propagator bp(ls);
     ls.propagate_bounds_for_touched_rows(bp);
-    lean_assert(ev.size() == 4);
-    lean_assert(contains_j_kind(x, GE, - one_of_type<mpq>(), ev));
+    SASSERT(ev.size() == 4);
+    SASSERT(contains_j_kind(x, GE, - one_of_type<mpq>(), ev));
 }
 void test_bound_propagation() {
     test_total_case_u();
@@ -2955,17 +2972,17 @@ void test_int_set() {
     s.insert(1);
     s.insert(2);
     s.print(std::cout);
-    lean_assert(s.contains(2));
-    lean_assert(s.size() == 2);
+    SASSERT(s.contains(2));
+    SASSERT(s.size() == 2);
     s.erase(2);
-    lean_assert(s.size() == 1);
+    SASSERT(s.size() == 1);
     s.erase(2);
-    lean_assert(s.size() == 1);
+    SASSERT(s.size() == 1);
     s.print(std::cout);
     s.insert(3);
     s.insert(2);
     s.clear();
-    lean_assert(s.size() == 0);
+    SASSERT(s.size() == 0);
     
     
 }
@@ -3112,7 +3129,7 @@ void test_lp_local(int argn, char**argv) {
         return finalize(0);
     }
 
-#ifdef LEAN_DEBUG
+#ifdef Z3DEBUG
     if (args_parser.option_is_used("--test_swaps")) {
         sparse_matrix<double, double> m(10);
         fill_matrix(m);
@@ -3142,7 +3159,7 @@ void test_lp_local(int argn, char**argv) {
         return finalize(ret);
     }
 
-#ifdef LEAN_DEBUG
+#ifdef Z3DEBUG
     lp_settings settings;
     update_settings(args_parser, settings);
     if (args_parser.option_is_used("--test_lu")) {
@@ -3219,11 +3236,11 @@ void test_lp_local(int argn, char**argv) {
         ret = 0;
         return finalize(ret);
     }
-    //  lean::ccc = 0;
+    //  lp::ccc = 0;
     return finalize(0);
     test_init_U();
     test_replace_column();
-#ifdef LEAN_DEBUG
+#ifdef Z3DEBUG
     sparse_matrix_with_permutaions_test();
     test_dense_matrix();
     test_swap_operations();
@@ -3236,5 +3253,5 @@ void test_lp_local(int argn, char**argv) {
 }
 }
 void tst_lp(char ** argv, int argc, int& i) {
-    lean::test_lp_local(argc - 2, argv + 2);
+    lp::test_lp_local(argc - 2, argv + 2);
 }
diff --git a/src/test/smt_reader.h b/src/test/smt_reader.h
index 38e3f4157..437cb7a6b 100644
--- a/src/test/smt_reader.h
+++ b/src/test/smt_reader.h
@@ -1,9 +1,22 @@
-/*
-  Copyright (c) 2013 Microsoft Corporation. All rights reserved.
-  Released under Apache 2.0 license as described in the file LICENSE.
+/*++
+Copyright (c) 2017 Microsoft Corporation
 
-  Author: Lev Nachmanson
-*/
+Module Name:
+
+    <name>
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Lev Nachmanson (levnach)
+
+Revision History:
+
+
+--*/
 
 #pragma once
 
@@ -23,7 +36,7 @@
 #include "util/lp/lar_constraints.h"
 #include <sstream>
 #include <cstdlib>
-namespace lean {
+namespace lp {
 
     template<typename T>
     T from_string(const std::string& str) {
@@ -108,13 +121,13 @@ namespace lean {
 
         void fill_simple_elem(lisp_elem & lm) {
             int separator = first_separator();
-            lean_assert(-1 != separator && separator != 0);
+            SASSERT(-1 != separator && separator != 0);
             lm.m_head = m_line.substr(0, separator);
             m_line = m_line.substr(separator);
         }
 
         void fill_nested_elem(lisp_elem & lm) {
-            lean_assert(m_line[0] == '(');
+            SASSERT(m_line[0] == '(');
             m_line = m_line.substr(1);
             int separator = first_separator();
             lm.m_head = m_line.substr(0, separator);
@@ -181,11 +194,11 @@ namespace lean {
         }
 
         void adjust_rigth_side(formula_constraint & /* c*/, lisp_elem & /*el*/) {
-            // lean_assert(el.m_head == "0"); // do nothing for the time being
+            // SASSERT(el.m_head == "0"); // do nothing for the time being
         }
 
         void set_constraint_coeffs(formula_constraint & c, lisp_elem & el) {
-            lean_assert(el.m_elems.size() == 2);
+            SASSERT(el.m_elems.size() == 2);
             set_constraint_coeffs_on_coeff_element(c, el.m_elems[0]);
             adjust_rigth_side(c, el.m_elems[1]);
         }
@@ -201,7 +214,7 @@ namespace lean {
                 add_mult_elem(c, el.m_elems);
             } else if (el.m_head == "~") {
                 lisp_elem & minel = el.m_elems[0];
-                lean_assert(minel.is_simple());
+                SASSERT(minel.is_simple());
                 c.m_right_side += mpq(str_to_int(minel.m_head));
             } else {
                 std::cout << "unexpected input " << el.m_head << std::endl;
@@ -211,14 +224,14 @@ namespace lean {
         }
 
         std::string get_name(lisp_elem & name) {
-            lean_assert(name.is_simple());
-            lean_assert(!is_integer(name.m_head));
+            SASSERT(name.is_simple());
+            SASSERT(!is_integer(name.m_head));
             return name.m_head;
         }
 
 
         void add_mult_elem(formula_constraint & c, std::vector<lisp_elem> & els) {
-            lean_assert(els.size() == 2);
+            SASSERT(els.size() == 2);
             mpq coeff = get_coeff(els[0]);
             std::string col_name = get_name(els[1]);
             c.add_pair(coeff, col_name);
@@ -228,16 +241,16 @@ namespace lean {
             if (le.is_simple()) {
                 return mpq(str_to_int(le.m_head));
             } else {
-                lean_assert(le.m_head == "~");
-                lean_assert(le.size() == 1);
+                SASSERT(le.m_head == "~");
+                SASSERT(le.size() == 1);
                 lisp_elem & el = le.m_elems[0];
-                lean_assert(el.is_simple());
+                SASSERT(el.is_simple());
                 return -mpq(str_to_int(el.m_head));
             }
         }
 
         int str_to_int(std::string & s) {
-            lean_assert(is_integer(s));
+            SASSERT(is_integer(s));
             return atoi(s.c_str());
         }
 
@@ -245,7 +258,7 @@ namespace lean {
             if (el.size()) {
                 add_complex_sum_elem(c, el);
             } else {
-                lean_assert(is_integer(el.m_head));
+                SASSERT(is_integer(el.m_head));
                 int v = atoi(el.m_head.c_str());
                 mpq vr(v);
                 c.m_right_side -= vr;
@@ -263,7 +276,7 @@ namespace lean {
             } else if (el.m_head == "+") {
                 add_sum(c, el.m_elems);
             } else {
-                lean_assert(false); // unexpected input
+                SASSERT(false); // unexpected input
             }
         }
 
diff --git a/src/test/test_file_reader.h b/src/test/test_file_reader.h
index c7a9e3b8b..74dad419b 100644
--- a/src/test/test_file_reader.h
+++ b/src/test/test_file_reader.h
@@ -1,9 +1,23 @@
-/*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
+/*++
+Copyright (c) 2017 Microsoft Corporation
+
+Module Name:
+
+    <name>
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Lev Nachmanson (levnach)
+
+Revision History:
+
+
+--*/
 
-Author: Lev Nachmanson
-*/
 #pragma once
 
 // reads a text file
@@ -15,7 +29,7 @@ Author: Lev Nachmanson
 #include "util/lp/lp_utils.h"
 #include "util/lp/lp_solver.h"
 
-namespace lean {
+namespace lp {
 
 template <typename T>
 struct test_result {