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, 5 insertions, 0 deletions

diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp
index ee71dea74..63bb42e7a 100644
--- a/src/theory/arith/simplex.cpp
+++ b/src/theory/arith/simplex.cpp
@@ -241,6 +241,7 @@ bool SimplexDecisionProcedure::findConflictOnTheQueue(SearchPeriod type) {
 
 Result::Sat SimplexDecisionProcedure::findModel(bool exactResult){
   Assert(d_conflictVariable == ARITHVAR_SENTINEL);
+  Assert(d_queue.inCollectionMode());
 
   if(d_queue.empty()){
     return Result::SAT;
@@ -352,6 +353,10 @@ Result::Sat SimplexDecisionProcedure::findModel(bool exactResult){
 
 
   d_pivotsInRound.purge();
+  // ensure that the conflict variable is still in the queue.
+  if(d_conflictVariable != ARITHVAR_SENTINEL){
+    d_queue.enqueueIfInconsistent(d_conflictVariable);
+  }
   d_conflictVariable = ARITHVAR_SENTINEL;
 
   d_queue.transitionToCollectionMode();