Reverse a stack using Dafny

Question

I'm learning Dafny and could not find a solution for this problem yet. I have this method that reverses a stack, poping from a stack and pushing into another. But it doesnt work, since dafny points that "A postcondition might not hold on this return path." on method Reverse.

var arr: array<nat>;
var tail: nat;
const initialSize := 5;

ghost var Content: seq<nat>;


predicate Reversed(seq1:seq<nat>, seq2: seq<nat>)
    requires |seq1| > 0
    requires |seq1| == |seq2|
{
    forall j :: 0 <= j < |seq1| ==> seq1[j] == seq2[|seq1|-1-j]
}

A postcondition might not hold on this return path. Verifier
Stack.dfy(88, 12): This is the postcondition that might not hold.
Stack.dfy(10, 15): Related location < Reversed predicate

method Reverse()
    requires |Content| > 0
    ensures old(|Content|) == |Content|
    ensures Reversed(old(Content), Content)
{
    var newArray := new nat[arr.Length];
    var newTail := 0;
    ghost var newContent: seq<nat>;
    var element;
    while(tail>0)
        // invariant Content[|Content|-1] == newContent[|newContent|-1]
    {
        // Pop from old stack
        tail := tail - 1;
        element := arr[tail];
        Content := arr[0..tail];
        // Push into new stack
        newArray[newTail] := element;
        newTail := newTail + 1;
        newContent := newContent + [element];
    }

    arr := newArray;
    tail:= newTail;
    Content := newContent;
}

I already tried to figure out some loop invariants but without success.

Edit: I'm using autocontracts