diff --git a/examples/mutualExclusionToken/selfstab-ring/why3session.xml b/examples/mutualExclusionToken/selfstab-ring/why3session.xml
index 0eab7b2..8293788 100644
--- a/examples/mutualExclusionToken/selfstab-ring/why3session.xml
+++ b/examples/mutualExclusionToken/selfstab-ring/why3session.xml
@@ -2,7 +2,7 @@
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "https://www.why3.org/why3session.dtd">
 <why3session shape_version="6">
-<prover id="0" name="Z3" version="4.11.2" timelimit="1" steplimit="0" memlimit="1000"/>
+<prover id="0" name="Z3" version="4.11.2" timelimit="1200" steplimit="0" memlimit="1000"/>
 <prover id="1" name="Alt-Ergo" version="2.4.2" timelimit="5" steplimit="0" memlimit="1000"/>
 <file format="whyml" proved="true">
 <path name=".."/><path name="selfstab-ring.mlw"/>
@@ -14,38 +14,30 @@
  <proof prover="1"><result status="valid" time="0.010000" steps="63"/></proof>
  </goal>
  <goal name="trans&#39;vc" expl="VC for trans" proved="true">
- <transf name="unfold" proved="true" arg1="inv">
-  <goal name="trans&#39;vc.0" expl="VC for trans" proved="true">
-  <transf name="split_all_full" proved="true" >
-   <goal name="trans&#39;vc.0.0" expl="postcondition" proved="true">
-   <proof prover="1" timelimit="1200"><result status="valid" time="0.754841" steps="32013"/></proof>
-   </goal>
-   <goal name="trans&#39;vc.0.1" expl="postcondition" proved="true">
-   <proof prover="1" timelimit="1200"><result status="valid" time="0.006626" steps="7"/></proof>
-   </goal>
-   <goal name="trans&#39;vc.0.2" expl="postcondition" proved="true">
-   <proof prover="0"><result status="valid" time="0.108042" steps="958375"/></proof>
-   </goal>
-   <goal name="trans&#39;vc.0.3" expl="postcondition" proved="true">
-   <proof prover="1" timelimit="1"><result status="valid" time="0.141224" steps="5729"/></proof>
-   </goal>
-   <goal name="trans&#39;vc.0.4" expl="postcondition" proved="true">
-   <proof prover="0"><result status="valid" time="0.019330" steps="79453"/></proof>
-   </goal>
-   <goal name="trans&#39;vc.0.5" expl="postcondition" proved="true">
-   <proof prover="0"><result status="valid" time="0.031172" steps="153247"/></proof>
-   </goal>
-   <goal name="trans&#39;vc.0.6" expl="postcondition" proved="true">
-   <transf name="split_vc" proved="true" >
-    <goal name="trans&#39;vc.0.6.0" expl="postcondition" proved="true">
-    <proof prover="0"><result status="valid" time="0.705729" steps="9210314"/></proof>
-    </goal>
-   </transf>
-   </goal>
-   <goal name="trans&#39;vc.0.7" expl="postcondition" proved="true">
-   <proof prover="0"><result status="valid" time="0.018245" steps="62654"/></proof>
-   </goal>
-  </transf>
+ <transf name="split_all_full" proved="true" >
+  <goal name="trans&#39;vc.0" expl="postcondition" proved="true">
+  <proof prover="0"><result status="valid" time="0.015921" steps="54048"/></proof>
+  </goal>
+  <goal name="trans&#39;vc.1" expl="postcondition" proved="true">
+  <proof prover="0"><result status="valid" time="0.013354" steps="39489"/></proof>
+  </goal>
+  <goal name="trans&#39;vc.2" expl="postcondition" proved="true">
+  <proof prover="0"><result status="valid" time="0.170432" steps="1539135"/></proof>
+  </goal>
+  <goal name="trans&#39;vc.3" expl="postcondition" proved="true">
+  <proof prover="0"><result status="valid" time="0.013887" steps="42157"/></proof>
+  </goal>
+  <goal name="trans&#39;vc.4" expl="postcondition" proved="true">
+  <proof prover="0"><result status="valid" time="0.017414" steps="79357"/></proof>
+  </goal>
+  <goal name="trans&#39;vc.5" expl="postcondition" proved="true">
+  <proof prover="0"><result status="valid" time="0.030093" steps="153051"/></proof>
+  </goal>
+  <goal name="trans&#39;vc.6" expl="postcondition" proved="true">
+  <proof prover="0"><result status="valid" time="0.306929" steps="3138168"/></proof>
+  </goal>
+  <goal name="trans&#39;vc.7" expl="postcondition" proved="true">
+  <proof prover="0"><result status="valid" time="0.015670" steps="62268"/></proof>
   </goal>
  </transf>
  </goal>
diff --git a/examples/mutualExclusionToken/selfstab-ring/why3shapes.gz b/examples/mutualExclusionToken/selfstab-ring/why3shapes.gz
index 6249c67..b4b09f1 100644
Binary files a/examples/mutualExclusionToken/selfstab-ring/why3shapes.gz and b/examples/mutualExclusionToken/selfstab-ring/why3shapes.gz differ