diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h
index a50d3ed37..784293461 100644
--- a/src/sat/sat_lookahead.h
+++ b/src/sat/sat_lookahead.h
@@ -353,7 +353,7 @@ namespace sat {
             candidate(bool_var v, double r): m_var(v), m_rating(r) {}
         };
         svector<candidate> m_candidates;
-        uint_set           m_select_lookahead_vars;
+        tracked_uint_set   m_select_lookahead_vars;
 
         double get_rating(bool_var v) const { return m_rating[v]; }
         double get_rating(literal l) const { return get_rating(l.var()); }
diff --git a/src/util/sat_literal.h b/src/util/sat_literal.h
index 920b0528b..aeb23bddd 100644
--- a/src/util/sat_literal.h
+++ b/src/util/sat_literal.h
@@ -110,12 +110,10 @@ namespace sat {
 
     inline void negate(literal_vector& ls) { for (unsigned i = 0; i < ls.size(); ++i) ls[i].neg(); }
 
-    typedef tracked_uint_set uint_set;
-
-    typedef uint_set bool_var_set;
+    typedef tracked_uint_set bool_var_set;
 
     class literal_set {
-        uint_set m_set;
+        tracked_uint_set m_set;
     public:
         literal_set(literal_vector const& v) {
             for (unsigned i = 0; i < v.size(); ++i) insert(v[i]);
@@ -141,9 +139,9 @@ namespace sat {
         void reset() { m_set.reset(); }
         void finalize() { m_set.finalize(); }
         class iterator {
-            uint_set::iterator m_it;
+            tracked_uint_set::iterator m_it;
         public:
-            iterator(uint_set::iterator it):m_it(it) {}
+            iterator(tracked_uint_set::iterator it):m_it(it) {}
             literal operator*() const { return to_literal(*m_it); }
             iterator& operator++() { ++m_it; return *this; }
             iterator operator++(int) { iterator tmp = *this; ++m_it; return tmp; }