Option `cpa.predicate.overflowVariablesAreRelevant` is currently unused and might still be buggy
I introduced this feature towards the end of 2017, probably as part of the SV-COMP efforts (trying to get better overflow verification for the busybox tasks). I added a new type of variables to the variable classification that marks variables that could contribute to an overflow.
I think this did not have the desired effect, at least for the busybox tasks, so it was never switched on in any config. I would expect however that this is worth switching on in the overflow configurations, because we could then use cpa.predicate.ignoreIrrelevantVariables=true
, which already shows significant performance benefits for the regular predicateAnalysis
.
This simply needs to be tried out, but I currently have no time for fiddling around with it, so I create this issue such that this is documented.
The config config/includes/predicateAnalysis--overflow.properties
currently sets:
cpa.predicate.ignoreIrrelevantVariables = false
It should be tested whether the following setting:
cpa.predicate.ignoreIrrelevantVariables = true
cpa.predicate.overflowVariablesAreRelevant = true
- is sound
- speeds up overflow verification on the sv-benchmarks
In case 1. is violated, this means that there are still some bugs which need to be fixed first.