Update proofs!

colis-anr · Feb 19, 2020 · 34aaf76 · 34aaf76
1 parent 588f912
commit 34aaf76
Show file tree

Hide file tree

Showing 6 changed files with 1,115 additions and 1,188 deletions.
diff --git a/src/concrete/interpreter/why3session.xml b/src/concrete/interpreter/why3session.xml
diff --git a/src/concrete/interpreter/why3shapes.gz b/src/concrete/interpreter/why3shapes.gz
diff --git a/src/concrete/semantics/why3session.xml b/src/concrete/semantics/why3session.xml
@@ -33,7 +33,7 @@
   <proof prover="5"><result status="valid" time="0.01" steps="58"/></proof>
   </goal>
   <goal name="concat_empty_left&#39;vc.1" expl="postcondition" proved="true">
-  <proof prover="5" timelimit="5"><result status="valid" time="6.00" steps="6077"/></proof>
+  <proof prover="5" timelimit="5"><result status="valid" time="7.05" steps="6077"/></proof>
   </goal>
  </transf>
  </goal>
@@ -70,16 +70,22 @@
   <proof prover="5"><result status="valid" time="0.01" steps="14"/></proof>
   </goal>
   <goal name="concat_assoc&#39;vc.1" expl="variant decrease" proved="true">
-  <proof prover="1"><result status="valid" time="0.04" steps="14167"/></proof>
+  <transf name="split_vc" proved="true" >
+   <goal name="concat_assoc&#39;vc.1.0" expl="variant decrease" proved="true">
+   <proof prover="4" timelimit="10"><result status="valid" time="0.03" steps="47997"/></proof>
+   </goal>
+   <goal name="concat_assoc&#39;vc.1.1" expl="variant decrease" proved="true">
+   <proof prover="4" timelimit="5"><result status="valid" time="0.03" steps="37700"/></proof>
+   </goal>
+  </transf>
   </goal>
   <goal name="concat_assoc&#39;vc.2" expl="postcondition" proved="true">
   <transf name="split_vc" proved="true" >
    <goal name="concat_assoc&#39;vc.2.0" expl="postcondition" proved="true">
-   <proof prover="4" timelimit="5"><result status="valid" time="0.03" steps="39880"/></proof>
+   <proof prover="1" timelimit="1" memlimit="1000"><result status="valid" time="0.05" steps="12228"/></proof>
    </goal>
    <goal name="concat_assoc&#39;vc.2.1" expl="postcondition" proved="true">
-   <proof prover="4" timelimit="10"><result status="valid" time="0.03" steps="58843"/></proof>
-   <proof prover="5" timelimit="10" memlimit="4000"><result status="timeout" time="10.00"/></proof>
+   <proof prover="4" timelimit="10"><result status="valid" time="0.02" steps="58843"/></proof>
    </goal>
   </transf>
   </goal>
@@ -180,17 +186,21 @@
  <proof prover="5"><result status="valid" time="0.21" steps="143"/></proof>
  </goal>
  <goal name="eval_foreach_concat&#39;vc" expl="VC for eval_foreach_concat" proved="true">
- <proof prover="5" timelimit="10"><result status="valid" time="2.27" steps="970"/></proof>
+ <proof prover="5" timelimit="10"><result status="valid" time="3.24" steps="970"/></proof>
  </goal>
  <goal name="eval_foreach_last&#39;vc" expl="VC for eval_foreach_last" proved="true">
  <transf name="split_vc" proved="true" >
   <goal name="eval_foreach_last&#39;vc.0" expl="postcondition" proved="true">
   <transf name="inversion_arg_pr" proved="true" arg1="H1">
    <goal name="eval_foreach_last&#39;vc.0.0" expl="postcondition" proved="true">
-   <proof prover="5"><result status="valid" time="0.96" steps="719"/></proof>
+   <transf name="split_vc" proved="true" >
+    <goal name="eval_foreach_last&#39;vc.0.0.0" expl="postcondition" proved="true">
+    <proof prover="5" timelimit="10" memlimit="4000"><result status="valid" time="2.21" steps="719"/></proof>
+    </goal>
+   </transf>
    </goal>
    <goal name="eval_foreach_last&#39;vc.0.1" expl="postcondition" proved="true">
-   <proof prover="5"><result status="valid" time="0.16" steps="26"/></proof>
+   <proof prover="5"><result status="valid" time="0.07" steps="26"/></proof>
    </goal>
    <goal name="eval_foreach_last&#39;vc.0.2" expl="postcondition" proved="true">
    <proof prover="5"><result status="valid" time="0.27" steps="44"/></proof>
@@ -200,18 +210,18 @@
   <goal name="eval_foreach_last&#39;vc.1" expl="postcondition" proved="true">
   <transf name="inversion_arg_pr" proved="true" arg1="H1">
    <goal name="eval_foreach_last&#39;vc.1.0" expl="postcondition" proved="true">
-   <proof prover="5"><result status="valid" time="0.23" steps="39"/></proof>
+   <proof prover="5"><result status="valid" time="0.09" steps="39"/></proof>
    </goal>
    <goal name="eval_foreach_last&#39;vc.1.1" expl="postcondition" proved="true">
-   <proof prover="5"><result status="valid" time="0.09" steps="26"/></proof>
+   <proof prover="5"><result status="valid" time="0.11" steps="26"/></proof>
    </goal>
    <goal name="eval_foreach_last&#39;vc.1.2" expl="postcondition" proved="true">
-   <proof prover="5"><result status="valid" time="0.26" steps="115"/></proof>
+   <proof prover="5"><result status="valid" time="0.43" steps="115"/></proof>
    </goal>
   </transf>
   <transf name="split_vc" proved="true" >
    <goal name="eval_foreach_last&#39;vc.1.0" expl="postcondition" proved="true">
-   <proof prover="5" timelimit="10" memlimit="4000"><result status="valid" time="1.79" steps="1085"/></proof>
+   <proof prover="5" timelimit="10" memlimit="4000"><result status="valid" time="2.18" steps="1085"/></proof>
    </goal>
   </transf>
   </goal>

diff --git a/src/concrete/semantics/why3shapes.gz b/src/concrete/semantics/why3shapes.gz