method toArrayConvert(s:seq<int>) returns(a:array<int>)
requires |s|>0;
ensures |s| == a.Length;
ensures multiset(s[..]) == multiset(old(s[..]))
ensures forall i::0<=i<a.Length ==> s[i] == a[i]; //This is the postcondition that might not hold.
{
  a :=new int[|s|];
  var i:int :=0;
  while i<|s|
  decreases |s| - i;
  invariant 0<=i<=|s|;
  invariant perm(a,old(a));
    {
        a[i]:=s[i];
        i:=i+1;
    }
  return a; //A postcondition might not hold on this return path.
}