When the analysed program contains a static array of large size (approx. >80 000 elements), the analysis always ends with TRUE even though the program contains an error.
This occurs when check_properties is run on a program with loops before computing a program invariant (e.g. when --k-induction is used). The reason for this bug is that with such a large size array, the solver always evaluates the program SSA (without any additional invariant) as unsatisfiable. This causes the property checker to think that all loops have been unwound and that an assertion in a loop always holds (instead, it holds for the first iteration, but not for the following ones).
The bug can be reproduced on an SV-COMP example array-examples/standard_init1_false-unreach-call_ground.c using the --k-induction switch.
When the analysed program contains a static array of large size (approx. >80 000 elements), the analysis always ends with TRUE even though the program contains an error.
This occurs when check_properties is run on a program with loops before computing a program invariant (e.g. when --k-induction is used). The reason for this bug is that with such a large size array, the solver always evaluates the program SSA (without any additional invariant) as unsatisfiable. This causes the property checker to think that all loops have been unwound and that an assertion in a loop always holds (instead, it holds for the first iteration, but not for the following ones).
The bug can be reproduced on an SV-COMP example
array-examples/standard_init1_false-unreach-call_ground.cusing the--k-inductionswitch.