diff --git a/src/test/CMakeLists.txt b/src/test/CMakeLists.txt
index a273d4e77..4ddc1b8cb 100644
--- a/src/test/CMakeLists.txt
+++ b/src/test/CMakeLists.txt
@@ -37,7 +37,6 @@ add_executable(test-z3
   dl_table.cpp
   dl_util.cpp
   doc.cpp
-  dlist.cpp
   egraph.cpp
   escaped.cpp
   euf_bv_plugin.cpp
diff --git a/src/test/dlist.cpp b/src/test/dlist.cpp
deleted file mode 100644
index 81689699f..000000000
--- a/src/test/dlist.cpp
+++ /dev/null
@@ -1,170 +0,0 @@
-#include <cassert>
-#include <iostream>
-#include "util/dlist.h"
-
-class TestNode : public dll_base<TestNode> {
-public:
-    int value;
-    TestNode(int val) : value(val) {
-        init(this);
-    }
-};
-
-// Test the prev() method
-void test_prev() {
-    TestNode node(1);
-    assert(node.prev() == &node);
-    std::cout << "test_prev passed." << std::endl;
-}
-
-// Test the next() method
-void test_next() {
-    TestNode node(1);
-    assert(node.next() == &node);
-    std::cout << "test_next passed." << std::endl;
-}
-
-// Test the const prev() method
-void test_const_prev() {
-    const TestNode node(1);
-    assert(node.prev() == &node);
-    std::cout << "test_const_prev passed." << std::endl;
-}
-
-// Test the const next() method
-void test_const_next() {
-    const TestNode node(1);
-    assert(node.next() == &node);
-    std::cout << "test_const_next passed." << std::endl;
-}
-
-// Test the init() method
-void test_init() {
-    TestNode node(1);
-    node.init(&node);
-    assert(node.next() == &node);
-    assert(node.prev() == &node);
-    assert(node.invariant());
-    std::cout << "test_init passed." << std::endl;
-}
-
-// Test the pop() method
-void test_pop() {
-    TestNode* list = nullptr;
-    TestNode node1(1);
-    TestNode::push_to_front(list, &node1);
-    TestNode* popped = TestNode::pop(list);
-    assert(popped == &node1);
-    assert(list == nullptr);
-    assert(popped->next() == popped);
-    assert(popped->prev() == popped);
-    std::cout << "test_pop passed." << std::endl;
-}
-
-// Test the insert_after() method
-void test_insert_after() {
-    TestNode node1(1);
-    TestNode node2(2);
-    node1.insert_after(&node2);
-    assert(node1.next() == &node2);
-    assert(node2.prev() == &node1);
-    assert(node1.prev() == &node2);
-    assert(node2.next() == &node1);
-    assert(node1.invariant());
-    assert(node2.invariant());
-    std::cout << "test_insert_after passed." << std::endl;
-}
-
-// Test the insert_before() method
-void test_insert_before() {
-    TestNode node1(1);
-    TestNode node2(2);
-    node1.insert_before(&node2);
-    assert(node1.prev() == &node2);
-    assert(node2.next() == &node1);
-    assert(node1.next() == &node2);
-    assert(node2.prev() == &node1);
-    assert(node1.invariant());
-    assert(node2.invariant());
-    std::cout << "test_insert_before passed." << std::endl;
-}
-
-// Test the remove_from() method
-void test_remove_from() {
-    TestNode* list = nullptr;
-    TestNode node1(1);
-    TestNode node2(2);
-    TestNode::push_to_front(list, &node1);
-    TestNode::push_to_front(list, &node2);
-    TestNode::remove_from(list, &node1);
-    assert(list == &node2);
-    assert(node2.next() == &node2);
-    assert(node2.prev() == &node2);
-    assert(node1.next() == &node1);
-    assert(node1.prev() == &node1);
-    std::cout << "test_remove_from passed." << std::endl;
-}
-
-// Test the push_to_front() method
-void test_push_to_front() {
-    TestNode* list = nullptr;
-    TestNode node1(1);
-    TestNode::push_to_front(list, &node1);
-    assert(list == &node1);
-    assert(node1.next() == &node1);
-    assert(node1.prev() == &node1);
-    std::cout << "test_push_to_front passed." << std::endl;
-}
-
-// Test the detach() method
-void test_detach() {
-    TestNode node(1);
-    TestNode::detach(&node);
-    assert(node.next() == &node);
-    assert(node.prev() == &node);
-    assert(node.invariant());
-    std::cout << "test_detach passed." << std::endl;
-}
-
-// Test the invariant() method
-void test_invariant() {
-    TestNode node1(1);
-    assert(node1.invariant());
-    TestNode node2(2);
-    node1.insert_after(&node2);
-    assert(node1.invariant());
-    assert(node2.invariant());
-    std::cout << "test_invariant passed." << std::endl;
-}
-
-// Test the contains() method
-void test_contains() {
-    TestNode* list = nullptr;
-    TestNode node1(1);
-    TestNode node2(2);
-    TestNode::push_to_front(list, &node1);
-    TestNode::push_to_front(list, &node2);
-    assert(TestNode::contains(list, &node1));
-    assert(TestNode::contains(list, &node2));
-    TestNode node3(3);
-    assert(!TestNode::contains(list, &node3));
-    std::cout << "test_contains passed." << std::endl;
-}
-
-int tst_dlist() {
-    test_prev();
-    test_next();
-    test_const_prev();
-    test_const_next();
-    test_init();
-    test_pop();
-    test_insert_after();
-    test_insert_before();
-    test_remove_from();
-    test_push_to_front();
-    test_detach();
-    test_invariant();
-    test_contains();
-    std::cout << "All tests passed." << std::endl;
-    return 0;
-}
diff --git a/src/test/main.cpp b/src/test/main.cpp
index 0d3679529..0c3d0e01a 100644
--- a/src/test/main.cpp
+++ b/src/test/main.cpp
@@ -188,7 +188,6 @@ int main(int argc, char ** argv) {
     TST(total_order);
     TST(dl_table);
     TST(dl_context);
-    TST(dlist);
     TST(dl_util);
     TST(dl_product_relation);
     TST(dl_relation);
diff --git a/src/util/dlist.h b/src/util/dlist.h
index 584817785..3d9efacd5 100644
--- a/src/util/dlist.h
+++ b/src/util/dlist.h
@@ -255,4 +255,4 @@ template < typename T
 dll_iterator<T> end(T const& list)
 {
     return dll_iterator<T>::mk_end(&list);
-}
\ No newline at end of file
+} 
\ No newline at end of file