#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], b[10];
  
  $assert(eq(a, 10, b));
}