Bug in Dafny's 1.9.1 console version

Dec 8, 2014 at 3:53 PM
When the following code is checked using the console version 1.9.1, in spite of the fact that the while loop should not be verified successfully, Dafny does not report any error.

class Bug {
  var list:array<int>;

  method Foo()
  modifies this`list;
  {
    list := new int[10];

    var i:int := 0;
    while (i < 10)
    decreases i;
    {
    }
  }
}

The problem seems to be in assignment to the array list, when it is placed as a variable of the class. If you remove the assignment, or you defined list as a local variable, then Dafny reports the expected error related to the loop.
Dec 8, 2014 at 4:34 PM
In fact, the previous bug can be reduced to what follows:

class Bug {
var arr : array<int>;

method Bla() {
    var s := new Bug;
    s.arr := new int[4];
    assert false;
}
}