Add Option for Strict Location-Matching in Correctness-Witness Validation
Currently, the correctness-witness validation of CPAchecker tries to match each invariant in the witness to program locations. If this fails for an invariant, the invariant is ignored. I understand that this makes sense because a correctness witness may still be valid, even if it contains bogus-invariants at infeasible or non-existing program locations.
But there are use-cases in which we want to make sure that all invariants contained in a correctness witness are valid. A simple example is debugging of correctness witnesses.
So it would be great to have an option that makes CPAchecker reject a correctness witness if the witness contains an invariant that can't be matched to at least one program location. As a bonus, CPAchecker could report which invariant failed.