1 files changed, 4 insertions, 3 deletions
diff --git a/src/util/node_visitor.h b/src/util/node_visitor.h
index e444ba6e2..4c8e646bd 100644
--- a/src/util/node_visitor.h
+++ b/src/util/node_visitor.h
@@ -36,10 +36,11 @@ class NodeVisitor {
   /**
    * Guard against NodeVisitor<> being re-entrant.
    */
+  template <class T>
   class GuardReentry {
-    bool& d_guard;
+    T& d_guard;
   public:
-    GuardReentry(bool& guard)
+    GuardReentry(T& guard)
     : d_guard(guard) {
       Assert(!d_guard);
       d_guard = true;
@@ -71,7 +72,7 @@ public:
    */
   static typename Visitor::return_type run(Visitor& visitor, TNode node) {
 
-    GuardReentry guard(bool(s_inRun));
+    GuardReentry<CVC4_THREADLOCAL_TYPE(bool)> guard(s_inRun);
 
     // Notify of a start
     visitor.start(node);