@function max2: int, int -> int

@axiom A1: all x,y: int. x >= y ==> max2(x, y) = x

@axiom A2: all x,y: int. y >= x ==> max2(x, y) = y

@requires true

@ensures m = max2(x,y)

@program
     @var x, y,  m : int

     if (x >= y) 
	    m = x;
     else 
            m = y;
@end
--