Commit 0b57906c authored by MARCHE Claude's avatar MARCHE Claude

update sessions

parent 1f1f8b2c
......@@ -4,7 +4,7 @@
<why3session shape_version="4">
<prover id="2" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../algo63.mlw" proved="true">
<theory name="Algo63" proved="true" sum="97df5190bde02efd9e0de8cdbea3356f">
<theory name="Algo63" proved="true">
<goal name="VC exchange" expl="VC for exchange" proved="true">
<proof prover="2"><result status="valid" time="0.03" steps="62"/></proof>
</goal>
......
......@@ -4,7 +4,7 @@
<why3session shape_version="4">
<prover id="3" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../algo63.mlw" proved="true">
<theory name="Algo63" proved="true" sum="97df5190bde02efd9e0de8cdbea3356f">
<theory name="Algo63" proved="true">
<goal name="VC exchange" expl="VC for exchange" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="VC exchange.0" expl="index in array bounds" proved="true">
......@@ -186,7 +186,7 @@
<proof prover="3"><result status="valid" time="0.38" steps="610"/></proof>
</goal>
<goal name="VC partition_.51" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.28" steps="386"/></proof>
<proof prover="3"><result status="valid" time="0.15" steps="386"/></proof>
</goal>
<goal name="VC partition_.52" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01" steps="18"/></proof>
......
......@@ -4,7 +4,7 @@
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../algo64.mlw" proved="true">
<theory name="Algo64" proved="true" sum="d424a975b8a7b2f1bb6825629de9143a">
<theory name="Algo64" proved="true">
<goal name="VC quicksort" expl="VC for quicksort" proved="true">
<proof prover="0"><result status="valid" time="0.67" steps="2087"/></proof>
</goal>
......
......@@ -4,7 +4,7 @@
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../algo65.mlw" proved="true">
<theory name="Algo65" proved="true" sum="06510cf0c04926152c626875f383e149">
<theory name="Algo65" proved="true">
<goal name="VC find" expl="VC for find" proved="true">
<proof prover="0"><result status="valid" time="0.52" steps="1688"/></proof>
</goal>
......
......@@ -80,7 +80,7 @@
<goal name="VC binary_sort.21.0" expl="loop invariant preservation" proved="true">
<transf name="case" proved="true" arg1="(j=k)">
<goal name="VC binary_sort.21.0.0" expl="true case (loop invariant preservation)" proved="true">
<proof prover="1" timelimit="10" memlimit="4000"><result status="valid" time="1.50" steps="1017"/></proof>
<proof prover="1" timelimit="10" memlimit="4000"><result status="valid" time="1.50" steps="1019"/></proof>
</goal>
<goal name="VC binary_sort.21.0.1" expl="false case (loop invariant preservation)" proved="true">
<proof prover="1" timelimit="1"><result status="valid" time="0.80" steps="689"/></proof>
......
......@@ -4,7 +4,7 @@
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../bubble_sort.mlw" proved="true">
<theory name="BubbleSort" proved="true" sum="6a88fa014742f7a66d4e38a455762c82">
<theory name="BubbleSort" proved="true">
<goal name="VC bubble_sort" expl="VC for bubble_sort" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="VC bubble_sort.0" expl="loop invariant init" proved="true">
......
......@@ -147,7 +147,7 @@
<proof prover="7"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="VC shortest_path_code.12.0.1" expl="VC for shortest_path_code" proved="true">
<proof prover="8" timelimit="1" memlimit="1000"><result status="valid" time="0.56" steps="1315"/></proof>
<proof prover="8" timelimit="1" memlimit="1000"><result status="valid" time="0.56" steps="1316"/></proof>
</goal>
<goal name="VC shortest_path_code.12.0.2" expl="VC for shortest_path_code" proved="true">
<proof prover="7"><result status="valid" time="0.02"/></proof>
......@@ -159,15 +159,15 @@
<proof prover="7"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC shortest_path_code.12.0.5" expl="VC for shortest_path_code" proved="true">
<proof prover="8"><result status="valid" time="1.44" steps="2782"/></proof>
<proof prover="8"><result status="valid" time="1.44" steps="2783"/></proof>
</goal>
<goal name="VC shortest_path_code.12.0.6" expl="VC for shortest_path_code" proved="true">
<transf name="case" proved="true" arg1="(v = v1)">
<goal name="VC shortest_path_code.12.0.6.0" expl="true case" proved="true">
<proof prover="4" memlimit="2000"><result status="valid" time="2.10" steps="2671"/></proof>
<proof prover="4" memlimit="2000"><result status="valid" time="1.79" steps="2672"/></proof>
</goal>
<goal name="VC shortest_path_code.12.0.6.1" expl="false case" proved="true">
<proof prover="8"><result status="valid" time="0.96" steps="2030"/></proof>
<proof prover="8"><result status="valid" time="0.96" steps="2031"/></proof>
</goal>
</transf>
</goal>
......
......@@ -4,7 +4,7 @@
<why3session shape_version="4">
<prover id="2" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../find.mlw" proved="true">
<theory name="FIND" proved="true" sum="9a937b8cad77b48e77de37b6f7effb86">
<theory name="FIND" proved="true">
<goal name="VC _N" expl="VC for _N" proved="true">
<proof prover="2"><result status="valid" time="0.00" steps="1"/></proof>
</goal>
......@@ -70,10 +70,10 @@
<goal name="VC find.18" expl="loop invariant preservation" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="VC find.18.0" expl="VC for find" proved="true">
<proof prover="2" timelimit="15"><result status="valid" time="3.96" steps="3067"/></proof>
<proof prover="2" timelimit="15"><result status="valid" time="3.96" steps="3026"/></proof>
</goal>
<goal name="VC find.18.1" expl="VC for find" proved="true">
<proof prover="2" timelimit="15"><result status="valid" time="4.67" steps="3347"/></proof>
<proof prover="2" timelimit="15"><result status="valid" time="4.67" steps="3304"/></proof>
</goal>
<goal name="VC find.18.2" expl="VC for find" proved="true">
<proof prover="2"><result status="valid" time="1.82" steps="1378"/></proof>
......@@ -91,7 +91,7 @@
<proof prover="2"><result status="valid" time="0.02" steps="57"/></proof>
</goal>
<goal name="VC find.18.7" expl="VC for find" proved="true">
<proof prover="2"><result status="valid" time="0.63" steps="231"/></proof>
<proof prover="2"><result status="valid" time="0.63" steps="236"/></proof>
</goal>
</transf>
</goal>
......
......@@ -4,7 +4,7 @@
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../flag.mlw" proved="true">
<theory name="Flag" proved="true" sum="9e47e5e7289c0f5b96b7d19586fc4d1f">
<theory name="Flag" proved="true">
<goal name="VC dutch_flag" expl="VC for dutch_flag" proved="true">
<proof prover="0"><result status="valid" time="0.38" steps="881"/></proof>
</goal>
......
......@@ -8,7 +8,7 @@
<prover id="4" name="Eprover" version="1.8-001" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="9" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../gcd.mlw" proved="true">
<theory name="EuclideanAlgorithm" proved="true" sum="44d7bb87668a49a2f2a4f5b307eac883">
<theory name="EuclideanAlgorithm" proved="true">
<goal name="VC euclid" expl="VC for euclid" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="VC euclid.0" expl="check modulo by zero" proved="true">
......@@ -26,12 +26,12 @@
</transf>
</goal>
</theory>
<theory name="EuclideanAlgorithmIterative" proved="true" sum="3ff6d7d9dd6e825392762f38be2bf072">
<theory name="EuclideanAlgorithmIterative" proved="true">
<goal name="VC euclid" expl="VC for euclid" proved="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
</theory>
<theory name="BinaryGcd" proved="true" sum="f288abe81fe0bb1c65550b0d7201e3b9">
<theory name="BinaryGcd" proved="true">
<goal name="even1" proved="true">
<proof prover="9"><result status="valid" time="0.01" steps="19"/></proof>
</goal>
......@@ -140,7 +140,7 @@
</transf>
</goal>
</theory>
<theory name="EuclideanAlgorithm63" proved="true" sum="2957f2c27fa5f1ab089e561053c1d9ac">
<theory name="EuclideanAlgorithm63" proved="true">
<goal name="VC euclid" expl="VC for euclid" proved="true">
<proof prover="1"><result status="valid" time="0.24"/></proof>
</goal>
......
......@@ -6,17 +6,17 @@
<prover id="2" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="3" name="Coq" version="8.7.1" timelimit="0" steplimit="0" memlimit="0"/>
<file name="../gcd_vc_sp.mlw" proved="true">
<theory name="EuclideanAlgorithm" proved="true" sum="44d7bb87668a49a2f2a4f5b307eac883">
<theory name="EuclideanAlgorithm" proved="true">
<goal name="VC euclid" expl="VC for euclid" proved="true">
<proof prover="2"><result status="valid" time="0.06"/></proof>
</goal>
</theory>
<theory name="EuclideanAlgorithmIterative" proved="true" sum="3ff6d7d9dd6e825392762f38be2bf072">
<theory name="EuclideanAlgorithmIterative" proved="true">
<goal name="VC euclid" expl="VC for euclid" proved="true">
<proof prover="2"><result status="valid" time="0.09"/></proof>
</goal>
</theory>
<theory name="BinaryGcd" proved="true" sum="f288abe81fe0bb1c65550b0d7201e3b9">
<theory name="BinaryGcd" proved="true">
<goal name="even1" proved="true">
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
......@@ -125,7 +125,7 @@
</transf>
</goal>
</theory>
<theory name="EuclideanAlgorithm63" proved="true" sum="2957f2c27fa5f1ab089e561053c1d9ac">
<theory name="EuclideanAlgorithm63" proved="true">
<goal name="VC euclid" expl="VC for euclid" proved="true">
<proof prover="2"><result status="valid" time="0.08"/></proof>
</goal>
......
......@@ -5,7 +5,7 @@
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Z3" version="4.4.0" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../gnome_sort.mlw" proved="true">
<theory name="GnomeSort" proved="true" sum="a854fa5002cbedc85b249f5d1c7ed472">
<theory name="GnomeSort" proved="true">
<goal name="VC gnome_sort" expl="VC for gnome_sort" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="VC gnome_sort.0" expl="loop invariant init" proved="true">
......
......@@ -5,7 +5,7 @@
<prover id="0" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="1.30" timelimit="36" steplimit="0" memlimit="1000"/>
<file name="../insertion_sort.mlw" proved="true">
<theory name="InsertionSort" proved="true" sum="f15d16b0aa8edb88df314c3410aa655b">
<theory name="InsertionSort" proved="true">
<goal name="VC insertion_sort" expl="VC for insertion_sort" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="VC insertion_sort.0" expl="loop invariant init" proved="true">
......@@ -80,7 +80,7 @@
<proof prover="3"><result status="valid" time="0.01" steps="28"/></proof>
</goal>
</theory>
<theory name="InsertionSortGen" proved="true" sum="f1a4031b8ce80859842a7a90e9e30ee3">
<theory name="InsertionSortGen" proved="true">
<goal name="VC insertion_sort" expl="VC for insertion_sort" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="VC insertion_sort.0" expl="loop invariant init" proved="true">
......
......@@ -4,22 +4,22 @@
<why3session shape_version="4">
<prover id="2" name="Alt-Ergo" version="1.30" timelimit="36" steplimit="0" memlimit="1000"/>
<file name="../insertion_sort_naive.mlw" proved="true">
<theory name="InsertionSortNaive" proved="true" sum="a4f65d18f0c985a7668d8fb3cba76c9f">
<theory name="InsertionSortNaive" proved="true">
<goal name="VC sort" expl="VC for sort" proved="true">
<proof prover="2"><result status="valid" time="1.53" steps="925"/></proof>
</goal>
</theory>
<theory name="InsertionSortNaiveGen" proved="true" sum="fc8a818e2ed534d1a523461dcc7c70c8">
<theory name="InsertionSortNaiveGen" proved="true">
<goal name="VC sort" expl="VC for sort" proved="true">
<proof prover="2"><result status="valid" time="0.95" steps="1751"/></proof>
</goal>
</theory>
<theory name="InsertionSortParam" proved="true" sum="87055066af3eb8e53d4047ea582c0191">
<theory name="InsertionSortParam" proved="true">
<goal name="VC sort" expl="VC for sort" proved="true">
<proof prover="2"><result status="valid" time="0.90" steps="1594"/></proof>
</goal>
</theory>
<theory name="InsertionSortParamBad" proved="true" sum="6d297b995ebd5654590bda56ce307a9b">
<theory name="InsertionSortParamBad" proved="true">
<goal name="VC sort" expl="VC for sort" proved="true">
<proof prover="2"><result status="valid" time="1.19" steps="2722"/></proof>
</goal>
......
......@@ -38,7 +38,7 @@
<goal name="VC maximum.4" expl="loop invariant preservation" proved="true">
<transf name="split_intros_goal_wp" proved="true" >
<goal name="VC maximum.4.0" expl="VC for maximum" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="19"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="21"/></proof>
</goal>
<goal name="VC maximum.4.1" expl="VC for maximum" proved="true">
<transf name="right" proved="true" >
......@@ -51,13 +51,13 @@
<proof prover="2"><result status="valid" time="0.10"/></proof>
</goal>
<goal name="VC maximum.4.1.0.2" expl="VC for maximum" proved="true">
<proof prover="1" timelimit="1"><result status="valid" time="0.03" steps="57"/></proof>
<proof prover="1" timelimit="1"><result status="valid" time="0.03" steps="59"/></proof>
</goal>
<goal name="VC maximum.4.1.0.3" expl="VC for maximum" proved="true">
<proof prover="3"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC maximum.4.1.0.4" expl="VC for maximum" proved="true">
<proof prover="1" memlimit="2000"><result status="valid" time="4.08" steps="3019"/></proof>
<proof prover="1" memlimit="2000"><result status="valid" time="4.08" steps="3072"/></proof>
</goal>
</transf>
</goal>
......
......@@ -5,7 +5,7 @@
<prover id="0" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../mccarthy_vc_sp.mlw" proved="true">
<theory name="McCarthy91" proved="true" sum="13b896e51d6f77e4be03ed7c66d03ca8">
<theory name="McCarthy91" proved="true">
<goal name="VC f91" expl="VC for f91" proved="true">
<proof prover="1"><result status="valid" time="0.00"/></proof>
</goal>
......@@ -16,7 +16,7 @@
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
</theory>
<theory name="McCarthy91Mach" proved="true" sum="7d4600e0ee1b08517405296863b5c9d8">
<theory name="McCarthy91Mach" proved="true">
<goal name="VC f91" expl="VC for f91" proved="true">
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
......
......@@ -6,9 +6,9 @@
<prover id="4" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="11" name="Alt-Ergo" version="1.30" timelimit="11" steplimit="0" memlimit="1000"/>
<file name="../mergesort_array.mlw" proved="true">
<theory name="Elt" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e">
<theory name="Elt" proved="true">
</theory>
<theory name="Merge" proved="true" sum="813126ce9841041d232baba709089035">
<theory name="Merge" proved="true">
<goal name="VC merge" expl="VC for merge" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="VC merge.0" expl="loop invariant init" proved="true">
......@@ -167,7 +167,7 @@
<goal name="VC merge_using.11" expl="assertion" proved="true">
<transf name="inline_goal" proved="true" >
<goal name="VC merge_using.11.0" expl="assertion" proved="true">
<proof prover="4" timelimit="11"><result status="valid" time="0.62"/></proof>
<proof prover="4" timelimit="11"><result status="valid" time="0.45"/></proof>
</goal>
</transf>
</goal>
......@@ -192,7 +192,7 @@
</transf>
</goal>
</theory>
<theory name="TopDownMergesort" proved="true" sum="0e1da44e6888d41d694e6eab8f1c4adc">
<theory name="TopDownMergesort" proved="true">
<goal name="VC mergesort_rec" expl="VC for mergesort_rec" proved="true">
<proof prover="11"><result status="valid" time="0.33" steps="694"/></proof>
</goal>
......@@ -200,7 +200,7 @@
<proof prover="11"><result status="valid" time="0.01" steps="36"/></proof>
</goal>
</theory>
<theory name="BottomUpMergesort" proved="true" sum="3a8575d5f117f4c925fe7aa77a6dac60">
<theory name="BottomUpMergesort" proved="true">
<goal name="VC bottom_up_mergesort" expl="VC for bottom_up_mergesort" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="VC bottom_up_mergesort.0" expl="loop invariant init" proved="true">
......@@ -325,7 +325,7 @@
</transf>
</goal>
</theory>
<theory name="NaturalMergesort" proved="true" sum="e57520d034e6f5becdbb8f87b610ca27">
<theory name="NaturalMergesort" proved="true">
<goal name="VC find_run" expl="VC for find_run" proved="true">
<proof prover="11"><result status="valid" time="0.02" steps="47"/></proof>
</goal>
......
......@@ -3,15 +3,15 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../Nat.mlw">
<theory name="Nat">
<goal name="WP_parameter nat_to_int_nonnegative" expl="VC for nat_to_int_nonnegative">
<proof prover="1"><result status="valid" time="0.01" steps="14"/></proof>
<file name="../Nat.mlw" proved="true">
<theory name="Nat" proved="true">
<goal name="VC nat_to_int_nonnegative" expl="VC for nat_to_int_nonnegative" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="18"/></proof>
</goal>
<goal name="WP_parameter add_nat_simulate_add_int" expl="VC for add_nat_simulate_add_int">
<proof prover="1"><result status="valid" time="0.03" steps="82"/></proof>
<goal name="VC add_nat_simulate_add_int" expl="VC for add_nat_simulate_add_int" proved="true">
<proof prover="1"><result status="valid" time="0.03" steps="42"/></proof>
</goal>
<goal name="one_nat_value" expl="">
<goal name="one_nat_value" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="5"/></proof>
</goal>
</theory>
......
......@@ -4,7 +4,7 @@
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../quicksort.mlw" proved="true">
<theory name="Quicksort" proved="true" sum="2a868e31374bafdd7feffbd9eccfa58d">
<theory name="Quicksort" proved="true">
<goal name="VC quick_rec" expl="VC for quick_rec" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="VC quick_rec.0" expl="index in array bounds" proved="true">
......@@ -103,17 +103,17 @@
<proof prover="0"><result status="valid" time="0.01" steps="22"/></proof>
</goal>
</theory>
<theory name="Shuffle" proved="true" sum="5784873acff0f6be9471667822c9d384">
<theory name="Shuffle" proved="true">
<goal name="VC shuffle" expl="VC for shuffle" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="53"/></proof>
</goal>
</theory>
<theory name="QuicksortWithShuffle" proved="true" sum="97b10106a2a679162e43a0f382387347">
<theory name="QuicksortWithShuffle" proved="true">
<goal name="VC qs" expl="VC for qs" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
</theory>
<theory name="Quicksort3way" proved="true" sum="71958d8c4aeb3e8a7700c71c49103067">
<theory name="Quicksort3way" proved="true">
<goal name="VC quick_rec" expl="VC for quick_rec" proved="true">
<proof prover="0"><result status="valid" time="3.51" steps="6499"/></proof>
<transf name="split_goal_wp" proved="true" >
......@@ -252,7 +252,7 @@
<proof prover="0"><result status="valid" time="0.00" steps="11"/></proof>
</goal>
</theory>
<theory name="Test" proved="true" sum="d5d60b2323c955244d4f499a3a11e8ce">
<theory name="Test" proved="true">
<goal name="VC test1" expl="VC for test1" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="13"/></proof>
</goal>
......
......@@ -4,7 +4,7 @@
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../selection_sort.mlw" proved="true">
<theory name="SelectionSort" proved="true" sum="12573246303aa566c40172f97eed082e">
<theory name="SelectionSort" proved="true">
<goal name="VC selection_sort" expl="VC for selection_sort" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="VC selection_sort.0" expl="loop invariant init" proved="true">
......
......@@ -5,9 +5,9 @@
<prover id="0" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../skew_heaps.mlw" proved="true">
<theory name="Heap" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e">
<theory name="Heap" proved="true">
</theory>
<theory name="SkewHeaps" proved="true" sum="63aa80fdc4832811bc58d8fdcff29c30">
<theory name="SkewHeaps" proved="true">
<goal name="VC root_is_min" expl="VC for root_is_min" proved="true">
<proof prover="1"><result status="valid" time="0.65" steps="1358"/></proof>
</goal>
......@@ -27,7 +27,7 @@
<proof prover="1"><result status="valid" time="0.02" steps="144"/></proof>
</goal>
</theory>
<theory name="HeapSort" proved="true" sum="36984cdc5144dd34796210d23d1a6846">
<theory name="HeapSort" proved="true">
<goal name="VC heapsort" expl="VC for heapsort" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="VC heapsort.0" expl="loop invariant init" proved="true">
......
......@@ -229,7 +229,7 @@
<proof prover="10"><result status="timeout" time="1.01"/></proof>
</goal>
<goal name="ok16" proved="true">
<proof prover="1"><result status="timeout" time="1.00"/></proof>
<proof prover="1"><result status="unknown" time="1.00"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="timeout" time="0.87"/></proof>
<proof prover="5"><result status="valid" time="0.00"/></proof>
......@@ -239,7 +239,7 @@
<proof prover="10"><result status="timeout" time="1.01"/></proof>
</goal>
<goal name="ok17" proved="true">
<proof prover="1"><result status="timeout" time="1.00"/></proof>
<proof prover="1"><result status="unknown" time="1.00"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="timeout" time="1.01"/></proof>
<proof prover="5"><result status="valid" time="0.00"/></proof>
......@@ -403,7 +403,7 @@
</goal>
<goal name="smoke4">
<proof prover="0" timelimit="1"><result status="timeout" time="0.99"/></proof>
<proof prover="1"><result status="timeout" time="2.30"/></proof>
<proof prover="1"><result status="timeout" time="1.00"/></proof>
<proof prover="3"><result status="unknown" time="0.01"/></proof>
<proof prover="4"><result status="timeout" time="0.96"/></proof>
<proof prover="5" timelimit="1"><result status="timeout" time="1.00"/></proof>
......@@ -468,7 +468,7 @@
</goal>
<goal name="f1">
<proof prover="0" timelimit="1"><result status="timeout" time="1.01"/></proof>
<proof prover="1"><result status="timeout" time="2.00"/></proof>
<proof prover="1"><result status="timeout" time="1.00"/></proof>
<proof prover="3"><result status="unknown" time="0.01"/></proof>
<proof prover="4"><result status="timeout" time="0.86"/></proof>
<proof prover="5" timelimit="1"><result status="timeout" time="1.00"/></proof>
......@@ -489,7 +489,7 @@
</goal>
<goal name="f2">
<proof prover="0" timelimit="1"><result status="timeout" time="1.01"/></proof>
<proof prover="1"><result status="timeout" time="2.00"/></proof>
<proof prover="1"><result status="timeout" time="1.00"/></proof>
<proof prover="3"><result status="unknown" time="0.00"/></proof>
<proof prover="4"><result status="timeout" time="0.85"/></proof>
<proof prover="5" timelimit="1"><result status="timeout" time="1.00"/></proof>
......@@ -519,7 +519,7 @@
<proof prover="10"><result status="timeout" time="1.01"/></proof>
</goal>
<goal name="g3a" proved="true">
<proof prover="1"><result status="timeout" time="2.00"/></proof>
<proof prover="1"><result status="timeout" time="1.00"/></proof>
<proof prover="3" timelimit="5"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="valid" time="0.04" steps="100"/></proof>
<proof prover="5"><result status="valid" time="0.00"/></proof>
......@@ -545,7 +545,7 @@
</goal>
<goal name="f3">
<proof prover="0" timelimit="1"><result status="timeout" time="1.00"/></proof>
<proof prover="1"><result status="timeout" time="2.00"/></proof>
<proof prover="1"><result status="timeout" time="1.00"/></proof>
<proof prover="3"><result status="unknown" time="0.00"/></proof>
<proof prover="4"><result status="timeout" time="1.00"/></proof>
<proof prover="5" timelimit="1"><result status="timeout" time="1.00"/></proof>
......@@ -1012,7 +1012,7 @@
<proof prover="10"><result status="timeout" time="1.01"/></proof>
</goal>
<goal name="ok19" proved="true">
<proof prover="1"><result status="timeout" time="1.00"/></proof>
<proof prover="1"><result status="unknown" time="1.00"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="timeout" time="0.90"/></proof>
<proof prover="5"><result status="valid" time="0.00"/></proof>
......@@ -1156,7 +1156,7 @@
</goal>
<goal name="smoke4">
<proof prover="0" timelimit="1"><result status="timeout" time="1.00"/></proof>
<proof prover="1"><result status="unknown" time="2.18"/></proof>
<proof prover="1"><result status="timeout" time="2.18"/></proof>
<proof prover="3"><result status="unknown" time="0.00"/></proof>
<proof prover="4"><result status="timeout" time="0.86"/></proof>
<proof prover="5" timelimit="1"><result status="timeout" time="1.00"/></proof>
......@@ -1425,7 +1425,7 @@
<proof prover="10"><result status="timeout" time="1.01"/></proof>
</goal>
<goal name="ok16" proved="true">
<proof prover="1"><result status="timeout" time="1.00"/></proof>
<proof prover="1"><result status="unknown" time="1.00"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="timeout" time="0.88"/></proof>
<proof prover="5"><result status="valid" time="0.00"/></proof>
......@@ -1599,7 +1599,7 @@
</goal>
<goal name="smoke4">
<proof prover="0" timelimit="1"><result status="timeout" time="1.01"/></proof>
<proof prover="1"><result status="timeout" time="2.04"/></proof>
<proof prover="1"><result status="timeout" time="1.00"/></proof>
<proof prover="3"><result status="unknown" time="0.00"/></proof>
<proof prover="4"><result status="timeout" time="0.91"/></proof>
<proof prover="5" timelimit="1"><result status="timeout" time="1.00"/></proof>
......@@ -1796,7 +1796,7 @@
<proof prover="10"><result status="valid" time="0.02" steps="95"/></proof>
</goal>
<goal name="ok8" proved="true">
<proof prover="1"><result status="valid" time="0.86"/></proof>
<proof prover="1"><result status="valid" time="0.62"/></proof>
<proof prover="3" timelimit="5"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="valid" time="0.05" steps="95"/></proof>
<proof prover="5"><result status="valid" time="0.00"/></proof>
......@@ -1807,7 +1807,7 @@
</goal>
<goal name="ok9" proved="true">
<proof prover="0"><result status="valid" time="0.14" steps="97"/></proof>
<proof prover="1"><result status="valid" time="0.87"/></proof>
<proof prover="1"><result status="valid" time="0.62"/></proof>
<proof prover="3" timelimit="5"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="valid" time="0.05" steps="97"/></proof>
<proof prover="5"><result status="valid" time="0.00"/></proof>
......@@ -2031,7 +2031,7 @@
</goal>
<goal name="smoke3">
<proof prover="0" timelimit="1"><result status="timeout" time="0.99"/></proof>
<proof prover="1"><result status="unknown" time="2.00"/></proof>
<proof prover="1"><result status="unknown" time="1.61"/></proof>
<proof prover="3"><result status="unknown" time="0.01"/></proof>
<proof prover="4"><result status="timeout" time="1.00"/></proof>
<proof prover="5" timelimit="1"><result status="timeout" time="1.00"/></proof>
......@@ -2042,7 +2042,7 @@
</goal>
<goal name="smoke4">
<proof prover="0" timelimit="1"><result status="timeout" time="1.00"/></proof>
<proof prover="1"><result status="timeout" time="2.02"/></proof>
<proof prover="1"><result status="timeout" time="1.00"/></proof>
<proof prover="3"><result status="unknown" time="0.01"/></proof>
<proof prover="4"><result status="timeout" time="0.99"/></proof>
<proof prover="5" timelimit="1"><result status="timeout" time="0.99"/></proof>
......
......@@ -35,12 +35,12 @@
<transf name="split_goal_wp" >
<goal name="VC triplet.0" expl="assertion" proved="true">
<proof prover="4"><result status="timeout" time="5.00"/></proof>
<proof prover="6"><result status="valid" time="1.00"/></proof>
<proof prover="6"><result status="valid" time="0.66"/></proof>
</goal>
<goal name="VC triplet.1" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="4.68" steps="10733"/></proof>
<proof prover="4"><result status="valid" time="0.31"/></proof>
<proof prover="5"><result status="valid" time="1.46"/></proof>
<proof prover="5"><result status="valid" time="1.02"/></proof>
</goal>
<goal name="VC triplet.2" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.21"/></proof>
......@@ -54,9 +54,9 @@
<proof prover="1"><result status="outofmemory" time="4.28"/></proof>
<proof prover="2"><result status="timeout" time="5.00"/></proof>
<proof prover="3"><result status="timeout" time="5.00"/></proof>
<proof prover="4"><result status="valid" time="1.40"/></proof>
<proof prover="5"><result status="timeout" time="8.00"/></proof>
<proof prover="6"><result status="valid" time="4.18"/></proof>
<proof prover="4"><result status="valid" time="1.06"/></proof>
<proof prover="5"><result status="timeout" time="5.00"/></proof>
<proof prover="6"><result status="valid" time="2.81"/></proof>
</goal>
<goal name="VC triplet.4" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.29"/></proof>
......@@ -65,7 +65,7 @@
<proof prover="3"><result status="valid" time="0.26"/></proof>
</goal>
<goal name="VC triplet.5" expl="assertion" proved="true">
<proof prover="2" timelimit="10" memlimit="4000"><result status="valid" time="11.04" steps="20126"/></proof>
<proof prover="2" timelimit="10" memlimit="4000"><result status="valid" time="9.18" steps="20126"/></proof>
</goal>
<goal name="VC triplet.6" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.25"/></proof>
......@@ -75,12 +75,12 @@
<proof prover="4"><result status="valid" time="0.14"/></proof>
<proof prover="5"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="VC triplet.7" expl="assertion">
<proof prover="5"><result status="timeout" time="5.00"/></proof>
<proof prover="6"><result status="timeout" time="5.00"/></proof>
<goal name="VC triplet.7" expl="assertion" proved="true">
<proof prover="5"><result status="valid" time="4.38"/></proof>
<proof prover="6"><result status="valid" time="3.82"/></proof>
<proof prover="7"><result status="timeout" time="5.01"/></proof>
<proof prover="8"><result status="timeout" time="5.00"/></proof>
<proof prover="9"><result status="unknown" time="4.78"/></proof>
<proof prover="9"><result status="unknown" time="9.88"/></proof>
</goal>
<goal name="VC triplet.8" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.06"/></proof>
......@@ -90,9 +90,9 @@
<proof prover="4"><result status="valid" time="0.15"/></proof>
<proof prover="5"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="VC triplet.9" expl="assertion" proved="true">
<goal name="VC triplet.9" expl="assertion">
<proof prover="5"><result status="timeout" time="5.00"/></proof>
<proof prover="6"><result status="valid" time="2.90"/></proof>
<proof prover="6"><result status="timeout" time="6.00"/></proof>
</goal>
</transf>
</goal>
......@@ -153,7 +153,7 @@
<proof prover="6"><result status="timeout" time="5.00"/></proof>
<proof prover="7"><result status="timeout" time="5.02"/></proof>
<proof prover="8"><result status="timeout" time="5.00"/></proof>