struct INTEGER32 {
//	int value; // Ok
	long long value; // Fails
};

typedef struct INTEGER32 int32;

/*@
  	  requires \valid(x) && \valid(y);
	ensures A:  \valid(x);
*/
void add (int32* x, int32* y){
	int32 erg;
	erg.value = x->value + y->value;
}