diff options
author | Tim King <taking@cs.nyu.edu> | 2012-05-17 23:00:43 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-05-17 23:00:43 +0000 |
commit | f1ad95cdc8b678a51a7d69f7c19712d267fe9f4c (patch) | |
tree | 2b7ee147b2d24750677479d2dc66efe504d422d4 /src/theory/arith/matrix.h | |
parent | f49378f9acb65b78ab29d89d37c644d0b203ebae (diff) |
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
Diffstat (limited to 'src/theory/arith/matrix.h')
-rw-r--r-- | src/theory/arith/matrix.h | 8 |
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); } |