Commit f5fc33ec authored by MARCHE Claude's avatar MARCHE Claude

updated sessions after running a full replay with forced save

parent cce2eb15
...@@ -2,30 +2,30 @@ ...@@ -2,30 +2,30 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN" <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd"> "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4"> <why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.95.1" timelimit="5" memlimit="1000"/> <prover id="0" name="CVC3" version="2.4.1" timelimit="5" memlimit="1000"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="5" memlimit="1000"/> <prover id="1" name="Alt-Ergo" version="0.95.1" timelimit="5" memlimit="1000"/>
<prover id="2" name="Z3" version="3.2" timelimit="5" memlimit="1000"/> <prover id="2" name="Z3" version="3.2" timelimit="5" memlimit="1000"/>
<file name="../add_list.mlw" expanded="true"> <file name="../add_list.mlw" expanded="true">
<theory name="SumList"> <theory name="SumList" sum="3880e7768b9fbb987ee1c04cefb36cde">
</theory> </theory>
<theory name="AddListRec" expanded="true"> <theory name="AddListRec" sum="0e8ef89f2db251f08e2ead111b715f73" expanded="true">
<goal name="WP_parameter sum" expl="VC for sum" sum="0ad629c2956d434cdf621a03e0b7c7ba" expanded="true"> <goal name="WP_parameter sum" expl="VC for sum" expanded="true">
<proof prover="0"><result status="valid" time="0.02"/></proof> <proof prover="0"><result status="valid" time="0.01"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof> <proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof> <proof prover="2"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="WP_parameter main" expl="VC for main" sum="6b4e350cd7d1b4015bab61dc01e96aec" expanded="true"> <goal name="WP_parameter main" expl="VC for main" expanded="true">
<proof prover="1"><result status="valid" time="0.02"/></proof> <proof prover="0"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof> <proof prover="2"><result status="valid" time="0.02"/></proof>
</goal> </goal>
</theory> </theory>
<theory name="AddListImp" expanded="true"> <theory name="AddListImp" sum="e32a291b70f70653cf52bd57a896af4d" expanded="true">
<goal name="WP_parameter sum" expl="VC for sum" sum="82f58e47d4e58d15d59a87efee2a6ad8" expanded="true"> <goal name="WP_parameter sum" expl="VC for sum" expanded="true">
<proof prover="1"><result status="valid" time="0.02"/></proof> <proof prover="0"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof> <proof prover="2"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="WP_parameter main" expl="VC for main" sum="9051692e9ac1a4d1f56386a0fd7d440f" expanded="true"> <goal name="WP_parameter main" expl="VC for main" expanded="true">
<proof prover="1"><result status="valid" time="0.02"/></proof> <proof prover="0"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof> <proof prover="2"><result status="valid" time="0.02"/></proof>
</goal> </goal>
</theory> </theory>
......
This diff is collapsed.
...@@ -4,59 +4,59 @@ ...@@ -4,59 +4,59 @@
<why3session shape_version="4"> <why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/> <prover id="0" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<file name="../algo64.mlw" expanded="true"> <file name="../algo64.mlw" expanded="true">
<theory name="Algo64" expanded="true"> <theory name="Algo64" sum="103ff1827edf820d54c612b484b267e3" expanded="true">
<goal name="WP_parameter quicksort" expl="VC for quicksort" sum="b3c80285a2f93720ffbeec07fe9484f7" expanded="true"> <goal name="WP_parameter quicksort" expl="VC for quicksort" expanded="true">
<transf name="split_goal_wp" expanded="true"> <transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter quicksort.1" expl="1. precondition" sum="60641f0dd6fd791e2eb04365466e4b67"> <goal name="WP_parameter quicksort.1" expl="1. precondition">
<proof prover="0"><result status="valid" time="0.02"/></proof> <proof prover="0"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="WP_parameter quicksort.2" expl="2. variant decrease" sum="d044cdfb327536252d9d35d6c8c8d779"> <goal name="WP_parameter quicksort.2" expl="2. variant decrease">
<proof prover="0"><result status="valid" time="0.01"/></proof> <proof prover="0"><result status="valid" time="0.01"/></proof>
</goal> </goal>
<goal name="WP_parameter quicksort.3" expl="3. precondition" sum="c51bbed49cb41b5186ee449ca22b5d0f"> <goal name="WP_parameter quicksort.3" expl="3. precondition">
<proof prover="0"><result status="valid" time="0.01"/></proof> <proof prover="0"><result status="valid" time="0.01"/></proof>
</goal> </goal>
<goal name="WP_parameter quicksort.4" expl="4. assertion" sum="a62cc8ba874159b234bb59428fe08b3c"> <goal name="WP_parameter quicksort.4" expl="4. assertion">
<proof prover="0"><result status="valid" time="0.14"/></proof> <proof prover="0"><result status="valid" time="0.14"/></proof>
</goal> </goal>
<goal name="WP_parameter quicksort.5" expl="5. variant decrease" sum="cbc7bedb98f7451986a3718eda496a7c"> <goal name="WP_parameter quicksort.5" expl="5. variant decrease">
<proof prover="0"><result status="valid" time="0.02"/></proof> <proof prover="0"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="WP_parameter quicksort.6" expl="6. precondition" sum="fff053c1414e1610d034118e841c6500"> <goal name="WP_parameter quicksort.6" expl="6. precondition">
<proof prover="0"><result status="valid" time="0.02"/></proof> <proof prover="0"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="WP_parameter quicksort.7" expl="7. assertion" sum="c286faac90136a80939022ab618896af"> <goal name="WP_parameter quicksort.7" expl="7. assertion">
<proof prover="0"><result status="valid" time="2.07"/></proof> <proof prover="0"><result status="valid" time="2.07"/></proof>
</goal> </goal>
<goal name="WP_parameter quicksort.8" expl="8. postcondition" sum="bf52bb94f3ce94cc8aeb29cfbd99aba5"> <goal name="WP_parameter quicksort.8" expl="8. postcondition">
<proof prover="0"><result status="valid" time="0.53"/></proof> <proof prover="0"><result status="valid" time="0.53"/></proof>
</goal> </goal>
<goal name="WP_parameter quicksort.9" expl="9. postcondition" sum="97cc3e363dcba7833cc03add00eca267"> <goal name="WP_parameter quicksort.9" expl="9. postcondition">
<proof prover="0"><result status="valid" time="0.16"/></proof> <proof prover="0"><result status="valid" time="0.16"/></proof>
</goal> </goal>
<goal name="WP_parameter quicksort.10" expl="10. postcondition" sum="16dcef28364b3606b5af7ea67b96d36c"> <goal name="WP_parameter quicksort.10" expl="10. postcondition">
<proof prover="0"><result status="valid" time="0.01"/></proof> <proof prover="0"><result status="valid" time="0.01"/></proof>
</goal> </goal>
<goal name="WP_parameter quicksort.11" expl="11. postcondition" sum="a2af1e38ef1266733de9df088d4b57d3"> <goal name="WP_parameter quicksort.11" expl="11. postcondition">
<proof prover="0"><result status="valid" time="0.02"/></proof> <proof prover="0"><result status="valid" time="0.02"/></proof>
</goal> </goal>
</transf> </transf>
</goal> </goal>
<goal name="WP_parameter qs" expl="VC for qs" sum="c020ba36a9f1cbc706a81299d7e67dc5"> <goal name="WP_parameter qs" expl="VC for qs">
<transf name="split_goal_wp"> <transf name="split_goal_wp">
<goal name="WP_parameter qs.1" expl="1. precondition" sum="af20b26413ca9ad74cd53bb91ad9bf58"> <goal name="WP_parameter qs.1" expl="1. precondition">
<proof prover="0"><result status="valid" time="0.02"/></proof> <proof prover="0"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="WP_parameter qs.2" expl="2. postcondition" sum="8c72e4401654ed269af73c95614802d2"> <goal name="WP_parameter qs.2" expl="2. postcondition">
<proof prover="0"><result status="valid" time="0.02"/></proof> <proof prover="0"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="WP_parameter qs.3" expl="3. postcondition" sum="abf810b8c32150c26b4a3f3e6aacac6e"> <goal name="WP_parameter qs.3" expl="3. postcondition">
<proof prover="0"><result status="valid" time="0.02"/></proof> <proof prover="0"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="WP_parameter qs.4" expl="4. postcondition" sum="ba4a3b43dca6859d783d70d4c5b16669"> <goal name="WP_parameter qs.4" expl="4. postcondition">
<proof prover="0"><result status="valid" time="0.01"/></proof> <proof prover="0"><result status="valid" time="0.01"/></proof>
</goal> </goal>
<goal name="WP_parameter qs.5" expl="5. postcondition" sum="8532155787a9b770710dad8ca4324c1f"> <goal name="WP_parameter qs.5" expl="5. postcondition">
<proof prover="0"><result status="valid" time="0.01"/></proof> <proof prover="0"><result status="valid" time="0.01"/></proof>
</goal> </goal>
</transf> </transf>
......
...@@ -4,132 +4,132 @@ ...@@ -4,132 +4,132 @@
<why3session shape_version="4"> <why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/> <prover id="0" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<file name="../algo65.mlw" expanded="true"> <file name="../algo65.mlw" expanded="true">
<theory name="Algo65" expanded="true"> <theory name="Algo65" sum="a79e01fdec32b266dcbb4b6cfabd8ee7" expanded="true">
<goal name="WP_parameter find" expl="VC for find" sum="6868a7addea3afd6aefa8d9aa500c4dc" expanded="true"> <goal name="WP_parameter find" expl="VC for find" expanded="true">
<transf name="split_goal" expanded="true"> <transf name="split_goal" expanded="true">
<goal name="WP_parameter find.1" expl="1. precondition" sum="cf061e6b0c714b137f5b85834f75c045"> <goal name="WP_parameter find.1" expl="1. precondition">
<proof prover="0"><result status="valid" time="0.00"/></proof> <proof prover="0"><result status="valid" time="0.00"/></proof>
</goal> </goal>
<goal name="WP_parameter find.2" expl="2. variant decrease" sum="a220fe990bf8270627c276501ad45e38"> <goal name="WP_parameter find.2" expl="2. variant decrease">
<proof prover="0"><result status="valid" time="0.00"/></proof> <proof prover="0"><result status="valid" time="0.00"/></proof>
</goal> </goal>
<goal name="WP_parameter find.3" expl="3. precondition" sum="82a3df1ed87ce5e4bb60696b5f6a3825"> <goal name="WP_parameter find.3" expl="3. precondition">
<proof prover="0"><result status="valid" time="0.01"/></proof> <proof prover="0"><result status="valid" time="0.01"/></proof>
</goal> </goal>
<goal name="WP_parameter find.4" expl="4. assertion" sum="fca08a55f93b232b4ad0c12ac4cbe9ce"> <goal name="WP_parameter find.4" expl="4. assertion">
<proof prover="0"><result status="valid" time="0.01"/></proof> <proof prover="0"><result status="valid" time="0.01"/></proof>
</goal> </goal>
<goal name="WP_parameter find.5" expl="5. assertion" sum="611a958d5fef40cbafefc98b75bffa4d"> <goal name="WP_parameter find.5" expl="5. assertion">
<proof prover="0"><result status="valid" time="0.02"/></proof> <proof prover="0"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="WP_parameter find.6" expl="6. assertion" sum="ed9124e274593de98fac324c81bf7245" expanded="true"> <goal name="WP_parameter find.6" expl="6. assertion" expanded="true">
<transf name="split_goal_wp" expanded="true"> <transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter find.6.1" expl="1. assertion" sum="3146622a4f15a5bf2b8b9cb7bf70dd43" expanded="true"> <goal name="WP_parameter find.6.1" expl="1. assertion" expanded="true">
<proof prover="0" timelimit="6"><result status="valid" time="0.19"/></proof> <proof prover="0" timelimit="6"><result status="valid" time="0.19"/></proof>
</goal> </goal>
<goal name="WP_parameter find.6.2" expl="2. assertion" sum="e7631e9a86bd4136b65da1d42a82c807"> <goal name="WP_parameter find.6.2" expl="2. assertion">
<proof prover="0"><result status="valid" time="0.11"/></proof> <proof prover="0"><result status="valid" time="0.11"/></proof>
</goal> </goal>
</transf> </transf>
</goal> </goal>
<goal name="WP_parameter find.7" expl="7. variant decrease" sum="d6f051702eae57638697208968e570d5"> <goal name="WP_parameter find.7" expl="7. variant decrease">
<proof prover="0"><result status="valid" time="0.02"/></proof> <proof prover="0"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="WP_parameter find.8" expl="8. precondition" sum="a81e1cb1c269da1f11dab3955f3b9f53"> <goal name="WP_parameter find.8" expl="8. precondition">
<proof prover="0"><result status="valid" time="0.01"/></proof> <proof prover="0"><result status="valid" time="0.01"/></proof>
</goal> </goal>
<goal name="WP_parameter find.9" expl="9. assertion" sum="050916e733a8abc8f1240832dc4f8743"> <goal name="WP_parameter find.9" expl="9. assertion">
<proof prover="0"><result status="valid" time="0.01"/></proof> <proof prover="0"><result status="valid" time="0.01"/></proof>
</goal> </goal>
<goal name="WP_parameter find.10" expl="10. assertion" sum="b7afc00bc364084b94495440f0c56cd7"> <goal name="WP_parameter find.10" expl="10. assertion">
<proof prover="0"><result status="valid" time="0.02"/></proof> <proof prover="0"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="WP_parameter find.11" expl="11. assertion" sum="b3b44a7e1c5e0e4d9cbd64f68acee82b"> <goal name="WP_parameter find.11" expl="11. assertion">
<proof prover="0"><result status="valid" time="0.02"/></proof> <proof prover="0"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="WP_parameter find.12" expl="12. postcondition" sum="bb5774bdeb0f6de6e33539d629f1fc47"> <goal name="WP_parameter find.12" expl="12. postcondition">
<proof prover="0"><result status="valid" time="0.02"/></proof> <proof prover="0"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="WP_parameter find.13" expl="13. postcondition" sum="ace58a0a0af2452f20ba3cc6bee7a1ff"> <goal name="WP_parameter find.13" expl="13. postcondition">
<proof prover="0"><result status="valid" time="0.03"/></proof> <proof prover="0"><result status="valid" time="0.03"/></proof>
</goal> </goal>
<goal name="WP_parameter find.14" expl="14. postcondition" sum="d4274f39a4d9a3988b0a9350791059c7"> <goal name="WP_parameter find.14" expl="14. postcondition">
<proof prover="0"><result status="valid" time="0.03"/></proof> <proof prover="0"><result status="valid" time="0.03"/></proof>
</goal> </goal>
<goal name="WP_parameter find.15" expl="15. assertion" sum="23c7795c72accf45e816adc86111d0e6"> <goal name="WP_parameter find.15" expl="15. assertion">
<proof prover="0"><result status="valid" time="0.02"/></proof> <proof prover="0"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="WP_parameter find.16" expl="16. assertion" sum="46601176c8bce521c2b5e8b3cdef9e46"> <goal name="WP_parameter find.16" expl="16. assertion">
<proof prover="0"><result status="valid" time="0.38"/></proof> <proof prover="0"><result status="valid" time="0.38"/></proof>
</goal> </goal>
<goal name="WP_parameter find.17" expl="17. postcondition" sum="5ca076829a6dca77ec3295edbc24e302"> <goal name="WP_parameter find.17" expl="17. postcondition">
<proof prover="0"><result status="valid" time="0.02"/></proof> <proof prover="0"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="WP_parameter find.18" expl="18. postcondition" sum="7ae7e503d1f1c56492aadee5e6c148a5"> <goal name="WP_parameter find.18" expl="18. postcondition">
<proof prover="0"><result status="valid" time="0.02"/></proof> <proof prover="0"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="WP_parameter find.19" expl="19. postcondition" sum="d699c7c1c0240e53b960aea5b968334c"> <goal name="WP_parameter find.19" expl="19. postcondition">
<proof prover="0"><result status="valid" time="0.31"/></proof> <proof prover="0"><result status="valid" time="0.31"/></proof>
</goal> </goal>
<goal name="WP_parameter find.20" expl="20. assertion" sum="d51d465d2733ba90f6a8cd9b0d4188d5"> <goal name="WP_parameter find.20" expl="20. assertion">
<proof prover="0"><result status="valid" time="0.02"/></proof> <proof prover="0"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="WP_parameter find.21" expl="21. assertion" sum="3bd11013b6347e5b0ce603840d0e61a8"> <goal name="WP_parameter find.21" expl="21. assertion">
<proof prover="0"><result status="valid" time="0.05"/></proof> <proof prover="0"><result status="valid" time="0.05"/></proof>
</goal> </goal>
<goal name="WP_parameter find.22" expl="22. variant decrease" sum="60dc3bbdbbe8c13cd4a598f9ca7970e1"> <goal name="WP_parameter find.22" expl="22. variant decrease">
<proof prover="0"><result status="valid" time="0.02"/></proof> <proof prover="0"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="WP_parameter find.23" expl="23. precondition" sum="3e017f8cc37735ada2c643ca0277fd48"> <goal name="WP_parameter find.23" expl="23. precondition">
<proof prover="0"><result status="valid" time="0.02"/></proof> <proof prover="0"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="WP_parameter find.24" expl="24. assertion" sum="7273309b4f11ac8b28fe9cf94cc0d5e9"> <goal name="WP_parameter find.24" expl="24. assertion">
<proof prover="0"><result status="valid" time="0.02"/></proof> <proof prover="0"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="WP_parameter find.25" expl="25. assertion" sum="e5450e1070053b8b21b5524adc818bc5"> <goal name="WP_parameter find.25" expl="25. assertion">
<proof prover="0"><result status="valid" time="0.04"/></proof> <proof prover="0"><result status="valid" time="0.04"/></proof>
</goal> </goal>
<goal name="WP_parameter find.26" expl="26. assertion" sum="66a97e2afd938ff54fa2e76e2e63d72e" expanded="true"> <goal name="WP_parameter find.26" expl="26. assertion" expanded="true">
<transf name="split_goal_wp" expanded="true"> <transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter find.26.1" expl="1. assertion" sum="17565d374941f5cd2fdfc12fd5b46a2e" expanded="true"> <goal name="WP_parameter find.26.1" expl="1. assertion" expanded="true">
<proof prover="0" timelimit="6"><result status="valid" time="0.24"/></proof> <proof prover="0" timelimit="6"><result status="valid" time="0.24"/></proof>
</goal> </goal>
<goal name="WP_parameter find.26.2" expl="2. assertion" sum="b8157af81a7f2cea28ee5eba0529e815"> <goal name="WP_parameter find.26.2" expl="2. assertion">
<proof prover="0"><result status="valid" time="0.25"/></proof> <proof prover="0"><result status="valid" time="0.25"/></proof>
</goal> </goal>
</transf> </transf>
</goal> </goal>
<goal name="WP_parameter find.27" expl="27. postcondition" sum="4be978c8aa81e1e8d04f01cf77aec93e"> <goal name="WP_parameter find.27" expl="27. postcondition">
<proof prover="0"><result status="valid" time="0.01"/></proof> <proof prover="0"><result status="valid" time="0.01"/></proof>
</goal> </goal>
<goal name="WP_parameter find.28" expl="28. postcondition" sum="594f0e3452dfe9da6eb6b5c601022102"> <goal name="WP_parameter find.28" expl="28. postcondition">
<proof prover="0"><result status="valid" time="0.32"/></proof> <proof prover="0"><result status="valid" time="0.32"/></proof>
</goal> </goal>
<goal name="WP_parameter find.29" expl="29. postcondition" sum="81c6d96a20e09585b55e8209e4a60b6c"> <goal name="WP_parameter find.29" expl="29. postcondition">
<proof prover="0"><result status="valid" time="0.02"/></proof> <proof prover="0"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="WP_parameter find.30" expl="30. assertion" sum="a2c453f787c7d4ad06b1832977ba6964"> <goal name="WP_parameter find.30" expl="30. assertion">
<proof prover="0"><result status="valid" time="0.02"/></proof> <proof prover="0"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="WP_parameter find.31" expl="31. assertion" sum="22301f65968a1948d798fb8f406315f8"> <goal name="WP_parameter find.31" expl="31. assertion">
<proof prover="0"><result status="valid" time="0.04"/></proof> <proof prover="0"><result status="valid" time="0.04"/></proof>
</goal> </goal>
<goal name="WP_parameter find.32" expl="32. postcondition" sum="28eb85680f8896c3847e6248c8cff17f"> <goal name="WP_parameter find.32" expl="32. postcondition">
<proof prover="0"><result status="valid" time="0.02"/></proof> <proof prover="0"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="WP_parameter find.33" expl="33. postcondition" sum="e399b60fde9a3c31959fdc79f480442f"> <goal name="WP_parameter find.33" expl="33. postcondition">
<proof prover="0"><result status="valid" time="0.01"/></proof> <proof prover="0"><result status="valid" time="0.01"/></proof>
</goal> </goal>
<goal name="WP_parameter find.34" expl="34. postcondition" sum="4aeacf170cbb5f5cef8b2e7b5c219916"> <goal name="WP_parameter find.34" expl="34. postcondition">
<proof prover="0" timelimit="15"><result status="valid" time="0.03"/></proof> <proof prover="0" timelimit="15"><result status="valid" time="0.03"/></proof>
</goal> </goal>
<goal name="WP_parameter find.35" expl="35. postcondition" sum="43bc239a23be62b316053c7f739544a0"> <goal name="WP_parameter find.35" expl="35. postcondition">
<proof prover="0"><result status="valid" time="0.02"/></proof> <proof prover="0"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="WP_parameter find.36" expl="36. postcondition" sum="536d83e81ec3adde250c8e48eaac39e3"> <goal name="WP_parameter find.36" expl="36. postcondition">
<proof prover="0"><result status="valid" time="0.02"/></proof> <proof prover="0"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="WP_parameter find.37" expl="37. postcondition" sum="521f1f0810b6fc300bb37910e077f0f5"> <goal name="WP_parameter find.37" expl="37. postcondition">
<proof prover="0"><result status="valid" time="0.01"/></proof> <proof prover="0"><result status="valid" time="0.01"/></proof>
</goal> </goal>
</transf> </transf>
......
...@@ -4,43 +4,43 @@ ...@@ -4,43 +4,43 @@
<why3session shape_version="4"> <why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.95.2" timelimit="6" memlimit="1000"/> <prover id="0" name="Alt-Ergo" version="0.95.2" timelimit="6" memlimit="1000"/>
<file name="../all_distinct.mlw" expanded="true"> <file name="../all_distinct.mlw" expanded="true">
<theory name="AllDistinct" expanded="true"> <theory name="AllDistinct" sum="cdb61a5905b9fa18eb71d98750f2c5ce" expanded="true">
<goal name="WP_parameter all_distinct" expl="VC for all_distinct" sum="9cd8ab30056665aa598b63118511deb6" expanded="true"> <goal name="WP_parameter all_distinct" expl="VC for all_distinct" expanded="true">
<transf name="split_goal_wp" expanded="true"> <transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter all_distinct.1" expl="1. array creation size" sum="169dead4ca86d70a93945d7a849a4ddf" expanded="true"> <goal name="WP_parameter all_distinct.1" expl="1. array creation size" expanded="true">
<proof prover="0"><result status="valid" time="0.02"/></proof> <proof prover="0"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="WP_parameter all_distinct.2" expl="2. postcondition" sum="8d038b937a7ed02cbabc2d03293374eb" expanded="true"> <goal name="WP_parameter all_distinct.2" expl="2. postcondition" expanded="true">
<proof prover="0"><result status="valid" time="0.02"/></proof> <proof prover="0"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="WP_parameter all_distinct.3" expl="3. loop invariant init" sum="f2a72af703403a88e25a697c4ddfa52a" expanded="true"> <goal name="WP_parameter all_distinct.3" expl="3. loop invariant init" expanded="true">
<proof prover="0"><result status="valid" time="0.02"/></proof> <proof prover="0"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="WP_parameter all_distinct.4" expl="4. loop invariant init" sum="ce1590976f77ddc643d8fbdac4674fb8" expanded="true"> <goal name="WP_parameter all_distinct.4" expl="4. loop invariant init" expanded="true">
<proof prover="0"><result status="valid" time="0.02"/></proof> <proof prover="0"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="WP_parameter all_distinct.5" expl="5. index in array bounds" sum="f1a081032a623863f610a04ad56ba8cb" expanded="true"> <goal name="WP_parameter all_distinct.5" expl="5. index in array bounds" expanded="true">
<proof prover="0"><result status="valid" time="0.01"/></proof> <proof prover="0"><result status="valid" time="0.01"/></proof>
</goal> </goal>
<goal name="WP_parameter all_distinct.6" expl="6. type invariant" sum="0a3d6cdd22086870ccdd20acf950acb1" expanded="true"> <goal name="WP_parameter all_distinct.6" expl="6. type invariant" expanded="true">
<proof prover="0"><result status="valid" time="0.02"/></proof> <proof prover="0"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="WP_parameter all_distinct.7" expl="7. index in array bounds" sum="025eb7e13690ff51b15e41ac95352a8f" expanded="true"> <goal name="WP_parameter all_distinct.7" expl="7. index in array bounds" expanded="true">
<proof prover="0"><result status="valid" time="0.02"/></proof> <proof prover="0"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="WP_parameter all_distinct.8" expl="8. postcondition" sum="abed04285d21c6c786ac5473f4cbb8fe" expanded="true"> <goal name="WP_parameter all_distinct.8" expl="8. postcondition" expanded="true">
<proof prover="0"><result status="valid" time="0.01"/></proof> <proof prover="0"><result status="valid" time="0.01"/></proof>
</goal> </goal>
<goal name="WP_parameter all_distinct.9" expl="9. index in array bounds" sum="bd4aee6919c6b60b4e0886f97d37c2c3" expanded="true"> <goal name="WP_parameter all_distinct.9" expl="9. index in array bounds" expanded="true">
<proof prover="0"><result status="valid" time="0.02"/></proof> <proof prover="0"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="WP_parameter all_distinct.10" expl="10. loop invariant preservation" sum="b5160b76e1b3e97ac33d9a4547eb9ad5" expanded="true"> <goal name="WP_parameter all_distinct.10" expl="10. loop invariant preservation" expanded="true">
<proof prover="0"><result status="valid" time="0.02"/></proof> <proof prover="0"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="WP_parameter all_distinct.11" expl="11. loop invariant preservation" sum="646cfed7474750745a5a8bffbd5d0672" expanded="true"> <goal name="WP_parameter all_distinct.11" expl="11. loop invariant preservation" expanded="true">
<proof prover="0"><result status="valid" time="0.02"/></proof> <proof prover="0"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="WP_parameter all_distinct.12" expl="12. postcondition" sum="3010bad4861a5d4b8f8591549feced61" expanded="true"> <goal name="WP_parameter all_distinct.12" expl="12. postcondition" expanded="true">
<proof prover="0"><result status="valid" time="0.01"/></proof> <proof prover="0"><result status="valid" time="0.01"/></proof>
</goal> </goal>
</transf> </transf>
......
...@@ -6,65 +6,65 @@ ...@@ -6,65 +6,65 @@
<prover id="1" name="Z3" version="3.2" timelimit="5" memlimit="1000"/> <prover id="1" name="Z3" version="3.2" timelimit="5" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/> <prover id="2" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<file name="../arm.mlw" expanded="true"> <file name="../arm.mlw" expanded="true">
<theory name="M" expanded="true"> <theory name="M" sum="605769bd5022610ed3b9e18df3b7e809" expanded="true">
<goal name="WP_parameter insertion_sort" expl="VC for insertion_sort" sum="12ad10e0643d819dcdf614beb2a7db7f"> <goal name="WP_parameter insertion_sort" expl="VC for insertion_sort">
<transf name="split_goal_wp"> <transf name="split_goal_wp">
<goal name="WP_parameter insertion_sort.1" expl="1. loop invariant init" sum="62cedfa9a8840be299dc60f48e358e9d"> <goal name="WP_parameter insertion_sort.1" expl="1. loop invariant init">
<proof prover="2"><result status="valid" time="0.00"/></proof> <proof prover="2"><result status="valid" time="0.00"/></proof>
</goal> </goal>
<goal name="WP_parameter insertion_sort.2" expl="2. loop invariant init" sum="b847af6941605e2d7d0f84017c990223"> <goal name="WP_parameter insertion_sort.2" expl="2. loop invariant init">
<proof prover="2"><result status="valid" time="0.01"/></proof> <proof prover="2"><result status="valid" time="0.01"/></proof>
</goal> </goal>
<goal name="WP_parameter insertion_sort.3" expl="3. type invariant" sum="fd006cfa55f9c725523fa4d12ca78e01"> <goal name="WP_parameter insertion_sort.3" expl="3. type invariant">
<proof prover="2"><result status="valid" time="0.02"/></proof> <proof prover="2"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="WP_parameter insertion_sort.4" expl="4. index in array bounds" sum="f227e497d584beb98543bab70b47919b"> <goal name="WP_parameter insertion_sort.4" expl="4. index in array bounds">
<proof prover="2"><result status="valid" time="0.02"/></proof> <proof prover="2"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="WP_parameter insertion_sort.5" expl="5. index in array bounds" sum="ba9aa8802c1c8bbb7224a4ff9eb6cb57"> <goal name="WP_parameter insertion_sort.5" expl="5. index in array bounds">
<proof prover="2"><result status="valid" time="0.02"/></proof> <proof prover="2"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="WP_parameter insertion_sort.6" expl="6. index in array bounds" sum="d5a19d25ce8ded0495d70f00972b3a9a"> <goal name="WP_parameter insertion_sort.6" expl="6. index in array bounds">
<proof prover="2"><result status="valid" time="0.02"/></proof> <proof prover="2"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="WP_parameter insertion_sort.7" expl="7. index in array bounds" sum="9bff97babe4eca7f0409aed0b47935ec"> <goal name="WP_parameter insertion_sort.7" expl="7. index in array bounds">
<proof prover="2"><result status="valid" time="0.03"/></proof> <proof prover="2"><result status="valid" time="0.03"/></proof>
</goal> </goal>
<goal name="WP_parameter insertion_sort.8" expl="8. index in array bounds" sum="d24f30ba4db1835ea6c7cbe67360299b"> <goal name="WP_parameter insertion_sort.8" expl="8. index in array bounds">
<proof prover="2"><result status="valid" time="0.02"/></proof> <proof prover="2"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="WP_parameter insertion_sort.9" expl="9. index in array bounds" sum="891cbbbe7c1a5380ce4c569a6fab8ff3"> <goal name="WP_parameter insertion_sort.9" expl="9. index in array bounds">
<proof prover="2"><result status="valid" time="0.02"/></proof> <proof prover="2"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="WP_parameter insertion_sort.10" expl="10. loop invariant preservation" sum="2c65e9965e0b58c50e58909f7dce52b4">