update some obsolete sessions

examples/binomial_heap/why3session.xml

@@ -179,7 +179,7 @@
  <goal name="VC merge" expl="VC for merge" proved="true">
  <transf name="split_goal_right" proved="true" >
   <goal name="VC merge.0" expl="variant decrease" proved="true">
-  <proof prover="1"><result status="valid" time="0.01" steps="39"/></proof>
+  <proof prover="1"><result status="valid" time="0.01" steps="38"/></proof>
   </goal>
   <goal name="VC merge.1" expl="precondition" proved="true">
   <proof prover="1"><result status="valid" time="0.01" steps="60"/></proof>
@@ -194,7 +194,7 @@
   <proof prover="1"><result status="valid" time="0.01" steps="74"/></proof>
   </goal>
   <goal name="VC merge.5" expl="variant decrease" proved="true">
-  <proof prover="1"><result status="valid" time="0.01" steps="41"/></proof>
+  <proof prover="1"><result status="valid" time="0.01" steps="39"/></proof>
   </goal>
   <goal name="VC merge.6" expl="precondition" proved="true">
   <proof prover="1"><result status="valid" time="0.01" steps="12"/></proof>

examples/coincidence_count_list/why3session.xml

@@ -9,7 +9,7 @@
  <proof prover="0"><result status="valid" time="0.00" steps="3"/></proof>
  </goal>
  <goal name="VC coincidence_count" expl="VC for coincidence_count" proved="true">
- <proof prover="0"><result status="valid" time="2.20" steps="9039"/></proof>
+ <proof prover="0"><result status="valid" time="2.20" steps="9025"/></proof>
  </goal>
 </theory>
 <theory name="CoincidenceCountAnyType" proved="true">
@@ -17,7 +17,7 @@
  <proof prover="0"><result status="valid" time="0.00" steps="4"/></proof>
  </goal>
  <goal name="VC coincidence_count" expl="VC for coincidence_count" proved="true">
- <proof prover="0"><result status="valid" time="0.65" steps="4378"/></proof>
+ <proof prover="0"><result status="valid" time="0.65" steps="4363"/></proof>
  </goal>
 </theory>
 <theory name="CoincidenceCountList" proved="true">
@@ -25,7 +25,7 @@
  <proof prover="0"><result status="valid" time="0.00" steps="3"/></proof>
  </goal>
  <goal name="VC coincidence_count" expl="VC for coincidence_count" proved="true">
- <proof prover="0"><result status="valid" time="0.15" steps="1018"/></proof>
+ <proof prover="0"><result status="valid" time="0.15" steps="991"/></proof>
  </goal>
 </theory>
 </file>

examples/gcd/why3session.xml

@@ -89,7 +89,7 @@
   <proof prover="6"><result status="valid" time="0.01" steps="10"/></proof>
   </goal>
   <goal name="VC binary_gcd.9" expl="variant decrease" proved="true">
-  <proof prover="6"><result status="valid" time="0.02" steps="15"/></proof>
+  <proof prover="6"><result status="valid" time="0.01" steps="15"/></proof>
   </goal>
   <goal name="VC binary_gcd.10" expl="precondition" proved="true">
   <proof prover="6"><result status="valid" time="0.01" steps="15"/></proof>
@@ -110,7 +110,7 @@
   <proof prover="6"><result status="valid" time="0.01" steps="10"/></proof>
   </goal>
   <goal name="VC binary_gcd.16" expl="variant decrease" proved="true">
-  <proof prover="6"><result status="valid" time="0.01" steps="17"/></proof>
+  <proof prover="6"><result status="valid" time="0.02" steps="17"/></proof>
   </goal>
   <goal name="VC binary_gcd.17" expl="precondition" proved="true">
   <proof prover="6"><result status="valid" time="0.01" steps="15"/></proof>

examples/gcd_vc_sp/why3session.xml

@@ -75,7 +75,7 @@
   <proof prover="2"><result status="valid" time="0.02"/></proof>
   </goal>
   <goal name="VC binary_gcd.9" expl="variant decrease" proved="true">
-  <proof prover="2"><result status="valid" time="0.05"/></proof>
+  <proof prover="2"><result status="valid" time="0.04"/></proof>
   </goal>
   <goal name="VC binary_gcd.10" expl="precondition" proved="true">
   <proof prover="2"><result status="valid" time="0.04"/></proof>
@@ -96,7 +96,7 @@
   <proof prover="2"><result status="valid" time="0.02"/></proof>
   </goal>
   <goal name="VC binary_gcd.16" expl="variant decrease" proved="true">
-  <proof prover="2"><result status="valid" time="0.04"/></proof>
+  <proof prover="2"><result status="valid" time="0.05"/></proof>
   </goal>
   <goal name="VC binary_gcd.17" expl="precondition" proved="true">
   <proof prover="2"><result status="valid" time="0.03"/></proof>

examples/prover/ISet/why3session.xml

@@ -74,7 +74,7 @@
   <proof prover="1"><result status="valid" time="0.04" steps="32"/></proof>
   </goal>
   <goal name="VC merge.3" expl="variant decrease" proved="true">
-  <proof prover="1"><result status="valid" time="0.01" steps="21"/></proof>
+  <proof prover="1"><result status="valid" time="0.01" steps="20"/></proof>
   </goal>
   <goal name="VC merge.4" expl="precondition" proved="true">
   <proof prover="1"><result status="valid" time="0.02" steps="15"/></proof>
@@ -86,7 +86,7 @@
   <proof prover="1"><result status="valid" time="0.04" steps="33"/></proof>
   </goal>
   <goal name="VC merge.7" expl="variant decrease" proved="true">
-  <proof prover="1"><result status="valid" time="0.01" steps="23"/></proof>
+  <proof prover="1"><result status="valid" time="0.01" steps="21"/></proof>
   </goal>
   <goal name="VC merge.8" expl="precondition" proved="true">
   <proof prover="1"><result status="valid" time="0.01" steps="8"/></proof>

examples/vstte12_tree_reconstruction/why3session.xml

@@ -49,7 +49,7 @@
   <proof prover="0"><result status="valid" time="0.01" steps="32"/></proof>
   </goal>
   <goal name="VC build_rec.3" expl="variant decrease" proved="true">
-  <proof prover="0"><result status="valid" time="0.02" steps="9"/></proof>
+  <proof prover="0"><result status="valid" time="0.02" steps="6"/></proof>
   </goal>
   <goal name="VC build_rec.4" expl="variant decrease" proved="true">
   <proof prover="0"><result status="valid" time="0.03" steps="61"/></proof>