diff options
| author | Tim King <taking@cs.nyu.edu> | 2012-06-14 19:29:25 +0000 |
|---|---|---|
| committer | Tim King <taking@cs.nyu.edu> | 2012-06-14 19:29:25 +0000 |
| commit | 2581001b96a64e1d11d826cf554d378ac522bbe2 (patch) | |
| tree | 438024c782ce3a92aa44559772a6c4378332f958 /src/theory/arith/theory_arith.h | |
| parent | da1e7aaacab8dd4e9b80b752f362d190c1472543 (diff) | |
Fixed arithmetic consistency issue. The simplex conflict variable had to be reenqueued so that the queue was a superset of the failing assertions. This adds a super expensive debug routine unenqueuedVariablesAreConsistent() that catches this bug. This is enabled when -d arith::consistency is turned on. make check passes with this flag enabled.
Diffstat (limited to 'src/theory/arith/theory_arith.h')
| -rw-r--r-- | src/theory/arith/theory_arith.h | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 556495c97..4983b0557 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -460,6 +460,7 @@ private: * Returns true iff every variable is consistent in the partial model. */ bool entireStateIsConsistent(); + bool unenqueuedVariablesAreConsistent(); bool isImpliedUpperBound(ArithVar var, Node exp); bool isImpliedLowerBound(ArithVar var, Node exp); |