Clarification of keys cycle-head and invariant is needed for termination witnesses

[MartinSpiessl]

It has become unclear whether enforcing the current spec that says:

Thus, a node for which the cyclehead key is set, must also contain an invariant description.

makes sense. For now, we are planning to disable the check (cf. #31). Potential improvements will be discussed in this issue with the goal of either reenabling the check and clarifying the spec or removing the constraint for good.

[danieldietsch]

The current spec is actually here. And it is rather ... coarse. Basically it says: either use the violation witness format (compatible with Ultimate) or use an extension of the violation witness format (compatible with CPAchecker and Ultimate).

You referenced the specification for termination witnesses for CPAchecker which requires that

• exactly one node is marked as cyclehead,
• this node must have an ìnvariant, and
• other nodes might have an invariant, but are likely ignored in the stem, and might be used in the loop to provide invariants for program loops.

For SV-COMP 22 we can try and fix this. I would say:

• Lift CPAcheckers spec to the top level.
• Having a cyclehead seems helpful, lets require it.
• Forcing an invariant at that location seems unnecessary, drop it.
• Allow invariant for all nodes, make them like the invariants in the correctness witness (to avoid confusion).

[MartinSpiessl]

Thanks for the pointers and the nice high-level summary and recommendation.
I think that all sounds very reasonable and I would go with that proposal if nobody dissents.

I would like to get more comments by other tool authors, e.g.:

@TBunk
@mchalupa
@viktormalik /@peterschrammel

As far as I see those tools already output a cyclehead. CBMC and ESBMC never proof non-termination anyway, they just return true if they were able to explore the full state space, so there is also no effect on them if we make the cyclehead mandatory, do you agree @tautschnig?