Invariants in witnesses produced by CPAchecker contain out of scope variables
Currently for some programs CPAchecker exports invariants in witnesses version 2.0 which contain out of scope variables. This happens for example when a variable is declared locally in the loop but is then used in the invariant. Since the witness export relies on the interface ExpressionTreeReportingState
to export the invariants, it may be the case that they are reporting out of scope variables. Another possibility is that the witness export is considering wrong abstract states to build the invariant.
A possible solution would be to filter out the out of scope variables when creating the invariant, but this may result in a large overapproximation.
For an example for which this occurs you can use the following command line for the sample task loop-lit/bh2017-ex1-poly.i:
scripts/cpa.sh -svcomp24 -heap 10000M -benchmark -timelimit '900 s' -spec sv-benchmarks/c/properties/unreach-call.prp sv-benchmarks/c/loop-lit/bh2017-ex1-poly.i
the witness in version 2.0 under output/witness.yml
contains the variable j
in the invariant for the outer loop at line 16 where it has not yet been defined, since it is only defined in the inner loop.