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

1 files changed, 6 insertions, 2 deletions

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);
     }