Commit 188182e0 authored by MARCHE Claude's avatar MARCHE Claude

update proof sessions

parent 70a028ad
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<why3session
name="./einstein/why3session.xml">
name="examples/einstein/why3session.xml">
<prover
id="0"
name="Alt-Ergo"
version="0.94"/>
<prover
id="1"
name="Alt-Ergo"
version="0.95-dev"/>
<prover
id="2"
name="CVC3"
version="2.2"/>
<prover
id="2"
id="3"
name="CVC3"
version="2.4.1"/>
<prover
id="3"
id="4"
name="Eprover"
version="1.4"/>
<prover
id="4"
id="5"
name="Simplify"
version="1.5.4"/>
<prover
id="6"
name="Spass"
version="3.7"/>
<prover
id="5"
id="7"
name="Vampire"
version="0.6"/>
<prover
id="6"
id="8"
name="Yices"
version="1.0.25"/>
<prover
id="7"
id="9"
name="Z3"
version="2.19"/>
<prover
id="8"
id="10"
name="Z3"
version="3.2"/>
<file
name="../einstein.why"
verified="false"
expanded="false">
expanded="true">
<theory
name="Bijection"
locfile="./einstein/../einstein.why"
locfile="examples/einstein/../einstein.why"
loclnum="7" loccnumb="7" loccnume="16"
verified="true"
expanded="true">
</theory>
<theory
name="Einstein"
locfile="./einstein/../einstein.why"
locfile="examples/einstein/../einstein.why"
loclnum="18" loccnumb="7" loccnume="15"
verified="true"
expanded="true">
......@@ -60,7 +68,7 @@
</theory>
<theory
name="EinsteinClues"
locfile="./einstein/../einstein.why"
locfile="examples/einstein/../einstein.why"
loclnum="51" loccnumb="7" loccnume="20"
verified="true"
expanded="true">
......@@ -69,7 +77,7 @@
</theory>
<theory
name="Goals"
locfile="./einstein/../einstein.why"
locfile="examples/einstein/../einstein.why"
loclnum="107" loccnumb="7" loccnume="12"
verified="false"
expanded="true">
......@@ -77,27 +85,27 @@
name="Goals about Einstein&apos;s problem"/>
<goal
name="G1"
locfile="./einstein/../einstein.why"
locfile="examples/einstein/../einstein.why"
loclnum="125" loccnumb="7" loccnume="9"
sum="06ba27fea40ec01abe97b14656973ae0"
proved="true"
expanded="true"
shape="ainfix =ato_aFishaGerman">
<proof
prover="7"
prover="9"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
<result status="valid" time="0.03"/>
</proof>
<proof
prover="4"
prover="6"
timelimit="3"
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="2.86"/>
<result status="timeout" time="3.01"/>
</proof>
<proof
prover="0"
......@@ -105,80 +113,96 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="unknown" time="9.93"/>
<result status="unknown" time="9.74"/>
</proof>
<proof
prover="1"
prover="2"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="3.22"/>
<result status="valid" time="2.69"/>
</proof>
<proof
prover="2"
prover="3"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="2.74"/>
<result status="valid" time="2.33"/>
</proof>
<proof
prover="8"
timelimit="2"
memlimit="0"
prover="7"
timelimit="10"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.06"/>
<result status="unknown" time="9.96"/>
</proof>
<proof
prover="5"
timelimit="116"
timelimit="10"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="10.18"/>
</proof>
<proof
prover="10"
timelimit="2"
memlimit="0"
obsolete="false"
archived="false">
<result status="unknown" time="92.88"/>
<result status="valid" time="0.06"/>
</proof>
<proof
prover="6"
prover="8"
timelimit="3"
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="4.21"/>
<result status="unknown" time="3.02"/>
</proof>
<proof
prover="3"
prover="1"
timelimit="10"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="8.01"/>
</proof>
<proof
prover="4"
timelimit="3"
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="2.99"/>
<result status="timeout" time="2.98"/>
</proof>
</goal>
<goal
name="Wrong"
locfile="./einstein/../einstein.why"
locfile="examples/einstein/../einstein.why"
loclnum="126" loccnumb="7" loccnume="12"
sum="db47bc1012a788c5c3b9e23ade3d9ad3"
proved="false"
expanded="true"
shape="ainfix =ato_aCatsaSwede">
<proof
prover="7"
prover="9"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="11.82"/>
<result status="timeout" time="10.07"/>
</proof>
<proof
prover="4"
prover="6"
timelimit="3"
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="2.41"/>
<result status="timeout" time="3.00"/>
</proof>
<proof
prover="0"
......@@ -186,67 +210,83 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="unknown" time="7.32"/>
<result status="unknown" time="7.03"/>
</proof>
<proof
prover="1"
prover="2"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="10.12"/>
<result status="timeout" time="10.04"/>
</proof>
<proof
prover="2"
prover="3"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="11.92"/>
<result status="timeout" time="10.08"/>
</proof>
<proof
prover="8"
timelimit="2"
memlimit="0"
prover="7"
timelimit="10"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="2.71"/>
<result status="unknown" time="9.94"/>
</proof>
<proof
prover="5"
timelimit="116"
timelimit="10"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="10.01"/>
</proof>
<proof
prover="10"
timelimit="2"
memlimit="0"
obsolete="false"
archived="false">
<result status="unknown" time="103.29"/>
<result status="timeout" time="2.07"/>
</proof>
<proof
prover="6"
prover="8"
timelimit="3"
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="3.71"/>
<result status="unknown" time="3.05"/>
</proof>
<proof
prover="3"
prover="1"
timelimit="10"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="6.53"/>
</proof>
<proof
prover="4"
timelimit="3"
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="2.99"/>
<result status="timeout" time="2.98"/>
</proof>
</goal>
<goal
name="G2"
locfile="./einstein/../einstein.why"
locfile="examples/einstein/../einstein.why"
loclnum="127" loccnumb="7" loccnume="9"
sum="b1175583f277129e0f204fae414ad8ca"
proved="true"
expanded="true"
shape="ainfix =ato_aCatsaNorwegian">
<proof
prover="7"
prover="9"
timelimit="10"
memlimit="0"
obsolete="false"
......@@ -254,12 +294,12 @@
<result status="valid" time="0.03"/>
</proof>
<proof
prover="4"
prover="6"
timelimit="3"
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="2.40"/>
<result status="timeout" time="2.99"/>
</proof>
<proof
prover="0"
......@@ -267,50 +307,66 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="unknown" time="7.32"/>
<result status="unknown" time="7.01"/>
</proof>
<proof
prover="1"
prover="2"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="2.42"/>
<result status="valid" time="2.02"/>
</proof>
<proof
prover="2"
prover="3"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="2.76"/>
<result status="valid" time="2.14"/>
</proof>
<proof
prover="8"
timelimit="2"
memlimit="0"
prover="5"
timelimit="10"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.06"/>
<result status="timeout" time="10.03"/>
</proof>
<proof
prover="5"
timelimit="116"
prover="7"
timelimit="10"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="9.92"/>
</proof>
<proof
prover="10"
timelimit="2"
memlimit="0"
obsolete="false"
archived="false">
<result status="unknown" time="108.01"/>
<result status="valid" time="0.05"/>
</proof>
<proof
prover="6"
prover="8"
timelimit="3"
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="3.11"/>
<result status="unknown" time="3.04"/>
</proof>
<proof
prover="3"
prover="1"
timelimit="10"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="6.56"/>
</proof>
<proof
prover="4"
timelimit="3"
memlimit="0"
obsolete="false"
......
This diff is collapsed.
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/usr/local/share/why3/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<why3session
name="wp3/why3session.xml">
name="examples/hoare_logic/wp3/why3session.xml">
<prover
id="0"
name="Alt-Ergo"
......@@ -16,6 +16,10 @@
version="8.3pl3"/>
<prover
id="3"
name="Coq"
version="8.3pl4"/>
<prover
id="4"
name="Z3"
version="3.2"/>
<file
......@@ -24,13 +28,13 @@
expanded="true">
<theory
name="ImpExpr"
locfile="wp3/../wp3.mlw"
locfile="examples/hoare_logic/wp3/../wp3.mlw"
loclnum="6" loccnumb="7" loccnume="14"
verified="false"
expanded="true">
<goal
name="eval_subst_term"
locfile="wp3/../wp3.mlw"
locfile="examples/hoare_logic/wp3/../wp3.mlw"
loclnum="101" loccnumb="6" loccnume="21"
sum="ef98d2b97884863e1cbe533969818f1f"
proved="false"
......@@ -40,30 +44,30 @@
prover="0"
timelimit="2"
memlimit="1000"
obsolete="true"
obsolete="false"
archived="false">
<result status="unknown" time="0.24"/>
<result status="unknown" time="0.16"/>
</proof>
<proof
prover="1"
timelimit="2"
memlimit="1000"
obsolete="true"
obsolete="false"
archived="false">
<result status="timeout" time="2.19"/>
<result status="timeout" time="2.08"/>
</proof>
<proof
prover="3"
prover="4"
timelimit="2"
memlimit="1000"
obsolete="true"
obsolete="false"
archived="false">
<result status="timeout" time="2.28"/>
<result status="timeout" time="2.09"/>
</proof>
</goal>
<goal
name="eval_term_change_free"
locfile="wp3/../wp3.mlw"
locfile="examples/hoare_logic/wp3/../wp3.mlw"
loclnum="107" loccnumb="6" loccnume="27"
sum="430b7d02bdb3f2e8cec81e288e46c026"
proved="false"
......@@ -73,30 +77,30 @@
prover="0"
timelimit="2"
memlimit="1000"
obsolete="true"
obsolete="false"
archived="false">
<result status="unknown" time="0.21"/>
<result status="unknown" time="0.15"/>
</proof>
<proof
prover="1"
timelimit="2"
memlimit="1000"
obsolete="true"
obsolete="false"
archived="false">
<result status="timeout" time="2.10"/>
<result status="timeout" time="2.06"/>
</proof>
<proof
prover="3"
prover="4"
timelimit="2"
memlimit="1000"
obsolete="true"
obsolete="false"
archived="false">
<result status="timeout" time="2.08"/>
<result status="timeout" time="2.01"/>
</proof>
</goal>
<goal
name="eval_subst"
locfile="wp3/../wp3.mlw"
locfile="examples/hoare_logic/wp3/../wp3.mlw"
loclnum="133" loccnumb="6" loccnume="16"
sum="b9e2179371c7b6be3e45cd792f8954a3"
proved="false"
......@@ -106,63 +110,63 @@
prover="0"
timelimit="2"
memlimit="1000"
obsolete="true"
obsolete="false"
archived="false">
<result status="unknown" time="0.11"/>
<result status="unknown" time="0.07"/>
</proof>
<proof
prover="1"
timelimit="2"
memlimit="1000"
obsolete="true"
obsolete="false"
archived="false">
<result status="timeout" time="2.11"/>
<result status="timeout" time="2.06"/>
</proof>
<proof
prover="3"
prover="4"
timelimit="2"
memlimit="1000"
obsolete="true"
obsolete="false"
archived="false">
<result status="timeout" time="2.19"/>
<result status="timeout" time="2.06"/>
</proof>
</goal>
<goal
name="eval_swap"
locfile="wp3/../wp3.mlw"
locfile="examples/hoare_logic/wp3/../wp3.mlw"
loclnum="139" loccnumb="6" loccnume="15"
sum="c507b815677e32c2dc3fa56fcbc973f8"
proved="false"
proved="true"
expanded="true"
shape="aeval_fmlaV1asetasetV2V4V6V3V5V0qaeval_fmlaV1asetasetV2V3V5V4V6V0Iainfix =V3V4NF">
<proof
prover="0"
timelimit="2"
memlimit="1000"
obsolete="true"
obsolete="false"
archived="false">
<result status="unknown" time="0.06"/>
<result status="unknown" time="0.02"/>
</proof>
<proof
prover="1"
timelimit="2"
memlimit="1000"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="3"
prover="4"
timelimit="2"
memlimit="1000"
obsolete="true"
obsolete="false"
archived="false">
<result status="timeout" time="2.10"/>
<result status="timeout" time="2.06"/>
</proof>
</goal>
<goal
name="eval_change_free"
locfile="wp3/../wp3.mlw"
locfile="examples/hoare_logic/wp3/../wp3.mlw"