blob: 5adced6d870497b0f64bb45104c8f4257c17e935 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
function {:inline true} foo(x: int) : bool
{
x > 0
}
function {:inline false} foo2(x: int) : bool;
axiom (forall x: int :: {:inline false} { foo2(x): bool } foo2(x): bool == (x > 0));
function foo3(x: int) : bool;
axiom (forall x: int :: { foo3(x): bool } foo3(x): bool == (x > 0));
Boogie program verifier finished with 0 verified, 0 errors
|
