#pragma CIVL ACSL

/*@ predicate eq(int *a[], int len, int * b) =
  @   \forall int i; 0 <= i && i < len ==> *a[i] == b[i];
  @*/
int main(){
  int * a[10];
  int b[10];
  
  $assert(eq(a, 10, b));
}