updated proof sessions on moloch

parent 459b7b3b
This diff is collapsed.
This diff is collapsed.
......@@ -3,167 +3,168 @@
<why3session name="examples/programs/insertion_sort/why3session.xml">
<file name="../insertion_sort.mlw" verified="true" expanded="true">
<theory name="WP InsertionSort" verified="true" expanded="true">
<goal name="WP_parameter insertion_sort" expl="correctness of parameter insertion_sort" sum="bc3a6120adf2049be457856f1baff403" proved="true" expanded="true">
<goal name="WP_parameter insertion_sort" expl="correctness of parameter insertion_sort" sum="52df11dfc4b1b1606ca27380dcf91a75" proved="true" expanded="true">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter insertion_sort.1" expl="normal postcondition" sum="8a83eb3d3e1d906f6d1a291c7e68654f" proved="true" expanded="false">
<goal name="WP_parameter insertion_sort.1" expl="normal postcondition" sum="bb6492bb0670c7bb75e24ba8da2a88e2" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="30" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter insertion_sort.2" expl="for loop initialization" sum="d823763feca46ffe0936829894f004de" proved="true" expanded="false">
<goal name="WP_parameter insertion_sort.2" expl="for loop initialization" sum="1e417f4ec6a45a2be290cc3e6fc35473" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="30" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter insertion_sort.3" expl="for loop preservation" sum="21459ef296a7ea9ec57999ff5524be62" proved="true" expanded="true">
<goal name="WP_parameter insertion_sort.3" expl="for loop preservation" sum="ce2751087c1b44c33a1945304e896655" proved="true" expanded="true">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter insertion_sort.3.1" expl="for loop preservation" sum="a2c2c11d1665e60531729b47497902ab" proved="true" expanded="false">
<goal name="WP_parameter insertion_sort.3.1" expl="for loop preservation" sum="1fc8f8a33493bc212cf613b97d1bdaf5" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="30" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter insertion_sort.3.2" expl="for loop preservation" sum="ed0bef84df2eb8e1592dd4781d1e3ea5" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="8.59"/>
<goal name="WP_parameter insertion_sort.3.2" expl="for loop preservation" sum="dda6b7bb0df5896a7498d61e1bab580f" proved="true" expanded="false">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter insertion_sort.3.3" expl="for loop preservation" sum="fbf3fba2d0700655dc599cea30c179dd" proved="true" expanded="false">
<goal name="WP_parameter insertion_sort.3.3" expl="for loop preservation" sum="4c5ef1fc9cbccfe9b38fa239ccce671b" proved="true" expanded="false">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter insertion_sort.3.4" expl="for loop preservation" sum="3b93ba7f664d67daee54a808301575d0" proved="true" expanded="false">
<goal name="WP_parameter insertion_sort.3.4" expl="for loop preservation" sum="2b4a02a52328dd3ae37e3fbcf4e6e065" proved="true" expanded="false">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter insertion_sort.3.5" expl="for loop preservation" sum="131b7f79ac0efc72a3c852bc690c79af" proved="true" expanded="false">
<goal name="WP_parameter insertion_sort.3.5" expl="for loop preservation" sum="b6cd8b74e4abdad61d699b45afcf91e1" proved="true" expanded="false">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter insertion_sort.3.6" expl="for loop preservation" sum="ba185f70d1caa35b02582be78209c478" proved="true" expanded="false">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.04"/>
<goal name="WP_parameter insertion_sort.3.6" expl="for loop preservation" sum="7469ac21f28641078ecf05befb432b4a" proved="true" expanded="false">
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.10"/>
</proof>
</goal>
<goal name="WP_parameter insertion_sort.3.7" expl="for loop preservation" sum="55c905465bdd1f889004f27654a161e2" proved="true" expanded="true">
<goal name="WP_parameter insertion_sort.3.7" expl="for loop preservation" sum="a79927e40e82f44bb2b90202f518345c" proved="true" expanded="true">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter insertion_sort.3.7.1" expl="for loop preservation" sum="6999b5952ed0db51b6e05976c81a1cdc" proved="true" expanded="false">
<goal name="WP_parameter insertion_sort.3.7.1" expl="for loop preservation" sum="a18c6d454fee9e450b12110bd9e7db2d" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter insertion_sort.3.7.2" expl="for loop preservation" sum="beaf48edf96cecc237e27f7ff511d3f4" proved="true" expanded="false">
<goal name="WP_parameter insertion_sort.3.7.2" expl="for loop preservation" sum="50d8b516f2f3651f71e4efa9e2ac7642" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter insertion_sort.3.7.3" expl="for loop preservation" sum="f0733df5b462ba543582561312965c2d" proved="true" expanded="true">
<goal name="WP_parameter insertion_sort.3.7.3" expl="for loop preservation" sum="075afbb9aa06a22be826b537dbf2212c" proved="true" expanded="true">
<proof prover="coq" timelimit="10" edited="insertion_sort_WP_InsertionSort_WP_parameter_insertion_sort_1.v" obsolete="false">
<result status="valid" time="0.58"/>
<result status="valid" time="0.57"/>
</proof>
</goal>
<goal name="WP_parameter insertion_sort.3.7.4" expl="for loop preservation" sum="eca5cfab2c4201aa910ca8642d5183fb" proved="true" expanded="false">
<goal name="WP_parameter insertion_sort.3.7.4" expl="for loop preservation" sum="756f7fe0e228ea72695f12fe2ab1edd1" proved="true" expanded="false">
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.12"/>
<result status="valid" time="0.10"/>
</proof>
</goal>
<goal name="WP_parameter insertion_sort.3.7.5" expl="for loop preservation" sum="730fdaf1ff6d25b3da515773d0d8164f" proved="true" expanded="false">
<goal name="WP_parameter insertion_sort.3.7.5" expl="for loop preservation" sum="cc3c7f1b977d1749b4166a006261c7ae" proved="true" expanded="false">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="1.80"/>
<result status="valid" time="1.75"/>
</proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter insertion_sort.3.8" expl="for loop preservation" sum="ba495261035f2d0b4998d37630318a3c" proved="true" expanded="false">
<goal name="WP_parameter insertion_sort.3.8" expl="for loop preservation" sum="5b62db4c1432a705b008b863a253ad64" proved="true" expanded="false">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof prover="alt-ergo" timelimit="30" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter insertion_sort.3.9" expl="for loop preservation" sum="9b166607ee4741735832e3669a54198f" proved="true" expanded="false">
<goal name="WP_parameter insertion_sort.3.9" expl="for loop preservation" sum="b19426a5d510062a4ccb7ae7c3b43b43" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="30" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter insertion_sort.3.10" expl="for loop preservation" sum="f6490b0329fb7943c181d0cc2bde175a" proved="true" expanded="false">
<goal name="WP_parameter insertion_sort.3.10" expl="for loop preservation" sum="396ea238782f9a6e6b140616631fe0c3" proved="true" expanded="false">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter insertion_sort.3.11" expl="for loop preservation" sum="ad9f3460488d56ddc38ed52699786c71" proved="true" expanded="false">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.04"/>
</proof>
<goal name="WP_parameter insertion_sort.3.11" expl="for loop preservation" sum="5ad6de4ad305198f5d9e6bff737f0222" proved="true" expanded="false">
<transf name="split_goal" proved="true" expanded="false">
<goal name="WP_parameter insertion_sort.3.11.1" expl="for loop preservation" sum="5ad6de4ad305198f5d9e6bff737f0222" proved="true" expanded="false">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.04"/>
</proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter insertion_sort.3.12" expl="for loop preservation" sum="500763abc5d5cebac9ccc10553764f20" proved="true" expanded="false">
<goal name="WP_parameter insertion_sort.3.12" expl="for loop preservation" sum="3b06628d16ec9615d78d1fe59d95b9ef" proved="true" expanded="false">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter insertion_sort.3.13" expl="for loop preservation" sum="31d486d834ea31da4517158023216858" proved="true" expanded="false">
<goal name="WP_parameter insertion_sort.3.13" expl="for loop preservation" sum="6f0fd17e727ebbf5cc9422090d3365ce" proved="true" expanded="false">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter insertion_sort.3.14" expl="for loop preservation" sum="7afa433023157105092e6fe898ab0cf5" proved="true" expanded="false">
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<goal name="WP_parameter insertion_sort.3.14" expl="for loop preservation" sum="5487e3c6216b417d7f62ec51d750e3de" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="30" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal name="WP_parameter insertion_sort.3.15" expl="for loop preservation" sum="08f7db0e1e109e6b9241a83ce7b8be31" proved="true" expanded="false">
<goal name="WP_parameter insertion_sort.3.15" expl="for loop preservation" sum="cdd1c1fdf67e200f33ddcf17b1e60790" proved="true" expanded="false">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal name="WP_parameter insertion_sort.3.16" expl="for loop preservation" sum="60640ae10b3fe9f11840f76f52a0bc08" proved="true" expanded="false">
<goal name="WP_parameter insertion_sort.3.16" expl="for loop preservation" sum="ecfab033d4dd9d047905e54287fb3267" proved="true" expanded="false">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal name="WP_parameter insertion_sort.3.17" expl="for loop preservation" sum="2fc87a21e4f6716b13162a04b52af2b8" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="30" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<goal name="WP_parameter insertion_sort.3.17" expl="for loop preservation" sum="4287adf46acf015271010995d8abb858" proved="true" expanded="false">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal name="WP_parameter insertion_sort.3.18" expl="for loop preservation" sum="f5b0599767315937e11b02b0ce2ecdec" proved="true" expanded="false">
<goal name="WP_parameter insertion_sort.3.18" expl="for loop preservation" sum="0fb561d9f960f932181d3ea8756b4bb1" proved="true" expanded="false">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter insertion_sort.3.19" expl="for loop preservation" sum="35da8b8517b6afc6195f7e1f8219e5e3" proved="true" expanded="false">
<goal name="WP_parameter insertion_sort.3.19" expl="for loop preservation" sum="8ce0c1bce0303508d0623a011a2a29d7" proved="true" expanded="false">
<transf name="split_goal" proved="true" expanded="false">
<goal name="WP_parameter insertion_sort.3.19.1" expl="for loop preservation" sum="4ba731b5f55ee4b7a87587dc92b1df7b" proved="true" expanded="false">
<goal name="WP_parameter insertion_sort.3.19.1" expl="for loop preservation" sum="e5a30d8c682249f3b7ce2ae8073297b3" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter insertion_sort.3.19.2" expl="for loop preservation" sum="077f3072257a27564247ad79a8ff6843" proved="true" expanded="false">
<goal name="WP_parameter insertion_sort.3.19.2" expl="for loop preservation" sum="124e17a3f3ee82824d1eb8cbcf5b8ade" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter insertion_sort.3.20" expl="for loop preservation" sum="e74d04fcc77fb684f7374098d63af312" proved="true" expanded="false">
<goal name="WP_parameter insertion_sort.3.20" expl="for loop preservation" sum="75dc2a24503ea34b53169d53de464e2d" proved="true" expanded="false">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter insertion_sort.3.21" expl="for loop preservation" sum="061a74f0c0e3a2431d42e080689bc38b" proved="true" expanded="false">
<goal name="WP_parameter insertion_sort.3.21" expl="for loop preservation" sum="b4c3c90f52459988cece36a839594a4d" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="30" edited="" obsolete="false">
<result status="valid" time="18.69"/>
<result status="valid" time="19.82"/>
</proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter insertion_sort.4" expl="normal postcondition" sum="415dc3a913dc323b67ffdb8578361ddc" proved="true" expanded="false">
<goal name="WP_parameter insertion_sort.4" expl="normal postcondition" sum="31133fccb9f8e19b1389d9c2199b636b" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="30" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
......
......@@ -22,22 +22,46 @@
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter sqrt.1" expl="normal postcondition" sum="bb87fe0b8434e8d093943f1210b71ec5" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter sqrt.2" expl="normal postcondition" sum="84710358cd8ada1454c80929dd0b421a" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter sqrt.3" expl="loop invariant init" sum="c11b288394dbf06ca63d6f183eed8902" proved="true" expanded="true">
<proof prover="z3" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.55"/>
</proof>
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter sqrt.3.1" expl="correctness of parameter sqrt" sum="e2c9e9d55c1fb96ff6927b0bf7ea08c3" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter sqrt.3.2" expl="correctness of parameter sqrt" sum="89a7b5a1daf6b4e2519b771a686341ed" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter sqrt.3.3" expl="correctness of parameter sqrt" sum="1e7292150fa5b3ff64df1f967aa339dd" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.34"/>
</proof>
</goal>
<goal name="WP_parameter sqrt.3.4" expl="correctness of parameter sqrt" sum="7c4b5c925e20094d1a40d385f8888899" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter sqrt.3.5" expl="correctness of parameter sqrt" sum="6ecbaf6ffa704b33dd36c7a1db072d41" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter sqrt.4" expl="loop invariant preservation" sum="635d4755b940a642f5f361e72d63b2ad" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="11.31"/>
<result status="valid" time="9.22"/>
</proof>
</goal>
<goal name="WP_parameter sqrt.5" expl="loop variant decreases" sum="0e4fa9a7a38870c021afae8a4e42ba92" proved="true" expanded="true">
......@@ -47,7 +71,7 @@
</goal>
<goal name="WP_parameter sqrt.6" expl="normal postcondition" sum="ee09cf3d584c24c45c524135e3d35bf3" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.22"/>
<result status="valid" time="0.18"/>
</proof>
</goal>
</transf>
......
This diff is collapsed.
......@@ -3,34 +3,44 @@
<why3session name="examples/programs/muller/why3session.xml">
<file name="../muller.mlw" verified="true" expanded="true">
<theory name="WP Muller" verified="true" expanded="true">
<goal name="WP_parameter compact" expl="correctness of parameter compact" sum="bcedd535085039b1a724f6ab75f1b818" proved="true" expanded="true">
<goal name="WP_parameter compact" expl="correctness of parameter compact" sum="e0d9de9cbb5be379c4a4b699abf1a591" proved="true" expanded="true">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter compact.1" expl="for loop initialization" sum="dd0305a2f1fce9b990ae437ad6329b29" proved="true" expanded="true">
<goal name="WP_parameter compact.1" expl="precondition" sum="8d7dd66c74645ad012bcb4ba69b4e9c5" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter compact.2" expl="for loop initialization" sum="298245d5916edcd2a81a00c9a9672d29" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter compact.2" expl="for loop preservation" sum="f43e9c0f1402db49303a2ad429bd45f7" proved="true" expanded="true">
<goal name="WP_parameter compact.3" expl="for loop preservation" sum="c8e091485b0cb29d289366398dd24982" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter compact.3" expl="for loop initialization" sum="c0e3d5971e572acd3db62fb9e102a17c" proved="true" expanded="true">
<goal name="WP_parameter compact.4" expl="for loop initialization" sum="c0e3d5971e572acd3db62fb9e102a17c" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter compact.4" expl="for loop preservation" sum="4eac813b68d3b337fe13742d52c581ec" proved="true" expanded="true">
<goal name="WP_parameter compact.5" expl="for loop preservation" sum="4eac813b68d3b337fe13742d52c581ec" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter compact.5" expl="for loop initialization" sum="a2e57724df2cb5bae002bfdde74ecae8" proved="true" expanded="true">
<goal name="WP_parameter compact.6" expl="precondition" sum="ac8613151f21c8de359a74b14fe8d685" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.08"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter compact.7" expl="for loop initialization" sum="3e2510029b7c8c85e870ea4845346dca" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.05"/>
</proof>
</goal>
<goal name="WP_parameter compact.6" expl="for loop preservation" sum="2ca955a9ae47f0ea983401697e0a5c48" proved="true" expanded="true">
<goal name="WP_parameter compact.8" expl="for loop preservation" sum="952c11e9ad48698d16b735d95d2079dc" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.08"/>
</proof>
......
......@@ -3,68 +3,65 @@
<why3session name="examples/programs/same_fringe/why3session.xml">
<file name="../same_fringe.mlw" verified="true" expanded="true">
<theory name="WP SameFringe" verified="true" expanded="true">
<goal name="WP_parameter enum" expl="correctness of parameter enum" sum="e9726f7d7c95a4794564455c355d2e98" proved="true" expanded="true">
<goal name="WP_parameter enum" expl="correctness of parameter enum" sum="bdf86692af3d9108fb10b1c5ad0566cb" proved="true" expanded="true">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter enum.1" expl="correctness of parameter enum" sum="1d4de1209b3d1ba88eede8b20f8490ca" proved="true" expanded="true">
<goal name="WP_parameter enum.1" expl="correctness of parameter enum" sum="a6693a559bfaec7856fabbbd720cd46d" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal name="WP_parameter enum.2" expl="correctness of parameter enum" sum="7d167a1f5d4bba0cac2051700bc46f20" proved="true" expanded="true">
<goal name="WP_parameter enum.2" expl="correctness of parameter enum" sum="1738f0e9c67bc5354834008977e07775" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter enum.3" expl="correctness of parameter enum" sum="d589051c538ea56f9067cf37e4338ad5" proved="true" expanded="true">
<goal name="WP_parameter enum.3" expl="correctness of parameter enum" sum="ad0c532ed8c898123ca6cc75e6c44cb5" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter eq_enum" expl="correctness of parameter eq_enum" sum="36b971b55004683d0deea3ef3b0e6bb2" proved="true" expanded="true">
<goal name="WP_parameter eq_enum" expl="correctness of parameter eq_enum" sum="d3dfe508d88185c560d08001b044edcb" proved="true" expanded="true">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter eq_enum.1" expl="correctness of parameter eq_enum" sum="ea0d4c9d1c8f7d167e87e7aff53ca816" proved="true" expanded="true">
<goal name="WP_parameter eq_enum.1" expl="correctness of parameter eq_enum" sum="541824b988f4678bfb4e4b13dab9ba9b" proved="true" expanded="true">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.05"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="3.34"/>
</proof>
</goal>
<goal name="WP_parameter eq_enum.2" expl="correctness of parameter eq_enum" sum="b18e08658a466dcd098260a484056321" proved="true" expanded="true">
<goal name="WP_parameter eq_enum.2" expl="correctness of parameter eq_enum" sum="6af4cbaa87aae0d4f4abb13e1285a5e1" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.04"/>
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter eq_enum.3" expl="correctness of parameter eq_enum" sum="d657e3002ead9ebcaaa3a070f87652d8" proved="true" expanded="true">
<goal name="WP_parameter eq_enum.3" expl="correctness of parameter eq_enum" sum="57cd5beee94ebf4da014c8011ed7ec67" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter eq_enum.4" expl="correctness of parameter eq_enum" sum="7b9b8abedf01c11d772a4ae8cac1b761" proved="true" expanded="true">
<goal name="WP_parameter eq_enum.4" expl="correctness of parameter eq_enum" sum="25a36c430de0ebe984ce2e0f408f1a07" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter eq_enum.5" expl="correctness of parameter eq_enum" sum="9339223a232b57f6153c3bc438d59b41" proved="true" expanded="true">
<goal name="WP_parameter eq_enum.5" expl="correctness of parameter eq_enum" sum="97b8f446464842dc4d839da5b5961fdb" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter eq_enum.6" expl="correctness of parameter eq_enum" sum="a7f92507aab9c8f1d05ec29fc269e39f" proved="true" expanded="true">
<goal name="WP_parameter eq_enum.6" expl="correctness of parameter eq_enum" sum="32374fa5283ef3c4909474d899dcacdf" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter same_fringe" expl="normal postcondition" sum="1613d8190d23c87c5b9cf7f82a003225" proved="true" expanded="true">
<goal name="WP_parameter same_fringe" expl="normal postcondition" sum="735f92bd11fb50afcf213c093d95fac9" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
</theory>
......
......@@ -45,49 +45,77 @@
<result status="valid" time="0.05"/>
</proof>
</goal>
<goal name="WP_parameter list_member" expl="correctness of parameter list_member" sum="b4187b983e65459b73a851378ae0705f" proved="true" expanded="true">
<goal name="WP_parameter list_member" expl="correctness of parameter list_member" sum="9f5379910e3ab69268b87110e5b2f6ec" proved="true" expanded="true">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter list_member.1" expl="loop invariant init" sum="31f4e55cabffdd4d63e20199d1a77867" proved="true" expanded="true">
<goal name="WP_parameter list_member.1" expl="loop invariant init" sum="2427534f9875ef4f7e740348ecc9d19d" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter list_member.2" expl="precondition" sum="edfdcfe23487d8d0453cb4a42accae64" proved="true" expanded="true">
<goal name="WP_parameter list_member.2" expl="precondition" sum="7a9c559ad726b570a0fed8c28839b8c6" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter list_member.3" expl="precondition" sum="58f178b2f8c525bf8edc57ed7808237d" proved="true" expanded="true">
<goal name="WP_parameter list_member.3" expl="precondition" sum="a79ad62ad6ed9ec59a2c74fe848e05cf" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter list_member.4" expl="loop invariant preservation" sum="927d4cc123030bc09cf89d7be84c6724" proved="true" expanded="true">
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.67"/>
</proof>
<goal name="WP_parameter list_member.4" expl="loop invariant preservation" sum="215c974d6dfeff935e146faf4d7f3d1b" proved="true" expanded="true">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter list_member.4.1" expl="correctness of parameter list_member" sum="3f821be6ffa21b09036aed73b7e68d2c" proved="true" expanded="true">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.12"/>
</proof>
</goal>
<goal name="WP_parameter list_member.4.2" expl="correctness of parameter list_member" sum="3cd22ee1b24afb93f8750c379e9bcdd7" proved="true" expanded="true">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.07"/>
</proof>
</goal>
<goal name="WP_parameter list_member.4.3" expl="correctness of parameter list_member" sum="85e836a5b807b34786be3770ff8b6fa4" proved="true" expanded="true">
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="2.52"/>
</proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter list_member.5" expl="loop variant decreases" sum="6bbef49de1a1b1573727678eefae860e" proved="true" expanded="true">
<goal name="WP_parameter list_member.5" expl="loop variant decreases" sum="cb0bf341f17f4423bdd86b8daea61963" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter list_member.6" expl="precondition" sum="0e12c88f2567c5f0aea89a6304cd0642" proved="true" expanded="true">
<goal name="WP_parameter list_member.6" expl="precondition" sum="b6dd890555e5d40155e34a086b903a05" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter list_member.7" expl="loop invariant preservation" sum="7f5d2ee098045d0c9285ac28dfa83a7d" proved="true" expanded="true">
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.67"/>
</proof>
<goal name="WP_parameter list_member.7" expl="loop invariant preservation" sum="e3639fdc1ba5b66b2a667882e81e97fe" proved="true" expanded="true">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter list_member.7.1" expl="correctness of parameter list_member" sum="ed16b3cb409a9d3e6b5ae66a984b7c5c" proved="true" expanded="true">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.11"/>
</proof>
</goal>
<goal name="WP_parameter list_member.7.2" expl="correctness of parameter list_member" sum="a12565f4a5f0fdfc92419781c589db1d" proved="true" expanded="true">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.07"/>
</proof>
</goal>
<goal name="WP_parameter list_member.7.3" expl="correctness of parameter list_member" sum="95edc94d7c8ef7c3869e1d2dd4bf6513" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.04"/>
</proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter list_member.8" expl="loop variant decreases" sum="c067362f1067ed1aaabae3ef66460a35" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
<goal name="WP_parameter list_member.8" expl="loop variant decreases" sum="14eaf30bacee199698f2da78eefadb73" proved="true" expanded="true">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.10"/>
</proof>
</goal>
<goal name="WP_parameter list_member.9" expl="normal postcondition" sum="911c750ca19f35b9e7d64137fb7d7a4a" proved="true" expanded="true">
<goal name="WP_parameter list_member.9" expl="normal postcondition" sum="9a8c7edb62f1e94f565c826dabfd1479" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
......
......@@ -5,7 +5,7 @@
<theory name="WP MaxAndSum" verified="true" expanded="true">
<goal name="WP_parameter max_sum" expl="correctness of parameter max_sum" sum="4385c731695d5dfaf677a2e64e525aa3" proved="true" expanded="true">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter max_sum.1" expl="normal postcondition" sum="50bff07f8e225489792e93970faf39bd" proved="true" expanded="true">
<goal name="WP_parameter max_sum.1" expl="correctness of parameter max_sum" sum="50bff07f8e225489792e93970faf39bd" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
......@@ -49,7 +49,7 @@
</goal>
</transf>
</goal>
<goal name="WP_parameter max_sum.4" expl="normal postcondition" sum="24085f97178d85b4b3755974f802c949" proved="true" expanded="true">
<goal name="WP_parameter max_sum.4" expl="correctness of parameter max_sum" sum="24085f97178d85b4b3755974f802c949" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
......@@ -60,71 +60,91 @@
<theory name="WP MaxAndSum2" verified="true" expanded="true">
<goal name="WP_parameter max_sum" expl="correctness of parameter max_sum" sum="511e229ad52d526ab7b61ac3af286c3c" proved="true" expanded="true">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter max_sum.1" expl="normal postcondition" sum="a25d062c03fcef01c886de12151b080f" proved="true" expanded="true">
<goal name="WP_parameter max_sum.1" expl="correctness of parameter max_sum" sum="1527d45f4103d912473c45e5e2b3f0e0" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>