diff options
author | Tim King <taking@cs.nyu.edu> | 2011-02-25 19:28:48 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2011-02-25 19:28:48 +0000 |
commit | 616a0b85d1abd20f173890025585c640525f07cc (patch) | |
tree | d069ba92c65eb4626c361f523c03fa5f0a83a169 /src/theory/arith/simplex.cpp | |
parent | 48101a9e2416a16b645f31936776694a25cf9efd (diff) |
- 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).
Diffstat (limited to 'src/theory/arith/simplex.cpp')
-rw-r--r-- | src/theory/arith/simplex.cpp | 8 |
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; } |