Linux Driver Verification » BLAST

If the program has only one useful block (which is unsound by itself), BLAST fails with Invalid_argument("index out of bounds"). Here's an example:

int main()
{
  if (2+2 == 5){
    ERROR: goto ERROR;
  }
  return 0;
}