Why does Dafny fails to verify this simple code?

I'm trying to prove certain properties of integer lists hold. To begin with it, I wrote method Check1 below, utilizing a method given by CoPilot.

method FlipSeq(s: seq<int>) returns (res: seq<int>)
  ensures |s| == |res|
{
  res := [];
  var i := 0;

  while i < |s|
    invariant 0 <= i <= |s|
    invariant |res| == i
    invariant forall j :: 0 <= j < i ==> res[j] == if s[j] == 1 then 0 else 1
  {
    res := res + [if s[i] == 1 then 0 else 1];
    i := i + 1;
  }
}

method Check1()
{
  var xs := [0, 1, 0, 1, 0, 1];
  var ys := FlipSeq(xs);  //  [1, 0, 1, 0, 1, 0]

  assert xs[0] != ys[0];
}

Now Dafny says the assertion might not hold in Check1(). I have no idea what's wrong here. Thanks for any help.

In Dafny when you call a method it only remembers/asserts whatever is in your post conditions (i.e the ensures). If you use a function Dafny will evaluate the function body to verify. So you were missing an ensure statement about what your method did to the result.

predicate IsBinary(num: int) {
    num == 0 || num == 1
}

predicate IsBinarySeq(s: seq<int>) {
    // forall i :: 0 <= i < |s| ==> (s[i] == 0 || s[i] == 1)
    forall i :: 0 <= i < |s| ==> IsBinary(s[i])
}

function Flip(num: int): int 
    requires IsBinary(num)
    ensures IsBinary(Flip(num))
{
    if num == 1 then 0 else 1
}

function FlipS(s: seq<int>): seq<int> 
    requires IsBinarySeq(s)
    ensures IsBinarySeq(FlipS(s))
{
    if s == [] then [] else (if s[0] == 1 then [0] else [1])+FlipS(s[1..])
}

method FlipSeq(s: seq<int>) returns (res: seq<int>)
  requires IsBinarySeq(s)
  ensures |s| == |res|
  ensures forall i :: 0 <= i < |res| ==> res[i] == Flip(s[i])
{
  res := [];
  var i := 0;

  while i < |s|
    invariant 0 <= i <= |s|
    invariant |res| == i
    invariant forall j :: 0 <= j < i ==> res[j] == if s[j] == 1 then 0 else 1
  {
    res := res + [if s[i] == 1 then 0 else 1];
    i := i + 1;
  }
}

method Check1()
{
  var xs := [0, 1, 0, 1, 0, 1];
  assert IsBinarySeq(xs);
  var ys := FlipSeq(xs);  //  [1, 0, 1, 0, 1, 0]
  var zs := FlipS(xs);
  assert zs[0] != xs[0];

  assert xs[0] != ys[0];
}