Test/smoke/Output


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25

-------------------- smoke0.bpl --------------------
found unreachable code:
implementation b(x: int)
{
  var y: int;
  var y@0: int;


  anon0:
    assume true;
    assume true;
    goto anon3_Then;

  anon3_Then:
    assume true;
    assume x < 0;
    y := 1;
    assume 1 <= y && y <= 1;
    assert false;
    return;
}


Boogie program verifier finished with 4 verified, 0 errors