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

fix obsolete session

parent 72ae1e01
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session
name="hoare_logic/wp_total/why3session.xml">
name="wp_total/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"
name="CVC3"
version="2.4.1"/>
<prover
id="eprover"
name="Eprover"
version="1.4"/>
<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"/>
id="2"
name="Coq"
version="8.3pl3"/>
<prover
id="z3-2"
id="3"
name="Z3"
version="2.19"/>
<prover
id="z3-3"
name="Z3"
version="3.2"/>
<file
name="../wp_total.mlw"
verified="false"
expanded="true">
<theory
name="Imp"
verified="true"
expanded="false">
locfile="wp_total/../wp_total.mlw"
loclnum="3" loccnumb="7" loccnume="10"
verified="false"
expanded="true">
<goal
name="Test13"
sum="73bbbaa8c21789c90ae1492389624f69"
locfile="wp_total/../wp_total.mlw"
loclnum="72" loccnumb="5" loccnume="11"
sum="6a77fae6a0de7332ea76321b19090325"
proved="true"
expanded="false"
shape="ainfix =aeval_termamy_stateaTconstc13aVintc13">
<proof
prover="alt-ergo"
prover="0"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="Test42"
sum="c67f233c2316e72217883017f57ca1e2"
locfile="wp_total/../wp_total.mlw"
loclnum="75" loccnumb="5" loccnume="11"
sum="64bfa684b345cd4c94782188611bec2d"
proved="true"
expanded="false"
shape="ainfix =aeval_termamy_stateaTvarc0aVintc42">
<proof
prover="alt-ergo"
prover="0"
timelimit="5"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="Test0"
sum="885605cf9e6760a76dd4318b5fcc374f"
locfile="wp_total/../wp_total.mlw"
loclnum="78" loccnumb="5" loccnume="10"
sum="d71e61ea0d0d8ae5002f73dc1ab133ad"
proved="true"
expanded="false"
shape="ainfix =aeval_termamy_stateaTderefc0aVintc0">
<proof
prover="z3-2"
prover="3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.02"/>
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
</proof>
<proof
prover="cvc3-2.2"
prover="1"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="alt-ergo"
prover="0"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="Test55"
sum="c25f2c9530fa274e23a3e9bf53658474"
locfile="wp_total/../wp_total.mlw"
loclnum="81" loccnumb="5" loccnume="11"
sum="2e5cd53572e8edf10322c0a26a0e44b8"
proved="true"
expanded="false"
shape="ainfix =aeval_termamy_stateaTbinaTvarc0aOplusaTconstc13aVintc55">
<proof
prover="coq"
prover="2"
timelimit="5"
edited="wp_total_Imp_Test55_1.v"
obsolete="false">
<result status="valid" time="0.55"/>
obsolete="false"
archived="false">
<result status="valid" time="0.92"/>
</proof>
</goal>
<goal
name="eval_subst_term"
sum="5eb5401d86d177e17922bfa574a80e48"
locfile="wp_total/../wp_total.mlw"
loclnum="119" loccnumb="6" loccnume="21"
sum="20e08700f59ca0b97bbda3be6c60a6e5"
proved="true"
expanded="false"
shape="ainfix =aeval_termV0asubst_termV1V2V3aeval_termamk stateavar_envV0asetaref_envV0V2aeval_termV0V3V1F">
<proof
prover="coq"
prover="2"
timelimit="5"
edited="wp_total_Imp_eval_subst_term_1.v"
obsolete="false">
<result status="valid" time="0.54"/>
obsolete="false"
archived="false">
<result status="valid" time="0.97"/>
</proof>
</goal>
<goal
name="eval_subst"
sum="cc8ae4faf69066486b982c524c5dbe80"
proved="true"
expanded="false"
locfile="wp_total/../wp_total.mlw"
loclnum="137" loccnumb="6" loccnume="16"
sum="0b8239c98fdd9f2b4f693dd1371a58f6"
proved="false"
expanded="true"
shape="aeval_fmlaamk stateavar_envV1asetaref_envV1V2aeval_termV1V3V0qaeval_fmlaV1asubstV0V2V3F">
<proof
prover="coq"
prover="2"
timelimit="5"
edited="wp_total_Imp_eval_subst_2.v"
obsolete="false">
<result status="valid" time="0.56"/>
obsolete="false"
archived="false">
<result status="unknown" time="0.92"/>
</proof>
</goal>
<goal
name="check_skip"
sum="c85ed2d1699c7627680e4c4474a1dd24"
locfile="wp_total/../wp_total.mlw"
loclnum="154" loccnumb="6" loccnume="16"
sum="4b4c2f678575cd51e32aaaa39c5a9de3"
proved="true"
expanded="false"
shape="ainfix =V0aSskipNOainfix =V0aSskipF">
<proof
prover="alt-ergo"
prover="0"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="Ass42"
sum="8946d6ab1408129605768573a83f254f"
locfile="wp_total/../wp_total.mlw"
loclnum="204" loccnumb="7" loccnume="12"
sum="afb72905c10342f570fe71e474a95a28"
proved="true"
expanded="false"
shape="Lc0ainfix =agetaref_envV1V0aVintc42Iaone_stepamy_stateaSassignV0aTconstc42V1aSskipF">
<proof
prover="alt-ergo"
prover="0"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.08"/>
obsolete="false"
archived="false">
<result status="valid" time="0.17"/>
</proof>
</goal>
<goal
name="If42"
sum="621331c8289eadee0bffcb621b686eba"
locfile="wp_total/../wp_total.mlw"
loclnum="210" loccnumb="7" loccnume="11"
sum="fd94d6c2190eda0d9b426a1c313b2d4d"
proved="true"
expanded="false"
shape="Lc0ainfix =agetaref_envV2V0aVintc13Iaone_stepV1V3V2aSskipIaone_stepamy_stateaSifaTbinaTderefV0aOleaTconstc10aSassignV0aTconstc13aSassignV0aTconstc42V1V3F">
<proof
prover="coq"
prover="2"
timelimit="5"
edited="wp_total_Imp_If42_1.v"
obsolete="false">
<result status="valid" time="0.70"/>
obsolete="false"
archived="false">
<result status="valid" time="1.12"/>
</proof>
</goal>
<goal
name="steps_non_neg"
sum="2d79e092f9c6e122ccaa35d005c311f8"
locfile="wp_total/../wp_total.mlw"
loclnum="241" loccnumb="6" loccnume="19"
sum="e27dfbdbc40c15795ffb2a49f1d0ff4c"
proved="true"
expanded="false"
shape="ainfix >=V4c0Iamany_stepsV0V2V1V3V4F">
<proof
prover="coq"
prover="2"
timelimit="5"
edited="wp_total_Imp_steps_non_neg_1.v"
obsolete="false">
<result status="valid" time="0.53"/>
obsolete="false"
archived="false">
<result status="valid" time="0.92"/>
</proof>
</goal>
<goal
name="many_steps_seq"
sum="80707f02d94fc6a60e260ec34849847c"
locfile="wp_total/../wp_total.mlw"
loclnum="245" loccnumb="6" loccnume="20"
sum="6917cd3a3e80db5d3fd2b1fa673679e2"
proved="true"
expanded="false"
shape="ainfix =V4ainfix +ainfix +c1V6V7Aamany_stepsV5V3V1aSskipV7Aamany_stepsV0V2V5aSskipV6EIamany_stepsV0aSseqV2V3V1aSskipV4F">
<proof
prover="coq"
prover="2"
timelimit="5"
edited="wp_total_Imp_many_steps_seq_1.v"
obsolete="false">
<result status="valid" time="0.61"/>
obsolete="false"
archived="false">
<result status="valid" time="1.05"/>
</proof>
</goal>
<goal
name="skip_rule"
sum="0b28a425f02c50dbd76a1eedbb42dbdc"
locfile="wp_total/../wp_total.mlw"
loclnum="274" loccnumb="6" loccnume="15"
sum="217d63588a21fa7ad821b8d871c09945"
proved="true"
expanded="false"
shape="avalid_tripleV0aSskipV0F">
<proof
prover="alt-ergo"
prover="0"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="1.59"/>
obsolete="false"
archived="false">
<result status="valid" time="1.56"/>
</proof>
</goal>
<goal
name="assign_rule"
sum="09c93c2ad9b01e881d20c288190d2bca"
locfile="wp_total/../wp_total.mlw"
loclnum="277" loccnumb="6" loccnume="17"
sum="aba37f16d271198ae5b7dfc39d7cc9a7"
proved="true"
expanded="false"
shape="avalid_tripleasubstV0V1V2aSassignV1V2V0F">
<proof
prover="coq"
prover="2"
timelimit="5"
edited="wp_total_Imp_assign_rule_1.v"
obsolete="false">
<result status="valid" time="0.61"/>
obsolete="false"
archived="false">
<result status="valid" time="0.98"/>
</proof>
</goal>
<goal
name="seq_rule"
sum="9900a241b0cd385b545308baac7162ab"
locfile="wp_total/../wp_total.mlw"
loclnum="281" loccnumb="6" loccnume="14"
sum="f1cf9dd3ebefb41ebe50d46642366856"
proved="true"
expanded="false"
shape="avalid_tripleV0aSseqV3V4V1Iavalid_tripleV2V4V1Aavalid_tripleV0V3V2F">
<proof
prover="z3-2"
prover="3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.04"/>
obsolete="false"
archived="false">
<result status="valid" time="0.07"/>
</proof>
</goal>
<goal
name="if_rule"
sum="c63598af102884475eb6d730531e8ca2"
locfile="wp_total/../wp_total.mlw"
loclnum="286" loccnumb="6" loccnume="13"
sum="5b9d1548b545a3673c0c928b8dbecef5"
proved="true"
expanded="false"
shape="avalid_tripleV1aSifV0V3V4V2Iavalid_tripleaFandV1aFnotaFtermV0V4V2Aavalid_tripleaFandV1aFtermV0V3V2F">
<proof
prover="coq"
prover="2"
timelimit="5"
edited="wp_total_Imp_if_rule_1.v"
obsolete="false">
<result status="valid" time="0.65"/>
obsolete="false"
archived="false">
<result status="valid" time="1.09"/>
</proof>
</goal>
<goal
name="assert_rule"
sum="80621c5cb8b97d0a529a33e48a728a5e"
locfile="wp_total/../wp_total.mlw"
loclnum="292" loccnumb="6" loccnume="17"
sum="d6a4280992f518ec98fc872ba36175c8"
proved="true"
expanded="false"
shape="avalid_tripleV1aSassertV0V1Iavalid_fmlaaFimpliesV1V0F">
<proof
prover="coq"
prover="2"
timelimit="5"
edited="wp_total_Imp_assert_rule_1.v"
obsolete="false">
<result status="valid" time="0.59"/>
obsolete="false"
archived="false">
<result status="valid" time="1.01"/>
</proof>
</goal>
<goal
name="assert_rule_ext"
sum="a669eb36cbc51beebb64bf280cc017a6"
locfile="wp_total/../wp_total.mlw"
loclnum="296" loccnumb="6" loccnume="21"
sum="25cb5365c92e302a136ffbb3e96d6054"
proved="true"
expanded="false"
shape="avalid_tripleaFimpliesV0V1aSassertV0V1F">
<proof
prover="coq"
prover="2"
timelimit="5"
edited="wp_total_Imp_assert_rule_ext_1.v"
obsolete="false">
<result status="valid" time="0.58"/>
obsolete="false"
archived="false">
<result status="valid" time="1.00"/>
</proof>
</goal>
<goal
name="while_rule"
sum="1133fbd4964fd9c61f28b212eba9d5f8"
locfile="wp_total/../wp_total.mlw"
loclnum="300" loccnumb="6" loccnume="16"
sum="0f6a6de65bfb668dc51d372154aa6803"
proved="true"
expanded="false"
shape="avalid_tripleV1aSwhileV0V1V2aFandaFnotaFtermV0V1Iavalid_tripleaFandaFtermV0V1V2V1F">
<proof
prover="coq"
prover="2"
timelimit="5"
edited="wp_total_Imp_while_rule_1.v"
obsolete="false">
<result status="valid" time="0.72"/>
obsolete="false"
archived="false">
<result status="valid" time="1.21"/>
</proof>
</goal>
<goal
name="while_rule_ext"
sum="a59215763073f106d7e759f033ef9a21"
locfile="wp_total/../wp_total.mlw"
loclnum="305" loccnumb="6" loccnume="20"
sum="311c28274b23efde0bb1f5fe83c9de7f"
proved="true"
expanded="false"
shape="avalid_tripleV2aSwhileV0V1V3aFandaFnotaFtermV0V2Iavalid_tripleaFandaFtermV0V2V3V2Iavalid_fmlaaFimpliesV2V1F">
<proof
prover="coq"
prover="2"
timelimit="5"
edited="wp_total_Imp_while_rule_ext_1.v"
obsolete="false">
<result status="valid" time="0.69"/>
obsolete="false"
archived="false">
<result status="valid" time="1.14"/>
</proof>
</goal>
<goal
name="consequence_rule"
sum="ba4df7de10af9c0a89d1dd0a80e90f6d"
locfile="wp_total/../wp_total.mlw"
loclnum="311" loccnumb="6" loccnume="22"
sum="b9254275c3cbbc996afae79b202b07d3"
proved="true"
expanded="false"
shape="avalid_tripleV1V4V3Iavalid_fmlaaFimpliesV2V3Iavalid_tripleV0V4V2Iavalid_fmlaaFimpliesV1V0F">
<proof
prover="z3-2"
prover="3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.05"/>
obsolete="false"
archived="false">
<result status="valid" time="0.10"/>
</proof>
<proof
prover="cvc3-2.2"
prover="1"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.67"/>
obsolete="false"
archived="false">
<result status="valid" time="1.18"/>
</proof>
</goal>
</theory>
<theory
name="WP WP"
locfile="wp_total/../wp_total.mlw"
loclnum="339" loccnumb="7" loccnume="9"
verified="false"
expanded="true">
<goal
name="WP_parameter wp"
locfile="wp_total/../wp_total.mlw"
loclnum="343" loccnumb="10" loccnume="12"
expl="parameter wp"
sum="d93d5cb9013f441420d5183d3fc07cc5"
sum="a91a4afa65657a32ccce911911868ad9"
proved="false"
expanded="true"
shape="CV0aSskipavalid_tripleV1V0V1aSseqVVavalid_tripleV5V0V1Iavalid_tripleV5V2V4FIavalid_tripleV4V3V1FaSassignVVavalid_tripleasubstV1V6V7V0V1aSifVVVavalid_tripleaFandaFimpliesaFtermV8V11aFimpliesaFnotaFtermV8V12V0V1Iavalid_tripleV12V10V1FIavalid_tripleV11V9V1FaSassertVavalid_tripleaFimpliesV13V1V0V1aSwhileVVVavalid_tripleaFandV15aFandaFimpliesaFandaFtermV14V15V17aFimpliesaFandaFnotaFtermV14V15V1V0V1Iavalid_tripleV17V16V15FFF">
<label
name="expl:parameter wp">
</label>
<proof
prover="coq"
prover="2"
timelimit="5"
edited="wp_total_WP_WP_WP_parameter_wp_2.v"
obsolete="false">
<result status="unknown" time="0.56"/>
obsolete="false"
archived="false">
<result status="unknown" time="0.92"/>
</proof>
<transf
name="split_goal"
......@@ -388,141 +414,172 @@
expanded="true">
<goal
name="WP_parameter wp.1"
locfile="wp_total/../wp_total.mlw"
loclnum="343" loccnumb="10" loccnume="12"
expl="parameter wp"
sum="16ea833f8e34f438109f7f91fea8f705"
sum="6b4b340c578067c16a8e4426b676df6f"
proved="true"
expanded="false"
shape="CV0aSskipavalid_tripleV1V0V1aSseqVVtaSassignVVtaSifVVVtaSassertVtaSwhileVVVtFF">
<label
name="expl:parameter wp">
</label>
<proof
prover="alt-ergo"
prover="0"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.02"/>
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal
name="WP_parameter wp.2"
locfile="wp_total/../wp_total.mlw"
loclnum="343" loccnumb="10" loccnume="12"
expl="parameter wp"
sum="7fa9c674a4e050fd23c0c2ffa8222e5a"
sum="6d061b49e52263f1cb3cddd6940df0e2"
proved="true"
expanded="false"
shape="CV0aSskiptaSseqVVavalid_tripleV5V0V1Iavalid_tripleV5V2V4FIavalid_tripleV4V3V1FaSassignVVtaSifVVVtaSassertVtaSwhileVVVtFF">
<label
name="expl:parameter wp">
</label>
<proof
prover="alt-ergo"
prover="0"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.02"/>
obsolete="false"
archived="false">