portfolio merge

4 files changed, 9 insertions, 6 deletions

diff --git a/src/theory/arith/arith_priority_queue.cpp b/src/theory/arith/arith_priority_queue.cpp
index 3b1f5f395..e74a250a3 100644
--- a/src/theory/arith/arith_priority_queue.cpp
+++ b/src/theory/arith/arith_priority_queue.cpp
@@ -191,12 +191,15 @@ void ArithPriorityQueue::transitionToDifferenceMode() {
 
   switch(d_pivotRule){
   case MINIMUM:
+    Debug("arith::pivotRule") << "Making the minimum heap." << endl;
     make_heap(d_diffQueue.begin(), d_diffQueue.end(), VarDRatPair::minimumRule);
     break;
   case BREAK_TIES:
+    Debug("arith::pivotRule") << "Making the break ties heap." << endl;
     make_heap(d_diffQueue.begin(), d_diffQueue.end(), VarDRatPair::breakTiesRules);
     break;
   case MAXIMUM:
+    Debug("arith::pivotRule") << "Making the maximum heap." << endl;
     make_heap(d_diffQueue.begin(), d_diffQueue.end(), VarDRatPair::maximumRule);
     break;
   }
diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp
index 27fb0bb02..26cdb2cdb 100644
--- a/src/theory/arith/simplex.cpp
+++ b/src/theory/arith/simplex.cpp
@@ -619,9 +619,9 @@ Node SimplexDecisionProcedure::updateInconsistentVars(){
   if(d_queue.empty()){
     return Node::null();
   }
-  static unsigned int instance = 0;
-  ++instance;
 
+  static CVC4_THREADLOCAL(unsigned int) instance = 0;
+  ++instance;
   Debug("arith::updateInconsistentVars") << "begin updateInconsistentVars() "
                                          << instance << endl;
 
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 64e713b0a..268829105 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -1223,7 +1223,7 @@ void TheoryArith::presolve(){
 
   if(Debug.isOn("paranoid:check_tableau")){ d_simplex.debugCheckTableau(); }
 
-  static int callCount = 0;
+  static CVC4_THREADLOCAL(unsigned) callCount = 0;
   Debug("arith::presolve") << "TheoryArith::presolve #" << (callCount++) << endl;
 
   d_learner.clear();
diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h
index 9c69ec684..511982d48 100644
--- a/src/theory/arith/theory_arith_type_rules.h
+++ b/src/theory/arith/theory_arith_type_rules.h
@@ -29,7 +29,7 @@ namespace arith {
 class ArithConstantTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate) {
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
     if (n.getKind() == kind::CONST_RATIONAL) return nodeManager->realType();
     return nodeManager->integerType();
   }
@@ -38,7 +38,7 @@ public:
 class ArithOperatorTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate) {
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
     TypeNode integerType = nodeManager->integerType();
     TypeNode realType = nodeManager->realType();
     TNode::iterator child_it = n.begin();
@@ -65,7 +65,7 @@ public:
 class ArithPredicateTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-      throw (TypeCheckingExceptionPrivate) {
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ) {
       TypeNode integerType = nodeManager->integerType();
       TypeNode realType = nodeManager->realType();