Fixed proof session for binary heaps example

examples/programs/vacid_0_binary_heaps/proofs/why3session.xml

 <?xml version="1.0" encoding="UTF-8"?>
-<!DOCTYPE why3session SYSTEM "/home/jcf/why3/share/why3session.dtd">
+<!DOCTYPE why3session SYSTEM "/usr/local/share/why3/why3session.dtd">
 <why3session
  name="proofs/why3session.xml">
  <prover
@@ -5327,13 +5327,13 @@
  <file
   name="../heapsort.mlw"
   verified="true"
-  expanded="true">
+  expanded="false">
   <theory
    name="WP HeapSort"
    locfile="proofs/../heapsort.mlw"
    loclnum="2" loccnumb="7" loccnume="15"
    verified="true"
-   expanded="true">
+   expanded="false">
    <goal
     name="Min_of_sorted"
     locfile="proofs/../heapsort.mlw"
@@ -5358,14 +5358,14 @@
     expl="parameter heapSort"
     sum="83d38d95e99d32dc2e08f0b3bdd91d07"
     proved="true"
-    expanded="true"
+    expanded="false"
     shape="ainfix =aelementsV5c0V0aelementsV1c0V0Aasorted_subV5c0V0Iainfix &lt;=agetV5V6amin_bagamodelV4Iainfix &lt;V6ainfix +ainfix -V0c1c1Aainfix &lt;=c0V6FAasorted_subV5c0ainfix +ainfix -V0c1c1Aainfix =aelementsV1c0V0aunionamodelV4aelementsV5c0ainfix +ainfix -V0c1c1Aainfix =acardamodelV4ainfix -V0ainfix +ainfix -V0c1c1Aainfix &lt;=ainfix +ainfix -V0c1c1V0Aainfix &lt;=c0ainfix +ainfix -V0c1c1Aainfix &lt;=agetV10V11amin_bagamodelV8Iainfix &lt;V11ainfix +V7c1Aainfix &lt;=c0V11FAasorted_subV10c0ainfix +V7c1Aainfix =aelementsV1c0V0aunionamodelV8aelementsV10c0ainfix +V7c1Aainfix =acardamodelV8ainfix -V0ainfix +V7c1Aainfix &lt;=ainfix +V7c1V0Aainfix &lt;=c0ainfix +V7c1Aainfix &lt;=agetV10V7amin_bagamodelV8Iainfix =V10asetV5V7V9FAainfix &lt;V7V0Aainfix &lt;=c0V7Iainfix =acardamodelV4ainfix +acardamodelV8c1Aainfix =amodelV4aaddV9amodelV8Aainfix =V9amin_bagamodelV4FFAainfix =amodelV4aempty_bagNIainfix &lt;=agetV5V12amin_bagamodelV4Iainfix &lt;V12V7Aainfix &lt;=c0V12FAasorted_subV5c0V7Aainfix =aelementsV1c0V0aunionamodelV4aelementsV5c0V7Aainfix =acardamodelV4ainfix -V0V7Aainfix &lt;=V7V0Aainfix &lt;=c0V7Iainfix &lt;=V7ainfix -V0c1Aainfix &lt;=c0V7FFFAainfix &lt;=agetV1V13amin_bagamodelV3Iainfix &lt;V13c0Aainfix &lt;=c0V13FAasorted_subV1c0c0Aainfix =aelementsV1c0V0aunionamodelV3aelementsV1c0c0Aainfix =acardamodelV3ainfix -V0c0Aainfix &lt;=c0V0Aainfix &lt;=c0c0Iainfix &lt;=c0ainfix -V0c1Aainfix =aelementsV1c0V0aelementsV1c0V0Aasorted_subV1c0V0Iainfix &gt;c0ainfix -V0c1Iainfix =amodelV3aelementsV1c0ainfix +ainfix -V0c1c1Aainfix =acardamodelV3ainfix +ainfix -V0c1c1Aainfix &lt;=ainfix +ainfix -V0c1c1V0Aainfix &lt;=c0ainfix +ainfix -V0c1c1Aainfix =amodelV15aelementsV1c0ainfix +V14c1Aainfix =acardamodelV15ainfix +V14c1Aainfix &lt;=ainfix +V14c1V0Aainfix &lt;=c0ainfix +V14c1Iainfix =amodelV15aaddagetV1V14amodelV3FAainfix &lt;V14V0Aainfix &lt;=c0V14Iainfix =amodelV3aelementsV1c0V14Aainfix =acardamodelV3V14Aainfix &lt;=V14V0Aainfix &lt;=c0V14Iainfix &lt;=V14ainfix -V0c1Aainfix &lt;=c0V14FFAainfix =amodelV2aelementsV1c0c0Aainfix =acardamodelV2c0Aainfix &lt;=c0V0Aainfix &lt;=c0c0Iainfix &lt;=c0ainfix -V0c1Aainfix =aelementsV17c0V0aelementsV1c0V0Aasorted_subV17c0V0Iainfix &lt;=agetV17V18amin_bagamodelV16Iainfix &lt;V18ainfix +ainfix -V0c1c1Aainfix &lt;=c0V18FAasorted_subV17c0ainfix +ainfix -V0c1c1Aainfix =aelementsV1c0V0aunionamodelV16aelementsV17c0ainfix +ainfix -V0c1c1Aainfix =acardamodelV16ainfix -V0ainfix +ainfix -V0c1c1Aainfix &lt;=ainfix +ainfix -V0c1c1V0Aainfix &lt;=c0ainfix +ainfix -V0c1c1Aainfix &lt;=agetV22V23amin_bagamodelV20Iainfix &lt;V23ainfix +V19c1Aainfix &lt;=c0V23FAasorted_subV22c0ainfix +V19c1Aainfix =aelementsV1c0V0aunionamodelV20aelementsV22c0ainfix +V19c1Aainfix =acardamodelV20ainfix -V0ainfix +V19c1Aainfix &lt;=ainfix +V19c1V0Aainfix &lt;=c0ainfix +V19c1Aainfix &lt;=agetV22V19amin_bagamodelV20Iainfix =V22asetV17V19V21FAainfix &lt;V19V0Aainfix &lt;=c0V19Iainfix =acardamodelV16ainfix +acardamodelV20c1Aainfix =amodelV16aaddV21amodelV20Aainfix =V21amin_bagamodelV16FFAainfix =amodelV16aempty_bagNIainfix &lt;=agetV17V24amin_bagamodelV16Iainfix &lt;V24V19Aainfix &lt;=c0V24FAasorted_subV17c0V19Aainfix =aelementsV1c0V0aunionamodelV16aelementsV17c0V19Aainfix =acardamodelV16ainfix -V0V19Aainfix &lt;=V19V0Aainfix &lt;=c0V19Iainfix &lt;=V19ainfix -V0c1Aainfix &lt;=c0V19FFFAainfix &lt;=agetV1V25amin_bagamodelV2Iainfix &lt;V25c0Aainfix &lt;=c0V25FAasorted_subV1c0c0Aainfix =aelementsV1c0V0aunionamodelV2aelementsV1c0c0Aainfix =acardamodelV2ainfix -V0c0Aainfix &lt;=c0V0Aainfix &lt;=c0c0Iainfix &lt;=c0ainfix -V0c1Aainfix =aelementsV1c0V0aelementsV1c0V0Aasorted_subV1c0V0Iainfix &gt;c0ainfix -V0c1Iainfix &gt;c0ainfix -V0c1Iainfix =amodelV2aempty_bagFAainfix &lt;=c0V0Iainfix &gt;=V0c0FF">
     <label
      name="expl:parameter heapSort"/>
     <transf
      name="split_goal"
      proved="true"
-     expanded="true">
+     expanded="false">
      <goal
       name="WP_parameter heapSort.1"
       locfile="proofs/../heapsort.mlw"
@@ -5438,19 +5438,12 @@
        archived="false">
        <result status="valid" time="0.01"/>
       </proof>
-      <proof
-       prover="5"
-       timelimit="10"
-       obsolete="false"
-       archived="false">
-       <result status="unknown" time="0.00"/>
-      </proof>
       <proof
        prover="8"
-       timelimit="11"
+       timelimit="30"
        obsolete="false"
        archived="false">
-       <result status="unknown" time="11.07"/>
+       <result status="valid" time="28.60"/>
       </proof>
       <proof
        prover="9"
@@ -5582,10 +5575,10 @@
         </proof>
         <proof
          prover="8"
-         timelimit="5"
+         timelimit="11"
          obsolete="false"
          archived="false">
-         <result status="unknown" time="5.08"/>
+         <result status="valid" time="6.55"/>
         </proof>
         <proof
          prover="9"
@@ -5594,13 +5587,6 @@
          archived="false">
          <result status="valid" time="0.02"/>
         </proof>
-        <proof
-         prover="4"
-         timelimit="10"
-         obsolete="false"
-         archived="false">
-         <result status="timeout" time="9.97"/>
-        </proof>
        </goal>
        <goal
         name="WP_parameter heapSort.3.4"
@@ -6343,7 +6329,7 @@
       expl="normal postcondition"
       sum="403a589052aaa165235c63d00f6cbb6d"
       proved="true"
-      expanded="true"
+      expanded="false"
       shape="ainfix =aelementsV5c0V0aelementsV1c0V0Aasorted_subV5c0V0Iainfix &lt;=agetV5V6amin_bagamodelV4Iainfix &lt;V6ainfix +ainfix -V0c1c1Aainfix &lt;=c0V6FAasorted_subV5c0ainfix +ainfix -V0c1c1Aainfix =aelementsV1c0V0aunionamodelV4aelementsV5c0ainfix +ainfix -V0c1c1Aainfix =acardamodelV4ainfix -V0ainfix +ainfix -V0c1c1Aainfix &lt;=ainfix +ainfix -V0c1c1V0Aainfix &lt;=c0ainfix +ainfix -V0c1c1FFIainfix &lt;=c0ainfix -V0c1Iainfix =amodelV3aelementsV1c0ainfix +ainfix -V0c1c1Aainfix =acardamodelV3ainfix +ainfix -V0c1c1Aainfix &lt;=ainfix +ainfix -V0c1c1V0Aainfix &lt;=c0ainfix +ainfix -V0c1c1FIainfix &lt;=c0ainfix -V0c1Iainfix =amodelV2aempty_bagFIainfix &lt;=c0V0Iainfix &gt;=V0c0FF">
       <label
        name="expl:parameter heapSort"/>
@@ -6390,7 +6376,7 @@
  <file
   name="../heap_model.why"
   verified="true"
-  expanded="true">
+  expanded="false">
   <theory
    name="Model"
    locfile="proofs/../heap_model.why"