Before merging this we should verify that it is not just because the condition transfer functions are quite strong that we end up with this warning because the predecessor is in fact unreachable.

We should have this behavior either way independently of any particular task if we want to be serious about soundness.
If the both branches dead warning is triggered too generously, that's a separate precision problem for that.

I tried forcing Apron to somehow reduce integer constraints in #1585 to avoid the spurious cautiousness but none of it is particularly nice.
We should see from (our own) pre-runs how often this actually comes up on sv-benchmarks and then decide what to do about these.