Ensure that returns are removed when using an ai analysis

[danpoe]

It seems that currently most ai analyses (except the value set analysis) assume that returns have been removed from the goto program. However, many features that use an ai analysis (like the slicer) don't remove returns before they work on the goto program.

[TGWDB]

Closing this due to age and lack of clear problem (I recognise that some analysis appears to assume returns are no longer there, but if there is no actual error or behaviour problem in cbmc it is not clear this requires attention at this time).

If you believe this is erroneous please reopen this issue.