mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
18 lines
196 B
Plaintext
18 lines
196 B
Plaintext
module Test
|
|
|
|
use array.Array
|
|
use mach.array.Array63
|
|
|
|
constant d: Array.array int
|
|
val e: Array63.array int
|
|
|
|
goal a: d[1] = 5
|
|
|
|
let f i =
|
|
e[i] <- 5;
|
|
e[i]
|
|
|
|
goal c: d[3] = 5
|
|
|
|
end
|