projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: bf7bd71) | patch
Disable arrays in eager bit-blasting (#8785)
authoryoni206 <yoni206@users.noreply.github.com>
Thu, 2 Jun 2022 03:08:43 +0000 (06:08 +0300)
committerGitHub <noreply@github.com>
Thu, 2 Jun 2022 03:08:43 +0000 (03:08 +0000)
commit1bcf55c6e616aef0aa5de7fea6c5d37588b135a0
treeabcb8f2161dcb05bedb4b0a07f87353bf44973d8tree
parentbf7bd719996501a52a1d757d5c268b5ddc03dd14commit | diff
Disable arrays in eager bit-blasting (#8785)

Fixes cvc5/cvc5-projects#461 . This does not allow arrays in eager bit-blasting, that is, only QF_BV and QF_UFBV are allowed. The reason is that Ackermannization (which is turned on in eager bit-blasting) eliminates array operators but does not eliminate array variables, that later cause a logic exception.
src/smt/set_defaults.cpp diff | blob | history
test/regress/cli/regress0/bv/ackermann3.smt2 diff | blob | history