The correct answer was:

method search(a: array<int>) returns (i: int)
  requires a.Length > 1 && a[0] == a[a.Length-1]
  ensures 0 <= i < a.Length-1 && a[i] >= a[i+1]
{  
  i := a.Length - 2;
  var j := 0;
  while i != j
    invariant 0 <= j <= i < a.Length - 1 && a[j] >= a[i + 1]
  {
    var m := (i + j) / 2;

    if a[j] >= a[m + 1]{
      i := m;
    } else {
      j := m + 1;
    }
  }
}