Commit 0d48318f authored by MARCHE Claude's avatar MARCHE Claude

FoVeOOS competition

parent 3f02264b
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session
name="tree_max/why3session.xml">
<prover
id="alt-ergo"
name="Alt-Ergo"
version="0.93"/>
<prover
id="coq"
name="Coq"
version="8.2pl1"/>
<prover
id="coq-realize"
name="Coq Realize"
version="8.2pl1"/>
<prover
id="cvc3"
name="CVC3"
version="2.2"/>
<prover
id="eprover"
name="Eprover"
version="1.4 Namring"/>
<prover
id="gappa"
name="Gappa"
version="0.15.1"/>
<prover
id="simplify"
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"
name="Z3"
version="2.19"/>
<file
name="../tree_max.mlw"
verified="true"
expanded="true">
<theory
name="BinTree"
verified="true"
expanded="true">
<goal
name="ge_trans"
sum="e4503548ffd2c062100f2478dda74f40"
proved="true"
expanded="true"
shape="age_treeV1V0Iage_treeV2V0Aainfix >=V1V2F">
<proof
prover="coq"
timelimit="5"
edited="tree_max_BinTree_ge_trans_1.v"
obsolete="false">
<result status="valid" time="0.46"/>
</proof>
</goal>
</theory>
<theory
name="WP TreeMax"
verified="true"
expanded="true">
<goal
name="WP_parameter max_aux"
expl="parameter max_aux"
sum="e168cf51ea3d960886cfa60b8045edd4"
proved="true"
expanded="true"
shape="CV0aNullainfix >=V1V1Aage_treeV1V0aTreeVVVamemV6V0Oainfix =V6V1Aainfix >=V6V1Aage_treeV6V0IamemV6V3Oainfix =V6V5Aainfix >=V6V5Aage_treeV6V3FIamemV5V4Oainfix =V5amaxV2V1Aainfix >=V5amaxV2V1Aage_treeV5V4FFF">
<proof
prover="alt-ergo"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.06"/>
</proof>
<proof
prover="z3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="1.70"/>
</proof>
</goal>
<goal
name="WP_parameter max"
expl="parameter max"
sum="70efde547458e0084865db1d5c7c34f3"
proved="true"
expanded="true"
shape="CV0aNullfaTreeVVVamemV5V0Aage_treeV5V0IamemV5V2Oainfix =V5V4Aainfix >=V5V4Aage_treeV5V2FIamemV4V3Oainfix =V4V1Aainfix >=V4V1Aage_treeV4V3FIainfix =V0aNullNF">
<proof
prover="alt-ergo"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="z3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.05"/>
</proof>
</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