Skip to content

GitLab

Commit ab0785fa authored by MARCHE Claude's avatar MARCHE Claude
Browse files

update obsolete proofs

parent 7f923798
Hide whitespace changes
Inline Side-by-side
Showing with 777 additions and 747 deletions
examples/check-builtin/intreal/why3session.xml
View file @ ab0785fa
......@@ -40,7 +40,7 @@
name="G1"
locfile="check-builtin/intreal/../intreal.why"
loclnum="7" loccnumb="7" loccnume="9"
sum="20afd849649327f8ce871cf32df073a5"
sum="f471c6c924b564aee8f4934746236ec5"
proved="true"
expanded="false"
shape="ainfix =afrom_intc2c2.0">
......@@ -56,7 +56,7 @@
timelimit="10"
obsolete="false"
archived="false">
<result status="timeout" time="10.23"/>
<result status="timeout" time="10.39"/>
</proof>
<proof
prover="0"
......@@ -84,14 +84,14 @@
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="0.07"/>
<result status="valid" time="0.08"/>
</proof>
</goal>
<goal
name="G2"
locfile="check-builtin/intreal/../intreal.why"
loclnum="8" loccnumb="7" loccnume="9"
sum="a57fa086b524e91e1f4709c5fffd0414"
sum="a03422ffac4ca142a1a0e2945b8150b1"
proved="true"
expanded="false"
shape="ainfix =afloorc1.5c1">
......@@ -100,35 +100,35 @@
timelimit="10"
obsolete="false"
archived="false">
<result status="timeout" time="10.08"/>
<result status="timeout" time="10.12"/>
</proof>
<proof
prover="3"
timelimit="10"
obsolete="false"
archived="false">
<result status="timeout" time="10.36"/>
<result status="timeout" time="10.04"/>
</proof>
<proof
prover="0"
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="3.36"/>
<result status="valid" time="3.42"/>
</proof>
<proof
prover="5"
timelimit="10"
obsolete="false"
archived="false">
<result status="timeout" time="10.09"/>
<result status="timeout" time="10.13"/>
</proof>
</goal>
<goal
name="G3"
locfile="check-builtin/intreal/../intreal.why"
loclnum="9" loccnumb="7" loccnume="9"
sum="2ad04c0284892aba197a2bdb696ea487"
sum="5a0b387c12f9700c3e3c3646efbd68aa"
proved="true"
expanded="false"
shape="ainfix =aceilc1.5c2">
......@@ -137,35 +137,35 @@
timelimit="10"
obsolete="false"
archived="false">
<result status="timeout" time="10.09"/>
<result status="timeout" time="10.13"/>
</proof>
<proof
prover="3"
timelimit="10"
obsolete="false"
archived="false">
<result status="timeout" time="10.51"/>
<result status="timeout" time="10.22"/>
</proof>
<proof
prover="0"
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="4.08"/>
<result status="valid" time="3.94"/>
</proof>
<proof
prover="5"
timelimit="10"
obsolete="false"
archived="false">
<result status="timeout" time="10.09"/>
<result status="timeout" time="10.13"/>
</proof>
</goal>
<goal
name="G4"
locfile="check-builtin/intreal/../intreal.why"
loclnum="10" loccnumb="7" loccnume="9"
sum="c51d63dbcb75d556d2a4263d111c77e0"
sum="350db14fcb4c074460205c9f3bdfb7d7"
proved="false"
expanded="false"
shape="ainfix =aflooraprefix -.c1.5aprefix -c2">
......@@ -174,35 +174,35 @@
timelimit="10"
obsolete="false"
archived="false">
<result status="timeout" time="10.09"/>
<result status="timeout" time="10.13"/>
</proof>
<proof
prover="3"
timelimit="10"
obsolete="false"
archived="false">
<result status="timeout" time="10.28"/>
<result status="timeout" time="10.10"/>
</proof>
<proof
prover="0"
timelimit="10"
obsolete="false"
archived="false">
<result status="timeout" time="10.08"/>
<result status="timeout" time="10.03"/>
</proof>
<proof
prover="5"
timelimit="10"
obsolete="false"
archived="false">
<result status="timeout" time="10.10"/>
<result status="timeout" time="10.13"/>
</proof>
</goal>
<goal
name="G5"
locfile="check-builtin/intreal/../intreal.why"
loclnum="11" loccnumb="7" loccnume="9"
sum="714563f1666f1a4fa77b3bd8828d1e0f"
sum="fe76735f57427088f9dc7c492260de1d"
proved="false"
expanded="false"
shape="ainfix =aceilaprefix -.c1.5aprefix -c1">
......@@ -211,35 +211,35 @@
timelimit="10"
obsolete="false"
archived="false">
<result status="timeout" time="10.10"/>
<result status="timeout" time="10.13"/>
</proof>
<proof
prover="3"
timelimit="10"
obsolete="false"
archived="false">
<result status="timeout" time="10.49"/>
<result status="timeout" time="10.38"/>
</proof>
<proof
prover="0"
timelimit="10"
obsolete="false"
archived="false">
<result status="timeout" time="10.08"/>
<result status="timeout" time="10.02"/>
</proof>
<proof
prover="5"
timelimit="10"
obsolete="false"
archived="false">
<result status="timeout" time="10.09"/>
<result status="timeout" time="10.13"/>
</proof>
</goal>
<goal
name="G6"
locfile="check-builtin/intreal/../intreal.why"
loclnum="12" loccnumb="7" loccnume="9"
sum="c4a1742575b0745b9ae2635176e84016"
sum="35b4ccc44d873f0925f27ecf4bc7ebe1"
proved="true"
expanded="false"
shape="ainfix <=afloorV0aceilV0F">
......@@ -248,14 +248,14 @@
timelimit="10"
obsolete="false"
archived="false">
<result status="timeout" time="10.09"/>
<result status="timeout" time="10.13"/>
</proof>
<proof
prover="3"
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="0.31"/>
<result status="valid" time="0.28"/>
</proof>
<proof
prover="0"
......@@ -283,14 +283,14 @@
timelimit="10"
obsolete="false"
archived="false">
<result status="timeout" time="10.10"/>
<result status="timeout" time="10.13"/>
</proof>
</goal>
<goal
name="G7"
locfile="check-builtin/intreal/../intreal.why"
loclnum="13" loccnumb="7" loccnume="9"
sum="5d3b163e24b215d6a71ec79674c9ec54"
sum="ef9cf6577bfe5fa811d8cab87076ba52"
proved="true"
expanded="false"
shape="ainfix =afrom_intafloorV0V0NIainfix <afloorV0aceilV0F">
......@@ -306,7 +306,7 @@
timelimit="10"
obsolete="false"
archived="false">
<result status="timeout" time="10.24"/>
<result status="timeout" time="10.03"/>
</proof>
<proof
prover="0"
......
examples/einstein/why3session.xml
View file @ ab0785fa
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session
name="examples/einstein/why3session.xml">
name="./einstein/why3session.xml">
<prover
id="0"
name="Alt-Ergo"
......@@ -41,17 +41,17 @@
<file
name="../einstein.why"
verified="false"
expanded="true">
expanded="false">
<theory
name="Bijection"
locfile="examples/einstein/../einstein.why"
locfile="./einstein/../einstein.why"
loclnum="7" loccnumb="7" loccnume="16"
verified="true"
expanded="true">
</theory>
<theory
name="Einstein"
locfile="examples/einstein/../einstein.why"
locfile="./einstein/../einstein.why"
loclnum="18" loccnumb="7" loccnume="15"
verified="true"
expanded="true">
......@@ -61,7 +61,7 @@
</theory>
<theory
name="EinsteinClues"
locfile="examples/einstein/../einstein.why"
locfile="./einstein/../einstein.why"
loclnum="51" loccnumb="7" loccnume="20"
verified="true"
expanded="true">
......@@ -71,7 +71,7 @@
</theory>
<theory
name="Goals"
locfile="examples/einstein/../einstein.why"
locfile="./einstein/../einstein.why"
loclnum="107" loccnumb="7" loccnume="12"
verified="false"
expanded="true">
......@@ -80,9 +80,9 @@
</label>
<goal
name="G1"
locfile="examples/einstein/../einstein.why"
locfile="./einstein/../einstein.why"
loclnum="125" loccnumb="7" loccnume="9"
sum="b29963ab2946f6e953e24adc18bc2422"
sum="06ba27fea40ec01abe97b14656973ae0"
proved="true"
expanded="true"
shape="ainfix =ato_aFishaGerman">
......@@ -98,28 +98,28 @@
timelimit="3"
obsolete="false"
archived="false">
<result status="timeout" time="2.99"/>
<result status="timeout" time="3.02"/>
</proof>
<proof
prover="0"
timelimit="10"
obsolete="false"
archived="false">
<result status="unknown" time="0.17"/>
<result status="unknown" time="8.48"/>
</proof>
<proof
prover="1"
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="2.53"/>
<result status="valid" time="2.41"/>
</proof>
<proof
prover="2"
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="2.27"/>
<result status="valid" time="2.25"/>
</proof>
<proof
prover="8"
......@@ -133,28 +133,28 @@
timelimit="3"
obsolete="false"
archived="false">
<result status="unknown" time="2.99"/>
<result status="unknown" time="3.00"/>
</proof>
<proof
prover="6"
timelimit="3"
obsolete="false"
archived="false">
<result status="timeout" time="3.02"/>
<result status="timeout" time="3.11"/>
</proof>
<proof
prover="3"
timelimit="3"
obsolete="false"
archived="false">
<result status="timeout" time="2.98"/>
<result status="timeout" time="2.99"/>
</proof>
</goal>
<goal
name="Wrong"
locfile="examples/einstein/../einstein.why"
locfile="./einstein/../einstein.why"
loclnum="126" loccnumb="7" loccnume="12"
sum="b6ada39e4ed1ac554d7bdbccbfadcff3"
sum="db47bc1012a788c5c3b9e23ade3d9ad3"
proved="false"
expanded="true"
shape="ainfix =ato_aCatsaSwede">
......@@ -163,7 +163,7 @@
timelimit="10"
obsolete="false"
archived="false">
<result status="timeout" time="10.08"/>
<result status="timeout" time="10.02"/>
</proof>
<proof
prover="4"
......@@ -177,56 +177,56 @@
timelimit="10"
obsolete="false"
archived="false">
<result status="unknown" time="0.17"/>
<result status="unknown" time="6.99"/>
</proof>
<proof
prover="1"
timelimit="10"
obsolete="false"
archived="false">
<result status="timeout" time="10.08"/>
<result status="timeout" time="10.03"/>
</proof>
<proof
prover="2"
timelimit="10"
obsolete="false"
archived="false">
<result status="timeout" time="10.08"/>
<result status="timeout" time="10.13"/>
</proof>
<proof
prover="8"
timelimit="2"
obsolete="false"
archived="false">
<result status="timeout" time="2.02"/>
<result status="timeout" time="2.00"/>
</proof>
<proof
prover="5"
timelimit="3"
obsolete="false"
archived="false">
<result status="unknown" time="2.99"/>
<result status="unknown" time="3.00"/>
</proof>
<proof
prover="6"
timelimit="3"
obsolete="false"
archived="false">
<result status="timeout" time="3.02"/>
<result status="timeout" time="3.01"/>
</proof>
<proof
prover="3"
timelimit="3"
obsolete="false"
archived="false">
<result status="timeout" time="2.98"/>
<result status="timeout" time="2.99"/>
</proof>
</goal>
<goal
name="G2"
locfile="examples/einstein/../einstein.why"
locfile="./einstein/../einstein.why"
loclnum="127" loccnumb="7" loccnume="9"
sum="ad118f1b69459bb42f50fa8c2063d069"
sum="b1175583f277129e0f204fae414ad8ca"
proved="true"
expanded="true"
shape="ainfix =ato_aCatsaNorwegian">
......@@ -242,56 +242,56 @@
timelimit="3"
obsolete="false"
archived="false">
<result status="timeout" time="3.05"/>
<result status="timeout" time="3.00"/>
</proof>
<proof
prover="0"
timelimit="10"
obsolete="false"
archived="false">
<result status="unknown" time="0.18"/>
<result status="unknown" time="6.93"/>
</proof>
<proof
prover="1"
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="1.99"/>
<result status="valid" time="2.00"/>
</proof>
<proof
prover="2"
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="2.21"/>
<result status="valid" time="2.14"/>
</proof>
<proof
prover="8"
timelimit="2"
obsolete="false"
archived="false">
<result status="valid" time="0.05"/>
<result status="valid" time="0.04"/>
</proof>
<proof
prover="5"
timelimit="3"
obsolete="false"
archived="false">
<result status="unknown" time="3.01"/>
<result status="unknown" time="3.03"/>
</proof>
<proof
prover="6"
timelimit="3"
obsolete="false"
archived="false">
<result status="timeout" time="3.02"/>
<result status="timeout" time="3.11"/>
</proof>
<proof
prover="3"
timelimit="3"
obsolete="false"
archived="false">
<result status="timeout" time="2.98"/>
<result status="timeout" time="3.00"/>
</proof>
</goal>
</theory>
......
examples/hello_proof/why3session.xml
View file @ ab0785fa
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session
name="hello_proof/why3session.xml">
name="./hello_proof/why3session.xml">
<prover
id="alt-ergo"
id="0"
name="Alt-Ergo"
version="0.94"/>
<prover
id="coq"
name="Coq"
version="8.3pl3"/>
<prover
id="cvc3-2.2"
id="1"
name="CVC3"
version="2.2"/>
<prover
id="cvc3-2.4"
id="2"
name="CVC3"
version="2.4.1"/>
<prover
id="eprover"
name="Eprover"
version="1.4"/>
<prover
id="gappa"
name="Gappa"
version="0.15.1"/>
id="3"
name="Coq"
version="8.3pl3"/>
<prover
id="simplify"
id="4"
name="Simplify"
version="1.5.4"/>
<prover
id="spass"
name="Spass"
version="3.7"/>
<prover
id="vampire"
name="Vampire"
version="0.6"/>
<prover
id="verit"
name="veriT"
version="dev"/>
<prover
id="yices"
name="Yices"
version="1.0.25"/>
<prover
id="z3-2"
id="5"
name="Z3"
version="2.19"/>
<prover
id="z3-3"
id="6"
name="Z3"
version="3.2"/>
<file
name="../hello_proof.why"
verified="false"
expanded="true">
expanded="false">
<theory
name="HelloProof"
locfile="./hello_proof/../hello_proof.why"
loclnum="1" loccnumb="7" loccnume="17"
verified="false"
expanded="true">
<label
name="My very first Why3 theory">
</label>
<goal
name="G1"
sum="770f70aa36289c763128092468f7b8be"
locfile="./hello_proof/../hello_proof.why"
loclnum="3" loccnumb="7" loccnume="9"
sum="4daf9675e70ee6481b1153fe95f7c750"
proved="true"
expanded="true"
shape="t">
<proof
prover="z3-2"
prover="5"
timelimit="5"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="z3-3"
timelimit="2"
edited=""
obsolete="false">
prover="0"
timelimit="5"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="alt-ergo"
prover="1"
timelimit="5"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="cvc3-2.2"
prover="2"
timelimit="5"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>