projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 0dce010) | patch
Patch for the subtype theoryof mode to make the equalities over disequal types get...
authorTim King <taking@cs.nyu.edu>
Fri, 6 Jun 2014 15:45:16 +0000 (11:45 -0400)
committerTim King <taking@cs.nyu.edu>
Fri, 6 Jun 2014 20:26:40 +0000 (16:26 -0400)
commit6ec8f46e9a7315057ac8fb5c58a6b44cf5a5159e
tree9afae28a572c91b4c9f93ca137c84d1fa1808aeftree
parent0dce010bea47bc6a318eece2bd92ed2305b64c21commit | diff
Patch for the subtype theoryof mode to make the equalities over disequal types get sent to the theory of the type.
Adding a new test case for bug 569.
Fixes to the normal form of arithmetic so that real terms are before integer terms.
src/theory/arith/arith_rewriter.cpp diff | blob | history
src/theory/arith/normal_form.cpp diff | blob | history
src/theory/arith/normal_form.h diff | blob | history
src/theory/theory.cpp diff | blob | history
test/regress/regress0/arith/Makefile.am diff | blob | history
test/regress/regress0/arith/bug569.smt2 [new file with mode: 0644] blob