Commit 6cca4ffc authored by Raphael Rieu-Helft's avatar Raphael Rieu-Helft
Browse files

Fix another session

parent 83265f53
......@@ -149,10 +149,10 @@
<proof prover="4" memlimit="2000"><result status="valid" time="0.00" steps="15"/></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="10"/></proof>
</goal>
<goal name="VC sprod.4" expl="exceptional postcondition" proved="true">
<proof prover="4" memlimit="2000"><result status="valid" time="0.00" steps="10"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
......@@ -579,10 +579,10 @@
<goal name="VC add_expr.4" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC add_expr.4.0" expl="postcondition" proved="true">
<proof prover="3" memlimit="1000"><result status="valid" time="0.46"/></proof>
<proof prover="3"><result status="valid" time="1.05"/></proof>
</goal>
<goal name="VC add_expr.4.1" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.25"/></proof>
<proof prover="0" timelimit="1"><result status="valid" time="0.07"/></proof>
</goal>
</transf>
</goal>
......@@ -643,10 +643,10 @@
<goal name="VC add_expr.17.0.0" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC add_expr.17.0.0.0" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.38"/></proof>
<proof prover="3"><result status="valid" time="1.18"/></proof>
</goal>
<goal name="VC add_expr.17.0.0.1" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.25"/></proof>
<proof prover="0" timelimit="1"><result status="valid" time="0.14"/></proof>
</goal>
</transf>
</goal>
......@@ -1070,7 +1070,7 @@
<goal name="VC gauss_jordan.27.0" expl="assertion" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC gauss_jordan.27.0.0" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.11"/></proof>
<proof prover="0"><result status="valid" time="0.23"/></proof>
</goal>
<goal name="VC gauss_jordan.27.0.1" expl="VC for gauss_jordan" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
......@@ -1083,14 +1083,14 @@
<goal name="VC gauss_jordan.27.0.3.0" expl="VC for gauss_jordan" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC gauss_jordan.27.0.3.0.0" expl="VC for gauss_jordan" proved="true">
<proof prover="4"><result status="valid" time="0.27" steps="554"/></proof>
<proof prover="4"><result status="valid" time="0.27" steps="529"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="VC gauss_jordan.27.0.4" expl="VC for gauss_jordan" proved="true">
<proof prover="0"><result status="valid" time="0.16"/></proof>
<proof prover="0"><result status="valid" time="0.29"/></proof>
</goal>
</transf>
</goal>
......@@ -1137,7 +1137,7 @@
<proof prover="2"><result status="valid" time="0.13"/></proof>
</goal>
<goal name="VC gauss_jordan.37.3" expl="VC for gauss_jordan" proved="true">
<proof prover="4"><result status="valid" time="0.26" steps="544"/></proof>
<proof prover="4"><result status="valid" time="0.26" steps="520"/></proof>
</goal>
<goal name="VC gauss_jordan.37.4" expl="VC for gauss_jordan" proved="true">
<proof prover="0"><result status="valid" time="0.15"/></proof>
......@@ -1296,7 +1296,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="32"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="32"/></proof>
</goal>
<goal name="VC linear_decision.18" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="82"/></proof>
......@@ -1306,24 +1306,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="32"/></proof>
<proof prover="4"><result status="valid" time="0.01" steps="32"/></proof>
</goal>
<goal name="VC linear_decision.21" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="82"/></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="10"/></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="10"/></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="10"/></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="10"/></proof>
</goal>
<goal name="VC linear_decision.26" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
......@@ -1341,10 +1341,10 @@
<proof prover="4"><result status="valid" time="0.02" steps="96"/></proof>
</goal>
<goal name="VC linear_decision.31" expl="integer overflow" 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 name="VC linear_decision.32" expl="variant decrease" proved="true">
<proof prover="4"><result status="valid" time="0.01" steps="37"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="37"/></proof>
</goal>
<goal name="VC linear_decision.33" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="94"/></proof>
......@@ -1357,12 +1357,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="10"/></proof>
</goal>
<goal name="VC linear_decision.37" expl="integer overflow" 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 name="VC linear_decision.38" expl="variant decrease" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="37"/></proof>
<proof prover="4"><result status="valid" time="0.01" steps="37"/></proof>
</goal>
<goal name="VC linear_decision.39" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="94"/></proof>
......@@ -1375,7 +1376,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="10"/></proof>
</goal>
<goal name="VC linear_decision.43" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
......@@ -1406,16 +1406,16 @@
<proof prover="4"><result status="valid" time="0.02" steps="92"/></proof>
</goal>
<goal name="VC linear_decision.52" 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.53" 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.54" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.03" steps="90"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="90"/></proof>
</goal>
<goal name="VC linear_decision.55" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.03" steps="40"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="40"/></proof>
</goal>
<goal name="VC linear_decision.56" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="37"/></proof>
......@@ -1424,16 +1424,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="35"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="35"/></proof>
</goal>
<goal name="VC linear_decision.59" 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.60" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="90"/></proof>
<proof prover="4"><result status="valid" time="0.03" steps="90"/></proof>
</goal>
<goal name="VC linear_decision.61" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="40"/></proof>
<proof prover="4"><result status="valid" time="0.03" steps="40"/></proof>
</goal>
<goal name="VC linear_decision.62" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="37"/></proof>
......@@ -1491,17 +1491,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="10"/></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="10"/></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="10"/></proof>
</goal>
<goal name="VC linear_decision.84" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
......@@ -1552,16 +1552,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>
......@@ -3712,7 +3712,7 @@
<goal name="VC prop_ctx.75.3.0" expl="VC for prop_ctx" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="VC prop_ctx.75.3.0.0" expl="VC for prop_ctx" proved="true">
<proof prover="0" timelimit="15" memlimit="2000"><result status="valid" time="0.85"/></proof>
<proof prover="0" timelimit="15" memlimit="2000"><result status="valid" time="1.10"/></proof>
</goal>
</transf>
</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