We consider as the loop head of a do-while loop the location at the beginning of the loop body (right before the first statement). This is also what ends up being the widening point.

However, the YAML witnesses paper states for all loop_invariants that the invariant must always hold immediately before evaluating the loop condition. For do-while loops that is at the end of the loop body, not at the beginning.
This is different from what was considered loop_invariant in the old YAML witness draft (without invariant_set). I only realized this while describing them for my thesis.