Commit f982defa authored by Raphael Rieu-Helft's avatar Raphael Rieu-Helft

Fix sessions

parent 76d0b561
......@@ -24,17 +24,17 @@
</goal>
<goal name="VC wmpn_add_1.3" expl="loop invariant init" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.04" steps="22"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.04" steps="21"/></proof>
</goal>
<goal name="VC wmpn_add_1.4" expl="loop invariant init" proved="true">
<proof prover="5" timelimit="5"><result status="valid" time="0.01" steps="24"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.01" steps="23"/></proof>
</goal>
<goal name="VC wmpn_add_1.5" expl="loop invariant init" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.04" steps="26"/></proof>
</goal>
<goal name="VC wmpn_add_1.6" expl="loop invariant init" proved="true">
<proof prover="5" timelimit="5"><result status="valid" time="0.06" steps="96"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.06" steps="94"/></proof>
</goal>
<goal name="VC wmpn_add_1.7" expl="loop invariant init" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof>
......@@ -50,7 +50,7 @@
<goal name="VC wmpn_add_1.10.0" expl="VC for wmpn_add_1" proved="true">
<transf name="introduce_premises" proved="true" >
<goal name="VC wmpn_add_1.10.0.0" expl="VC for wmpn_add_1" proved="true">
<proof prover="0"><result status="valid" time="0.36"/></proof>
<proof prover="0"><result status="valid" time="0.53"/></proof>
</goal>
</transf>
</goal>
......@@ -75,7 +75,7 @@
<proof prover="2"><result status="valid" time="0.11"/></proof>
</goal>
<goal name="VC wmpn_add_1.16" expl="assertion" proved="true">
<proof prover="5"><result status="valid" time="0.40" steps="53"/></proof>
<proof prover="5"><result status="valid" time="0.68" steps="52"/></proof>
</goal>
<goal name="VC wmpn_add_1.17" expl="loop invariant init" proved="true">
<proof prover="2"><result status="valid" time="0.08"/></proof>
......@@ -96,7 +96,7 @@
<proof prover="2"><result status="valid" time="0.11"/></proof>
</goal>
<goal name="VC wmpn_add_1.23" expl="assertion" proved="true">
<proof prover="5"><result status="valid" time="0.76" steps="201"/></proof>
<proof prover="5"><result status="valid" time="1.13" steps="197"/></proof>
</goal>
<goal name="VC wmpn_add_1.24" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
......@@ -117,14 +117,14 @@
<proof prover="2"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="VC wmpn_add_1.30" expl="loop invariant preservation" proved="true">
<proof prover="5"><result status="valid" time="0.49" steps="78"/></proof>
<proof prover="5"><result status="valid" time="0.81" steps="77"/></proof>
</goal>
<goal name="VC wmpn_add_1.31" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.11"/></proof>
<proof prover="2"><result status="valid" time="0.24"/></proof>
</goal>
<goal name="VC wmpn_add_1.32" expl="postcondition" proved="true">
<proof prover="0" memlimit="1000"><result status="valid" time="0.02"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.44" steps="63"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.82" steps="62"/></proof>
</goal>
<goal name="VC wmpn_add_1.33" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
......@@ -133,10 +133,10 @@
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC wmpn_add_1.35" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="0.11"/></proof>
<proof prover="2"><result status="valid" time="0.28"/></proof>
</goal>
<goal name="VC wmpn_add_1.36" expl="assertion" proved="true">
<proof prover="5"><result status="valid" time="0.38" steps="78"/></proof>
<proof prover="5"><result status="valid" time="0.66" steps="77"/></proof>
</goal>
<goal name="VC wmpn_add_1.37" expl="loop variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
......@@ -175,7 +175,7 @@
<proof prover="2"><result status="valid" time="0.10"/></proof>
</goal>
<goal name="VC wmpn_add_1.49" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.65"/></proof>
<proof prover="0"><result status="valid" time="0.92"/></proof>
</goal>
<goal name="VC wmpn_add_1.50" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
......@@ -196,7 +196,7 @@
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC wmpn_add_1.56" expl="loop invariant preservation" proved="true">
<proof prover="5"><result status="valid" time="0.15" steps="58"/></proof>
<proof prover="5"><result status="valid" time="0.15" steps="57"/></proof>
</goal>
<goal name="VC wmpn_add_1.57" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.10"/></proof>
......@@ -215,7 +215,7 @@
</goal>
<goal name="VC wmpn_add_1.62" expl="loop invariant init" proved="true">
<proof prover="3"><result status="valid" time="0.06"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.08" steps="20"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.08" steps="19"/></proof>
</goal>
<goal name="VC wmpn_add_1.63" expl="loop invariant init" proved="true">
<proof prover="2"><result status="valid" time="0.16"/></proof>
......@@ -225,17 +225,17 @@
</goal>
<goal name="VC wmpn_add_1.65" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.12"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.06" steps="38"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.06" steps="37"/></proof>
</goal>
<goal name="VC wmpn_add_1.66" expl="precondition" proved="true">
<proof prover="5" timelimit="5"><result status="valid" time="0.04" steps="39"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.04" steps="38"/></proof>
</goal>
<goal name="VC wmpn_add_1.67" expl="assertion" proved="true">
<proof prover="5" timelimit="5"><result status="valid" time="0.08" steps="112"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.08" steps="106"/></proof>
</goal>
<goal name="VC wmpn_add_1.68" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.05" steps="37"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.05" steps="36"/></proof>
</goal>
<goal name="VC wmpn_add_1.69" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
......@@ -253,10 +253,10 @@
<proof prover="2"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="VC wmpn_add_1.74" expl="loop invariant preservation" proved="true">
<proof prover="5"><result status="valid" time="0.04" steps="44"/></proof>
<proof prover="5"><result status="valid" time="0.04" steps="42"/></proof>
</goal>
<goal name="VC wmpn_add_1.75" expl="loop invariant preservation" proved="true">
<proof prover="5"><result status="valid" time="0.04" steps="71"/></proof>
<proof prover="5"><result status="valid" time="0.04" steps="69"/></proof>
</goal>
<goal name="VC wmpn_add_1.76" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.06"/></proof>
......@@ -274,7 +274,7 @@
<goal name="VC wmpn_add_n.0" expl="loop invariant init" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC wmpn_add_n.0.0" expl="VC for wmpn_add_n" proved="true">
<proof prover="5" timelimit="5" memlimit="2000"><result status="valid" time="0.03" steps="11"/></proof>
<proof prover="5" timelimit="5" memlimit="2000"><result status="valid" time="0.03" steps="10"/></proof>
</goal>
<goal name="VC wmpn_add_n.0.1" expl="VC for wmpn_add_n" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
......@@ -282,11 +282,11 @@
</transf>
</goal>
<goal name="VC wmpn_add_n.1" expl="loop invariant init" proved="true">
<proof prover="5" timelimit="5"><result status="valid" time="0.03" steps="81"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.03" steps="67"/></proof>
</goal>
<goal name="VC wmpn_add_n.2" expl="loop invariant init" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.10" steps="15"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.10" steps="13"/></proof>
</goal>
<goal name="VC wmpn_add_n.3" expl="loop invariant init" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
......@@ -307,7 +307,7 @@
<proof prover="5" timelimit="5"><result status="valid" time="0.09" steps="40"/></proof>
</goal>
<goal name="VC wmpn_add_n.8" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.57"/></proof>
<proof prover="0"><result status="valid" time="0.90"/></proof>
</goal>
<goal name="VC wmpn_add_n.9" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
......@@ -334,7 +334,7 @@
<proof prover="3"><result status="valid" time="0.17"/></proof>
</goal>
<goal name="VC wmpn_add_n.12.0.0.2" proved="true">
<proof prover="3"><result status="valid" time="0.16"/></proof>
<proof prover="3"><result status="valid" time="0.28"/></proof>
</goal>
</transf>
</goal>
......@@ -382,10 +382,10 @@
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC wmpn_add.1" expl="loop invariant init" proved="true">
<proof prover="5"><result status="valid" time="0.03" steps="88"/></proof>
<proof prover="5"><result status="valid" time="0.03" steps="75"/></proof>
</goal>
<goal name="VC wmpn_add.2" expl="loop invariant init" proved="true">
<proof prover="5" timelimit="5"><result status="valid" time="0.07" steps="17"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.07" steps="14"/></proof>
</goal>
<goal name="VC wmpn_add.3" expl="loop invariant init" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
......@@ -410,7 +410,7 @@
</transf>
</goal>
<goal name="VC wmpn_add.8" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.60"/></proof>
<proof prover="0"><result status="valid" time="0.83"/></proof>
</goal>
<goal name="VC wmpn_add.9" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
......@@ -434,7 +434,7 @@
<proof prover="3"><result status="valid" time="0.16"/></proof>
</goal>
<goal name="VC wmpn_add.12.0.0.2" proved="true">
<proof prover="2"><result status="valid" time="0.20"/></proof>
<proof prover="2"><result status="valid" time="0.38"/></proof>
</goal>
</transf>
</goal>
......@@ -488,7 +488,7 @@
<goal name="VC wmpn_add.26" expl="precondition" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC wmpn_add.26.0" expl="VC for wmpn_add" proved="true">
<proof prover="0"><result status="valid" time="3.26"/></proof>
<proof prover="0"><result status="valid" time="5.27"/></proof>
</goal>
<goal name="VC wmpn_add.26.1" expl="VC for wmpn_add" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof>
......@@ -496,7 +496,7 @@
</transf>
</goal>
<goal name="VC wmpn_add.27" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.66"/></proof>
<proof prover="0"><result status="valid" time="0.85"/></proof>
</goal>
<goal name="VC wmpn_add.28" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
......@@ -505,22 +505,22 @@
<proof prover="2"><result status="valid" time="0.10"/></proof>
</goal>
<goal name="VC wmpn_add.30" expl="integer overflow" proved="true">
<proof prover="5" timelimit="5"><result status="valid" time="0.18" steps="69"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.18" steps="67"/></proof>
</goal>
<goal name="VC wmpn_add.31" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="0.21"/></proof>
</goal>
<goal name="VC wmpn_add.32" expl="assertion" proved="true">
<proof prover="5"><result status="valid" time="0.16" steps="58"/></proof>
<proof prover="5"><result status="valid" time="0.16" steps="56"/></proof>
</goal>
<goal name="VC wmpn_add.33" expl="loop invariant init" proved="true">
<proof prover="3"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC wmpn_add.34" expl="loop invariant init" proved="true">
<proof prover="5" timelimit="5"><result status="valid" time="0.23" steps="61"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.23" steps="59"/></proof>
</goal>
<goal name="VC wmpn_add.35" expl="loop invariant init" proved="true">
<proof prover="5" timelimit="5"><result status="valid" time="0.23" steps="61"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.23" steps="59"/></proof>
</goal>
<goal name="VC wmpn_add.36" expl="loop invariant init" proved="true">
<proof prover="2"><result status="valid" time="0.15"/></proof>
......@@ -529,7 +529,7 @@
<proof prover="2"><result status="valid" time="0.11"/></proof>
</goal>
<goal name="VC wmpn_add.38" expl="precondition" proved="true">
<proof prover="5" timelimit="5"><result status="valid" time="0.24" steps="84"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.40" steps="82"/></proof>
</goal>
<goal name="VC wmpn_add.39" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.14"/></proof>
......@@ -541,29 +541,29 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC wmpn_add.42" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.80"/></proof>
<proof prover="0"><result status="valid" time="1.08"/></proof>
</goal>
<goal name="VC wmpn_add.43" expl="assertion" proved="true">
<proof prover="5" timelimit="5"><result status="valid" time="0.27" steps="80"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.42" steps="78"/></proof>
</goal>
<goal name="VC wmpn_add.44" expl="integer overflow" proved="true">
<proof prover="5" timelimit="5"><result status="valid" time="0.28" steps="98"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.28" steps="96"/></proof>
</goal>
<goal name="VC wmpn_add.45" expl="loop variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC wmpn_add.46" expl="loop invariant preservation" proved="true">
<proof prover="5" timelimit="5"><result status="valid" time="0.27" steps="83"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.27" steps="81"/></proof>
</goal>
<goal name="VC wmpn_add.47" expl="loop invariant preservation" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC wmpn_add.47.0" expl="loop invariant preservation" proved="true">
<proof prover="5"><result status="valid" time="0.28" steps="85"/></proof>
<proof prover="5"><result status="valid" time="0.48" steps="83"/></proof>
</goal>
</transf>
</goal>
<goal name="VC wmpn_add.48" expl="loop invariant preservation" proved="true">
<proof prover="5"><result status="valid" time="0.27" steps="85"/></proof>
<proof prover="5"><result status="valid" time="0.51" steps="83"/></proof>
</goal>
<goal name="VC wmpn_add.49" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.13"/></proof>
......@@ -581,7 +581,7 @@
<proof prover="2"><result status="valid" time="0.10"/></proof>
</goal>
<goal name="VC wmpn_add.54" expl="assertion" proved="true">
<proof prover="5"><result status="valid" time="0.14" steps="93"/></proof>
<proof prover="5"><result status="valid" time="0.14" steps="91"/></proof>
</goal>
<goal name="VC wmpn_add.55" expl="loop variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
......@@ -596,7 +596,7 @@
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC wmpn_add.59" expl="loop invariant preservation" proved="true">
<proof prover="5"><result status="valid" time="0.13" steps="61"/></proof>
<proof prover="5"><result status="valid" time="0.13" steps="59"/></proof>
</goal>
<goal name="VC wmpn_add.60" expl="loop invariant preservation" proved="true">
<proof prover="2" timelimit="5"><result status="valid" time="0.16"/></proof>
......@@ -633,7 +633,7 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC wmpn_add.70" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.68"/></proof>
<proof prover="0"><result status="valid" time="1.26"/></proof>
</goal>
<goal name="VC wmpn_add.71" expl="assertion" proved="true">
<proof prover="5"><result status="valid" time="0.07" steps="59"/></proof>
......@@ -651,10 +651,10 @@
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC wmpn_add.76" expl="loop invariant preservation" proved="true">
<proof prover="5"><result status="valid" time="0.03" steps="65"/></proof>
<proof prover="5"><result status="valid" time="0.03" steps="64"/></proof>
</goal>
<goal name="VC wmpn_add.77" expl="loop invariant preservation" proved="true">
<proof prover="5"><result status="valid" time="0.12" steps="106"/></proof>
<proof prover="5"><result status="valid" time="0.12" steps="105"/></proof>
</goal>
<goal name="VC wmpn_add.78" expl="postcondition" proved="true">
<proof prover="5"><result status="valid" time="0.03" steps="46"/></proof>
......@@ -700,13 +700,13 @@
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC wmpn_add.90" expl="assertion" proved="true">
<proof prover="0" timelimit="10"><result status="valid" time="0.66"/></proof>
<proof prover="0" timelimit="10"><result status="valid" time="1.10"/></proof>
</goal>
<goal name="VC wmpn_add.91" expl="assertion" proved="true">
<proof prover="5"><result status="valid" time="0.02" steps="47"/></proof>
</goal>
<goal name="VC wmpn_add.92" expl="integer overflow" proved="true">
<proof prover="5" timelimit="5"><result status="valid" time="0.02" steps="66"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.02" steps="65"/></proof>
</goal>
<goal name="VC wmpn_add.93" expl="loop variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
......@@ -718,10 +718,10 @@
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC wmpn_add.96" expl="loop invariant preservation" proved="true">
<proof prover="5" timelimit="5"><result status="valid" time="0.03" steps="53"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.03" steps="52"/></proof>
</goal>
<goal name="VC wmpn_add.97" expl="loop invariant preservation" proved="true">
<proof prover="5"><result status="valid" time="0.10" steps="94"/></proof>
<proof prover="5"><result status="valid" time="0.10" steps="93"/></proof>
</goal>
<goal name="VC wmpn_add.98" expl="postcondition" proved="true">
<proof prover="5" timelimit="5"><result status="valid" time="0.04" steps="35"/></proof>
......@@ -740,7 +740,7 @@
<proof prover="2" timelimit="5" memlimit="2000"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC wmpn_add_in_place.1" expl="loop invariant init" proved="true">
<proof prover="5" timelimit="5" memlimit="2000"><result status="valid" time="0.04" steps="74"/></proof>
<proof prover="5" timelimit="5" memlimit="2000"><result status="valid" time="0.04" steps="62"/></proof>
</goal>
<goal name="VC wmpn_add_in_place.2" expl="loop invariant init" proved="true">
<proof prover="2" timelimit="5" memlimit="2000"><result status="valid" time="0.07"/></proof>
......@@ -749,7 +749,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="18"/></proof>
<proof prover="5" timelimit="5" memlimit="2000"><result status="valid" time="0.03" steps="14"/></proof>
</goal>
<goal name="VC wmpn_add_in_place.5" expl="precondition" proved="true">
<transf name="split_goal_right" proved="true" >
......@@ -777,7 +777,7 @@
<proof prover="5"><result status="valid" time="0.02" steps="61"/></proof>
</goal>
<goal name="VC wmpn_add_in_place.11" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.61"/></proof>
<proof prover="0"><result status="valid" time="1.16"/></proof>
</goal>
<goal name="VC wmpn_add_in_place.12" expl="precondition" proved="true">
<proof prover="2" timelimit="5"><result status="valid" time="0.05"/></proof>
......@@ -795,13 +795,13 @@
<goal name="VC wmpn_add_in_place.15.0.0" expl="assertion" proved="true">
<transf name="reflection_f" proved="true" arg1="mp_decision">
<goal name="VC wmpn_add_in_place.15.0.0.0" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.20"/></proof>
<proof prover="0"><result status="valid" time="0.38"/></proof>
</goal>
<goal name="VC wmpn_add_in_place.15.0.0.1" proved="true">
<proof prover="3"><result status="valid" time="0.22"/></proof>
</goal>
<goal name="VC wmpn_add_in_place.15.0.0.2" proved="true">
<proof prover="3"><result status="valid" time="0.18"/></proof>
<proof prover="3"><result status="valid" time="0.31"/></proof>
</goal>
</transf>
</goal>
......@@ -825,7 +825,7 @@
<proof prover="3"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC wmpn_add_in_place.21" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.32"/></proof>
<proof prover="0"><result status="valid" time="0.50"/></proof>
</goal>
<goal name="VC wmpn_add_in_place.22" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.15"/></proof>
......@@ -866,23 +866,23 @@
<proof prover="5" timelimit="5" memlimit="2000"><result status="valid" time="0.04" steps="64"/></proof>
</goal>
<goal name="VC wmpn_add_in_place.32" expl="precondition" proved="true">
<proof prover="5" timelimit="50" memlimit="2000"><result status="valid" time="0.04" steps="41"/></proof>
<proof prover="5" timelimit="50" memlimit="2000"><result status="valid" time="0.04" steps="40"/></proof>
</goal>
<goal name="VC wmpn_add_in_place.33" expl="precondition" proved="true">
<proof prover="5" timelimit="5" memlimit="2000"><result status="valid" time="0.04" steps="42"/></proof>
<proof prover="5" timelimit="5" memlimit="2000"><result status="valid" time="0.04" steps="41"/></proof>
</goal>
<goal name="VC wmpn_add_in_place.34" expl="precondition" proved="true">
<proof prover="5" timelimit="5" memlimit="2000"><result status="valid" time="0.04" steps="53"/></proof>
<proof prover="5" timelimit="5" memlimit="2000"><result status="valid" time="0.04" steps="52"/></proof>
</goal>
<goal name="VC wmpn_add_in_place.35" expl="assertion" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC wmpn_add_in_place.35.0" expl="assertion" proved="true">
<proof prover="5"><result status="valid" time="0.11" steps="155"/></proof>
<proof prover="5"><result status="valid" time="0.11" steps="148"/></proof>
</goal>
</transf>
</goal>
<goal name="VC wmpn_add_in_place.36" expl="assertion" proved="true">
<proof prover="5"><result status="valid" time="0.04" steps="80"/></proof>
<proof prover="5"><result status="valid" time="0.04" steps="79"/></proof>
</goal>
<goal name="VC wmpn_add_in_place.37" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof>
......@@ -897,7 +897,7 @@
<proof prover="2"><result status="valid" time="0.20"/></proof>
</goal>
<goal name="VC wmpn_add_in_place.41" expl="assertion" proved="true">
<proof prover="5" timelimit="5" memlimit="2000"><result status="valid" time="0.24" steps="59"/></proof>
<proof prover="5" timelimit="5" memlimit="2000"><result status="valid" time="0.24" steps="57"/></proof>
</goal>
<goal name="VC wmpn_add_in_place.42" expl="assertion" proved="true">
<transf name="split_goal_right" proved="true" >
......@@ -905,10 +905,10 @@
<proof prover="2"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC wmpn_add_in_place.42.1" expl="assertion" proved="true">
<proof prover="5" timelimit="5" memlimit="2000"><result status="valid" time="0.21" steps="62"/></proof>
<proof prover="5" timelimit="5" memlimit="2000"><result status="valid" time="0.38" steps="60"/></proof>
</goal>
<goal name="VC wmpn_add_in_place.42.2" expl="VC for wmpn_add_in_place" proved="true">
<proof prover="5"><result status="valid" time="0.22" steps="87"/></proof>
<proof prover="5"><result status="valid" time="0.40" steps="85"/></proof>
</goal>
<goal name="VC wmpn_add_in_place.42.3" expl="VC for wmpn_add_in_place" proved="true">
<proof prover="2"><result status="valid" time="0.03"/></proof>
......@@ -919,13 +919,13 @@
<proof prover="2"><result status="valid" time="0.13"/></proof>
</goal>
<goal name="VC wmpn_add_in_place.44" expl="precondition" proved="true">
<proof prover="5"><result status="valid" time="0.21" steps="61"/></proof>
<proof prover="5"><result status="valid" time="0.21" steps="59"/></proof>
</goal>
<goal name="VC wmpn_add_in_place.45" expl="precondition" proved="true">
<proof prover="5" timelimit="5" memlimit="2000"><result status="valid" time="0.32" steps="62"/></proof>
<proof prover="5" timelimit="5" memlimit="2000"><result status="valid" time="0.32" steps="60"/></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="112"/></proof>
<proof prover="5" timelimit="5" memlimit="2000"><result status="valid" time="0.27" steps="110"/></proof>
</goal>
<goal name="VC wmpn_add_in_place.47" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
......@@ -937,7 +937,7 @@
<proof prover="2"><result status="valid" time="0.11"/></proof>
</goal>
<goal name="VC wmpn_add_in_place.50" expl="assertion" proved="true">
<proof prover="5"><result status="valid" time="0.16" steps="86"/></proof>
<proof prover="5"><result status="valid" time="0.16" steps="84"/></proof>
</goal>
<goal name="VC wmpn_add_in_place.51" expl="loop variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.05"/></proof>
......@@ -946,7 +946,7 @@
<proof prover="3"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC wmpn_add_in_place.53" expl="loop invariant preservation" proved="true">
<proof prover="5"><result status="valid" time="0.25" steps="61"/></proof>
<proof prover="5"><result status="valid" time="0.25" steps="59"/></proof>
</goal>
<goal name="VC wmpn_add_in_place.54" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
......@@ -955,7 +955,7 @@
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC wmpn_add_in_place.56" expl="loop invariant preservation" proved="true">
<proof prover="5"><result status="valid" time="0.16" steps="87"/></proof>
<proof prover="5"><result status="valid" time="0.32" steps="85"/></proof>
</goal>
<goal name="VC wmpn_add_in_place.57" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.10"/></proof>
......@@ -1038,7 +1038,7 @@
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC wmpn_incr.6" expl="loop invariant init" proved="true">
<proof prover="5"><result status="valid" time="0.12" steps="92"/></proof>
<proof prover="5"><result status="valid" time="0.12" steps="90"/></proof>
</goal>
<goal name="VC wmpn_incr.7" expl="loop invariant init" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
......@@ -1082,12 +1082,12 @@
<goal name="VC wmpn_incr.20" expl="assertion" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC wmpn_incr.20.0" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="0.13"/></proof>
<proof prover="2"><result status="valid" time="0.28"/></proof>
</goal>
</transf>
</goal>
<goal name="VC wmpn_incr.21" expl="assertion" proved="true">
<proof prover="5"><result status="valid" time="0.41" steps="57"/></proof>
<proof prover="5"><result status="valid" time="0.60" steps="56"/></proof>
</goal>
<goal name="VC wmpn_incr.22" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.12"/></proof>
......@@ -1104,7 +1104,7 @@
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC wmpn_incr.24.2" expl="VC for wmpn_incr" proved="true">
<proof prover="5"><result status="valid" time="0.50" steps="76"/></proof>
<proof prover="5"><result status="valid" time="0.50" steps="75"/></proof>
</goal>
<goal name="VC wmpn_incr.24.3" expl="VC for wmpn_incr" proved="true">
<proof prover="2"><result status="valid" time="0.03"/></proof>
......@@ -1115,16 +1115,16 @@
<proof prover="2"><result status="valid" time="0.10"/></proof>
</goal>
<goal name="VC wmpn_incr.26" expl="postcondition" proved="true">
<proof prover="5"><result status="valid" time="0.50" steps="61"/></proof>
<proof prover="5"><result status="valid" time="0.70" steps="60"/></proof>
</goal>
<goal name="VC wmpn_incr.27" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.12"/></proof>
<proof prover="2"><result status="valid" time="0.26"/></proof>
</goal>
<goal name="VC wmpn_incr.28" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="0.15"/></proof>
</goal>
<goal name="VC wmpn_incr.29" expl="assertion" proved="true">
<proof prover="5"><result status="valid" time="0.39" steps="74"/></proof>
<proof prover="5"><result status="valid" time="0.54" steps="73"/></proof>
</goal>
<goal name="VC wmpn_incr.30" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="0.16"/></proof>
......@@ -1145,7 +1145,7 @@
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC wmpn_incr.36" expl="loop invariant preservation" proved="true">
<proof prover="5"><result status="valid" time="0.37" steps="76"/></proof>
<proof prover="5"><result status="valid" time="0.37" steps="75"/></proof>
</goal>
<goal name="VC wmpn_incr.37" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.22"/></proof>
......@@ -1202,7 +1202,7 @@
<proof prover="2"><result status="valid" time="0.10"/></proof>
</goal>
<goal name="VC wmpn_incr.48" expl="postcondition" proved="true">
<proof prover="5"><result status="valid" time="0.16" steps="74"/></proof>
<proof prover="5"><result status="valid" time="0.16" steps="70"/></proof>
</goal>
<goal name="VC wmpn_incr.49" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
......@@ -1227,10 +1227,10 @@
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC wmpn_incr_1.5" expl="loop invariant init" proved="true">
<proof prover="5"><result status="valid" time="0.06" steps="21"/></proof>
<proof prover="5"><result status="valid" time="0.06" steps="20"/></proof>
</goal>
<goal name="VC wmpn_incr_1.6" expl="loop invariant init" proved="true">
<proof prover="5"><result status="valid" time="0.09" steps="19"/></proof>
<proof prover="5"><result status="valid" time="0.09" steps="18"/></proof>
</goal>
<goal name="VC wmpn_incr_1.7" expl="precondition" proved="true">
<proof prover="5"><result status="valid" time="0.04" steps="97"/></proof>
......@@ -1271,19 +1271,19 @@
<goal name="VC wmpn_incr_1.19" expl="assertion" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC wmpn_incr_1.19.0" expl="assertion" proved="true">
<proof prover="5" timelimit="5"><result status="valid" time="0.02" steps="47"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.02" steps="46"/></proof>
</goal>
<goal name="VC wmpn_incr_1.19.1" expl="VC for wmpn_incr_1" proved="true">
<proof prover="5" timelimit="5"><result status="valid" time="0.02" steps="48"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.02" steps="47"/></proof>
</goal>
<goal name="VC wmpn_incr_1.19.2" expl="VC for wmpn_incr_1" proved="true">
<proof prover="5" timelimit="5"><result status="valid" time="0.02" steps="48"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.02" steps="47"/></proof>
</goal>
<goal name="VC wmpn_incr_1.19.3" expl="VC for wmpn_incr_1" proved="true">
<proof prover="5" timelimit="5"><result status="valid" time="0.02" steps="48"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.02" steps="47"/></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.20" steps="176"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.20" steps="170"/></proof>
</goal>
</transf>
</goal>
......@@ -1291,7 +1291,7 @@
<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.07" steps="118"/></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>
......@@ -1303,16 +1303,16 @@
<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.02" steps="50"/></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.02" steps="66"/></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>
<proof prover="5"><result status="valid" time="0.07" steps="69"/></proof>
</goal>
<goal name="VC wmpn_incr_1.28" expl="assertion" proved="true">
<proof prover="5"><result status="valid" time="0.02" steps="54"/></proof>
<proof prover="5"><result status="valid" time="0.02" steps="53"/></proof>
</goal>
<goal name="VC wmpn_incr_1.29" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
......@@ -1321,13 +1321,13 @@
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC wmpn_incr_1.31" expl="precondition" proved="true">
<proof prover="5"><result status="valid" time="0.05" steps="139"/></proof>
<proof prover="5"><result status="valid" time="0.05" steps="132"/></proof>
</goal>
<goal name="VC wmpn_incr_1.32" expl="assertion" proved="true">
<proof prover="5"><result status="valid" time="0.02" steps="57"/></proof>
<proof prover="5"><result status="valid" time="0.02" steps="56"/></proof>
</goal>
<goal name="VC wmpn_incr_1.33" expl="assertion" proved="true">
<proof prover="5"><result status="valid" time="0.09" steps="120"/></proof>
<proof prover="5"><result status="valid" time="0.09" steps="114"/></proof>
</goal>
<goal name="VC wmpn_incr_1.34" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
......@@ -1336,7 +1336,7 @@
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC wmpn_incr_1.36" expl="assertion" proved="true">
<proof prover="5"><result status="valid" time="0.03" steps="44"/></proof>
<proof prover="5"><result status="valid" time="0.03" steps="43"/></proof>
</goal>
<goal name="VC wmpn_incr_1.37" expl="integer overflow" proved="true">
<proof prover="3"><result status="valid" time="0.26"/></proof>
......@@ -1344,19 +1344,19 @@
<goal name="VC wmpn_incr_1.38" expl="assertion" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC wmpn_incr_1.38.0" expl="assertion" proved="true">
<proof prover="5" timelimit="5"><result status="valid" time="0.02" steps="48"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.02" steps="46"/></proof>
</goal>
<goal name="VC wmpn_incr_1.38.1" expl="VC for wmpn_incr_1" proved="true">
<proof prover="5" timelimit="5"><result status="valid" time="0.02" steps="49"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.02" steps="47"/></proof>
</goal>
<goal name="VC wmpn_incr_1.38.2" expl="VC for wmpn_incr_1" proved="true">
<proof prover="5" timelimit="5"><result status="valid" time="0.02" steps="49"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.02" steps="47"/></proof>
</goal>