Using old and predicates in post condition can confuse Dafny?

Mar 29, 2014 at 6:15 AM
We have been trying to ponder why this code does not work with predicates.

We have two predicates not_eq and not_eq_ex

static predicate not_eq(a:array<int>, b:array<int>)
requires a!=null;
requires b!=null;
requires a.Length == b.Length;
reads a;
reads b;
{
//a.Length != b.Length ||
!(forall x:: 0 <= x < a.Length ==> a[x] == b[x])
}

static predicate not_eq_ex(a:array<int>, b:array<int>)
requires a!=null;
requires b!=null;
requires a.Length == b.Length;
reads a;
reads b;
{
//a.Length != b.Length ||
exists y:: 0 <= y < a.Length && a[y] != b[y]
}

static method Main(a:array<int>)
requires a != null && a.Length > 0;
requires a[0] == 4;
modifies a;
ensures old(a[0]) != a[0];
// ensures not_eq(a, old(a)); //--- LINE 1
// ensures not_eq_ex(a, old(a)); //--- LINE 2
//These are just copy pasted and s/b[x]/old(a[x])/ from above
ensures exists y:: 0 <= y < a.Length && a[y] != old(a[y]);
ensures !(forall x:: 0 <= x < a.Length ==> (a[x] == old(a[x])));
{
a[0] := 5;
return;
}

Dafny verifies the above code. However when we uncomment LINE 1 and LINE 2, Dafny complains about postcondition not being satisfied.

The predicates in LINE 1 and LINE 2 are exactly what we say in the subsequent lines.

What is wrong with our understanding here?