typedef /*@abstract@*/ /*@mutable@*/ int *tam;
typedef /*@abstract@*/ /*@immutable@*/ int *tai;
typedef /*@abstract@*/ /*@immutable@*/ int *tmixm; /* 1. inconsistently declared as immutable */
typedef /*@abstract@*/ /*@immutable@*/ int *tmixa; /* 2. inconsistently declared as abstract type */
typedef /*@abstract@*/ /*@mutable@*/   int *tmixi; /* 3. inconsistently declared as mutable */
typedef /*@mutable@*/ int *tm;
typedef /*@immutable@*/ int *ti;