Add "ERROR (both branches dead)" verdict for SV-COMP

[sim642]

Closes #1576.

[michael-schwarz]

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.

[sim642]

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.

[michael-schwarz]

LGTM! We should keep a keen lookout for the instances of this.

I'm still wondering if if we can devise some way to not raise this when it's simply to imprecision of domains (Maybe don't raise it for Polyhedra at all now?)

[sim642]

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.