Anotation rules for while rule in deductive verification
As you have already said, the second and third rule include a variant t to prove termination whereas the first rule does not consider it.

The second rule guarantees that the variant is always non-negative. This is necessary to have a lower bound for the variant which decreases every iteration.

The third rule relaxes that condition a little bit. The variant is always non-negative except in the last iteration (where e is false at the end of the block). This still guarantees termination (who cares about the variant if we know it's the last iteration?).

I think whether you choose the second or third rule is a matter of taste. Until now I knew only the second one. It should be easy to alter code or a variant whose correctness can be shown by the third rule such that it is also provable with the second one.

Choosing the first rule is of course only an option if you're not interested in termination.