update sessions

examples/WP_revisited/wp2/why3session.xml

@@ -120,7 +120,7 @@
  <proof prover="2"><result status="valid" time="0.08" steps="267"/></proof>
  </goal>
  <goal name="assign_rule" proved="true">
- <proof prover="2"><result status="valid" time="0.56" steps="1816"/></proof>
+ <proof prover="2"><result status="valid" time="0.72" steps="1816"/></proof>
  </goal>
  <goal name="seq_rule" proved="true">
  <proof prover="2"><result status="valid" time="0.14" steps="407"/></proof>

examples/avl/tables/why3session.xml

@@ -793,7 +793,7 @@
      <proof prover="5" timelimit="5"><result status="valid" time="0.26" steps="937"/></proof>
      </goal>
      <goal name="VC symdiff.11.1.1.1" expl="postcondition" proved="true">
-     <proof prover="5" timelimit="5"><result status="valid" time="0.94" steps="3532"/></proof>
+     <proof prover="5" timelimit="5"><result status="valid" time="1.17" steps="3532"/></proof>
      </goal>
     </transf>
     </goal>

examples/bitcount/why3session.xml

@@ -450,7 +450,7 @@
   <proof prover="6"><result status="valid" time="0.04" steps="87"/></proof>
   </goal>
   <goal name="VC proof3.8" expl="assertion" proved="true">
-  <proof prover="2"><result status="valid" time="0.71"/></proof>
+  <proof prover="2"><result status="valid" time="0.51"/></proof>
   <proof prover="4"><result status="valid" time="0.10"/></proof>
   <proof prover="6"><result status="valid" time="0.05" steps="114"/></proof>
   </goal>
@@ -581,7 +581,7 @@
  <transf name="split_goal_right" proved="true" >
   <goal name="VC count.0" expl="precondition" proved="true">
   <proof prover="0"><result status="valid" time="0.02"/></proof>
-  <proof prover="2"><result status="valid" time="0.23"/></proof>
+  <proof prover="2"><result status="valid" time="0.10"/></proof>
   <proof prover="4"><result status="valid" time="0.08"/></proof>
   <proof prover="5"><result status="valid" time="0.04"/></proof>
   <proof prover="6"><result status="valid" time="0.04" steps="84"/></proof>
@@ -759,7 +759,7 @@
   <proof prover="5"><result status="valid" time="0.04"/></proof>
   </goal>
   <goal name="VC count_or.3" expl="assertion" proved="true">
-  <proof prover="4"><result status="valid" time="1.70"/></proof>
+  <proof prover="4"><result status="valid" time="2.02"/></proof>
   </goal>
   <goal name="VC count_or.4" expl="postcondition" proved="true">
   <proof prover="0"><result status="valid" time="0.08"/></proof>

examples/bitvector_examples/why3session.xml

@@ -134,7 +134,7 @@
  <goal name="VC bp1" expl="VC for bp1" proved="true">
  <proof prover="4"><result status="valid" time="0.02"/></proof>
  </goal>
- <goal name="VC bp1&#39;" expl="VC for bp1'" proved="true">
+ <goal name="VC bp1&#39;" expl="VC for bp1&#39;" proved="true">
  <proof prover="4"><result status="valid" time="0.01"/></proof>
  </goal>
  <goal name="VC bp2" expl="VC for bp2" proved="true">

examples/bitvectors/bitvector/why3session.xml

@@ -214,7 +214,7 @@
  <proof prover="4" timelimit="30"><result status="valid" time="4.30" steps="1784"/></proof>
  </goal>
  <goal name="to_nat_0x00001FFF" proved="true">
- <proof prover="4" timelimit="30"><result status="valid" time="5.03" steps="1718"/></proof>
+ <proof prover="4" timelimit="30"><result status="valid" time="4.16" steps="1718"/></proof>
  </goal>
  <goal name="to_nat_0x00003FFF" proved="true">
  <proof prover="4" timelimit="30"><result status="valid" time="3.62" steps="1603"/></proof>
@@ -232,7 +232,7 @@
  <proof prover="6" timelimit="30"><result status="valid" time="1.64"/></proof>
  </goal>
  <goal name="to_nat_0x0007FFFF" proved="true">
- <proof prover="6" timelimit="30"><result status="valid" time="1.57"/></proof>
+ <proof prover="6" timelimit="30"><result status="valid" time="1.13"/></proof>
  </goal>
  <goal name="to_nat_0x000FFFFF" proved="true">
  <proof prover="6" timelimit="30"><result status="valid" time="0.94"/></proof>

examples/bitvectors/double_of_int/why3session.xml

@@ -180,7 +180,7 @@
  <proof prover="8"><result status="valid" time="0.19"/></proof>
  </goal>
  <goal name="from_int2c_to_nat_sub_neg" proved="true">
- <proof prover="5" timelimit="5" edited="double_of_int_DoubleOfInt_from_int2c_to_nat_sub_neg_1.v"><result status="valid" time="0.86"/></proof>
+ <proof prover="5" timelimit="5" edited="double_of_int_DoubleOfInt_from_int2c_to_nat_sub_neg_1.v"><result status="valid" time="0.66"/></proof>
  </goal>
  <goal name="lemma1_neg" proved="true">
  <transf name="split_all_full" proved="true" >
@@ -240,7 +240,7 @@
    <goal name="lemma2.0.0" proved="true">
    <transf name="inline_goal" proved="true" >
     <goal name="lemma2.0.0.0" proved="true">
-    <proof prover="11" timelimit="30" memlimit="4000"><result status="valid" time="4.63"/></proof>
+    <proof prover="11" timelimit="30" memlimit="4000"><result status="valid" time="4.04"/></proof>
     </goal>
    </transf>
    </goal>
@@ -357,14 +357,14 @@
  <proof prover="2"><result status="valid" time="0.22"/></proof>
  <proof prover="4"><result status="valid" time="0.09"/></proof>
  <proof prover="6"><result status="valid" time="0.00"/></proof>
- <proof prover="8"><result status="valid" time="0.94"/></proof>
+ <proof prover="8"><result status="valid" time="0.73"/></proof>
  <proof prover="10"><result status="valid" time="0.07" steps="97"/></proof>
  </goal>
  <goal name="MainResult" proved="true">
  <proof prover="2"><result status="valid" time="0.26"/></proof>
  <proof prover="4"><result status="valid" time="3.62"/></proof>
  <proof prover="6" timelimit="11"><result status="valid" time="3.12"/></proof>
- <proof prover="8"><result status="valid" time="0.95"/></proof>
+ <proof prover="8"><result status="valid" time="0.74"/></proof>
  <proof prover="10"><result status="valid" time="0.26" steps="146"/></proof>
  </goal>
 </theory>

examples/bitvectors/power2/why3session.xml

@@ -591,7 +591,7 @@
    <proof prover="5"><result status="valid" time="0.02"/></proof>
    </goal>
    <goal name="Pow2_int_real.0.1" expl="recursive case" proved="true">
-   <transf name="replace" proved="true" arg1="x" arg2="((x-'1)+'1)">
+   <transf name="replace" proved="true" arg1="x" arg2="((x-&#39;1)+&#39;1)">
     <goal name="Pow2_int_real.0.1.0" expl="recursive case" proved="true">
     <proof prover="7" timelimit="1"><result status="valid" time="0.12" steps="135"/></proof>
     </goal>

examples/bts/13375/why3session.xml

@@ -3,11 +3,9 @@
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="4">
 <prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
-<file name="../13375.mlw" expanded="true">
-<theory name="Signed" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
-</theory>
-<theory name="Spec" sum="21786b3b1a47d0fdba2fd0d1a15299f4" expanded="true">
- <goal name="VC to_int_" expl="VC for to_int_" expanded="true">
+<file name="../13375.mlw" proved="true">
+<theory name="Spec" proved="true">
+ <goal name="VC to_int_" expl="VC for to_int_" proved="true">
  <proof prover="1"><result status="valid" time="0.00" steps="2"/></proof>
  </goal>
 </theory>

examples/bts/138/why3session.xml

@@ -8,7 +8,7 @@
  </goal>
 </theory>
 <theory name="Test2">
- <goal name="VC f" expl="VC for f">
+ <goal name="VC f">
  </goal>
 </theory>
 </file>

examples/bts/20445/why3session.xml

@@ -4,9 +4,7 @@
 <why3session shape_version="4">
 <prover id="0" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
 <file name="../20445.mlw">
-<theory name="A" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e">
-</theory>
-<theory name="B" sum="dfd8f3fdf296078f4789df7fcaac1191">
+<theory name="B">
  <goal name="G">
  <proof prover="0" timelimit="1"><result status="unknown" time="0.00"/></proof>
  </goal>

examples/bts/71_disambiguation/why3session.xml

@@ -16,7 +16,7 @@
  <proof prover="0"><result status="valid" time="0.00"/></proof>
  <transf name="cut" arg1="(0 + 0 = 2)">
   <goal name="g.0">
-  <transf name="cut" arg1="(1.0 +' 1.3 = 2.2)">
+  <transf name="cut" arg1="(1.0 +&#39; 1.3 = 2.2)">
    <goal name="g.0.0">
    </goal>
    <goal name="g.0.1">

examples/bts/fsetint/why3session.xml

@@ -25,7 +25,7 @@
  <proof prover="1"><result status="unknown" time="0.01"/></proof>
  <proof prover="4"><result status="timeout" time="1.00"/></proof>
  <proof prover="5"><result status="unknown" time="0.00"/></proof>
- <proof prover="6"><result status="timeout" time="2.00"/></proof>
+ <proof prover="6"><result status="timeout" time="1.00"/></proof>
  <proof prover="7"><result status="timeout" time="1.00"/></proof>
  </goal>
  <goal name="foo">

examples/check-builtin/int/why3session.xml

@@ -15,7 +15,7 @@
  <proof prover="1"><result status="valid" time="0.00"/></proof>
  <proof prover="4"><result status="timeout" time="1.00"/></proof>
  <proof prover="5"><result status="valid" time="0.00"/></proof>
- <proof prover="6"><result status="timeout" time="2.00"/></proof>
+ <proof prover="6"><result status="timeout" time="1.00"/></proof>
  <proof prover="7"><result status="valid" time="0.00" steps="0"/></proof>
  <proof prover="8"><result status="timeout" time="1.00"/></proof>
  <proof prover="9"><result status="valid" time="0.00"/></proof>
@@ -24,7 +24,7 @@
  <proof prover="1"><result status="valid" time="0.00"/></proof>
  <proof prover="4"><result status="timeout" time="1.00"/></proof>
  <proof prover="5"><result status="valid" time="0.00"/></proof>
- <proof prover="6"><result status="timeout" time="2.00"/></proof>
+ <proof prover="6"><result status="timeout" time="1.00"/></proof>
  <proof prover="7"><result status="valid" time="0.00" steps="0"/></proof>
  <proof prover="8"><result status="timeout" time="1.00"/></proof>
  <proof prover="9"><result status="valid" time="0.00"/></proof>
@@ -78,7 +78,7 @@
  <proof prover="1"><result status="valid" time="0.00"/></proof>
  <proof prover="4"><result status="timeout" time="1.00"/></proof>
  <proof prover="5"><result status="valid" time="0.00"/></proof>
- <proof prover="6"><result status="timeout" time="2.00"/></proof>
+ <proof prover="6"><result status="timeout" time="1.00"/></proof>
  <proof prover="7"><result status="valid" time="0.00" steps="1"/></proof>
  <proof prover="8"><result status="valid" time="0.58"/></proof>
  <proof prover="9"><result status="valid" time="0.00"/></proof>
@@ -87,7 +87,7 @@
  <proof prover="1"><result status="valid" time="0.00"/></proof>
  <proof prover="4"><result status="timeout" time="1.00"/></proof>
  <proof prover="5"><result status="valid" time="0.00"/></proof>
- <proof prover="6"><result status="timeout" time="2.00"/></proof>
+ <proof prover="6"><result status="timeout" time="1.00"/></proof>
  <proof prover="7"><result status="valid" time="0.00" steps="0"/></proof>
  <proof prover="8"><result status="valid" time="0.09"/></proof>
  <proof prover="9"><result status="valid" time="0.00"/></proof>
@@ -107,7 +107,7 @@
  <proof prover="1"><result status="valid" time="0.00"/></proof>
  <proof prover="4"><result status="timeout" time="1.00"/></proof>
  <proof prover="5"><result status="valid" time="0.01"/></proof>
- <proof prover="6"><result status="timeout" time="2.00"/></proof>
+ <proof prover="6"><result status="timeout" time="1.00"/></proof>
  <proof prover="7"><result status="valid" time="0.00" steps="5"/></proof>
  <proof prover="8"><result status="timeout" time="1.00"/></proof>
  <proof prover="9"><result status="valid" time="0.01"/></proof>

examples/edit_distance/why3session.xml

@@ -144,10 +144,10 @@
   <proof prover="3"><result status="valid" time="0.04"/></proof>
   </goal>
   <goal name="VC distance.5" expl="index in array bounds" proved="true">
-  <proof prover="11"><result status="valid" time="0.02"/></proof>
+  <proof prover="11"><result status="valid" time="0.03"/></proof>
   </goal>
   <goal name="VC distance.6" expl="index in array bounds" proved="true">
-  <proof prover="11"><result status="valid" time="0.03"/></proof>
+  <proof prover="11"><result status="valid" time="0.02"/></proof>
   </goal>
   <goal name="VC distance.7" expl="index in array bounds" proved="true">
   <proof prover="11"><result status="valid" time="0.03"/></proof>

examples/esterel/why3session.xml

@@ -15,7 +15,7 @@
  <proof prover="6"><result status="valid" time="0.16" steps="221"/></proof>
  </goal>
  <goal name="VC intersection" expl="VC for intersection" proved="true">
- <proof prover="6"><result status="valid" time="0.18" steps="189"/></proof>
+ <proof prover="6"><result status="valid" time="0.06" steps="189"/></proof>
  </goal>
  <goal name="VC aboveMin" expl="VC for aboveMin" proved="true">
  <transf name="split_goal_right" proved="true" >

examples/isqrt_von_neumann/why3session.xml

@@ -223,7 +223,7 @@
   <proof prover="3"><result status="valid" time="0.14"/></proof>
   </goal>
   <goal name="VC isqrt32.22" expl="loop invariant preservation" proved="true">
-  <proof prover="3"><result status="valid" time="0.75"/></proof>
+  <proof prover="3"><result status="valid" time="0.49"/></proof>
   </goal>
   <goal name="VC isqrt32.23" expl="loop invariant preservation" proved="true">
   <proof prover="3"><result status="valid" time="0.52"/></proof>
@@ -271,7 +271,7 @@
   <proof prover="3"><result status="valid" time="0.14"/></proof>
   </goal>
   <goal name="VC isqrt32.33" expl="loop invariant preservation" proved="true">
-  <proof prover="3"><result status="valid" time="0.70"/></proof>
+  <proof prover="3"><result status="valid" time="0.51"/></proof>
   </goal>
   <goal name="VC isqrt32.34" expl="loop invariant preservation" proved="true">
   <proof prover="3"><result status="valid" time="0.30"/></proof>
@@ -292,7 +292,7 @@
   <proof prover="3"><result status="valid" time="0.12"/></proof>
   </goal>
   <goal name="VC isqrt32.40" expl="loop invariant preservation" proved="true">
-  <proof prover="3" timelimit="120"><result status="valid" time="113.76"/></proof>
+  <proof prover="3" timelimit="120"><result status="valid" time="86.22"/></proof>
   </goal>
   <goal name="VC isqrt32.41" expl="postcondition" proved="true">
   <proof prover="3"><result status="valid" time="0.16"/></proof>
@@ -356,19 +356,19 @@
   <proof prover="3"><result status="valid" time="0.01"/></proof>
   </goal>
   <goal name="VC isqrt64.14" expl="assertion" proved="true">
-  <proof prover="3"><result status="valid" time="0.68"/></proof>
+  <proof prover="3"><result status="valid" time="0.49"/></proof>
   </goal>
   <goal name="VC isqrt64.15" expl="assertion" proved="true">
-  <proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="1.46"/></proof>
+  <proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="0.98"/></proof>
   </goal>
   <goal name="VC isqrt64.16" expl="assertion" proved="true">
-  <proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="1.96"/></proof>
+  <proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="1.20"/></proof>
   </goal>
   <goal name="VC isqrt64.17" expl="assertion" proved="true">
-  <proof prover="3" timelimit="5"><result status="valid" time="1.33"/></proof>
+  <proof prover="3" timelimit="5"><result status="valid" time="0.91"/></proof>
   </goal>
   <goal name="VC isqrt64.18" expl="assertion" proved="true">
-  <proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="2.47"/></proof>
+  <proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="1.58"/></proof>
   </goal>
   <goal name="VC isqrt64.19" expl="loop variant decrease" proved="true">
   <transf name="split_goal_right" proved="true" >
@@ -376,12 +376,12 @@
    <proof prover="3"><result status="valid" time="0.43"/></proof>
    </goal>
    <goal name="VC isqrt64.19.1" expl="VC for isqrt64" proved="true">
-   <proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="1.69"/></proof>
+   <proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="1.17"/></proof>
    </goal>
   </transf>
   </goal>
   <goal name="VC isqrt64.20" expl="loop invariant preservation" proved="true">
-  <proof prover="3"><result status="valid" time="0.55"/></proof>
+  <proof prover="3"><result status="valid" time="0.36"/></proof>
   </goal>
   <goal name="VC isqrt64.21" expl="loop invariant preservation" proved="true">
   <proof prover="3"><result status="valid" time="0.50"/></proof>
@@ -390,7 +390,7 @@
   <proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="2.54"/></proof>
   </goal>
   <goal name="VC isqrt64.23" expl="loop invariant preservation" proved="true">
-  <proof prover="3" timelimit="60"><result status="valid" time="2.15"/></proof>
+  <proof prover="3" timelimit="60"><result status="valid" time="1.70"/></proof>
   </goal>
   <goal name="VC isqrt64.24" expl="loop invariant preservation" proved="true">
   <proof prover="3"><result status="valid" time="0.50"/></proof>
@@ -399,7 +399,7 @@
   <proof prover="3"><result status="valid" time="0.01"/></proof>
   </goal>
   <goal name="VC isqrt64.26" expl="loop invariant preservation" proved="true">
-  <proof prover="3"><result status="valid" time="1.08"/></proof>
+  <proof prover="3"><result status="valid" time="0.75"/></proof>
   </goal>
   <goal name="VC isqrt64.27" expl="loop invariant preservation" proved="true">
   <transf name="introduce_premises" proved="true" >
@@ -423,7 +423,7 @@
   <proof prover="3"><result status="valid" time="0.51"/></proof>
   </goal>
   <goal name="VC isqrt64.29" expl="loop invariant preservation" proved="true">
-  <proof prover="3"><result status="valid" time="0.72"/></proof>
+  <proof prover="3"><result status="valid" time="0.54"/></proof>
   </goal>
   <goal name="VC isqrt64.30" expl="loop variant decrease" proved="true">
   <transf name="split_goal_right" proved="true" >
@@ -431,7 +431,7 @@
    <proof prover="3"><result status="valid" time="0.42"/></proof>
    </goal>
    <goal name="VC isqrt64.30.1" expl="VC for isqrt64" proved="true">
-   <proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="1.55"/></proof>
+   <proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="1.22"/></proof>
    </goal>
   </transf>
   </goal>
@@ -439,13 +439,13 @@
   <proof prover="3"><result status="valid" time="0.45"/></proof>
   </goal>
   <goal name="VC isqrt64.32" expl="loop invariant preservation" proved="true">
-  <proof prover="3"><result status="valid" time="0.64"/></proof>
+  <proof prover="3"><result status="valid" time="0.37"/></proof>
   </goal>
   <goal name="VC isqrt64.33" expl="loop invariant preservation" proved="true">
-  <proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="2.61"/></proof>
+  <proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="2.20"/></proof>
   </goal>
   <goal name="VC isqrt64.34" expl="loop invariant preservation" proved="true">
-  <proof prover="3"><result status="valid" time="1.38"/></proof>
+  <proof prover="3"><result status="valid" time="1.00"/></proof>
   </goal>
   <goal name="VC isqrt64.35" expl="loop invariant preservation" proved="true">
   <proof prover="3"><result status="valid" time="0.01"/></proof>
@@ -460,7 +460,7 @@
   <proof prover="3"><result status="valid" time="0.01"/></proof>
   </goal>
   <goal name="VC isqrt64.39" expl="loop invariant preservation" proved="true">
-  <proof prover="3"><result status="valid" time="0.66"/></proof>
+  <proof prover="3"><result status="valid" time="0.40"/></proof>
   </goal>
   <goal name="VC isqrt64.40" expl="loop invariant preservation" proved="true">
   <transf name="introduce_premises" proved="true" >
@@ -529,7 +529,7 @@
                 <goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0.1.1" expl="false case" proved="true">
                 <transf name="case" proved="true" arg1="(res_g = (0:t))">