WTO is computed multiple times

[Maxime-Derri]

The WTO is computed both during the CFG computation (in case loop counters are inserted into Bourdoncle components) and before generating pre- and post-invariants. When loop counters are inserted in the CFG, Bourdoncle components can be easily updated as labels are stored in reverse order. See #948 for a prototype.