diff --git a/src/tests/util/CMakeLists.txt b/src/tests/util/CMakeLists.txt
index fe9af0c9f..6154db36a 100644
--- a/src/tests/util/CMakeLists.txt
+++ b/src/tests/util/CMakeLists.txt
@@ -40,3 +40,6 @@ add_test(splay_tree ${CMAKE_CURRENT_BINARY_DIR}/splay_tree)
 add_executable(splay_map splay_map.cpp)
 target_link_libraries(splay_map ${EXTRA_LIBS})
 add_test(splay_map ${CMAKE_CURRENT_BINARY_DIR}/splay_map)
+add_executable(trace trace.cpp)
+target_link_libraries(trace ${EXTRA_LIBS})
+add_test(trace ${CMAKE_CURRENT_BINARY_DIR}/trace)
diff --git a/src/tests/util/trace.cpp b/src/tests/util/trace.cpp
new file mode 100644
index 000000000..445733050
--- /dev/null
+++ b/src/tests/util/trace.cpp
@@ -0,0 +1,18 @@
+/*
+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/trace.h"
+using namespace lean;
+
+int main() {
+    lean_assert(!is_trace_enabled("name"));
+    enable_trace("name");
+    lean_assert(is_trace_enabled("name"));
+    disable_trace("name");
+    lean_assert(!is_trace_enabled("name"));
+    return has_violations() ? 1 : 0;
+}