Commit 27adc1e5 authored by MARCHE Claude's avatar MARCHE Claude

updated sessions on orcus

parent 8e5318b7
......@@ -20,7 +20,7 @@
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
</theory>
<theory name="BinarySearchInt32" sum="4b2f95ee2a0f21c4f20c47716b429187" expanded="true">
<theory name="BinarySearchInt32" sum="902b39131261e18de4c4c65692531fe9" expanded="true">
<goal name="WP_parameter binary_search" expl="VC for binary_search" expanded="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.22"/></proof>
......@@ -56,7 +56,7 @@
<proof prover="1"><result status="valid" time="0.32"/></proof>
</goal>
<goal name="WP_parameter binary_search.11" expl="11. assertion">
<proof prover="1"><result status="valid" time="0.66"/></proof>
<proof prover="1"><result status="valid" time="0.92"/></proof>
</goal>
<goal name="WP_parameter binary_search.12" expl="12. index in array bounds">
<proof prover="1"><result status="valid" time="0.01"/></proof>
......@@ -71,7 +71,7 @@
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter binary_search.16" expl="16. loop invariant preservation">
<proof prover="1"><result status="valid" time="3.81"/></proof>
<proof prover="1"><result status="valid" time="5.14"/></proof>
</goal>
<goal name="WP_parameter binary_search.17" expl="17. loop variant decrease">
<proof prover="1"><result status="valid" time="0.02"/></proof>
......@@ -89,13 +89,13 @@
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter binary_search.22" expl="22. loop invariant preservation">
<proof prover="1"><result status="valid" time="3.54"/></proof>
<proof prover="1"><result status="valid" time="4.86"/></proof>
</goal>
<goal name="WP_parameter binary_search.23" expl="23. loop variant decrease">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter binary_search.24" expl="24. postcondition">
<proof prover="1"><result status="valid" time="0.46"/></proof>
<proof prover="1"><result status="valid" time="0.74"/></proof>
</goal>
<goal name="WP_parameter binary_search.25" expl="25. exceptional postcondition">
<proof prover="1"><result status="valid" time="0.01"/></proof>
......
......@@ -9,21 +9,21 @@
<file name="../euler001.mlw" expanded="true">
<theory name="DivModHints" sum="f7fdece9a19249c4382a43566f166530">
<goal name="mod_div_unique">
<proof prover="0" memlimit="0" edited="euler001_DivModHints_mod_div_unique_1.v"><result status="valid" time="1.06"/></proof>
<proof prover="0" memlimit="0" edited="euler001_DivModHints_mod_div_unique_1.v"><result status="valid" time="2.03"/></proof>
</goal>
<goal name="mod_succ_1">
<proof prover="0" memlimit="0" edited="euler001_DivModHints_mod_succ_1_1.v"><result status="valid" time="1.15"/></proof>
<proof prover="0" memlimit="0" edited="euler001_DivModHints_mod_succ_1_1.v"><result status="valid" time="2.09"/></proof>
</goal>
<goal name="mod_succ_2">
<proof prover="0" memlimit="0" edited="euler001_DivModHints_mod_succ_2_1.v"><result status="valid" time="1.14"/></proof>
<proof prover="0" memlimit="0" edited="euler001_DivModHints_mod_succ_2_1.v"><result status="valid" time="2.16"/></proof>
</goal>
<goal name="div_succ_1">
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="div_succ_2">
<proof prover="1"><result status="valid" time="0.10"/></proof>
<proof prover="2"><result status="valid" time="0.91"/></proof>
<proof prover="3" timelimit="30" memlimit="1000"><result status="valid" time="2.20"/></proof>
<proof prover="2"><result status="valid" time="1.23"/></proof>
<proof prover="3" timelimit="30" memlimit="1000"><result status="valid" time="3.22"/></proof>
</goal>
<goal name="mod2_mul2">
<proof prover="1" timelimit="5"><result status="valid" time="0.01"/></proof>
......@@ -61,7 +61,7 @@
</theory>
<theory name="TriangularNumbers" sum="91847fa59365859f1ae00cac3b34c298">
<goal name="tr_mod_2">
<proof prover="0" edited="euler001_TriangularNumbers_tr_mod_2_1.v"><result status="valid" time="1.07"/></proof>
<proof prover="0" edited="euler001_TriangularNumbers_tr_mod_2_1.v"><result status="valid" time="1.90"/></proof>
</goal>
<goal name="tr_repr">
<proof prover="2" timelimit="5"><result status="valid" time="0.02"/></proof>
......@@ -76,22 +76,22 @@
<theory name="SumMultiple" sum="90bf0acc57cc35c41e0a28734c52e85d">
<goal name="mod_15">
<proof prover="1"><result status="valid" time="0.13"/></proof>
<proof prover="3" memlimit="1000"><result status="valid" time="0.81"/></proof>
<proof prover="3" memlimit="1000"><result status="valid" time="1.20"/></proof>
</goal>
<goal name="Closed_formula_0">
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.14"/></proof>
<proof prover="3" memlimit="1000"><result status="valid" time="0.22"/></proof>
<proof prover="3" memlimit="1000"><result status="valid" time="0.47"/></proof>
</goal>
<goal name="Closed_formula_n">
<proof prover="1" timelimit="10"><result status="valid" time="1.62"/></proof>
<proof prover="3" timelimit="10" memlimit="1000"><result status="valid" time="4.68"/></proof>
<proof prover="1" timelimit="10"><result status="valid" time="2.58"/></proof>
<proof prover="3" timelimit="10" memlimit="1000"><result status="valid" time="7.40"/></proof>
</goal>
<goal name="Closed_formula_n_3">
<proof prover="1" timelimit="10"><result status="valid" time="2.94"/></proof>
<proof prover="1" timelimit="10"><result status="valid" time="3.93"/></proof>
</goal>
<goal name="Closed_formula_n_5">
<proof prover="1" timelimit="5"><result status="valid" time="0.37"/></proof>
<proof prover="1" timelimit="5"><result status="valid" time="0.52"/></proof>
</goal>
<goal name="Closed_formula_n_15">
<proof prover="1" timelimit="5"><result status="valid" time="0.30"/></proof>
......@@ -115,10 +115,10 @@
<proof prover="3" memlimit="1000"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="Closed_Formula">
<proof prover="0" timelimit="30" edited="euler001_SumMultiple_Closed_Formula_1.v"><result status="valid" time="1.14"/></proof>
<proof prover="0" timelimit="30" edited="euler001_SumMultiple_Closed_Formula_1.v"><result status="valid" time="1.97"/></proof>
</goal>
</theory>
<theory name="Euler001" sum="2e1715ee1490669d54ae7931f68ca9c4">
<theory name="Euler001" sum="270c2a79b43cdbc70abf108abe165df9">
<goal name="WP_parameter solve" expl="VC for solve">
<proof prover="1"><result status="valid" time="0.06"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
......
......@@ -2,10 +2,10 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Coq" version="8.4pl4" timelimit="5" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.2" timelimit="10" memlimit="1000"/>
<prover id="2" name="CVC3" version="2.4.1" timelimit="10" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="0.95.1" timelimit="10" memlimit="1000"/>
<prover id="0" name="CVC4" version="1.2" timelimit="10" memlimit="1000"/>
<prover id="1" name="Coq" version="8.4pl4" timelimit="5" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="0.95.1" timelimit="10" memlimit="1000"/>
<prover id="3" name="CVC3" version="2.4.1" timelimit="10" memlimit="1000"/>
<prover id="4" name="Z3" version="2.19" timelimit="10" memlimit="0"/>
<prover id="5" name="Z3" version="4.3.1" timelimit="6" memlimit="1000"/>
<prover id="6" name="Eprover" version="1.8-001" timelimit="6" memlimit="1000"/>
......@@ -16,16 +16,16 @@
<goal name="WP_parameter euclid" expl="VC for euclid">
<transf name="split_goal_wp">
<goal name="WP_parameter euclid.1" expl="1. postcondition">
<proof prover="2" memlimit="0"><result status="valid" time="0.02"/></proof>
<proof prover="3" timelimit="2" memlimit="0"><result status="valid" time="0.01"/></proof>
<proof prover="2" timelimit="2" memlimit="0"><result status="valid" time="0.01"/></proof>
<proof prover="3" memlimit="0"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter euclid.2" expl="2. division by zero">
<proof prover="7" timelimit="5"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter euclid.3" expl="3. variant decrease">
<proof prover="2" timelimit="5"><result status="valid" time="0.02"/></proof>
<proof prover="3" timelimit="5"><result status="valid" time="0.03"/></proof>
<proof prover="2" timelimit="5"><result status="valid" time="0.03"/></proof>
<proof prover="3" timelimit="5"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter euclid.4" expl="4. precondition">
<proof prover="2" memlimit="0"><result status="valid" time="0.02"/></proof>
......@@ -33,9 +33,9 @@
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter euclid.5" expl="5. postcondition">
<proof prover="0" timelimit="10" edited="gcd_WP_EuclideanAlgorithm_WP_parameter_gcd_1.v"><result status="valid" time="1.12"/></proof>
<proof prover="1"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.04"/></proof>
<proof prover="0"><result status="valid" time="0.03"/></proof>
<proof prover="1" timelimit="10" edited="gcd_WP_EuclideanAlgorithm_WP_parameter_gcd_1.v"><result status="valid" time="1.80"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
</transf>
</goal>
......@@ -44,23 +44,23 @@
<goal name="WP_parameter euclid" expl="VC for euclid">
<transf name="split_goal_wp">
<goal name="WP_parameter euclid.1" expl="1. loop invariant init">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter euclid.2" expl="2. division by zero">
<proof prover="7" timelimit="5"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter euclid.3" expl="3. loop invariant preservation">
<proof prover="3"><result status="valid" time="0.06"/></proof>
<proof prover="2"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="WP_parameter euclid.4" expl="4. loop invariant preservation">
<proof prover="3"><result status="valid" time="0.04"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter euclid.5" expl="5. loop variant decrease">
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="0"><result status="valid" time="0.02"/></proof>
<proof prover="5" timelimit="30"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter euclid.6" expl="6. postcondition">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
......@@ -79,7 +79,7 @@
<proof prover="7" memlimit="1000"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="gcd_even_odd">
<proof prover="0" edited="gcd_BinaryGcd_gcd_even_odd_2.v"><result status="valid" time="0.94"/></proof>
<proof prover="1" edited="gcd_BinaryGcd_gcd_even_odd_2.v"><result status="valid" time="1.77"/></proof>
</goal>
<goal name="gcd_even_odd2">
<proof prover="7" memlimit="1000"><result status="valid" time="0.17"/></proof>
......@@ -125,7 +125,7 @@
<proof prover="7" memlimit="1000"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter binary_gcd.9" expl="9. postcondition">
<proof prover="2" timelimit="6"><result status="valid" time="0.02"/></proof>
<proof prover="3" timelimit="6"><result status="valid" time="0.02"/></proof>
<proof prover="6"><result status="valid" time="0.14"/></proof>
</goal>
<goal name="WP_parameter binary_gcd.10" expl="10. division by zero">
......@@ -162,21 +162,21 @@
</goal>
<goal name="WP_parameter binary_gcd.19" expl="19. variant decrease">
<proof prover="7" memlimit="1000"><result status="valid" time="0.08"/></proof>
<proof prover="8"><result status="valid" time="0.04"/></proof>
<proof prover="8"><result status="valid" time="0.15"/></proof>
</goal>
<goal name="WP_parameter binary_gcd.20" expl="20. precondition">
<proof prover="6"><result status="valid" time="3.92"/></proof>
<proof prover="6"><result status="valid" time="6.75"/></proof>
<proof prover="7" memlimit="1000"><result status="valid" time="0.03"/></proof>
<proof prover="8"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter binary_gcd.21" expl="21. postcondition">
<proof prover="6"><result status="valid" time="0.45"/></proof>
<proof prover="6"><result status="valid" time="0.69"/></proof>
<proof prover="8"><result status="valid" time="0.03"/></proof>
</goal>
</transf>
</goal>
</theory>
<theory name="EuclideanAlgorithm31" sum="6fc84d7a7a467a63727310894524cee2" expanded="true">
<theory name="EuclideanAlgorithm31" sum="02149e0bcaa0718abbda1cf1641de5d2" expanded="true">
<goal name="WP_parameter euclid" expl="VC for euclid">
<transf name="split_goal_wp">
<goal name="WP_parameter euclid.1" expl="1. integer overflow">
......@@ -192,13 +192,13 @@
<proof prover="7" timelimit="5"><result status="valid" time="0.10"/></proof>
</goal>
<goal name="WP_parameter euclid.5" expl="5. variant decrease">
<proof prover="7" timelimit="5"><result status="valid" time="0.52"/></proof>
<proof prover="7" timelimit="5"><result status="valid" time="1.13"/></proof>
</goal>
<goal name="WP_parameter euclid.6" expl="6. precondition">
<proof prover="7" timelimit="5"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter euclid.7" expl="7. postcondition">
<proof prover="7" timelimit="5"><result status="valid" time="0.54"/></proof>
<proof prover="7" timelimit="5"><result status="valid" time="1.14"/></proof>
</goal>
</transf>
</goal>
......
......@@ -11,16 +11,16 @@
</theory>
<theory name="InPlaceRev" sum="fd2061728df4ef10ceafdbfcc7847ac8" expanded="true">
<goal name="list_seg_frame" expanded="true">
<proof prover="0" edited="linked_list_rev_WP_InPlaceRev_list_seg_frame_1.v" obsolete="true"><result status="valid" time="1.13"/></proof>
<proof prover="0" edited="linked_list_rev_WP_InPlaceRev_list_seg_frame_1.v"><result status="valid" time="2.09"/></proof>
</goal>
<goal name="list_seg_functional" expanded="true">
<proof prover="0" edited="linked_list_rev_WP_InPlaceRev_list_seg_functional_1.v" obsolete="true"><result status="valid" time="1.08"/></proof>
<proof prover="0" edited="linked_list_rev_WP_InPlaceRev_list_seg_functional_1.v"><result status="valid" time="2.14"/></proof>
</goal>
<goal name="list_seg_sublistl" expanded="true">
<proof prover="0" edited="linked_list_rev_WP_InPlaceRev_list_seg_sublistl_1.v" obsolete="true"><result status="valid" time="1.05"/></proof>
<proof prover="0" edited="linked_list_rev_WP_InPlaceRev_list_seg_sublistl_1.v"><result status="valid" time="2.10"/></proof>
</goal>
<goal name="list_seg_no_repet" expanded="true">
<proof prover="0" edited="linked_list_rev_WP_InPlaceRev_list_seg_no_repet_1.v" obsolete="true"><result status="valid" time="1.07"/></proof>
<proof prover="0" edited="linked_list_rev_WP_InPlaceRev_list_seg_no_repet_1.v"><result status="valid" time="2.04"/></proof>
</goal>
<goal name="WP_parameter in_place_reverse" expl="VC for in_place_reverse">
<transf name="split_goal_wp">
......
......@@ -2,20 +2,21 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.95.1" timelimit="14" memlimit="1000"/>
<prover id="0" name="Eprover" version="1.6" timelimit="30" memlimit="1000"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="30" memlimit="1000"/>
<prover id="2" name="Eprover" version="1.6" timelimit="30" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.4" timelimit="3" memlimit="1000"/>
<prover id="4" name="Z3" version="2.19" timelimit="10" memlimit="0"/>
<prover id="5" name="CVC4" version="1.0" timelimit="30" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="0.95.1" timelimit="14" memlimit="1000"/>
<prover id="3" name="Z3" version="2.19" timelimit="10" memlimit="0"/>
<prover id="4" name="CVC4" version="1.4" timelimit="3" memlimit="1000"/>
<prover id="5" name="Z3" version="4.3.1" timelimit="30" memlimit="1000"/>
<prover id="6" name="Spass" version="3.7" timelimit="30" memlimit="1000"/>
<prover id="7" name="Z3" version="4.3.1" timelimit="30" memlimit="1000"/>
<prover id="8" name="Yices" version="1.0.38" timelimit="7" memlimit="0"/>
<prover id="7" name="Yices" version="1.0.38" timelimit="7" memlimit="0"/>
<prover id="8" name="Z3" version="3.2" timelimit="30" memlimit="1000"/>
<prover id="9" name="Metis" version="2.3" timelimit="5" memlimit="4000"/>
<prover id="10" name="Z3" version="3.2" timelimit="30" memlimit="1000"/>
<prover id="10" name="Eprover" version="1.8-001" timelimit="5" memlimit="1000"/>
<prover id="11" name="veriT" version="201310" timelimit="5" memlimit="4000"/>
<prover id="12" name="CVC4" version="1.3" timelimit="3" memlimit="1000"/>
<prover id="13" name="Vampire" version="0.6" timelimit="20" memlimit="1000"/>
<prover id="12" name="Alt-Ergo" version="0.95.2" timelimit="30" memlimit="1000"/>
<prover id="13" name="CVC4" version="1.3" timelimit="3" memlimit="1000"/>
<prover id="14" name="Vampire" version="0.6" timelimit="20" memlimit="1000"/>
<file name="../einstein.why" expanded="true">
<theory name="Bijection" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
......@@ -23,54 +24,56 @@
</theory>
<theory name="EinsteinClues" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
<theory name="Goals" sum="236691f22067dd774f4c7b98c626f214">
<theory name="Goals" sum="236691f22067dd774f4c7b98c626f214" expanded="true">
<goal name="G1">
<proof prover="0" timelimit="17"><result status="valid" time="15.57"/></proof>
<proof prover="1"><result status="unknown" time="0.06"/></proof>
<proof prover="2"><result status="timeout" time="29.79"/></proof>
<proof prover="3"><result status="unknown" time="0.04"/></proof>
<proof prover="4"><result status="valid" time="0.96"/></proof>
<proof prover="5"><result status="unknown" time="0.30"/></proof>
<proof prover="6"><result status="valid" time="4.66"/></proof>
<proof prover="7"><result status="valid" time="3.84"/></proof>
<proof prover="8"><result status="unknown" time="0.00"/></proof>
<proof prover="2" timelimit="17"><result status="valid" time="18.69"/></proof>
<proof prover="3"><result status="valid" time="1.20"/></proof>
<proof prover="4"><result status="unknown" time="0.04"/></proof>
<proof prover="5"><result status="valid" time="4.51"/></proof>
<proof prover="6"><result status="valid" time="5.72"/></proof>
<proof prover="7"><result status="unknown" time="0.00"/></proof>
<proof prover="8"><result status="valid" time="0.26"/></proof>
<proof prover="9"><result status="unknown" time="9.99"/></proof>
<proof prover="10"><result status="valid" time="0.26"/></proof>
<proof prover="10"><result status="valid" time="4.15"/></proof>
<proof prover="11"><result status="valid" time="0.02"/></proof>
<proof prover="12"><result status="unknown" time="0.06"/></proof>
<proof prover="13"><result status="valid" time="1.75"/></proof>
<proof prover="12"><result status="valid" time="16.91"/></proof>
<proof prover="13"><result status="unknown" time="0.06"/></proof>
<proof prover="14"><result status="valid" time="2.21"/></proof>
</goal>
<goal name="Wrong">
<proof prover="0" timelimit="5"><result status="timeout" time="5.00"/></proof>
<proof prover="0" timelimit="5"><result status="timeout" time="4.96"/></proof>
<proof prover="1" timelimit="5"><result status="unknown" time="0.06"/></proof>
<proof prover="2" timelimit="5"><result status="timeout" time="4.96"/></proof>
<proof prover="3"><result status="unknown" time="0.04"/></proof>
<proof prover="4" timelimit="5"><result status="timeout" time="4.95"/></proof>
<proof prover="5" timelimit="5"><result status="unknown" time="0.30"/></proof>
<proof prover="2" timelimit="5"><result status="timeout" time="5.00"/></proof>
<proof prover="3" timelimit="5"><result status="timeout" time="4.95"/></proof>
<proof prover="4"><result status="unknown" time="0.04"/></proof>
<proof prover="5" timelimit="5"><result status="timeout" time="4.97"/></proof>
<proof prover="6" timelimit="5"><result status="timeout" time="4.99"/></proof>
<proof prover="7" timelimit="5"><result status="timeout" time="4.97"/></proof>
<proof prover="8" timelimit="5"><result status="unknown" time="0.00"/></proof>
<proof prover="7" timelimit="5"><result status="unknown" time="0.00"/></proof>
<proof prover="8" timelimit="5"><result status="timeout" time="4.96"/></proof>
<proof prover="9"><result status="unknown" time="10.02"/></proof>
<proof prover="10" timelimit="5"><result status="timeout" time="4.96"/></proof>
<proof prover="10" timelimit="30"><result status="timeout" time="29.96"/></proof>
<proof prover="11"><result status="timeout" time="4.97"/></proof>
<proof prover="12"><result status="unknown" time="0.06"/></proof>
<proof prover="13" timelimit="5"><result status="unknown" time="10.08"/></proof>
<proof prover="12"><result status="unknown" time="12.60"/></proof>
<proof prover="13"><result status="unknown" time="0.06"/></proof>
<proof prover="14" timelimit="5"><result status="unknown" time="10.08"/></proof>
</goal>
<goal name="G2">
<proof prover="0"><result status="valid" time="9.46"/></proof>
<proof prover="0"><result status="valid" time="26.77"/></proof>
<proof prover="1"><result status="unknown" time="0.06"/></proof>
<proof prover="2"><result status="valid" time="20.12"/></proof>
<proof prover="3"><result status="unknown" time="0.04"/></proof>
<proof prover="4"><result status="valid" time="2.26"/></proof>
<proof prover="5"><result status="unknown" time="0.31"/></proof>
<proof prover="6"><result status="valid" time="4.52"/></proof>
<proof prover="7"><result status="valid" time="3.79"/></proof>
<proof prover="8"><result status="unknown" time="0.00"/></proof>
<proof prover="9"><result status="valid" time="3.88"/></proof>
<proof prover="10"><result status="valid" time="0.66"/></proof>
<proof prover="2"><result status="valid" time="11.56"/></proof>
<proof prover="3"><result status="valid" time="2.70"/></proof>
<proof prover="4"><result status="unknown" time="0.04"/></proof>
<proof prover="5"><result status="valid" time="4.45"/></proof>
<proof prover="6"><result status="valid" time="5.40"/></proof>
<proof prover="7"><result status="unknown" time="0.00"/></proof>
<proof prover="8"><result status="valid" time="0.83"/></proof>
<proof prover="9"><result status="valid" time="5.86"/></proof>
<proof prover="10"><result status="valid" time="1.12"/></proof>
<proof prover="11"><result status="valid" time="0.02"/></proof>
<proof prover="12"><result status="unknown" time="0.06"/></proof>
<proof prover="13"><result status="valid" time="1.43"/></proof>
<proof prover="12"><result status="valid" time="10.49"/></proof>
<proof prover="13"><result status="unknown" time="0.06"/></proof>
<proof prover="14"><result status="valid" time="1.91"/></proof>
</goal>
</theory>
</file>
......
This diff is collapsed.
This diff is collapsed.
......@@ -74,13 +74,13 @@
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter merge.20" expl="20. loop invariant preservation">
<proof prover="5"><result status="valid" time="0.39"/></proof>
<proof prover="5"><result status="valid" time="0.75"/></proof>
</goal>
<goal name="WP_parameter merge.21" expl="21. loop invariant preservation">
<proof prover="5"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="WP_parameter merge.22" expl="22. loop invariant preservation">
<proof prover="1"><result status="valid" time="2.99"/></proof>
<proof prover="1"><result status="valid" time="4.67"/></proof>
</goal>
<goal name="WP_parameter merge.23" expl="23. loop invariant preservation">
<proof prover="1" timelimit="5"><result status="valid" time="0.29"/></proof>
......@@ -92,16 +92,16 @@
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter merge.26" expl="26. loop invariant preservation">
<proof prover="5"><result status="valid" time="0.40"/></proof>
<proof prover="5"><result status="valid" time="0.75"/></proof>
</goal>
<goal name="WP_parameter merge.27" expl="27. loop invariant preservation">
<proof prover="1"><result status="valid" time="3.15"/></proof>
<proof prover="1"><result status="valid" time="4.27"/></proof>
</goal>
<goal name="WP_parameter merge.28" expl="28. loop invariant preservation">
<proof prover="5"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="WP_parameter merge.29" expl="29. loop invariant preservation">
<proof prover="0" edited="mergesort_queue_MergesortQueue_WP_parameter_merge_3.v" obsolete="true"><result status="valid" time="1.02"/></proof>
<proof prover="0" edited="mergesort_queue_MergesortQueue_WP_parameter_merge_3.v"><result status="valid" time="1.89"/></proof>
</goal>
<goal name="WP_parameter merge.30" expl="30. loop variant decrease">
<proof prover="4"><result status="valid" time="0.03"/></proof>
......@@ -110,7 +110,7 @@
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter merge.32" expl="32. loop invariant preservation">
<proof prover="5"><result status="valid" time="0.54"/></proof>
<proof prover="5"><result status="valid" time="0.83"/></proof>
</goal>
<goal name="WP_parameter merge.33" expl="33. loop invariant preservation">
<proof prover="4"><result status="valid" time="0.14"/></proof>
......@@ -119,7 +119,7 @@
<proof prover="5"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="WP_parameter merge.35" expl="35. loop invariant preservation">
<proof prover="1" timelimit="5"><result status="valid" time="1.30"/></proof>
<proof prover="1" timelimit="5"><result status="valid" time="1.86"/></proof>
</goal>
<goal name="WP_parameter merge.36" expl="36. loop variant decrease">
<proof prover="4"><result status="valid" time="0.02"/></proof>
......@@ -214,7 +214,7 @@
<proof prover="4" timelimit="6"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter mergesort.5" expl="5. loop invariant preservation">
<proof prover="2"><result status="valid" time="3.81"/></proof>
<proof prover="2"><result status="valid" time="5.21"/></proof>
</goal>
<goal name="WP_parameter mergesort.6" expl="6. loop invariant preservation">
<proof prover="4" timelimit="6"><result status="valid" time="0.06"/></proof>
......@@ -250,7 +250,7 @@
<proof prover="4" timelimit="6"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter mergesort.16" expl="16. postcondition">
<proof prover="4" timelimit="6"><result status="valid" time="0.98"/></proof>
<proof prover="4" timelimit="6"><result status="valid" time="1.52"/></proof>
</goal>
<goal name="WP_parameter mergesort.17" expl="17. assertion">
<proof prover="1"><result status="valid" time="0.08"/></proof>
......
This diff is collapsed.
......@@ -7,7 +7,7 @@
<prover id="2" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<file name="../there_and_back_again.mlw" expanded="true">
<theory name="Convolution" sum="140c7a774b0ea66d8bf9d025eb37a013" expanded="true">
<theory name="Convolution" sum="ba0b2f319de0699f33cf9bce8b499d5e" expanded="true">
<goal name="WP_parameter convolution_rec" expl="VC for convolution_rec">
<transf name="split_goal_wp">
<goal name="WP_parameter convolution_rec.1" expl="1. postcondition">
......@@ -48,7 +48,7 @@
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter palindrome_rec.3" expl="3. postcondition">
<proof prover="3"><result status="valid" time="1.20"/></proof>
<proof prover="3"><result status="valid" time="1.88"/></proof>
</goal>
<goal name="WP_parameter palindrome_rec.4" expl="4. postcondition">
<proof prover="2"><result status="valid" time="0.02"/></proof>
......@@ -73,14 +73,14 @@
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter palindrome_rec.11" expl="11. exceptional postcondition">
<proof prover="1"><result status="valid" time="0.35"/></proof>
<proof prover="1"><result status="valid" time="0.50"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter palindrome_rec.12" expl="12. unreachable point">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter palindrome_rec.13" expl="13. exceptional postcondition">
<proof prover="0" edited="there_and_back_again_Palindrome_WP_parameter_palindrome_rec_2.v"><result status="valid" time="1.15"/></proof>
<proof prover="0" edited="there_and_back_again_Palindrome_WP_parameter_palindrome_rec_2.v"><result status="valid" time="1.99"/></proof>
</goal>
<goal name="WP_parameter palindrome_rec.14" expl="14. unreachable point">
<proof prover="1"><result status="valid" time="0.00"/></proof>
......
This diff is collapsed.
......@@ -20,7 +20,7 @@
</transf>
</goal>
<goal name="depths_unique">
<proof prover="0" timelimit="30" edited="vstte12_tree_reconstruction_Tree_depths_unique_1.v"><result status="valid" time="1.11"/></proof>
<proof prover="0" timelimit="30" edited="vstte12_tree_reconstruction_Tree_depths_unique_1.v"><result status="valid" time="1.69"/></proof>
</goal>
<goal name="depths_prefix">
<transf name="induction_ty_lex">
......@@ -74,10 +74,10 @@
<proof prover="5" memlimit="0"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter build_rec.7" expl="7. exceptional postcondition">
<proof prover="0" edited="vstte12_tree_reconstruction_WP_TreeReconstruction_WP_parameter_build_rec_3.v"><result status="valid" time="1.05"/></proof>
<proof prover="0" edited="vstte12_tree_reconstruction_WP_TreeReconstruction_WP_parameter_build_rec_3.v"><result status="valid" time="2.29"/></proof>
</goal>
<goal name="WP_parameter build_rec.8" expl="8. exceptional postcondition">
<proof prover="0" edited="vstte12_tree_reconstruction_WP_TreeReconstruction_WP_parameter_build_rec_4.v"><result status="valid" time="0.96"/></proof>
<proof prover="0" edited="vstte12_tree_reconstruction_WP_TreeReconstruction_WP_parameter_build_rec_4.v"><result status="valid" time="2.09"/></proof>
</goal>
</transf>
</goal>
......@@ -87,10 +87,10 @@
<proof prover="5" memlimit="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter build.2" expl="2. exceptional postcondition">
<proof prover="0" edited="vstte12_tree_reconstruction_WP_TreeReconstruction_WP_parameter_build_3.v"><result status="valid" time="1.00"/></proof>
<proof prover="0" edited="vstte12_tree_reconstruction_WP_TreeReconstruction_WP_parameter_build_3.v"><result status="valid" time="2.21"/></proof>
</goal>
<goal name="WP_parameter build.3" expl="3. exceptional postcondition">
<proof prover="0" edited="vstte12_tree_reconstruction_WP_TreeReconstruction_WP_parameter_build_4.v"><result status="valid" time="1.00"/></proof>
<proof prover="0" edited="vstte12_tree_reconstruction_WP_TreeReconstruction_WP_parameter_build_4.v"><result status="valid" time="2.05"/></proof>
</goal>
</transf>
</goal>
......@@ -99,15 +99,15 @@
<goal name="WP_parameter harness" expl="VC for harness">
<transf name="split_goal_wp">
<goal name="WP_parameter harness.1" expl="1. postcondition">
<proof prover="0" edited="vstte12_tree_reconstruction_WP_Harness_WP_parameter_harness_3.v"><result status="valid" time="1.08"/></proof>
<proof prover="0" edited="vstte12_tree_reconstruction_WP_Harness_WP_parameter_harness_3.v"><result status="valid" time="1.98"/></proof>
</goal>
<goal name="WP_parameter harness.2" expl="2.">
<proof prover="0" edited="vstte12_tree_reconstruction_WP_Harness_WP_parameter_harness_4.v"><result status="valid" time="1.15"/></proof>
<proof prover="0" edited="vstte12_tree_reconstruction_WP_Harness_WP_parameter_harness_4.v"><result status="valid" time="2.04"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter harness2" expl="VC for harness2">
<proof prover="0" edited="vstte12_tree_reconstruction_WP_Harness_WP_parameter_harness2_2.v"><result status="valid" time="1.17"/></proof>
<proof prover="0" edited="vstte12_tree_reconstruction_WP_Harness_WP_parameter_harness2_2.v"><result status="valid" time="2.44"/></proof>
</goal>
</theory>
<theory name="ZipperBasedTermination" sum="ecdbc871d09372b90b85380073efb0c7">
......@@ -133,16 +133,16 @@
</theory>
<theory name="ZipperBased" sum="635fff34f68f9bb192ecae9d6130e46e" expanded="true">
<goal name="forest_depths_append">
<proof prover="0" edited="vstte12_tree_reconstruction_WP_ZipperBased_forest_depths_append_1.v" obsolete="true"><result status="valid" time="1.10"/></proof>
<proof prover="0" edited="vstte12_tree_reconstruction_WP_ZipperBased_forest_depths_append_1.v"><result status="valid" time="2.13"/></proof>
</goal>
<goal name="g_append">
<proof prover="0" timelimit="20" edited="vstte12_tree_reconstruction_WP_ZipperBased_g_append_1.v" obsolete="true"><result status="valid" time="1.59"/></proof>
<proof prover="0" timelimit="20" edited="vstte12_tree_reconstruction_WP_ZipperBased_g_append_1.v"><result status="valid" time="3.14"/></proof>
</goal>
<goal name="right_nil">
<proof prover="0" timelimit="29" edited="vstte12_tree_reconstruction_WP_ZipperBased_right_nil_1.v" obsolete="true"><result status="valid" time="6.24"/></proof>
<proof prover="0" timelimit="29" edited="vstte12_tree_reconstruction_WP_ZipperBased_right_nil_1.v"><result status="valid" time="10.05"/></proof>
</goal>
<goal name="main_lemma">
<proof prover="0" timelimit="20" edited="vstte12_tree_reconstruction_WP_ZipperBased_main_lemma_1.v" obsolete="true"><result status="valid" time="1.31"/></proof>
<proof prover="0" timelimit="20" edited="vstte12_tree_reconstruction_WP_ZipperBased_main_lemma_1.v"><result status="valid" time="2.42"/></proof>
</goal>
<goal name="WP_parameter tc" expl="VC for tc">
<transf name="split_goal_wp">
......@@ -165,16 +165,16 @@
</goal>
<goal name="WP_parameter tc.5" expl="5. precondition">
<proof prover="1"><result status="valid" time="0.05"/></proof>
<proof prover="3"><result status="valid" time="5.30"/></proof>
<proof prover="5" memlimit="1000"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="8.34"/></proof>
<proof prover="5" memlimit="1000"><result status="valid" time="0.14"/></proof>
</goal>
<goal name="WP_parameter tc.6" expl="6. postcondition">
<proof prover="1"><result status="valid" time="0.39"/></proof>
<proof prover="3"><result status="valid" time="0.71"/></proof>
<proof prover="3"><result status="valid" time="1.17"/></proof>
</goal>
<goal name="WP_parameter tc.7" expl="7. exceptional postcondition">
<proof prover="1"><result status="valid" time="2.08"/></proof>
<proof prover="3"><result status="valid" time="0.38"/></proof>
<proof prover="1"><result status="valid" time="3.75"/></proof>
<proof prover="3"><result status="valid" time="0.68"/></proof>
</goal>
<goal name="WP_parameter tc.8" expl="8. variant decrease">
<proof prover="1"><result status="valid" time="0.06"/></proof>
......@@ -182,10 +182,10 @@
<proof prover="5" memlimit="1000"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter tc.9" expl="9. precondition">
<proof prover="5" memlimit="1000"><result status="valid" time="0.88"/></proof>
<proof prover="5" memlimit="1000"><result status="valid" time="1.47"/></proof>
</goal>
<goal name="WP_parameter tc.10" expl="10. postcondition">
<proof prover="1"><result status="valid" time="0.06"/></proof>
<proof prover="1"><result status="valid" time="0.17"/></proof>
<proof prover="3"><result status="valid" time="0.08"/></proof>
<proof prover="5" memlimit="1000"><result status="valid" time="0.02"/></proof>
</goal>
......@@ -202,7 +202,7 @@
<goal name="WP_parameter tc.13" expl="13. precondition">
<proof prover="1"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.04"/></proof>
<proof prover="5" memlimit="1000"><result status="valid" time="0.70"/></proof>
<proof prover="5" memlimit="1000"><result status="valid" time="1.05"/></proof>
</goal>
<goal name="WP_parameter tc.14" expl="14. postcondition">
<proof prover="1"><result status="valid" time="0.02"/></proof>
......@@ -224,12 +224,12 @@
<proof prover="5" memlimit="1000"><result status="valid" time="0.36"/></proof>
</goal>
<goal name="WP_parameter tc.18" expl="18. postcondition">
<proof prover="1"><result status="valid" time="7.72"/></proof>
<proof prover="3"><result status="valid" time="0.79"/></proof>
<proof prover="1"><result status="valid" time="9.30"/></proof>
<proof prover="3"><result status="valid" time="1.33"/></proof>
</goal>
<goal name="WP_parameter tc.19" expl="19. exceptional postcondition">
<proof prover="1"><result status="valid" time="5.07"/></proof>
<proof prover="3"><result status="valid" time="0.47"/></proof>
<proof prover="3"><result status="valid" time="0.79"/></proof>
</goal>