- This commit adds some debugging information to ArithPriorityQueue.

- There was a missing break statement in ArithPriorityQueue. This addresses the bug discovered in the debug regression (http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=1566&reference_id=1548&category=1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,29&p=10).

1 files changed, 8 insertions, 0 deletions

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;
 }