3 files changed, 11 insertions, 11 deletions
diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index a232ad33b..566bf3a68 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -84,7 +84,7 @@ RewriteResponse TheoryBVRewriter::postRewrite(TNode node) {
   return RewriteResponse(REWRITE_DONE, result);
 }
 
-AllRewriteRules* TheoryBVRewriter::s_allRules = NULL;
+CVC4_THREADLOCAL(AllRewriteRules*) TheoryBVRewriter::s_allRules = NULL;
 
 void TheoryBVRewriter::init() {
   s_allRules = new AllRewriteRules;
diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h
index 11a55ca61..f0eb621ca 100644
--- a/src/theory/bv/theory_bv_rewriter.h
+++ b/src/theory/bv/theory_bv_rewriter.h
@@ -32,7 +32,7 @@ struct AllRewriteRules;
 
 class TheoryBVRewriter {
 
-  static AllRewriteRules* s_allRules;
+  static CVC4_THREADLOCAL(AllRewriteRules*) s_allRules;
 
 public:
 
diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h
index 926ceb767..192295bc0 100644
--- a/src/theory/bv/theory_bv_type_rules.h
+++ b/src/theory/bv/theory_bv_type_rules.h
@@ -30,7 +30,7 @@ namespace bv {
 class BitVectorConstantTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate) {
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
     return nodeManager->mkBitVectorType(n.getConst<BitVector>().getSize());
   }
 };
@@ -38,7 +38,7 @@ public:
 class BitVectorCompRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate) {
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ) {
       TypeNode lhs = n[0].getType(check);
       TypeNode rhs = n[1].getType(check);
@@ -53,7 +53,7 @@ public:
 class BitVectorArithRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate) {
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
     unsigned maxWidth = 0;
     TNode::iterator it = n.begin();
     TNode::iterator it_end = n.end();
@@ -72,7 +72,7 @@ public:
 class BitVectorFixedWidthTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate) {
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
     TNode::iterator it = n.begin();
     TypeNode t = (*it).getType(check);
     if( check ) {
@@ -93,7 +93,7 @@ public:
 class BitVectorPredicateTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate) {
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ) {
       TypeNode lhsType = n[0].getType(check);
       if (!lhsType.isBitVector()) {
@@ -111,7 +111,7 @@ public:
 class BitVectorExtractTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate) {
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
     BitVectorExtract extractInfo = n.getOperator().getConst<BitVectorExtract>();
 
     // NOTE: We're throwing a type-checking exception here even
@@ -137,7 +137,7 @@ public:
 class BitVectorConcatRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate) {
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
     unsigned size = 0;
     TNode::iterator it = n.begin();
     TNode::iterator it_end = n.end();
@@ -158,7 +158,7 @@ public:
 class BitVectorRepeatTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate) {
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
     TypeNode t = n[0].getType(check);
     // NOTE: We're throwing a type-checking exception here even
     // when check is false, bc if the argument isn't a bit-vector
@@ -174,7 +174,7 @@ public:
 class BitVectorExtendTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate) {
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
     TypeNode t = n[0].getType(check);
     // NOTE: We're throwing a type-checking exception here even
     // when check is false, bc if the argument isn't a bit-vector