Commit 87187479 authored by Jean-Christophe's avatar Jean-Christophe

updated example

parent 50460793
......@@ -31,3 +31,9 @@ module Fill
(forall i: int. start <= i < result -> contains t a[i]) }
end
(*
Local Variables:
compile-command: "why3ide fill.mlw"
End:
*)
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session
name="examples/programs/fill/why3session.xml">
name="fill/why3session.xml">
<prover
id="0"
name="Alt-Ergo"
......@@ -14,27 +14,19 @@
id="2"
name="CVC3"
version="2.4.1"/>
<prover
id="3"
name="Z3"
version="2.19"/>
<prover
id="4"
name="Z3"
version="3.2"/>
<file
name="../fill.mlw"
verified="true"
expanded="true">
<theory
name="WP Fill"
locfile="examples/programs/fill/../fill.mlw"
locfile="fill/../fill.mlw"
loclnum="4" loccnumb="7" loccnume="11"
verified="true"
expanded="true">
<goal
name="WP_parameter fill"
locfile="examples/programs/fill/../fill.mlw"
locfile="fill/../fill.mlw"
loclnum="16" loccnumb="10" loccnume="14"
expl="parameter fill"
sum="a7f6d0a4fd8b99196978e39ff255fcf5"
......@@ -44,41 +36,24 @@
<label
name="expl:parameter fill">
</label>
<proof
prover="3"
timelimit="10"
obsolete="false"
archived="false">
<result status="unknown" time="0.18"/>
</proof>
<proof
prover="1"
timelimit="10"
obsolete="false"
archived="false">
obsolete="false">
<result status="valid" time="0.05"/>
</proof>
<proof
prover="0"
timelimit="10"
obsolete="false"
archived="false">
obsolete="false">
<result status="valid" time="0.05"/>
</proof>
<proof
prover="2"
timelimit="10"
obsolete="false"
archived="false">
obsolete="false">
<result status="valid" time="0.10"/>
</proof>
<proof
prover="4"
timelimit="10"
obsolete="false"
archived="false">
<result status="timeout" time="10.10"/>
</proof>
</goal>
</theory>
</file>
......
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