[IntToBV] Add check for unsupported operators (#8949)
authorAndres Noetzli <andres.noetzli@gmail.com>
Mon, 11 Jul 2022 17:57:22 +0000 (10:57 -0700)
committerGitHub <noreply@github.com>
Mon, 11 Jul 2022 17:57:22 +0000 (17:57 +0000)
commit5f7eee9f639496ce4959206999f4576a7da32663
tree9502d7ed72d14bd169ea96e2dfb51fd3121d5932
parent79db74b6976354141e2cee776d07a47f5c2af423
[IntToBV] Add check for unsupported operators (#8949)

Fixes #8935. This adds a check for unsupported operators in the IntToBV
preprocessing pass and improves error messages. Previously, operators
such as str.to_int, which return an integer but do not take an integer
as an argument were not detected as unsupported.
src/preprocessing/passes/int_to_bv.cpp
test/regress/cli/CMakeLists.txt
test/regress/cli/regress0/int-to-bv/issue8935-unsupported-operators.smt2 [new file with mode: 0644]