Commit fa8c97b5 authored by Sylvain Dailler's avatar Sylvain Dailler

Add test for issue 116

parent f42a7ddf
module Test
use array.Array
use mach.array.Array63
constant d: Array.array int
constant e: Array63.array int
(* goal a: e[1] = 5*)
goal c: Array.([]) d 3 = 5
(* goal g: Array63.([]) e 3 = 5 *)
end
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="5">
<file name="../116_array_access.mlw" proved="true">
<theory name="Test">
<goal name="c">
</goal>
</theory>
</file>
</why3session>
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment