projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ddd3797) | patch
fixed bug in datatypes decision procedure enforcing rewriting of incorrectly applied...
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 26 Oct 2012 17:18:14 +0000 (17:18 +0000)
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 26 Oct 2012 17:18:14 +0000 (17:18 +0000)
commit25cb880b2e3cd3f3624f9c2ba399a2a50b4b2da7
treeea6435737fb0a677816301b717ad44d8b75b3564tree
parentddd3797ee72443bd35f6cea146c3752ea0dd2286commit | diff
fixed bug in datatypes decision procedure enforcing rewriting of incorrectly applied selector terms, this effects two regression test where TCC fails, using --disable-dt-rewrite-error-sel changes answer of both regression tests
src/theory/datatypes/theory_datatypes.cpp diff | blob | history
test/regress/regress0/datatypes/datatype1.cvc diff | blob | history
test/regress/regress0/datatypes/datatype3.cvc diff | blob | history