diff options
| author | Tim King <taking@cs.nyu.edu> | 2011-02-21 00:22:18 +0000 |
|---|---|---|
| committer | Tim King <taking@cs.nyu.edu> | 2011-02-21 00:22:18 +0000 |
| commit | 71b73af2ff69f41d71b892d6fc920a7b38fe736a (patch) | |
| tree | 8828c05c8f2618072a2d93860d8c4126d7f4b560 /src/theory/arith/theory_arith.cpp | |
| parent | 0db4ec99a2f289b66878d0ca3be9d43492eff3ad (diff) | |
- Adds the statistic d_avgNumRowsNotContainingOnPivot.
- Removed a bug in row counting in row counting.
Diffstat (limited to 'src/theory/arith/theory_arith.cpp')
| -rw-r--r-- | src/theory/arith/theory_arith.cpp | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 4e84c85db..6084e3463 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -694,9 +694,11 @@ void TheoryArith::permanentlyRemoveVariable(ArithVar v){ Node eq = row->asEquality(d_arithVarToNodeMap); if(Debug.isOn("row::print")) row->printRow(); + if(Debug.isOn("tableau")) d_tableau.printTableau(); Debug("arith::permanentlyRemoveVariable") << eq << endl; delete row; + Assert(d_tableau.getRowCount(v) == 0); Assert(d_removedRows.find(v) == d_removedRows.end()); d_removedRows[v] = eq; } |