blob: 10181400d765dbc4bbc930d1b631aa238c3d477e (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
type ref;
function PLUS(int, int, int) returns (int);
function Rep(int, int) returns (int);
//PLUS(a,b,z)
// ERROR
axiom(forall a:int, b:int, z:int :: Rep(a,b) == Rep(a,0));
axiom(forall n:int, x:int :: {Rep(n,x)} (exists k:int :: Rep(n,x) == x));
// END ERROR
procedure main ( )
{
assert (PLUS(0, 4, 55)!=0);
}
|
