2 files changed, 15 insertions, 0 deletions
diff --git a/src/theory/arith/arith_priority_queue.cpp b/src/theory/arith/arith_priority_queue.cpp
index 417115ab9..14a228e62 100644
--- a/src/theory/arith/arith_priority_queue.cpp
+++ b/src/theory/arith/arith_priority_queue.cpp
@@ -70,6 +70,7 @@ void ArithPriorityQueue::enqueueIfInconsistent(ArithVar basic){
     case VariableOrder:
       d_varOrderQueue.push_back(basic);
       push_heap(d_varOrderQueue.begin(), d_varOrderQueue.end(), std::greater<ArithVar>());
+      break;
     case Difference:
       d_diffQueue.push_back(computeDiff(basic));
       push_heap(d_diffQueue.begin(), d_diffQueue.end());
@@ -85,6 +86,8 @@ void ArithPriorityQueue::transitionToDifferenceMode() {
   Assert(d_varOrderQueue.empty());
   Assert(d_diffQueue.empty());
 
+  Debug("arith::priorityqueue") << "transitionToDifferenceMode()" << endl;
+
   ArithVarArray::const_iterator i = d_candidates.begin(), end = d_candidates.end();
   for(; i != end; ++i){
     ArithVar var = *i;
@@ -106,6 +109,8 @@ void ArithPriorityQueue::transitionToVariableOrderMode() {
   Assert(d_varOrderQueue.empty());
   Assert(d_candidates.empty());
 
+  Debug("arith::priorityqueue") << "transitionToVariableOrderMode()" << endl;
+
   DifferenceArray::const_iterator i = d_diffQueue.begin(), end = d_diffQueue.end();
   for(; i != end; ++i){
     ArithVar var = (*i).variable();
@@ -128,6 +133,8 @@ void ArithPriorityQueue::transitionToCollectionMode() {
   Assert(d_candidates.empty());
   Assert(d_varOrderQueue.empty());
 
+  Debug("arith::priorityqueue") << "transitionToCollectionMode()" << endl;
+
   d_modeInUse = Collection;
 }
 
diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp
index 25d154bae..c8f1ce3e8 100644
--- a/src/theory/arith/simplex.cpp
+++ b/src/theory/arith/simplex.cpp
@@ -429,6 +429,11 @@ Node SimplexDecisionProcedure::updateInconsistentVars(){
   if(d_queue.empty()){
     return Node::null();
   }
+  static unsigned int instance = 0;
+
+  ++instance;
+  Debug("arith::updateInconsistentVars") << "begin updateInconsistentVars() "
+                                         << instance << endl;
 
   d_queue.transitionToDifferenceMode();
 
@@ -459,6 +464,9 @@ Node SimplexDecisionProcedure::updateInconsistentVars(){
 
   Assert(d_queue.inCollectionMode());
 
+  Debug("arith::updateInconsistentVars") << "end updateInconsistentVars() "
+                                         << instance << endl;
+
   return possibleConflict;
 }