-
Virgile Prevosto authored
Actions are sequential, which means that `$x=foo; $y = $x;` must be specified as `ensures aorai_y == aorai_x;`, not `\old(aorai_x)`.
029c9438
Actions are sequential, which means that `$x=foo; $y = $x;` must be specified as `ensures aorai_y == aorai_x;`, not `\old(aorai_x)`.