Fix for bug 316. If the flag @CVC4_TLS_SUPPORTED@ is false, function pointers cannot...

diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index 586f37073f892c38ce708ee0801114f25b618201..2b48977b63c4e2ecb3ac3c0f46cc062eefe02b96 100644 (file)
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -33,7 +33,7 @@ using namespace CVC4::theory::bv;
 
 // CVC4_THREADLOCAL(AllRewriteRules*) TheoryBVRewriter::s_allRules = NULL;
 // CVC4_THREADLOCAL(TimerStat*) TheoryBVRewriter::d_rewriteTimer = NULL;
-CVC4_THREADLOCAL(RewriteFunction) TheoryBVRewriter::d_rewriteTable[kind::LAST_KIND]; 
+RewriteFunction TheoryBVRewriter::d_rewriteTable[kind::LAST_KIND]; 
 void TheoryBVRewriter::init() {
    // s_allRules = new AllRewriteRules;
    // d_rewriteTimer = new TimerStat("theory::bv::rewriteTimer");

diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h
index e72c1a910da99a0a84c96e6dfdb55380eb2fa6b3..7ce914477ab014a5900dec7def4444da306982d7 100644 (file)
--- a/src/theory/bv/theory_bv_rewriter.h
+++ b/src/theory/bv/theory_bv_rewriter.h
@@ -35,7 +35,9 @@ typedef RewriteResponse (*RewriteFunction) (TNode);
 class TheoryBVRewriter {
   // static CVC4_THREADLOCAL(AllRewriteRules*) s_allRules;
   // static CVC4_THREADLOCAL(TimerStat*) d_rewriteTimer; 
-  static CVC4_THREADLOCAL(RewriteFunction) d_rewriteTable[kind::LAST_KIND];
+
+#warning "TODO: Double check thread safety and make sure the fix compiles on mac."
+  static RewriteFunction d_rewriteTable[kind::LAST_KIND];
 
   static RewriteResponse IdentityRewrite(TNode node);
   static RewriteResponse UndefinedRewrite(TNode node);