/* THIS FILE WAS GENERATED TO BE USED IN CADUCEUS
 *
 */
#include "liss_caduceus_list.h"
#include "liss_caduceus_set.h"

	/*@ ensures
	@ \result >= x && \result >= y &&
	@ \forall int z; z >= x && z >= y => z >= \result
	@*/
int max(int x, int y)
{
	int res = 0;

	if ((x >= y))
	{
		res = x;
	}
	else
	{
		res = y;
	}

	return res;
}

void main()
{
	int a = 2, b = 4, c = 0;

	c = max(a,b);

	/* THIS CODE LINES WILL NOT BE READ BY CADUCEUS
	printf("%d", c);
	printf("\n");
	*/

}
