diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index e04db2e57e..75c3541b54 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -502,8 +502,6 @@ function(add_exec_test name tgt)
 endfunction()
 
 add_subdirectory(tests/util)
-add_subdirectory(tests/kernel)
-add_subdirectory(tests/library)
 
 # Include style check
 if (NOT(${CMAKE_SYSTEM_NAME} MATCHES "Windows") AND PYTHONINTERP_FOUND)
diff --git a/src/tests/kernel/CMakeLists.txt b/src/tests/kernel/CMakeLists.txt
deleted file mode 100644
index 1e55298487..0000000000
--- a/src/tests/kernel/CMakeLists.txt
+++ /dev/null
@@ -1,6 +0,0 @@
-add_executable(level level.cpp)
-target_link_libraries(level leanstatic)
-add_exec_test(level "level")
-add_executable(max_sharing max_sharing.cpp)
-target_link_libraries(max_sharing leanstatic)
-add_exec_test(max_sharing "max_sharing")
diff --git a/src/tests/kernel/level.cpp b/src/tests/kernel/level.cpp
deleted file mode 100644
index ccce32ecc1..0000000000
--- a/src/tests/kernel/level.cpp
+++ /dev/null
@@ -1,82 +0,0 @@
-/*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include <locale>
-#include "runtime/exception.h"
-#include "util/test.h"
-#include "util/init_module.h"
-#include "util/sexpr/init_module.h"
-#include "kernel/init_module.h"
-#include "kernel/level.h"
-#include "library/init_module.h"
-using namespace lean;
-
-static void check_serializer(level const & l) {
-    std::ostringstream out;
-    serializer s(out);
-    s << l << l;
-    std::istringstream in(out.str());
-    deserializer d(in);
-    level l1, l2;
-    d >> l1 >> l2;
-    lean_assert_eq(l, l1);
-    lean_assert_eq(l, l2);
-}
-
-static void tst1() {
-    level zero;
-    level one = mk_succ(zero);
-    level two = mk_succ(one);
-    lean_assert(mk_max(one, two) == two);
-    lean_assert(mk_imax(one, two) == two);
-    lean_assert(mk_imax(two, zero) == zero);
-    check_serializer(two);
-    check_serializer(one);
-    level p = mk_univ_param("p");
-    lean_assert(mk_imax(p, zero) == zero);
-    lean_assert(mk_max(zero, p) == p);
-    lean_assert(mk_max(p, zero) == p);
-    lean_assert(mk_max(p, one) != p);
-    check_serializer(mk_max(p, one));
-    check_serializer(mk_imax(p, one));
-    check_serializer(mk_imax(one, p));
-    check_serializer(mk_imax(mk_succ(p), p));
-    std::cout << pp(mk_max(p, mk_max(mk_succ(mk_univ_param("a")), one))) << "\n";
-}
-
-static void tst2() {
-    level zero;
-    level one = mk_succ(zero);
-    level two = mk_succ(one);
-    level p1 = mk_univ_param("p1");
-    level p2 = mk_univ_param("p2");
-    level m1 = mk_univ_mvar("m1");
-    lean_assert(is_equivalent(mk_succ(p2), mk_max(p2, mk_succ(p2))));
-    lean_assert(is_equivalent(mk_max(p1, p2), mk_max(p2, p1)));
-    lean_assert(!is_equivalent(mk_imax(p1, p2), mk_imax(p2, p1)));
-    lean_assert(is_equivalent(mk_imax(mk_succ(p1), mk_succ(p2)), mk_imax(mk_succ(p2), mk_succ(p1))));
-    lean_assert(is_equivalent(mk_succ(mk_max(m1, p1)), mk_max(mk_succ(p1), mk_succ(m1))));
-    lean_assert(is_equivalent(one, mk_succ(zero)));
-    lean_assert(!is_equivalent(zero, two));
-    lean_assert(!is_equivalent(zero, p2));
-}
-
-int main() {
-    save_stack_info();
-    initialize_util_module();
-    initialize_sexpr_module();
-    initialize_kernel_module();
-    initialize_library_core_module();
-    initialize_library_module();
-    tst1();
-    tst2();
-    finalize_library_module();
-    finalize_library_core_module();
-    finalize_kernel_module();
-    finalize_sexpr_module();
-    finalize_util_module();
-    return has_violations() ? 1 : 0;
-}
diff --git a/src/tests/kernel/max_sharing.cpp b/src/tests/kernel/max_sharing.cpp
deleted file mode 100644
index cd5440c160..0000000000
--- a/src/tests/kernel/max_sharing.cpp
+++ /dev/null
@@ -1,82 +0,0 @@
-/*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include <iostream>
-#include "util/test.h"
-#include "util/init_module.h"
-#include "util/sexpr/init_module.h"
-#include "kernel/abstract.h"
-#include "kernel/init_module.h"
-#include "library/init_module.h"
-#include "library/max_sharing.h"
-#include "library/print.h"
-using namespace lean;
-
-static void tst1() {
-    max_sharing_fn max_fn;
-    expr a1 = mk_const("a");
-    expr a2 = mk_const("a");
-    expr N = mk_const("N");
-    expr x = mk_local("x", N);
-    expr y = mk_local("y", N);
-    expr f = mk_const("f");
-    expr F1, F2;
-    F1 = mk_app(f, Fun(x, mk_app(f, x, x)), Fun(y, mk_app(f, y, y)));
-    lean_assert(!is_eqp(app_arg(app_fn(F1)), app_arg(F1)));
-    F2 = max_fn(F1);
-    std::cout << F2 << "\n";
-    lean_assert(!is_eqp(app_arg(app_fn(F2)), app_arg(F2))); // name matter
-    max_fn.clear();
-}
-
-static void tst2() {
-    max_sharing_fn max_fn1;
-    max_sharing_fn max_fn2;
-    expr x   = mk_const("x");
-    expr f   = mk_const("f");
-    expr g   = mk_const("g");
-    expr t1  = max_fn2(max_fn1(mk_app(f, mk_app(g, x))));
-    expr t2  = max_fn2(mk_app(f, t1, mk_app(g, x)));
-    expr arg1 = app_arg(app_arg(app_fn(t2)));
-    expr arg2 = app_arg(t2);
-    lean_assert(is_eqp(arg1, arg2));
-}
-
-static void tst3() {
-    max_sharing_fn max_fn;
-    expr a1 = mk_const("a");
-    expr a2 = mk_const("a");
-    expr a3 = mk_const("a");
-    expr g  = mk_const("g");
-    expr f  = mk_const("f");
-    expr new_a1 = max_fn(a1);
-    lean_assert(is_eqp(new_a1, a1));
-    expr t1 = max_fn(mk_app(f, a2));
-    lean_assert(is_eqp(app_arg(t1), a1));
-    expr t2 = max_fn(mk_app(f, a2));
-    lean_assert(is_eqp(t1, t2));
-    expr t3 = max_fn(mk_app(f, a3));
-    lean_assert(is_eqp(t1, t3));
-}
-
-int main() {
-    save_stack_info();
-    initialize_util_module();
-    initialize_sexpr_module();
-    initialize_kernel_module();
-    initialize_library_core_module();
-    initialize_library_module();
-    init_default_print_fn();
-    tst1();
-    tst2();
-    tst3();
-    finalize_library_module();
-    finalize_library_core_module();
-    finalize_kernel_module();
-    finalize_sexpr_module();
-    finalize_util_module();
-    return has_violations() ? 1 : 0;
-}
diff --git a/src/tests/library/CMakeLists.txt b/src/tests/library/CMakeLists.txt
deleted file mode 100644
index d3ff550309..0000000000
--- a/src/tests/library/CMakeLists.txt
+++ /dev/null
@@ -1,18 +0,0 @@
-add_executable(expr_lt expr_lt.cpp)
-target_link_libraries(expr_lt leanstatic)
-add_exec_test(expr_lt "expr_lt")
-add_executable(deep_copy deep_copy.cpp)
-target_link_libraries(deep_copy leanstatic)
-add_exec_test(deep_copy "deep_copy")
-add_executable(occurs occurs.cpp)
-target_link_libraries(occurs leanstatic)
-add_exec_test(occurs "occurs")
-add_executable(head_map head_map.cpp)
-target_link_libraries(head_map leanstatic)
-add_exec_test(head_map "head_map")
-add_executable(parray parray.cpp)
-target_link_libraries(parray leanstatic)
-add_exec_test(parray "parray")
-add_executable(phashtable phashtable.cpp)
-target_link_libraries(phashtable leanstatic)
-add_exec_test(phashtable "phashtable")
diff --git a/src/tests/library/deep_copy.cpp b/src/tests/library/deep_copy.cpp
deleted file mode 100644
index 8e14a46b58..0000000000
--- a/src/tests/library/deep_copy.cpp
+++ /dev/null
@@ -1,45 +0,0 @@
-/*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include "util/test.h"
-#include "util/init_module.h"
-#include "util/sexpr/init_module.h"
-#include "kernel/for_each_fn.h"
-#include "kernel/abstract.h"
-#include "kernel/init_module.h"
-#include "library/init_module.h"
-#include "library/deep_copy.h"
-using namespace lean;
-
-static void tst1() {
-    expr f = mk_const("f");
-    expr a = mk_const("a");
-    expr x = mk_bvar(0);
-    expr Type = mk_Type();
-    expr t = Type;
-    expr z = mk_const("z");
-    expr m = mk_metavar("a", Type);
-    expr F = mk_pi("y", t, mk_lambda("x", t, mk_app(f, mk_app(f, mk_app(f, x, a), mk_const("10")), mk_app(f, x, m))));
-    expr G = deep_copy(F);
-    lean_assert(F == G);
-    lean_assert(!is_eqp(F, G));
-}
-
-int main() {
-    save_stack_info();
-    initialize_util_module();
-    initialize_sexpr_module();
-    initialize_kernel_module();
-    initialize_library_core_module();
-    initialize_library_module();
-    tst1();
-    finalize_library_module();
-    finalize_library_core_module();
-    finalize_kernel_module();
-    finalize_sexpr_module();
-    finalize_util_module();
-    return has_violations() ? 1 : 0;
-}
diff --git a/src/tests/library/expr_lt.cpp b/src/tests/library/expr_lt.cpp
deleted file mode 100644
index 993fe7ee3d..0000000000
--- a/src/tests/library/expr_lt.cpp
+++ /dev/null
@@ -1,41 +0,0 @@
-/*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include "util/test.h"
-#include "kernel/abstract.h"
-#include "library/expr_lt.h"
-#include "util/init_module.h"
-using namespace lean;
-
-static void lt(expr const & e1, expr const & e2, bool expected) {
-    lean_assert(is_lt(e1, e2, false) == expected);
-    lean_assert(is_lt(e1, e2, false) == !(e1 == e2 || (is_lt(e2, e1, false))));
-}
-
-static void tst1() {
-    lt(mk_bvar(0), mk_bvar(0), false);
-    lt(mk_bvar(0), mk_bvar(1), true);
-    lt(mk_const("a"), mk_const("b"), true);
-    lt(mk_const("a"), mk_const("a"), false);
-    lt(mk_bvar(1), mk_const("a"), true);
-    lt(mk_app(mk_const("f"), mk_bvar(0)), mk_app(mk_const("f"), mk_bvar(0), mk_const("a")), true);
-    lt(mk_app(mk_const("f"), mk_bvar(0), mk_const("a"), mk_const("b")), mk_app(mk_const("f"), mk_bvar(0), mk_const("a")), false);
-    lt(mk_app(mk_const("f"), mk_bvar(0), mk_const("a")), mk_app(mk_const("g"), mk_bvar(0), mk_const("a")), true);
-    lt(mk_app(mk_const("f"), mk_bvar(0), mk_const("a")), mk_app(mk_const("f"), mk_bvar(1), mk_const("a")), true);
-    lt(mk_app(mk_const("f"), mk_bvar(0), mk_const("a")), mk_app(mk_const("f"), mk_bvar(0), mk_const("b")), true);
-    lt(mk_app(mk_const("f"), mk_bvar(0), mk_const("a")), mk_app(mk_const("f"), mk_bvar(0), mk_const("a")), false);
-    lt(mk_app(mk_const("g"), mk_bvar(0), mk_const("a")), mk_app(mk_const("f"), mk_bvar(0), mk_const("a")), false);
-    lt(mk_app(mk_const("f"), mk_bvar(1), mk_const("a")), mk_app(mk_const("f"), mk_bvar(0), mk_const("a")), false);
-    lt(mk_app(mk_const("f"), mk_bvar(0), mk_const("b")), mk_app(mk_const("f"), mk_bvar(0), mk_const("a")), false);
-}
-
-int main() {
-    save_stack_info();
-    initialize_util_module();
-    tst1();
-    finalize_util_module();
-    return has_violations() ? 1 : 0;
-}
diff --git a/src/tests/library/head_map.cpp b/src/tests/library/head_map.cpp
deleted file mode 100644
index 5100854806..0000000000
--- a/src/tests/library/head_map.cpp
+++ /dev/null
@@ -1,74 +0,0 @@
-/*
-Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include "util/test.h"
-#include "util/init_module.h"
-#include "util/sexpr/init_module.h"
-#include "kernel/abstract.h"
-#include "kernel/init_module.h"
-#include "library/init_module.h"
-#include "library/head_map.h"
-using namespace lean;
-
-static void tst1() {
-    head_map<expr> map;
-    expr a = mk_const("a");
-    expr f = mk_const("f");
-    expr b = mk_const("b");
-    expr Prop = mk_Prop();
-    expr x = mk_local("x", Prop);
-    expr l1 = Fun(x, x);
-    expr l2 = Fun(x, mk_app(f, x));
-    lean_assert(l1 != l2);
-    lean_assert(map.empty());
-    map.insert(a, a);
-    lean_assert(map.contains(a));
-    map.insert(a, b);
-    lean_assert(map.contains(a));
-    map.erase(a, b);
-    lean_assert(map.contains(a));
-    map.erase(a, a);
-    lean_assert(!map.contains(a));
-    lean_assert(map.empty());
-    map.insert(l1, a);
-    map.insert(l2, b);
-    lean_assert(map.contains(l1));
-    lean_assert(length(*map.find(l1)) == 2);
-    auto size_fn = [](head_map<expr> const & m) {
-        unsigned r = 0;
-        m.for_each_entry([&](head_index const &, expr const &) { r++; });
-        return r;
-    };
-    lean_assert(size_fn(map) == 2);
-    map.insert(a, a);
-    lean_assert(size_fn(map) == 3);
-    map.erase(l1);
-    lean_assert(size_fn(map) == 1);
-    map.insert(a, b);
-    lean_assert(size_fn(map) == 2);
-    map.erase(a);
-    lean_assert(size_fn(map) == 0);
-    lean_assert(map.empty());
-    map.insert(mk_app(f, a), mk_app(f, a));
-    map.insert(mk_app(f, b), mk_app(f, b));
-    lean_assert(length(*map.find(mk_app(f, a))) == 2);
-}
-
-int main() {
-    save_stack_info();
-    initialize_util_module();
-    initialize_sexpr_module();
-    initialize_kernel_module();
-    initialize_library_core_module();
-    initialize_library_module();
-    tst1();
-    finalize_library_module();
-    finalize_library_core_module();
-    finalize_kernel_module();
-    finalize_sexpr_module();
-    finalize_util_module();
-    return has_violations() ? 1 : 0;
-}
diff --git a/src/tests/library/occurs.cpp b/src/tests/library/occurs.cpp
deleted file mode 100644
index d9e22e6c8e..0000000000
--- a/src/tests/library/occurs.cpp
+++ /dev/null
@@ -1,45 +0,0 @@
-/*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include "util/test.h"
-#include "util/init_module.h"
-#include "util/sexpr/init_module.h"
-#include "kernel/abstract.h"
-#include "library/util.h"
-#include "kernel/init_module.h"
-#include "library/init_module.h"
-using namespace lean;
-
-static void tst1() {
-    expr f = mk_const("f");
-    expr a = mk_const("a");
-    expr b = mk_const("b");
-    expr Type = mk_Type();
-    expr T = Type;
-    expr a1 = mk_local("a", T);
-    lean_assert(occurs(f, f));
-    lean_assert(!occurs(a, f));
-    lean_assert(occurs(a, mk_app(f, a)));
-    lean_assert(occurs("a", mk_app(f, a)));
-    lean_assert(!occurs("b", f));
-    lean_assert(!occurs(a, Fun(a1, mk_app(f, a1))));
-}
-
-int main() {
-    save_stack_info();
-    initialize_util_module();
-    initialize_sexpr_module();
-    initialize_kernel_module();
-    initialize_library_core_module();
-    initialize_library_module();
-    tst1();
-    finalize_library_module();
-    finalize_library_core_module();
-    finalize_kernel_module();
-    finalize_sexpr_module();
-    finalize_util_module();
-    return has_violations() ? 1 : 0;
-}
diff --git a/src/tests/library/parray.cpp b/src/tests/library/parray.cpp
deleted file mode 100644
index 6c24ffb0fa..0000000000
--- a/src/tests/library/parray.cpp
+++ /dev/null
@@ -1,196 +0,0 @@
-/*
-Copyright (c) 2017 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include <utility>
-#include <random>
-#include <vector>
-#include "util/test.h"
-#include "util/init_module.h"
-#include "util/sexpr/init_module.h"
-#include "kernel/init_module.h"
-#include "library/init_module.h"
-#include "library/parray.h"
-using namespace lean;
-
-void tst1() {
-    parray<unsigned> a(10, 0);
-    lean_assert(a[0] == 0);
-    lean_assert(a.size() == 10);
-    parray<unsigned> b = a;
-    a.set(0, 1);
-    lean_assert(a[0] == 1);
-    lean_assert(a[1] == 0);
-    lean_assert(b[0] == 0);
-    lean_assert(a[0] == 1);
-}
-
-void driver(unsigned max_sz, unsigned max_val, unsigned num_it,
-            double push_back_freq,
-            double pop_back_freq,
-            double set_freq,
-            double copy_freq) {
-    parray<unsigned> v1;
-    std::vector<unsigned> v2;
-    std::mt19937   rng;
-    rng.seed(static_cast<unsigned int>(time(0)));
-    std::uniform_int_distribution<unsigned int> uint_dist;
-    std::vector<std::pair<parray<unsigned>, std::vector<unsigned>>> copies;
-    size_t acc_sz = 0;
-    for (unsigned i = 0; i < num_it; i++) {
-        acc_sz += v1.size();
-        double f = static_cast<double>(uint_dist(rng) % 10000) / 10000.0;
-        if (f < copy_freq) {
-            copies.emplace_back(v1, v2);
-        }
-        f = static_cast<double>(uint_dist(rng) % 10000) / 10000.0;
-        if (f < push_back_freq) {
-            if (v1.size() < max_sz) {
-                unsigned a = uint_dist(rng) % max_val;
-                v1.push_back(a);
-                v2.push_back(a);
-            }
-        }
-        if (v1.size() > 0) {
-            f = static_cast<double>(uint_dist(rng) % 10000) / 10000.0;
-            if (f < pop_back_freq) {
-                if (v1.size() >= max_sz)
-                    continue;
-                v1.pop_back();
-                v2.pop_back();
-            }
-        }
-        if (v1.size() > 0) {
-            f = static_cast<double>(uint_dist(rng) % 10000) / 10000.0;
-            if (f < set_freq) {
-                unsigned idx = uint_dist(rng) % v1.size();
-                unsigned a   = uint_dist(rng) % max_val;
-                v1.set(idx, a);
-                v2[idx] = a;
-            }
-        }
-        f = static_cast<double>(uint_dist(rng) % 10000) / 10000.0;
-        lean_assert(v1.size() == v2.size());
-        for (unsigned i = 0; i < v2.size(); i++) {
-            lean_assert(v1[i] == v2[i]);
-        }
-    }
-    for (std::pair<parray<unsigned>, std::vector<unsigned>> const & p : copies) {
-        lean_assert(p.first.size() == p.second.size());
-        for (unsigned i = 0; i < p.second.size(); i++) {
-            lean_assert(p.first[i] == p.second[i]);
-        }
-    }
-    std::cout << "\n";
-    std::cout << "Copies created:  " << copies.size() << "\n";
-    std::cout << "Average size:    " << static_cast<double>(acc_sz) / static_cast<double>(num_it) << "\n";
-}
-
-static void tst2() {
-    driver(4,  32, 10000, 0.5, 0.1, 0.5, 0.1);
-    driver(4,  32, 10000, 0.5, 0.1, 0.5, 0.1);
-    driver(4,  32, 10000, 0.5, 0.1, 0.5, 0.5);
-    driver(16, 16, 100000, 0.5, 0.5, 0.5, 0.01);
-    driver(16, 16, 100000, 0.5, 0.1, 0.5, 0.01);
-    driver(16, 16, 100000, 0.5, 0.6, 0.5, 0.01);
-    driver(16, 16, 10000, 0.5, 0.1, 0.5, 0.0);
-}
-
-static void tst3(unsigned n) {
-    parray<unsigned> v1;
-    v1.push_back(0);
-    parray<unsigned> v2 = v1;
-    for (unsigned i = 0; i < n; i++)
-        v1.push_back(i);
-    unsigned r = 0;
-    for (unsigned i = 0; i < n; i++)
-        r += v1[n - i - 1];
-    std::cout << ">> " << r << "\n";
-}
-
-static void tst_perf(unsigned sz, unsigned num_updates, unsigned num_iter, bool unshare) {
-    parray<unsigned> v1(sz, 0);
-    parray<unsigned> v2 = v1;
-    for (unsigned i = 0; i < num_updates; i++) {
-        v1.set(i, i);
-    }
-    if (unshare) {
-        /* The following loop is very expensive without ensure_unshared */
-        v1.ensure_unshared();
-    }
-    for (unsigned i = 0; i < num_iter; i++) {
-        unsigned u1 = v1[i];
-        unsigned u2 = v2[i];
-        lean_assert(u1 == i);
-        lean_assert(u2 == 0);
-    }
-}
-
-class Foo {
-    unsigned * m_data;
-public:
-    Foo():m_data(new unsigned(1)) {}
-    Foo(Foo const & src):m_data(new unsigned(*src.m_data)) {}
-    Foo(Foo && src):m_data(new unsigned(*src.m_data)) {}
-    Foo(unsigned n):m_data(new unsigned(n)) {}
-    ~Foo() { delete m_data; }
-
-    Foo & operator=(Foo const & src) {
-        *m_data = *src.m_data;
-        return *this;
-    }
-
-    Foo & operator=(Foo const && src) {
-        *m_data = *src.m_data;
-        return *this;
-    }
-
-    unsigned get_val() const { return *m_data; }
-};
-
-static void tst4() {
-    parray<Foo> v1;
-    v1.push_back(Foo(2));
-    v1.push_back(Foo(3));
-    parray<Foo> v2 = v1;
-    for (unsigned i = 0; i < 10; i++)
-        v1.push_back(Foo(i));
-    v1.set(0, Foo(100));
-    v1.set(1, Foo(100));
-    lean_assert(v2.size() == 2);
-    lean_assert(v2[0].get_val() == 2);
-    lean_assert(v2[1].get_val() == 3);
-    parray<Foo> v3 = v1;
-    v1.pop_back();
-    v1.pop_back();
-    lean_assert(v1.size() == 10);
-    lean_assert(v3.size() == 12);
-}
-
-int main() {
-    save_stack_info();
-    initialize_util_module();
-    initialize_sexpr_module();
-    initialize_kernel_module();
-    initialize_library_core_module();
-    initialize_library_module();
-
-    tst1();
-    tst2();
-    tst3(100000);
-    tst4();
-    tst_perf(100000, 100000, 10000, true);
-    tst_perf(100000, 100000, 10000, false);
-    tst_perf(100000, 10000, 10000, true);
-    // The following test is slow (as expected) because it will not split the path.
-    // tst_perf(100000, 10000, 10000, false);
-
-    finalize_library_module();
-    finalize_library_core_module();
-    finalize_kernel_module();
-    finalize_sexpr_module();
-    finalize_util_module();
-    return has_violations() ? 1 : 0;
-}
diff --git a/src/tests/library/phashtable.cpp b/src/tests/library/phashtable.cpp
deleted file mode 100644
index 65df36840e..0000000000
--- a/src/tests/library/phashtable.cpp
+++ /dev/null
@@ -1,275 +0,0 @@
-/*
-Copyright (c) 2017 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include <utility>
-#include <random>
-#include <vector>
-#include <functional>
-#include <unordered_set>
-#include "util/test.h"
-#include "util/timeit.h"
-#include "util/init_module.h"
-#include "util/rb_map.h"
-#include "util/sexpr/init_module.h"
-#include "kernel/init_module.h"
-#include "library/init_module.h"
-#include "library/phashtable.h"
-#include "library/phash_map.h"
-using namespace lean;
-
-typedef phashtable<unsigned, std::hash<unsigned>, std::equal_to<unsigned>, true> unsigned_set;
-typedef std::unordered_set<unsigned, std::hash<unsigned>> std_unsigned_set;
-
-void tst1() {
-    unsigned_set s;
-    lean_assert(s.size() == 0);
-    s.insert(10);
-    s.for_each([](unsigned v) {
-            lean_assert(v == 10);
-        });
-    lean_assert(s.contains(10));
-    lean_assert(!s.contains(20));
-    lean_assert(s.find(10));
-    auto v = s.find(10);
-    lean_assert(v && *v == 10);
-    lean_assert(!s.find(20));
-    s.erase(20);
-    lean_assert(s.check_invariant());
-    lean_assert(s.contains(10));
-    s.erase(10);
-    lean_assert(!s.contains(10));
-    lean_assert(s.check_invariant());
-}
-
-static void tst2() {
-    std::uniform_int_distribution<unsigned int> uint_dist;
-    std::mt19937   rng;
-    rng.seed(static_cast<unsigned int>(time(0)));
-    const unsigned N = 10000;
-    unsigned vals[N];
-    unsigned_set s1;
-    for (unsigned i = 1; i < N; i ++) {
-        unsigned v = uint_dist(rng) % (N / 2);
-        s1.insert(v);
-        vals[i] = v;
-        lean_assert(s1.contains(v));
-    }
-    std::cout << "step1\n"; std::cout.flush();
-    for (unsigned i = 1; i < N; i ++) {
-        lean_assert(s1.contains(vals[i]));
-    }
-    std::cout << "step2\n"; std::cout.flush();
-    for (unsigned i = 1; i < N; i += 2) {
-        s1.erase(vals[i]);
-        lean_assert(!s1.contains(vals[i]));
-    }
-    std::cout << "step3\n"; std::cout.flush();
-    for (unsigned i = 1; i < N; i += 2) {
-        s1.insert(vals[i]);
-    }
-    std::cout << "step4\n"; std::cout.flush();
-    for (unsigned i = 1; i < N; i ++) {
-        lean_assert(s1.contains(vals[i]));
-    }
-}
-
-static void tst3() {
-    std::uniform_int_distribution<unsigned int> uint_dist;
-    std::mt19937   rng;
-    rng.seed(static_cast<unsigned int>(time(0)));
-    unsigned_set     s1;
-    std_unsigned_set s2;
-    unsigned N = uint_dist(rng) % 1000;
-    for (unsigned i = 0; i < N; i++) {
-        unsigned v = uint_dist(rng)%1000;
-        if (uint_dist(rng) % 3 == 2) {
-            s1.erase(v);
-            s2.erase(v);
-            lean_assert(!s1.contains(v));
-        } else {
-            s1.insert(v);
-            s2.insert(v);
-            lean_assert(s1.contains(v));
-        }
-    }
-    {
-        std_unsigned_set::iterator it  = s2.begin();
-        std_unsigned_set::iterator end = s2.end();
-        for (; it != end; ++it) {
-            lean_assert(s1.contains(*it));
-        }
-    }
-    {
-        unsigned n = 0;
-        s1.for_each([&](unsigned v) {
-                lean_assert(s2.find(v) != s2.end());
-                n++;
-            });
-        lean_assert(n == s1.size());
-    }
-    lean_assert(s1.size() == s2.size());
-}
-
-static void tst4() {
-    unsigned_set s1;
-    s1.insert(10);
-    s1.insert(20);
-    unsigned_set s2 = s1;
-    lean_assert(s2.contains(10));
-    lean_assert(s2.contains(20));
-    lean_assert(!s2.contains(30));
-    s2.insert(30);
-    lean_assert(s2.contains(30));
-    lean_assert(!s1.contains(30));
-}
-
-static void tst5() {
-    /* This example would take a few minute if we use std_unsigned_set.
-       With unsigned_set, it takes a few milliseconds. */
-    timeit timer(std::cout, "tst5");
-    unsigned_set s1;
-    for (unsigned i = 0; i < 100000; i++) {
-        s1.insert(i);
-    }
-    for (unsigned i = 0; i < 100000; i++) {
-        unsigned_set s2 = s1;
-        s2.insert(99999999);
-        lean_assert(s2.contains(10));
-        lean_assert(s2.contains(99999999));
-    }
-    lean_assert(!s1.contains(99999999));
-}
-
-typedef phash_map<unsigned, unsigned, std::hash<unsigned>, std::equal_to<unsigned>, true> umap;
-
-static void tst6() {
-    umap m;
-    m.insert(1, 2);
-    lean_assert(m.contains(1));
-    lean_assert(m.find(1) == optional<unsigned>(2));
-    m.insert(1, 3);
-    lean_assert(m.contains(1));
-    lean_assert(m.find(1) == optional<unsigned>(3));
-    lean_assert(m.contains(1));
-    m.insert(2, 4);
-    m.for_each([](unsigned k, unsigned v) {
-            lean_assert(k == 1 || k == 2);
-            lean_assert(v == 3 || v == 4);
-        });
-    lean_assert(m.size() == 2);
-    lean_assert(m.contains(2));
-    lean_assert(m.contains(1));
-    m.erase(1);
-    lean_assert(!m.contains(1));
-    lean_assert(m.find(2) == optional<unsigned>(4));
-    lean_assert(m.size() == 1);
-}
-
-void tst7(unsigned num, unsigned seed) {
-    timeit t(std::cout, "phash_map + finalization");
-    umap m;
-    {
-        timeit t(std::cout, "phash_map");
-        std::mt19937   rng;
-        rng.seed(seed);
-        std::uniform_int_distribution<unsigned int> uint_dist;
-        for (unsigned i = 0; i < num; i++) {
-            m.insert(uint_dist(rng), uint_dist(rng));
-        }
-    }
-}
-
-void tst8(unsigned num, unsigned seed) {
-    timeit t(std::cout, "phash_map with trail and num/100 snapshots + finalization");
-    umap m;
-    std::vector<umap> snapshots;
-    {
-        timeit t(std::cout, "phash_map with trail and num/100 snapshots");
-        std::mt19937   rng;
-        rng.seed(seed);
-        std::uniform_int_distribution<unsigned int> uint_dist;
-        for (unsigned k = 0; k < 100; k++) {
-            snapshots.push_back(m);
-            for (unsigned i = 0; i < num / 100; i++) {
-                m.insert(uint_dist(rng), uint_dist(rng));
-            }
-        }
-    }
-}
-
-void tst9(unsigned num, unsigned seed) {
-    timeit t(std::cout, "phash_map with trail and 1 snapshot + finalization");
-    umap m;
-    {
-        timeit t(std::cout, "phash_map with trail and 1 snapshot");
-        std::mt19937   rng;
-        rng.seed(seed);
-        std::uniform_int_distribution<unsigned int> uint_dist;
-        m.insert(uint_dist(rng), uint_dist(rng));
-        umap m2 = m;
-        for (unsigned i = 1; i < num; i++) {
-            m.insert(uint_dist(rng), uint_dist(rng));
-        }
-    }
-}
-
-void tst10(unsigned num, unsigned seed) {
-    timeit t(std::cout, "rb_map + finalization");
-    unsigned_map<unsigned> m;
-    {
-        timeit t(std::cout, "rb_map");
-        std::mt19937   rng;
-        rng.seed(seed);
-        std::uniform_int_distribution<unsigned int> uint_dist;
-        for (unsigned i = 0; i < num; i++) {
-            m.insert(uint_dist(rng), uint_dist(rng));
-        }
-    }
-}
-
-void tst11(unsigned num, unsigned seed) {
-    timeit t(std::cout, "unordered_map + finalization");
-    std::unordered_map<unsigned, unsigned, std::hash<unsigned>, std::equal_to<unsigned>> m;
-    {
-        timeit t(std::cout, "unordered_map");
-        std::mt19937   rng;
-        rng.seed(seed);
-        std::uniform_int_distribution<unsigned int> uint_dist;
-        for (unsigned i = 0; i < num; i++) {
-            m.insert(std::make_pair(uint_dist(rng), uint_dist(rng)));
-        }
-    }
-}
-
-int main() {
-    save_stack_info();
-    initialize_util_module();
-    initialize_sexpr_module();
-    initialize_kernel_module();
-    initialize_library_core_module();
-    initialize_library_module();
-
-    tst1();
-    tst2();
-    for (int i = 0; i < 1000; i++)
-        tst3();
-    tst4();
-    tst5();
-    tst6();
-#if 0
-    tst7(10000000, 2);
-    tst8(10000000, 2);
-    tst9(10000000, 2);
-    tst10(10000000, 2);
-    tst11(10000000, 2);
-#endif
-    finalize_library_module();
-    finalize_library_core_module();
-    finalize_kernel_module();
-    finalize_sexpr_module();
-    finalize_util_module();
-    return has_violations() ? 1 : 0;
-}