Wrong verdict for ite-tasks
During experiments on handcrafted tasks (featuring ite-pattern) CPAchecker and ESBMC have returned wrong verdicts for following three tasks: two_ites_8
, ite_chain_8
, and nosixes_8
.
AVR has returned the correct verdicts for nosixes_8
and ite_chain_8
, but failed to return any verdict for two_ites_8
. The difference of verdicts between AVR, which takes the Btor2 tasks as input directly, and CPAchecker and ESBMC, which rely on the translation of Btor2C, might indicate that the translations of these tasks are not correct.
The set of ite tasks consist of four different families, where the number in the filename indicates the bit-vector width used to determine the size of the arrays. For example: two_ites_3
uses arrays of size 8.
Notice how all wrong verdicts were returned for tasks that use bit-vectors of width 8 for their arrays.
Figuring out the cause might be of interest.