nightly bench: replay proofs with coq 8.5 using Coq 8.4pl6

0e378e25 · MARCHE Claude · 7e94fa68 · 0e378e25 · 0e378e25 · 0e378e25
Commit 0e378e25 authored Feb 23, 2016 by MARCHE Claude
13 changed files
--- a/examples/bitvectors/bitvector/why3session.xml
+++ b/examples/bitvectors/bitvector/why3session.xml
@@ -2,7 +2,7 @@
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="4">
-<prover id="1" name="Coq" version="8.5" timelimit="5" steplimit="1" memlimit="1000"/>
+<prover id="0" name="Coq" version="8.4pl6" timelimit="5" steplimit="1" memlimit="1000"/>
 <prover id="2" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="1" memlimit="1000"/>
 <prover id="3" name="CVC3" version="2.4.1" timelimit="5" steplimit="1" memlimit="1000"/>
 <prover id="6" name="CVC4" version="1.4" timelimit="5" steplimit="1" memlimit="4000"/>
@@ -31,16 +31,16 @@
 <proof prover="6" memlimit="1000"><result status="valid" time="0.03"/></proof>
 </goal>
 <goal name="to_nat_of_zero2">
- <proof prover="1" edited="bitvector_BitVector_to_nat_of_zero2_1.v"><result status="valid" time="0.66"/></proof>
+ <proof prover="0" edited="bitvector_BitVector_to_nat_of_zero2_1.v"><result status="valid" time="0.92"/></proof>
 </goal>
 <goal name="to_nat_of_zero">
- <proof prover="1" timelimit="30" edited="bitvector_BitVector_to_nat_of_zero_1.v"><result status="valid" time="1.51"/></proof>
+ <proof prover="0" timelimit="30" edited="bitvector_BitVector_to_nat_of_zero_1.v"><result status="valid" time="2.78"/></proof>
 </goal>
 <goal name="to_nat_of_one">
- <proof prover="1" edited="bitvector_BitVector_to_nat_of_one_1.v"><result status="valid" time="1.41"/></proof>
+ <proof prover="0" edited="bitvector_BitVector_to_nat_of_one_1.v"><result status="valid" time="1.86"/></proof>
 </goal>
 <goal name="to_nat_sub_footprint">
- <proof prover="1" timelimit="7" edited="bitvector_BitVector_to_nat_sub_footprint_1.v"><result status="valid" time="2.51"/></proof>
+ <proof prover="0" timelimit="7" edited="bitvector_BitVector_to_nat_sub_footprint_1.v"><result status="valid" time="3.73"/></proof>
 </goal>
 <goal name="nth_from_int_low_even">
 <proof prover="2"><result status="valid" time="0.02" steps="68"/></proof>
@@ -72,7 +72,7 @@
 <proof prover="3"><result status="valid" time="0.11"/></proof>
 </goal>
 <goal name="nth_from_int2c_plus_pow2">
- <proof prover="1" timelimit="10" edited="bitvector_BitVector_nth_from_int2c_plus_pow2_1.v"><result status="valid" time="0.81"/></proof>
+ <proof prover="0" timelimit="10" edited="bitvector_BitVector_nth_from_int2c_plus_pow2_1.v"><result status="valid" time="1.28"/></proof>
 <proof prover="2"><result status="valid" time="0.12" steps="85"/></proof>
 </goal>
 </theory>
@@ -87,13 +87,13 @@
 <proof prover="2"><result status="valid" time="0.06" steps="73"/></proof>
 <proof prover="3" timelimit="3"><result status="valid" time="0.07"/></proof>
 <proof prover="6" memlimit="1000"><result status="valid" time="0.04"/></proof>
- <proof prover="10"><result status="valid" time="0.76"/></proof>
+ <proof prover="10"><result status="valid" time="0.53"/></proof>
 </goal>
 <goal name="Test2">
 <proof prover="2"><result status="valid" time="0.04" steps="70"/></proof>
 <proof prover="3" timelimit="3"><result status="valid" time="0.06"/></proof>
 <proof prover="6" memlimit="1000"><result status="valid" time="0.04"/></proof>
- <proof prover="9"><result status="valid" time="2.20"/></proof>
+ <proof prover="9"><result status="valid" time="2.58"/></proof>
 <proof prover="10"><result status="valid" time="0.51"/></proof>
 </goal>
 <goal name="Test3">
@@ -107,14 +107,14 @@
 <proof prover="2"><result status="valid" time="0.04" steps="71"/></proof>
 <proof prover="3" timelimit="3"><result status="valid" time="0.07"/></proof>
 <proof prover="6" memlimit="1000"><result status="valid" time="0.04"/></proof>
- <proof prover="9"><result status="valid" time="2.13"/></proof>
+ <proof prover="9"><result status="valid" time="2.59"/></proof>
 <proof prover="10"><result status="valid" time="0.53"/></proof>
 </goal>
 <goal name="Test5">
 <proof prover="2"><result status="valid" time="0.05" steps="71"/></proof>
 <proof prover="3" timelimit="3"><result status="valid" time="0.07"/></proof>
 <proof prover="6" memlimit="1000"><result status="valid" time="0.04"/></proof>
- <proof prover="9"><result status="valid" time="2.15"/></proof>
+ <proof prover="9"><result status="valid" time="2.62"/></proof>
 <proof prover="10"><result status="valid" time="0.50"/></proof>
 </goal>
 <goal name="Test6">
@@ -128,7 +128,7 @@
 <proof prover="2"><result status="valid" time="0.04" steps="78"/></proof>
 <proof prover="3" timelimit="3"><result status="valid" time="0.10"/></proof>
 <proof prover="6" memlimit="1000"><result status="valid" time="0.05"/></proof>
- <proof prover="9"><result status="valid" time="2.31"/></proof>
+ <proof prover="9"><result status="valid" time="2.83"/></proof>
 <proof prover="10"><result status="valid" time="0.52"/></proof>
 </goal>
 <goal name="to_nat_0x00000001">
@@ -156,7 +156,7 @@
 <proof prover="6" timelimit="30"><result status="valid" time="21.52"/></proof>
 </goal>
 <goal name="to_nat_0x000001FF">
- <proof prover="6" timelimit="30"><result status="valid" time="19.74"/></proof>
+ <proof prover="6" timelimit="30"><result status="valid" time="17.48"/></proof>
 </goal>
 <goal name="to_nat_0x000003FF">
 <proof prover="6" timelimit="30"><result status="valid" time="14.09"/></proof>
@@ -177,13 +177,13 @@
 <proof prover="6" timelimit="30"><result status="valid" time="4.20"/></proof>
 </goal>
 <goal name="to_nat_0x0000FFFF">
- <proof prover="6" memlimit="1000"><result status="valid" time="3.66"/></proof>
+ <proof prover="6" memlimit="1000"><result status="valid" time="3.10"/></proof>
 </goal>
 <goal name="to_nat_0x0001FFFF">
- <proof prover="6" memlimit="1000"><result status="valid" time="3.42"/></proof>
+ <proof prover="6" memlimit="1000"><result status="valid" time="2.42"/></proof>
 </goal>
 <goal name="to_nat_0x0003FFFF">
- <proof prover="6" memlimit="1000"><result status="valid" time="2.65"/></proof>
+ <proof prover="6" memlimit="1000"><result status="valid" time="1.81"/></proof>
 </goal>
 <goal name="to_nat_0x0007FFFF">
 <proof prover="6" memlimit="1000"><result status="valid" time="1.56"/></proof>

--- a/examples/bts/13849/why3session.xml
+++ b/examples/bts/13849/why3session.xml
@@ -2,11 +2,11 @@
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="4">
-<prover id="0" name="Coq" version="8.5" timelimit="10" steplimit="1" memlimit="0"/>
+<prover id="1" name="Coq" version="8.4pl6" timelimit="10" steplimit="1" memlimit="0"/>
 <file name="../13849.why" expanded="true">
 <theory name="T" sum="fe6d0a97ed129807ad9b025e583a359d" expanded="true">
 <goal name="x" expanded="true">
- <proof prover="0" edited="13849_T_x_2.v"><result status="valid" time="0.66"/></proof>
+ <proof prover="1" edited="13849_T_x_2.v"><result status="valid" time="0.66"/></proof>
 </goal>
 </theory>
 </file>

--- a/examples/cursor/why3session.xml
+++ b/examples/cursor/why3session.xml
@@ -2,15 +2,15 @@
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="4">
-<prover id="0" name="Z3" version="4.3.1" timelimit="6" memlimit="1000"/>
-<prover id="1" name="Alt-Ergo" version="0.95.2" timelimit="6" memlimit="1000"/>
-<prover id="2" name="CVC4" version="1.3" timelimit="6" memlimit="1000"/>
-<prover id="3" name="Alt-Ergo" version="0.99.1" timelimit="10" memlimit="1000"/>
-<prover id="4" name="CVC4" version="1.4" timelimit="10" memlimit="1000"/>
+<prover id="0" name="Z3" version="4.3.1" timelimit="6" steplimit="1" memlimit="1000"/>
+<prover id="1" name="Alt-Ergo" version="0.95.2" timelimit="6" steplimit="1" memlimit="1000"/>
+<prover id="2" name="CVC4" version="1.3" timelimit="6" steplimit="1" memlimit="1000"/>
+<prover id="3" name="Alt-Ergo" version="0.99.1" timelimit="10" steplimit="1" memlimit="1000"/>
+<prover id="4" name="CVC4" version="1.4" timelimit="10" steplimit="1" memlimit="1000"/>
 <file name="../cursor.mlw">
 <theory name="Cursor" sum="d41d8cd98f00b204e9800998ecf8427e">
 </theory>
-<theory name="TestCursor" sum="d3f25d0a48011e3256d18a93710d9c10">
+<theory name="TestCursor" sum="4a864b2c874ceb1b6d23670c5e40f80b">
 <goal name="WP_parameter sum" expl="VC for sum">
 <transf name="split_goal_wp">
  <goal name="WP_parameter sum.1" expl="1. loop invariant init">
@@ -43,8 +43,8 @@
  <proof prover="3"><result status="valid" time="0.02" steps="11"/></proof>
  </goal>
  <goal name="WP_parameter sum.9" expl="9. loop invariant preservation">
-  <proof prover="1"><result status="valid" time="0.00" steps="17"/></proof>
-  <proof prover="3"><result status="valid" time="0.02" steps="17"/></proof>
+  <proof prover="1"><result status="valid" time="0.00" steps="20"/></proof>
+  <proof prover="3"><result status="valid" time="0.02" steps="24"/></proof>
  </goal>
  <goal name="WP_parameter sum.10" expl="10. loop variant decrease">
  <proof prover="1"><result status="valid" time="0.02" steps="11"/></proof>
@@ -64,7 +64,7 @@
 <proof prover="1"><result status="valid" time="0.01" steps="0"/></proof>
 </goal>
 <goal name="WP_parameter next" expl="VC for next">
- <proof prover="1"><result status="valid" time="0.02" steps="43"/></proof>
+ <proof prover="1"><result status="valid" time="0.02" steps="47"/></proof>
 </goal>
 </theory>
 <theory name="TestListCursor" sum="276fdd29d401c8dff3727e118f9377bb">

--- a/examples/cursor/why3shapes.gz
+++ b/examples/cursor/why3shapes.gz
--- a/examples/logic/lagrange_inequality/why3session.xml
+++ b/examples/logic/lagrange_inequality/why3session.xml
@@ -2,9 +2,9 @@
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="4">
-<prover id="0" name="Coq" version="8.5" timelimit="5" steplimit="1" memlimit="4000"/>
 <prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="1" memlimit="1000"/>
 <prover id="2" name="CVC3" version="2.4.1" timelimit="3" steplimit="1" memlimit="1000"/>
+<prover id="3" name="Coq" version="8.4pl6" timelimit="5" steplimit="1" memlimit="4000"/>
 <prover id="5" name="CVC4" version="1.4" timelimit="5" steplimit="1" memlimit="1000"/>
 <prover id="6" name="MetiTarski" version="2.4" timelimit="5" steplimit="1" memlimit="1000"/>
 <prover id="11" name="Z3" version="4.3.2" timelimit="5" steplimit="1" memlimit="1000"/>
@@ -31,11 +31,11 @@
 <proof prover="11"><result status="valid" time="0.00"/></proof>
 </goal>
 <goal name="sqr_le_sqrt">
- <proof prover="0" edited="lagrange_inequality_CauchySchwarzInequality_sqr_le_sqrt_1.v"><result status="valid" time="1.13"/></proof>
+ <proof prover="3" edited="lagrange_inequality_CauchySchwarzInequality_sqr_le_sqrt_1.v"><result status="valid" time="1.53"/></proof>
 <proof prover="6"><result status="valid" time="0.04"/></proof>
 </goal>
 <goal name="CauchySchwarz">
- <proof prover="0" edited="lagrange_inequality_CauchySchwarzInequality_CauchySchwarz_1.v"><result status="valid" time="1.02"/></proof>
+ <proof prover="3" edited="lagrange_inequality_CauchySchwarzInequality_CauchySchwarz_1.v"><result status="valid" time="1.26"/></proof>
 </goal>
 </theory>
 <theory name="TriangleInequality" sum="c1ce71fbadfa600580a354699d029b51" expanded="true">
@@ -48,7 +48,7 @@
 <proof prover="6"><result status="valid" time="0.06"/></proof>
 </goal>
 <goal name="triangle">
- <proof prover="0" memlimit="1000" edited="lagrange_inequality_TriangleInequality_triangle_1.v"><result status="valid" time="0.50"/></proof>
+ <proof prover="3" memlimit="1000" edited="lagrange_inequality_TriangleInequality_triangle_1.v"><result status="valid" time="0.95"/></proof>
 </goal>
 </theory>
 </file>

--- a/examples/logic/my_cosine/why3session.xml
+++ b/examples/logic/my_cosine/why3session.xml
@@ -3,13 +3,13 @@
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="4">
 <prover id="0" name="Gappa" version="1.2.0" timelimit="2" steplimit="1" memlimit="0"/>
-<prover id="2" name="Coq" version="8.5" timelimit="5" steplimit="1" memlimit="1000"/>
+<prover id="1" name="Coq" version="8.4pl6" timelimit="5" steplimit="1" memlimit="1000"/>
 <prover id="3" name="MetiTarski" version="2.4" timelimit="5" steplimit="1" memlimit="1000"/>
 <prover id="5" name="Alt-Ergo" version="0.99.1" timelimit="3" steplimit="1" memlimit="0"/>
 <file name="../my_cosine.why" expanded="true">
 <theory name="CosineSingle" sum="019a78f095283927a6b919da92d1c881" expanded="true">
 <goal name="MethodError" expanded="true">
- <proof prover="2" edited="my_cosine_CosineSingle_MethodError_1.v"><result status="valid" time="2.21"/></proof>
+ <proof prover="1" edited="my_cosine_CosineSingle_MethodError_1.v"><result status="valid" time="4.07"/></proof>
 <proof prover="3"><result status="valid" time="0.24"/></proof>
 </goal>
 <goal name="TotalErrorFullyExpanded" expanded="true">

--- a/examples/logic/real/why3session.xml
+++ b/examples/logic/real/why3session.xml
@@ -2,12 +2,12 @@
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="4">
-<prover id="0" name="Coq" version="8.5" timelimit="5" steplimit="1" memlimit="1000"/>
+<prover id="1" name="Coq" version="8.4pl6" timelimit="5" steplimit="1" memlimit="1000"/>
 <prover id="2" name="MetiTarski" version="2.4" timelimit="5" steplimit="1" memlimit="1000"/>
 <file name="../real.why" expanded="true">
 <theory name="CosineSingle" sum="07d8b5837de2d4c94b4fcaab63e15669" expanded="true">
 <goal name="MethodError" expanded="true">
- <proof prover="0" edited="real_CosineSingle_MethodError_1.v"><result status="valid" time="1.91"/></proof>
+ <proof prover="1" edited="real_CosineSingle_MethodError_1.v"><result status="valid" time="4.08"/></proof>
 <proof prover="2"><result status="valid" time="0.11"/></proof>
 </goal>
 </theory>

--- a/examples/logic/sorted_list/why3session.xml
+++ b/examples/logic/sorted_list/why3session.xml
@@ -2,7 +2,7 @@
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="4">
-<prover id="0" name="Coq" version="8.5" timelimit="5" steplimit="1" memlimit="0"/>
+<prover id="1" name="Coq" version="8.4pl6" timelimit="5" steplimit="1" memlimit="0"/>
 <prover id="2" name="Z3" version="4.3.2" timelimit="5" steplimit="1" memlimit="1000"/>
 <prover id="3" name="CVC3" version="2.4.1" timelimit="5" steplimit="1" memlimit="0"/>
 <prover id="6" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="1" memlimit="1000"/>
@@ -17,7 +17,7 @@
 <proof prover="2"><result status="valid" time="0.00"/></proof>
 </goal>
 <goal name="sorted_mem" expanded="true">
- <proof prover="0" edited="sorted_list_SortedList_sorted_mem_1.v"><result status="valid" time="0.50"/></proof>
+ <proof prover="1" edited="sorted_list_SortedList_sorted_mem_1.v"><result status="valid" time="0.75"/></proof>
 </goal>
 </theory>
 <theory name="SortedIntList" sum="b630995dca805d46336501a60025b5e3" expanded="true">

--- a/examples/logic/triangle_inequality/why3session.xml
+++ b/examples/logic/triangle_inequality/why3session.xml
@@ -2,11 +2,11 @@
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="4">
-<prover id="0" name="Coq" version="8.5" timelimit="5" steplimit="1" memlimit="1000"/>
 <prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="1" memlimit="1000"/>
+<prover id="2" name="Coq" version="8.4pl6" timelimit="5" steplimit="1" memlimit="1000"/>
 <prover id="3" name="CVC3" version="2.4.1" timelimit="5" steplimit="1" memlimit="1000"/>
 <prover id="4" name="CVC4" version="1.4" timelimit="5" steplimit="1" memlimit="1000"/>
-<prover id="5" name="Z3" version="4.4.0" timelimit="5" memlimit="4000"/>
+<prover id="5" name="Z3" version="4.4.0" timelimit="5" steplimit="1" memlimit="4000"/>
 <prover id="7" name="Z3" version="3.2" timelimit="3" steplimit="1" memlimit="1000"/>
 <prover id="8" name="Z3" version="4.3.2" timelimit="5" steplimit="1" memlimit="1000"/>
 <prover id="11" name="MetiTarski" version="2.4" timelimit="5" steplimit="1" memlimit="1000"/>
@@ -398,7 +398,7 @@
 <proof prover="11"><result status="valid" time="0.03"/></proof>
 </goal>
 <goal name="CauchySchwarz_aux_non_null">
- <proof prover="0" edited="triangle_inequality_CauchySchwarzInequality_CauchySchwarz_aux_non_null_1.v"><result status="valid" time="0.61"/></proof>
+ <proof prover="2" edited="triangle_inequality_CauchySchwarzInequality_CauchySchwarz_aux_non_null_1.v"><result status="valid" time="0.92"/></proof>
 <proof prover="11"><result status="valid" time="0.03"/></proof>
 </goal>
 <goal name="norm_null">
@@ -430,7 +430,7 @@
 <proof prover="11"><result status="valid" time="0.07"/></proof>
 </goal>
 <goal name="CauchySchwarz">
- <proof prover="0" edited="triangle_inequality_CauchySchwarzInequality_CauchySchwarz_1.v"><result status="valid" time="0.60"/></proof>
+ <proof prover="2" edited="triangle_inequality_CauchySchwarzInequality_CauchySchwarz_1.v"><result status="valid" time="1.03"/></proof>
 </goal>
 </theory>
 <theory name="TriangleInequality" sum="0e6e449288baab6d459040c11cfc2eb5" expanded="true">
@@ -443,7 +443,7 @@
 <proof prover="11"><result status="valid" time="0.04"/></proof>
 </goal>
 <goal name="triangle">
- <proof prover="0" edited="triangle_inequality_TriangleInequality_triangle_1.v"><result status="valid" time="0.60"/></proof>
+ <proof prover="2" edited="triangle_inequality_TriangleInequality_triangle_1.v"><result status="valid" time="0.92"/></proof>
 </goal>
 </theory>
 </file>

--- a/examples/nightly-bench.sh
+++ b/examples/nightly-bench.sh
@@ -103,7 +103,7 @@ target_name = "Coq"
 target_version = "$COQVER"
 version = "8.4pl5"

-[uninstalled_prover policy2]
+[uninstalled_prover policy3]
 alternative = ""
 name = "Coq"
 policy = "upgrade"
@@ -112,6 +112,15 @@ target_name = "Coq"
 target_version = "$COQVER"
 version = "8.4pl6"

+[uninstalled_prover policy4]
+alternative = ""
+name = "Coq"
+policy = "upgrade"
+target_alternative = ""
+target_name = "Coq"
+target_version = "$COQVER"
+version = "8.5"
+
 EOF
 fi


--- a/examples/stdlib/list/why3session.xml
+++ b/examples/stdlib/list/why3session.xml
@@ -7,7 +7,7 @@
 <prover id="2" name="CVC4" version="1.4" timelimit="5" steplimit="1" memlimit="1000"/>
 <prover id="3" name="Spass" version="3.7" timelimit="5" steplimit="1" memlimit="1000"/>
 <prover id="4" name="Eprover" version="1.8-001" timelimit="5" steplimit="1" memlimit="1000"/>
-<prover id="5" name="Coq" version="8.5" timelimit="5" steplimit="1" memlimit="4000"/>
+<prover id="6" name="Coq" version="8.4pl6" timelimit="5" steplimit="1" memlimit="4000"/>
 <file name="../../../theories/list.why" expanded="true">
 <theory name="List" sum="d41d8cd98f00b204e9800998ecf8427e">
 </theory>
@@ -110,7 +110,7 @@
 <goal name="mem_append">
 <transf name="induction_ty_lex">
  <goal name="mem_append.1" expl="1.">
-  <proof prover="0"><result status="valid" time="0.21" steps="184"/></proof>
+  <proof prover="0"><result status="valid" time="0.06" steps="184"/></proof>
  </goal>
 </transf>
 </goal>
@@ -149,7 +149,7 @@
 <goal name="reverse_append">
 <transf name="induction_ty_lex">
  <goal name="reverse_append.1" expl="1.">
-  <proof prover="0"><result status="valid" time="0.59" steps="254"/></proof>
+  <proof prover="0"><result status="valid" time="0.29" steps="254"/></proof>
  </goal>
 </transf>
 </goal>
@@ -254,16 +254,16 @@
   <proof prover="0"><result status="valid" time="0.00" steps="10"/></proof>
   </goal>
   <goal name="sorted_append.1.5" expl="5.">
-   <proof prover="2"><result status="valid" time="0.38"/></proof>
+   <proof prover="2"><result status="valid" time="0.16"/></proof>
   </goal>
   <goal name="sorted_append.1.6" expl="6.">
-   <proof prover="2"><result status="valid" time="3.89"/></proof>
+   <proof prover="2"><result status="valid" time="1.63"/></proof>
   </goal>
   <goal name="sorted_append.1.7" expl="7.">
   <proof prover="0"><result status="valid" time="0.03" steps="80"/></proof>
   </goal>
   <goal name="sorted_append.1.8" expl="8.">
-   <proof prover="1"><result status="valid" time="4.11"/></proof>
+   <proof prover="1"><result status="valid" time="1.63"/></proof>
   </goal>
  </transf>
  </goal>
@@ -305,10 +305,10 @@
   <proof prover="0"><result status="valid" time="0.15" steps="142"/></proof>
   </goal>
   <goal name="rev_append_sorted_incr.1.7" expl="7.">
-   <proof prover="4"><result status="valid" time="1.31"/></proof>
+   <proof prover="4"><result status="valid" time="0.53"/></proof>
   </goal>
   <goal name="rev_append_sorted_incr.1.8" expl="8.">
-   <proof prover="4"><result status="valid" time="3.04"/></proof>
+   <proof prover="4"><result status="valid" time="1.13"/></proof>
   </goal>
  </transf>
  </goal>
@@ -390,7 +390,7 @@
 <goal name="reverse_num_occ">
 <transf name="induction_ty_lex">
  <goal name="reverse_num_occ.1" expl="1.">
-  <proof prover="0"><result status="valid" time="0.43" steps="468"/></proof>
+  <proof prover="0"><result status="valid" time="0.20" steps="468"/></proof>
  </goal>
 </transf>
 </goal>
@@ -412,7 +412,7 @@
 <proof prover="0"><result status="valid" time="0.22" steps="380"/></proof>
 </goal>
 <goal name="Permut_cons_append">
- <proof prover="0"><result status="valid" time="0.31" steps="165"/></proof>
+ <proof prover="0"><result status="valid" time="0.16" steps="165"/></proof>
 </goal>
 <goal name="Permut_assoc">
 <proof prover="0"><result status="valid" time="0.01" steps="10"/></proof>
@@ -427,7 +427,7 @@
 <proof prover="0"><result status="valid" time="0.01" steps="10"/></proof>
 </goal>
 <goal name="Permut_length">
- <proof prover="5" edited="list_Permut_Permut_length_2.v"><result status="valid" time="1.69"/></proof>
+ <proof prover="6" edited="list_Permut_Permut_length_2.v"><result status="valid" time="2.25"/></proof>
 </goal>
 </theory>
 <theory name="Distinct" sum="e56aed12f61edef3656befad5f86e1ba">
@@ -439,7 +439,7 @@
   <proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
   </goal>
   <goal name="distinct_append.1.2" expl="2.">
-   <proof prover="2"><result status="valid" time="2.18"/></proof>
+   <proof prover="2"><result status="valid" time="0.91"/></proof>
   </goal>
  </transf>
  </goal>

--- a/examples/tests-provers/coq-interval/why3session.xml
+++ b/examples/tests-provers/coq-interval/why3session.xml
@@ -2,11 +2,11 @@
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="4">
-<prover id="0" name="Coq" version="8.5" timelimit="5" steplimit="1" memlimit="1000"/>
+<prover id="1" name="Coq" version="8.4pl6" timelimit="5" steplimit="1" memlimit="1000"/>
 <file name="../coq-interval.why" expanded="true">
 <theory name="P" sum="e9497a01253e3a23bfd449128777d698" expanded="true">
 <goal name="pow_eps2_max_int" expanded="true">
- <proof prover="0" edited="coqmninterval_P_pow_eps2_max_int_1.v"><result status="valid" time="3.13"/></proof>
+ <proof prover="1" edited="coqmninterval_P_pow_eps2_max_int_1.v"><result status="valid" time="3.13"/></proof>
 </goal>
 </theory>
 </file>

--- a/examples/verifythis_fm2012_LRS/why3session.xml
+++ b/examples/verifythis_fm2012_LRS/why3session.xml
@@ -2,7 +2,7 @@
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="4">
-<prover id="0" name="Coq" version="8.5" timelimit="5" steplimit="1" memlimit="4000"/>
+<prover id="1" name="Coq" version="8.4pl6" timelimit="5" steplimit="1" memlimit="4000"/>
 <prover id="3" name="CVC3" version="2.4.1" timelimit="10" steplimit="1" memlimit="4000"/>
 <prover id="11" name="Vampire" version="0.6" timelimit="5" steplimit="1" memlimit="4000"/>
 <prover id="12" name="Alt-Ergo" version="0.99.1" timelimit="10" steplimit="1" memlimit="4000"/>
@@ -532,7 +532,7 @@
 <proof prover="15"><result status="valid" time="0.01"/></proof>
 </goal>
 <goal name="permut_permutation">
- <proof prover="0" timelimit="6" memlimit="1000" edited="verifythis_fm2012_lcp_SuffixArray_permut_permutation_1.v"><result status="valid" time="2.26"/></proof>
+ <proof prover="1" timelimit="6" memlimit="1000" edited="verifythis_fm2012_lcp_SuffixArray_permut_permutation_1.v"><result status="valid" time="1.12"/></proof>
 </goal>
 <goal name="WP_parameter create" expl="VC for create">
 <transf name="split_goal_wp">
@@ -621,7 +621,7 @@
  </goal>
  <goal name="WP_parameter create.12" expl="12. type invariant">
  <proof prover="3" memlimit="1000"><result status="valid" time="0.10"/></proof>
-  <proof prover="11"><result status="valid" time="4.28"/></proof>
+  <proof prover="11"><result status="valid" time="3.51"/></proof>
  <proof prover="12" memlimit="1000"><result status="valid" time="0.08" steps="76"/></proof>
  <proof prover="14" memlimit="1000"><result status="valid" time="0.06"/></proof>
  </goal>
@@ -643,7 +643,7 @@
  </goal>
  <goal name="WP_parameter lcp.3" expl="3. precondition">
  <proof prover="3" memlimit="1000"><result status="valid" time="0.05"/></proof>
-  <proof prover="11"><result status="valid" time="3.62"/></proof>
+  <proof prover="11"><result status="valid" time="3.00"/></proof>
  <proof prover="12" memlimit="1000"><result status="valid" time="0.01" steps="17"/></proof>
  <proof prover="13" memlimit="1000"><result status="valid" time="0.06"/></proof>
  <proof prover="14" memlimit="1000"><result status="valid" time="0.02"/></proof>
@@ -752,7 +752,7 @@
  </goal>
  <goal name="WP_parameter lrs.11" expl="11. precondition">
  <proof prover="3" memlimit="1000"><result status="valid" time="0.02"/></proof>
-  <proof prover="11"><result status="valid" time="3.56"/></proof>
+  <proof prover="11"><result status="valid" time="2.93"/></proof>
  <proof prover="12" memlimit="1000"><result status="valid" time="0.01" steps="23"/></proof>
  <proof prover="13" memlimit="1000"><result status="valid" time="0.04"/></proof>
  <proof prover="14" memlimit="1000"><result status="valid" time="0.04"/></proof>
@@ -774,11 +774,11 @@
  </goal>
  <goal name="WP_parameter lrs.14" expl="14. loop invariant preservation">
  <proof prover="3" memlimit="1000"><result status="valid" time="0.16"/></proof>
-  <proof prover="11"><result status="valid" time="3.78"/></proof>
+  <proof prover="11"><result status="valid" time="3.25"/></proof>
  <proof prover="12" memlimit="1000"><result status="valid" time="0.02" steps="45"/></proof>
  <proof prover="13" memlimit="1000"><result status="valid" time="0.05"/></proof>
  <proof prover="14" memlimit="1000"><result status="valid" time="0.04"/></proof>
-  <proof prover="15"><result status="valid" time="0.50"/></proof>
+  <proof prover="15"><result status="valid" time="0.31"/></proof>
  </goal>
  <goal name="WP_parameter lrs.15" expl="15. loop invariant preservation">
  <proof prover="3" memlimit="1000"><result status="valid" time="0.17"/></proof>
@@ -820,17 +820,17 @@
  <proof prover="15"><result status="valid" time="0.01"/></proof>
  </goal>
  <goal name="WP_parameter lrs.21" expl="21. loop invariant preservation">
-  <proof prover="3" memlimit="1000"><result status="valid" time="2.92"/></proof>
+  <proof prover="3" memlimit="1000"><result status="valid" time="2.15"/></proof>
  <proof prover="14" memlimit="1000"><result status="valid" time="0.04"/></proof>
  </goal>
  <goal name="WP_parameter lrs.22" expl="22. assertion">
  <proof prover="3" memlimit="1000"><result status="valid" time="0.15"/></proof>
  <proof prover="12" memlimit="1000"><result status="valid" time="0.03" steps="54"/></proof>
  <proof prover="14" memlimit="1000"><result status="valid" time="0.05"/></proof>
-  <proof prover="15"><result status="valid" time="1.81"/></proof>
+  <proof prover="15"><result status="valid" time="1.10"/></proof>
  </goal>
  <goal name="WP_parameter lrs.23" expl="23. assertion">
-  <proof prover="0" memlimit="1000" edited="verifythis_fm2012_lcp_LRS_WP_parameter_lrs_10.v"><result status="valid" time="0.98"/></proof>
+  <proof prover="1" memlimit="1000" edited="verifythis_fm2012_lcp_LRS_WP_parameter_lrs_10.v"><result status="valid" time="1.61"/></proof>
  </goal>
  <goal name="WP_parameter lrs.24" expl="24. postcondition">
  <proof prover="3" memlimit="1000"><result status="valid" time="0.02"/></proof>
@@ -856,7 +856,7 @@
  <proof prover="15"><result status="valid" time="0.01"/></proof>
  </goal>
  <goal name="WP_parameter lrs.27" expl="27. postcondition">
-  <proof prover="0" edited="verifythis_fm2012_lcp_LRS_WP_parameter_lrs_12.v"><result status="valid" time="0.81"/></proof>
+  <proof prover="1" edited="verifythis_fm2012_lcp_LRS_WP_parameter_lrs_12.v"><result status="valid" time="1.31"/></proof>
  </goal>
 </transf>
 </goal>