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

diff --git a/src/theory/arith/matrix.cpp b/src/theory/arith/matrix.cpp
index 18fbf395ed73bddf381537eccea1315184dc7d51..6320f87ce91fd3157fd974cd67364f159d183623 100644 (file)
--- 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 b1be488289cb88fad61458c390555ff06585c3fe..5becdc9fb4f36994501770a281cc6e5fa1d1126f 100644 (file)
--- 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 1bd3277cde8d9a6f09616922149fc12007ae35d3..524079938c12187d0727007fa381faa596c84dcd 100644 (file)
--- 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 0b631aa9d2c1d08ca3249a3d16369a62ba1237f6..4aac76eacb237eeacb13d17aa580991f20544a88 100644 (file)
--- 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;