Find solution for assumptions with "irrelevant" variables
Original issue created by @PhilippWendler on 2017-03-03 at 14:56:32, last modified on 2017-03-03 at 14:56:32
The PredicateCPA ignores all variables that are not necessary for the reachability of the error location with the option cpa.predicate.ignoreIrrelevantVariables
(on by the default). Specifically, these variables are not put in the SSAMap and thus never have their index increased. If formulas are created with such variables and conjuncted to the PathFormula, this can easily lead to contradicting assumptions, which make the analysis potentially unsound.
This can for example be triggered with assumptions, see the attached example files with command line scripts/cpa.sh -predicateAnalysis -setprop specification=assume.spc test.c
.
A workaround is to disable ignoreIrrelevantVariables
.
Better solutions could be to increment SSA indices of irrelevant variables when they are assigned, or filtering of the assumptions with regard to irrelevant variables.