8 files changed, 9 insertions, 15 deletions
diff --git a/src/theory/arith/dual_simplex.cpp b/src/theory/arith/dual_simplex.cpp
index 1f855b1dd..c2b95890a 100644
--- a/src/theory/arith/dual_simplex.cpp
+++ b/src/theory/arith/dual_simplex.cpp
@@ -17,7 +17,6 @@
 #include "theory/arith/dual_simplex.h"
 
 #include "base/output.h"
-#include "base/tls.h"
 #include "options/arith_options.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/arith/constraint.h"
@@ -63,7 +62,7 @@ DualSimplexDecisionProcedure::Statistics::~Statistics(){
 Result::Sat DualSimplexDecisionProcedure::dualFindModel(bool exactResult){
   Assert(d_conflictVariables.empty());
 
-  static CVC4_THREAD_LOCAL unsigned int instance = 0;
+  static thread_local unsigned int instance = 0;
   instance = instance + 1;
   d_pivots = 0;
 
diff --git a/src/theory/arith/fc_simplex.cpp b/src/theory/arith/fc_simplex.cpp
index 198c22e77..07c6b1691 100644
--- a/src/theory/arith/fc_simplex.cpp
+++ b/src/theory/arith/fc_simplex.cpp
@@ -17,7 +17,6 @@
 #include "theory/arith/fc_simplex.h"
 
 #include "base/output.h"
-#include "base/tls.h"
 #include "options/arith_options.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/arith/constraint.h"
@@ -92,7 +91,7 @@ Result::Sat FCSimplexDecisionProcedure::findModel(bool exactResult){
   Assert(d_sgnDisagreements.empty());
 
   d_pivots = 0;
-  static CVC4_THREAD_LOCAL unsigned int instance = 0;
+  static thread_local unsigned int instance = 0;
   instance = instance + 1;
   static const bool verbose = false;
 
diff --git a/src/theory/arith/soi_simplex.cpp b/src/theory/arith/soi_simplex.cpp
index 43ea51384..31301df61 100644
--- a/src/theory/arith/soi_simplex.cpp
+++ b/src/theory/arith/soi_simplex.cpp
@@ -19,7 +19,6 @@
 #include <algorithm>
 
 #include "base/output.h"
-#include "base/tls.h"
 #include "options/arith_options.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/arith/constraint.h"
@@ -104,7 +103,7 @@ Result::Sat SumOfInfeasibilitiesSPD::findModel(bool exactResult){
   Assert(d_sgnDisagreements.empty());
 
   d_pivots = 0;
-  static CVC4_THREAD_LOCAL unsigned int instance = 0;
+  static thread_local unsigned int instance = 0;
   instance = instance + 1;
   static const bool verbose = false;
 
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index ad0ce2e86..6db246b8b 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -24,7 +24,6 @@
 #include <vector>
 
 #include "base/output.h"
-#include "base/tls.h"
 #include "context/cdhashset.h"
 #include "context/cdinsert_hashmap.h"
 #include "context/cdlist.h"
@@ -4400,7 +4399,7 @@ void TheoryArithPrivate::presolve(){
 
   if(Debug.isOn("paranoid:check_tableau")){ d_linEq.debugCheckTableau(); }
 
-  static CVC4_THREAD_LOCAL unsigned callCount = 0;
+  static thread_local unsigned callCount = 0;
   if(Debug.isOn("arith::presolve")) {
     Debug("arith::presolve") << "TheoryArithPrivate::presolve #" << callCount << endl;
     callCount = callCount + 1;
diff --git a/src/theory/bv/bitblast/aig_bitblaster.cpp b/src/theory/bv/bitblast/aig_bitblaster.cpp
index f2417deb6..b06062cf4 100644
--- a/src/theory/bv/bitblast/aig_bitblaster.cpp
+++ b/src/theory/bv/bitblast/aig_bitblaster.cpp
@@ -116,7 +116,7 @@ Abc_Obj_t* mkIte<Abc_Obj_t*>(Abc_Obj_t* cond, Abc_Obj_t* a, Abc_Obj_t* b) {
   return Abc_AigMux(AigBitblaster::currentAigM(), cond, a, b); 
 }
 
-CVC4_THREAD_LOCAL Abc_Ntk_t* AigBitblaster::s_abcAigNetwork = nullptr;
+thread_local Abc_Ntk_t* AigBitblaster::s_abcAigNetwork = nullptr;
 
 Abc_Ntk_t* AigBitblaster::currentAigNtk() {
   if (!AigBitblaster::s_abcAigNetwork) {
diff --git a/src/theory/bv/bitblast/aig_bitblaster.h b/src/theory/bv/bitblast/aig_bitblaster.h
index bd624bf92..6d21b69e6 100644
--- a/src/theory/bv/bitblast/aig_bitblaster.h
+++ b/src/theory/bv/bitblast/aig_bitblaster.h
@@ -21,8 +21,6 @@
 
 #include "theory/bv/bitblast/bitblaster.h"
 
-#include "base/tls.h"
-
 class Abc_Obj_t_;
 typedef Abc_Obj_t_ Abc_Obj_t;
 
@@ -57,7 +55,7 @@ class AigBitblaster : public TBitblaster<Abc_Obj_t*>
   typedef std::unordered_map<TNode, Abc_Obj_t*, TNodeHashFunction> TNodeAigMap;
   typedef std::unordered_map<Node, Abc_Obj_t*, NodeHashFunction> NodeAigMap;
 
-  static CVC4_THREAD_LOCAL Abc_Ntk_t* s_abcAigNetwork;
+  static thread_local Abc_Ntk_t* s_abcAigNetwork;
   std::unique_ptr<context::Context> d_nullContext;
   std::unique_ptr<prop::SatSolver> d_satSolver;
   TNodeAigMap d_aigCache;
diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index 8b5d34cf4..2c9ccf46a 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -30,8 +30,8 @@ using namespace CVC4::theory;
 using namespace CVC4::theory::bv;
 
 
-// CVC4_THREAD_LOCAL AllRewriteRules* TheoryBVRewriter::s_allRules = NULL;
-// CVC4_THREAD_LOCAL TimerStat* TheoryBVRewriter::d_rewriteTimer = NULL;
+// thread_local AllRewriteRules* TheoryBVRewriter::s_allRules = NULL;
+// thread_local TimerStat* TheoryBVRewriter::d_rewriteTimer = NULL;
 RewriteFunction TheoryBVRewriter::d_rewriteTable[kind::LAST_KIND]; 
 void TheoryBVRewriter::init() {
    // s_allRules = new AllRewriteRules;
diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
index 6319e1196..58f4832c0 100644
--- a/src/theory/rewriter.cpp
+++ b/src/theory/rewriter.cpp
@@ -35,7 +35,7 @@ static TheoryId theoryOf(TNode node) {
 }
 
 #ifdef CVC4_ASSERTIONS
-static CVC4_THREAD_LOCAL std::unordered_set<Node, NodeHashFunction>* s_rewriteStack = NULL;
+static thread_local std::unordered_set<Node, NodeHashFunction>* s_rewriteStack = NULL;
 #endif /* CVC4_ASSERTIONS */
 
 class RewriterInitializer {