Globalizing an Assertion
global: a == a0 
static int search(int a[], int v)
  { 
  for( int i = 0; i < a.length; i++ )
    {
    if( a[i] == v )
      {r = i;
      return i;
      }
    } r = -1;
  return -1;
  }
 [((   i) a[i] == v) ¨ a[r] == v] ^ [((   i) a[i] == v) ¨ r == -1]