Attention une mise à jour du service Gitlab va être effectuée le mardi 18 janvier (et non lundi 17 comme annoncé précédemment) entre 18h00 et 18h30. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes.

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

updated sessions

parent 7ef4d568
This diff is collapsed.
......@@ -4,60 +4,60 @@
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<file name="../algo64.mlw" expanded="true">
<theory name="Algo64" sum="1ec0a3f1e17ceff8852749848d670adf" expanded="true">
<theory name="Algo64" sum="e28f0a9f616adcce7784ce7c284474f0" expanded="true">
<goal name="WP_parameter quicksort" expl="VC for quicksort" expanded="true">
<transf name="split_goal_wp" expanded="true">
<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" steps="5"/></proof>
</goal>
<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" steps="9"/></proof>
</goal>
<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" steps="9"/></proof>
</goal>
<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" steps="172"/></proof>
</goal>
<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" steps="13"/></proof>
</goal>
<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" steps="13"/></proof>
</goal>
<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" steps="738"/></proof>
</goal>
<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" steps="555"/></proof>
</goal>
<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" steps="122"/></proof>
</goal>
<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" steps="19"/></proof>
</goal>
<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" steps="9"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter qs" expl="VC for qs">
<transf name="split_goal_wp">
<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" steps="2"/></proof>
</goal>
<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" steps="20"/></proof>
</goal>
<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" steps="6"/></proof>
</goal>
<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" steps="4"/></proof>
</goal>
<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" steps="5"/></proof>
</goal>
</transf>
</goal>
......
......@@ -4,133 +4,133 @@
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<file name="../algo65.mlw" expanded="true">
<theory name="Algo65" sum="f297bc897608fdbbb7049b99c8687b76" expanded="true">
<theory name="Algo65" sum="d8d516c8ad33e7a2736cb548287e47bf" expanded="true">
<goal name="WP_parameter find" expl="VC for find" expanded="true">
<transf name="split_goal_wp" expanded="true">
<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" steps="6"/></proof>
</goal>
<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" steps="11"/></proof>
</goal>
<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" steps="11"/></proof>
</goal>
<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" steps="21"/></proof>
</goal>
<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" steps="42"/></proof>
</goal>
<goal name="WP_parameter find.6" expl="6. assertion" expanded="true">
<transf name="split_goal_wp" 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" steps="159"/></proof>
</goal>
<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" steps="66"/></proof>
</goal>
</transf>
</goal>
<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" steps="14"/></proof>
</goal>
<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" steps="14"/></proof>
</goal>
<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" steps="16"/></proof>
</goal>
<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" steps="19"/></proof>
</goal>
<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" steps="19"/></proof>
</goal>
<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" steps="17"/></proof>
</goal>
<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" steps="19"/></proof>
</goal>
<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" steps="19"/></proof>
</goal>
<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" steps="65"/></proof>
</goal>
<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" steps="178"/></proof>
</goal>
<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" steps="96"/></proof>
</goal>
<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" steps="32"/></proof>
</goal>
<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" steps="118"/></proof>
</goal>
<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" steps="36"/></proof>
</goal>
<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" steps="48"/></proof>
</goal>
<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" steps="13"/></proof>
</goal>
<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" steps="13"/></proof>
</goal>
<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" steps="26"/></proof>
</goal>
<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" steps="69"/></proof>
</goal>
<goal name="WP_parameter find.26" expl="26. assertion" expanded="true">
<transf name="split_goal_wp" 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" steps="182"/></proof>
</goal>
<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" steps="87"/></proof>
</goal>
</transf>
</goal>
<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" steps="87"/></proof>
</goal>
<goal name="WP_parameter find.28" expl="28. postcondition">
<proof prover="0"><result status="valid" time="0.19"/></proof>
<proof prover="0"><result status="valid" time="0.19" steps="94"/></proof>
</goal>
<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" steps="32"/></proof>
</goal>
<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" steps="13"/></proof>
</goal>
<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" steps="36"/></proof>
</goal>
<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" steps="13"/></proof>
</goal>
<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" steps="34"/></proof>
</goal>
<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" steps="34"/></proof>
</goal>
<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" steps="20"/></proof>
</goal>
<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" steps="8"/></proof>
</goal>
<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" steps="8"/></proof>
</goal>
</transf>
</goal>
......
......@@ -4,44 +4,44 @@
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.95.2" timelimit="6" memlimit="1000"/>
<file name="../all_distinct.mlw" expanded="true">
<theory name="AllDistinct" sum="48f48153848ce8df2f233a23475559a8" expanded="true">
<theory name="AllDistinct" sum="7d203083e179a8844f043988072c4161" expanded="true">
<goal name="WP_parameter all_distinct" expl="VC for all_distinct" expanded="true">
<transf name="split_goal_wp" 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" steps="2"/></proof>
</goal>
<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.01" steps="8"/></proof>
</goal>
<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" steps="8"/></proof>
</goal>
<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" steps="9"/></proof>
</goal>
<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.02" steps="7"/></proof>
</goal>
<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" steps="7"/></proof>
</goal>
<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.01" steps="9"/></proof>
</goal>
<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" steps="17"/></proof>
</goal>
<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" steps="10"/></proof>
</goal>
<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" steps="36"/></proof>
</goal>
<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" steps="33"/></proof>
</goal>
<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.02" steps="16"/></proof>
</goal>
</transf>
</goal>
......
......@@ -6,66 +6,66 @@
<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"/>
<file name="../arm.mlw" expanded="true">
<theory name="M" sum="364881118cece723649e3e44aebab016" expanded="true">
<theory name="M" sum="d97450a6c255beed8bf40f7d503e79cd" expanded="true">
<goal name="WP_parameter insertion_sort" expl="VC for insertion_sort">
<transf name="split_goal_wp">
<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" steps="6"/></proof>
</goal>
<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" steps="15"/></proof>
</goal>
<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" steps="15"/></proof>
</goal>
<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" steps="17"/></proof>
</goal>
<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" steps="19"/></proof>
</goal>
<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" steps="21"/></proof>
</goal>
<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" steps="21"/></proof>
</goal>
<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" steps="21"/></proof>
</goal>
<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" steps="22"/></proof>
</goal>
<goal name="WP_parameter insertion_sort.10" expl="10. loop invariant preservation">
<proof prover="2"><result status="valid" time="1.14"/></proof>
<proof prover="2"><result status="valid" time="1.14" steps="80"/></proof>
</goal>
<goal name="WP_parameter insertion_sort.11" expl="11. loop variant decrease">
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.02" steps="24"/></proof>
</goal>
<goal name="WP_parameter insertion_sort.12" expl="12. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.02" steps="27"/></proof>
</goal>
<goal name="WP_parameter insertion_sort.13" expl="13. loop variant decrease">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.01" steps="21"/></proof>
</goal>
<goal name="WP_parameter insertion_sort.14" expl="14. type invariant">
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.00" steps="10"/></proof>
</goal>
<goal name="WP_parameter insertion_sort.15" expl="15. postcondition">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
</transf>
</goal>
</theory>
<theory name="ARM" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
<theory name="InsertionSortExample" sum="3a186d2e250b6bfbe467bdc9027aa95a" expanded="true">
<theory name="InsertionSortExample" sum="035a2f3e51417e24f6e447e2c9f5b21b" expanded="true">
<goal name="WP_parameter path_init_l2" expl="VC for path_init_l2">
<proof prover="0" memlimit="1000"><result status="valid" time="0.02"/></proof>
<proof prover="0" memlimit="1000"><result status="valid" time="0.02" steps="19"/></proof>
<proof prover="1"><result status="valid" time="0.14"/></proof>
</goal>
<goal name="WP_parameter path_l2_exit" expl="VC for path_l2_exit">
<proof prover="0" timelimit="10"><result status="valid" time="0.01"/></proof>
<proof prover="0" timelimit="10"><result status="valid" time="0.01" steps="9"/></proof>
</goal>
</theory>
</file>
......
......@@ -5,9 +5,9 @@
<prover id="0" name="CVC3" version="2.4.1" timelimit="10" memlimit="0"/>
<prover id="1" name="Alt-Ergo" version="0.95.1" timelimit="10" memlimit="0"/>
<file name="../assigning_meanings_to_programs.mlw">
<theory name="Sum" sum="af7d1a332a96db2b26a8223d4d0fe226" expanded="true">
<theory name="Sum" sum="de5b5ac815e310c038a383137b72227a" 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="1"><result status="valid" time="0.02" steps="21"/></proof>
</goal>
</theory>
<theory name="Division" sum="d23c114c7ff9509b0b89b152002ffc98" expanded="true">
......
......@@ -14,7 +14,7 @@
</theory>
<theory name="ResizableArraySpec" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="BagImpl" sum="e5c247f3bba7104c0837200325f56fbc" expanded="true">
<theory name="BagImpl" sum="c074bbe9d2c1ec9b335517b85d5e7b49" expanded="true">
<goal name="WP_parameter create" expl="VC for create">
<proof prover="4"><result status="valid" time="0.01" steps="14"/></proof>
</goal>
......@@ -22,7 +22,7 @@
<proof prover="4"><result status="valid" time="0.01" steps="15"/></proof>
</goal>
<goal name="WP_parameter add" expl="VC for add">
<proof prover="2"><result status="valid" time="2.76"/></proof>
<proof prover="2"><result status="valid" time="0.38"/></proof>
</goal>
<goal name="WP_parameter get" expl="VC for get">
<proof prover="4"><result status="valid" time="0.00" steps="11"/></proof>
......@@ -69,7 +69,7 @@
<proof prover="4"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="WP_parameter remove.14" expl="14. assertion">
<proof prover="1"><result status="valid" time="0.64"/></proof>
<proof prover="1"><result status="valid" time="0.32"/></proof>
</goal>
<goal name="WP_parameter remove.15" expl="15. assertion">
<proof prover="2"><result status="valid" time="0.02"/></proof>
......@@ -93,7 +93,7 @@
</transf>
</goal>
</theory>
<theory name="Harness" sum="528e93ede1770450354a9703428c111b" expanded="true">
<theory name="Harness" sum="f635e6da8b24a4255f98ac62c1ecc04e" expanded="true">
<goal name="WP_parameter test1" expl="VC for test1">
<transf name="split_goal_wp">
<goal name="WP_parameter test1.1" expl="1. assertion">
......
......@@ -8,79 +8,79 @@
<file name="../balance.mlw" expanded="true">
<theory name="Roberval" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="Puzzle8" sum="66fcb4862ec53a83dc3d6d11a1f2b52c">
<theory name="Puzzle8" sum="7bd261b5c4cef46f4acc04f8507db7d7">
<goal name="WP_parameter solve3" expl="VC for solve3">
<proof prover="0"><result status="valid" time="0.02"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="0"><result status="valid" time="0.02" steps="47"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="41"/></proof>
</goal>
<goal name="WP_parameter solve8" expl="VC for solve8">
<transf name="split_goal_wp">
<goal name="WP_parameter solve8.1" expl="1. index in array bounds">
<proof prover="0"><result status="valid" time="0.02"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="0"><result status="valid" time="0.02" steps="7"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="7"/></proof>
</goal>
<goal name="WP_parameter solve8.2" expl="2. index in array bounds">
<proof prover="0"><result status="valid" time="0.01"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="5"/></proof>
</goal>
<goal name="WP_parameter solve8.3" expl="3. index in array bounds">
<proof prover="0"><result status="valid" time="0.01"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="0"><result status="valid" time="0.01" steps="7"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="7"/></proof>
</goal>
<goal name="WP_parameter solve8.4" expl="4. index in array bounds">
<proof prover="0"><result status="valid" time="0.01"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="0"><result status="valid" time="0.01" steps="9"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="9"/></proof>
</goal>
<goal name="WP_parameter solve8.5" expl="5. index in array bounds">
<proof prover="0"><result status="valid" time="0.03"/></proof>
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="0"><result status="valid" time="0.03" steps="11"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="11"/></proof>
</goal>
<goal name="WP_parameter solve8.6" expl="6. index in array bounds">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="0"><result status="valid" time="0.00" steps="13"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="13"/></proof>
</goal>
<goal name="WP_parameter solve8.7" expl="7. precondition">
<proof prover="1" timelimit="6"><result status="valid" time="0.03"/></proof>
<proof prover="1" timelimit="6"><result status="valid" time="0.03" steps="15"/></proof>
</goal>
<goal name="WP_parameter solve8.8" expl="8. precondition">
<proof prover="0"><result status="valid" time="0.01"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="0"><result status="valid" time="0.01" steps="18"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="18"/></proof>
</goal>
<goal name="WP_parameter solve8.9" expl="9. precondition">
<proof prover="0"><result status="valid" time="0.02"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="0"><result status="valid" time="0.02" steps="72"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="78"/></proof>
</goal>
<goal name="WP_parameter solve8.10" expl="10. precondition">
<proof prover="0"><result status="valid" time="0.04"/></proof>
<proof prover="1"><result status="valid" time="0.10"/></proof>
<proof prover="0"><result status="valid" time="0.04" steps="18"/></proof>
<proof prover="1"><result status="valid" time="0.10" steps="18"/></proof>
</goal>
<goal name="WP_parameter solve8.11" expl="11. precondition">
<proof prover="0"><result status="valid" time="0.03"/></proof>
<proof prover="1"><result status="valid" time="0.05"/></proof>
<proof prover="0"><result status="valid" time="0.03" steps="91"/></proof>
<proof prover="1"><result status="valid" time="0.05" steps="97"/></proof>
</goal>
<goal name="WP_parameter solve8.12" expl="12. index in array bounds">
<proof prover="0"><result status="valid" time="0.01"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="0"><result status="valid" time="0.01" steps="21"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="21"/></proof>
</goal>
<goal name="WP_parameter solve8.13" expl="13. index in array bounds">
<proof prover="0"><result status="valid" time="0.02"/></proof>
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="0"><result status="valid" time="0.02" steps="20"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="20"/></proof>
</goal>
<goal name="WP_parameter solve8.14" expl="14. precondition">
<proof prover="1" timelimit="6"><result status="valid" time="0.02"/></proof>
<proof prover="1" timelimit="6"><result status="valid" time="0.02" steps="22"/></proof>
</goal>
<goal name="WP_parameter solve8.15" expl="15. postcondition">
<proof prover="0"><result status="valid" time="0.13"/></proof>
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="0"><result status="valid" time="0.13" steps="82"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="82"/></proof>
</goal>
<goal name="WP_parameter solve8.16" expl="16. postcondition">
<proof prover="0"><result status="valid" time="0.20"/></proof>
<proof prover="1"><result status="valid" time="0.27"/></proof>
<proof prover="0"><result status="valid" time="0.20" steps="143"/></proof>
<proof prover="1"><result status="valid" time="0.27" steps="143"/></proof>
</goal>
</transf>
</goal>
</theory>
<theory name="Puzzle12" sum="399ee69ce388e015dd48291b6dab63aa" expanded="true">
<theory name="Puzzle12" sum="e4074fbfee82e2d49008a68498e7c5d6" expanded="true">
<goal name="WP_parameter solve12" expl="VC for solve12" expanded="true">
<proof prover="2"><result status="valid" time="0.29"/></proof>
</goal>
......