`ERROR` verdict for both branches dead in SV-COMP

[sim642]

Apparently there are SV-COMP tasks where we output the "both branches dead" unsoundness warning, but still happily give a true SV-COMP result. We've been lucky that this hasn't caused unsound verdicts.
In these cases the verdict should instead be something like ERROR (both branches dead).

We do this for fixpoint errors with ERROR (fixpoint).

[karoliineh]

The example I stumbled upon was termination-restricted-15/IntPath.c

extern int __VERIFIER_nondet_int(void);

int main() {
    int i;
    int x;
    int y;
    i = __VERIFIER_nondet_int();
    x = 0;
    y = 0;
    
    if (i > 10) {
        x = 1;
    } else {
        y = 1;
    }
    while (x == y) { }
    
    return 0;
}

which yields:

...
[Error][Analyzer][Unsound] both branches over condition 'x == y' are dead (./termination-restricted-15/IntPath.c:18:12-18:18)
SV-COMP result: true
[Warning][Analyzer] Invariant Apron: cannot convert to cil var in overflow preserving manner: term18_5_id0#1998
[Info][Witness] witness generation summary:
  total generation entries: 1
[Error][Analyzer][Unsound] Both branches dead

[michael-schwarz]

The example I stumbled upon was termination-restricted-15/IntPath.c

Looks like it may be an unsoundness in our apron bindings we only bump into for polyhedra, which are enabled for termination.

[sim642]

Looks like it may be an unsoundness in our apron bindings we only bump into for polyhedra, which are enabled for termination.

It's not that, because it also happens with octagon. Anyway, I extracted the unsoundness itself to #1578.

[sim642]

There's something else odd going on as well: even though termination is supposed to make us use polyhedra, it's actually still using octagon. Explicitly setting the domain from command line works.

EDIT: Forcing a single unroll and polyhedra, there's a state with

 [|2y#302-1=0; 2x#301-1=0; term18_5_id0#1998-1=0; -2i#300+2147483657>=0; 2i#300+2147483637>=0|]

which isn't bottom according to Apron and thus we don't make it dead.
Only when doing some subsequent operations, Apron realizes the contradiction (due to integer variables), so both branches are dead.
So it's not as simple as the predecessor being dead/bottom even.