Skip to content

GitLab

why3
why3
Commit 82e3b5fb authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files
Options

update sessions (part 2)

parent b899b99b
Hide whitespace changes
Inline Side-by-side
Showing with 758 additions and 592 deletions
examples/check-builtin/int/why3session.xml
View file @ 82e3b5fb
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session
name="examples/check-builtin/int/why3session.xml">
name="check-builtin/int/why3session.xml">
<prover
id="alt-ergo"
name="Alt-Ergo"
......
examples/explicit_subst/why3session.xml
View file @ 82e3b5fb
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session
name="examples/explicit_subst/why3session.xml">
name="explicit_subst/why3session.xml">
<prover
id="alt-ergo"
name="Alt-Ergo"
......
examples/hello_proof/why3session.xml
View file @ 82e3b5fb
......@@ -5,7 +5,7 @@
<prover
id="alt-ergo"
name="Alt-Ergo"
version="0.93"/>
version="0.94"/>
<prover
id="coq"
name="Coq"
......@@ -69,7 +69,7 @@
expanded="true"
shape="t">
<proof
prover="alt-ergo"
prover="z3-2"
timelimit="5"
edited=""
obsolete="false">
......@@ -83,22 +83,22 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="cvc3-2.2"
prover="alt-ergo"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="simplify"
timelimit="10"
prover="cvc3-2.2"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="z3-2"
timelimit="5"
prover="simplify"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
......@@ -142,7 +142,7 @@
<result status="unknown" time="0.50"/>
</proof>
<proof
prover="alt-ergo"
prover="z3-2"
timelimit="5"
edited=""
obsolete="false">
......@@ -156,15 +156,15 @@
<result status="unknown" time="0.00"/>
</proof>
<proof
prover="simplify"
timelimit="10"
prover="alt-ergo"
timelimit="5"
edited=""
obsolete="false">
<result status="unknown" time="0.00"/>
</proof>
<proof
prover="z3-2"
timelimit="5"
prover="simplify"
timelimit="10"
edited=""
obsolete="false">
<result status="unknown" time="0.00"/>
......@@ -177,7 +177,7 @@
expanded="true"
shape="fOt">
<proof
prover="alt-ergo"
prover="z3-2"
timelimit="5"
edited=""
obsolete="false">
......@@ -191,22 +191,22 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="cvc3-2.2"
prover="alt-ergo"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="simplify"
timelimit="10"
prover="cvc3-2.2"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="z3-2"
timelimit="5"
prover="simplify"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
......@@ -223,12 +223,12 @@
</goal>
<goal
name="G3"
sum="7fe60c475f2475c85d5b44f460c0a030"
sum="30f7a9e2b4315fc204f5d5e6bd9b23e3"
proved="true"
expanded="true"
shape="ainfix >=ainfix *V0V0c0F">
<proof
prover="alt-ergo"
prover="z3-2"
timelimit="5"
edited=""
obsolete="false">
......@@ -242,25 +242,25 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="cvc3-2.2"
prover="alt-ergo"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="simplify"
timelimit="3"
prover="cvc3-2.2"
timelimit="5"
edited=""
obsolete="false">
<result status="unknown" time="0.00"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="z3-2"
timelimit="5"
prover="simplify"
timelimit="3"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
<result status="unknown" time="0.00"/>
</proof>
<proof
prover="cvc3-2.4"
......
examples/hoare_logic/imp/why3session.xml
View file @ 82e3b5fb
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session
name="imp/why3session.xml">
name="hoare_logic/imp/why3session.xml">
<prover
id="alt-ergo"
name="Alt-Ergo"
version="0.93"/>
version="0.94"/>
<prover
id="coq"
name="Coq"
version="8.2pl1"/>
version="8.3pl2"/>
<prover
id="cvc3-2.2"
name="CVC3"
version="2.2"/>
<prover
id="cvc3-2.4"
name="CVC3"
version="2.4.1"/>
<prover
id="eprover"
name="Eprover"
......@@ -46,6 +50,10 @@
id="z3-2"
name="Z3"
version="2.19"/>
<prover
id="z3-3"
name="Z3"
version="3.2"/>
<file
name="../imp.why"
verified="false"
......@@ -61,25 +69,25 @@
expanded="false"
shape="ainfix =V0V1NOainfix =V0V1F">
<proof
prover="cvc3-2.2"
prover="z3-2"
timelimit="3"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="alt-ergo"
prover="cvc3-2.2"
timelimit="3"
edited=""
obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="z3-2"
prover="alt-ergo"
timelimit="3"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
......@@ -100,12 +108,12 @@
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="Test13"
sum="bc53c41524b84304eb79b4e36fef8af8"
sum="89034cff3a243960c6fe7b2b2a91966f"
proved="true"
expanded="false"
shape="Laconstc0ainfix =aeval_exprV0aEconstc13c13">
......@@ -114,40 +122,40 @@
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="alt-ergo"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="eprover"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="vampire"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="spass"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="Test42"
sum="78671d09729d8ffd84136c2dcf7eb74b"
sum="991bca434c242bd0fc4fcae7860bb583"
proved="true"
expanded="false"
shape="Lamk_identc0Lasetaconstc0V0c42ainfix =aeval_exprV1aEvarV0c42">
......@@ -156,40 +164,40 @@
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="alt-ergo"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="eprover"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="vampire"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.14"/>
<result status="valid" time="0.08"/>
</proof>
<proof
prover="spass"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.05"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="Test55"
sum="9f1ffc89f69ccb03e44edbf6adfebb8d"
sum="13ad67fe0a83a4e1ece624124c864703"
proved="true"
expanded="false"
shape="Lamk_identc0Lasetaconstc0V0c42ainfix =aeval_exprV1aEbinaEvarV0aOplusaEconstc13c55">
......@@ -198,19 +206,19 @@
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="alt-ergo"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.04"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="Ass42"
sum="456c846b124e10fccdeb72291a3819b0"
sum="2eae993f753f8826c606f370e5382862"
proved="true"
expanded="false"
shape="Lamk_identc0Laconstc0ainfix =agetV2V0c42Iaone_stepV1aSassignV0aEconstc42V2aSskipF">
......@@ -219,19 +227,19 @@
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.04"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="alt-ergo"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.06"/>
<result status="valid" time="0.05"/>
</proof>
</goal>
<goal
name="If42"
sum="9c97951c8cf8d86219396907bf0260eb"
sum="12b5437a3440e505c69b24e6e91a75b8"
proved="true"
expanded="false"
shape="Lamk_identc0Laconstc0ainfix =agetV3V0c42Iaone_stepV2V4V3aSskipIaone_stepV1aSifaEvarV0aSassignV0aEconstc13aSassignV0aEconstc42V2V4F">
......@@ -240,19 +248,19 @@
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.47"/>
<result status="valid" time="0.35"/>
</proof>
<proof
prover="alt-ergo"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.84"/>
<result status="valid" time="1.04"/>
</proof>
</goal>
<goal
name="progress"
sum="3e029691d2ae6f6e5afe69a1860de120"
sum="1de081684224e7f85881292371e2b0b0"
proved="true"
expanded="false"
shape="aone_stepV0V1V2V3EIainfix =V1aSskipNF">
......@@ -261,12 +269,12 @@
timelimit="5"
edited="imp_Imp_progress_1.v"
obsolete="false">
<result status="valid" time="0.68"/>
<result status="valid" time="0.52"/>
</proof>
</goal>
<goal
name="many_steps_seq_rec"
sum="11055dd7c0d1df4d3beead62e71fb0d0"
sum="1437eebbf80b92b8c7d930a8e1f09f1d"
proved="true"
expanded="false"
shape="amany_stepsV6V5V1aSskipAamany_stepsV0V4V6aSskipEIainfix =V2aSseqV4V5FIainfix =V3aSskipIamany_stepsV0V2V1V3F">
......@@ -280,35 +288,35 @@
</goal>
<goal
name="many_steps_seq"
sum="dd8b486013219116b304a7fa85098017"
sum="c454267b2ebd89d6185e11ed0374c13c"
proved="true"
expanded="false"
shape="amany_stepsV4V3V1aSskipAamany_stepsV0V2V4aSskipEIamany_stepsV0aSseqV2V3V1aSskipF">
<proof
prover="cvc3-2.2"
prover="z3-2"
timelimit="3"
edited=""
obsolete="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="alt-ergo"
prover="cvc3-2.2"
timelimit="3"
edited=""
obsolete="false">
<result status="valid" time="0.05"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="z3-2"
prover="alt-ergo"
timelimit="3"
edited=""
obsolete="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.04"/>
</proof>
</goal>
<goal
name="eval_subst_expr"
sum="977774231aa576a9290e4f9016c04ed0"
sum="f5d51c7e4199b965800307ebb3d10140"
proved="true"
expanded="false"
shape="ainfix =aeval_exprV0asubst_exprV1V2V3aeval_exprasetV0V2aeval_exprV0V3V1F">
......@@ -317,12 +325,12 @@
timelimit="5"
edited="imp_Imp_eval_subst_expr_1.v"
obsolete="false">
<result status="valid" time="0.61"/>
<result status="valid" time="0.53"/>
</proof>
</goal>
<goal
name="eval_subst"
sum="a104713723b4fa4f3517a9438902ec80"
sum="99eaa712e77012cdbc17731732304877"
proved="true"
expanded="false"
shape="aeval_fmlaasetV0V2aeval_exprV0V3V1qaeval_fmlaV0asubstV1V2V3F">
......@@ -331,12 +339,12 @@
timelimit="5"
edited="imp_Imp_eval_subst_2.v"
obsolete="false">
<result status="valid" time="0.52"/>
<result status="valid" time="0.55"/>
</proof>
</goal>
<goal
name="skip_rule"
sum="e7044c767994d31b5b88e917bfff9ac0"
sum="6f634e9ba9fef417c81e04f8c64a990a"
proved="true"
expanded="false"
shape="avalid_tripleV0aSskipV0F">
......@@ -345,12 +353,12 @@
timelimit="3"
edited="imp_Imp_skip_rule_1.v"
obsolete="false">
<result status="valid" time="0.60"/>
<result status="valid" time="0.58"/>
</proof>
</goal>
<goal
name="assign_rule"
sum="0ec8e9f1b70042827e8a4110996d5ce6"
sum="1c2200a7792284ba6d0a78d2f2a04be9"
proved="true"
expanded="false"
shape="avalid_tripleasubstV0V1V2aSassignV1V2V0F">
......@@ -359,12 +367,12 @@
timelimit="5"
edited="imp_Imp_assign_rule_1.v"
obsolete="false">
<result status="valid" time="0.58"/>
<result status="valid" time="0.59"/>
</proof>
</goal>
<goal
name="seq_rule"
sum="b0875f2e4e3ff470e938fb16ff79cd67"
sum="3430e48f60bc03df61fed9db4f65710b"
proved="true"
expanded="false"
shape="avalid_tripleV0aSseqV3V4V1Iavalid_tripleV2V4V1Aavalid_tripleV0V3V2F">
......@@ -373,19 +381,19 @@
timelimit="3"
edited="imp_Imp_seq_rule_2.v"
obsolete="false">
<result status="valid" time="0.61"/>
<result status="valid" time="0.54"/>
</proof>
<proof
prover="z3-2"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.07"/>
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal
name="if_rule"
sum="8e1f396662d807419bc751cf7f6d58b9"
sum="17c3ab55261d3b73b0b5cd8d446dc3d4"
proved="true"
expanded="false"
shape="avalid_tripleV1aSifV0V3V4V2Iavalid_tripleaFandV1aFnotaFtermV0V4V2Aavalid_tripleaFandV1aFtermV0V3V2F">
......@@ -394,12 +402,12 @@
timelimit="3"
edited="imp_Imp_if_rule_1.v"
obsolete="false">
<result status="valid" time="0.61"/>
<result status="valid" time="0.56"/>
</proof>
</goal>
<goal
name="while_rule_rec"
sum="094bc644f8c198e43d4d30be08dab9f4"
sum="e78d7b18fc6e38f4102faaf8fc7ac692"
proved="false"
expanded="true"
shape="aeval_fmlaV4aFandaFnotaFtermV0V1Iaeval_fmlaV3V1Iainfix =V6aSskipIainfix =V5aSwhileV0V2Iamany_stepsV3V5V4V6FIavalid_tripleaFandaFtermV0V1V2V1F">
......@@ -407,36 +415,36 @@
prover="coq"
timelimit="5"
edited="imp_Imp_while_rule_rec_1.v"
obsolete="true">
<result status="unknown" time="0.59"/>
obsolete="false">
<result status="unknown" time="0.53"/>
</proof>
</goal>
<goal
name="while_rule"
sum="78107beafe1c5ce0bd6dd9b7a96554f4"
sum="160833addfc656befefa1bbe6863cac0"
proved="true"
expanded="true"
shape="avalid_tripleV1aSwhileV0V2aFandaFnotaFtermV0V1Iavalid_tripleaFandaFtermV0V1V2V1F">
<proof
prover="cvc3-2.2"
prover="z3-2"
timelimit="3"
edited=""
obsolete="false">
<result status="valid" time="0.18"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="alt-ergo"
prover="cvc3-2.2"
timelimit="3"
edited=""
obsolete="false">
<result status="valid" time="0.35"/>
<result status="valid" time="0.10"/>
</proof>
<proof
prover="z3-2"
prover="alt-ergo"
timelimit="3"
edited=""
obsolete="false">
<result status="valid" time="0.06"/>
<result status="valid" time="0.37"/>
</proof>
</goal>
</theory>
......
examples/hoare_logic/wp/why3session.xml
View file @ 82e3b5fb
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session
name="wp/why3session.xml">
name="hoare_logic/wp/why3session.xml">
<prover
id="alt-ergo"
name="Alt-Ergo"
version="0.93"/>
version="0.94"/>
<prover
id="coq"
name="Coq"
version="8.2pl1"/>
version="8.3pl2"/>
<prover
id="cvc3-2.2"
name="CVC3"
version="2.2"/>
<prover
id="cvc3-2.4"
name="CVC3"
version="2.4.1"/>
<prover
id="eprover"
name="Eprover"
......@@ -46,6 +50,10 @@
id="z3-2"
name="Z3"
version="2.19"/>
<prover
id="z3-3"
name="Z3"
version="3.2"/>
<file
name="../wp.mlw"
verified="false"
......@@ -56,7 +64,7 @@