projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: f68d074) | patch
int-blaster: direct support for bvcomp (#8640)
authoryoni206 <yoni206@users.noreply.github.com>
Wed, 20 Apr 2022 15:39:16 +0000 (18:39 +0300)
committerGitHub <noreply@github.com>
Wed, 20 Apr 2022 15:39:16 +0000 (15:39 +0000)
commit854b81c30cbd189e89ef143f4a6aae6ac0deb915
tree58b0b4989fb039097076e2e4061ae264cd1d7eb8tree
parentf68d074187bd78f11204ce0f4480c7116100af19commit | diff
int-blaster: direct support for bvcomp (#8640)

This PR adds a translation of bvcomp using an ite.
Fixes cvc5/cvc5-projects#417
and contains the failed formula as a regression.
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_proj_417.smt2 [new file with mode: 0644] blob