diff options
| author | Tim King <taking@cs.nyu.edu> | 2012-11-19 17:16:16 +0000 |
|---|---|---|
| committer | Tim King <taking@cs.nyu.edu> | 2012-11-19 17:16:16 +0000 |
| commit | 1f80df98e2766a0202741d9e924bf842ba2225b5 (patch) | |
| tree | 8ab2ece58fcf56de4b179cdb24b13df5be770695 /test/regress | |
| parent | 913691ef342edf411a33b81ecc071682978af858 (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.
Diffstat (limited to 'test/regress')
0 files changed, 0 insertions, 0 deletions