source: CIVL/mods/dev.civl.com/examples/ACSLTransformation/acslLogicFunctionsBad.cvl@ cb4d4f4

$input int a[10][10];
$input int b[10];

#pragma CIVL ACSL

/*@ logic int f(int[10] *a) = a[0][0];
  @
  @ logic int g(int *a) = a[0];
  @*/

int main() {
  //@ assert a[0][0] == b[1] ==> f(a) != g(b+1);
  return 0;
}