bearophile Wrote: > /*@ assert (\forall int i; 0 <= i && i < n; a[i] != null); > This can be done with array op assert(a[0..n].notSame(null));