Commit e27ff68e authored by Sylvain Dailler's avatar Sylvain Dailler

Update obsolete session

parent 8a19e02e
......@@ -300,7 +300,7 @@
<proof prover="5"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="VC proof1.6.2" expl="VC for proof1" proved="true">
<proof prover="4"><result status="valid" time="1.32"/></proof>
<proof prover="4"><result status="valid" time="1.00"/></proof>
<proof prover="6"><result status="valid" time="0.04" steps="96"/></proof>
</goal>
</transf>
......
......@@ -269,7 +269,7 @@
<proof prover="12"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC poke.5" expl="postcondition" proved="true">
<proof prover="12"><result status="valid" time="0.01"/></proof>
<proof prover="12"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC poke.6" expl="postcondition" proved="true">
<proof prover="12"><result status="valid" time="0.02"/></proof>
......@@ -284,7 +284,7 @@
<proof prover="12"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC poke.10" expl="postcondition" proved="true">
<proof prover="12"><result status="valid" time="0.02"/></proof>
<proof prover="12"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC poke.11" expl="precondition" proved="true">
<proof prover="12"><result status="valid" time="0.04"/></proof>
......@@ -293,13 +293,13 @@
<proof prover="12"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC poke.13" expl="loop invariant init" proved="true">
<proof prover="12"><result status="valid" time="0.02"/></proof>
<proof prover="12"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC poke.14" expl="loop invariant init" proved="true">
<proof prover="12"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC poke.15" expl="loop invariant init" proved="true">
<proof prover="12"><result status="valid" time="0.01"/></proof>
<proof prover="12"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC poke.16" expl="precondition" proved="true">
<proof prover="12"><result status="valid" time="0.03"/></proof>
......
......@@ -77,7 +77,7 @@
<proof prover="0"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC counting_sort.21" expl="loop invariant preservation" proved="true">
<proof prover="0" timelimit="10" memlimit="4000"><result status="valid" time="0.86"/></proof>
<proof prover="0" timelimit="10" memlimit="4000"><result status="valid" time="1.12"/></proof>
</goal>
<goal name="VC counting_sort.22" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.10" steps="204"/></proof>
......@@ -179,7 +179,7 @@
<proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC in_place_counting_sort.22" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.38"/></proof>
<proof prover="0"><result status="valid" time="0.53"/></proof>
</goal>
<goal name="VC in_place_counting_sort.23" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.13" steps="234"/></proof>
......
......@@ -16,13 +16,13 @@
<proof prover="7"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC relax.1" expl="postcondition" proved="true">
<proof prover="7"><result status="valid" time="0.04"/></proof>
<proof prover="7"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC relax.2" expl="postcondition" proved="true">
<proof prover="7"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC relax.3" expl="postcondition" proved="true">
<proof prover="7"><result status="valid" time="0.01"/></proof>
<proof prover="7"><result status="valid" time="0.04"/></proof>
</goal>
</transf>
</goal>
......@@ -108,7 +108,7 @@
<proof prover="7"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC shortest_path_code.6" expl="loop invariant init" proved="true">
<proof prover="2"><result status="valid" time="2.45"/></proof>
<proof prover="2"><result status="valid" time="3.78"/></proof>
<proof prover="5"><result status="valid" time="1.46"/></proof>
</goal>
<goal name="VC shortest_path_code.7" expl="loop invariant init" proved="true">
......
......@@ -157,7 +157,7 @@
</transf>
</goal>
<goal name="VC two_equal_elements.33" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.70"/></proof>
<proof prover="0"><result status="valid" time="0.50"/></proof>
</goal>
<goal name="VC two_equal_elements.34" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.04"/></proof>
......
......@@ -19,10 +19,10 @@
<goal name="size_left.0" proved="true">
<transf name="destruct_alg" proved="true" arg1="t">
<goal name="size_left.0.0" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="size_left.0.1" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
......
......@@ -380,7 +380,7 @@
<proof prover="3"><result status="valid" time="0.50"/></proof>
</goal>
<goal name="VC isqrt64.22" expl="loop invariant preservation" proved="true">
<proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="2.06"/></proof>
<proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="2.42"/></proof>
</goal>
<goal name="VC isqrt64.23" expl="loop invariant preservation" proved="true">
<proof prover="3" timelimit="60"><result status="valid" time="1.70"/></proof>
......@@ -401,7 +401,7 @@
<goal name="VC isqrt64.27.0.0" expl="loop invariant preservation" proved="true">
<transf name="rewrite" proved="true" arg1="sqr_add2">
<goal name="VC isqrt64.27.0.0.0" expl="loop invariant preservation" proved="true">
<proof prover="3" timelimit="30"><result status="valid" time="5.15"/></proof>
<proof prover="3" timelimit="30"><result status="valid" time="5.80"/></proof>
</goal>
</transf>
</goal>
......@@ -611,7 +611,7 @@
</transf>
</goal>
<goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0.1.1.1.0.0.1.0.0.1" expl="rewrite premises" proved="true">
<proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="1.85"/></proof>
<proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="2.24"/></proof>
</goal>
</transf>
</goal>
......@@ -650,7 +650,7 @@
</transf>
</goal>
<goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0.1.1.1.0.0.1.0.1.0.0.1.0.0.0.0.1" expl="rewrite premises" proved="true">
<proof prover="3" timelimit="5"><result status="valid" time="1.90"/></proof>
<proof prover="3" timelimit="5"><result status="valid" time="2.34"/></proof>
</goal>
</transf>
</goal>
......@@ -674,12 +674,12 @@
</transf>
</goal>
<goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0.1.1.1.0.0.1.0.1.0.1" expl="rewrite premises" proved="true">
<proof prover="3" timelimit="5"><result status="valid" time="1.20"/></proof>
<proof prover="3" timelimit="5"><result status="valid" time="1.47"/></proof>
</goal>
</transf>
</goal>
<goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0.1.1.1.0.0.1.0.1.1" expl="rewrite premises" proved="true">
<proof prover="3" timelimit="5"><result status="valid" time="1.84"/></proof>
<proof prover="3" timelimit="5"><result status="valid" time="2.16"/></proof>
</goal>
</transf>
</goal>
......
......@@ -549,7 +549,7 @@
<proof prover="4"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC enum.2" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="8"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="21"/></proof>
<proof prover="4"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC enum.3" expl="postcondition" proved="true">
......
......@@ -487,7 +487,7 @@
<proof prover="6"><result status="valid" time="0.02" steps="34"/></proof>
</goal>
<goal name="VC delete.42" expl="postcondition" proved="true">
<proof prover="6"><result status="valid" time="0.01" steps="1"/></proof>
<proof prover="6"><result status="valid" time="0.01" steps="14"/></proof>
</goal>
<goal name="VC delete.43" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.13"/></proof>
......
......@@ -378,7 +378,7 @@
</goal>
<goal name="VC list_seg_no_repet.9" expl="assertion" proved="true">
<proof prover="2" timelimit="10"><result status="valid" time="1.27"/></proof>
<proof prover="4"><result status="valid" time="9.06"/></proof>
<proof prover="4"><result status="valid" time="6.63"/></proof>
</goal>
<goal name="VC list_seg_no_repet.10" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.20"/></proof>
......
......@@ -32,7 +32,7 @@
</goal>
<goal name="VC maximum.4.1" expl="VC for maximum" proved="true">
<transf name="right" proved="true" >
<goal name="VC maximum.4.1.0" expl="VC for maximum" proved="true">
<goal name="VC maximum.4.1.0" expl="right case" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC maximum.4.1.0.0" expl="VC for maximum" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof>
......
......@@ -28,7 +28,7 @@
<proof prover="0"><result status="valid" time="0.00" steps="14"/></proof>
</goal>
<goal name="VC merge.6" expl="loop invariant init" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
<proof prover="0"><result status="valid" time="0.00" steps="13"/></proof>
</goal>
<goal name="VC merge.7" expl="index in array bounds" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="20"/></proof>
......@@ -145,7 +145,7 @@
<proof prover="0"><result status="valid" time="0.01" steps="14"/></proof>
</goal>
<goal name="VC merge_using.5" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
<proof prover="0"><result status="valid" time="0.01" steps="13"/></proof>
</goal>
<goal name="VC merge_using.6" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="11"/></proof>
......@@ -185,7 +185,7 @@
<proof prover="0"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
<goal name="VC merge_using.17" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="1"/></proof>
<proof prover="0"><result status="valid" time="0.00" steps="10"/></proof>
</goal>
</transf>
</goal>
......@@ -514,7 +514,7 @@
<proof prover="0"><result status="valid" time="0.01" steps="13"/></proof>
</goal>
<goal name="VC naturalrec.3" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="1"/></proof>
<proof prover="0"><result status="valid" time="0.00" steps="10"/></proof>
</goal>
<goal name="VC naturalrec.4" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="6"/></proof>
......@@ -529,7 +529,7 @@
<proof prover="0"><result status="valid" time="0.01" steps="17"/></proof>
</goal>
<goal name="VC naturalrec.8" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
<proof prover="0"><result status="valid" time="0.01" steps="14"/></proof>
</goal>
<goal name="VC naturalrec.9" expl="loop invariant init" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="12"/></proof>
......@@ -541,7 +541,7 @@
<proof prover="0"><result status="valid" time="0.01" steps="20"/></proof>
</goal>
<goal name="VC naturalrec.12" expl="loop invariant init" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
<proof prover="0"><result status="valid" time="0.00" steps="17"/></proof>
</goal>
<goal name="VC naturalrec.13" expl="variant decrease" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="20"/></proof>
......
......@@ -747,7 +747,7 @@
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC wmpn_add_in_place.4" expl="loop invariant init" proved="true">
<proof prover="5" timelimit="5" memlimit="2000"><result status="valid" time="0.03" steps="9"/></proof>
<proof prover="5" timelimit="5" memlimit="2000"><result status="valid" time="0.03" steps="18"/></proof>
</goal>
<goal name="VC wmpn_add_in_place.5" expl="precondition" proved="true">
<transf name="split_goal_right" proved="true" >
......@@ -1264,7 +1264,7 @@
<proof prover="5"><result status="valid" time="0.04" steps="56"/></proof>
</goal>
<goal name="VC wmpn_incr_1.18" expl="integer overflow" proved="true">
<proof prover="3"><result status="valid" time="0.32"/></proof>
<proof prover="3"><result status="valid" time="0.26"/></proof>
</goal>
<goal name="VC wmpn_incr_1.19" expl="assertion" proved="true">
<transf name="split_vc" proved="true" >
......@@ -1286,7 +1286,7 @@
</transf>
</goal>
<goal name="VC wmpn_incr_1.20" expl="loop variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC wmpn_incr_1.21" expl="loop invariant preservation" proved="true">
<proof prover="5"><result status="valid" time="0.07" steps="122"/></proof>
......@@ -1295,16 +1295,16 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC wmpn_incr_1.23" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC wmpn_incr_1.24" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC wmpn_incr_1.25" expl="loop invariant preservation" proved="true">
<proof prover="5"><result status="valid" time="0.02" steps="51"/></proof>
<proof prover="5"><result status="valid" time="0.05" steps="51"/></proof>
</goal>
<goal name="VC wmpn_incr_1.26" expl="loop invariant preservation" proved="true">
<proof prover="5"><result status="valid" time="0.02" steps="67"/></proof>
<proof prover="5"><result status="valid" time="0.04" steps="67"/></proof>
</goal>
<goal name="VC wmpn_incr_1.27" expl="loop invariant preservation" proved="true">
<proof prover="5"><result status="valid" time="0.07" steps="70"/></proof>
......@@ -1337,7 +1337,7 @@
<proof prover="5"><result status="valid" time="0.03" steps="44"/></proof>
</goal>
<goal name="VC wmpn_incr_1.37" expl="integer overflow" proved="true">
<proof prover="3"><result status="valid" time="0.26"/></proof>
<proof prover="3"><result status="valid" time="0.32"/></proof>
</goal>
<goal name="VC wmpn_incr_1.38" expl="assertion" proved="true">
<transf name="split_vc" proved="true" >
......@@ -1354,12 +1354,12 @@
<proof prover="5" timelimit="5"><result status="valid" time="0.02" steps="49"/></proof>
</goal>
<goal name="VC wmpn_incr_1.38.4" expl="VC for wmpn_incr_1" proved="true">
<proof prover="5" timelimit="5"><result status="valid" time="0.03" steps="51"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.02" steps="51"/></proof>
</goal>
</transf>
</goal>
<goal name="VC wmpn_incr_1.39" expl="loop variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC wmpn_incr_1.40" expl="loop invariant preservation" proved="true">
<proof prover="5"><result status="valid" time="0.06" steps="122"/></proof>
......@@ -1368,16 +1368,16 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC wmpn_incr_1.42" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC wmpn_incr_1.43" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC wmpn_incr_1.44" expl="loop invariant preservation" proved="true">
<proof prover="5"><result status="valid" time="0.05" steps="51"/></proof>
<proof prover="5"><result status="valid" time="0.02" steps="51"/></proof>
</goal>
<goal name="VC wmpn_incr_1.45" expl="loop invariant preservation" proved="true">
<proof prover="5"><result status="valid" time="0.04" steps="67"/></proof>
<proof prover="5"><result status="valid" time="0.02" steps="67"/></proof>
</goal>
<goal name="VC wmpn_incr_1.46" expl="loop invariant preservation" proved="true">
<proof prover="5"><result status="valid" time="0.03" steps="70"/></proof>
......
......@@ -1110,7 +1110,7 @@
<proof prover="2"><result status="valid" time="0.14"/></proof>
</goal>
<goal name="VC wmpn_lshift_in_place.40.0.0.22" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.18"/></proof>
<proof prover="2"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="VC wmpn_lshift_in_place.40.0.0.23" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.16"/></proof>
......@@ -1128,7 +1128,7 @@
<proof prover="2"><result status="valid" time="0.13"/></proof>
</goal>
<goal name="VC wmpn_lshift_in_place.40.0.0.28" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.21"/></proof>
<proof prover="2"><result status="valid" time="0.14"/></proof>
</goal>
<goal name="VC wmpn_lshift_in_place.40.0.0.29" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.15"/></proof>
......@@ -1176,7 +1176,7 @@
<proof prover="2"><result status="valid" time="0.16"/></proof>
</goal>
<goal name="VC wmpn_lshift_in_place.40.0.0.44" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.14"/></proof>
<proof prover="2"><result status="valid" time="0.21"/></proof>
</goal>
<goal name="VC wmpn_lshift_in_place.40.0.0.45" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.14"/></proof>
......@@ -1221,7 +1221,7 @@
<proof prover="2"><result status="valid" time="0.20"/></proof>
</goal>
<goal name="VC wmpn_lshift_in_place.40.0.0.59" expl="apply premises" proved="true">