Commit 6e1e49a8 authored by MARCHE Claude's avatar MARCHE Claude

update sessions with new explanations

parent bd9acd41
......@@ -26,13 +26,13 @@
name="WP_parameter to_int_"
locfile="../13375.mlw"
loclnum="51" loccnumb="5" loccnume="12"
expl="parameter to_int_"
expl="VC for to_int_"
sum="4077c128df716cfc503b0898c655443c"
proved="true"
expanded="true"
shape="t">
<label
name="expl:parameter to_int_"/>
name="expl:VC for to_int_"/>
<proof
prover="0"
timelimit="5"
......
......@@ -19,13 +19,13 @@
name="WP_parameter f"
locfile="../13853.mlw"
loclnum="16" loccnumb="8" loccnume="9"
expl="exceptional postcondition"
expl="VC for f"
sum="893cd69e3c7345f5514a1b4ddab4cd80"
proved="true"
expanded="false"
shape="t">
<label
name="expl:parameter f"/>
name="expl:VC for f"/>
<proof
prover="0"
timelimit="10"
......@@ -39,13 +39,13 @@
name="WP_parameter g"
locfile="../13853.mlw"
loclnum="18" loccnumb="8" loccnume="9"
expl="exceptional postcondition"
expl="VC for g"
sum="bddadcafb90c4cc9043521e5c27e2f6f"
proved="true"
expanded="false"
shape="t">
<label
name="expl:parameter g"/>
name="expl:VC for g"/>
<proof
prover="0"
timelimit="10"
......
......@@ -27,13 +27,13 @@
name="WP_parameter max"
locfile="../array_max.mlw"
loclnum="21" loccnumb="6" loccnume="9"
expl="parameter max"
expl="VC for max"
sum="e8de669fdf43b35dd32e52ba558b85d9"
proved="true"
expanded="true"
shape="iainfix =V3V2Niainfix &lt;=agetV1V3agetV1V2ainfix &lt;ainfix -V2V4ainfix -V2V3Aainfix &lt;=c0ainfix -V2V3Aainfix &lt;=agetV1V5amaxagetV1V4agetV1V2Iainfix &lt;V5V0Aainfix &lt;V2V5Oainfix &lt;V5V4Aainfix &lt;=c0V5FAainfix &lt;V2V0Aainfix &lt;=V4V2Aainfix &lt;=c0V4Iainfix =V4ainfix +V3c1Fainfix &lt;ainfix -V6V3ainfix -V2V3Aainfix &lt;=c0ainfix -V2V3Aainfix &lt;=agetV1V7amaxagetV1V3agetV1V6Iainfix &lt;V7V0Aainfix &lt;V6V7Oainfix &lt;V7V3Aainfix &lt;=c0V7FAainfix &lt;V6V0Aainfix &lt;=V3V6Aainfix &lt;=c0V3Iainfix =V6ainfix -V2c1FAainfix &lt;V3V0Aainfix &lt;=c0V3Aainfix &lt;V2V0Aainfix &lt;=c0V2ainfix &lt;=agetV1V8agetV1V3Iainfix &lt;V8V0Aainfix &lt;=c0V8FAainfix &lt;V3V0Aainfix &lt;=c0V3Iainfix &lt;=agetV1V9amaxagetV1V3agetV1V2Iainfix &lt;V9V0Aainfix &lt;V2V9Oainfix &lt;V9V3Aainfix &lt;=c0V9FAainfix &lt;V2V0Aainfix &lt;=V3V2Aainfix &lt;=c0V3FAainfix &lt;=agetV1V10amaxagetV1c0agetV1ainfix -V0c1Iainfix &lt;V10V0Aainfix &lt;ainfix -V0c1V10Oainfix &lt;V10c0Aainfix &lt;=c0V10FAainfix &lt;ainfix -V0c1V0Aainfix &lt;=c0ainfix -V0c1Aainfix &lt;=c0c0Iainfix &lt;c0V0FF">
<label
name="expl:parameter max"/>
name="expl:VC for max"/>
<proof
prover="0"
timelimit="7"
......
......@@ -34,13 +34,13 @@
name="WP_parameter duplet"
locfile="../duplets.mlw"
loclnum="43" loccnumb="6" loccnume="12"
expl="parameter duplet"
expl="VC for duplet"
sum="18fdae12af8c0e3d1e3cb70ddbf7f8f8"
proved="true"
expanded="true"
shape="ais_dupletV3V4V5NICV1aNonefaSomeVainfix =V6agetV2V4NIainfix &lt;V5V0Aainfix &lt;V4V5Aainfix &lt;V4ainfix +ainfix -V0c2c1Aainfix &lt;=c0V4FNAiCV1aNonefaSomeVainfix =V9V8ais_dupletV3V10V11NICV1aNonefaSomeVainfix =V12agetV2V10NIainfix &lt;V11V0Aainfix &lt;V10V11Aainfix &lt;V10ainfix +V7c1Aainfix &lt;=c0V10Fais_dupletV3V13V14NICV1aNonefaSomeVainfix =V15agetV2V13NIainfix &lt;V14V0Aainfix &lt;V13V14Aainfix &lt;V13ainfix +V7c1Aainfix &lt;=c0V13FIais_dupletV3V7V16NIainfix &lt;V16ainfix +ainfix -V0c1c1Aainfix &lt;V7V16FAiainfix =agetV2V17V8CV1aNonefaSomeVainfix =V20agetV2V18NAais_dupletV3V18V19Iainfix =V19V17Aainfix =V18V7Fais_dupletV3V7V21NIainfix &lt;V21ainfix +V17c1Aainfix &lt;V7V21FAainfix &lt;V17V0Aainfix &lt;=c0V17Iais_dupletV3V7V22NIainfix &lt;V22V17Aainfix &lt;V7V22FIainfix &lt;=V17ainfix -V0c1Aainfix &lt;=ainfix +V7c1V17FAais_dupletV3V7V23NIainfix &lt;V23ainfix +V7c1Aainfix &lt;V7V23FIainfix &lt;=ainfix +V7c1ainfix -V0c1Aais_dupletV3V24V25NICV1aNonefaSomeVainfix =V26agetV2V24NIainfix &lt;V25V0Aainfix &lt;V24V25Aainfix &lt;V24ainfix +V7c1Aainfix &lt;=c0V24FIainfix &gt;ainfix +V7c1ainfix -V0c1LagetV2V7Aainfix &lt;V7V0Aainfix &lt;=c0V7Iais_dupletV3V27V28NICV1aNonefaSomeVainfix =V29agetV2V27NIainfix &lt;V28V0Aainfix &lt;V27V28Aainfix &lt;V27V7Aainfix &lt;=c0V27FIainfix &lt;=V7ainfix -V0c2Aainfix &lt;=c0V7FAais_dupletV3V30V31NICV1aNonefaSomeVainfix =V32agetV2V30NIainfix &lt;V31V0Aainfix &lt;V30V31Aainfix &lt;V30c0Aainfix &lt;=c0V30FIainfix &lt;=c0ainfix -V0c2Aainfix &gt;c0ainfix -V0c2NICV1aNonefaSomeVainfix =V35agetV2V33NAais_dupletV3V33V34EAainfix &lt;=c2V0Lamk arrayV0V2FF">
<label
name="expl:parameter duplet"/>
name="expl:VC for duplet"/>
<proof
prover="1"
timelimit="5"
......@@ -62,13 +62,13 @@
name="WP_parameter duplets"
locfile="../duplets.mlw"
loclnum="74" loccnumb="6" loccnume="13"
expl="parameter duplets"
expl="VC for duplets"
sum="e99b05c40c9b643592e49bc2013aff3f"
proved="true"
expanded="true"
shape="ainfix =agetV1V3agetV1V6NAais_dupletV2V6V7Aais_dupletV2V3V4Iainfix =V5agetV1V6NAais_dupletV2V6V7FAainfix =V5agetV1V8NAais_dupletV2V8V9EAainfix &lt;=c2V0LagetV1V4Aainfix &lt;V4V0Aainfix &lt;=c0V4Iais_dupletV2V3V4FAais_dupletV2V10V11EAainfix &lt;=c2V0Iainfix =agetV1V12agetV1V14NAais_dupletV2V14V15Aais_dupletV2V12V13EAainfix &lt;=c4V0Lamk arrayV0V1FF">
<label
name="expl:parameter duplets"/>
name="expl:VC for duplets"/>
<proof
prover="0"
timelimit="5"
......
......@@ -48,13 +48,13 @@
name="WP_parameter max_aux"
locfile="../tree_max.mlw"
loclnum="58" loccnumb="10" loccnume="17"
expl="parameter max_aux"
expl="VC for max_aux"
sum="ff881f65aef0140a6dfc905eb5fda89a"
proved="true"
expanded="true"
shape="CV0aNullainfix &gt;=V1V1Aage_treeV1V0aTreeVVVamemV6V0Oainfix =V6V1Aainfix &gt;=V6V1Aage_treeV6V0IamemV6V3Oainfix =V6V5Aainfix &gt;=V6V5Aage_treeV6V3FACV0aNullfaTreewVVainfix =V8V3Oainfix =V7V3IamemV5V4Oainfix =V5amaxV2V1Aainfix &gt;=V5amaxV2V1Aage_treeV5V4FACV0aNullfaTreewVVainfix =V10V4Oainfix =V9V4F">
<label
name="expl:parameter max_aux"/>
name="expl:VC for max_aux"/>
<proof
prover="0"
timelimit="5"
......@@ -68,13 +68,13 @@
name="WP_parameter max"
locfile="../tree_max.mlw"
loclnum="67" loccnumb="6" loccnume="9"
expl="postcondition"
expl="VC for max"
sum="28e5d856901e66fadb02844681ad3b11"
proved="true"
expanded="true"
shape="CV0aNullfaTreeVVVamemV5V0Aage_treeV5V0IamemV5V2Oainfix =V5V4Aainfix &gt;=V5V4Aage_treeV5V2FIamemV4V3Oainfix =V4V1Aainfix &gt;=V4V1Aage_treeV4V3FIainfix =V0aNullNF">
<label
name="expl:parameter max"/>
name="expl:VC for max"/>
<proof
prover="0"
timelimit="5"
......
......@@ -424,7 +424,7 @@
memlimit="4000"
obsolete="false"
archived="false">
<result status="timeout" time="5.25"/>
<result status="timeout" time="5.96"/>
</proof>
</goal>
<goal
......@@ -521,7 +521,7 @@
memlimit="4000"
obsolete="false"
archived="false">
<result status="timeout" time="5.14"/>
<result status="timeout" time="5.00"/>
</proof>
</goal>
<goal
......@@ -707,7 +707,7 @@
memlimit="4000"
obsolete="false"
archived="false">
<result status="timeout" time="6.35"/>
<result status="timeout" time="5.27"/>
</proof>
</goal>
</theory>
......
......@@ -74,6 +74,7 @@
name="G2.1"
locfile="../hello_proof.why"
loclnum="5" loccnumb="7" loccnume="9"
expl="1."
sum="b84cad55140412a1b6f988cba7a0ebd1"
proved="false"
expanded="true"
......@@ -108,6 +109,7 @@
name="G2.2"
locfile="../hello_proof.why"
loclnum="5" loccnumb="7" loccnume="9"
expl="2."
sum="fdf75c799e5829c6e57c69e76f88886a"
proved="true"
expanded="true"
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/cmarche/recherche/why3/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<why3session shape_version="2">
<prover
id="0"
......@@ -2197,7 +2197,7 @@
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.44"/>
<result status="valid" time="0.24"/>
</proof>
<proof
prover="3"
......@@ -2255,7 +2255,7 @@
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.25"/>
<result status="valid" time="0.44"/>
</proof>
<proof
prover="3"
......@@ -2321,7 +2321,7 @@
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="4.25"/>
<result status="valid" time="8.79"/>
</proof>
<proof
prover="5"
......@@ -2379,7 +2379,7 @@
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="8.08"/>
<result status="valid" time="9.18"/>
</proof>
<proof
prover="5"
......@@ -2429,7 +2429,7 @@
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="4.63"/>
<result status="valid" time="2.47"/>
</proof>
<proof
prover="3"
......@@ -2603,7 +2603,7 @@
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="4.12"/>
<result status="valid" time="8.51"/>
</proof>
<proof
prover="3"
......@@ -2828,7 +2828,7 @@
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="9.98"/>
<result status="valid" time="8.88"/>
</proof>
<proof
prover="1"
......@@ -4410,7 +4410,7 @@
edited="blocking_semantics5_WP_monotonicity_2.v"
obsolete="false"
archived="false">
<result status="valid" time="1.21"/>
<result status="valid" time="0.97"/>
</proof>
<proof
prover="5"
......
......@@ -654,13 +654,13 @@
name="WP_parameter compute_writes"
locfile="../wp2.mlw"
loclnum="396" loccnumb="10" loccnume="24"
expl="parameter compute_writes"
expl="VC for compute_writes"
sum="8c2444ab4823ee0a1abdbd5fb49c1f73"
proved="true"
expanded="false"
shape="CV0aSskipaassignsV1aemptyV3Iamany_stepsV1V2V0V3V4aSskipV5FaSassignVwaassignsV7asingletonV6V9Iamany_stepsV7V8V0V9V10aSskipV11FaSseqVVaassignsV16aunionV15V14V18Iamany_stepsV16V17V0V18V19aSskipV20FIaassignsV21V15V23Iamany_stepsV21V22V12V23V24aSskipV25FFIaassignsV26V14V28Iamany_stepsV26V27V13V28V29aSskipV30FFaSifwVVaassignsV35aunionV34V33V37Iamany_stepsV35V36V0V37V38aSskipV39FIaassignsV40V34V42Iamany_stepsV40V41V31V42V43aSskipV44FFIaassignsV45V33V47Iamany_stepsV45V46V32V47V48aSskipV49FFaSwhilewwVaassignsV52V51V54Iamany_stepsV52V53V0V54V55aSskipV56FIaassignsV57V51V59Iamany_stepsV57V58V50V59V60aSskipV61FFaSassertwaassignsV62aemptyV64Iamany_stepsV62V63V0V64V65aSskipV66FF">
<label
name="expl:parameter compute_writes"/>
name="expl:VC for compute_writes"/>
<transf
name="split_goal"
proved="true"
......@@ -669,13 +669,13 @@
name="WP_parameter compute_writes.1"
locfile="../wp2.mlw"
loclnum="396" loccnumb="10" loccnume="24"
expl="postcondition"
expl="1. postcondition"
sum="cc9319762b0bc1611b7e16b341216c93"
proved="true"
expanded="false"
shape="CV0aSskipaassignsV1aemptyV3Iamany_stepsV1V2V0V3V4aSskipV5FaSassignVwtaSseqVVtaSifwVVtaSwhilewwVtaSassertwtF">
<label
name="expl:parameter compute_writes"/>
name="expl:VC for compute_writes"/>
<proof
prover="0"
timelimit="3"
......@@ -689,13 +689,13 @@
name="WP_parameter compute_writes.2"
locfile="../wp2.mlw"
loclnum="396" loccnumb="10" loccnume="24"
expl="postcondition"
expl="2. postcondition"
sum="68b043510e407df3816d0ce7aac52594"
proved="true"
expanded="false"
shape="CV0aSskiptaSassignVwaassignsV2asingletonV1V4Iamany_stepsV2V3V0V4V5aSskipV6FaSseqVVtaSifwVVtaSwhilewwVtaSassertwtF">
<label
name="expl:parameter compute_writes"/>
name="expl:VC for compute_writes"/>
<proof
prover="3"
timelimit="3"
......@@ -710,13 +710,13 @@
name="WP_parameter compute_writes.3"
locfile="../wp2.mlw"
loclnum="396" loccnumb="10" loccnume="24"
expl="postcondition"
expl="3. postcondition"
sum="e92018a3cd7629424f5e6f75703c93df"
proved="true"
expanded="false"
shape="CV0aSskiptaSassignVwtaSseqVVaassignsV6aunionV5V4V8Iamany_stepsV6V7V0V8V9aSskipV10FIaassignsV11V5V13Iamany_stepsV11V12V2V13V14aSskipV15FFIaassignsV16V4V18Iamany_stepsV16V17V3V18V19aSskipV20FFaSifwVVtaSwhilewwVtaSassertwtF">
<label
name="expl:parameter compute_writes"/>
name="expl:VC for compute_writes"/>
<proof
prover="4"
timelimit="5"
......@@ -738,13 +738,13 @@
name="WP_parameter compute_writes.4"
locfile="../wp2.mlw"
loclnum="396" loccnumb="10" loccnume="24"
expl="postcondition"
expl="4. postcondition"
sum="04f02a5f3c9b30d1b8610eb3e4005a44"
proved="true"
expanded="false"
shape="CV0aSskiptaSassignVwtaSseqVVtaSifwVVaassignsV8aunionV7V6V10Iamany_stepsV8V9V0V10V11aSskipV12FIaassignsV13V7V15Iamany_stepsV13V14V4V15V16aSskipV17FFIaassignsV18V6V20Iamany_stepsV18V19V5V20V21aSskipV22FFaSwhilewwVtaSassertwtF">
<label
name="expl:parameter compute_writes"/>
name="expl:VC for compute_writes"/>
<proof
prover="3"
timelimit="3"
......@@ -759,13 +759,13 @@
name="WP_parameter compute_writes.5"
locfile="../wp2.mlw"
loclnum="396" loccnumb="10" loccnume="24"
expl="postcondition"
expl="5. postcondition"
sum="d5376a5e25db163dbf2aa636e75f2b7f"
proved="true"
expanded="false"
shape="CV0aSskiptaSassignVwtaSseqVVtaSifwVVtaSwhilewwVaassignsV8V7V10Iamany_stepsV8V9V0V10V11aSskipV12FIaassignsV13V7V15Iamany_stepsV13V14V6V15V16aSskipV17FFaSassertwtF">
<label
name="expl:parameter compute_writes"/>
name="expl:VC for compute_writes"/>
<proof
prover="3"
timelimit="3"
......@@ -780,13 +780,13 @@
name="WP_parameter compute_writes.6"
locfile="../wp2.mlw"
loclnum="396" loccnumb="10" loccnume="24"
expl="postcondition"
expl="6. postcondition"
sum="68c0020cf62818bc3e3e3f5f7f8a9a71"
proved="true"
expanded="false"
shape="CV0aSskiptaSassignVwtaSseqVVtaSifwVVtaSwhilewwVtaSassertwaassignsV7aemptyV9Iamany_stepsV7V8V0V9V10aSskipV11FF">
<label
name="expl:parameter compute_writes"/>
name="expl:VC for compute_writes"/>
<proof
prover="3"
timelimit="3"
......@@ -803,13 +803,13 @@
name="WP_parameter wp"
locfile="../wp2.mlw"
loclnum="428" loccnumb="10" loccnume="12"
expl="parameter wp"
expl="VC for wp"
sum="a5bb90ca75d988a5f3327a76aa664868"
proved="true"
expanded="false"
shape="CV0aSskipavalid_tripleV1V0V1aSseqVVavalid_tripleV5V0V1Iavalid_tripleV5V2V4FIavalid_tripleV4V3V1FaSassignVVavalid_tripleaFletV8V7asubstV1V6V8V0V1Iafresh_in_fmlaV8V1FaSifVVVavalid_tripleaFandaFimpliesaFtermV9V13aFimpliesaFnotaFtermV9V12V0V1Iavalid_tripleV13V10V1FIavalid_tripleV12V11V1FaSassertVavalid_tripleaFimpliesV14V1V0V1aSwhileVVVavalid_tripleaFandV16V19V0V1Iaeval_fmlaV22V23V19Iamany_stepsV20V21V17V22V23aSskipV24FAaeval_fmlaV20V21aFandaFimpliesaFandaFtermV15V16V18aFimpliesaFandaFnotaFtermV15V16V1Iaeval_fmlaV20V21V19FFIavalid_tripleV18V17V16FF">
<label
name="expl:parameter wp"/>
name="expl:VC for wp"/>
<transf
name="split_goal"
proved="true"
......@@ -818,13 +818,13 @@
name="WP_parameter wp.1"
locfile="../wp2.mlw"
loclnum="428" loccnumb="10" loccnume="12"
expl="postcondition"
expl="1. postcondition"
sum="06925acf611bd4e387ea94906ab92a48"
proved="true"
expanded="false"
shape="CV0aSskipavalid_tripleV1V0V1aSseqVVtaSassignVVtaSifVVVtaSassertVtaSwhileVVVtF">
<label
name="expl:parameter wp"/>
name="expl:VC for wp"/>
<proof
prover="0"
timelimit="3"
......@@ -870,13 +870,13 @@
name="WP_parameter wp.2"
locfile="../wp2.mlw"
loclnum="428" loccnumb="10" loccnume="12"
expl="postcondition"
expl="2. postcondition"
sum="b5906335979baf7b7b5f011fe549d714"
proved="true"
expanded="false"
shape="CV0aSskiptaSseqVVavalid_tripleV5V0V1Iavalid_tripleV5V2V4FIavalid_tripleV4V3V1FaSassignVVtaSifVVVtaSassertVtaSwhileVVVtF">
<label
name="expl:parameter wp"/>
name="expl:VC for wp"/>
<proof
prover="0"
timelimit="3"
......@@ -922,13 +922,13 @@
name="WP_parameter wp.3"
locfile="../wp2.mlw"
loclnum="428" loccnumb="10" loccnume="12"
expl="postcondition"
expl="3. postcondition"
sum="cdf49cc0d486ffe057613fda60d8aff8"
proved="true"
expanded="false"
shape="CV0aSskiptaSseqVVtaSassignVVavalid_tripleaFletV6V5asubstV1V4V6V0V1Iafresh_in_fmlaV6V1FaSifVVVtaSassertVtaSwhileVVVtF">
<label
name="expl:parameter wp"/>
name="expl:VC for wp"/>
<proof
prover="0"
timelimit="3"
......@@ -974,13 +974,13 @@
name="WP_parameter wp.4"
locfile="../wp2.mlw"
loclnum="428" loccnumb="10" loccnume="12"
expl="postcondition"
expl="4. postcondition"
sum="112e644b7c1359531a8228d027763854"
proved="true"
expanded="false"
shape="CV0aSskiptaSseqVVtaSassignVVtaSifVVVavalid_tripleaFandaFimpliesaFtermV6V10aFimpliesaFnotaFtermV6V9V0V1Iavalid_tripleV10V7V1FIavalid_tripleV9V8V1FaSassertVtaSwhileVVVtF">
<label
name="expl:parameter wp"/>
name="expl:VC for wp"/>
<proof
prover="3"
timelimit="3"
......@@ -995,13 +995,13 @@
name="WP_parameter wp.5"
locfile="../wp2.mlw"
loclnum="428" loccnumb="10" loccnume="12"
expl="postcondition"
expl="5. postcondition"
sum="c8d6341f72be51c765e727c4e2c4831d"
proved="true"
expanded="false"
shape="CV0aSskiptaSseqVVtaSassignVVtaSifVVVtaSassertVavalid_tripleaFimpliesV9V1V0V1aSwhileVVVtF">
<label
name="expl:parameter wp"/>
name="expl:VC for wp"/>
<proof
prover="0"
timelimit="3"
......@@ -1047,13 +1047,13 @@
name="WP_parameter wp.6"
locfile="../wp2.mlw"
loclnum="428" loccnumb="10" loccnume="12"
expl="postcondition"
expl="6. postcondition"
sum="99af72620f9b7802bed4ae76ef59eb99"
proved="true"
expanded="false"
shape="CV0aSskiptaSseqVVtaSassignVVtaSifVVVtaSassertVtaSwhileVVVavalid_tripleaFandV11V14V0V1Iaeval_fmlaV17V18V14Iamany_stepsV15V16V12V17V18aSskipV19FAaeval_fmlaV15V16aFandaFimpliesaFandaFtermV10V11V13aFimpliesaFandaFnotaFtermV10V11V1Iaeval_fmlaV15V16V14FFIavalid_tripleV13V12V11FF">
<label
name="expl:parameter wp"/>
name="expl:VC for wp"/>
<proof
prover="3"
timelimit="5"
......
......@@ -594,7 +594,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="2.20"/>
<result status="valid" time="2.75"/>
</proof>
</goal>
<goal
......
......@@ -414,13 +414,13 @@
name="WP_parameter wp"
locfile="../wp_total.mlw"
loclnum="343" loccnumb="10" loccnume="12"
expl="parameter wp"
expl="VC for wp"
sum="ca36efc8b3606fb37e394c56407b804c"
proved="false"
expanded="true"
shape="CV0aSskipavalid_tripleV1V0V1aSseqVVavalid_tripleV5V0V1Iavalid_tripleV5V2V4FIavalid_tripleV4V3V1FaSassignVVavalid_tripleasubstV1V6V7V0V1aSifVVVavalid_tripleaFandaFimpliesaFtermV8V12aFimpliesaFnotaFtermV8V11V0V1Iavalid_tripleV12V9V1FIavalid_tripleV11V10V1FaSassertVavalid_tripleaFimpliesV13V1V0V1aSwhileVVVavalid_tripleaFandV15aFandaFimpliesaFandaFtermV14V15V17aFimpliesaFandaFnotaFtermV14V15V1V0V1Iavalid_tripleV17V16V15FF">
<label
name="expl:parameter wp"/>
name="expl:VC for wp"/>
<proof
prover="2"
timelimit="5"
......@@ -438,13 +438,13 @@
name="WP_parameter wp.1"
locfile="../wp_total.mlw"
loclnum="343" loccnumb="10" loccnume="12"
expl="postcondition"
expl="1. postcondition"
sum="d6cc82e1eaea36ec027025bacc29124d"
proved="true"
expanded="false"
shape="CV0aSskipavalid_tripleV1V0V1aSseqVVtaSassignVVtaSifVVVtaSassertVtaSwhileVVVtF">
<label
name="expl:parameter wp"/>
name="expl:VC for wp"/>
<proof
prover="0"
timelimit="5"
......@@ -458,13 +458,13 @@
name="WP_parameter wp.2"
locfile="../wp_total.mlw"
loclnum="343" loccnumb="10" loccnume="12"
expl="postcondition"
expl="2. postcondition"
sum="76687642530d6b2b926881d6a1b65459"
proved="true"
expanded="false"
shape="CV0aSskiptaSseqVVavalid_tripleV5V0V1Iavalid_tripleV5V2V4FIavalid_tripleV4V3V1FaSassignVVtaSifVVVtaSassertVtaSwhileVVVtF">
<label
name="expl:parameter wp"/>
name="expl:VC for wp"/>
<proof
prover="0"
timelimit="5"
......@@ -478,13 +478,13 @@
name="WP_parameter wp.3"
locfile="../wp_total.mlw"
loclnum="343" loccnumb="10" loccnume="12"
expl="postcondition"
expl="3. postcondition"
sum="f18c418c598f9362ab0c1259acc1e691"
proved="true"
expanded="false"
shape="CV0aSskiptaSseqVVtaSassignVVavalid_tripleasubstV1V4V5V0V1aSifVVVtaSassertVtaSwhileVVVtF">
<label
name="expl:parameter wp"/>
name="expl:VC for wp"/>
<proof
prover="0"
timelimit="5"
......@@ -498,13 +498,13 @@
name="WP_parameter wp.4"
locfile="../wp_total.mlw"
loclnum="343" loccnumb="10" loccnume="12"
expl="postcondition"
expl="4. postcondition"
sum="f530afffd2fb136a2c17c31939ae49c9"
proved="true"
expanded="false"
shape="CV0aSskiptaSseqVVtaSassignVVtaSifVVVavalid_tripleaFandaFimpliesaFtermV6V10aFimpliesaFnotaFtermV6V9V0V1Iavalid_tripleV10V7V1FIavalid_tripleV9V8V1FaSassertVtaSwhileVVVtF">
<label
name="expl:parameter wp"/>
name="expl:VC for wp"/>
<proof
prover="0"
timelimit="5"
......@@ -534,13 +534,13 @@
name="WP_parameter wp.5"
locfile="../wp_total.mlw"
loclnum="343" loccnumb="10" loccnume="12"
expl="postcondition"
expl="5. postcondition"
sum="e21e50f41a61c72f110c52d0ced8b9b4"
proved="true"
expanded="true"
shape="CV0aSskiptaSseqVVtaSassignVVtaSifVVVtaSassertVavalid_tripleaFimpliesV9V1V0V1aSwhileVVVtF">
<label
name="expl:parameter wp"/>
name="expl:VC for wp"/>
<proof
prover="0"
timelimit="5"
......@@ -579,13 +579,13 @@
name="WP_parameter wp.6"
locfile="../wp_total.mlw"
loclnum="343" loccnumb="10" loccnume="12"
expl="postcondition"
expl="6. postcondition"
sum="abb6c6de1c3af669e9cd8cd046a9d4ae"
proved="false"
expanded="true"
shape="CV0aSskiptaSseqVVtaSassignVVtaSifVVVtaSassertVtaSwhileVVVavalid_tripleaFandV11aFandaFimpliesaFandaFtermV10V11V13aFimpliesaFandaFnotaFtermV10V11V1V0V1Iavalid_tripleV13V12V11FF">
<label
name="expl:parameter wp"/>
name="expl:VC for wp"/>
<proof
prover="0"
timelimit="5"
......
......@@ -34,13 +34,13 @@
name="WP_parameter sum"
locfile="../add_list.mlw"
loclnum="32" loccnumb="8" loccnume="11"
expl="parameter sum"
expl="VC for sum"
sum="32888636214c7fa4e230bf82e6ac77a3"
proved="true"
expanded="true"
shape="CV0aNilainfix =c0.0aadd_realV0Aainfix =c0aadd_intV0aConsVVCV1aIntegerVainfix =V4aadd_realV0Aainfix =ainfix +V5V3aadd_intV0aRealVainfix =ainfix +.V6V4aadd_realV0Aainfix =V3aadd_intV0Iainfix =V4aadd_realV2Aainfix =V3aadd_intV2FF">
<label
name="expl:parameter sum"/>
name="expl:VC for sum"/>
<proof
prover="0"
timelimit="5"
......@@ -70,13 +70,13 @@
name="WP_parameter main"
locfile="../add_list.mlw"
loclnum="44" loccnumb="4" loccnume="8"
expl="parameter main"
expl="VC for main"
sum="3a10ec75818cb1e12caf058f54c4a224"
proved="true"
expanded="true"
shape="ainfix =V1c4.7Aainfix =V0c22Iainfix =V1aadd_realaConsaIntegerc5aConsaRealc3.3aConsaIntegerc8aConsaRealc1.4aConsaIntegerc9aNilAainfix =V0aadd_intaConsaIntegerc5aConsaRealc3.3aConsaIntegerc8aConsaRealc1.4aConsaIntegerc9aNilF">
<label
name="expl:parameter main"/>
name="expl:VC for main"/>
<proof
prover="1"
timelimit="5"
......@@ -105,13 +105,13 @@
name="WP_parameter sum"
locfile="../add_list.mlw"
loclnum="63" loccnumb="4" loccnume="7"
expl="parameter sum"
expl="VC for sum"
sum="3b3017f3af26037f138ec976b52d04a1"
proved="true"
expanded="true"
shape="CV1aNilainfix =V2aadd_realV0Aainfix =V3aadd_intV0aConsaIntegerVVainfix =ainfix +.V2aadd_realV7aadd_realV0Aainfix =ainfix +V6aadd_intV7aadd_intV0Iainfix =V7V5FIainfix =V6ainfix +V3V4FaConsaRealVVainfix =ainfix +.V10aadd_realV11aadd_realV0Aainfix =ainfix +V3aadd_intV11aadd_intV0Iainfix =V11V9FIainfix =V10ainfix +.V2V8FIainfix =ainfix +.V2aadd_realV1aadd_realV0Aainfix =ainfix +V3aadd_intV1aadd_intV0FAainfix =ainfix +.c0.0aadd_realV0aadd_realV0Aainfix =ainfix +c0aadd_intV0aadd_intV0F">
<label
name="expl:parameter sum"/>
name="expl:VC for sum"/>
<proof
prover="1"
timelimit="5"
......@@ -133,13 +133,13 @@
name="WP_parameter main"
locfile="../add_list.mlw"
loclnum="86" loccnumb="4" loccnume="8"
expl="parameter main"
expl="VC for main"
sum="60c8394cd30207d93f17d7c3fedfc0e9"
proved="true"
expanded="true"
shape="ainfix =V1c4.7Aainfix =V0c22Iainfix =V1aadd_realaConsaIntegerc5aConsaRealc3.3aConsaIntegerc8aConsaRealc1.4aConsaIntegerc9aNilAainfix =V0aadd_intaConsaIntegerc5aConsaRealc3.3aConsaIntegerc8aConsaRealc1.4aConsaIntegerc9aNilF">
<label
name="expl:parameter main"/>
name="expl:VC for main"/>
<proof
prover="1"
timelimit="5"
......
This source diff could not be displayed because it is too large. You can view the blob instead.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
......@@ -23,13 +23,13 @@
name="WP_parameter insertion_sort"
locfile="../arm.mlw"
loclnum="16" loccnumb="6" loccnume="20"
expl="parameter insertion_sort"
expl="VC for insertion_sort"
sum="7748fd507776784f81c6745ae3a11c7f"
proved="false"
expanded="false"
shape="iainfix &lt;=V5c10iainfix &lt;agetV13V11agetV13ainfix -V11c1ainfix &lt;V18V11Aainfix &lt;=c0V11Aainfix &lt;=ainfix *c2V15ainfix +ainfix *ainfix -V5c2ainfix -V5c1ainfix *c2ainfix -V5V18Aainvamk arrayV0V17Aainfix &lt;=V18V5Aainfix &lt;=c1V18Iainfix =V18ainfix -V11c1FIainfix =V17asetV16ainfix -V11c1agetV13V11FAainfix &lt;ainfix -V11c1V0Aainfix &lt;=c0ainfix -V11c1Iainfix =V16asetV13V11agetV13ainfix -V11c1FAainfix &lt;V11V0Aainfix &lt;=c0V11Aainfix &lt;ainfix -V11c1V0Aainfix &lt;=c0ainfix -V11c1Aainfix &lt;V11V0Aainfix &lt;=c0V11Iainfix =V15ainfix +V12c1Fainfix &lt;ainfix -c10V19ainfix -c10V5Aainfix &lt;=c0ainfix -c10V5Aainfix &lt;=ainfix *c2V12ainfix *ainfix -V19c2ainfix -V19c1Aainfix =V10ainfix -V19c2AainvV14Aainfix &lt;=V19c11Aainfix &lt;=c2V19Iainfix =V19ainfix +V5c1FAainfix &lt;V11V0Aainfix &lt;=c0V11Aainfix &lt;ainfix -V11c1V0Aainfix &lt;=c0ainfix -V11c1Iainfix &lt;=ainfix *c2V12ainfix +ainfix *ainfix -V5c2ainfix -V5c1ainfix *c2ainfix -V5V11AainvV14Aainfix &lt;=V11V5Aainfix &lt;=c1V11Lamk arrayV0V13FAainfix &lt;=ainfix *c2V6ainfix +ainfix *ainfix -V5c2ainfix -V5c1ainfix *c2ainfix -V5V5AainvV9Aainfix &lt;=V5V5Aainfix &lt;=c1V5Iainfix =V10ainfix +V7c1Fainfix &lt;=V6c45Aainfix =V7c9Iainfix &lt;=ainfix *c2V6ainfix *ainfix -V5c2ainfix -V5c1Aainfix =V7ainfix -V5c2AainvV9Aainfix &lt;=V5c11Aainfix &lt;=c2V5Lamk arrayV0V8FAainfix &lt;=ainfix *c2V1ainfix *ainfix -c2c2ainfix -c2c1Aainfix =V2ainfix -c2c2AainvV4Aainfix &lt;=c2c11Aainfix &lt;=c2c2Iainfix =V1c0Aainfix =V2c0AainvV4Lamk arrayV0V3FF">
<label
name="expl:parameter insertion_sort"/>
name="expl:VC for insertion_sort"/>
</goal>
</theory>
<theory
......@@ -49,13 +49,13 @@
name="WP_parameter path_init_l2"
locfile="../arm.mlw"
loclnum="120" loccnumb="6" loccnume="18"
expl="postcondition"
expl="VC for path_init_l2"
sum="795f8de35a06a3c2af46ce51dec5f462"
proved="true"
expanded="true"
shape="ainv_l2V5V0V2Iainfix =V5amixfix [&lt;-]V1ainfix -V0c16V4FIainfix =V4c2FIainfix =V3c0FIainfix =V2c0FIainvV1AaseparationV0F">
<label
name="expl:parameter path_init_l2"/>