diff options
| -rw-r--r-- | src/theory/arith/simplex.cpp | 5 | ||||
| -rw-r--r-- | 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)); |