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 26 27 28 29 30
// RUN: %boogie -infer:j "%s" > "%t" // RUN: %diff "%s.expect" "%t" const TEST: name; procedure P() { var i: int; var N: int; start: assume N >= 0; i := 0; assert i <= N; goto LoopHead; LoopHead: goto LoopBody, AfterLoop; LoopBody: assume i < N; i := i + 1; goto LoopHead; AfterLoop: assume !(i < N); assert i == N; return; } type name;