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

Update sessions

parent 9fedeaf3
...@@ -20,40 +20,40 @@ ...@@ -20,40 +20,40 @@
<proof prover="5"><result status="valid" time="0.03" steps="11"/></proof> <proof prover="5"><result status="valid" time="0.03" steps="11"/></proof>
</goal> </goal>
<goal name="VC wmpn_cmp.2" expl="assertion" proved="true"> <goal name="VC wmpn_cmp.2" expl="assertion" proved="true">
<proof prover="5"><result status="valid" time="0.05" steps="40"/></proof> <proof prover="5"><result status="valid" time="0.05" steps="39"/></proof>
</goal> </goal>
<goal name="VC wmpn_cmp.3" expl="precondition" proved="true"> <goal name="VC wmpn_cmp.3" expl="precondition" proved="true">
<proof prover="5"><result status="valid" time="0.03" steps="47"/></proof> <proof prover="5"><result status="valid" time="0.03" steps="46"/></proof>
</goal> </goal>
<goal name="VC wmpn_cmp.4" expl="integer overflow" proved="true"> <goal name="VC wmpn_cmp.4" expl="integer overflow" proved="true">
<proof prover="5"><result status="valid" time="0.04" steps="26"/></proof> <proof prover="5"><result status="valid" time="0.04" steps="25"/></proof>
</goal> </goal>
<goal name="VC wmpn_cmp.5" expl="assertion" proved="true"> <goal name="VC wmpn_cmp.5" expl="assertion" proved="true">
<proof prover="5"><result status="valid" time="0.03" steps="16"/></proof> <proof prover="5"><result status="valid" time="0.03" steps="15"/></proof>
</goal> </goal>
<goal name="VC wmpn_cmp.6" expl="precondition" proved="true"> <goal name="VC wmpn_cmp.6" expl="precondition" proved="true">
<proof prover="5"><result status="valid" time="0.03" steps="28"/></proof> <proof prover="5"><result status="valid" time="0.03" steps="27"/></proof>
</goal> </goal>
<goal name="VC wmpn_cmp.7" expl="precondition" proved="true"> <goal name="VC wmpn_cmp.7" expl="precondition" proved="true">
<proof prover="5"><result status="valid" time="0.06" steps="28"/></proof> <proof prover="5"><result status="valid" time="0.06" steps="27"/></proof>
</goal> </goal>
<goal name="VC wmpn_cmp.8" expl="precondition" proved="true"> <goal name="VC wmpn_cmp.8" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof> <proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="5"><result status="valid" time="0.05" steps="20"/></proof> <proof prover="5"><result status="valid" time="0.05" steps="19"/></proof>
</goal> </goal>
<goal name="VC wmpn_cmp.9" expl="precondition" proved="true"> <goal name="VC wmpn_cmp.9" expl="precondition" 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>
<goal name="VC wmpn_cmp.10" expl="assertion" proved="true"> <goal name="VC wmpn_cmp.10" expl="assertion" proved="true">
<proof prover="5"><result status="valid" time="0.04" steps="51"/></proof> <proof prover="5"><result status="valid" time="0.04" steps="50"/></proof>
</goal> </goal>
<goal name="VC wmpn_cmp.11" expl="precondition" proved="true"> <goal name="VC wmpn_cmp.11" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof> <proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="5"><result status="valid" time="0.05" steps="23"/></proof> <proof prover="5"><result status="valid" time="0.05" steps="22"/></proof>
</goal> </goal>
<goal name="VC wmpn_cmp.12" expl="precondition" proved="true"> <goal name="VC wmpn_cmp.12" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof> <proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="5"><result status="valid" time="0.07" steps="24"/></proof> <proof prover="5"><result status="valid" time="0.07" steps="23"/></proof>
</goal> </goal>
<goal name="VC wmpn_cmp.13" expl="precondition" proved="true"> <goal name="VC wmpn_cmp.13" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.06"/></proof> <proof prover="1"><result status="valid" time="0.06"/></proof>
...@@ -61,7 +61,7 @@ ...@@ -61,7 +61,7 @@
<goal name="VC wmpn_cmp.14" expl="assertion" proved="true"> <goal name="VC wmpn_cmp.14" expl="assertion" proved="true">
<transf name="inline_goal" proved="true" > <transf name="inline_goal" proved="true" >
<goal name="VC wmpn_cmp.14.0" expl="assertion" proved="true"> <goal name="VC wmpn_cmp.14.0" expl="assertion" proved="true">
<proof prover="5"><result status="valid" time="0.04" steps="36"/></proof> <proof prover="5"><result status="valid" time="0.04" steps="35"/></proof>
</goal> </goal>
</transf> </transf>
</goal> </goal>
...@@ -76,11 +76,11 @@ ...@@ -76,11 +76,11 @@
</transf> </transf>
</goal> </goal>
<goal name="VC wmpn_cmp.16" expl="postcondition" proved="true"> <goal name="VC wmpn_cmp.16" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.16"/></proof> <proof prover="3"><result status="valid" time="0.03"/></proof>
</goal> </goal>
<goal name="VC wmpn_cmp.17" expl="assertion" proved="true"> <goal name="VC wmpn_cmp.17" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof> <proof prover="3"><result status="valid" time="0.03"/></proof>
<proof prover="5"><result status="valid" time="0.05" steps="26"/></proof> <proof prover="5"><result status="valid" time="0.05" steps="25"/></proof>
</goal> </goal>
<goal name="VC wmpn_cmp.18" expl="precondition" proved="true"> <goal name="VC wmpn_cmp.18" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.10"/></proof> <proof prover="1"><result status="valid" time="0.10"/></proof>
...@@ -88,7 +88,7 @@ ...@@ -88,7 +88,7 @@
<goal name="VC wmpn_cmp.19" expl="assertion" proved="true"> <goal name="VC wmpn_cmp.19" expl="assertion" proved="true">
<transf name="inline_goal" proved="true" > <transf name="inline_goal" proved="true" >
<goal name="VC wmpn_cmp.19.0" expl="assertion" proved="true"> <goal name="VC wmpn_cmp.19.0" expl="assertion" proved="true">
<proof prover="5"><result status="valid" time="0.04" steps="37"/></proof> <proof prover="5"><result status="valid" time="0.04" steps="36"/></proof>
</goal> </goal>
</transf> </transf>
</goal> </goal>
...@@ -103,20 +103,20 @@ ...@@ -103,20 +103,20 @@
</transf> </transf>
</goal> </goal>
<goal name="VC wmpn_cmp.21" expl="postcondition" proved="true"> <goal name="VC wmpn_cmp.21" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof> <proof prover="0"><result status="valid" time="0.16"/></proof>
</goal> </goal>
<goal name="VC wmpn_cmp.22" expl="loop variant decrease" proved="true"> <goal name="VC wmpn_cmp.22" expl="loop variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof> <proof prover="3"><result status="valid" time="0.03"/></proof>
<proof prover="5"><result status="valid" time="0.03" steps="20"/></proof> <proof prover="5"><result status="valid" time="0.03" steps="19"/></proof>
</goal> </goal>
<goal name="VC wmpn_cmp.23" expl="loop invariant preservation" proved="true"> <goal name="VC wmpn_cmp.23" expl="loop invariant preservation" proved="true">
<proof prover="5"><result status="valid" time="0.04" steps="20"/></proof> <proof prover="5"><result status="valid" time="0.04" steps="19"/></proof>
</goal> </goal>
<goal name="VC wmpn_cmp.24" expl="loop invariant preservation" proved="true"> <goal name="VC wmpn_cmp.24" expl="loop invariant preservation" 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>
<goal name="VC wmpn_cmp.25" expl="precondition" proved="true"> <goal name="VC wmpn_cmp.25" expl="precondition" proved="true">
<proof prover="5"><result status="valid" time="0.04" steps="44"/></proof> <proof prover="5"><result status="valid" time="0.04" steps="43"/></proof>
</goal> </goal>
<goal name="VC wmpn_cmp.26" expl="postcondition" proved="true"> <goal name="VC wmpn_cmp.26" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof> <proof prover="3"><result status="valid" time="0.03"/></proof>
......
...@@ -72,13 +72,13 @@ ...@@ -72,13 +72,13 @@
<proof prover="1"><result status="valid" time="0.04"/></proof> <proof prover="1"><result status="valid" time="0.04"/></proof>
</goal> </goal>
<goal name="VC wmpn_copyi.20" expl="loop invariant preservation" proved="true"> <goal name="VC wmpn_copyi.20" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.06" steps="212"/></proof> <proof prover="0"><result status="valid" time="0.06" steps="198"/></proof>
</goal> </goal>
<goal name="VC wmpn_copyi.21" expl="loop invariant preservation" proved="true"> <goal name="VC wmpn_copyi.21" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof> <proof prover="1"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="VC wmpn_copyi.22" expl="loop invariant preservation" proved="true"> <goal name="VC wmpn_copyi.22" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.05" steps="98"/></proof> <proof prover="0"><result status="valid" time="0.05" steps="96"/></proof>
</goal> </goal>
<goal name="VC wmpn_copyi.23" expl="loop invariant preservation" proved="true"> <goal name="VC wmpn_copyi.23" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.03"/></proof> <proof prover="1"><result status="valid" time="0.03"/></proof>
...@@ -99,7 +99,7 @@ ...@@ -99,7 +99,7 @@
<proof prover="1"><result status="valid" time="0.02"/></proof> <proof prover="1"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="VC wmpn_copyi.29" expl="loop invariant preservation" proved="true"> <goal name="VC wmpn_copyi.29" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="106"/></proof> <proof prover="0"><result status="valid" time="0.02" steps="104"/></proof>
</goal> </goal>
<goal name="VC wmpn_copyi.30" expl="postcondition" proved="true"> <goal name="VC wmpn_copyi.30" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof> <proof prover="1"><result status="valid" time="0.02"/></proof>
...@@ -121,10 +121,10 @@ ...@@ -121,10 +121,10 @@
<proof prover="1"><result status="valid" time="0.02"/></proof> <proof prover="1"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="VC wmpn_zero_p.3" expl="assertion" proved="true"> <goal name="VC wmpn_zero_p.3" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="14"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="13"/></proof>
</goal> </goal>
<goal name="VC wmpn_zero_p.4" expl="precondition" proved="true"> <goal name="VC wmpn_zero_p.4" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="22"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="21"/></proof>
</goal> </goal>
<goal name="VC wmpn_zero_p.5" expl="precondition" proved="true"> <goal name="VC wmpn_zero_p.5" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof> <proof prover="1"><result status="valid" time="0.02"/></proof>
...@@ -136,7 +136,7 @@ ...@@ -136,7 +136,7 @@
<proof prover="1"><result status="valid" time="0.02"/></proof> <proof prover="1"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="VC wmpn_zero_p.8" expl="postcondition" proved="true"> <goal name="VC wmpn_zero_p.8" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.03" steps="47"/></proof> <proof prover="2"><result status="valid" time="0.03" steps="45"/></proof>
</goal> </goal>
<goal name="VC wmpn_zero_p.9" expl="assertion" proved="true"> <goal name="VC wmpn_zero_p.9" expl="assertion" proved="true">
<proof prover="1"><result status="valid" time="0.01"/></proof> <proof prover="1"><result status="valid" time="0.01"/></proof>
...@@ -148,7 +148,7 @@ ...@@ -148,7 +148,7 @@
<proof prover="1"><result status="valid" time="0.02"/></proof> <proof prover="1"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="VC wmpn_zero_p.12" expl="loop invariant preservation" proved="true"> <goal name="VC wmpn_zero_p.12" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="36"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="35"/></proof>
</goal> </goal>
<goal name="VC wmpn_zero_p.13" expl="postcondition" proved="true"> <goal name="VC wmpn_zero_p.13" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.01"/></proof> <proof prover="1"><result status="valid" time="0.01"/></proof>
...@@ -185,10 +185,10 @@ ...@@ -185,10 +185,10 @@
<proof prover="1"><result status="valid" time="0.03"/></proof> <proof prover="1"><result status="valid" time="0.03"/></proof>
</goal> </goal>
<goal name="VC wmpn_zero.8" expl="loop invariant preservation" proved="true"> <goal name="VC wmpn_zero.8" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.10" steps="106"/></proof> <proof prover="0"><result status="valid" time="0.10" steps="102"/></proof>
</goal> </goal>
<goal name="VC wmpn_zero.9" expl="loop invariant preservation" proved="true"> <goal name="VC wmpn_zero.9" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="50"/></proof> <proof prover="0"><result status="valid" time="0.02" steps="49"/></proof>
</goal> </goal>
<goal name="VC wmpn_zero.10" expl="postcondition" proved="true"> <goal name="VC wmpn_zero.10" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.03"/></proof> <proof prover="1"><result status="valid" time="0.03"/></proof>
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment