with also variable renaming

In old CFG there is an incorrect duplication of stmt and
returns after the conditional. The new CFG has been checked and
the resulting proof obligations are semantically identical to the
previous ones.

with associated variable renaming