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/substitutions.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/substitutions.h')
0 files changed, 0 insertions, 0 deletions