examples/bts/116_array_access.mlw

   1 module Test
   2
   3   use array.Array
   4   use mach.array.Array63
   5
   6   constant d: Array.array int
   7   val e: Array63.array int
   8
   9   goal a: d[1] = 5
  10
  11   let f i =
  12     e[i] <- 5;
  13     e[i]
  14
  15   goal c: d[3] = 5
  16
  17 end