Commit 4145bba5 authored by MARCHE Claude's avatar MARCHE Claude

update obsolete sessions

parent 265e2a01
......@@ -334,10 +334,10 @@
<goal name="eval_change_free.0.10.0.0" proved="true">
<transf name="destruct_alg" proved="true" arg1="x1">
<goal name="eval_change_free.0.10.0.0.0" proved="true">
<proof prover="7"><result status="valid" time="0.08"/></proof>
<proof prover="7"><result status="valid" time="0.13"/></proof>
</goal>
<goal name="eval_change_free.0.10.0.0.1" proved="true">
<proof prover="7"><result status="valid" time="0.13"/></proof>
<proof prover="7"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="eval_change_free.0.10.0.0.2" proved="true">
<proof prover="7"><result status="valid" time="0.14"/></proof>
......
This diff is collapsed.
......@@ -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="182ac0040d40be24d9b569a79008de0a">
<theory name="Algo63" proved="true" sum="b882ca24fd9e33b8497d2ffd24d75517">
<goal name="VC exchange" expl="VC for exchange" proved="true">
<proof prover="2"><result status="valid" time="0.03" steps="62"/></proof>
</goal>
......@@ -184,7 +184,7 @@
</transf>
</goal>
<goal name="VC partition" expl="VC for partition" proved="true">
<proof prover="2"><result status="valid" time="2.98" steps="545"/></proof>
<proof prover="2"><result status="valid" time="3.54" steps="545"/></proof>
</goal>
</theory>
</file>
......
......@@ -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="182ac0040d40be24d9b569a79008de0a">
<theory name="Algo63" proved="true" sum="b882ca24fd9e33b8497d2ffd24d75517">
<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">
......@@ -217,7 +217,7 @@
<proof prover="3"><result status="valid" time="0.00" steps="9"/></proof>
</goal>
<goal name="VC partition.3" expl="postcondition" proved="true">
<proof prover="3" timelimit="30"><result status="valid" time="9.06" steps="727"/></proof>
<proof prover="3" timelimit="30"><result status="valid" time="10.73" steps="727"/></proof>
</goal>
</transf>
</goal>
......
......@@ -3,12 +3,12 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../algo64.mlw" expanded="true">
<theory name="Algo64" sum="33eec8b1d41141f7c4227fd23b153b43" expanded="true">
<goal name="VC quicksort" expl="VC for quicksort" expanded="true">
<file name="../algo64.mlw" proved="true">
<theory name="Algo64" proved="true" sum="53d17c1a5a0d90843aaf1177717a079b">
<goal name="VC quicksort" expl="VC for quicksort" proved="true">
<proof prover="0"><result status="valid" time="0.67" steps="2087"/></proof>
</goal>
<goal name="VC qs" expl="VC for qs" expanded="true">
<goal name="VC qs" expl="VC for qs" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="34"/></proof>
</goal>
</theory>
......
......@@ -3,10 +3,10 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../algo65.mlw" expanded="true">
<theory name="Algo65" sum="f4ab5bd585e0df34ba24ae65241e03dc" expanded="true">
<goal name="VC find" expl="VC for find" expanded="true">
<proof prover="0"><result status="valid" time="0.52" steps="1682"/></proof>
<file name="../algo65.mlw" proved="true">
<theory name="Algo65" proved="true" sum="db2c890cb561211fa36098a88daddfac">
<goal name="VC find" expl="VC for find" proved="true">
<proof prover="0"><result status="valid" time="0.52" steps="1688"/></proof>
</goal>
</theory>
</file>
......
......@@ -6,7 +6,7 @@
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../binary_sort.mlw" proved="true">
<theory name="BinarySort" proved="true" sum="f45759e091adf1bc93196907f82c65a8">
<theory name="BinarySort" proved="true" sum="c1c832159f18a903011e9a535c30f2f6">
<goal name="VC occ_shift" expl="VC for occ_shift" proved="true">
<proof prover="0"><result status="valid" time="0.54"/></proof>
</goal>
......@@ -77,10 +77,10 @@
</goal>
<goal name="VC binary_sort.21" expl="loop invariant preservation" proved="true">
<transf name="case" proved="true" arg1="(j=k)">
<goal name="VC binary_sort.21.0" expl="loop invariant preservation" proved="true">
<proof prover="1" timelimit="10" memlimit="4000"><result status="valid" time="1.66" steps="1272"/></proof>
<goal name="VC binary_sort.21.0" expl="true case (loop invariant preservation)" proved="true">
<proof prover="1" timelimit="10" memlimit="4000"><result status="valid" time="1.66" steps="1019"/></proof>
</goal>
<goal name="VC binary_sort.21.1" expl="loop invariant preservation" proved="true">
<goal name="VC binary_sort.21.1" expl="false case (loop invariant preservation)" proved="true">
<proof prover="1" timelimit="1"><result status="valid" time="0.75" steps="689"/></proof>
</goal>
</transf>
......
......@@ -4,14 +4,14 @@
<why3session shape_version="4">
<prover id="0" name="Z3" version="4.4.0" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../71_disambiguation.mlw">
<theory name="M" proved="true" sum="bc734e8ea460fb0a12336599478f2cd1">
<theory name="M" proved="true" sum="2557322e65bc648467bc260a3a8fbbc4">
<goal name="g" proved="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<transf name="compute_in_goal" proved="true" >
</transf>
</goal>
</theory>
<theory name="M1" proved="true" sum="03a869518d4c28a7d6c15bc9acecb5cd">
<theory name="M1" proved="true" sum="f65ffb4d889019a8435ba0d47668c91d">
<goal name="g" proved="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<transf name="cut" arg1="(0 +^ 0 = 2)">
......@@ -28,11 +28,11 @@
</transf>
</goal>
</theory>
<theory name="M2" sum="85517374ec06b4406222c7e84e769b16">
<theory name="M2" sum="8c032081a5a61311604b36d1847123f3">
<goal name="g">
</goal>
</theory>
<theory name="M3" sum="85517374ec06b4406222c7e84e769b16">
<theory name="M3" sum="8c032081a5a61311604b36d1847123f3">
<goal name="g">
</goal>
</theory>
......
......@@ -4,7 +4,7 @@
<why3session shape_version="4">
<prover id="0" name="CVC4" version="1.5" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../79_compute_unsound.mlw">
<theory name="Soundness" sum="aa1c41b51a76f536179c52b8dcf8a473">
<theory name="Soundness" sum="2d090cdfc8e910c26281f31254572c4d">
<goal name="A" proved="true">
<proof prover="0"><result status="valid" time="0.17"/></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="../bubble_sort.mlw" proved="true">
<theory name="BubbleSort" proved="true" sum="3652d10a9dbb20e7dbddea3c6210177c">
<theory name="BubbleSort" proved="true" sum="6b92ef189b7fec9778d9694b28a1b549">
<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">
......
......@@ -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="75e4da35bcfff9f53aa3139c022463b5">
<theory name="FIND" proved="true" sum="1a76ddb1c204395893984aa32657718e">
<goal name="VC _N" expl="VC for _N" proved="true">
<proof prover="2"><result status="valid" time="0.00" steps="1"/></proof>
</goal>
......@@ -70,7 +70,7 @@
<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="3091"/></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="3304"/></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="233"/></proof>
<proof prover="2"><result status="valid" time="0.63" steps="231"/></proof>
</goal>
</transf>
</goal>
......
......@@ -3,9 +3,9 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../flag.mlw" expanded="true">
<theory name="Flag" sum="356f2a9a7cb8ab27eb11b3eeda262a24" expanded="true">
<goal name="VC dutch_flag" expl="VC for dutch_flag" expanded="true">
<file name="../flag.mlw" proved="true">
<theory name="Flag" proved="true" sum="81c5d40a4619f95c6530c5b4c048eb78">
<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>
</theory>
......
......@@ -4,56 +4,56 @@
<why3session shape_version="4">
<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" expanded="true">
<theory name="GnomeSort" sum="e0230b8d892afe35879c5b8724baa6db" expanded="true">
<goal name="VC gnome_sort" expl="VC for gnome_sort" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="VC gnome_sort.1" expl="loop invariant init">
<file name="../gnome_sort.mlw" proved="true">
<theory name="GnomeSort" proved="true" sum="197e7e26e8ad6469a200f513fa22cbc1">
<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">
<proof prover="0"><result status="valid" time="0.01" steps="2"/></proof>
</goal>
<goal name="VC gnome_sort.2" expl="loop invariant init">
<goal name="VC gnome_sort.1" expl="loop invariant init" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="5"/></proof>
</goal>
<goal name="VC gnome_sort.3" expl="loop invariant init">
<goal name="VC gnome_sort.2" expl="loop invariant init" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="7"/></proof>
</goal>
<goal name="VC gnome_sort.4" expl="index in array bounds">
<goal name="VC gnome_sort.3" expl="index in array bounds" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="VC gnome_sort.5" expl="index in array bounds">
<goal name="VC gnome_sort.4" expl="index in array bounds" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="VC gnome_sort.6" expl="loop variant decrease">
<goal name="VC gnome_sort.5" expl="loop variant decrease" proved="true">
<proof prover="2"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="VC gnome_sort.7" expl="loop invariant preservation">
<goal name="VC gnome_sort.6" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="VC gnome_sort.8" expl="loop invariant preservation">
<goal name="VC gnome_sort.7" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="43"/></proof>
</goal>
<goal name="VC gnome_sort.9" expl="loop invariant preservation">
<goal name="VC gnome_sort.8" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
<goal name="VC gnome_sort.10" expl="precondition">
<goal name="VC gnome_sort.9" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
<goal name="VC gnome_sort.11" expl="loop variant decrease">
<goal name="VC gnome_sort.10" expl="loop variant decrease" proved="true">
<proof prover="2"><result status="valid" time="0.13"/></proof>
</goal>
<goal name="VC gnome_sort.12" expl="loop invariant preservation">
<goal name="VC gnome_sort.11" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
<goal name="VC gnome_sort.13" expl="loop invariant preservation">
<goal name="VC gnome_sort.12" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="71"/></proof>
</goal>
<goal name="VC gnome_sort.14" expl="loop invariant preservation">
<goal name="VC gnome_sort.13" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.05" steps="89"/></proof>
</goal>
<goal name="VC gnome_sort.15" expl="postcondition">
<goal name="VC gnome_sort.14" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="VC gnome_sort.16" expl="postcondition">
<goal name="VC gnome_sort.15" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
</transf>
......
......@@ -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="315462109a8ecc6d9bc049e7716915e9">
<theory name="InsertionSort" proved="true" sum="7d409220b2aeb21118af4d3b09cba578">
<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="a91128def340846b1a5bc01ebff316d6">
<theory name="InsertionSortGen" proved="true" sum="c44c33bed0cc21d37f76c87132b82598">
<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="4e423f542edf8b4716ba739641a77f34">
<theory name="InsertionSortNaive" proved="true" sum="b9aa096dcd0d721dfeccdd534f6c1c12">
<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="aa82e9edb909009a6daf254fa7318350">
<theory name="InsertionSortNaiveGen" proved="true" sum="992b2ef93d578f098eb2a65814b04d54">
<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="2e9a54a9b22898b1a45ab86283be7029">
<theory name="InsertionSortParam" proved="true" sum="cbddda87c83323308437a7867449f3ed">
<goal name="VC sort" expl="VC for sort" proved="true">
<proof prover="2"><result status="valid" time="0.90" steps="1608"/></proof>
<proof prover="2"><result status="valid" time="0.90" steps="1594"/></proof>
</goal>
</theory>
<theory name="InsertionSortParamBad" proved="true" sum="a59368e9540111f015bbcdc1980230c9">
<theory name="InsertionSortParamBad" proved="true" sum="633f1ddfe611df9e201244bc22fd5263">
<goal name="VC sort" expl="VC for sort" proved="true">
<proof prover="2"><result status="valid" time="1.19" steps="2722"/></proof>
</goal>
......
......@@ -8,7 +8,7 @@
<file name="../mergesort_array.mlw" proved="true">
<theory name="Elt" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="Merge" proved="true" sum="405999e81e8fd2ec57ffdf9de058895f">
<theory name="Merge" proved="true" sum="146d2a64eeeaa96ce62aef3a38036bea">
<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">
......@@ -192,7 +192,7 @@
</transf>
</goal>
</theory>
<theory name="TopDownMergesort" proved="true" sum="814f5716e1d1790163ddb43664bc5dd1">
<theory name="TopDownMergesort" proved="true" sum="0f1686f4a454d13d52a3eea1f4294399">
<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="c82da4b23e3d491b8ae741f95f2100c1">
<theory name="BottomUpMergesort" proved="true" sum="154dad8af7aaa25cf87af0e6ec0b6008">
<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="e5582422d8dba3b12c1e7dd54599bdf5">
<theory name="NaturalMergesort" proved="true" sum="7debbd642dc6403cfdaec0417d1bb072">
<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>
......
......@@ -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="3bc1bf4601f28ddf521d7f3f5a3bacb7">
<theory name="Quicksort" proved="true" sum="321000cd00824b2485c3775a40ff00bb">
<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">
......@@ -77,7 +77,7 @@
<proof prover="0"><result status="valid" time="0.01" steps="18"/></proof>
</goal>
<goal name="VC quick_rec.23" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.28" steps="504"/></proof>
<proof prover="0"><result status="valid" time="0.28" steps="500"/></proof>
</goal>
<goal name="VC quick_rec.24" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.04" steps="188"/></proof>
......@@ -103,17 +103,17 @@
<proof prover="0"><result status="valid" time="0.01" steps="22"/></proof>
</goal>
</theory>
<theory name="Shuffle" proved="true" sum="f9ccbfe5351a6469576b3b7242ebcaaf">
<theory name="Shuffle" proved="true" sum="19b4857176adc4db08e01024cc3ea008">
<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="99534a12f4896fd6b91f30aa9e128637">
<theory name="QuicksortWithShuffle" proved="true" sum="38c5b42f33402b0225aa19f01696a951">
<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="6406f882c1cf4cbf1443c79b8c0503a3">
<theory name="Quicksort3way" proved="true" sum="ccd3f3c2ac98ab6d48e74f59d1cf16aa">
<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="2e9c0dbef61ba1079beaaec580ec4725">
<theory name="Test" proved="true" sum="f2d52e24d82ae2590365860ce75c2cb7">
<goal name="VC test1" expl="VC for test1" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="11"/></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="65e77a0b278639c5ed7c6698eb79d8d4">
<theory name="SelectionSort" proved="true" sum="593dd0918071994ab834b2bacbd6ace5">
<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">
......
......@@ -27,7 +27,7 @@
<proof prover="1"><result status="valid" time="0.02" steps="144"/></proof>
</goal>
</theory>
<theory name="HeapSort" proved="true" sum="6522ddf446f64a8e33c5d7c7d330f011">
<theory name="HeapSort" proved="true" sum="87a90c3b66ea1a3aae90ddb93dcfe7aa">
<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">
......
......@@ -5,8 +5,8 @@
<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.01" timelimit="6" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="Coq" version="8.6.1" timelimit="6" steplimit="0" memlimit="1000"/>
<prover id="4" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="5" name="Coq" version="8.7.1" timelimit="6" steplimit="0" memlimit="1000"/>
<prover id="6" name="Z3" version="4.5.0" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../../../stdlib/array.mlw" proved="true">
<theory name="Array" proved="true" sum="d12f98c64e888261d80af67de4830724">
......@@ -39,12 +39,12 @@
</theory>
<theory name="ArrayExchange" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="ArrayPermut" proved="true" sum="a6458b840741a86432e42458b770b11f">
<theory name="ArrayPermut" proved="true" sum="01b98addf0f2beb2040296aa46c603dc">
<goal name="exchange_permut_sub" proved="true">
<proof prover="3" edited="array_ArrayPermut_exchange_permut_sub_1.v"><result status="valid" time="1.57"/></proof>
<proof prover="5" edited="array_ArrayPermut_exchange_permut_sub_1.v"><result status="valid" time="1.57"/></proof>
</goal>
<goal name="permut_sub_weakening" proved="true">
<proof prover="3" edited="array_ArrayPermut_permut_sub_weakening_2.v"><result status="valid" time="0.51"/></proof>
<proof prover="5" edited="array_ArrayPermut_permut_sub_weakening_2.v"><result status="valid" time="0.51"/></proof>
</goal>
<goal name="exchange_permut_all" proved="true">
<proof prover="4"><result status="valid" time="0.06"/></proof>
......
......@@ -5,7 +5,7 @@
<prover id="0" name="Z3" version="4.5.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../vacid_0_sparse_array.mlw" proved="true">
<theory name="SparseArray" proved="true" sum="0ea603bec8f3354a3404298d888f944a">
<theory name="SparseArray" proved="true" sum="60ccbaf5dec152eecaed98dea25eb2b2">
<goal name="VC sparse_array" expl="VC for sparse_array" proved="true">
<proof prover="2"><result status="valid" time="0.00" steps="9"/></proof>
</goal>
......@@ -52,10 +52,10 @@
<proof prover="2"><result status="valid" time="0.02" steps="63"/></proof>
</goal>
<goal name="VC set.6" expl="type invariant" proved="true">
<proof prover="2"><result status="valid" time="1.92" steps="2981"/></proof>
<proof prover="2"><result status="valid" time="1.92" steps="2729"/></proof>
</goal>
<goal name="VC set.7" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="1.46" steps="2000"/></proof>
<proof prover="2"><result status="valid" time="1.46" steps="1965"/></proof>
</goal>
<goal name="VC set.8" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.06" steps="111"/></proof>
......@@ -63,7 +63,7 @@
</transf>
</goal>
</theory>
<theory name="Harness" proved="true" sum="c10828e8105c26fcbea7fd4e3eff95c9">
<theory name="Harness" proved="true" sum="d41f7672e26afb7bd16a2bc3f63221e7">
<goal name="VC default" expl="VC for default" proved="true">
<proof prover="2"><result status="valid" time="0.01" steps="1"/></proof>
</goal>
......@@ -74,7 +74,7 @@
<proof prover="2"><result status="valid" time="0.00" steps="1"/></proof>
</goal>
<goal name="VC harness" expl="VC for harness" proved="true">
<proof prover="2"><result status="valid" time="0.61" steps="2047"/></proof>
<proof prover="2"><result status="valid" time="0.61" steps="2244"/></proof>
</goal>
<goal name="VC bench" expl="VC for bench" proved="true">
<proof prover="2"><result status="valid" time="0.02" steps="172"/></proof>
......
......@@ -6,7 +6,7 @@
<prover id="2" name="Z3" version="4.4.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../verifythis_2017_pair_insertion_sort.mlw" proved="true">
<theory name="Challenge1" proved="true" sum="d92f05561835685a059df447195af1f6">
<theory name="Challenge1" proved="true" sum="8f518787c3955bb0492bff101300c191">
<goal name="VC pair_insertion_sort" expl="VC for pair_insertion_sort" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="VC pair_insertion_sort.0" expl="loop invariant init" proved="true">
......@@ -135,7 +135,7 @@
<proof prover="0"><result status="valid" time="0.02" steps="114"/></proof>
</goal>
<goal name="VC pair_insertion_sort.41" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="1.53" steps="1298"/></proof>
<proof prover="0"><result status="valid" time="0.54" steps="378"/></proof>
</goal>
<goal name="VC pair_insertion_sort.42" expl="index in array bounds" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="20"/></proof>
......@@ -266,7 +266,7 @@
<proof prover="0"><result status="valid" time="0.04" steps="155"/></proof>
</goal>
<goal name="VC pair_insertion_sort.84" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.56" steps="430"/></proof>
<proof prover="0"><result status="valid" time="0.75" steps="430"/></proof>
</goal>
<goal name="VC pair_insertion_sort.85" expl="index in array bounds" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="19"/></proof>
......
......@@ -41,7 +41,7 @@
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
</theory>
<theory name="SuffixSort" proved="true" sum="88f1e523c780e8550e1ad0c8c1d7b3ce">
<theory name="SuffixSort" proved="true" sum="5fcd59f8d4b64106db72a10e08cfed53">
<goal name="VC compare" expl="VC for compare" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="VC compare.0" expl="precondition" proved="true">
......@@ -151,7 +151,7 @@
<proof prover="2"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="VC sort.22" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.09"/></proof>
<proof prover="2"><result status="valid" time="0.20"/></proof>
</goal>
<goal name="VC sort.23" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.51" steps="615"/></proof>
......@@ -183,12 +183,12 @@
</transf>
</goal>
</theory>
<theory name="SuffixSort_test" proved="true" sum="daef7c8e6a363d4fa25db3f4a9adec19">
<theory name="SuffixSort_test" proved="true" sum="f6f5f741b9dc130f0a8607a040d91544">
<goal name="VC bench" expl="VC for bench" proved="true">
<proof prover="2"><result status="valid" time="0.34"/></proof>
</goal>
</theory>
<theory name="SuffixArray" proved="true" sum="a9e9a5e332dedfbe15479a4d99b0e324">
<theory name="SuffixArray" proved="true" sum="d73eab9d245382d053b90a74ab35cd99">
<goal name="VC suffixArray" expl="VC for suffixArray" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
......@@ -249,12 +249,12 @@
</transf>
</goal>
</theory>
<theory name="SuffixArray_test" proved="true" sum="78ab0127c0cbd10e30c446b3435a219f">
<theory name="SuffixArray_test" proved="true" sum="52a99b42cbb4456b3b8a7b0a2ade66a8">
<goal name="VC bench" expl="VC for bench" proved="true">
<proof prover="2"><result status="valid" time="0.05"/></proof>
</goal>
</theory>
<theory name="LRS" proved="true" sum="f31032dd455fa74477360f342ab726a4">
<theory name="LRS" proved="true" sum="ad81d082c2eb896c12f7884767d18a30">
<goal name="lcp_sym" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="33"/></proof>
</goal>
......@@ -297,7 +297,7 @@
<proof prover="2"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="VC lrs.10" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.20"/></proof>
<proof prover="2"><result status="valid" time="0.34"/></proof>
</goal>
<goal name="VC lrs.11" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.03"/></proof>
......@@ -309,7 +309,7 @@
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC lrs.14" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.19"/></proof>
<proof prover="2"><result status="valid" time="0.36"/></proof>
</goal>
<goal name="VC lrs.15" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="0.08"/></proof>
......@@ -362,7 +362,7 @@
</transf>
</goal>
</theory>
<theory name="LRS_test" proved="true" sum="4ab50b53ed3df0308fc01d271ab8fd26">
<theory name="LRS_test" proved="true" sum="5db99886d40b2a0b6d95a589412a35d5">
<goal name="VC bench" expl="VC for bench" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
......
......@@ -2,13 +2,13 @@
<!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.7.1" timelimit="5" steplimit="0" memlimit="4000"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="20" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="1.30" timelimit="20" steplimit="0" memlimit="0"/>
<prover id="4" name="CVC4" version="1.4" timelimit="30" steplimit="0" memlimit="1000"/>
<prover id="5" name="Z3" version="4.3.2" timelimit="30" steplimit="0" memlimit="1000"/>
<prover id="6" name="Coq" version="8.6.1" timelimit="5" steplimit="0" memlimit="4000"/>
<file name="../vstte10_inverting.mlw" proved="true">
<theory name="InvertingAnInjection" proved="true" sum="8b7fd916422a55e4335d0eb82e4c640d">
<theory name="InvertingAnInjection" proved="true" sum="bc3c6864f19951cbc0f2a0c5cd9476dd">
<goal name="VC inverting" expl="VC for inverting" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="VC inverting.0" expl="loop invariant init" proved="true">
......@@ -24,7 +24,7 @@
<proof prover="1" memlimit="0"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="VC inverting.4" expl="postcondition" proved="true">
<proof prover="6" edited="vstte10_inverting_WP_InvertingAnInjection_WP_parameter_inverting_1.v"><result status="valid" time="0.34"/></proof>
<proof prover="0" edited="vstte10_inverting_WP_InvertingAnInjection_WP_parameter_inverting_1.v"><result status="valid" time="0.34"/></proof>
</goal>
<goal name="VC inverting.5" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.00" steps="11"/></proof>
......@@ -54,7 +54,7 @@
<proof prover="2" timelimit="10"><result status="valid" time="0.00" steps="7"/></proof>
</goal>
<goal name="VC inverting2.5.1" expl="VC for inverting2" proved="true">
<proof prover="6" memlimit="1000" edited="vstte10_inverting_InvertingAnInjection_VC_inverting2_1.v"><result status="valid" time="0.39"/></proof>
<proof prover="0" memlimit="1000" edited="vstte10_inverting_InvertingAnInjection_VC_inverting2_1.v"><result status="valid" time="0.39"/></proof>
</goal>
<goal name="VC inverting2.5.2" expl="VC for inverting2" proved="true">
<proof prover="1" timelimit="30"><result status="valid" time="0.01"/></proof>
......@@ -70,7 +70,7 @@
</transf>
</goal>
</theory>
<theory name="Test" proved="true" sum="d971fbbbccb0cd37522be3ccfa26f33e">
<theory name="Test" proved="true" sum="3ab5ea7f5be85dc04cc10c7a598a0d9a">
<goal name="VC test" expl="VC for test" proved="true">
<transf name="split_goal_wp" proved="true" >