blob: 4141bdb0ade2893c9ce4e1e3c0d1542057332971 (
plain)
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
|