6 files changed, 42 insertions, 2 deletions
diff --git a/src/theory/arith/row_vector.cpp b/src/theory/arith/row_vector.cpp
index 07fc0186d..2af03bf08 100644
--- a/src/theory/arith/row_vector.cpp
+++ b/src/theory/arith/row_vector.cpp
@@ -117,7 +117,8 @@ void RowVector::merge(VarCoeffArray& arr,
     }else{
       Rational res = getCoefficient(*curr1) + c * getCoefficient(*curr2);
       if(res != 0){
-        ++counts[getArithVar(*curr2)];
+        //The variable is not new so the count stays the same
+        //bug: ++counts[getArithVar(*curr2)];
 
         arr.push_back(make_pair(getArithVar(*curr1), res));
       }else{
@@ -177,6 +178,7 @@ ReducedRowVector::ReducedRowVector(ArithVar basic,
   merge(d_entries, d_contains, justBasic, Rational(1), d_rowCount);
 
   Assert(wellFormed());
+  Assert(d_rowCount[d_basic] == 1);
 }
 
 void ReducedRowVector::substitute(const ReducedRowVector& row_s){
@@ -192,6 +194,7 @@ void ReducedRowVector::substitute(const ReducedRowVector& row_s){
 
   Assert(!has(x_s));
   Assert(wellFormed());
+  Assert(d_rowCount[basic()] == 1);
 }
 
 void ReducedRowVector::pivot(ArithVar x_j){
@@ -202,6 +205,9 @@ void ReducedRowVector::pivot(ArithVar x_j){
   d_basic = x_j;
 
   Assert(wellFormed());
+  //The invariant Assert(d_rowCount[basic()] == 1); does not hold.
+  //This is because the pivot is within the row first then
+  //is moved through the propagated through the rest of the tableau.
 }
 
 
@@ -237,3 +243,10 @@ Node ReducedRowVector::asEquality(const ArithVarToNodeMap& map) const{
   Node basicVar = (map.find(basic()))->second;
   return NodeBuilder<2>(EQUAL) << basicVar << sum;
 }
+
+
+ReducedRowVector::~ReducedRowVector(){
+  //This executes before the super classes destructor RowVector,
+  // which will set this to 0.
+  Assert(d_rowCount[basic()] == 1);
+}
diff --git a/src/theory/arith/row_vector.h b/src/theory/arith/row_vector.h
index 2b48564a4..85a188063 100644
--- a/src/theory/arith/row_vector.h
+++ b/src/theory/arith/row_vector.h
@@ -178,6 +178,7 @@ public:
                    const std::vector< Rational >& coefficients,
                    std::vector<uint32_t>& count);
 
+  ~ReducedRowVector();
 
   ArithVar basic() const{
     Assert(basicIsSet());
diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp
index 0f4f27a76..d8d39c24f 100644
--- a/src/theory/arith/simplex.cpp
+++ b/src/theory/arith/simplex.cpp
@@ -22,7 +22,9 @@ SimplexDecisionProcedure::Statistics::Statistics():
   d_selectInitialConflictTime("theory::arith::selectInitialConflictTime"),
   d_pivotsAfterConflict("theory::arith::pivotsAfterConflict", 0),
   d_checksWithWastefulPivots("theory::arith::checksWithWastefulPivots", 0),
-  d_pivotTime("theory::arith::pivotTime")
+  d_pivotTime("theory::arith::pivotTime"),
+  d_avgNumRowsNotContainingOnUpdate("theory::arith::avgNumRowsNotContainingOnUpdate"),
+  d_avgNumRowsNotContainingOnPivot("theory::arith::avgNumRowsNotContainingOnPivot")
 {
   StatisticsRegistry::registerStat(&d_statPivots);
   StatisticsRegistry::registerStat(&d_statUpdates);
@@ -36,6 +38,9 @@ SimplexDecisionProcedure::Statistics::Statistics():
   StatisticsRegistry::registerStat(&d_pivotsAfterConflict);
   StatisticsRegistry::registerStat(&d_checksWithWastefulPivots);
   StatisticsRegistry::registerStat(&d_pivotTime);
+
+  StatisticsRegistry::registerStat(&d_avgNumRowsNotContainingOnUpdate);
+  StatisticsRegistry::registerStat(&d_avgNumRowsNotContainingOnPivot);
 }
 
 SimplexDecisionProcedure::Statistics::~Statistics(){
@@ -51,6 +56,9 @@ SimplexDecisionProcedure::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_pivotsAfterConflict);
   StatisticsRegistry::unregisterStat(&d_checksWithWastefulPivots);
   StatisticsRegistry::unregisterStat(&d_pivotTime);
+
+  StatisticsRegistry::unregisterStat(&d_avgNumRowsNotContainingOnUpdate);
+  StatisticsRegistry::unregisterStat(&d_avgNumRowsNotContainingOnPivot);
 }
 
 /* procedure AssertLower( x_i >= c_i ) */
@@ -188,6 +196,10 @@ void SimplexDecisionProcedure::update(ArithVar x_i, const DeltaRational& v){
 
   d_partialModel.setAssignment(x_i, v);
 
+  Assert(d_tableau.getNumRows() >= d_tableau.getRowCount(x_i));
+  double difference = ((double)d_tableau.getNumRows()) - ((double) d_tableau.getRowCount(x_i));
+
+  (d_statistics.d_avgNumRowsNotContainingOnUpdate).addEntry(difference);
   if(Debug.isOn("paranoid:check_tableau")){
     checkTableau();
   }
@@ -261,8 +273,12 @@ void SimplexDecisionProcedure::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaR
     ++(d_statistics.d_pivotsAfterConflict);
   }
 
+  Assert(d_tableau.getNumRows() >= d_tableau.getRowCount(x_j));
+  double difference = ((double)d_tableau.getNumRows()) - ((double) d_tableau.getRowCount(x_j));
+  (d_statistics.d_avgNumRowsNotContainingOnPivot).addEntry(difference);
   d_tableau.pivot(x_i, x_j);
 
+
   checkBasicVariable(x_j);
 
   // Debug found conflict
diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h
index 84d7cdcbb..c5c4da661 100644
--- a/src/theory/arith/simplex.h
+++ b/src/theory/arith/simplex.h
@@ -208,6 +208,10 @@ private:
 
     IntStat d_pivotsAfterConflict, d_checksWithWastefulPivots;
     TimerStat d_pivotTime;
+
+    AverageStat d_avgNumRowsNotContainingOnUpdate;
+    AverageStat d_avgNumRowsNotContainingOnPivot;
+
     Statistics();
     ~Statistics();
   };
diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h
index 32c2986e3..36d61ba25 100644
--- a/src/theory/arith/tableau.h
+++ b/src/theory/arith/tableau.h
@@ -59,6 +59,10 @@ public:
   {}
   ~Tableau();
 
+  size_t getNumRows() const {
+    return d_basicVariables.size();
+  }
+
   void increaseSize(){
     d_basicVariables.increaseSize();
     d_rowsTable.push_back(NULL);
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 4e84c85db..6084e3463 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -694,9 +694,11 @@ void TheoryArith::permanentlyRemoveVariable(ArithVar v){
     Node eq = row->asEquality(d_arithVarToNodeMap);
 
     if(Debug.isOn("row::print")) row->printRow();
+    if(Debug.isOn("tableau")) d_tableau.printTableau();
     Debug("arith::permanentlyRemoveVariable") << eq << endl;
     delete row;
 
+    Assert(d_tableau.getRowCount(v) == 0);
     Assert(d_removedRows.find(v) ==  d_removedRows.end());
     d_removedRows[v] = eq;
   }