1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21
var x: int; var y: int; procedure p(); implementation p() { start: assume {:inferred} true; assume x < y; assume {:inferred} true; return; } Boogie program verifier finished with 0 verified, 0 errors