mattulbrich / dive

Dafny Interactive Verification Environment (DIVE)
GNU General Public License v3.0
4 stars 0 forks source link

updated sequence variables are not considered for anonymisation #185

Closed mattulbrich closed 3 years ago

mattulbrich commented 4 years ago

Currently the assignment to r is overlooked in the following such that this verifies (and should not):

method m() 
{
   var r := [42];
   while(r[0] > 0) {
      r[0] := 0;
   }
   assert r[0] == 42;
}
mattulbrich commented 4 years ago

There is a branch fix-185 adding a failing test case.