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.

1 files changed, 6 insertions, 0 deletions

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. */