From 2581001b96a64e1d11d826cf554d378ac522bbe2 Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Thu, 14 Jun 2012 19:29:25 +0000
Subject: Fixed arithmetic consistency issue.  The simplex conflict variable
 had to be reenqueued so that the queue was a superset of the failing
 assertions.  This adds a super expensive debug routine
 unenqueuedVariablesAreConsistent() that catches this bug.  This is enabled
 when -d arith::consistency is turned on. make check passes with this flag
 enabled.

---
 src/theory/arith/simplex.h | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'src/theory/arith/simplex.h')

diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h
index d260ff9b4..a1c69548c 100644
--- a/src/theory/arith/simplex.h
+++ b/src/theory/arith/simplex.h
@@ -224,6 +224,12 @@ public:
     d_queue.clear();
   }
 
+
+  bool debugIsInCollectionQueue(ArithVar var) const{
+    Assert(d_queue.inCollectionMode());
+    return d_queue.collectionModeContains(var);
+  }
+
 private:
 
   /** Reports a conflict to on the output channel. */
-- 
cgit v1.2.3