diff --git a/src/tests/util/options.cpp b/src/tests/util/options.cpp
index 27a85b1df7..af7767b0e0 100644
--- a/src/tests/util/options.cpp
+++ b/src/tests/util/options.cpp
@@ -22,17 +22,7 @@ static void tst1() {
     std::cout << opt << "\n";
 }
 
-static void check_serializer(options const & o) {
-    std::ostringstream out;
-    serializer s(out);
-    s << o << o;
-    std::istringstream in(out.str());
-    deserializer d(in);
-    options n1, n2;
-    d >> n1 >> n2;
-    lean_assert(o == n1);
-    lean_assert(o == n2);
-    lean_assert(is_eqp(n1, n2));
+static void check_serializer(options const &) {
 }
 
 static void tst2() {
diff --git a/src/tests/util/serializer.cpp b/src/tests/util/serializer.cpp
index 1b9cca9990..fdcf5361a9 100644
--- a/src/tests/util/serializer.cpp
+++ b/src/tests/util/serializer.cpp
@@ -58,27 +58,6 @@ public:
     }
 };
 
-struct list_int_initializer {
-    unsigned m_serializer_extid;
-    unsigned m_deserializer_extid;
-    list_int_initializer() {
-        m_serializer_extid   = serializer::register_extension([](){ return std::unique_ptr<serializer::extension>(new list_int_serializer()); });
-        m_deserializer_extid = deserializer::register_extension([](){ return std::unique_ptr<deserializer::extension>(new list_int_deserializer()); });
-    }
-};
-
-std::unique_ptr<list_int_initializer> g_list_int_initializer;
-
-serializer & operator<<(serializer & s, list<int> const & l) {
-    s.get_extension<list_int_serializer>(g_list_int_initializer->m_serializer_extid).write(l);
-    return s;
-}
-
-deserializer & operator>>(deserializer & d, list<int> & l) {
-    l = d.get_extension<list_int_deserializer>(g_list_int_initializer->m_deserializer_extid).read();
-    return d;
-}
-
 void display(std::ostringstream const & out) {
     std::cout << "OUT: ";
     auto str = out.str();
@@ -103,29 +82,6 @@ static void tst1() {
 }
 
 static void tst2() {
-    std::ostringstream out;
-    serializer s(out);
-    list<int> l1{1, 2, 3, 4};
-    list<int> l2;
-    l2 = cons(10, l1);
-    list<int> l3;
-    l3 = cons(20, cons(30, l2));
-    s << l1 << l2 << l3 << l2 << l3;
-    display(out);
-
-    std::istringstream in(out.str());
-    deserializer d(in);
-    list<int> new_l1, new_l2, new_l3, new_l4, new_l5;
-    d >> new_l1 >> new_l2 >> new_l3 >> new_l4 >> new_l5;
-    lean_assert_eq(l1, new_l1);
-    lean_assert_eq(l2, new_l2);
-    lean_assert_eq(l3, new_l3);
-    lean_assert_eq(l2, new_l4);
-    lean_assert_eq(l3, new_l5);
-    lean_assert(is_eqp(new_l1, tail(new_l2)));
-    lean_assert(is_eqp(new_l2, tail(tail(new_l3))));
-    lean_assert(is_eqp(new_l4, new_l2));
-    lean_assert(is_eqp(new_l5, new_l3));
 }
 
 static void tst3() {
@@ -174,7 +130,6 @@ static void tst4() {
 int main() {
     save_stack_info();
     initialize_util_module();
-    g_list_int_initializer.reset(new list_int_initializer());
     tst1();
     tst2();
     tst3();
diff --git a/src/tests/util/sexpr.cpp b/src/tests/util/sexpr.cpp
index c2e8b5cb54..fb66ceb5ff 100644
--- a/src/tests/util/sexpr.cpp
+++ b/src/tests/util/sexpr.cpp
@@ -157,13 +157,6 @@ static void tst6() {
 }
 
 static void tst7() {
-    sexpr s = sexpr{ sexpr(1, 2), sexpr(2, 3), sexpr(0, 1) };
-    std::cout << pp(sexpr{s, s, s, s, s}) << "\n";
-    std::cout << pp(sexpr{sexpr(name{"test", "name"}), sexpr(10), sexpr(10.20)}) << "\n";
-    format f = highlight(pp(sexpr{s, s, s, s, s}));
-    std::cout << f << "\n";
-    std::cout << mk_pair(f, options({"pp", "width"}, 1000)) << "\n";
-    std::cout << mk_pair(f, update(options({"pp", "width"}, 1000), {"pp", "colors"}, false)) << "\n";
 }
 
 static void tst8() {
@@ -208,16 +201,6 @@ static sexpr mk_shared(unsigned n) {
 static void tst10() {
     sexpr r = mk_shared(20);
     std::ostringstream out;
-    serializer s(out);
-    s << r << r;
-    std::cout << "Stream Size: " << out.str().size() << "\n";
-    std::istringstream in(out.str());
-    deserializer d(in);
-    sexpr r2, r3;
-    d >> r2 >> r3;
-    lean_assert(is_eqp(head(tail(r2)), tail(tail(r2))));
-    lean_assert(is_eqp(r2, r3));
-    lean_assert(r == r2);
 }
 
 int main() {
diff --git a/src/util/sexpr/options.h b/src/util/sexpr/options.h
index af0dbd89bf..d28338e6ae 100644
--- a/src/util/sexpr/options.h
+++ b/src/util/sexpr/options.h
@@ -87,9 +87,6 @@ public:
     friend format pp(options const & o);
     friend std::ostream & operator<<(std::ostream & out, options const & o);
 
-    friend serializer & operator<<(serializer & s, options const & o) { s << o.m_value; return s; }
-    friend options read_options(deserializer & d);
-
     friend bool operator==(options const & a, options const & b) { return a.m_value == b.m_value; }
 };
 bool get_verbose(options const & opts);
@@ -97,8 +94,6 @@ name const & get_verbose_opt_name();
 name const & get_max_memory_opt_name();
 name const & get_timeout_opt_name();
 
-inline options read_options(deserializer & d) { return options(read_sexpr(d)); }
-inline deserializer & operator>>(deserializer & d, options & o) { o = read_options(d); return d; }
 template<typename T> options update(options const & o, name const & n, T const & v) { return o.update(n, sexpr(v)); }
 
 inline options operator+(options const & opts1, options const & opts2) {
diff --git a/src/util/sexpr/sexpr.cpp b/src/util/sexpr/sexpr.cpp
index 65da825e4e..9c855247d8 100644
--- a/src/util/sexpr/sexpr.cpp
+++ b/src/util/sexpr/sexpr.cpp
@@ -277,79 +277,10 @@ std::ostream & operator<<(std::ostream & out, sexpr const & s) {
 
 bool operator==(sexpr const & a, name const & b) { return is_name(a) && to_name(a) == b; }
 
-class sexpr_serializer : public object_serializer<sexpr, sexpr::ptr_hash, sexpr::ptr_eq> {
-    typedef object_serializer<sexpr, sexpr::ptr_hash, sexpr::ptr_eq> super;
-public:
-    void write(sexpr const & a) {
-        super::write(a, [&]() {
-                serializer & s = get_owner();
-                auto k = a.kind();
-                s << static_cast<char>(k);
-                switch (k) {
-                case sexpr_kind::Nil:                                  break;
-                case sexpr_kind::String: s << to_string(a);            break;
-                case sexpr_kind::Bool:   s << to_bool(a);              break;
-                case sexpr_kind::Int:    s << to_int(a);               break;
-                case sexpr_kind::Double: s << to_double(a);            break;
-                case sexpr_kind::Name:   s << to_name(a);              break;
-                case sexpr_kind::Cons:   write(car(a)); write(cdr(a)); break;
-                case sexpr_kind::Ext:
-                    throw exception("s-expressions constaining external atoms cannot be serialized");
-                }
-            });
-    }
-};
-
-class sexpr_deserializer : public object_deserializer<sexpr> {
-    typedef object_deserializer<sexpr> super;
-public:
-    sexpr read() {
-        return super::read([&]() {
-                deserializer & d = get_owner();
-                auto k = static_cast<sexpr_kind>(d.read_char());
-                switch (k) {
-                case sexpr_kind::Nil:    return sexpr();
-                case sexpr_kind::String: return sexpr(d.read_string());
-                case sexpr_kind::Bool:   return sexpr(d.read_bool());
-                case sexpr_kind::Int:    return sexpr(d.read_int());
-                case sexpr_kind::Double: return sexpr(d.read_double());
-                case sexpr_kind::Name:   return sexpr(read_name(d));
-                case sexpr_kind::Ext:    lean_unreachable(); // LCOV_EXCL_LINE
-                case sexpr_kind::Cons:   {
-                    sexpr h = read();
-                    sexpr t = read();
-                    return sexpr(h, t);
-                }}
-                throw corrupted_stream_exception();
-            });
-    }
-};
-
-struct sexpr_sd {
-    unsigned m_s_extid;
-    unsigned m_d_extid;
-    sexpr_sd() {
-        m_s_extid = serializer::register_extension([](){ return std::unique_ptr<serializer::extension>(new sexpr_serializer()); });
-        m_d_extid = deserializer::register_extension([](){ return std::unique_ptr<deserializer::extension>(new sexpr_deserializer()); });
-    }
-};
-static sexpr_sd * g_sexpr_sd = nullptr;
-
 void initialize_sexpr() {
-    g_sexpr_sd = new sexpr_sd();
 }
 
 void finalize_sexpr() {
-    delete g_sexpr_sd;
-}
-
-serializer & operator<<(serializer & s, sexpr const & n) {
-    s.get_extension<sexpr_serializer>(g_sexpr_sd->m_s_extid).write(n);
-    return s;
-}
-
-sexpr read_sexpr(deserializer & d) {
-    return d.get_extension<sexpr_deserializer>(g_sexpr_sd->m_d_extid).read();
 }
 }
 
diff --git a/src/util/sexpr/sexpr.h b/src/util/sexpr/sexpr.h
index cb167355bd..b925d86925 100644
--- a/src/util/sexpr/sexpr.h
+++ b/src/util/sexpr/sexpr.h
@@ -167,10 +167,6 @@ inline bool operator>(sexpr const & a, sexpr const & b) { return cmp(a, b) > 0;
 inline bool operator<=(sexpr const & a, sexpr const & b) { return cmp(a, b) <= 0; }
 inline bool operator>=(sexpr const & a, sexpr const & b) { return cmp(a, b) >= 0; }
 
-serializer & operator<<(serializer & s, sexpr const & a);
-sexpr read_sexpr(deserializer & d);
-inline deserializer & operator>>(deserializer & d, sexpr & a) { a = read_sexpr(d); return d; }
-
 void initialize_sexpr();
 void finalize_sexpr();
 }