diff --git a/examples/distributedLockNetwork/LDTDupl/why3session.xml b/examples/distributedLockNetwork/LDTDupl/why3session.xml
index e2abdca..f727250 100644
--- a/examples/distributedLockNetwork/LDTDupl/why3session.xml
+++ b/examples/distributedLockNetwork/LDTDupl/why3session.xml
@@ -126,7 +126,7 @@
       <proof prover="7" timelimit="1"><result status="valid" time="0.77" steps="6255"/></proof>
       </goal>
       <goal name="handleMsg&#39;refn&#39;vc.0.0.0.0.5" expl="postcondition" proved="true">
-      <proof prover="7" timelimit="5"><result status="valid" time="2.68" steps="42422"/></proof>
+      <proof prover="5" timelimit="10" memlimit="1000"><result status="valid" time="1.22" steps="158463"/></proof>
       </goal>
       <goal name="handleMsg&#39;refn&#39;vc.0.0.0.0.6" expl="postcondition" proved="true">
       <proof prover="5"><result status="valid" time="1.15" steps="84540"/></proof>
diff --git a/examples/leaderElection/ChangRoberts/why3session.xml b/examples/leaderElection/ChangRoberts/why3session.xml
index c2a5c50..81a4e41 100644
--- a/examples/leaderElection/ChangRoberts/why3session.xml
+++ b/examples/leaderElection/ChangRoberts/why3session.xml
@@ -56,7 +56,7 @@
     <goal name="act&#39;vc.0.9.0" expl="postcondition" proved="true">
     <transf name="split_vc" proved="true" >
      <goal name="act&#39;vc.0.9.0.0" expl="postcondition" proved="true">
-     <proof prover="3" memlimit="2000"><result status="valid" time="1.51" steps="125186"/></proof>
+     <proof prover="3" timelimit="20"><result status="valid" time="13.78" steps="904149"/></proof>
      </goal>
     </transf>
     </goal>
diff --git a/examples/mutualExclusionConcurrent/BakeryAtomic/why3session.xml b/examples/mutualExclusionConcurrent/BakeryAtomic/why3session.xml
index e1ec84e..b55718d 100644
--- a/examples/mutualExclusionConcurrent/BakeryAtomic/why3session.xml
+++ b/examples/mutualExclusionConcurrent/BakeryAtomic/why3session.xml
@@ -10,23 +10,23 @@
 <path name=".."/><path name="BakeryAtomic.mlw"/>
 <theory name="BakeryAtomic" proved="true">
  <goal name="refn&#39;vc" expl="VC for refn" proved="true">
- <proof prover="2"><result status="valid" time="0.000000" steps="0"/></proof>
+ <proof prover="2"><result status="valid" time="0.00" steps="0"/></proof>
  </goal>
  <goal name="a1&#39;vc" expl="VC for a1" proved="true">
  <transf name="split_vc" proved="true" >
   <goal name="a1&#39;vc.0" expl="postcondition" proved="true">
-  <proof prover="1" timelimit="5"><result status="valid" time="2.169501" steps="190441"/></proof>
+  <proof prover="1" timelimit="5"><result status="valid" time="2.69" steps="190441"/></proof>
   </goal>
   <goal name="a1&#39;vc.1" expl="postcondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.230000" steps="49415"/></proof>
+  <proof prover="0"><result status="valid" time="0.23" steps="49415"/></proof>
   </goal>
  </transf>
  </goal>
  <goal name="a2&#39;vc" expl="VC for a2" proved="true">
  <transf name="split_vc" proved="true" >
   <goal name="a2&#39;vc.0" expl="witness existence" proved="true">
-  <proof prover="2"><result status="valid" time="0.000000" steps="10"/></proof>
-  <proof prover="3"><result status="valid" time="0.020000"/></proof>
+  <proof prover="2"><result status="valid" time="0.00" steps="12"/></proof>
+  <proof prover="3"><result status="valid" time="0.02"/></proof>
   </goal>
   <goal name="a2&#39;vc.1" expl="postcondition" proved="true">
   <transf name="split_vc" proved="true" >
@@ -37,16 +37,16 @@
      <goal name="a2&#39;vc.1.0.0.0" expl="postcondition" proved="true">
      <transf name="split_all_full" proved="true" >
       <goal name="a2&#39;vc.1.0.0.0.0" expl="postcondition" proved="true">
-      <proof prover="1"><result status="valid" time="0.040000" steps="17151"/></proof>
+      <proof prover="1"><result status="valid" time="0.04" steps="17322"/></proof>
       </goal>
       <goal name="a2&#39;vc.1.0.0.0.1" expl="postcondition" proved="true">
-      <proof prover="2"><result status="valid" time="0.050000" steps="350"/></proof>
+      <proof prover="2"><result status="valid" time="0.05" steps="367"/></proof>
       </goal>
       <goal name="a2&#39;vc.1.0.0.0.2" expl="postcondition" proved="true">
-      <proof prover="1"><result status="valid" time="0.140000" steps="37509"/></proof>
+      <proof prover="1"><result status="valid" time="0.14" steps="37680"/></proof>
       </goal>
       <goal name="a2&#39;vc.1.0.0.0.3" expl="postcondition" proved="true">
-      <proof prover="1"><result status="valid" time="0.130000" steps="38384"/></proof>
+      <proof prover="1"><result status="valid" time="0.13" steps="38545"/></proof>
       </goal>
      </transf>
      </goal>
@@ -61,16 +61,16 @@
      <goal name="a2&#39;vc.1.1.0.0" expl="postcondition" proved="true">
      <transf name="split_all_full" proved="true" >
       <goal name="a2&#39;vc.1.1.0.0.0" expl="postcondition" proved="true">
-      <proof prover="1"><result status="valid" time="0.050000" steps="18164"/></proof>
+      <proof prover="1"><result status="valid" time="0.05" steps="18590"/></proof>
       </goal>
       <goal name="a2&#39;vc.1.1.0.0.1" expl="postcondition" proved="true">
-      <proof prover="2"><result status="valid" time="0.020000" steps="727"/></proof>
+      <proof prover="2"><result status="valid" time="0.02" steps="751"/></proof>
       </goal>
       <goal name="a2&#39;vc.1.1.0.0.2" expl="postcondition" proved="true">
-      <proof prover="1"><result status="valid" time="0.810269" steps="94345"/></proof>
+      <proof prover="1"><result status="valid" time="0.81" steps="94771"/></proof>
       </goal>
       <goal name="a2&#39;vc.1.1.0.0.3" expl="postcondition" proved="true">
-      <proof prover="1" timelimit="3"><result status="valid" time="1.350219" steps="129019"/></proof>
+      <proof prover="1" timelimit="3"><result status="valid" time="1.79" steps="136518"/></proof>
       </goal>
      </transf>
      </goal>
@@ -81,16 +81,16 @@
      <goal name="a2&#39;vc.1.1.1.0" expl="postcondition" proved="true">
      <transf name="split_all_full" proved="true" >
       <goal name="a2&#39;vc.1.1.1.0.0" expl="postcondition" proved="true">
-      <proof prover="1"><result status="valid" time="0.040000" steps="18514"/></proof>
+      <proof prover="1"><result status="valid" time="0.04" steps="18658"/></proof>
       </goal>
       <goal name="a2&#39;vc.1.1.1.0.1" expl="postcondition" proved="true">
-      <proof prover="2"><result status="valid" time="0.040000" steps="709"/></proof>
+      <proof prover="2"><result status="valid" time="0.04" steps="753"/></proof>
       </goal>
       <goal name="a2&#39;vc.1.1.1.0.2" expl="postcondition" proved="true">
-      <proof prover="1"><result status="valid" time="1.044720" steps="108550"/></proof>
+      <proof prover="1"><result status="valid" time="0.38" steps="59273"/></proof>
       </goal>
       <goal name="a2&#39;vc.1.1.1.0.3" expl="postcondition" proved="true">
-      <proof prover="1" timelimit="5"><result status="valid" time="2.036490" steps="174527"/></proof>
+      <proof prover="1" timelimit="5"><result status="valid" time="0.31" steps="49964"/></proof>
       </goal>
      </transf>
      </goal>
@@ -103,10 +103,10 @@
   <goal name="a2&#39;vc.2" expl="postcondition" proved="true">
   <transf name="split_vc" proved="true" >
    <goal name="a2&#39;vc.2.0" expl="postcondition" proved="true">
-   <proof prover="0"><result status="valid" time="0.300000" steps="59394"/></proof>
+   <proof prover="0"><result status="valid" time="0.30" steps="59226"/></proof>
    </goal>
    <goal name="a2&#39;vc.2.1" expl="postcondition" proved="true">
-   <proof prover="0"><result status="valid" time="0.090000" steps="20064"/></proof>
+   <proof prover="0"><result status="valid" time="0.09" steps="20408"/></proof>
    </goal>
   </transf>
   </goal>
@@ -119,23 +119,23 @@
    <goal name="a3&#39;vc.0.0" expl="postcondition" proved="true">
    <transf name="split_all_full" proved="true" >
     <goal name="a3&#39;vc.0.0.0" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.040000" steps="17355"/></proof>
+    <proof prover="1"><result status="valid" time="0.04" steps="17355"/></proof>
     </goal>
     <goal name="a3&#39;vc.0.0.1" expl="postcondition" proved="true">
-    <proof prover="2"><result status="valid" time="0.020000" steps="341"/></proof>
+    <proof prover="2"><result status="valid" time="0.02" steps="341"/></proof>
     </goal>
     <goal name="a3&#39;vc.0.0.2" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.090000" steps="36107"/></proof>
+    <proof prover="1"><result status="valid" time="0.20" steps="36107"/></proof>
     </goal>
     <goal name="a3&#39;vc.0.0.3" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.245099" steps="41403"/></proof>
+    <proof prover="1"><result status="valid" time="0.25" steps="41403"/></proof>
     </goal>
    </transf>
    </goal>
   </transf>
   </goal>
   <goal name="a3&#39;vc.1" expl="postcondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.290000" steps="64442"/></proof>
+  <proof prover="0"><result status="valid" time="0.29" steps="64442"/></proof>
   </goal>
  </transf>
  </goal>
@@ -146,30 +146,30 @@
    <goal name="a4&#39;vc.0.0" expl="postcondition" proved="true">
    <transf name="split_all_full" proved="true" >
     <goal name="a4&#39;vc.0.0.0" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.040000" steps="14249"/></proof>
+    <proof prover="1"><result status="valid" time="0.04" steps="14249"/></proof>
     </goal>
     <goal name="a4&#39;vc.0.0.1" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.050000" steps="17835"/></proof>
+    <proof prover="1"><result status="valid" time="0.05" steps="17835"/></proof>
     </goal>
     <goal name="a4&#39;vc.0.0.2" expl="postcondition" proved="true">
-    <proof prover="0"><result status="valid" time="0.590000" steps="67937"/></proof>
+    <proof prover="0"><result status="valid" time="0.59" steps="67937"/></proof>
     </goal>
     <goal name="a4&#39;vc.0.0.3" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.070000" steps="26046"/></proof>
+    <proof prover="1"><result status="valid" time="0.07" steps="26046"/></proof>
     </goal>
    </transf>
    </goal>
   </transf>
   </goal>
   <goal name="a4&#39;vc.1" expl="postcondition" proved="true">
-  <proof prover="0" timelimit="3"><result status="valid" time="0.850000" steps="122675"/></proof>
+  <proof prover="0" timelimit="3"><result status="valid" time="1.13" steps="122675"/></proof>
   </goal>
  </transf>
  </goal>
  <goal name="a5&#39;vc" expl="VC for a5" proved="true">
  <transf name="split_vc" proved="true" >
   <goal name="a5&#39;vc.0" expl="witness existence" proved="true">
-  <proof prover="3"><result status="valid" time="0.020000"/></proof>
+  <proof prover="3"><result status="valid" time="0.02"/></proof>
   </goal>
   <goal name="a5&#39;vc.1" expl="postcondition" proved="true">
   <transf name="split_vc" proved="true" >
@@ -178,16 +178,16 @@
     <goal name="a5&#39;vc.1.0.0" expl="postcondition" proved="true">
     <transf name="split_all_full" proved="true" >
      <goal name="a5&#39;vc.1.0.0.0" expl="postcondition" proved="true">
-     <proof prover="2"><result status="valid" time="0.410000" steps="6934"/></proof>
+     <proof prover="2"><result status="valid" time="0.67" steps="6913"/></proof>
      </goal>
      <goal name="a5&#39;vc.1.0.0.1" expl="postcondition" proved="true">
-     <proof prover="2"><result status="valid" time="0.030000" steps="624"/></proof>
+     <proof prover="2"><result status="valid" time="0.03" steps="638"/></proof>
      </goal>
      <goal name="a5&#39;vc.1.0.0.2" expl="postcondition" proved="true">
-     <proof prover="1" timelimit="3"><result status="valid" time="1.290079" steps="149426"/></proof>
+     <proof prover="1" timelimit="3"><result status="valid" time="1.29" steps="149493"/></proof>
      </goal>
      <goal name="a5&#39;vc.1.0.0.3" expl="postcondition" proved="true">
-     <proof prover="1"><result status="valid" time="0.549909" steps="68843"/></proof>
+     <proof prover="1"><result status="valid" time="0.55" steps="69001"/></proof>
      </goal>
     </transf>
     </goal>
@@ -198,16 +198,16 @@
     <goal name="a5&#39;vc.1.1.0" expl="postcondition" proved="true">
     <transf name="split_all_full" proved="true" >
      <goal name="a5&#39;vc.1.1.0.0" expl="postcondition" proved="true">
-     <proof prover="2"><result status="valid" time="0.520000" steps="5765"/></proof>
+     <proof prover="2"><result status="valid" time="0.88" steps="12049"/></proof>
      </goal>
      <goal name="a5&#39;vc.1.1.0.1" expl="postcondition" proved="true">
-     <proof prover="2"><result status="valid" time="0.270000" steps="3516"/></proof>
+     <proof prover="2"><result status="valid" time="0.47" steps="3966"/></proof>
      </goal>
      <goal name="a5&#39;vc.1.1.0.2" expl="postcondition" proved="true">
-     <proof prover="1"><result status="valid" time="0.771071" steps="93914"/></proof>
+     <proof prover="1"><result status="valid" time="0.77" steps="94045"/></proof>
      </goal>
      <goal name="a5&#39;vc.1.1.0.3" expl="postcondition" proved="true">
-     <proof prover="1"><result status="valid" time="0.705338" steps="95562"/></proof>
+     <proof prover="1"><result status="valid" time="0.71" steps="95718"/></proof>
      </goal>
     </transf>
     </goal>
@@ -216,7 +216,7 @@
   </transf>
   </goal>
   <goal name="a5&#39;vc.2" expl="postcondition" proved="true">
-  <proof prover="2" timelimit="5"><result status="valid" time="0.350000" steps="4661"/></proof>
+  <proof prover="2" timelimit="5"><result status="valid" time="0.67" steps="10057"/></proof>
   </goal>
   <goal name="a5&#39;vc.3" expl="postcondition" proved="true">
   <transf name="split_vc" proved="true" >
@@ -227,7 +227,7 @@
      <goal name="a5&#39;vc.3.0.0.0" expl="postcondition" proved="true">
      <transf name="split_vc" proved="true" >
       <goal name="a5&#39;vc.3.0.0.0.0" expl="postcondition" proved="true">
-      <proof prover="1" timelimit="30" memlimit="4000"><result status="valid" time="0.110000" steps="46623"/></proof>
+      <proof prover="1" timelimit="30" memlimit="4000"><result status="valid" time="0.29" steps="51182"/></proof>
       </goal>
      </transf>
      </goal>
@@ -240,7 +240,7 @@
     <goal name="a5&#39;vc.3.1.0" expl="postcondition" proved="true">
     <transf name="split_all_full" proved="true" >
      <goal name="a5&#39;vc.3.1.0.0" expl="postcondition" proved="true">
-     <proof prover="1"><result status="valid" time="0.020000" steps="10564"/></proof>
+     <proof prover="1"><result status="valid" time="0.02" steps="10785"/></proof>
      </goal>
     </transf>
     </goal>
@@ -257,23 +257,23 @@
    <goal name="a5a&#39;vc.0.0" expl="postcondition" proved="true">
    <transf name="split_all_full" proved="true" >
     <goal name="a5a&#39;vc.0.0.0" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.030000" steps="12989"/></proof>
+    <proof prover="1"><result status="valid" time="0.03" steps="12989"/></proof>
     </goal>
     <goal name="a5a&#39;vc.0.0.1" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.040000" steps="17473"/></proof>
+    <proof prover="1"><result status="valid" time="0.04" steps="17473"/></proof>
     </goal>
     <goal name="a5a&#39;vc.0.0.2" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.271119" steps="48072"/></proof>
+    <proof prover="1"><result status="valid" time="0.27" steps="48072"/></proof>
     </goal>
     <goal name="a5a&#39;vc.0.0.3" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.259240" steps="48389"/></proof>
+    <proof prover="1"><result status="valid" time="0.26" steps="48389"/></proof>
     </goal>
    </transf>
    </goal>
   </transf>
   </goal>
   <goal name="a5a&#39;vc.1" expl="postcondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.090000" steps="27179"/></proof>
+  <proof prover="0"><result status="valid" time="0.09" steps="27344"/></proof>
   </goal>
  </transf>
  </goal>
@@ -284,16 +284,16 @@
    <goal name="a6&#39;vc.0.0" expl="postcondition" proved="true">
    <transf name="split_all_full" proved="true" >
     <goal name="a6&#39;vc.0.0.0" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.050000" steps="24467"/></proof>
+    <proof prover="1"><result status="valid" time="0.05" steps="24467"/></proof>
     </goal>
     <goal name="a6&#39;vc.0.0.1" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.050000" steps="22755"/></proof>
+    <proof prover="1"><result status="valid" time="0.05" steps="22755"/></proof>
     </goal>
     <goal name="a6&#39;vc.0.0.2" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="1.089243" steps="128795"/></proof>
+    <proof prover="1"><result status="valid" time="1.31" steps="128795"/></proof>
     </goal>
     <goal name="a6&#39;vc.0.0.3" expl="postcondition" proved="true">
-    <proof prover="1" timelimit="3"><result status="valid" time="1.493804" steps="170673"/></proof>
+    <proof prover="1" timelimit="3"><result status="valid" time="1.92" steps="170673"/></proof>
     </goal>
    </transf>
    </goal>
@@ -304,7 +304,7 @@
    <goal name="a6&#39;vc.1.0" expl="postcondition" proved="true">
    <transf name="split_all_full" proved="true" >
     <goal name="a6&#39;vc.1.0.0" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.030000" steps="11381"/></proof>
+    <proof prover="1"><result status="valid" time="0.03" steps="11381"/></proof>
     </goal>
    </transf>
    </goal>
@@ -319,23 +319,23 @@
    <goal name="cs&#39;vc.0.0" expl="postcondition" proved="true">
    <transf name="split_all_full" proved="true" >
     <goal name="cs&#39;vc.0.0.0" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.050000" steps="21906"/></proof>
+    <proof prover="1"><result status="valid" time="0.05" steps="21906"/></proof>
     </goal>
     <goal name="cs&#39;vc.0.0.1" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.060000" steps="24927"/></proof>
+    <proof prover="1"><result status="valid" time="0.06" steps="24927"/></proof>
     </goal>
     <goal name="cs&#39;vc.0.0.2" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.335542" steps="61539"/></proof>
+    <proof prover="1"><result status="valid" time="0.34" steps="61543"/></proof>
     </goal>
     <goal name="cs&#39;vc.0.0.3" expl="postcondition" proved="true">
-    <proof prover="0" timelimit="3"><result status="valid" time="1.422400" steps="218921"/></proof>
+    <proof prover="0" timelimit="3"><result status="valid" time="1.78" steps="218921"/></proof>
     </goal>
    </transf>
    </goal>
   </transf>
   </goal>
   <goal name="cs&#39;vc.1" expl="postcondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.230000" steps="48681"/></proof>
+  <proof prover="0"><result status="valid" time="0.23" steps="48681"/></proof>
   </goal>
  </transf>
  </goal>
@@ -346,40 +346,40 @@
    <goal name="a7&#39;vc.0.0" expl="postcondition" proved="true">
    <transf name="split_all_full" proved="true" >
     <goal name="a7&#39;vc.0.0.0" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.050000" steps="20211"/></proof>
+    <proof prover="1"><result status="valid" time="0.05" steps="20210"/></proof>
     </goal>
     <goal name="a7&#39;vc.0.0.1" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.050000" steps="21860"/></proof>
+    <proof prover="1"><result status="valid" time="0.05" steps="21937"/></proof>
     </goal>
     <goal name="a7&#39;vc.0.0.2" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.323267" steps="55680"/></proof>
+    <proof prover="1"><result status="valid" time="0.32" steps="55916"/></proof>
     </goal>
     <goal name="a7&#39;vc.0.0.3" expl="postcondition" proved="true">
-    <proof prover="1"><result status="valid" time="0.090000" steps="29008"/></proof>
+    <proof prover="1"><result status="valid" time="0.09" steps="30672"/></proof>
     </goal>
    </transf>
    </goal>
   </transf>
   </goal>
   <goal name="a7&#39;vc.1" expl="postcondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.731632" steps="101173"/></proof>
+  <proof prover="0"><result status="valid" time="0.91" steps="101173"/></proof>
   </goal>
  </transf>
  </goal>
  <goal name="initWorldA&#39;refn&#39;vc" expl="VC for initWorldA&#39;refn" proved="true">
- <proof prover="2"><result status="valid" time="0.000000" steps="18"/></proof>
+ <proof prover="2"><result status="valid" time="0.00" steps="18"/></proof>
  </goal>
  <goal name="initWorldC&#39;refn&#39;vc" expl="VC for initWorldC&#39;refn" proved="true">
- <proof prover="2"><result status="valid" time="0.010000" steps="198"/></proof>
+ <proof prover="2"><result status="valid" time="0.01" steps="198"/></proof>
  </goal>
  <goal name="stepA&#39;refn&#39;vc" expl="VC for stepA&#39;refn" proved="true">
- <proof prover="2"><result status="valid" time="0.010000" steps="42"/></proof>
+ <proof prover="2"><result status="valid" time="0.01" steps="42"/></proof>
  </goal>
  <goal name="stepC&#39;refn&#39;vc" expl="VC for stepC&#39;refn" proved="true">
- <proof prover="2"><result status="valid" time="0.020000" steps="367"/></proof>
+ <proof prover="2"><result status="valid" time="0.02" steps="367"/></proof>
  </goal>
  <goal name="safety" proved="true">
- <proof prover="2" timelimit="5"><result status="valid" time="0.010000" steps="4"/></proof>
+ <proof prover="2" timelimit="5"><result status="valid" time="0.01" steps="4"/></proof>
  </goal>
 </theory>
 </file>
diff --git a/examples/mutualExclusionConcurrent/BakeryAtomic/why3shapes.gz b/examples/mutualExclusionConcurrent/BakeryAtomic/why3shapes.gz
index de14788..7dbece5 100644
Binary files a/examples/mutualExclusionConcurrent/BakeryAtomic/why3shapes.gz and b/examples/mutualExclusionConcurrent/BakeryAtomic/why3shapes.gz differ
diff --git a/examples/mutualExclusionConcurrent/Peterson/why3session.xml b/examples/mutualExclusionConcurrent/Peterson/why3session.xml
index 91f8326..779e8ec 100644
--- a/examples/mutualExclusionConcurrent/Peterson/why3session.xml
+++ b/examples/mutualExclusionConcurrent/Peterson/why3session.xml
@@ -9,34 +9,34 @@
 <path name=".."/><path name="Peterson.mlw"/>
 <theory name="Peterson" proved="true">
  <goal name="eq&#39;vc" expl="VC for eq" proved="true">
- <proof prover="1"><result status="valid" time="0.000000" steps="6"/></proof>
+ <proof prover="1"><result status="valid" time="0.00" steps="6"/></proof>
  </goal>
  <goal name="refn&#39;vc" expl="VC for refn" proved="true">
- <proof prover="1"><result status="valid" time="0.000000" steps="0"/></proof>
+ <proof prover="1"><result status="valid" time="0.00" steps="0"/></proof>
  </goal>
  <goal name="a1&#39;vc" expl="VC for a1" proved="true">
- <proof prover="0"><result status="valid" time="0.080000" steps="16549"/></proof>
+ <proof prover="0"><result status="valid" time="0.08" steps="16549"/></proof>
  </goal>
  <goal name="a2&#39;vc" expl="VC for a2" proved="true">
- <proof prover="0"><result status="valid" time="0.180000" steps="20859"/></proof>
+ <proof prover="0"><result status="valid" time="0.18" steps="20859"/></proof>
  </goal>
  <goal name="a3&#39;vc" expl="VC for a3" proved="true">
  <transf name="split_vc" proved="true" >
   <goal name="a3&#39;vc.0" expl="postcondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.060000" steps="1201"/></proof>
+  <proof prover="1"><result status="valid" time="0.06" steps="1309"/></proof>
   </goal>
   <goal name="a3&#39;vc.1" expl="postcondition" proved="true">
   <transf name="split_vc" proved="true" >
    <goal name="a3&#39;vc.1.0" expl="postcondition" proved="true">
-   <proof prover="2"><result status="valid" time="0.030000" steps="9473"/></proof>
+   <proof prover="2"><result status="valid" time="0.03" steps="9522"/></proof>
    </goal>
    <goal name="a3&#39;vc.1.1" expl="postcondition" proved="true">
    <transf name="split_vc" proved="true" >
     <goal name="a3&#39;vc.1.1.0" expl="postcondition" proved="true">
-    <proof prover="0" timelimit="5"><result status="valid" time="1.394695" steps="198668"/></proof>
+    <proof prover="0" timelimit="5"><result status="valid" time="1.39" steps="198668"/></proof>
     </goal>
     <goal name="a3&#39;vc.1.1.1" expl="postcondition" proved="true">
-    <proof prover="0" timelimit="5" memlimit="2000"><result status="valid" time="2.330000" steps="316869"/></proof>
+    <proof prover="0" timelimit="5" memlimit="2000"><result status="valid" time="2.33" steps="316869"/></proof>
     </goal>
    </transf>
    </goal>
@@ -47,33 +47,33 @@
  <goal name="cs&#39;vc" expl="VC for cs" proved="true">
  <transf name="split_vc" proved="true" >
   <goal name="cs&#39;vc.0" expl="postcondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.010000" steps="104"/></proof>
+  <proof prover="1"><result status="valid" time="0.01" steps="104"/></proof>
   </goal>
   <goal name="cs&#39;vc.1" expl="postcondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.870000" steps="94238"/></proof>
+  <proof prover="0"><result status="valid" time="0.87" steps="94238"/></proof>
   </goal>
  </transf>
  </goal>
  <goal name="a4&#39;vc" expl="VC for a4" proved="true">
- <proof prover="0"><result status="valid" time="0.100000" steps="19657"/></proof>
+ <proof prover="0"><result status="valid" time="0.10" steps="19657"/></proof>
  </goal>
  <goal name="initWorldA&#39;refn&#39;vc" expl="VC for initWorldA&#39;refn" proved="true">
- <proof prover="1"><result status="valid" time="0.010000" steps="16"/></proof>
+ <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
  </goal>
  <goal name="initWorldC&#39;refn&#39;vc" expl="VC for initWorldC&#39;refn" proved="true">
- <proof prover="1"><result status="valid" time="0.010000" steps="78"/></proof>
+ <proof prover="1"><result status="valid" time="0.01" steps="78"/></proof>
  </goal>
  <goal name="stepA&#39;refn&#39;vc" expl="VC for stepA&#39;refn" proved="true">
- <proof prover="1"><result status="valid" time="0.030000" steps="55"/></proof>
+ <proof prover="1"><result status="valid" time="0.03" steps="55"/></proof>
  </goal>
  <goal name="stepC&#39;refn&#39;vc" expl="VC for stepC&#39;refn" proved="true">
- <proof prover="1"><result status="valid" time="0.020000" steps="235"/></proof>
+ <proof prover="1"><result status="valid" time="0.02" steps="235"/></proof>
  </goal>
  <goal name="safety" proved="true">
- <proof prover="1"><result status="valid" time="0.010000" steps="84"/></proof>
+ <proof prover="1"><result status="valid" time="0.01" steps="84"/></proof>
  </goal>
  <goal name="safetyA" proved="true">
- <proof prover="1"><result status="valid" time="0.010000" steps="71"/></proof>
+ <proof prover="1"><result status="valid" time="0.01" steps="71"/></proof>
  </goal>
 </theory>
 </file>
diff --git a/examples/mutualExclusionConcurrent/Peterson/why3shapes.gz b/examples/mutualExclusionConcurrent/Peterson/why3shapes.gz
index 47f7bdd..dfe3f7a 100644
Binary files a/examples/mutualExclusionConcurrent/Peterson/why3shapes.gz and b/examples/mutualExclusionConcurrent/Peterson/why3shapes.gz differ
diff --git a/examples/paxosNoRefinement/paxos/why3session.xml b/examples/paxosNoRefinement/paxos/why3session.xml
index a9ec762..679deba 100644
--- a/examples/paxosNoRefinement/paxos/why3session.xml
+++ b/examples/paxosNoRefinement/paxos/why3session.xml
@@ -34,7 +34,19 @@
  <proof prover="3"><result status="valid" time="2.24" steps="13755"/></proof>
  </goal>
  <goal name="max_p" proved="true">
- <proof prover="2"><result status="valid" time="1.14" steps="128850"/></proof>
+ <transf name="split_vc" proved="true" >
+  <goal name="max_p.0" proved="true">
+  <transf name="inline_goal" proved="true" >
+   <goal name="max_p.0.0" proved="true">
+   <transf name="split_all_full" proved="true" >
+    <goal name="max_p.0.0.0" proved="true">
+    <proof prover="2" timelimit="1"><result status="valid" time="0.43" steps="80380"/></proof>
+    </goal>
+   </transf>
+   </goal>
+  </transf>
+  </goal>
+ </transf>
  </goal>
  <goal name="propose&#39;vc" expl="VC for propose" proved="true">
  <transf name="unfold" proved="true" arg1="indpred">
diff --git a/examples/paxosNoRefinement/paxos/why3shapes.gz b/examples/paxosNoRefinement/paxos/why3shapes.gz
index 8c5d4f3..0dc918b 100644
Binary files a/examples/paxosNoRefinement/paxos/why3shapes.gz and b/examples/paxosNoRefinement/paxos/why3shapes.gz differ
diff --git a/examples/waitFreeRegister/fourSlots/why3session.xml b/examples/waitFreeRegister/fourSlots/why3session.xml
index ee1e9b3..ca7398b 100644
--- a/examples/waitFreeRegister/fourSlots/why3session.xml
+++ b/examples/waitFreeRegister/fourSlots/why3session.xml
@@ -81,7 +81,7 @@
   <proof prover="2"><result status="valid" time="0.01" steps="16"/></proof>
   </goal>
   <goal name="a&#39;vc.1" expl="postcondition" proved="true">
-  <proof prover="2"><result status="valid" time="0.89" steps="18454"/></proof>
+  <proof prover="2" timelimit="10"><result status="valid" time="1.11" steps="18463"/></proof>
   </goal>
   <goal name="a&#39;vc.2" expl="postcondition" proved="true">
   <proof prover="0"><result status="valid" time="0.41" steps="72900"/></proof>
diff --git a/test.sh b/test.sh
index 5d613fd..4d99c45 100755
--- a/test.sh
+++ b/test.sh
@@ -73,4 +73,4 @@ echo "Failed: $failed" >> $GITHUB_STEP_SUMMARY
 
 echo ""
 echo "Replayed $runned from which $failed failed."
-exit $failed
\ No newline at end of file
+exit $failed