From b3ce68e7803dcb868004155b6d61a88a8dbe6c6f Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Fri, 29 Oct 2010 21:10:46 +0000
Subject: [PATCH] Fix for a problem caused by using a != instead of == in
 generateConflictBelow(). Resolves a bug introduced in -r1063.

---
 src/theory/arith/simplex.cpp | 5 +++--
 src/theory/arith/tableau.cpp | 3 +++
 2 files changed, 6 insertions(+), 2 deletions(-)

diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp
index be2b87252..e435fd3dc 100644
--- a/src/theory/arith/simplex.cpp
+++ b/src/theory/arith/simplex.cpp
@@ -388,8 +388,9 @@ Node SimplexDecisionProcedure::privateUpdateInconsistentVars(){
       }
       d_griggioRuleQueue.pop();
     }
+
     d_pivotStage = false;
-    return updateInconsistentVars();
+    return privateUpdateInconsistentVars();
   }
 
   Unreachable();
@@ -451,7 +452,7 @@ Node SimplexDecisionProcedure::generateConflictBelow(ArithVar conflictVar){
 
   for(ReducedRowVector::NonZeroIterator nbi = row_i->beginNonZero(), end = row_i->endNonZero(); nbi != end; ++nbi){
     ArithVar nonbasic = getArithVar(*nbi);
-    if(nonbasic != conflictVar) continue;
+    if(nonbasic == conflictVar) continue;
 
     const Rational& a_ij = nbi->second;
 
diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp
index c22c21a46..3c1cd36ba 100644
--- a/src/theory/arith/tableau.cpp
+++ b/src/theory/arith/tableau.cpp
@@ -63,6 +63,9 @@ void Tableau::pivot(ArithVar x_r, ArithVar x_s){
   Assert(d_basicManager.isMember(x_r));
   Assert(!d_basicManager.isMember(x_s));
 
+  Debug("tableau") << "Tableau::pivot("
+                   <<  x_r <<", " <<x_s <<")"  << endl;
+
   ReducedRowVector* row_s = lookup(x_r);
   Assert(row_s->has(x_s));
 
-- 
2.30.2