Do not add an impossible goal for loop termination
See this discussion
I reproduce the central part :
The only weird part of that commit is adding an impossible subgoal to diverging for-loops (which can diverge because of the divergent body, but cannot themselves be the reason of non-termination). Line 980 in vc.ml
(current HEAD) should probably be removed. Also, we should probably not add an impossible subgoal to a while-loop with a variant
, just because its body is divergent.