[wp] fixed duplication of stmt & return

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.