sca misses channel polls in never claims.
See the following program:

chan q = [3] of {byte};

byte x;

init{
q! 23;
}

never{
do
:: q ? [x];
:: q ?? [x];
od;
}

Submitted by Kees Pronk on 29 August 2011 at 22:33

and also misses other side-effect free operations on channels such as len(q), empty(q) etc