[Analyses] Wrong SUCCESS displayed when Bounded Model Checking is used
Step-by-step to reproduce:
- open the attached model
- open the component architecture
- open the “A/G, Contracts, Patterns” aspect of the component
- click “Check all”
Obtained result:
- first property is FAIL
- second property is SUCCESS
Expected result:
- first and second properties are FAIL
The reason is that the default length of BMC is set to 25, so no counter-example is found when we ask if the counter reaches 26. This is an expected situation since that’s an intrinsic aspect of BMC. However, it should not display “SUCCESS” but “UNKNOWN” or something else.
(from redmine: issue id 2127, created on 2014-09-05, closed on 2015-01-16)
- Uploads: