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.cpp | |
| 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.cpp')
| -rw-r--r-- | src/theory/arith/matrix.cpp | 2 |
1 files changed, 2 insertions, 0 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)); |