https://gcc.gnu.org/bugzilla/show_bug.cgi?id=118915
--- Comment #6 from Krister Walfridsson <kristerw at gcc dot gnu.org> ---
(In reply to Andrew Pinski from comment #3)
> I am kinda of shock that smtgcc didn't find this earlier.
My guess is that the relevant testcases are written similarly to
```
int main() {
if (b(a + 21, a + 6, a + 34, a + 26) != 2)
abort ();
return 0;
}
```
which makes smtgcc give up because a call to abort -- smtgcc would trivially
have found it for tests written as:
```
int foo(void)
{
return b(a + 21, a + 6, a + 34, a + 26);
}
int main() {
if (foo() != 2)
abort ();
return 0;
}
```
I'll add support for abort. Will be fun to see if we find more ancient bugs!
