viperproject
List of test cases that fail using more complete exhale
Here's a complete list of all test cases that fail using the --enableMoreCompleteExhale option, 14 in total:
all/issues/silicon/{0030, 0072, 0232, 0240, 0502, 0505}.vpr
all/predicates/arguments.vpr
quantifiedpermissions/issues/issue_{0149, 0184}.vpr
quantifiedpermissions/misc/misc1.vpr
quantifiedpermissions/sequences/self_framing.vpr
quantifiedpermissions/sets/generalized_shape.vpr
quantifiedpredicates/issues/unfolding.vpr
wands/regression/PackageStateConsolidation.vpr
An updated list: 8 tests fail in total.
Most fail because test annotations expect errors caused by incompleteness (i.e., these are not actual test failures):
- all/issues/silicon/0072.vpr
- all/issues/silicon/0232.vpr
- all/predicates/arguments.vpr
- quantifiedpermissions/issues/issue_0184.vpr
- quantifiedpermissions/sequences/self_framing.vpr
- quantifiedpredicates/issues/unfolding.vpr
Actual failures:
- quantifiedpermissions/sequences/mergesort.vpr
Here, the reason seems to be that the accesses to a.array result in different (newly-defined) values that are defined only inside a quantifier, but are needed to trigger it.
Timeout:
- all/sequences/sequences.vpr
This test is super flaky in general.
Update: quantifiedpermissions/sequences/mergesort.vpr works now. That means that currently, there are no test cases that fail with moreCompleteExhale except for the ones mentioned above that aren't actual test failures.