diff options
| author | Tim King <taking@cs.nyu.edu> | 2010-10-29 21:10:46 +0000 |
|---|---|---|
| committer | Tim King <taking@cs.nyu.edu> | 2010-10-29 21:10:46 +0000 |
| commit | b3ce68e7803dcb868004155b6d61a88a8dbe6c6f (patch) | |
| tree | 3927716d52c4f06ff606803d30c9949413c5556d /src/theory/arith/tableau.cpp | |
| parent | 4d305551927b2a667acaa796fb86d86aa6364b01 (diff) | |
Fix for a problem caused by using a != instead of == in generateConflictBelow(). Resolves a bug introduced in -r1063.
Diffstat (limited to 'src/theory/arith/tableau.cpp')
| -rw-r--r-- | src/theory/arith/tableau.cpp | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp index c22c21a46..3c1cd36ba 100644 --- a/src/theory/arith/tableau.cpp +++ b/src/theory/arith/tableau.cpp @@ -63,6 +63,9 @@ void Tableau::pivot(ArithVar x_r, ArithVar x_s){ Assert(d_basicManager.isMember(x_r)); Assert(!d_basicManager.isMember(x_s)); + Debug("tableau") << "Tableau::pivot(" + << x_r <<", " <<x_s <<")" << endl; + ReducedRowVector* row_s = lookup(x_r); Assert(row_s->has(x_s)); |