projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 913691e) | patch
Changed the splitting-on-demand lemmas of arithmetic to no longer contain the equalit...
authorTim King <taking@cs.nyu.edu>
Mon, 19 Nov 2012 17:16:16 +0000 (17:16 +0000)
committerTim King <taking@cs.nyu.edu>
Mon, 19 Nov 2012 17:16:16 +0000 (17:16 +0000)
commit1f80df98e2766a0202741d9e924bf842ba2225b5
tree8ab2ece58fcf56de4b179cdb24b13df5be770695tree
parent913691ef342edf411a33b81ecc071682978af858commit | diff
Changed the splitting-on-demand lemmas of arithmetic to no longer contain the equality being split on. Instead of issuing 'x != y implies (x < y or x > y)', the lemma is now '(x <= y or x >= y)'. This resolves bug 450.
src/theory/arith/constraint.cpp diff | blob | history