projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 6489cf5) | patch
Add regressions for #4707. (#5555)
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Tue, 1 Dec 2020 14:03:50 +0000 (15:03 +0100)
committerGitHub <noreply@github.com>
Tue, 1 Dec 2020 14:03:50 +0000 (15:03 +0100)
commitd452621ef035a0127d691618e85a4fa2ab6fa027
tree2459ff371748daa73d3271187676e7d48ce3d6a5tree
parent6489cf590b441aeb5e1bdf9800c9718d06842149commit | diff
Add regressions for #4707. (#5555)

The error from #4707 has been fixed in the meantime, this PR adds the example inputs as regressions.
Closes #4707.
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/issue4707-bv-to-bool-small.smt2 [new file with mode: 0644] blob
test/regress/regress2/issue4707-bv-to-bool-large.smt2 [new file with mode: 0644] blob