projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 1bcf55c) | patch
Restricting the bit-width in int-to-bv (#8814)
authoryoni206 <yoni206@users.noreply.github.com>
Thu, 2 Jun 2022 03:26:45 +0000 (06:26 +0300)
committerGitHub <noreply@github.com>
Thu, 2 Jun 2022 03:26:45 +0000 (03:26 +0000)
commit3003ba4636a5de1425869082cf4f497a256f4968
treefe159c45445fe31cd1c7e9ddc1117b54283e6e1btree
parent1bcf55c6e616aef0aa5de7fea6c5d37588b135a0commit | diff
Restricting the bit-width in int-to-bv (#8814)

`cvc5` only supports bit-widths of `unsigned` size for BitVector sorts (see, e.g., [here](https://github.com/cvc5/cvc5/blob/4338d9d49a41022d34cd4cbabf17a66fdf39efae/src/expr/node_manager_template.cpp#L178)).

This checks that the provided bit-width for the `int-to-bv` option is in the right range.

Fixes https://github.com/cvc5/cvc5-projects/issues/425 and includes a regression that is based on the test from the issue.
src/options/smt_options.toml diff | blob | history
test/regress/cli/CMakeLists.txt diff | blob | history
test/regress/cli/regress0/nl/proj-issue-425.smt2 [new file with mode: 0644] blob