diff --git a/examples/check-builtin/floats/why3session.xml b/examples/check-builtin/floats/why3session.xml
index 193b3af5d7947e1cc1fd984bfa9e8ee9526ac2d2..647dec04ef9af2f2a689b892dbdb8774a67c4059 100644
--- a/examples/check-builtin/floats/why3session.xml
+++ b/examples/check-builtin/floats/why3session.xml
@@ -1,7 +1,7 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session SYSTEM "why3session.dtd">
 <why3session
- name="examples/check-builtin/floats/why3session.xml">
+ name="check-builtin/floats/why3session.xml">
  <prover
   id="alt-ergo"
   name="Alt-Ergo"
@@ -9,7 +9,7 @@
  <prover
   id="coq"
   name="Coq"
-  version="8.2pl1"/>
+  version="8.3pl2"/>
  <prover
   id="cvc3"
   name="CVC3"
@@ -17,11 +17,23 @@
  <prover
   id="gappa"
   name="Gappa"
-  version="0.13.0"/>
+  version="0.15.0"/>
  <prover
   id="simplify"
   name="Simplify"
   version="1.5.4"/>
+ <prover
+  id="spass"
+  name="Spass"
+  version="3.7"/>
+ <prover
+  id="vampire"
+  name="Vampire"
+  version="0.6"/>
+ <prover
+  id="yices"
+  name="Yices"
+  version="1.0.25"/>
  <prover
   id="z3"
   name="Z3"
@@ -36,7 +48,7 @@
    expanded="true">
    <goal
     name="Round_single_01"
-    sum="b356284ef3c67cc31bb22f6c7deae9f0"
+    sum="4350d059bf72b21b36729eaccc394959"
     proved="true"
     expanded="true"
     shape="ainfix =aroundaNearestTiesToEvenc0.1c0x1.99999ap-4">
@@ -45,12 +57,12 @@
      timelimit="5"
      edited=""
      obsolete="false">
-     <result status="valid" time="0.01"/>
+     <result status="valid" time="0.00"/>
     </proof>
    </goal>
    <goal
     name="Round_double_01"
-    sum="a981e04c08472362dcca34e0f3487b74"
+    sum="fc4b69caf28748e651e23f375e300b70"
     proved="true"
     expanded="true"
     shape="ainfix =aroundaNearestTiesToEvenc0.1c0x1.999999999999ap-4">
@@ -59,12 +71,12 @@
      timelimit="5"
      edited=""
      obsolete="false">
-     <result status="valid" time="0.01"/>
+     <result status="valid" time="0.00"/>
     </proof>
    </goal>
    <goal
     name="Test00"
-    sum="532babe00b8785ec6f7286621c12a512"
+    sum="d126875bf4fc484b4b44c2b52b9da437"
     proved="true"
     expanded="true"
     shape="ainfix <=aprefix -c3.0V0Iainfix <=aabsV0c2.0F">
@@ -73,33 +85,33 @@
      timelimit="5"
      edited=""
      obsolete="false">
-     <result status="valid" time="0.03"/>
+     <result status="valid" time="0.00"/>
     </proof>
     <proof
      prover="alt-ergo"
      timelimit="5"
      edited=""
      obsolete="false">
-     <result status="valid" time="0.04"/>
+     <result status="valid" time="0.01"/>
     </proof>
     <proof
      prover="z3"
      timelimit="5"
      edited=""
      obsolete="false">
-     <result status="valid" time="0.04"/>
+     <result status="valid" time="0.02"/>
     </proof>
     <proof
      prover="gappa"
      timelimit="5"
      edited=""
      obsolete="false">
-     <result status="valid" time="0.01"/>
+     <result status="valid" time="0.00"/>
     </proof>
    </goal>
    <goal
     name="Test01"
-    sum="a2dc5970c8ef3c553ea90e0fc634da83"
+    sum="bcbfbae3da81b362e99b319253ef2a20"
     proved="true"
     expanded="true"
     shape="ainfix <=aabsainfix -ainfix *avalueV0avalueV0aroundaNearestTiesToEvenainfix *avalueV0avalueV0c0x1.p-52Iainfix <=avalueV0c2.0Aainfix <=aprefix -c2.0avalueV0F">
@@ -108,12 +120,12 @@
      timelimit="5"
      edited=""
      obsolete="false">
-     <result status="valid" time="0.01"/>
+     <result status="valid" time="0.00"/>
     </proof>
    </goal>
    <goal
     name="Test02"
-    sum="eb102544c66926067fe7350ea3f1ba87"
+    sum="1d3e20e12a14b6bd91a25d057da3b098"
     proved="true"
     expanded="true"
     shape="ainfix <=aabsainfix -ainfix *avalueV1avalueV1aroundaNearestTiesToEvenainfix *avalueV0avalueV0c0x1.p-52Iainfix =V1V0Iainfix <=aabsavalueV0c2.0F">
@@ -122,12 +134,12 @@
      timelimit="5"
      edited=""
      obsolete="false">
-     <result status="valid" time="0.01"/>
+     <result status="valid" time="0.00"/>
     </proof>
    </goal>
    <goal
     name="Test03"
-    sum="3d36d4470fa7e12c3ba550960abf7a6c"
+    sum="42c26c3443d67722883a37dfe8f9253c"
     proved="true"
     expanded="true"
     shape="ainfix <=asqrtainfix *ainfix -avalueV2ainfix *avalueV0avalueV0ainfix -avalueV1ainfix *avalueV0avalueV0c0x1.p-52Iainfix =V2V1Iainfix =avalueV1aroundaNearestTiesToEvenainfix *avalueV0avalueV0Iainfix <=aabsavalueV0c2.0F">
@@ -136,7 +148,7 @@
      timelimit="5"
      edited=""
      obsolete="false">
-     <result status="valid" time="0.01"/>
+     <result status="valid" time="0.00"/>
     </proof>
    </goal>
   </theory>
diff --git a/examples/programs/muller/why3session.xml b/examples/programs/muller/why3session.xml
index de5ba401b0153ccb1cb432e16dabeae1a15397aa..2b43ba1d7f77c0d78fae687d41ace14e527a6fdf 100644
--- a/examples/programs/muller/why3session.xml
+++ b/examples/programs/muller/why3session.xml
@@ -1,99 +1,285 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session SYSTEM "why3session.dtd">
-<why3session name="programs/muller/why3session.xml">
- <prover id="alt-ergo" name="Alt-Ergo" version="0.93"/>
- <prover id="coq" name="Coq" version="8.2pl1"/>
- <prover id="cvc3" name="CVC3" version="2.2"/>
- <prover id="gappa" name="Gappa" version="0.13.0"/>
- <prover id="simplify" name="Simplify" version="1.5.4"/>
- <prover id="z3" name="Z3" version="2.19"/>
- <file name="../muller.mlw" verified="true" expanded="true">
-  <theory name="WP Muller" verified="true" expanded="true">
-   <goal name="WP_parameter compact" expl="parameter compact" sum="199cbe3428eff0829e3355f60d4e5947" proved="true" expanded="true" shape="iainfix =agetV1V6c0Nainfix <=anum_ofV1c0ainfix +V6c1ainfix +V6c1Aainfix =V8anum_ofV1c0ainfix +V6c1Aainfix <=c0V8Iainfix =V8ainfix +V5c1FIainfix =V7asetV4V5agetV1V6FAainfix <V5V2Aainfix <=c0V5Aainfix <V6V0Aainfix <=c0V6ainfix <=anum_ofV1c0ainfix +V6c1ainfix +V6c1Aainfix =V5anum_ofV1c0ainfix +V6c1Aainfix <=c0V5Aainfix <V6V0Aainfix <=c0V6Iainfix <=anum_ofV1c0V6V6Aainfix =V5anum_ofV1c0V6Aainfix <=c0V5Iainfix <=V6ainfix -V0c1Aainfix <=c0V6FFFAainfix <=anum_ofV1c0c0c0Aainfix =V3anum_ofV1c0c0Aainfix <=c0V3Iainfix <=c0ainfix -V0c1Iainfix =V3c0FAainfix >=V2c0Iainfix <=anum_ofV1c0ainfix +ainfix -V0c1c1ainfix +ainfix -V0c1c1Aainfix =V2anum_ofV1c0ainfix +ainfix -V0c1c1Aainfix <=c0V2Aiainfix =agetV1V9c0Nainfix <=anum_ofV1c0ainfix +V9c1ainfix +V9c1Aainfix =V10anum_ofV1c0ainfix +V9c1Aainfix <=c0V10Iainfix =V10ainfix +V2c1Fainfix <=anum_ofV1c0ainfix +V9c1ainfix +V9c1Aainfix =V2anum_ofV1c0ainfix +V9c1Aainfix <=c0V2Aainfix <V9V0Aainfix <=c0V9Iainfix <=anum_ofV1c0V9V9Aainfix =V2anum_ofV1c0V9Aainfix <=c0V2Iainfix <=V9ainfix -V0c1Aainfix <=c0V9FFAainfix <=anum_ofV1c0c0c0Aainfix =c0anum_ofV1c0c0Aainfix <=c0c0Iainfix <=c0ainfix -V0c1Aiainfix =agetV1V14c0Nainfix <=anum_ofV1c0ainfix +V14c1ainfix +V14c1Aainfix =V16anum_ofV1c0ainfix +V14c1Aainfix <=c0V16Iainfix =V16ainfix +V13c1FIainfix =V15asetV12V13agetV1V14FAainfix <V13c0Aainfix <=c0V13Aainfix <V14V0Aainfix <=c0V14ainfix <=anum_ofV1c0ainfix +V14c1ainfix +V14c1Aainfix =V13anum_ofV1c0ainfix +V14c1Aainfix <=c0V13Aainfix <V14V0Aainfix <=c0V14Iainfix <=anum_ofV1c0V14V14Aainfix =V13anum_ofV1c0V14Aainfix <=c0V13Iainfix <=V14ainfix -V0c1Aainfix <=c0V14FFFAainfix <=anum_ofV1c0c0c0Aainfix =V11anum_ofV1c0c0Aainfix <=c0V11Iainfix <=c0ainfix -V0c1Iainfix =V11c0FAainfix >=c0c0Iainfix >c0ainfix -V0c1FF">
-    <transf name="split_goal" proved="true" expanded="true">
-     <goal name="WP_parameter compact.1" expl="precondition" sum="6c3030d41d5aca45af2bdfb8c97604fc" proved="true" expanded="true" shape="ainfix >=c0c0Iainfix >c0ainfix -V0c1FF">
-      <proof prover="cvc3" timelimit="10" edited="" obsolete="false">
-       <result status="valid" time="0.02"/>
+<why3session
+ name="programs/muller/why3session.xml">
+ <prover
+  id="alt-ergo"
+  name="Alt-Ergo"
+  version="0.93"/>
+ <prover
+  id="coq"
+  name="Coq"
+  version="8.3pl2"/>
+ <prover
+  id="cvc3"
+  name="CVC3"
+  version="2.2"/>
+ <prover
+  id="gappa"
+  name="Gappa"
+  version="0.15.0"/>
+ <prover
+  id="simplify"
+  name="Simplify"
+  version="1.5.4"/>
+ <prover
+  id="spass"
+  name="Spass"
+  version="3.7"/>
+ <prover
+  id="vampire"
+  name="Vampire"
+  version="0.6"/>
+ <prover
+  id="yices"
+  name="Yices"
+  version="1.0.25"/>
+ <prover
+  id="z3"
+  name="Z3"
+  version="2.19"/>
+ <file
+  name="../muller.mlw"
+  verified="true"
+  expanded="true">
+  <theory
+   name="WP Muller"
+   verified="true"
+   expanded="true">
+   <goal
+    name="WP_parameter compact"
+    expl="parameter compact"
+    sum="64672b3e7a2efc092b0ee8b665eafa4d"
+    proved="true"
+    expanded="true"
+    shape="iainfix =agetV1V6c0Nainfix <=anum_ofV1c0ainfix +V6c1ainfix +V6c1Aainfix =V8anum_ofV1c0ainfix +V6c1Aainfix <=c0V8Iainfix =V8ainfix +V5c1FIainfix =V7asetV4V5agetV1V6FAainfix <V5V2Aainfix <=c0V5Aainfix <V6V0Aainfix <=c0V6ainfix <=anum_ofV1c0ainfix +V6c1ainfix +V6c1Aainfix =V5anum_ofV1c0ainfix +V6c1Aainfix <=c0V5Aainfix <V6V0Aainfix <=c0V6Iainfix <=anum_ofV1c0V6V6Aainfix =V5anum_ofV1c0V6Aainfix <=c0V5Iainfix <=V6ainfix -V0c1Aainfix <=c0V6FFFAainfix <=anum_ofV1c0c0c0Aainfix =V3anum_ofV1c0c0Aainfix <=c0V3Iainfix <=c0ainfix -V0c1Iainfix =V3c0FAainfix >=V2c0Iainfix <=anum_ofV1c0ainfix +ainfix -V0c1c1ainfix +ainfix -V0c1c1Aainfix =V2anum_ofV1c0ainfix +ainfix -V0c1c1Aainfix <=c0V2Aiainfix =agetV1V9c0Nainfix <=anum_ofV1c0ainfix +V9c1ainfix +V9c1Aainfix =V10anum_ofV1c0ainfix +V9c1Aainfix <=c0V10Iainfix =V10ainfix +V2c1Fainfix <=anum_ofV1c0ainfix +V9c1ainfix +V9c1Aainfix =V2anum_ofV1c0ainfix +V9c1Aainfix <=c0V2Aainfix <V9V0Aainfix <=c0V9Iainfix <=anum_ofV1c0V9V9Aainfix =V2anum_ofV1c0V9Aainfix <=c0V2Iainfix <=V9ainfix -V0c1Aainfix <=c0V9FFAainfix <=anum_ofV1c0c0c0Aainfix =c0anum_ofV1c0c0Aainfix <=c0c0Iainfix <=c0ainfix -V0c1Aiainfix =agetV1V14c0Nainfix <=anum_ofV1c0ainfix +V14c1ainfix +V14c1Aainfix =V16anum_ofV1c0ainfix +V14c1Aainfix <=c0V16Iainfix =V16ainfix +V13c1FIainfix =V15asetV12V13agetV1V14FAainfix <V13c0Aainfix <=c0V13Aainfix <V14V0Aainfix <=c0V14ainfix <=anum_ofV1c0ainfix +V14c1ainfix +V14c1Aainfix =V13anum_ofV1c0ainfix +V14c1Aainfix <=c0V13Aainfix <V14V0Aainfix <=c0V14Iainfix <=anum_ofV1c0V14V14Aainfix =V13anum_ofV1c0V14Aainfix <=c0V13Iainfix <=V14ainfix -V0c1Aainfix <=c0V14FFFAainfix <=anum_ofV1c0c0c0Aainfix =V11anum_ofV1c0c0Aainfix <=c0V11Iainfix <=c0ainfix -V0c1Iainfix =V11c0FAainfix >=c0c0Iainfix >c0ainfix -V0c1FF">
+    <transf
+     name="split_goal"
+     proved="true"
+     expanded="true">
+     <goal
+      name="WP_parameter compact.1"
+      expl="precondition"
+      sum="7ab9a7fe054cc3f79fce84360c33c0fb"
+      proved="true"
+      expanded="true"
+      shape="ainfix >=c0c0Iainfix >c0ainfix -V0c1FF">
+      <proof
+       prover="cvc3"
+       timelimit="10"
+       edited=""
+       obsolete="false">
+       <result status="valid" time="0.00"/>
       </proof>
-      <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
-       <result status="valid" time="0.03"/>
+      <proof
+       prover="alt-ergo"
+       timelimit="10"
+       edited=""
+       obsolete="false">
+       <result status="valid" time="0.02"/>
       </proof>
-      <proof prover="z3" timelimit="10" edited="" obsolete="false">
-       <result status="valid" time="0.01"/>
+      <proof
+       prover="z3"
+       timelimit="10"
+       edited=""
+       obsolete="false">
+       <result status="valid" time="0.00"/>
       </proof>
      </goal>
-     <goal name="WP_parameter compact.2" expl="for loop initialization" sum="2bcce785c763c3cb52e78fd3d7d04937" proved="true" expanded="true" shape="ainfix <=anum_ofV1c0c0c0Aainfix =V2anum_ofV1c0c0Aainfix <=c0V2Iainfix <=c0ainfix -V0c1Iainfix =V2c0FIainfix >=c0c0Iainfix >c0ainfix -V0c1FF">
-      <proof prover="cvc3" timelimit="10" edited="" obsolete="false">
-       <result status="valid" time="0.01"/>
+     <goal
+      name="WP_parameter compact.2"
+      expl="for loop initialization"
+      sum="846707997ff357d052b12b2b479875f5"
+      proved="true"
+      expanded="true"
+      shape="ainfix <=anum_ofV1c0c0c0Aainfix =V2anum_ofV1c0c0Aainfix <=c0V2Iainfix <=c0ainfix -V0c1Iainfix =V2c0FIainfix >=c0c0Iainfix >c0ainfix -V0c1FF">
+      <proof
+       prover="cvc3"
+       timelimit="10"
+       edited=""
+       obsolete="false">
+       <result status="valid" time="0.00"/>
       </proof>
-      <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
+      <proof
+       prover="alt-ergo"
+       timelimit="10"
+       edited=""
+       obsolete="false">
        <result status="valid" time="0.01"/>
       </proof>
-      <proof prover="z3" timelimit="10" edited="" obsolete="false">
-       <result status="valid" time="0.03"/>
+      <proof
+       prover="z3"
+       timelimit="10"
+       edited=""
+       obsolete="false">
+       <result status="valid" time="0.01"/>
       </proof>
      </goal>
-     <goal name="WP_parameter compact.3" expl="for loop preservation" sum="de475910adf8d5aa313ce875c86833e8" proved="true" expanded="true" shape="iainfix =agetV1V5c0Nainfix <=anum_ofV1c0ainfix +V5c1ainfix +V5c1Aainfix =V7anum_ofV1c0ainfix +V5c1Aainfix <=c0V7Iainfix =V7ainfix +V4c1FIainfix =V6asetV3V4agetV1V5FAainfix <V4c0Aainfix <=c0V4Aainfix <V5V0Aainfix <=c0V5ainfix <=anum_ofV1c0ainfix +V5c1ainfix +V5c1Aainfix =V4anum_ofV1c0ainfix +V5c1Aainfix <=c0V4Aainfix <V5V0Aainfix <=c0V5Iainfix <=anum_ofV1c0V5V5Aainfix =V4anum_ofV1c0V5Aainfix <=c0V4Iainfix <=V5ainfix -V0c1Aainfix <=c0V5FFFIainfix <=c0ainfix -V0c1Iainfix =V2c0FIainfix >=c0c0Iainfix >c0ainfix -V0c1FF">
-      <proof prover="cvc3" timelimit="10" edited="" obsolete="false">
-       <result status="valid" time="0.01"/>
+     <goal
+      name="WP_parameter compact.3"
+      expl="for loop preservation"
+      sum="846df15b2d09e49c92d2c3fcb5ae5b2b"
+      proved="true"
+      expanded="true"
+      shape="iainfix =agetV1V5c0Nainfix <=anum_ofV1c0ainfix +V5c1ainfix +V5c1Aainfix =V7anum_ofV1c0ainfix +V5c1Aainfix <=c0V7Iainfix =V7ainfix +V4c1FIainfix =V6asetV3V4agetV1V5FAainfix <V4c0Aainfix <=c0V4Aainfix <V5V0Aainfix <=c0V5ainfix <=anum_ofV1c0ainfix +V5c1ainfix +V5c1Aainfix =V4anum_ofV1c0ainfix +V5c1Aainfix <=c0V4Aainfix <V5V0Aainfix <=c0V5Iainfix <=anum_ofV1c0V5V5Aainfix =V4anum_ofV1c0V5Aainfix <=c0V4Iainfix <=V5ainfix -V0c1Aainfix <=c0V5FFFIainfix <=c0ainfix -V0c1Iainfix =V2c0FIainfix >=c0c0Iainfix >c0ainfix -V0c1FF">
+      <proof
+       prover="cvc3"
+       timelimit="10"
+       edited=""
+       obsolete="false">
+       <result status="valid" time="0.00"/>
       </proof>
-      <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
+      <proof
+       prover="alt-ergo"
+       timelimit="10"
+       edited=""
+       obsolete="false">
        <result status="valid" time="0.02"/>
       </proof>
-      <proof prover="z3" timelimit="10" edited="" obsolete="false">
-       <result status="valid" time="0.02"/>
+      <proof
+       prover="z3"
+       timelimit="10"
+       edited=""
+       obsolete="false">
+       <result status="valid" time="0.01"/>
       </proof>
      </goal>
-     <goal name="WP_parameter compact.4" expl="for loop initialization" sum="f5287bb871d14db412179b4328d414ea" proved="true" expanded="true" shape="ainfix <=anum_ofV1c0c0c0Aainfix =c0anum_ofV1c0c0Aainfix <=c0c0Iainfix <=c0ainfix -V0c1FF">
-      <proof prover="cvc3" timelimit="10" edited="" obsolete="false">
-       <result status="valid" time="0.02"/>
+     <goal
+      name="WP_parameter compact.4"
+      expl="for loop initialization"
+      sum="e9dbcffca310c8d6b9006e842776e9a9"
+      proved="true"
+      expanded="true"
+      shape="ainfix <=anum_ofV1c0c0c0Aainfix =c0anum_ofV1c0c0Aainfix <=c0c0Iainfix <=c0ainfix -V0c1FF">
+      <proof
+       prover="cvc3"
+       timelimit="10"
+       edited=""
+       obsolete="false">
+       <result status="valid" time="0.00"/>
       </proof>
-      <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
-       <result status="valid" time="0.03"/>
+      <proof
+       prover="alt-ergo"
+       timelimit="10"
+       edited=""
+       obsolete="false">
+       <result status="valid" time="0.02"/>
       </proof>
-      <proof prover="z3" timelimit="10" edited="" obsolete="false">
-       <result status="valid" time="0.03"/>
+      <proof
+       prover="z3"
+       timelimit="10"
+       edited=""
+       obsolete="false">
+       <result status="valid" time="0.01"/>
       </proof>
      </goal>
-     <goal name="WP_parameter compact.5" expl="for loop preservation" sum="90345f3f3fbf5ffccfe847869df0b67e" proved="true" expanded="true" shape="iainfix =agetV1V3c0Nainfix <=anum_ofV1c0ainfix +V3c1ainfix +V3c1Aainfix =V4anum_ofV1c0ainfix +V3c1Aainfix <=c0V4Iainfix =V4ainfix +V2c1Fainfix <=anum_ofV1c0ainfix +V3c1ainfix +V3c1Aainfix =V2anum_ofV1c0ainfix +V3c1Aainfix <=c0V2Aainfix <V3V0Aainfix <=c0V3Iainfix <=anum_ofV1c0V3V3Aainfix =V2anum_ofV1c0V3Aainfix <=c0V2Iainfix <=V3ainfix -V0c1Aainfix <=c0V3FFIainfix <=c0ainfix -V0c1FF">
-      <proof prover="cvc3" timelimit="10" edited="" obsolete="false">
-       <result status="valid" time="0.02"/>
+     <goal
+      name="WP_parameter compact.5"
+      expl="for loop preservation"
+      sum="ae7a8a36678a4aa212199a9a1af9d1aa"
+      proved="true"
+      expanded="true"
+      shape="iainfix =agetV1V3c0Nainfix <=anum_ofV1c0ainfix +V3c1ainfix +V3c1Aainfix =V4anum_ofV1c0ainfix +V3c1Aainfix <=c0V4Iainfix =V4ainfix +V2c1Fainfix <=anum_ofV1c0ainfix +V3c1ainfix +V3c1Aainfix =V2anum_ofV1c0ainfix +V3c1Aainfix <=c0V2Aainfix <V3V0Aainfix <=c0V3Iainfix <=anum_ofV1c0V3V3Aainfix =V2anum_ofV1c0V3Aainfix <=c0V2Iainfix <=V3ainfix -V0c1Aainfix <=c0V3FFIainfix <=c0ainfix -V0c1FF">
+      <proof
+       prover="cvc3"
+       timelimit="10"
+       edited=""
+       obsolete="false">
+       <result status="valid" time="0.00"/>
       </proof>
-      <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
-       <result status="valid" time="0.05"/>
+      <proof
+       prover="alt-ergo"
+       timelimit="10"
+       edited=""
+       obsolete="false">
+       <result status="valid" time="0.04"/>
       </proof>
-      <proof prover="z3" timelimit="10" edited="" obsolete="false">
-       <result status="valid" time="0.03"/>
+      <proof
+       prover="z3"
+       timelimit="10"
+       edited=""
+       obsolete="false">
+       <result status="valid" time="0.02"/>
       </proof>
      </goal>
-     <goal name="WP_parameter compact.6" expl="precondition" sum="cc20a288fcb1a7dd081072845705f406" proved="true" expanded="true" shape="ainfix >=V2c0Iainfix <=anum_ofV1c0ainfix +ainfix -V0c1c1ainfix +ainfix -V0c1c1Aainfix =V2anum_ofV1c0ainfix +ainfix -V0c1c1Aainfix <=c0V2FIainfix <=c0ainfix -V0c1FF">
-      <proof prover="cvc3" timelimit="10" edited="" obsolete="false">
-       <result status="valid" time="0.01"/>
+     <goal
+      name="WP_parameter compact.6"
+      expl="precondition"
+      sum="38edff5bd35566635e235b736236c61d"
+      proved="true"
+      expanded="true"
+      shape="ainfix >=V2c0Iainfix <=anum_ofV1c0ainfix +ainfix -V0c1c1ainfix +ainfix -V0c1c1Aainfix =V2anum_ofV1c0ainfix +ainfix -V0c1c1Aainfix <=c0V2FIainfix <=c0ainfix -V0c1FF">
+      <proof
+       prover="cvc3"
+       timelimit="10"
+       edited=""
+       obsolete="false">
+       <result status="valid" time="0.00"/>
       </proof>
-      <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
+      <proof
+       prover="alt-ergo"
+       timelimit="10"
+       edited=""
+       obsolete="false">
        <result status="valid" time="0.02"/>
       </proof>
-      <proof prover="z3" timelimit="10" edited="" obsolete="false">
-       <result status="valid" time="0.03"/>
+      <proof
+       prover="z3"
+       timelimit="10"
+       edited=""
+       obsolete="false">
+       <result status="valid" time="0.01"/>
       </proof>
      </goal>
-     <goal name="WP_parameter compact.7" expl="for loop initialization" sum="c808a28af9ecbd8d0c27c0c39fd0a7a6" proved="true" expanded="true" shape="ainfix <=anum_ofV1c0c0c0Aainfix =V3anum_ofV1c0c0Aainfix <=c0V3Iainfix <=c0ainfix -V0c1Iainfix =V3c0FIainfix >=V2c0Iainfix <=anum_ofV1c0ainfix +ainfix -V0c1c1ainfix +ainfix -V0c1c1Aainfix =V2anum_ofV1c0ainfix +ainfix -V0c1c1Aainfix <=c0V2FIainfix <=c0ainfix -V0c1FF">
-      <proof prover="cvc3" timelimit="10" edited="" obsolete="false">
-       <result status="valid" time="0.02"/>
+     <goal
+      name="WP_parameter compact.7"
+      expl="for loop initialization"
+      sum="eb82285d7d3d60ca39435ee968e03f4c"
+      proved="true"
+      expanded="true"
+      shape="ainfix <=anum_ofV1c0c0c0Aainfix =V3anum_ofV1c0c0Aainfix <=c0V3Iainfix <=c0ainfix -V0c1Iainfix =V3c0FIainfix >=V2c0Iainfix <=anum_ofV1c0ainfix +ainfix -V0c1c1ainfix +ainfix -V0c1c1Aainfix =V2anum_ofV1c0ainfix +ainfix -V0c1c1Aainfix <=c0V2FIainfix <=c0ainfix -V0c1FF">
+      <proof
+       prover="cvc3"
+       timelimit="10"
+       edited=""
+       obsolete="false">
+       <result status="valid" time="0.00"/>
       </proof>
-      <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
+      <proof
+       prover="alt-ergo"
+       timelimit="10"
+       edited=""
+       obsolete="false">
        <result status="valid" time="0.02"/>
       </proof>
-      <proof prover="z3" timelimit="10" edited="" obsolete="false">
-       <result status="valid" time="0.03"/>
+      <proof
+       prover="z3"
+       timelimit="10"
+       edited=""
+       obsolete="false">
+       <result status="valid" time="0.01"/>
       </proof>
      </goal>
-     <goal name="WP_parameter compact.8" expl="for loop preservation" sum="a64be74b762c3de543dddce122a7c4cf" proved="true" expanded="true" shape="iainfix =agetV1V6c0Nainfix <=anum_ofV1c0ainfix +V6c1ainfix +V6c1Aainfix =V8anum_ofV1c0ainfix +V6c1Aainfix <=c0V8Iainfix =V8ainfix +V5c1FIainfix =V7asetV4V5agetV1V6FAainfix <V5V2Aainfix <=c0V5Aainfix <V6V0Aainfix <=c0V6ainfix <=anum_ofV1c0ainfix +V6c1ainfix +V6c1Aainfix =V5anum_ofV1c0ainfix +V6c1Aainfix <=c0V5Aainfix <V6V0Aainfix <=c0V6Iainfix <=anum_ofV1c0V6V6Aainfix =V5anum_ofV1c0V6Aainfix <=c0V5Iainfix <=V6ainfix -V0c1Aainfix <=c0V6FFFIainfix <=c0ainfix -V0c1Iainfix =V3c0FIainfix >=V2c0Iainfix <=anum_ofV1c0ainfix +ainfix -V0c1c1ainfix +ainfix -V0c1c1Aainfix =V2anum_ofV1c0ainfix +ainfix -V0c1c1Aainfix <=c0V2FIainfix <=c0ainfix -V0c1FF">
-      <proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
-       <result status="valid" time="0.10"/>
+     <goal
+      name="WP_parameter compact.8"
+      expl="for loop preservation"
+      sum="33bcca83eb809eebe713a95d46403d05"
+      proved="true"
+      expanded="true"
+      shape="iainfix =agetV1V6c0Nainfix <=anum_ofV1c0ainfix +V6c1ainfix +V6c1Aainfix =V8anum_ofV1c0ainfix +V6c1Aainfix <=c0V8Iainfix =V8ainfix +V5c1FIainfix =V7asetV4V5agetV1V6FAainfix <V5V2Aainfix <=c0V5Aainfix <V6V0Aainfix <=c0V6ainfix <=anum_ofV1c0ainfix +V6c1ainfix +V6c1Aainfix =V5anum_ofV1c0ainfix +V6c1Aainfix <=c0V5Aainfix <V6V0Aainfix <=c0V6Iainfix <=anum_ofV1c0V6V6Aainfix =V5anum_ofV1c0V6Aainfix <=c0V5Iainfix <=V6ainfix -V0c1Aainfix <=c0V6FFFIainfix <=c0ainfix -V0c1Iainfix =V3c0FIainfix >=V2c0Iainfix <=anum_ofV1c0ainfix +ainfix -V0c1c1ainfix +ainfix -V0c1c1Aainfix =V2anum_ofV1c0ainfix +ainfix -V0c1c1Aainfix <=c0V2FIainfix <=c0ainfix -V0c1FF">
+      <proof
+       prover="alt-ergo"
+       timelimit="10"
+       edited=""
+       obsolete="false">
+       <result status="valid" time="0.09"/>
       </proof>
-      <proof prover="z3" timelimit="10" edited="" obsolete="false">
-       <result status="valid" time="0.05"/>
+      <proof
+       prover="z3"
+       timelimit="10"
+       edited=""
+       obsolete="false">
+       <result status="valid" time="0.02"/>
       </proof>
      </goal>
     </transf>