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

Fix a session

parent 24cb7442
...@@ -1007,7 +1007,7 @@ ...@@ -1007,7 +1007,7 @@
<proof prover="2"><result status="valid" time="0.02"/></proof> <proof prover="2"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="VC gauss_jordan.8" expl="integer overflow" proved="true"> <goal name="VC gauss_jordan.8" expl="integer overflow" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof> <proof prover="2"><result status="valid" time="0.03"/></proof>
</goal> </goal>
<goal name="VC gauss_jordan.9" expl="loop invariant init" proved="true"> <goal name="VC gauss_jordan.9" expl="loop invariant init" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof> <proof prover="2"><result status="valid" time="0.02"/></proof>
...@@ -1118,7 +1118,7 @@ ...@@ -1118,7 +1118,7 @@
<proof prover="2"><result status="valid" time="0.03"/></proof> <proof prover="2"><result status="valid" time="0.03"/></proof>
</goal> </goal>
<goal name="VC gauss_jordan.34" expl="index in array bounds" proved="true"> <goal name="VC gauss_jordan.34" expl="index in array bounds" proved="true">
<proof prover="2"><result status="valid" time="0.68"/></proof> <proof prover="2"><result status="valid" time="0.45"/></proof>
<proof prover="4" memlimit="2000"><result status="valid" time="0.01" steps="43"/></proof> <proof prover="4" memlimit="2000"><result status="valid" time="0.01" steps="43"/></proof>
</goal> </goal>
<goal name="VC gauss_jordan.35" expl="precondition" proved="true"> <goal name="VC gauss_jordan.35" expl="precondition" proved="true">
...@@ -1152,7 +1152,7 @@ ...@@ -1152,7 +1152,7 @@
<proof prover="4" memlimit="2000"><result status="valid" time="0.01" steps="38"/></proof> <proof prover="4" memlimit="2000"><result status="valid" time="0.01" steps="38"/></proof>
</goal> </goal>
<goal name="VC gauss_jordan.39" expl="loop invariant preservation" proved="true"> <goal name="VC gauss_jordan.39" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.83"/></proof> <proof prover="2"><result status="valid" time="0.61"/></proof>
</goal> </goal>
<goal name="VC gauss_jordan.40" expl="loop invariant preservation" proved="true"> <goal name="VC gauss_jordan.40" expl="loop invariant preservation" proved="true">
<proof prover="4"><result status="valid" time="0.03" steps="50"/></proof> <proof prover="4"><result status="valid" time="0.03" steps="50"/></proof>
...@@ -1221,7 +1221,7 @@ ...@@ -1221,7 +1221,7 @@
<proof prover="4" memlimit="2000"><result status="valid" time="0.01" steps="20"/></proof> <proof prover="4" memlimit="2000"><result status="valid" time="0.01" steps="20"/></proof>
</goal> </goal>
<goal name="VC gauss_jordan.52" expl="integer overflow" proved="true"> <goal name="VC gauss_jordan.52" expl="integer overflow" proved="true">
<proof prover="2"><result status="valid" time="0.03"/></proof> <proof prover="2"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="VC gauss_jordan.53" expl="index in array bounds" proved="true"> <goal name="VC gauss_jordan.53" expl="index in array bounds" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="27"/></proof> <proof prover="4"><result status="valid" time="0.02" steps="27"/></proof>
...@@ -1270,7 +1270,7 @@ ...@@ -1270,7 +1270,7 @@
<proof prover="2"><result status="valid" time="0.02"/></proof> <proof prover="2"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="VC linear_decision.6" expl="integer overflow" proved="true"> <goal name="VC linear_decision.6" expl="integer overflow" proved="true">
<proof prover="2"><result status="valid" time="0.03"/></proof> <proof prover="2"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="VC linear_decision.7" expl="precondition" proved="true"> <goal name="VC linear_decision.7" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.06"/></proof> <proof prover="2"><result status="valid" time="0.06"/></proof>
...@@ -1280,7 +1280,7 @@ ...@@ -1280,7 +1280,7 @@
<proof prover="2"><result status="valid" time="0.03"/></proof> <proof prover="2"><result status="valid" time="0.03"/></proof>
</goal> </goal>
<goal name="VC linear_decision.9" expl="integer overflow" proved="true"> <goal name="VC linear_decision.9" expl="integer overflow" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof> <proof prover="2"><result status="valid" time="0.03"/></proof>
</goal> </goal>
<goal name="VC linear_decision.10" expl="array creation size" proved="true"> <goal name="VC linear_decision.10" expl="array creation size" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof> <proof prover="2"><result status="valid" time="0.04"/></proof>
...@@ -1350,7 +1350,7 @@ ...@@ -1350,7 +1350,7 @@
<proof prover="4"><result status="valid" time="0.02" steps="84"/></proof> <proof prover="4"><result status="valid" time="0.02" steps="84"/></proof>
</goal> </goal>
<goal name="VC linear_decision.31" expl="integer overflow" proved="true"> <goal name="VC linear_decision.31" expl="integer overflow" proved="true">
<proof prover="4"><result status="valid" time="0.03" steps="34"/></proof> <proof prover="4"><result status="valid" time="0.02" steps="34"/></proof>
</goal> </goal>
<goal name="VC linear_decision.32" expl="variant decrease" proved="true"> <goal name="VC linear_decision.32" expl="variant decrease" proved="true">
<proof prover="4"><result status="valid" time="0.01" steps="34"/></proof> <proof prover="4"><result status="valid" time="0.01" steps="34"/></proof>
...@@ -1368,7 +1368,7 @@ ...@@ -1368,7 +1368,7 @@
<proof prover="2"><result status="valid" time="0.01"/></proof> <proof prover="2"><result status="valid" time="0.01"/></proof>
</goal> </goal>
<goal name="VC linear_decision.37" expl="integer overflow" proved="true"> <goal name="VC linear_decision.37" expl="integer overflow" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="34"/></proof> <proof prover="4"><result status="valid" time="0.03" steps="34"/></proof>
</goal> </goal>
<goal name="VC linear_decision.38" expl="variant decrease" proved="true"> <goal name="VC linear_decision.38" expl="variant decrease" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="34"/></proof> <proof prover="4"><result status="valid" time="0.02" steps="34"/></proof>
...@@ -1390,23 +1390,22 @@ ...@@ -1390,23 +1390,22 @@
<proof prover="2"><result status="valid" time="0.01"/></proof> <proof prover="2"><result status="valid" time="0.01"/></proof>
</goal> </goal>
<goal name="VC linear_decision.44" expl="integer overflow" proved="true"> <goal name="VC linear_decision.44" expl="integer overflow" proved="true">
<proof prover="4"><result status="valid" time="0.03" steps="32"/></proof> <proof prover="1"><result status="valid" time="0.14"/></proof>
</goal> </goal>
<goal name="VC linear_decision.45" expl="variant decrease" proved="true"> <goal name="VC linear_decision.45" expl="variant decrease" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="32"/></proof> <proof prover="4"><result status="valid" time="0.02" steps="32"/></proof>
</goal> </goal>
<goal name="VC linear_decision.46" expl="precondition" proved="true"> <goal name="VC linear_decision.46" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="78"/></proof> <proof prover="4"><result status="valid" time="0.03" steps="78"/></proof>
</goal> </goal>
<goal name="VC linear_decision.47" expl="precondition" proved="true"> <goal name="VC linear_decision.47" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="37"/></proof> <proof prover="4"><result status="valid" time="0.03" steps="37"/></proof>
</goal> </goal>
<goal name="VC linear_decision.48" expl="precondition" proved="true"> <goal name="VC linear_decision.48" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="34"/></proof> <proof prover="4"><result status="valid" time="0.02" steps="34"/></proof>
</goal> </goal>
<goal name="VC linear_decision.49" expl="exceptional postcondition" proved="true"> <goal name="VC linear_decision.49" 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>
<proof prover="4"><result status="valid" time="0.01" steps="7"/></proof>
</goal> </goal>
<goal name="VC linear_decision.50" expl="precondition" proved="true"> <goal name="VC linear_decision.50" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="31"/></proof> <proof prover="4"><result status="valid" time="0.02" steps="31"/></proof>
...@@ -1415,16 +1414,16 @@ ...@@ -1415,16 +1414,16 @@
<proof prover="4"><result status="valid" time="0.02" steps="80"/></proof> <proof prover="4"><result status="valid" time="0.02" steps="80"/></proof>
</goal> </goal>
<goal name="VC linear_decision.52" expl="integer overflow" proved="true"> <goal name="VC linear_decision.52" expl="integer overflow" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="32"/></proof> <proof prover="4"><result status="valid" time="0.03" steps="32"/></proof>
</goal> </goal>
<goal name="VC linear_decision.53" expl="variant decrease" proved="true"> <goal name="VC linear_decision.53" expl="variant decrease" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="32"/></proof> <proof prover="4"><result status="valid" time="0.01" steps="32"/></proof>
</goal> </goal>
<goal name="VC linear_decision.54" expl="precondition" proved="true"> <goal name="VC linear_decision.54" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.03" steps="78"/></proof> <proof prover="4"><result status="valid" time="0.02" steps="78"/></proof>
</goal> </goal>
<goal name="VC linear_decision.55" expl="precondition" proved="true"> <goal name="VC linear_decision.55" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.03" steps="37"/></proof> <proof prover="4"><result status="valid" time="0.02" steps="37"/></proof>
</goal> </goal>
<goal name="VC linear_decision.56" expl="precondition" proved="true"> <goal name="VC linear_decision.56" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="34"/></proof> <proof prover="4"><result status="valid" time="0.02" steps="34"/></proof>
...@@ -1433,10 +1432,10 @@ ...@@ -1433,10 +1432,10 @@
<proof prover="2"><result status="valid" time="0.01"/></proof> <proof prover="2"><result status="valid" time="0.01"/></proof>
</goal> </goal>
<goal name="VC linear_decision.58" expl="integer overflow" proved="true"> <goal name="VC linear_decision.58" expl="integer overflow" proved="true">
<proof prover="4"><result status="valid" time="0.03" steps="32"/></proof> <proof prover="4"><result status="valid" time="0.02" steps="32"/></proof>
</goal> </goal>
<goal name="VC linear_decision.59" expl="variant decrease" proved="true"> <goal name="VC linear_decision.59" expl="variant decrease" proved="true">
<proof prover="4"><result status="valid" time="0.01" steps="32"/></proof> <proof prover="4"><result status="valid" time="0.02" steps="32"/></proof>
</goal> </goal>
<goal name="VC linear_decision.60" expl="precondition" proved="true"> <goal name="VC linear_decision.60" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="78"/></proof> <proof prover="4"><result status="valid" time="0.02" steps="78"/></proof>
...@@ -1448,13 +1447,14 @@ ...@@ -1448,13 +1447,14 @@
<proof prover="4"><result status="valid" time="0.02" steps="34"/></proof> <proof prover="4"><result status="valid" time="0.02" steps="34"/></proof>
</goal> </goal>
<goal name="VC linear_decision.63" expl="exceptional postcondition" proved="true"> <goal name="VC linear_decision.63" 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>
<proof prover="4"><result status="valid" time="0.01" steps="7"/></proof>
</goal> </goal>
<goal name="VC linear_decision.64" expl="exceptional postcondition" proved="true"> <goal name="VC linear_decision.64" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof> <proof prover="2"><result status="valid" time="0.01"/></proof>
</goal> </goal>
<goal name="VC linear_decision.65" expl="integer overflow" proved="true"> <goal name="VC linear_decision.65" expl="integer overflow" proved="true">
<proof prover="2"><result status="valid" time="0.03"/></proof> <proof prover="4"><result status="valid" time="0.03" steps="31"/></proof>
</goal> </goal>
<goal name="VC linear_decision.66" expl="variant decrease" proved="true"> <goal name="VC linear_decision.66" expl="variant decrease" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="31"/></proof> <proof prover="4"><result status="valid" time="0.02" steps="31"/></proof>
...@@ -3106,13 +3106,13 @@ ...@@ -3106,13 +3106,13 @@
<proof prover="2"><result status="valid" time="0.23"/></proof> <proof prover="2"><result status="valid" time="0.23"/></proof>
</goal> </goal>
<goal name="VC mp_decision.4" expl="exceptional postcondition" proved="true"> <goal name="VC mp_decision.4" 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>
<goal name="VC mp_decision.5" expl="exceptional postcondition" proved="true"> <goal name="VC mp_decision.5" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof> <proof prover="2"><result status="valid" time="0.01"/></proof>
</goal> </goal>
<goal name="VC mp_decision.6" expl="exceptional postcondition" proved="true"> <goal name="VC mp_decision.6" 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>
</transf> </transf>
</goal> </goal>
......
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