From 2b45658af3c8554c145a5624379f35f07166305c Mon Sep 17 00:00:00 2001
From: Claude Marche <Claude.Marche@inria.fr>
Date: Sun, 18 Jun 2017 18:56:58 +0200
Subject: [PATCH] fix sessions for nightly replay

---
 examples/mergesort_queue/why3session.xml  | 135 +++-------------------
 examples/tests-provers/bv/why3session.xml |  25 ++--
 2 files changed, 29 insertions(+), 131 deletions(-)

diff --git a/examples/mergesort_queue/why3session.xml b/examples/mergesort_queue/why3session.xml
index cee96726a..b1b102c10 100644
--- a/examples/mergesort_queue/why3session.xml
+++ b/examples/mergesort_queue/why3session.xml
@@ -2,265 +2,188 @@
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="4">
-<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
-<prover id="1" name="CVC3" version="2.4.1" timelimit="6" steplimit="0" memlimit="1000"/>
-<prover id="2" name="CVC4" version="1.4" timelimit="6" steplimit="0" memlimit="1000"/>
-<prover id="3" name="Coq" version="8.6" timelimit="10" steplimit="0" memlimit="0"/>
-<prover id="4" name="Alt-Ergo" version="1.20.prv" timelimit="1" steplimit="0" memlimit="1000"/>
-<prover id="5" name="Alt-Ergo" version="1.30" timelimit="2" steplimit="0" memlimit="1000"/>
-<prover id="6" name="Z3" version="4.4.1" timelimit="1" steplimit="0" memlimit="1000"/>
-<prover id="7" name="Z3" version="4.3.2" timelimit="6" steplimit="0" memlimit="1000"/>
+<prover id="2" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
+<prover id="5" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
+<prover id="8" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/>
 <file name="../mergesort_queue.mlw" expanded="true">
 <theory name="MergesortQueue" sum="3c38c1216cfab92b40972e70acecfeff" expanded="true">
  <goal name="Transitive.Trans" expl="">
- <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="5"/></proof>
  <proof prover="5"><result status="valid" time="0.01" steps="5"/></proof>
  </goal>
  <goal name="WP_parameter merge" expl="VC for merge">
  <transf name="split_goal_wp">
   <goal name="WP_parameter merge.1" expl="loop invariant init">
-  <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="4"/></proof>
   <proof prover="5"><result status="valid" time="0.01" steps="5"/></proof>
   </goal>
   <goal name="WP_parameter merge.2" expl="loop invariant init">
-  <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="11"/></proof>
   <proof prover="5"><result status="valid" time="0.01" steps="9"/></proof>
   </goal>
   <goal name="WP_parameter merge.3" expl="loop invariant init">
-  <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="11"/></proof>
   <proof prover="5"><result status="valid" time="0.01" steps="9"/></proof>
   </goal>
   <goal name="WP_parameter merge.4" expl="loop invariant init">
-  <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="20"/></proof>
   <proof prover="5"><result status="valid" time="0.01" steps="7"/></proof>
   </goal>
   <goal name="WP_parameter merge.5" expl="precondition">
-  <proof prover="0" obsolete="true"><result status="valid" time="0.01" steps="9"/></proof>
   <proof prover="5"><result status="valid" time="0.01" steps="10"/></proof>
   </goal>
   <goal name="WP_parameter merge.6" expl="loop invariant preservation">
-  <proof prover="0" obsolete="true"><result status="valid" time="0.01" steps="14"/></proof>
   <proof prover="5"><result status="valid" time="0.01" steps="10"/></proof>
   </goal>
   <goal name="WP_parameter merge.7" expl="loop invariant preservation">
-  <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="16"/></proof>
   <proof prover="5"><result status="valid" time="0.00" steps="10"/></proof>
   </goal>
   <goal name="WP_parameter merge.8" expl="loop invariant preservation">
-  <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="16"/></proof>
   <proof prover="5"><result status="valid" time="0.00" steps="10"/></proof>
   </goal>
   <goal name="WP_parameter merge.9" expl="loop invariant preservation">
-  <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="14"/></proof>
-  <proof prover="1" timelimit="10" memlimit="0" obsolete="true"><result status="valid" time="0.03"/></proof>
   <proof prover="5"><result status="valid" time="0.01" steps="10"/></proof>
   </goal>
   <goal name="WP_parameter merge.10" expl="loop variant decrease">
-  <proof prover="0" obsolete="true"><result status="valid" time="0.01" steps="14"/></proof>
   <proof prover="5"><result status="valid" time="0.01" steps="10"/></proof>
   </goal>
   <goal name="WP_parameter merge.11" expl="precondition">
-  <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="20"/></proof>
   <proof prover="5"><result status="valid" time="0.01" steps="13"/></proof>
   </goal>
   <goal name="WP_parameter merge.12" expl="loop invariant preservation">
-  <proof prover="2" obsolete="true"><result status="valid" time="0.22"/></proof>
-  <proof prover="5"><result status="valid" time="1.05" steps="2937"/></proof>
+  <proof prover="5"><result status="valid" time="1.05" steps="2499"/></proof>
   </goal>
   <goal name="WP_parameter merge.13" expl="loop invariant preservation">
-  <proof prover="2" obsolete="true"><result status="valid" time="0.08"/></proof>
-  <proof prover="5"><result status="valid" time="0.13" steps="416"/></proof>
+  <proof prover="5"><result status="valid" time="0.13" steps="518"/></proof>
   </goal>
   <goal name="WP_parameter merge.14" expl="loop invariant preservation">
-  <proof prover="0" obsolete="true"><result status="valid" time="0.12" steps="123"/></proof>
-  <proof prover="5"><result status="valid" time="0.03" steps="83"/></proof>
+  <proof prover="5"><result status="valid" time="0.03" steps="82"/></proof>
   </goal>
   <goal name="WP_parameter merge.15" expl="loop invariant preservation">
-  <proof prover="1" timelimit="5" obsolete="true"><result status="valid" time="0.09"/></proof>
   <proof prover="5"><result status="valid" time="0.17" steps="277"/></proof>
   </goal>
   <goal name="WP_parameter merge.16" expl="loop variant decrease">
-  <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="16"/></proof>
   <proof prover="5"><result status="valid" time="0.01" steps="21"/></proof>
   </goal>
   <goal name="WP_parameter merge.17" expl="precondition">
-  <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="20"/></proof>
   <proof prover="5"><result status="valid" time="0.01" steps="13"/></proof>
   </goal>
   <goal name="WP_parameter merge.18" expl="precondition">
-  <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="23"/></proof>
   <proof prover="5"><result status="valid" time="0.01" steps="16"/></proof>
   </goal>
   <goal name="WP_parameter merge.19" expl="precondition">
-  <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="18"/></proof>
   <proof prover="5"><result status="valid" time="0.01" steps="19"/></proof>
   </goal>
   <goal name="WP_parameter merge.20" expl="loop invariant preservation">
-  <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="44"/></proof>
   <proof prover="5"><result status="valid" time="0.97" steps="2701"/></proof>
   </goal>
   <goal name="WP_parameter merge.21" expl="loop invariant preservation">
-  <proof prover="0" obsolete="true"><result status="valid" time="0.03" steps="43"/></proof>
-  <proof prover="2" obsolete="true"><result status="valid" time="0.04"/></proof>
-  <proof prover="5"><result status="valid" time="0.15" steps="805"/></proof>
+  <proof prover="5"><result status="valid" time="0.15" steps="787"/></proof>
   </goal>
   <goal name="WP_parameter merge.22" expl="loop invariant preservation">
-  <proof prover="0" obsolete="true"><result status="valid" time="0.04" steps="43"/></proof>
-  <proof prover="2" obsolete="true"><result status="valid" time="0.04"/></proof>
-  <proof prover="5"><result status="timeout" time="2.00"/></proof>
-  <proof prover="6"><result status="valid" time="0.21"/></proof>
+  <proof prover="8"><result status="valid" time="0.13"/></proof>
   </goal>
   <goal name="WP_parameter merge.23" expl="loop invariant preservation">
-  <proof prover="0" obsolete="true"><result status="valid" time="0.06" steps="145"/></proof>
-  <proof prover="1" timelimit="10" memlimit="0" obsolete="true"><result status="valid" time="0.06"/></proof>
   <proof prover="5"><result status="valid" time="0.28" steps="308"/></proof>
   </goal>
   <goal name="WP_parameter merge.24" expl="loop variant decrease">
-  <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="40"/></proof>
   <proof prover="5"><result status="valid" time="0.02" steps="73"/></proof>
   </goal>
   <goal name="WP_parameter merge.25" expl="precondition">
-  <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="18"/></proof>
   <proof prover="5"><result status="valid" time="0.01" steps="19"/></proof>
   </goal>
   <goal name="WP_parameter merge.26" expl="loop invariant preservation">
-  <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="44"/></proof>
-  <proof prover="5"><result status="valid" time="1.16" steps="3073"/></proof>
+  <proof prover="5"><result status="valid" time="0.90" steps="2989"/></proof>
   </goal>
   <goal name="WP_parameter merge.27" expl="loop invariant preservation">
-  <proof prover="0" obsolete="true"><result status="valid" time="0.03" steps="43"/></proof>
-  <proof prover="2" obsolete="true"><result status="valid" time="0.04"/></proof>
-  <proof prover="5"><result status="timeout" time="2.00"/></proof>
-  <proof prover="6"><result status="valid" time="0.22"/></proof>
+  <proof prover="8"><result status="valid" time="0.14"/></proof>
   </goal>
   <goal name="WP_parameter merge.28" expl="loop invariant preservation">
-  <proof prover="0" obsolete="true"><result status="valid" time="0.03" steps="43"/></proof>
-  <proof prover="2" obsolete="true"><result status="valid" time="0.04"/></proof>
-  <proof prover="5"><result status="valid" time="0.15" steps="787"/></proof>
+  <proof prover="5"><result status="valid" time="0.15" steps="791"/></proof>
   </goal>
   <goal name="WP_parameter merge.29" expl="loop invariant preservation">
-  <proof prover="0" obsolete="true"><result status="valid" time="0.10" steps="147"/></proof>
-  <proof prover="2" timelimit="1"><result status="timeout" time="1.00"/></proof>
-  <proof prover="4"><result status="timeout" time="1.00"/></proof>
-  <proof prover="5"><result status="timeout" time="2.00"/></proof>
-  <proof prover="6" timelimit="10" memlimit="4000"><result status="valid" time="1.22"/></proof>
+  <proof prover="8" timelimit="10" memlimit="4000"><result status="valid" time="1.02"/></proof>
   </goal>
   <goal name="WP_parameter merge.30" expl="loop variant decrease">
-  <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="41"/></proof>
   <proof prover="5"><result status="valid" time="0.03" steps="74"/></proof>
   </goal>
   <goal name="WP_parameter merge.31" expl="precondition">
-  <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="20"/></proof>
   <proof prover="5"><result status="valid" time="0.00" steps="13"/></proof>
   </goal>
   <goal name="WP_parameter merge.32" expl="loop invariant preservation">
-  <proof prover="2" obsolete="true"><result status="valid" time="0.24"/></proof>
-  <proof prover="5"><result status="valid" time="1.26" steps="3333"/></proof>
+  <proof prover="5"><result status="valid" time="1.02" steps="3336"/></proof>
   </goal>
   <goal name="WP_parameter merge.33" expl="loop invariant preservation">
-  <proof prover="0" obsolete="true"><result status="valid" time="0.14" steps="128"/></proof>
-  <proof prover="5"><result status="valid" time="0.03" steps="84"/></proof>
+  <proof prover="5"><result status="valid" time="0.03" steps="83"/></proof>
   </goal>
   <goal name="WP_parameter merge.34" expl="loop invariant preservation">
-  <proof prover="2" obsolete="true"><result status="valid" time="0.07"/></proof>
-  <proof prover="5"><result status="valid" time="0.12" steps="415"/></proof>
+  <proof prover="5"><result status="valid" time="0.12" steps="531"/></proof>
   </goal>
   <goal name="WP_parameter merge.35" expl="loop invariant preservation">
-  <proof prover="1" timelimit="5" obsolete="true"><result status="valid" time="1.03"/></proof>
   <proof prover="5"><result status="valid" time="0.16" steps="277"/></proof>
   </goal>
   <goal name="WP_parameter merge.36" expl="loop variant decrease">
-  <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="36"/></proof>
   <proof prover="5"><result status="valid" time="0.01" steps="21"/></proof>
   </goal>
   <goal name="WP_parameter merge.37" expl="precondition">
-  <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="11"/></proof>
   <proof prover="5"><result status="valid" time="0.00" steps="12"/></proof>
   </goal>
   <goal name="WP_parameter merge.38" expl="loop invariant preservation">
-  <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="16"/></proof>
   <proof prover="5"><result status="valid" time="0.01" steps="12"/></proof>
   </goal>
   <goal name="WP_parameter merge.39" expl="loop invariant preservation">
-  <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="18"/></proof>
   <proof prover="5"><result status="valid" time="0.01" steps="12"/></proof>
   </goal>
   <goal name="WP_parameter merge.40" expl="loop invariant preservation">
-  <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="18"/></proof>
-  <proof prover="2" obsolete="true"><result status="valid" time="0.02"/></proof>
   <proof prover="5"><result status="valid" time="0.01" steps="12"/></proof>
   </goal>
   <goal name="WP_parameter merge.41" expl="loop invariant preservation">
-  <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="16"/></proof>
-  <proof prover="1" timelimit="10" memlimit="0" obsolete="true"><result status="valid" time="0.06"/></proof>
   <proof prover="5"><result status="valid" time="0.00" steps="12"/></proof>
   </goal>
   <goal name="WP_parameter merge.42" expl="loop variant decrease">
-  <proof prover="0" obsolete="true"><result status="valid" time="0.01" steps="36"/></proof>
   <proof prover="5"><result status="valid" time="0.01" steps="12"/></proof>
   </goal>
   <goal name="WP_parameter merge.43" expl="precondition">
-  <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="21"/></proof>
   <proof prover="5"><result status="valid" time="0.01" steps="14"/></proof>
   </goal>
   <goal name="WP_parameter merge.44" expl="precondition">
-  <proof prover="0" obsolete="true"><result status="valid" time="0.01" steps="24"/></proof>
   <proof prover="5"><result status="valid" time="0.01" steps="17"/></proof>
   </goal>
   <goal name="WP_parameter merge.45" expl="precondition">
-  <proof prover="0" obsolete="true"><result status="valid" time="0.01" steps="19"/></proof>
   <proof prover="5"><result status="valid" time="0.01" steps="20"/></proof>
   </goal>
   <goal name="WP_parameter merge.46" expl="loop invariant preservation">
-  <proof prover="2" obsolete="true"><result status="valid" time="0.22"/></proof>
   <proof prover="5"><result status="valid" time="0.01" steps="26"/></proof>
   </goal>
   <goal name="WP_parameter merge.47" expl="loop invariant preservation">
-  <proof prover="2" obsolete="true"><result status="valid" time="0.08"/></proof>
   <proof prover="5"><result status="valid" time="0.01" steps="29"/></proof>
   </goal>
   <goal name="WP_parameter merge.48" expl="loop invariant preservation">
-  <proof prover="1" obsolete="true"><result status="valid" time="2.52"/></proof>
   <proof prover="5"><result status="valid" time="0.01" steps="29"/></proof>
   </goal>
   <goal name="WP_parameter merge.49" expl="loop invariant preservation">
-  <proof prover="1" timelimit="5" obsolete="true"><result status="valid" time="0.19"/></proof>
   <proof prover="5"><result status="valid" time="0.02" steps="50"/></proof>
   </goal>
   <goal name="WP_parameter merge.50" expl="loop variant decrease">
-  <proof prover="0" obsolete="true"><result status="valid" time="0.03" steps="59"/></proof>
   <proof prover="5"><result status="valid" time="0.01" steps="27"/></proof>
   </goal>
   <goal name="WP_parameter merge.51" expl="precondition">
-  <proof prover="0" obsolete="true"><result status="valid" time="0.01" steps="19"/></proof>
   <proof prover="5"><result status="valid" time="0.01" steps="20"/></proof>
   </goal>
   <goal name="WP_parameter merge.52" expl="loop invariant preservation">
-  <proof prover="2" obsolete="true"><result status="valid" time="0.26"/></proof>
   <proof prover="5"><result status="valid" time="0.01" steps="26"/></proof>
   </goal>
   <goal name="WP_parameter merge.53" expl="loop invariant preservation">
-  <proof prover="1" obsolete="true"><result status="valid" time="2.29"/></proof>
   <proof prover="5"><result status="valid" time="0.01" steps="29"/></proof>
   </goal>
   <goal name="WP_parameter merge.54" expl="loop invariant preservation">
-  <proof prover="2" obsolete="true"><result status="valid" time="0.09"/></proof>
   <proof prover="5"><result status="valid" time="0.01" steps="29"/></proof>
   </goal>
   <goal name="WP_parameter merge.55" expl="loop invariant preservation">
-  <proof prover="3" edited="mergesort_queue_MergesortQueue_WP_parameter_merge_3.v" obsolete="true"><result status="valid" time="0.26"/></proof>
   <proof prover="5"><result status="valid" time="0.02" steps="50"/></proof>
   </goal>
   <goal name="WP_parameter merge.56" expl="loop variant decrease">
-  <proof prover="0" obsolete="true"><result status="valid" time="0.03" steps="58"/></proof>
   <proof prover="5"><result status="valid" time="0.01" steps="28"/></proof>
   </goal>
   <goal name="WP_parameter merge.57" expl="postcondition">
-  <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="10"/></proof>
   <proof prover="5"><result status="valid" time="0.00" steps="11"/></proof>
   </goal>
   <goal name="WP_parameter merge.58" expl="postcondition">
-  <proof prover="1" timelimit="5" obsolete="true"><result status="valid" time="0.07"/></proof>
   <proof prover="5"><result status="valid" time="0.04" steps="75"/></proof>
   </goal>
  </transf>
@@ -268,85 +191,63 @@
  <goal name="WP_parameter mergesort" expl="VC for mergesort" expanded="true">
  <transf name="split_goal_wp" expanded="true">
   <goal name="WP_parameter mergesort.1" expl="loop invariant init">
-  <proof prover="0" timelimit="6" obsolete="true"><result status="valid" time="0.07" steps="53"/></proof>
   <proof prover="5"><result status="valid" time="0.01" steps="26"/></proof>
   </goal>
   <goal name="WP_parameter mergesort.2" expl="loop invariant init">
-  <proof prover="0" timelimit="6" obsolete="true"><result status="valid" time="0.02" steps="4"/></proof>
   <proof prover="5"><result status="valid" time="0.01" steps="5"/></proof>
   </goal>
   <goal name="WP_parameter mergesort.3" expl="precondition">
-  <proof prover="0" timelimit="6" obsolete="true"><result status="valid" time="0.02" steps="7"/></proof>
   <proof prover="5"><result status="valid" time="0.01" steps="8"/></proof>
   </goal>
   <goal name="WP_parameter mergesort.4" expl="precondition">
-  <proof prover="0" timelimit="6" obsolete="true"><result status="valid" time="0.02" steps="13"/></proof>
   <proof prover="5"><result status="valid" time="0.01" steps="14"/></proof>
   </goal>
   <goal name="WP_parameter mergesort.5" expl="loop invariant preservation" expanded="true">
-  <proof prover="2" timelimit="30"><result status="valid" time="3.59"/></proof>
-  <proof prover="6" timelimit="10" memlimit="4000"><result status="valid" time="8.52"/></proof>
+  <proof prover="2"><result status="valid" time="2.76"/></proof>
+  <proof prover="8" timelimit="10" memlimit="4000"><result status="valid" time="5.89"/></proof>
   </goal>
   <goal name="WP_parameter mergesort.6" expl="loop invariant preservation">
-  <proof prover="0" timelimit="6" obsolete="true"><result status="valid" time="0.06" steps="76"/></proof>
   <proof prover="5"><result status="valid" time="0.03" steps="71"/></proof>
   </goal>
   <goal name="WP_parameter mergesort.7" expl="loop variant decrease">
-  <proof prover="0" timelimit="6" obsolete="true"><result status="valid" time="0.02" steps="27"/></proof>
   <proof prover="5"><result status="valid" time="0.01" steps="26"/></proof>
   </goal>
   <goal name="WP_parameter mergesort.8" expl="loop invariant preservation">
-  <proof prover="1" obsolete="true"><result status="valid" time="0.13"/></proof>
   <proof prover="5"><result status="valid" time="0.29" steps="226"/></proof>
-  <proof prover="7" obsolete="true"><result status="valid" time="0.23"/></proof>
   </goal>
   <goal name="WP_parameter mergesort.9" expl="loop invariant preservation">
-  <proof prover="0" timelimit="6" obsolete="true"><result status="valid" time="0.06" steps="29"/></proof>
   <proof prover="5"><result status="valid" time="0.02" steps="56"/></proof>
   </goal>
   <goal name="WP_parameter mergesort.10" expl="loop variant decrease">
-  <proof prover="0" timelimit="6" obsolete="true"><result status="valid" time="0.02" steps="18"/></proof>
   <proof prover="5"><result status="valid" time="0.01" steps="16"/></proof>
   </goal>
   <goal name="WP_parameter mergesort.11" expl="assertion">
-  <proof prover="0" timelimit="6" obsolete="true"><result status="valid" time="0.02" steps="7"/></proof>
   <proof prover="5"><result status="valid" time="0.01" steps="8"/></proof>
   </goal>
   <goal name="WP_parameter mergesort.12" expl="assertion">
-  <proof prover="0" timelimit="6" obsolete="true"><result status="valid" time="0.03" steps="48"/></proof>
   <proof prover="5"><result status="valid" time="0.01" steps="21"/></proof>
   </goal>
   <goal name="WP_parameter mergesort.13" expl="variant decrease">
-  <proof prover="0" timelimit="6" obsolete="true"><result status="valid" time="0.03" steps="45"/></proof>
-  <proof prover="2" obsolete="true"><result status="valid" time="0.02"/></proof>
   <proof prover="5"><result status="valid" time="0.02" steps="60"/></proof>
   </goal>
   <goal name="WP_parameter mergesort.14" expl="variant decrease">
-  <proof prover="0" timelimit="6" obsolete="true"><result status="valid" time="0.04" steps="49"/></proof>
-  <proof prover="2" obsolete="true"><result status="valid" time="0.03"/></proof>
   <proof prover="5"><result status="valid" time="0.01" steps="64"/></proof>
   </goal>
   <goal name="WP_parameter mergesort.15" expl="precondition">
-  <proof prover="0" timelimit="6" obsolete="true"><result status="valid" time="0.02" steps="12"/></proof>
   <proof prover="5"><result status="valid" time="0.00" steps="13"/></proof>
   </goal>
   <goal name="WP_parameter mergesort.16" expl="postcondition">
-  <proof prover="0" timelimit="6" obsolete="true"><result status="valid" time="0.39" steps="353"/></proof>
   <proof prover="5"><result status="valid" time="0.05" steps="104"/></proof>
   </goal>
   <goal name="WP_parameter mergesort.17" expl="assertion">
-  <proof prover="1" obsolete="true"><result status="valid" time="0.08"/></proof>
-  <proof prover="5"><result status="unknown" time="0.01"/></proof>
-  <proof prover="6"><result status="valid" time="0.10"/></proof>
+  <proof prover="8"><result status="valid" time="0.10"/></proof>
   </goal>
   <goal name="WP_parameter mergesort.18" expl="postcondition">
   <transf name="split_goal_wp">
    <goal name="WP_parameter mergesort.18.1" expl="VC for mergesort">
-   <proof prover="0" timelimit="6" obsolete="true"><result status="valid" time="0.02" steps="4"/></proof>
    <proof prover="5"><result status="valid" time="0.01" steps="5"/></proof>
    </goal>
    <goal name="WP_parameter mergesort.18.2" expl="VC for mergesort">
-   <proof prover="0" timelimit="6" obsolete="true"><result status="valid" time="0.02" steps="3"/></proof>
    <proof prover="5"><result status="valid" time="0.01" steps="4"/></proof>
    </goal>
   </transf>
diff --git a/examples/tests-provers/bv/why3session.xml b/examples/tests-provers/bv/why3session.xml
index 18f8f27f0..8d1c3ad77 100644
--- a/examples/tests-provers/bv/why3session.xml
+++ b/examples/tests-provers/bv/why3session.xml
@@ -9,7 +9,7 @@
 <prover id="4" name="Z3" version="4.4.0" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="5" name="Alt-Ergo" version="1.01" timelimit="1" steplimit="0" memlimit="1000"/>
 <file name="../bv.why" expanded="true">
-<theory name="CheckBV64" sum="a69e7936e9b3736b53a1a06d1557d503" expanded="true">
+<theory name="CheckBV64" sum="a69e7936e9b3736b53a1a06d1557d503">
  <goal name="ok_zero" expl="">
  <proof prover="0"><result status="valid" time="0.02" steps="87"/></proof>
  <proof prover="1"><result status="valid" time="0.02"/></proof>
@@ -208,19 +208,19 @@
  <proof prover="3"><result status="timeout" time="0.92"/></proof>
  <proof prover="4" timelimit="1"><result status="timeout" time="1.00"/></proof>
  </goal>
- <goal name="smoke6" expl="" expanded="true">
+ <goal name="smoke6" expl="">
  <proof prover="0" timelimit="1"><result status="timeout" time="1.00"/></proof>
  <proof prover="1"><result status="unknown" time="0.46"/></proof>
  <proof prover="2"><result status="unknown" time="0.00"/></proof>
  <proof prover="4" timelimit="1"><result status="timeout" time="1.00"/></proof>
  </goal>
- <goal name="smoke7" expl="" expanded="true">
+ <goal name="smoke7" expl="">
  <proof prover="0" timelimit="1"><result status="timeout" time="1.01"/></proof>
  <proof prover="1"><result status="unknown" time="0.51"/></proof>
  <proof prover="2"><result status="unknown" time="0.01"/></proof>
  <proof prover="4" timelimit="1"><result status="timeout" time="1.00"/></proof>
  </goal>
- <goal name="smoke8" expl="" expanded="true">
+ <goal name="smoke8" expl="">
  <proof prover="0" timelimit="1"><result status="timeout" time="1.00"/></proof>
  <proof prover="1"><result status="unknown" time="0.44"/></proof>
  <proof prover="2"><result status="unknown" time="0.00"/></proof>
@@ -382,7 +382,7 @@
  <proof prover="4"><result status="valid" time="0.02"/></proof>
  </goal>
 </theory>
-<theory name="CheckBV32" sum="9a0215c8a7245c48b487371f67df8950">
+<theory name="CheckBV32" sum="9a0215c8a7245c48b487371f67df8950" expanded="true">
  <goal name="ok_zero" expl="">
  <proof prover="0"><result status="valid" time="0.03" steps="87"/></proof>
  <proof prover="1"><result status="valid" time="0.03"/></proof>
@@ -596,15 +596,14 @@
  <proof prover="3"><result status="timeout" time="0.96"/></proof>
  <proof prover="4" timelimit="1"><result status="timeout" time="1.00"/></proof>
  </goal>
- <goal name="smoke8" expl="">
+ <goal name="smoke8" expl="" expanded="true">
  <proof prover="0" timelimit="1"><result status="timeout" time="1.01"/></proof>
  <proof prover="1"><result status="unknown" time="0.44"/></proof>
  <proof prover="2"><result status="unknown" time="0.00"/></proof>
- <proof prover="3"><result status="timeout" time="0.92"/></proof>
  <proof prover="4" timelimit="1"><result status="timeout" time="1.00"/></proof>
  </goal>
 </theory>
-<theory name="CheckBV16" sum="b944f76414b884563c0502c12ba6dc16">
+<theory name="CheckBV16" sum="b944f76414b884563c0502c12ba6dc16" expanded="true">
  <goal name="ok_zero" expl="">
  <proof prover="0"><result status="valid" time="0.04" steps="87"/></proof>
  <proof prover="1"><result status="valid" time="0.04"/></proof>
@@ -784,7 +783,7 @@
  <proof prover="3"><result status="timeout" time="0.96"/></proof>
  <proof prover="4" timelimit="1"><result status="timeout" time="1.00"/></proof>
  </goal>
- <goal name="smoke3" expl="">
+ <goal name="smoke3" expl="" expanded="true">
  <proof prover="0" timelimit="1"><result status="timeout" time="1.00"/></proof>
  <proof prover="1"><result status="unknown" time="0.48"/></proof>
  <proof prover="2"><result status="unknown" time="0.01"/></proof>
@@ -818,15 +817,14 @@
  <proof prover="3"><result status="timeout" time="0.95"/></proof>
  <proof prover="4" timelimit="1"><result status="timeout" time="1.00"/></proof>
  </goal>
- <goal name="smoke8" expl="">
+ <goal name="smoke8" expl="" expanded="true">
  <proof prover="0" timelimit="1"><result status="timeout" time="1.00"/></proof>
  <proof prover="1"><result status="unknown" time="0.43"/></proof>
  <proof prover="2"><result status="unknown" time="0.00"/></proof>
- <proof prover="3"><result status="timeout" time="0.97"/></proof>
  <proof prover="4" timelimit="1"><result status="timeout" time="1.00"/></proof>
  </goal>
 </theory>
-<theory name="CheckBV8" sum="05518dc91aa5666cf77ec6c0d7299767">
+<theory name="CheckBV8" sum="05518dc91aa5666cf77ec6c0d7299767" expanded="true">
  <goal name="ok_zero" expl="">
  <proof prover="0"><result status="valid" time="0.04" steps="87"/></proof>
  <proof prover="1"><result status="valid" time="0.05"/></proof>
@@ -1040,11 +1038,10 @@
  <proof prover="3"><result status="timeout" time="0.94"/></proof>
  <proof prover="4" timelimit="1"><result status="timeout" time="1.00"/></proof>
  </goal>
- <goal name="smoke8" expl="">
+ <goal name="smoke8" expl="" expanded="true">
  <proof prover="0" timelimit="1"><result status="timeout" time="1.01"/></proof>
  <proof prover="1"><result status="unknown" time="0.45"/></proof>
  <proof prover="2"><result status="unknown" time="0.01"/></proof>
- <proof prover="3"><result status="timeout" time="0.94"/></proof>
  <proof prover="4" timelimit="1"><result status="timeout" time="0.99"/></proof>
  </goal>
 </theory>
-- 
GitLab