diff options
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/node_visitor.h | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/util/node_visitor.h b/src/util/node_visitor.h index 687272b56..245c81224 100644 --- a/src/util/node_visitor.h +++ b/src/util/node_visitor.h @@ -32,7 +32,7 @@ template<typename Visitor> class NodeVisitor { /** For re-entry checking */ - static bool d_inRun; + static CVC4_THREADLOCAL(bool) d_inRun; class GuardReentry { bool& d_guard; @@ -111,7 +111,7 @@ public: }; template <typename Visitor> -bool NodeVisitor<Visitor>::d_inRun = false; +CVC4_THREADLOCAL(bool) NodeVisitor<Visitor>::d_inRun = false; } |