Fix conditions in irreducible loop analysis

[ailrst]

https://github.com/UQ-PAC/bil-to-boogie-translator/issues/191

The header block does not have conditions added to maintain the original control flow in the transformed loop.

I'm also unclear if there needs to be conditions to prevent loops between the header and a single dependent block when the flow is meant to switch between dependent blocks.

[l-kent]

From memory the way this works (though I haven't confirmed so this may be slightly off) is that we want to replace this:

block A
goto entry1

block B
goto entry2

with this:

block A
headerSwitch := 1
goto header

block B
headerSwitch := 2
goto header

block header
goto condition1, condition2

block condition1
assume headerSwitch == 1
goto entry1

block condition2
assume headerSwitch == 2
goto entry2

This can obviously just use bools for two blocks, or be extended to support any number of entrances to a loop.

This is not much of a priority though.