diff options
Diffstat (limited to 'src/expr/node_manager.h')
| -rw-r--r-- | src/expr/node_manager.h | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index fab5d4688..b1b0bc974 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -101,7 +101,7 @@ class NodeManager { expr::NodeValueIDHashFunction, expr::NodeValueIDEquality> NodeValueIDSet; - static CVC4_THREADLOCAL(NodeManager*) s_current; + static CVC4_THREAD_LOCAL NodeManager* s_current; Options* d_options; StatisticsRegistry* d_statisticsRegistry; |