From f1ad95cdc8b678a51a7d69f7c19712d267fe9f4c Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Thu, 17 May 2012 23:00:43 +0000
Subject: [PATCH] This fixes a fascinating segfault.  This is the sequence of
 events: 1) A restart occurs 2) A shared term is registered to arithmetic. 3)
 Arithmetic sets this up. 4) No new linear relations are added to arithmetic.
 5) Eventually a restart occurs. 6) Arithmetic resets the tableau as it has
 not had a row added since the last restart. 7) A new variable is added. 8)
 This exceeds the size of the column vector of the saved tableau by exactly
 one. 9) segfault

---
 src/theory/arith/matrix.cpp       |  2 ++
 src/theory/arith/matrix.h         |  8 ++++++--
 src/theory/arith/theory_arith.cpp | 25 ++++++++++---------------
 src/theory/arith/theory_arith.h   |  2 +-
 4 files changed, 19 insertions(+), 18 deletions(-)

diff --git a/src/theory/arith/matrix.cpp b/src/theory/arith/matrix.cpp
index 18fbf395e..6320f87ce 100644
--- a/src/theory/arith/matrix.cpp
+++ b/src/theory/arith/matrix.cpp
@@ -391,6 +391,8 @@ void Tableau::addRow(ArithVar basic,
                      const std::vector<Rational>& coefficients,
                      const std::vector<ArithVar>& variables)
 {
+  Assert(basic < getNumColumns());
+
   Assert(coefficients.size() == variables.size() );
   Assert(!isBasic(basic));
 
diff --git a/src/theory/arith/matrix.h b/src/theory/arith/matrix.h
index b1be48828..5becdc9fb 100644
--- a/src/theory/arith/matrix.h
+++ b/src/theory/arith/matrix.h
@@ -410,7 +410,11 @@ public:
 protected:
 
   void addEntry(RowIndex row, ArithVar col, const T& coeff){
+    Debug("tableau") << "addEntry(" << row << "," << col <<"," << coeff << ")" << std::endl;
+
     Assert(coeff != 0);
+    Assert(row < d_rows.size());
+    Assert(col < d_columns.size());
 
     EntryID newId = d_entries.newEntry();
     Entry& newEntry = d_entries.get(newId);
@@ -418,7 +422,6 @@ protected:
 
     Assert(newEntry.getCoefficient() != 0);
 
-    Debug("tableau") << "addEntry(" << row << "," << col <<"," << coeff << ")" << std::endl;
 
     ++d_entriesInUse;
 
@@ -444,7 +447,7 @@ protected:
     entry.markBlank();
 
     d_entries.freeEntry(id);
-}
+  }
 
 public:
 
@@ -495,6 +498,7 @@ public:
     for(; varsIter != varsEnd; ++coeffIter, ++varsIter){
       const Rational& coeff = *coeffIter;
       ArithVar var_i = *varsIter;
+      Assert(var_i < getNumColumns());
       addEntry(ridx, var_i, coeff);
     }
 
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 1bd3277cd..524079938 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -67,7 +67,7 @@ TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputCha
   d_diosolver(c),
   d_pbSubstitutions(u),
   d_restartsCounter(0),
-  d_rowHasBeenAdded(false),
+  d_tableauSizeHasBeenModified(false),
   d_tableauResetDensity(1.6),
   d_tableauResetPeriod(10),
   d_conflicts(c),
@@ -695,7 +695,7 @@ void TheoryArith::setupPolynomial(const Polynomial& poly) {
   }
 
   if(polyNode.getKind() == PLUS){
-    d_rowHasBeenAdded = true;
+    d_tableauSizeHasBeenModified = true;
 
     vector<ArithVar> variables;
     vector<Rational> coefficients;
@@ -800,6 +800,7 @@ ArithVar TheoryArith::requestArithVar(TNode x, bool slack){
   d_arithvarNodeMap.setArithVar(x,varX);
 
   d_tableau.increaseSize();
+  d_tableauSizeHasBeenModified = true;
 
   d_constraintDatabase.addVariable(varX);
 
@@ -1568,23 +1569,17 @@ void TheoryArith::notifyRestart(){
 
   ++d_restartsCounter;
 
-  static const bool debugResetPolicy = false;
-
   uint32_t currSize = d_tableau.size();
   uint32_t copySize = d_smallTableauCopy.size();
 
-  if(debugResetPolicy){
-    cout << "curr " << currSize << " copy " << copySize << endl;
-  }
-  if(d_rowHasBeenAdded){
-    if(debugResetPolicy){
-      cout << "row has been added must copy " << d_restartsCounter << endl;
-    }
-    d_smallTableauCopy = d_tableau;
-    d_rowHasBeenAdded = false;
-  }
+  Debug("arith::reset") << "curr " << currSize << " copy " << copySize << endl;
+  Debug("arith::reset") << "tableauSizeHasBeenModified " << d_tableauSizeHasBeenModified << endl;
 
-  if(!d_rowHasBeenAdded && d_restartsCounter >= RESET_START){
+  if(d_tableauSizeHasBeenModified){
+    Debug("arith::reset") << "row has been added must copy " << d_restartsCounter << endl;
+    d_smallTableauCopy = d_tableau;
+    d_tableauSizeHasBeenModified = false;
+  }else if( d_restartsCounter >= RESET_START){
     if(copySize >= currSize * 1.1 ){
       ++d_statistics.d_smallerSetToCurr;
       d_smallTableauCopy = d_tableau;
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 0b631aa9d..4aac76eac 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -215,7 +215,7 @@ private:
    * If d >= s_TABLEAU_RESET_DENSITY * d_initialDensity, the tableau
    * is set to d_initialTableau.
    */
-  bool d_rowHasBeenAdded;
+  bool d_tableauSizeHasBeenModified;
   double d_tableauResetDensity;
   uint32_t d_tableauResetPeriod;
   static const uint32_t s_TABLEAU_RESET_INCREMENT = 5;
-- 
2.30.2