Invariant export for witnesses of Predicate Analysis is broken

There seems to be a mismatch between the locations where the predicate analysis computes abstractions and the locations that are used in the witness. This leads to witnesses without invariants . I consider this a severe bug, since the witnesses are not useful at all.

Reproduce this with:

scripts/cpa.sh -predicateAnalysis -spec sv-comp-reachability -setprop cpa.arg.compressWitness=false -setprop cpa.arg.proofWitness=cwbrokenWitness.graphml cwbroken.c

Using the program cwbroken.c:

extern int __VERIFIER_nondet_int();
extern void __VERIFIER_error();

int main() {
  int i = 0;
  while (__VERIFIER_nondet_int()) {
    i = __VERIFIER_nondet_int();
    if (i!=0) {
      i = 0;
    }
  }
  if (i != 0) {
    __VERIFIER_error();
  }
}

For quicker reference, here is the CFA of cwbroken.c:

Predicate analysis unrolles the loop with abstraction states at CFA location N4. In the witness, the "enterLoopHead" goes to N3 instead: cwbrokenWitness.graphml

I probably already found the underlying problem. The nodes N4 and N3 in the witness are merged because the edge in between is considered irrelevant. Thus the invariants 1 and i==0 get merged via disjunction, i.e. the result is an invariant 1 aka true.