projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 4a45b80) | patch
Adding the failing QF_AUFLIA regression mentioned in last commit.
authorKshitij Bansal <kshitij@cs.nyu.edu>
Sat, 16 Jun 2012 23:04:15 +0000 (23:04 +0000)
committerKshitij Bansal <kshitij@cs.nyu.edu>
Sat, 16 Jun 2012 23:04:15 +0000 (23:04 +0000)
commit94d13d40b27beb6e1ae8ec8221f6610d9d1a024d
tree23923e2e838ffda91cf21800ca2c19505970b064tree
parent4a45b80a981a875cb560876dee2eb7bfa9db1e08commit | diff
Adding the failing QF_AUFLIA regression mentioned in last commit.
pp-regfile.delta02.smt is the one to look at with
--decision=justificaiton, the delta minimized version of pp-regfile,
which also gives wrong answer. due to various commits/fixes, delta01
gives correct answer currently.
test/regress/regress0/decision/Makefile.am diff | blob | history
test/regress/regress0/decision/pp-regfile.delta01.smt [new file with mode: 0644] blob
test/regress/regress0/decision/pp-regfile.delta01.smt.expect [new file with mode: 0644] blob
test/regress/regress0/decision/pp-regfile.delta02.smt [new file with mode: 0644] blob
test/regress/regress0/decision/pp-regfile.delta02.smt.expect [new file with mode: 0644] blob
test/regress/regress0/decision/pp-regfile.smt [new file with mode: 0644] blob
test/regress/regress0/decision/pp-regfile.smt.expect [new file with mode: 0644] blob