The correct solution to the problem is the following:

class A {
    var x : int 
    var y : int

  }

  class B 
  {
    const l : seq<A>

    method m()
        modifies (set a | a in l)`x
        ensures forall a :: a in l ==> a.x == 10
        ensures forall a :: a in l ==>  unchanged(a`y)
    {
       var it := 0;
       while it < |l|
            invariant 0 <= it <= |l|
            invariant forall a :: a in l[..it] ==> a.x == 10
        {
            l[it].x := 10;
            it := it + 1;
        }
    }
  }