Commit 28c19c22 authored by DAILLER Sylvain's avatar DAILLER Sylvain

245 theories

parent 19bd2368
......@@ -137,7 +137,7 @@
<goal name="VC inv_height" expl="VC for inv_height" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC inv_height.0" expl="assertion" proved="true">
<proof prover="2" timelimit="5"><result status="valid" time="0.07" steps="455"/></proof>
<proof prover="2" timelimit="5"><result status="valid" time="0.18" steps="455"/></proof>
</goal>
<goal name="VC inv_height.1" expl="variant decrease" proved="true">
<proof prover="2" timelimit="5"><result status="valid" time="0.01" steps="35"/></proof>
......
......@@ -923,7 +923,7 @@
<proof prover="5" timelimit="5" memlimit="2000"><result status="valid" time="0.32" steps="62"/></proof>
</goal>
<goal name="VC wmpn_add_in_place.46" expl="postcondition" proved="true">
<proof prover="5" timelimit="5" memlimit="2000"><result status="valid" time="0.27" steps="113"/></proof>
<proof prover="5" timelimit="5" memlimit="2000"><result status="valid" time="0.27" steps="112"/></proof>
</goal>
<goal name="VC wmpn_add_in_place.47" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
......@@ -1005,7 +1005,7 @@
<proof prover="5" timelimit="5" memlimit="2000"><result status="valid" time="0.02" steps="27"/></proof>
</goal>
<goal name="VC wmpn_add_in_place.69" expl="postcondition" proved="true">
<proof prover="5"><result status="valid" time="0.04" steps="69"/></proof>
<proof prover="5"><result status="valid" time="0.04" steps="68"/></proof>
</goal>
<goal name="VC wmpn_add_in_place.70" expl="postcondition" proved="true">
<proof prover="5" timelimit="5" memlimit="2000"><result status="valid" time="0.04" steps="29"/></proof>
......@@ -1281,30 +1281,30 @@
<proof prover="5" timelimit="5"><result status="valid" time="0.02" steps="48"/></proof>
</goal>
<goal name="VC wmpn_incr_1.19.4" expl="VC for wmpn_incr_1" proved="true">
<proof prover="5" timelimit="5"><result status="valid" time="0.19" steps="173"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.19" steps="176"/></proof>
</goal>
</transf>
</goal>
<goal name="VC wmpn_incr_1.20" 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.21" expl="loop invariant preservation" proved="true">
<proof prover="5"><result status="valid" time="0.07" steps="122"/></proof>
<proof prover="5"><result status="valid" time="0.06" steps="122"/></proof>
</goal>
<goal name="VC wmpn_incr_1.22" expl="loop invariant preservation" proved="true">
<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.05" steps="51"/></proof>
<proof prover="5"><result status="valid" time="0.02" 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.03" steps="70"/></proof>
......@@ -1359,25 +1359,25 @@
</transf>
</goal>
<goal name="VC wmpn_incr_1.39" 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.40" expl="loop invariant preservation" proved="true">
<proof prover="5"><result status="valid" time="0.06" steps="122"/></proof>
<proof prover="5"><result status="valid" time="0.07" steps="122"/></proof>
</goal>
<goal name="VC wmpn_incr_1.41" expl="loop invariant preservation" proved="true">
<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.02" steps="51"/></proof>
<proof prover="5"><result status="valid" time="0.05" 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.07" steps="70"/></proof>
......@@ -1559,7 +1559,7 @@
<proof prover="2"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="VC wmpn_add_1_in_place.47" expl="postcondition" proved="true">
<proof prover="5"><result status="valid" time="0.26" steps="126"/></proof>
<proof prover="5"><result status="valid" time="0.26" steps="125"/></proof>
</goal>
<goal name="VC wmpn_add_1_in_place.48" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
......
This diff is collapsed.
......@@ -122,7 +122,7 @@
<proof prover="5"><result status="valid" time="0.04" steps="9"/></proof>
</goal>
<goal name="VC value_sub_tail.2" expl="postcondition" proved="true">
<proof prover="5"><result status="valid" time="0.07" steps="39"/></proof>
<proof prover="5"><result status="valid" time="0.07" steps="42"/></proof>
</goal>
</transf>
</goal>
......@@ -238,7 +238,7 @@
<proof prover="5"><result status="valid" time="0.03" steps="11"/></proof>
</goal>
<goal name="VC value_sub_upper_bound.4" expl="postcondition" proved="true">
<proof prover="5"><result status="valid" time="0.08" steps="34"/></proof>
<proof prover="5"><result status="valid" time="0.08" steps="24"/></proof>
</goal>
</transf>
</goal>
......
......@@ -150,10 +150,10 @@
<proof prover="4" memlimit="2000"><result status="valid" time="0.00" steps="13"/></proof>
</goal>
<goal name="VC sprod.3" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="4" memlimit="2000"><result status="valid" time="0.00" steps="8"/></proof>
</goal>
<goal name="VC sprod.4" expl="exceptional postcondition" proved="true">
<proof prover="4" memlimit="2000"><result status="valid" time="0.00" steps="8"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
......@@ -1303,7 +1303,7 @@
</goal>
<goal name="VC linear_decision.17" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="4"><result status="valid" time="0.01" steps="30"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="30"/></proof>
</goal>
<goal name="VC linear_decision.18" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="74"/></proof>
......@@ -1313,24 +1313,24 @@
</goal>
<goal name="VC linear_decision.20" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="30"/></proof>
<proof prover="4"><result status="valid" time="0.01" steps="30"/></proof>
</goal>
<goal name="VC linear_decision.21" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="74"/></proof>
</goal>
<goal name="VC linear_decision.22" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="VC linear_decision.23" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="8"/></proof>
</goal>
<goal name="VC linear_decision.24" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="8"/></proof>
</goal>
<goal name="VC linear_decision.25" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="VC linear_decision.26" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
......@@ -1348,10 +1348,10 @@
<proof prover="4"><result status="valid" time="0.02" steps="88"/></proof>
</goal>
<goal name="VC linear_decision.31" expl="integer overflow" proved="true">
<proof prover="4"><result status="valid" time="0.03" steps="35"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="35"/></proof>
</goal>
<goal name="VC linear_decision.32" expl="variant decrease" proved="true">
<proof prover="4"><result status="valid" time="0.01" steps="35"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="35"/></proof>
</goal>
<goal name="VC linear_decision.33" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="86"/></proof>
......@@ -1364,12 +1364,13 @@
</goal>
<goal name="VC linear_decision.36" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="VC linear_decision.37" expl="integer overflow" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="35"/></proof>
<proof prover="4"><result status="valid" time="0.03" steps="35"/></proof>
</goal>
<goal name="VC linear_decision.38" expl="variant decrease" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="35"/></proof>
<proof prover="4"><result status="valid" time="0.01" steps="35"/></proof>
</goal>
<goal name="VC linear_decision.39" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="86"/></proof>
......@@ -1382,7 +1383,6 @@
</goal>
<goal name="VC linear_decision.42" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="VC linear_decision.43" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
......@@ -1413,16 +1413,16 @@
<proof prover="4"><result status="valid" time="0.02" steps="84"/></proof>
</goal>
<goal name="VC linear_decision.52" expl="integer overflow" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="33"/></proof>
<proof prover="4"><result status="valid" time="0.03" steps="33"/></proof>
</goal>
<goal name="VC linear_decision.53" expl="variant decrease" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="33"/></proof>
<proof prover="4"><result status="valid" time="0.01" steps="33"/></proof>
</goal>
<goal name="VC linear_decision.54" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.03" steps="82"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="82"/></proof>
</goal>
<goal name="VC linear_decision.55" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.03" steps="38"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="38"/></proof>
</goal>
<goal name="VC linear_decision.56" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="35"/></proof>
......@@ -1431,16 +1431,16 @@
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC linear_decision.58" expl="integer overflow" proved="true">
<proof prover="4"><result status="valid" time="0.03" steps="33"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="33"/></proof>
</goal>
<goal name="VC linear_decision.59" expl="variant decrease" proved="true">
<proof prover="4"><result status="valid" time="0.01" steps="33"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="33"/></proof>
</goal>
<goal name="VC linear_decision.60" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="82"/></proof>
<proof prover="4"><result status="valid" time="0.03" steps="82"/></proof>
</goal>
<goal name="VC linear_decision.61" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="38"/></proof>
<proof prover="4"><result status="valid" time="0.03" steps="38"/></proof>
</goal>
<goal name="VC linear_decision.62" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="35"/></proof>
......@@ -1498,17 +1498,17 @@
</goal>
<goal name="VC linear_decision.80" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="VC linear_decision.81" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="VC linear_decision.82" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="8"/></proof>
</goal>
<goal name="VC linear_decision.82" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="VC linear_decision.83" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="VC linear_decision.84" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
......@@ -1559,16 +1559,16 @@
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC linear_decision.99" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC linear_decision.100" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC linear_decision.101" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC linear_decision.102" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
......
......@@ -14,7 +14,7 @@
<goal name="VC pow2_64" expl="VC for pow2_64" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC pow2_64.0" expl="assertion" proved="true">
<proof prover="5"><result status="valid" time="0.03" steps="11"/></proof>
<proof prover="5"><result status="valid" time="0.03" steps="14"/></proof>
</goal>
<goal name="VC pow2_64.1" expl="assertion" proved="true">
<proof prover="5"><result status="valid" time="0.03" steps="11"/></proof>
......@@ -54,7 +54,7 @@
<goal name="VC lsld_ext.1" expl="assertion" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC lsld_ext.1.0" expl="VC for lsld_ext" proved="true">
<proof prover="2"><result status="valid" time="0.48"/></proof>
<proof prover="2"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC lsld_ext.1.1" expl="VC for lsld_ext" proved="true">
<proof prover="3" timelimit="1"><result status="valid" time="0.06"/></proof>
......@@ -878,7 +878,7 @@
<proof prover="2" timelimit="5"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="VC wmpn_lshift_in_place.6" expl="loop invariant init" proved="true">
<proof prover="1"><result status="valid" time="1.47"/></proof>
<proof prover="1"><result status="valid" time="2.33"/></proof>
</goal>
<goal name="VC wmpn_lshift_in_place.7" expl="loop invariant init" proved="true">
<proof prover="5" timelimit="1"><result status="valid" time="0.05" steps="36"/></proof>
......@@ -1089,7 +1089,7 @@
<proof prover="2"><result status="valid" time="0.21"/></proof>
</goal>
<goal name="VC wmpn_lshift_in_place.40.0.0.15" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.18"/></proof>
<proof prover="2"><result status="valid" time="0.14"/></proof>
</goal>
<goal name="VC wmpn_lshift_in_place.40.0.0.16" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.14"/></proof>
......@@ -1098,7 +1098,7 @@
<proof prover="2"><result status="valid" time="0.15"/></proof>
</goal>
<goal name="VC wmpn_lshift_in_place.40.0.0.18" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.14"/></proof>
<proof prover="2"><result status="valid" time="0.18"/></proof>
</goal>
<goal name="VC wmpn_lshift_in_place.40.0.0.19" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.18"/></proof>
......@@ -1140,10 +1140,10 @@
<proof prover="2"><result status="valid" time="0.14"/></proof>
</goal>
<goal name="VC wmpn_lshift_in_place.40.0.0.32" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.16"/></proof>
<proof prover="2"><result status="valid" time="0.15"/></proof>
</goal>
<goal name="VC wmpn_lshift_in_place.40.0.0.33" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.15"/></proof>
<proof prover="2"><result status="valid" time="0.14"/></proof>
</goal>
<goal name="VC wmpn_lshift_in_place.40.0.0.34" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.13"/></proof>
......@@ -1152,10 +1152,10 @@
<proof prover="2"><result status="valid" time="0.14"/></proof>
</goal>
<goal name="VC wmpn_lshift_in_place.40.0.0.36" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.15"/></proof>
<proof prover="2"><result status="valid" time="0.16"/></proof>
</goal>
<goal name="VC wmpn_lshift_in_place.40.0.0.37" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.14"/></proof>
<proof prover="2"><result status="valid" time="0.15"/></proof>
</goal>
<goal name="VC wmpn_lshift_in_place.40.0.0.38" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.23"/></proof>
......@@ -1370,7 +1370,7 @@
<proof prover="0"><result status="valid" time="0.18"/></proof>
</goal>
<goal name="VC wmpn_lshift_in_place.42.1" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.64"/></proof>
<proof prover="0"><result status="valid" time="0.67"/></proof>
</goal>
<goal name="VC wmpn_lshift_in_place.42.2" expl="VC for wmpn_lshift_in_place" proved="true">
<proof prover="2"><result status="valid" time="0.11"/></proof>
......
......@@ -1086,7 +1086,7 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC wmpn_mul_basecase.38.0.0.0.0.0.0.15" expl="apply premises" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC wmpn_mul_basecase.38.0.0.0.0.0.0.16" expl="apply premises" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
......@@ -1119,7 +1119,7 @@
<proof prover="2"><result status="valid" time="0.23"/></proof>
</goal>
<goal name="VC wmpn_mul_basecase.38.0.0.0.0.0.0.26" expl="apply premises" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC wmpn_mul_basecase.38.0.0.0.0.0.0.27" expl="apply premises" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
......@@ -1170,7 +1170,7 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC wmpn_mul_basecase.38.0.0.0.0.0.0.43" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.17"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC wmpn_mul_basecase.38.0.0.0.0.0.0.44" expl="apply premises" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
......@@ -1200,7 +1200,7 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC wmpn_mul_basecase.38.0.0.0.0.0.0.53" expl="apply premises" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC wmpn_mul_basecase.38.0.0.0.0.0.0.54" expl="apply premises" proved="true">
<proof prover="2"><result status="valid" time="0.23"/></proof>
......@@ -1221,7 +1221,7 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC wmpn_mul_basecase.38.0.0.0.0.0.0.60" expl="apply premises" 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_mul_basecase.38.0.0.0.0.0.0.61" expl="apply premises" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
......@@ -1233,7 +1233,7 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC wmpn_mul_basecase.38.0.0.0.0.0.0.64" expl="apply premises" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC wmpn_mul_basecase.38.0.0.0.0.0.0.65" expl="apply premises" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
......@@ -1275,7 +1275,7 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC wmpn_mul_basecase.38.0.0.0.0.0.0.78" expl="apply premises" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.17"/></proof>
</goal>
<goal name="VC wmpn_mul_basecase.38.0.0.0.0.0.0.79" expl="apply premises" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
......@@ -1287,7 +1287,7 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC wmpn_mul_basecase.38.0.0.0.0.0.0.82" expl="apply premises" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC wmpn_mul_basecase.38.0.0.0.0.0.0.83" expl="apply premises" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
......@@ -1317,7 +1317,7 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC wmpn_mul_basecase.38.0.0.0.0.0.0.92" expl="apply premises" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC wmpn_mul_basecase.38.0.0.0.0.0.0.93" expl="apply premises" proved="true">
<proof prover="3"><result status="valid" time="0.19"/></proof>
......@@ -1344,7 +1344,7 @@
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC wmpn_mul_basecase.38.0.0.0.0.0.0.101" expl="apply premises" 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_mul_basecase.38.0.0.0.0.0.0.102" expl="apply premises" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
......
......@@ -781,7 +781,7 @@
<goal name="VC wmpn_sub_in_place.15.0.0" expl="assertion" proved="true">
<transf name="reflection_f" proved="true" arg1="mp_decision">
<goal name="VC wmpn_sub_in_place.15.0.0.0" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="2.30"/></proof>
<proof prover="0"><result status="valid" time="2.64"/></proof>
</goal>
<goal name="VC wmpn_sub_in_place.15.0.0.1" proved="true">
<proof prover="3"><result status="valid" time="0.16"/></proof>
......@@ -910,7 +910,7 @@
<proof prover="2"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="VC wmpn_sub_in_place.46" expl="postcondition" proved="true">
<proof prover="5" timelimit="5" memlimit="2000"><result status="valid" time="0.32" steps="113"/></proof>
<proof prover="5" timelimit="5" memlimit="2000"><result status="valid" time="0.32" steps="112"/></proof>
</goal>
<goal name="VC wmpn_sub_in_place.47" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.07"/></proof>
......@@ -1005,7 +1005,7 @@
<proof prover="5" timelimit="5" memlimit="2000"><result status="valid" time="0.04" steps="27"/></proof>
</goal>
<goal name="VC wmpn_sub_in_place.69" expl="postcondition" proved="true">
<proof prover="5"><result status="valid" time="0.03" steps="69"/></proof>
<proof prover="5"><result status="valid" time="0.03" steps="68"/></proof>
</goal>
<goal name="VC wmpn_sub_in_place.70" expl="postcondition" proved="true">
<proof prover="5" timelimit="5" memlimit="2000"><result status="valid" time="0.02" steps="29"/></proof>
......@@ -1272,19 +1272,19 @@
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC wmpn_decr_1.17" expl="assertion" proved="true">
<proof prover="5"><result status="valid" time="0.04" steps="55"/></proof>
<proof prover="5"><result status="valid" time="0.03" steps="55"/></proof>
</goal>
<goal name="VC wmpn_decr_1.18" expl="integer overflow" proved="true">
<proof prover="3"><result status="valid" time="0.16"/></proof>
<proof prover="3"><result status="valid" time="0.20"/></proof>
</goal>
<goal name="VC wmpn_decr_1.19" expl="assertion" proved="true">
<proof prover="5"><result status="valid" time="0.45" steps="275"/></proof>
<proof prover="5"><result status="valid" time="0.45" steps="276"/></proof>
</goal>
<goal name="VC wmpn_decr_1.20" expl="loop variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC wmpn_decr_1.21" expl="loop invariant preservation" proved="true">
<proof prover="5"><result status="valid" time="0.04" steps="121"/></proof>
<proof prover="5"><result status="valid" time="0.08" steps="121"/></proof>
</goal>
<goal name="VC wmpn_decr_1.22" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
......@@ -1329,10 +1329,10 @@
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC wmpn_decr_1.36" expl="assertion" proved="true">
<proof prover="5"><result status="valid" time="0.03" steps="43"/></proof>
<proof prover="5"><result status="valid" time="0.04" steps="43"/></proof>
</goal>
<goal name="VC wmpn_decr_1.37" expl="integer overflow" proved="true">
<proof prover="3"><result status="valid" time="0.20"/></proof>
<proof prover="3"><result status="valid" time="0.16"/></proof>
</goal>
<goal name="VC wmpn_decr_1.38" expl="assertion" proved="true">
<transf name="split_vc" proved="true" >
......@@ -1360,7 +1360,7 @@
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC wmpn_decr_1.40" expl="loop invariant preservation" proved="true">
<proof prover="5"><result status="valid" time="0.08" steps="121"/></proof>
<proof prover="5"><result status="valid" time="0.04" steps="121"/></proof>
</goal>
<goal name="VC wmpn_decr_1.41" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
......@@ -1558,7 +1558,7 @@
<proof prover="2"><result status="valid" time="0.14"/></proof>
</goal>
<goal name="VC wmpn_sub_1_in_place.47" expl="postcondition" proved="true">
<proof prover="5"><result status="valid" time="0.15" steps="126"/></proof>
<proof prover="5"><result status="valid" time="0.15" steps="125"/></proof>
</goal>
<goal name="VC wmpn_sub_1_in_place.48" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
......
......@@ -43,7 +43,7 @@
<goal name="VC valuation.6" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC valuation.6.0" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="1.69"/></proof>
<proof prover="0"><result status="valid" time="4.42"/></proof>
</goal>
<goal name="VC valuation.6.1" expl="postcondition" proved="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
......@@ -134,7 +134,7 @@
<proof prover="5"><result status="valid" time="0.02" steps="25"/></proof>
</goal>
<goal name="valuation_pow.0.1" expl="recursive case" proved="true">
<proof prover="4"><result status="valid" time="0.69"/></proof>
<proof prover="4"><result status="valid" time="1.16"/></proof>
</goal>
</transf>
</goal>
......
......@@ -35,7 +35,7 @@
<goal name="VC tree_of_array_aux.6.1" expl="VC for tree_of_array_aux" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="VC tree_of_array_aux.6.1.0" expl="VC for tree_of_array_aux" proved="true">
<proof prover="2"><result status="valid" time="1.27" steps="1803"/></proof>
<proof prover="2"><result status="valid" time="1.27" steps="2103"/></proof>
</goal>
</transf>
</goal>
......@@ -56,7 +56,7 @@
<goal name="VC tree_of_array_aux.6.2.1.1" expl="false case" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="VC tree_of_array_aux.6.2.1.1.0" expl="false case" proved="true">
<proof prover="2"><result status="valid" time="1.09" steps="1079"/></proof>
<proof prover="2"><result status="valid" time="1.33" steps="1508"/></proof>
</goal>
</transf>
</goal>
......@@ -82,7 +82,7 @@
<proof prover="3"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC tree_of_array_aux.6.3.1.0.1.1" expl="false case (true case)" proved="true">
<proof prover="2" timelimit="1" memlimit="1000"><result status="valid" time="0.03" steps="93"/></proof>
<proof prover="2" timelimit="1" memlimit="1000"><result status="valid" time="0.03" steps="95"/></proof>
</goal>
</transf>
</goal>
......@@ -91,7 +91,7 @@
<goal name="VC tree_of_array_aux.6.3.1.1" expl="false case" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="VC tree_of_array_aux.6.3.1.1.0" expl="false case" proved="true">
<proof prover="2"><result status="valid" time="1.83" steps="1121"/></proof>
<proof prover="2"><result status="valid" time="1.83" steps="1104"/></proof>
</goal>
</transf>
</goal>
......
......@@ -24,7 +24,7 @@
<proof prover="4"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC tree_of_list_aux.5" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01" steps="36"/></proof>
<proof prover="3"><result status="valid" time="0.01" steps="37"/></proof>
</goal>
<goal name="VC tree_of_list_aux.6" expl="postcondition" proved="true">
<transf name="destruct_alg_subst" proved="true" arg1="l&#39;1">
......
......@@ -4,10 +4,11 @@
<why3session shape_version="5">
<prover id="0" name="CVC3" version="2.4.1" timelimit="10" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="10" steplimit="0" memlimit="1000"/>
<prover id="2" name="Z3" version="4.6.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="2" name="Z3" version="4.6.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="Z3" version="3.2" timelimit="10" steplimit="0" memlimit="1000"/>
<prover id="4" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="5" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="4000"/>
<prover id="6" name="CVC4" version="1.6" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="7" name="Z3" version="4.3.2" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../verifythis_PrefixSumRec.mlw" proved="true">
<theory name="PrefixSumRec" proved="true">
......@@ -55,9 +56,10 @@
</goal>
<goal name="VC phase1_frame.6" expl="postcondition" proved="true">
<proof prover="0" timelimit="5"><result status="valid" time="0.04"/></proof>
<transf name="remove" proved="true" arg1="real,bool,tuple0,unit,map,container,zero,one,( * ),(&lt;=),(&gt;=),abs,mod,power,get,make,is_power_of_2,Assoc,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm,Assoc1,Mul_distr_l,Mul_distr_r,Comm1,Unitary,NonTrivialRing,Refl,Trans,Antisymm,Total,ZeroLessOne,CompatOrderAdd,CompatOrderMult,Abs_le,Abs_pos,Div_mod,Div_bound,Mod_bound,Div_sign_pos,Div_sign_neg,Mod_sign_pos,Mod_sign_neg,Rounds_toward_zero,Div_1,Mod_1,Div_inf,Mod_inf,Div_mult,Mod_mult,Power_0,Power_s,Power_s_alt,Power_1,Power_sum,Power_mult,Power_comm1,Power_comm2,Power_non_neg,Power_monotonic,Sum_def_empty,Sum_def_non_empty,Sum_right_extension,Sum_transitivity,Sum_eq,array&#39;invariant,make_spec,Div_mod_2,is_power_of_2_1">
<transf name="remove" proved="true" arg1="real,bool,tuple0,unit,map,container,zero,one,( * ),(&lt;=),(&gt;=),abs,mod,power,get,set,([&lt;-]),length,([]&#39;),([&lt;-]&#39;),make,is_power_of_2,Assoc,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm,Assoc1,Mul_distr_l,Mul_distr_r,Comm1,Unitary,NonTrivialRing,Refl,Trans,Antisymm,Total,ZeroLessOne,CompatOrderAdd,CompatOrderMult,Abs_le,Abs_pos,Div_mod,Div_bound,Mod_bound,Div_sign_pos,Div_sign_neg,Mod_sign_pos,Mod_sign_neg,Rounds_toward_zero,Div_1,Mod_1,Div_inf,Mod_inf,Div_mult,Mod_mult,Power_0,Power_s,Power_s_alt,Power_1,Power_sum,Power_mult,Power_comm1,Power_comm2,Power_non_neg,Power_pos,Power_monotonic,Sum_def_empty,Sum_def_non_empty,Sum_right_extension,Sum_transitivity,Sum_eq,array&#39;invariant,([&lt;-])_spec,make_spec,Div_mod_2,is_power_of_2_1">
<goal name="VC phase1_frame.6.0" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.06"/></proof>
<proof prover="0" timelimit="1"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.07"/></proof>
</goal>
</transf>
</goal>
......@@ -94,7 +96,7 @@
<proof prover="5"><result status="valid" time="0.01" steps="7"/></proof>
</goal>
<goal name="VC phase1_frame2.6" expl="postcondition" proved="true">
<proof prover="0" timelimit="30" memlimit="4000"><result status="valid" time="4.32"/></proof>
<proof prover="0" timelimit="30" memlimit="4000"><result status="valid" time="5.23"/></proof>
<proof prover="3" timelimit="30" memlimit="4000"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
......@@ -164,7 +166,7 @@
<proof prover="0"><result status="valid" time="0.02"/></proof>