projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: da1e7aa) | patch
Fixed arithmetic consistency issue. The simplex conflict variable had to be reenqueu...
authorTim King <taking@cs.nyu.edu>
Thu, 14 Jun 2012 19:29:25 +0000 (19:29 +0000)
committerTim King <taking@cs.nyu.edu>
Thu, 14 Jun 2012 19:29:25 +0000 (19:29 +0000)
commit2581001b96a64e1d11d826cf554d378ac522bbe2
tree438024c782ce3a92aa44559772a6c4378332f958tree
parentda1e7aaacab8dd4e9b80b752f362d190c1472543commit | 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.
src/theory/arith/arith_priority_queue.h diff | blob | history
src/theory/arith/simplex.cpp diff | blob | history
src/theory/arith/simplex.h diff | blob | history
src/theory/arith/theory_arith.cpp diff | blob | history
src/theory/arith/theory_arith.h diff | blob | history
test/regress/regress0/arith/DTP_k2_n35_c175_s15.smt2 [new file with mode: 0644] blob
test/regress/regress0/arith/Makefile.am diff | blob | history