projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2f8226e) | patch
fixed problem with datatypes giving incorrect explanations, now corrected and improve...
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 23 Oct 2012 22:27:38 +0000 (22:27 +0000)
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 23 Oct 2012 22:27:38 +0000 (22:27 +0000)
commit697dd317af39a896865c99b922e80baac2bb4b23
treed7fe1ab437effafbc7cb70d30c40b49640afc6d1tree
parent2f8226e01f37035fe4edefb1e47d47b48638f832commit | diff
fixed problem with datatypes giving incorrect explanations, now corrected and improved.  this update fixes bug 428, also changes the result for 2 benchmarks where tcc in cvc3 fails (cvc4 had previously had been answering correctly by accident).
src/theory/datatypes/theory_datatypes.cpp diff | blob | history
src/theory/datatypes/theory_datatypes.h diff | blob | history
test/regress/regress0/datatypes/datatype1.cvc diff | blob | history
test/regress/regress0/datatypes/datatype3.cvc diff | blob | history