Change VC generation for "while true".
With this PR, we do not consider a continuation for a "while true" loop. I.e., Why3 will not generate VCs for traces leaving these loops through a failed loop condition. This is sound because all these VCs contain false as an hypothesis (the negation of the loop condition, true).
This change is important for code generated from mlcfg with the stackify algorithm, since all the loop generated by this algorithm are "while true" loops, left using local exceptions.