diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt
index 21d45453c..2b09230b9 100644
--- a/src/util/CMakeLists.txt
+++ b/src/util/CMakeLists.txt
@@ -65,6 +65,7 @@ z3_add_component(util
   MEMORY_INIT_FINALIZER_HEADERS
     debug.h
     gparams.h
+    scoped_timer.h
     prime_generator.h
     rational.h
     rlimit.h
diff --git a/src/util/scoped_timer.cpp b/src/util/scoped_timer.cpp
index a3be0cebc..5375ca96b 100644
--- a/src/util/scoped_timer.cpp
+++ b/src/util/scoped_timer.cpp
@@ -21,19 +21,19 @@ Revision History:
 
 #include "util/scoped_timer.h"
 #include "util/util.h"
+#include "util/vector.h"
 #include <chrono>
 #include <climits>
 #include <condition_variable>
 #include <mutex>
 #include <thread>
-#include <vector>
 
 struct state {
-    std::thread * m_thread = nullptr;
+    std::thread * m_thread { nullptr };
     std::timed_mutex m_mutex;
-    unsigned ms;
-    event_handler * eh;
-    int work = 0;
+    unsigned ms { 0 };
+    event_handler * eh { nullptr };
+    int work { 0 };
     std::condition_variable_any cv;
 };
 
@@ -43,7 +43,7 @@ struct state {
  * destructing threads blocked on condition variables leads to
  * deadlock.
  */
-static std::vector<state *> available_workers;
+static ptr_vector<state> available_workers;
 static std::mutex workers;
 
 static void thread_func(state *s) {
@@ -80,7 +80,8 @@ public:
         if (available_workers.empty()) {
             workers.unlock();
             s = new state;
-        } else {
+        } 
+        else {
             s = available_workers.back();
             available_workers.pop_back();
             workers.unlock();
@@ -92,7 +93,8 @@ public:
         if (!s->m_thread) {
             s->m_thread = new std::thread(thread_func, s);
             s->m_thread->detach();
-        } else {
+        } 
+        else {
             s->cv.notify_one();
         }
     }
@@ -112,3 +114,9 @@ scoped_timer::scoped_timer(unsigned ms, event_handler * eh) {
 scoped_timer::~scoped_timer() {
     dealloc(m_imp);
 }
+
+void finalize_scoped_timer() {
+    // TODO: stub to collect idle allocated timers.
+    // if a timer is not idle, we treat this as abnormal
+    // termination and don't commit to collecting the state.
+}
diff --git a/src/util/scoped_timer.h b/src/util/scoped_timer.h
index 1213d025b..7d44923fe 100644
--- a/src/util/scoped_timer.h
+++ b/src/util/scoped_timer.h
@@ -28,3 +28,8 @@ public:
     ~scoped_timer();
 };
 
+/*
+  ADD_FINALIZER('finalize_scoped_timer();')
+*/
+
+void finalize_scoped_timer();
diff --git a/src/util/symbol.h b/src/util/symbol.h
index 9fe40d83a..ab7d41c98 100644
--- a/src/util/symbol.h
+++ b/src/util/symbol.h
@@ -16,9 +16,6 @@ Author:
 Revision History:
 
 --*/
-#if 0
-  // include "util/new_symbol.h"
-#else
 #pragma once
 #include <climits>
 #include <string>
@@ -156,5 +153,4 @@ void finalize_symbols();
 // two non-numerical symbols are compared using string comparison.
 bool lt(symbol const & s1, symbol const & s2);
 
-#endif /* SYMBOL_H_ */