projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: cb49e01) | patch
bv-to-int: fix translation of bvneg (#8437)
authoryoni206 <yoni206@users.noreply.github.com>
Tue, 29 Mar 2022 20:00:32 +0000 (23:00 +0300)
committerGitHub <noreply@github.com>
Tue, 29 Mar 2022 20:00:32 +0000 (20:00 +0000)
commit3d21e4397f5f5db2266b623729542755b34b1996
treefe5ab3e996e643ff9cd87a2819aa9730b6de73a7tree
parentcb49e0143ac7b71a671b238cae6d0e63c0e90d2ecommit | diff
bv-to-int: fix translation of bvneg  (#8437)

The translation of bvneg to integers did not match the comment documenting it, causing #8413 .
This PR fixes the issue and includes the test from #8413 as well as a simpler test.
Fixes #8413 .
src/theory/bv/int_blaster.cpp diff | blob | history
test/regress/cli/CMakeLists.txt diff | blob | history
test/regress/cli/regress0/bv/bv_to_int_issue_8413_1.smt2 [new file with mode: 0644] blob
test/regress/cli/regress0/bv/bv_to_int_issue_8413_2.smt2 [new file with mode: 0644] blob