projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 8d0de29) | patch
bv-to-int: new tests from an issue (#5654)
authoryoni206 <yoni206@users.noreply.github.com>
Fri, 11 Dec 2020 23:08:23 +0000 (15:08 -0800)
committerGitHub <noreply@github.com>
Fri, 11 Dec 2020 23:08:23 +0000 (17:08 -0600)
commit107b1422f9549eb2128729c3fd173441029ba443
tree6f34ed2537fac701ba7557b4db7215f3678e9c47tree
parent8d0de294c259e789a149bc5ceb5d6501868e83d0commit | diff
bv-to-int: new tests from an issue (#5654)

#5293 pointed to assertion failures when employing --bv-to-int, starting from commit 94e3d9a.
The bug is not reproduced on current master, and so we would have this PR close #5293 .
This PR adds the benchmarks from #5293 .
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/bv/bv_to_int_5293_1.smt2 [new file with mode: 0644] blob
test/regress/regress0/bv/bv_to_int_5293_2.smt2 [new file with mode: 0644] blob