From 5fd936498d6652ecb1527a091c10de992196a5a7 Mon Sep 17 00:00:00 2001
From: claudio <belolourenco@gmail.com>
Date: Fri, 8 Mar 2024 15:21:50 +0000
Subject: [PATCH] update proofs

---
 .../LDTDupl/why3session.xml                   |   2 +-
 .../ChangRoberts/why3session.xml              |   2 +-
 .../BakeryAtomic/why3session.xml              | 132 +++++++++---------
 .../BakeryAtomic/why3shapes.gz                | Bin 6683 -> 6679 bytes
 .../Peterson/why3session.xml                  |  34 ++---
 .../Peterson/why3shapes.gz                    | Bin 1855 -> 1856 bytes
 .../paxosNoRefinement/paxos/why3session.xml   |  14 +-
 .../paxosNoRefinement/paxos/why3shapes.gz     | Bin 7296 -> 7531 bytes
 .../fourSlots/why3session.xml                 |   2 +-
 test.sh                                       |   2 +-
 10 files changed, 100 insertions(+), 88 deletions(-)

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 de147887ce040ee0d0fbf422a6d55b3e2e68d076..7dbece5e42c9a6e104bb41522c4865eaa845e6a2 100644
GIT binary patch
delta 6510
zcmV-!8Ik6jG?z4gABzY8000000RP2XS&v+~b$-{c(Ay+70&qKAg4jqwaiauG>>y)Q
z9)e)NHEv|oEsP}3_}}Lvd3m>5)RJ2A!%SC^yoZNp<M*9g`iI}VeD@dsHotrM*ZlLl
z`^SfWeyLyn<{w}9-}(C!J8}QZ<Ig{(@80~M_iy8m4{hjw)eo=z{g3$}{FLhVyBGfc
z;jdUOPV#mAcoNGz#_p=H`0k`mw3k+g{_XK0zsCIZ0EQ-kctoE}m#9}OFxXd|T%WYB
z{k!-1?T>%{&yzj5X^ykk{^#uDUwrr}<J;Yf_utRkpSak5ssClD`L8FgPu%!7{_PL%
ztCA<q@%`?9fQQ@IN$}OD_U**oiCc(p-}eXZ?p~Z;y)2JEzx+9uhZo-SuDSokzirCF
zs?*<}^Sci}y?^oc@!k9Q_>k`3!vmYC*Yo;%L|+9$O#9Op{0UmGzD_Gv%b`&JE6rGo
zk7KIK$A?4zAk94TJ-#ef!W5k(KM8XZgmc3xSU@;`zLc<@Kfs7mP8Pt&Y8c__%%6Y$
zkYOoUr~Ksqx6KL&e)#aFf37k_m2u*PuaNQK0iH{Jb{JSh)=m7z|Jr7Fm63ma-@jBL
zyeV?$e|m@gIOM>j@7}llU(Zfx4i&S9Jg?E|c^_U*JNv$#%n!}SaVF*cqG_F3?Kdmp
zCw<$00fxTk+N|9ryAP{QIFOnhJO;+H;V9W%H_y-G>uu@;w((*WihuO?@BZ-S?fbut
zbMyd(Iac3c+IFHpy!hq*{X>5D?q&Y<9@;*{{Nm~Ru8v2`X$aZ2IbIzY%Z4~wi>nK2
zf?w9Vn)kb&2j6{o`0y^LHdNE$chwKOIgIpwsV-$VJ483ZAKvWcet6TTYGmx@>QJA2
z8+TK0<D|^}ujT&Nm;e1Q|MWk*6>W)s>kslpvrJ3sO;}FT(>7g`#SraKt7DHxciT*b
zr`q^GMy;uZu8)Yb5qUPEZj8`j_s}#T_5;h-bhnQ@f6rUwweg3)?GA9y*LFO!;x;gU
z`nR`d;#-Q|_Q&+-jm@~9jDBkoszY~F*ZcmVF8cj;&HYp|T7~)j^1w>|<<ScP%9jYm
zvbWpaujnY-(u=vmmt?tWszsw&&ZWfSo6Nc@O>BI%^1|6s#p<Znq{$_5#O=Hi+q}A<
z#P*mY)&6+ZH{Jf*f&B@(b?@IFKIWZ&!z}R8k1u=sKGyNaF7uW|wU@}D`r&dkJ+_I*
zDXcD^wX1)#;2bX5{;|q^6#h~AN97;sa5EvN)A>i;+;zBAW*>E1q?=a{m#g%AqVDgD
z=Z02o(G+4g6~hr^TZ~wHG)uS~u3a#XrY$#fh}{$q^Qg97LA;%U?_vO8x-GPS-7$yD
z7h^Z`BTeypxEXu<KylY&&o!~`<I%^@qL1AQKi0j)<^X);b-4NGDb;kf{A!7Q<Wo%W
zs*b#-PF>htjWuV1ahA5zu8$QVJ_5d7HeD6k9n96@xElrSEWDZxX};EOCjKMu?#Fuk
zPy4G;T8-9|39HtDdih2^!+9rvA!gPg#2L1mSceb`+Pi-b)L$)D*Dvft*^^QyB~FT+
zq&`W|4P^oPm9ChvvJa&@`v8ehYLJckMNDL)erA=h*vj%iNbqSP8<>^4&Z;^qD~C}N
z+o)4wunjs?4P^}t{NJB6D6sw>f5zhNtgMU%e})eJ_a`zZlHYIRa~i}iAE-do9wJ&4
z#~j9a+lu(u>JOb)HBu%A^Qq*ja<sa%lB?ALMGM=7woo&K>;V6hB?T!la6Ne5UA6K`
z4bHG114U%)<iPUP$yGkcs>e7}BL?tsRtC#g+Tg)O9am4_>IqI3G?RY?6+Ci>|3e9G
zo5k^W6$q<&P-a`1YGt%@DDdh65ZGNXjN$sB9uPFDJ<H{ChB{x*?)tWDP-E(*1ND-9
zrm~aJ1tNcD)naf%Skaug9qDae&lI#zY`LMEsGz8nU$BK6P6K1v5a-t7>Visf<*wVZ
zkPN~1{AM1JXCrDea)H2#J%JTh2<&08MV((0Td^m$TVl1RQD#r0%$`P>t*%p_NAbA`
zD?X-XpG-wq&CMXBgyNglk89nZTFYANr<TrIcVvHcp+BhJDyn%mHHCWGncfnrZ6jny
zE4U;0O|M+PMYW22RkLibSuI}8wi{%=pPFxds`i3<D%PNq+n^e8*hsW*N{fAWr;i;}
zS61)_X{XWO_P$N~5(i_cYx-#4Sn$=xZRy<z`);Yx5)pE}uug2eBt}HZ)>>Od)HE=b
z4RL?87FQS4uvgc^{*2a(Gg>dsNPHV<#%ng+x5g&V4^R8at#x!VUi-2buXR=H=yk7M
zDg|<13gneiaF|Ws=GP@c?n=Ziy$|~eaM%}#!-YDs^52wFik2)J=x5}V7!6i6dl6x;
zXq{zBt`g1FoWM|pI6Y9QXJw1rCI7_S@vMI-IE8Xg!XC~`4hm6otL5Mv&^--%R8M``
z9@<M|cG*Gfd#Y+1{3GjB3mkPT>&OpXXZe%9eo?MYt(&Uz%CjuoDYACXXs4>4c}pNo
z17q2ot0R!qc@C>x4trWB-L7#eM&ooc27I;8qCU15qkUZ&!z{*VQyXL0wK1lw5@vs`
zWqoEYNvg(_9C;z!dSRW|SWWWTNC+G$)>dl+W7#B5uAR^p+&!($`RWILvmb-`Cp9`Z
z`6=bT;LRiQY(!lj5&J%-*!MBTzK<#BV+ZdVxBlbD+G(RFMTgrxD=2ZxMw>1F9!(lL
zeCsaF<%Y}X&ukhl=k1fxXZbh_=SzPZrT2WMj=_a?%V_pY?UpMH`rt43z;8H>-}IWT
zy_niInff22b#bfDG}=eKTTxT+lKc3&VR7AqtCr9W7oK-`ZZ#z4F3n9x@^$CsMk|bO
z+BrQ{F1}!z-f54Quop&NUwUx+3itkDUcP&aJG|E4LjwaywY-O(i<G+CF9d&H(5r>N
z;OpI|?bSi%*<Qev`-SZmTJI(7B`CYPG3L8s1z!&v!}aaYOg9hD&$Nq1EFie`VOqyR
zZaPH{xT=CF)rm`mQ57sHQ%{LvgzufLR5YXpTWMb=ek~@fHEYuGR=a7bBduz8p)0oP
zSgYN>b#B{Y5!0%<#d1Mmt!jT0iR_8=iPVY2_ZY$sT2zIRe)ukCg=?c}R+#LfFzJoL
zq!xuq%o@%;7ID^NvGQcx$(WO&lfh@~Yb$iLd^VirvmVB+^e|@8!_Y<#BNshPZCPkn
zO`_oz?N)}<fG%f-)212j?t)FN9yVPa!MT&8lanWh<G9}3slIn+Hl=@CeDBu2cPrn!
zt?%v1_tso8<+gFM8ejTzy2I;P?CTjl4h}cqGY!Z_y$TGBC0CEMiMwqD>ZRa3k;ZTn
zvfj5%Y;m8NU>;R&A?<?urh&0+h%;+(bwNYL{wf!h?hKl_Gic_{pqaZ&m}yU#=?Y=~
z{E9QnT$Ase<MzaPj~ajXZ5y#~+lX!3MvS(NTnMEcQ$vrrZ8I~Mi7&1yA#XnEVZ>WF
z)~Z&kVx=9rSGC4N*7VV==;PGFnOR7ukDYS#;9hvgaQh%0b3FS-fv9b)*p37Bv4ifL
zOV{?rpAo$6RZ<(T8%ej`s69I~9BNcqjT@r&vzDc8W@BYFm|=f?4!6aM8jg{%@bzNq
zmBhNDhP%ER?TYr%K99(=5w#iV2D?ET_3+l9inEW-8R6bD>sWKknHvw>SfP!Kg)?<L
zECxU0l*?8VsoW;=zS$!8%@(<Dwn+YoXr^BN7toA4Lo)ybYKvx+{lvXG7d}U6;tZwj
z;M_00e4jDy6S;pm=gFP1>?!BT%_F$n-8$#nd!+iNXuzQ5os#TLr21N^<{j^Em3rFo
z{#vQ!9$x^H6t!YByfpH0YFo9W<P&6SnaP*xB57_)O>L_BzD{nXj2{om>6e3(l-F}Y
zjYh(#Bf4dUo*cYQiavIrejG*ZB=|En?DPAtZOi_7>7{=t8sjTf+M>DA=pH+xESU8|
zvqaHUK1PP=>JwTe*fcPf4RLNQt}cMM@#|N9p~}$NYYjSktwCq6HQGqCXAk0CRpvch
zMtDq-v0#cezyCV9uzp_bDfxBRt`k7cR%ywyHdD`@Y1s^i4zoATV3OX$q)idpw{_&c
ztt0ns9Z6AJT_>7D%X<|Xzp|wnX^mu^)0cXZJ&CG-(;dvrROFhe$Q4tOTc#pcOhryi
zr5m4?Ur_S_{HDZ;@A@yatE!+1yGZC`2h;ba9tkwJ^{KxTleG*p2uA4a%?O>n8I$k~
zK!0m<GGl5e;znxBI=g;Nt?n^eUt;YRsux#{6Trp#j|Qgut3k+~SQCO=l1Q=ot8q1v
z(>Ak^)An^Dr*eYE3&u2Ch&k>c(`u%<fn=L%Gnkz=ZkpVJw7c!r*T-nZn~q_Zx;PDt
zWi#v@b<v!|VY5TS{{6o{zI*?thy3aXfPdM#^8WpQ)kFRGw*H7_%W9uKxBS}*C1=~s
zYYyM_e;2WOXbrTdL44aVoMrgR);DL)wRkmYu`xlt^4H&W|EDGOS4N1Ojr1psug$Rj
zqGoOC;$e<6X0oCrtDzMasZa3ELx!oYOrNXxv5Ad}uV#<^b!;*3aH#+8W^kc4L4T`%
zd2^WgO~*<7!(`T1?a>OR<|TIZ?5hPy)lD{N3aDr;!?o`de8Mx!{^NGu$Q@{CniSi~
zU1Cg&<aQAvD%a-0kL{mNy?7By$SPYViz~bYX`N@#)kiIpEiSz@M}4HDI?AIs@*{fz
zY|5fyN=xOEGNB~xif1VX$~+|hl7G{YtIZ=k$m|U^O2KC%qsUSb3qq(6QncwM=SR+t
z?r1lU31*_PHk4SD5<y39v=@wdR%|rVw#OtM<6`%ubwQR8Sai(UQiNhjx{^50o{7xz
zORbJt9=SR4?cs7tiix0P4vZIw!Ooh2ZCR0o=kcZBN5PI9d)f<+8|8y134als7>CB1
zBG<CWpuEZ1&j;1wvVbDA@MNP%+A~QU4^weAk`pl$sb>LF9;G-+ew6Ge+)>!0Fh`+}
zf{sFcd)eHoBD`hV7#_VOxR<2SaIfO2<WOZx`+2gN&eeR@c;SeY3?<u`a*P3y#}aR{
z)l*~(h!lJAFb6_cX_G=S0aSkTMmifj7dBesL=#V+EnfNP6z8@^k8(LDS5!uj6(*x$
z&NcD+^Th{cm4V!nnWijMfx&I^B6A(H%T2ubZ1FJ>PaNey#VkE9PI@Xr%51U^BDj<M
z4=I20;JFfx7cR@pnKe2Ujgz_(4TY$mq6P7)1+k-YM+Ftk=c}Vs44ND1y+uxC<|rCP
znzX?;l5rjE-#{IcL{5@qBA7>JYk9Cf#1M2LlbK!T$Fr+*F=~ntT-(SgI~I&*sKOM4
zObR*6(iHRbEj2Q@v5c0ugm^Nr62VB!YXN^R7Ll`9XW_Te$O-8Y%!RB9-Y6xdGo*Q8
zF=^{1UnlOj(J0i5GNFhIRs;iN5GGn;N~DassQI-l!_K>0heqV8c4R+4tc&MT8uCHI
zAlfStjWbRQfqE)ouxnZNwbUuj<)pO)AYlqP3H6(kL5g{g0zlWY>{-;g=r3KEX0m@?
zgxMruI37dfFqhT|$c)UjEc<#IStl(wz)jZR_K_(?FDMzwG)$BvyOw2NPou;mC1e?{
zu%vPz=6E6%IYKJ>7{#?L`+6D$L&cJ{R&js;u90Af@T8%r@shDMsJ(^~wPjY=4AA8Y
zAQ1tLXGbncU&T7Lmhm}2F-ieQ!L5I@8jL^`pgEq6<x09hq3pzey?fsUP!N_Z%YbJL
zAlxaNMMZrU*Gcp*4IPa-8gb!S#2)FG+C60P6iLk~dKHLp7o@mAadTOKjL34QO-Uu{
zEP#PT_9@~9Q4Cqu(#yyj0#X*a)^&J`Vu`qatSvdCb^)1b+XQIa1!#TLbmf2QQdBft
zV!1#Klu0P#8^9~jj9e?r+I>_^OsS|40iuFTOw^)LfDR1jU~f4!YGT+&#Q@S<>op^j
z7&)C{7Pv<_u(MW)=LW?L|EQQCxk`ww4D{x5aVnaWGQm=yS;mA-7F@BfDOr1Nl<?Zb
zBpBy_)zO7ORwsx0XYJ9NqoseNy%Hl5mB0uilmjLJ>%-ZiBMYk<#-s{!j2L%IjDv$n
zyI>Lt4Pa`K;>eX`Z4%&q%|ljyRE&_I2?$Y>D-ggXhg(<%W8kUaandGc(#F`Mfm!q|
z8#{rE%7S*1vdJ)!jPXFrD2595QjHo|{&ab84T0l100gBK7=J++F;0I%W#hT+`iZB@
z1J%Oa0DOqxLH%-8x(vBiQ!p~-mZ4TYU7m7*f#Nz9xXoVh90jhzkexv4z%T2Vy6p*M
zO0iWbt}-fyX1L=knaw;2W141I2yu=b?M+FsvQ*MON6K1f5ZBDOMa0PvO3=Rc6P&08
z&^<vKDU}eOg_uSqWL|$+AP|-vSV$n$gE?L~(@zp8G7d%1DoD~$2w90hfgL$7N{S8S
zbGRn;<y+(_TNUSpAeLhRVnIEFQBvVG=4;PMPpuL0EPLtVP@x!+iKtN3^xQI({}PPO
zzGsrNPudFj2_NK>0?;O0<SrsRL?p?X2`KYLW}s-$uuhhpd-i{A6(b*QCh+tUViAZj
z6dhFh7>mP=*Dd=rFMis-*vfHWmg17-PG>6#2rwy2LF$fV7=QMCouq<N8xZ>Nr;u8c
z6a>_nbr>y=5wx5U{!{ynIg@qs8GSq@s9d%VXUy0~FyO3^3Sfz%T6B_?W)r~AxG$0<
zXjy7oF&eD_8zX<12OvShdEtO{Fn_|fpJH)BNP)vE6%+|4z&do{Kpz6-+W8XKf&G<K
zK-qMl6&BYlZVgj3;2%Q>Xa;K-ikl$+T4o?&K|e*Q*Mj3LA`Vo=l#B}@Y}o|-SJFX8
zxEwXVwx2ZoVl|MlVTurl5vZr@U|L?)i|(m60mvhuAV+_F<XQwEMcm5{gal>9f~T0}
z@?`c?<dVY$3XDJwE_0z6n^2<+aZ{vpitXiodGVLUN(SiwJVb@@<ctm4NnFBY)b!S1
zx+R}!OWZRtdZ~dMP@8~YD=N~7d0%gv!8P2cZ23uX`S;!4`D)`_32kxp)&U%Ltv_5M
z@PxnM;%9#>j|yzc>YR$S*(pN+xkdPjDH$-Tl9$~5jN5zMfvEympQQ5KC-TMD+t3G|
zWJ#B7|CLIEVW2%ggC^8IKtx^803$*15(<g>4yF=*Jj%sWpkV=2^;t8J1@e}>0(oF8
zWk6tDfMUU#c<@OQQ7DOl9)Z)Nc3Ueetp(Al&EkK8m~9e;_!N->T!e!?rYN0}CK(FF
z8r;-i=!VIzBsW83eKW~ngBp#WVp+yP!hn&DQQnZ0f`PII@YR?Bx~4a0+<xgc9#l3d
zqZRy!`kDf(Epr_Um<<ls=_q$!x{Wc;fVU|b3zN*o5|Xos6c4(nobIO)>`S)^1i}cc
zWZ-`s=4>v>I!{{j$V_deuIbp59nK_fTS3~m!ZKo8fU_hdJk(AY!}V8lM<UZCRF+SS
zb*0F~Vp&SCMpo95k@bZINCU#&EWIKwK2b8jF+eeo8YyH#AV3$8ATU7SCsESWsiV&k
z9TjpYNAH=z?S|Y6UZUvXCSa=eFS;Au5RHEt!)uWd^!YB;R)EbU&>3Ao*x^^t7+?r@
zPGl8&t(ELKx0FU%$t9u(hSOP<7&0(~tiX?gns5n!)-7A7-xEp_*o+{9YJ$QQqVrlB
zJKbmEIkyZXVgilwRw(IN&H=C*<*cCox{~}RS3WgR$ao=xmAH`v0wpqOikD#d*5rTU
zd*6n)Civ$_hheN?6#^u1PKKJ|bj4mw*B3W5sjgSjpTl4%@%1gYhiw>42k`0uei@2E
zVnH($7s5iq)(RV|Pdt-@h+q<kH3NY3St{Us+#^A{Ok|g~2#V<E?H~itb%>Bv+sv%M
zbWTQ>g(Z$s*~6N?XbTp#hb(dyb<BStYrxqcq{vDrlkZz7HE)5ZR2^Z@;~~KVP*`o{
z5i^vr6Gc^YW(9TI+g|w;eXZ?1DHL2IBd*bygyZ#xD2bt<8}3q^POrb->5*iH7$}ZU
zTzVmrlt5G#Q6(koR8g6)wLQuPBgHK)2Z!Ks^;c6wq;Yr3LfUQW$!Eu~1*LyO^-s>{
zWSP}oS|yS5&gx+5`wghaH6+&eSo$+_kul+|tUiP%wZ*NOb0(Z42&Mew$d)LizicP(
zC9+&b6L_{7l*$T?>oxhDwM@D1q~&vL6@m=4;SIQvlGH#04B*-o6dfMYR5Zzqtq67`
zh^Ma+sac~&h>CD6F{*E0SO9<UXSu$<ovt3T-$E73fZmcS5*!8si!HojvZB3%rDMmx
z<i3R}oMNRtEDGQq53f*25-6Fw+GpoeEU<5(N&sC-lrx7SGF9{lsOo_AjHs_B<R+KD
zG%%g6uSlh*$P>riS4vcfO|S(D6dbsLhExryx<31by9w`vG`LZLt$=@JQ&yy0G?IZ#
zsmO6O1IdOx&u+oTVi-80&q`+#z147t<|;9R-N7A9{Yj{Jrrik1<8TMnABHg?yG$nH
z4ou8)21jBy1cXt~vztd{3_(X%jPT@SQAVI#>S&SJI)K60`m!I=EFQ4f#lorvJDK|8
U9rBER9!>rqhj;-rnPCC|06Q?@#sB~S

delta 6513
zcmV-%8II<cG@CSkABzY8000000RP2XX^&jFb^Weip>Iwc1mJeL1hJ8V;zkLW*g?jq
zd<cR8*SL|HZeb*O#{WKt<m20FQMc4m3~RcI<h#7Q8_&6~`|p1H`u$)0yZrw3U-QrJ
z?;juj>9v0S+rNM1f9LN{?8N;qk3avIe)H4+djBr|@X&^T-hBVo-~W&w!jGwbzkB8H
zAO4Ev;w0bJk0-IrW9+U9i|<eBM0;s<=wBZn@>|SL4`65#h)49vbcuSk0)u_U$@NM5
z*1!Ld-~I6C|2Wx`o8~xs>wnHZ{>6tMGrrxu`taSn{fUe1m-;V5&3`#@ed5Od<llY&
zp(=Ue9N+JM4tThYodjQfYTr)Wow$Vv_g#PB?(Ws;&Fk{`^Xs2;d3fbL@0$Bx{JW+c
ztUCStIluq-<A+!89^Ze6j}Pho13a*qdONSLNAy)7#IzrM!JnY@>g%*(wHyldpVExA
z_&BDze0(_c57Nvd-{H$*B}~yt@{=$pK{z+8f(3+s<4Xza`2&n7<zxYTtcDS;&iwi3
zj~SMNb;^(af7+~o;D?Vt_0Ls?s4`BR@D(yXKEQLS&kh5N$hwJt^1rqjUS;H8KlCqE
z2ycqq`5)h7KMpxC>H80D|F^RfnnT6xA<t`cdftbZ)6TxHC-Xz|ahyqczi3)#R{PD0
z_(|V?c7UPpxi)Ke$?n6d6Aq+i2akcVY&c4G*Uj_u_<EZ<fo;54h2kIm{rf-s^zOso
z#yNU`!W^sbFl{^0A71@(|KTCOfB!oFdJk<MVt)1XeOJe$<urtB+Z?YBjAcU{t;N*^
zHNh|IUCsNOo(I4A`0(+4PHm{B!|$pec5@hi=~G?GZgz-nf<OMWm;3RjK2;-QH&=)H
z<h!_=dKV{U?td-!zrOyjfBwh+-mPd${5yY;ubO3AQg6a?nx3}lnk<HBhguzbJi6Ov
zDm>N3|2}F>Ep&ZEoQ=q{5p`pP4!eh@0kI!gwx+v%<oSEvBCm}<{B3uDd%m{gnH9Hx
zfziLcI}_hh^tL~yM{jJ#{bcl8i%=c9qq^Sr4|UP+w`=aFlF=&6@0SNw@-L5G2vEL6
zD3-n3?tVo_*_K|+6}}|PRZ}e*&2la!7T;vnRcT`5tCbhdjw)71y(UdAi6d_3mDuLh
z1tqq}9I5ultG?;>-wy0g(5-v_Dc>A_W^s>xeA!#~v5r4Z`(2f%_VPH?K3tBZ$2Rde
zh1BJ9-hZmp94=Y?u}Xau{!#iz<sa#AGZm+k`A6Lxb+}YuA9Y)#n?Dbi>+^h`?&*uC
zhE{FS6kInI!x3a#j3|3FOQ0OCT`iBMEjM#;-4qY=sJ31~yq&`CqVqA`7TWHAmc!*M
zv77mkrpP_qh`N1{xa(2pno#$txZ`JW$8H54>z-nB=sof}+<fzt8oFA3wJ<;ODIR!L
zM_yB>F6?f`nzNudOV?@F$BGLd0opDbt_tnW<!W)-jWTu?TFr(uUuHLSQgvb9i|Rw#
zUyaaew4O*<wGPrt_i!7(0P#+LLd=9ih%;C>5e^|1pm+ZPfWMlpu3w0UvL~fZN}Los
zNqv%F8p;CiD_!AYB_2w5;sO4k)ZiKQi<o#u{md#?v6bL~i{R73GcYT4omF*KR{EkQ
zqEV;BAR2V28p?WN{MVl}*suN$KgQzitgK`PKZXwe_a`zZlHYBEbQ;7j52!%Y9wJ&4
z#~j9a+lu(u>JOb#H9jT>>8ZS`(zCj>@~YJVMT^~qu~0LF?AZR3B?T!lAU!DFUA6K`
z4bHG113P5w<UsJ%$yF-Is>e7}BL?tsRtC#g+Tg)O9am4_>IqI343mEa6+DWE|3V3F
zo5k^S6$q<&uw`3GY9+ICDDdh6aMxWhjN$sB9uN$wJ<H{ChB{x*?)tWDuwv?_1M8A~
zrV^9T1tNbY)MC&=Skaug9qDb}&g`>KY-ypJSfHqEU$BK1P6K1v5a-t7>VnE{<*w1P
z@C(8B)Mg%$XCrDea)G;wJ$DsXxa(oDMV()BTCwM}TTZoSP-f4d%$`A+t*%pxNAbA`
zD?X-XpG-wq&3z!GgyNg7k86#eTFYA3r<TrIcVvHcp+BhJC8~Kh^@DoancfYm9V28%
zE4U;0O|M-4fNB-_s%F_<vs%2GZ6nBhH}&26RBZ$GRIEWIw?Q@Hu<>W#lotEOP9Hm{
zuB_k<(N3fP&|5a`OB`gSuIZzFW5HJ&x21O@?7O8#H$=$w!aA|>k{A&sTUTurQPaR!
zHpG9?T3lUF!(Lqv`!hx_&KSKo<L_;x8L!!N-xZrYKRoRxx7N|gc<sw#yw*^yqu0H5
zsT9b4DUer6!C^Lin_rg*xhoO7^giq>z+qn`4j1ak%70TzDO$2@pr4UbV)Rzk>_vpV
zqIH%jxk@xwa{@yZ;`BhJo|P?fm;4iRv$KDu;1tR|341s%IVeQUt(JpxK=(B4Q9ZR}
zduT5`*<}Z@Z>Oql@Q<uhEpXJWtRp{ko#jvZ`bD`qweF|RE6=iUr^wnlqm!z7<}HCV
z4UA=Tu8u%b=Q*r)IqYejbi1CZ7(LU;81U6Ti~87NjP`Y946_)cO>K-}*T$H#N|=AO
zmi3vrB&ixxa^!_@>xFe<V>QWVBO!34SX-?PjAfHJxpqQZaQCzh=bP{O%~lNNpVZ^r
z<foMTf;W%Ivk`TDMC@CbV&B3P`xd64PaV8#+**&H>ZFZ!6di82tDwX!8*R4y_B|Rp
zeCsC7<$lX(&uscF=iQUhX8AM`=SzPVrMG;hron}7%joq?-IiM<`a<*js>}FIpV``q
zseO~F0Wx|Qx0+0&chuVzHT^C*kFPrx*ZsHZ2;Fetd5h;(M`CW%+;k&fw_a}a!T6@1
z)6?YQd!^}B_IUStVdU+l2e)r-?;qynyO+1aYyI^z?tiJ4*Uxi-Qg{1>zzTnQweS~w
zy?fqX9blgA1x&eL*lwWpUcz32v8&r+z9&}D^{_Eq-~P;W^YHvkyJW-yfLjlybt~ki
zOXPs5Dv(m0v{VRHfs!)ylqf~`-kC~8LTWIT_GRMMV!~OoCLL?FTb4S?s&*H;;;N3b
z+Ra<%w(S)$t(w~_7Zld2HjsbFo=Bfaok)C#A?%<<RT$}q?_yTCHkoFH$u0_$-Y86J
zQJBQ6;oM&lXZ;l`PsW{$IT<<`e8#@E!bZzy!&yG-Vcbd&V-`IOZS*j5(Zkesg?7~>
z8g9{UWjGDka%MPfn&Iv)*wpG_)7252J2^Tzd2%?8>y4f2duL`-y2XF@ZtZ)w^1a*o
z-mZLa%_UQAn<lIAr8lQLw4TMjosr|<Zv#5hfNRvNz`$2>^+=nz+g6}n3eFR03^yU`
zecQwq^O*_aQRNlVE|_l`7|Vt@vldquG(_yL@=)o{V3|9EW$p}?xyxjk_GFo^kmb*>
zIJ3+(@!mOZPn!3Lao>Nk5&M>n*tTrMXxYexOv*7e^q5;VGi#Z+;;Itz=93;qyoF<}
zYPBj>%AtEzYaC=v9nFe5PVJkSfpqHF=|&Ikg>wwI57IHmvv2f=+Qy3Q_)i}@=)Sph
zZD0Ht!Q0*>weh-<bnA`UvopJ)Mw8XJA!;vcS=wecR#t-**5`k4TdZi|7#R!SE~Z{d
ztSf4`>#NbOXdmtKh&&rnn~`p?8-!60Zw;C_`{<kv?me@PHMg9(alnlg+Q?Wq)5gPM
z@H0NSY&8+eZ6fa*Epp#zk^4rA<j+Ji_42=fX4Dy)0U%IYG^6Y@_v$?O9Hogfl(vI&
zzx48b#<ox7=A3^gcgC=%oF_Mr;Bt5CoNw=t>RX}#gO>M6vNw?GE2WxuyuVTEX~+93
zrIveq0ZdZViqY`W$j7N=)sm7=kf~)RU#g3wxgj;RsOq~qxs@`0XHZVRFgQthJ15j=
zB8)nsTUO}F!P}(hV+ZQTQPfU?A7jHlzyI2{?4OrDilTopzEY(vnk$X&u`|koSuZq8
z6iwx0WSFi#p;dxS17q0`=hout0*D*G^vW+(89IBVL1(Wt=<Jn78)^3JLA<NVyobvO
zk0~-1Ows1|UndvV&x<`JzwX*~0?64aEm_uP>e(|bo8i!5_Qn}Z(tDV+DMI^}j@-9&
z<i4dNX{%7{M003)r$XbGYiUMWBU$J4rJiI@qAK8Y2QxDjxn?SI#Z=^$smK*mkrPwt
z#;4^Mr}+SWQ)0#U{TH*Vs-OzHNa$k+)Ayzx2{gC#slN}CwhS`}Md<9U2%WtZlkp5d
ze@o_M#?(;6jntTRcKw=K-D9-A#M&)XFRmIVfQ$8S1*ZF}LCBt16M|flNU{3M;%XwN
zZDt{-?dwEN<phlvjA^zIbKF6u)l72($u`wyFgtDBG`R(7ciXM6kI{xV9m6hlaT*xQ
zX4pIGqB)1dW`~CThktu~|KU#$`OWtLf3tPv{fGaohx*}N{RNsWt9|<1@+TEa&bFJ^
z9DdXP9Afp*8fZ_0__kp<%kY)0Z_b=+@n+IuV}g3+ufOa57bW#Kj1V~+=}#D6n_>M$
z&Dzw(!yISKWJO6<Ln|&)pWvN`3{zd1K3DNm6B`xZ%pUve*kaz{Q2*R!aG^Fqf2%*Z
zIn4Z~<D~v!GV7c6Xa!UA61#f#&4Q%rCL1&bRJ4}i+V=@Q;hAOsaXWA14m31PitXes
zF{VXwy9g1LYxCfT_E%G{UJ<h~kcnJcl}I}01!bwVRF+w*<ZE-(M>?vbJc=VfvR9NX
zQAj#@#$Af|5qVA`SyT$cgL}>Cf5_G5k(`u?PR9U=F=Z2EQa1CVw8<_yJi?Eh9o^Ax
z9!sVa7Oj)Saw#ISBt7%NcpFuYNw>!&9^+#Fq)?7SEi&9|FM}1Tn5Z}@VX=FDt<_P>
zBR5CBJ)B}fTik$=E15&`u?UkW^I${KM#a~H9|b#d>}fAN9w~TfZ8nK<f1!vosf4pQ
zt_;pNA?AZ>aalkPD!6)JaxO>4C6f+T&N=&RoKLd=DUVVdB|l1b6z(YOQJAC9M?puS
zzP)T=NRXBAl@HQpp%uYkfpm!h7H3tqw4W!tNQ%)ZX^4}A(yTb1rQyXRV1@0n)l*~(
zh!lJA2ze<GmQJgzVj>SuQJEa07UTktxrwLG7N3jLCFx9Fc?2-ih(_{Ja3w@E!Zh*v
zv&CDJoJm0kSjAb9n9|OL!VF1dn`%y#=Cj3z$Wn?mdx~Q)x31ZcYx=@!(T0)`DSs-+
zNhxG7uAt@w!)?(b35US-(2PGt3*uD^Vn^kU3M!b-S0{KTY#>xJWeq8Xx<KA=m5PG{
zY+MKXw@@cWhS<%4vR28($fM!Xm7o<1X$k@LmDITyHN=eZk%wYb3Z_WLJ$IUUp(H8h
z)H<cUjYh$0&!yzNWCqF?qtwMl(tped4Zh~qS@>-<(xD_p9v2)7I;Nrm^Hi)svPB!c
zSSRkc(I{qEhI3US%hrY<Or#ufPg5>Z=W;E}u=6h0p%J;N9of$hYtN8lz!)A7GCNnS
z^gbw8j3ZJmvuj!QmDEA?R)qkLBJOnL8+Qbo;Es?UDJRRdEPD}kF8a&6%zqVWCz&H-
zlp~-N8y&fbN)1?cEz7>1Mu0iKUlo><(YTBdIxJFgQ36$7&9bkjk?=5#iX|I{3@cf4
z06HSLuO#5Ra4pNeo<<7s12q(|ST2UK;;jJG09X~qWm0QUdkrO;#2Mg3kulrCwF!X&
z00mC!7=Vme%lHhy6|=F{N`J?UbxbF#JfNe;mQwKKwkm$rdtYis3Fui6F8ja(DIdX1
zj7FW3na9_Ljz%4gxbUpD#6e+d(PuGB1~6n<(Oh#8iHij@XmeSBA&0vm329VLNdgE-
z#f;~cYZaty!EEFW0bWG!Wicr4DE6jg#9a;?R3LbtoUH=1?E<tuYJa*MFyK^Fl+i{4
zy4xJ2j+G9D3`~@A2awu*QcN-_+X_HMGFC;TL$N%FQn*MQ7hyXN`=l7_fc|23L21n_
z%fbT%fl*nXbwq|WG5nKafK83g%sX&0U$n%h3h6}@1q{z_v*3z-9YxD6CHTi#4y6Du
zypctE+^k8l*VZ1bIe%I@+AA?)4U(sF%s|Maq)<+o$4QvBoJ(Wp7%}dqm?(frJ<D0i
zRN!gKA|y#7dk9KRjMbkMqe(<ve86R=4QOvl4xj*q!NKT$5;JLI?9sq1`j(AzU^q>J
zMp_`?K@7+$hvc!~Hd?gWXZh3RG0=Mt#7#*<4g>E8jzTah+<(XlWv$5*PnYM51H$k~
zNnGqH1kS-PbbzuFI8nDyvhwNjEE!=FfL%$Eb4E%7gC;|U8SOx|)-iS46OOq+0#}BN
z+%mxHoV77VIs<r?Lv1`@A;dX$v^OOQmNobuV6cEd%|q0{<`N8CDUm{|{RAg!0d!B0
z#vN)Ou6d~tWq%O}gdCN`JZPk|TCh1@Inz%PXh7AIiU3#OcDZneq8XKeTT@hw+co5K
zxF+@GTjWVwfvBR+z_pTWR8(R#%vytb6j0NsZzW!2FPjbcHp)mKN=R`gVlv3_giF^V
zitAp^K4~l9Cw!1k3c%Wsh`2Ng3(|R)EH5g1r741$<A0`a+qxIu7NFFH1Z-Sj+S-(}
z3jE(&#XOv;r|#O*y!f1b4FiGE$Y521w*lPO7moq0LCSe&d7SYV-xsBtSg8#a2cpDT
z5KP4wJ+3ojx$^6vMH#?9wcnUCSvQ~2$5Vnz0`<eQLNnAY5J{e;^r1w>p-j|#6TmOH
zuOgtX%zwZ$jA6BL!~=Ha7T7Eb?ZY~lpRw(8EY66S^bGhT8Y{^p2`mI#1ARoWd$A7e
zucQK3!7>q$!pdYrF&2SfL#2<(2}JiM$iI>fkt57&Po-oaWE8H%qzk!LwVY_`M~{I2
zN;;5CN)~H^lDJejM|}~V*S5CLB{S1?FfFg@MSu6yn*eZ9fldg(<t&)R^->bT+i4BH
z1ZcNhp3FW+F79-PYhFudW#tl)BnSKe6;q``>%H7BFa81fNW~CHLJ(4*EF`8~2$~z?
z9PbvIZpjzgQWc+=5H4$!K@Cdod10cq!|{)asY~jfv*mMQ;{SPjFfx!a2Q3Ph$$1nd
zfPb#cIp|UZHooBE7c7sS2MdITn5tJEunX4#$49PaF9DG*x%&mT*9=(N;L39fP&50I
zr3aa36(<Vs-6h+9t@4zN7ZO)t@)_7FM%+~yLrfGHq;?c5;m4y~JjJeHzPRpypc9a5
zD+y#nP8OWjvXB?7i3gt~5uRZZ^qB!L0Dr0=AyILP%T_Z*1D^}=ERl*wZ-CEzlqk-)
znKZ5{D<dun>86Uz%@A4NOmf(uM&q+0TuBZ#K-tx-Vip9&F#_x+B{*<a-^PCFHaTZt
zZe2U(Fq4wlNaR>-0{39R8+{x1rQ291h4iVCZc)QEXmB}2sQiwZY$rdkFWn{qDSznt
zqDFWr3QhyA?{hFfj0P&$H644h!yzbELS{S&sE-b!RUvHxx3HZD_N%!gk!cbt%O}RV
zs=?j3o<tFm5v+s&wOlCRD=Mlb*2Oa=XBlAVOduX9fFnEa!M>4EIx1;Z2aT;s`)ttw
z{53w9mquu%I4VEFB-&y{1`6qwM}N2>8a0O3A|vSYU0PTItB$;YR%r(wSN~E>8sxGP
znpl5>EZK{0sf<L5Yg}bf0P}#MVt*O3(l!;<UrI>+l3NCYa%WU53MJjMYyuP5A|gq&
zN@9X6;zhSaCK{=&&qNR!T&S;tG>12%<7)Gp4$lr0B@+R-3K@zG8azz^5`PI>V-Qt$
zf(NY${yEYKFxa7@tDKNAF|eSEE}*+y;eT<8aJ`cL5(Wd(HMt<@03%T`Q}7X$v1AJ#
zjGGuWjIfZfwZg{gnP<|%ri^nbX}EQPDO44kjY%<+A+`Lz3X1gS?LavYLoHM>BoTdN
zJm6v}5?i>$e0Ml~*%p+d&VPXQ7UV$j8qk>n<t&_WVS071)Vu|rQgwvAjE9(YrjiFn
zk>Mu8Kj08SmaLJ)`&((Q=xc3n5~zzRL4c-$x&~_n@QjW!<K8R1-HpWhTH6EqC6B9#
zixPku66Yn6_K{qH8*;y6mHBGhtK@Z(C77&G%!+m_$oh*~6(Og*X@9SOc7XY$bU?wf
z1y`JmMmj29IpjYosL_BcP>*X!tnab(XXc`UBV~@P{^k<UbxKL|q>V5V^~RS~E|UJT
zoe&zyAqiRFxxTJUA;j!0z@_23Og_`{CARV<q--l^C{8szKtMK58}i)9{_2*K8CwzT
zNDxn7Ayi_iFO;HUE`Pv*_$GlLqE{>etYz1`X=J~JDvn_JfQ+d(J0MK07%&rjUqbMu
zBSv!HLKT~XGqx}-EeFa3a0R{;Ixz|sDcqX~ntc<iIES*OQuF}~F=`oLpL)$fE8)ZD
zwZ<0*rbfN+EETCTtS@AWr2t)P23CzK0=T6iRYR(-&wk-<Hh<zea4;@a6dP?!^^I)-
ziUlPBPk7A@BpdcJyQ%s+3CMBl!4MtrmIJE;5lOzn<%Fa&^;bg0%j_lsBj6DsaScV%
zDL6+I9nvet%xeT01cXs9vzx^Kf>1D8^iCjPv`|#qi+h3p!*8~}?1waq2P}56u&TjM
XroMQGJfmMmlM4R>LhlqtkYNA-P}#H9

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 47f7bdda49d27900d5949a24e47004ca2d9c82a8..dfe3f7ad83023bf42b9c953431d1aba3f360c099 100644
GIT binary patch
literal 1856
zcmV-G2fz3qiwFP!00000|D9LcZX?MJeb-m$ZL<4Rta}9*Ac6v;4S08f%%T^_%b>0q
zV?CBF$ves4hjr_VERQ!C7}H%W@{l}av08umaeMk=pW<ozM?9YH508J{%I%LoZ0yI8
zjPQ&PYJWYx#M}LTdbj_K$3t1&*oRZJzdXhfig3S>PD;h3>g4~)&CO=qZ`0wpjn9*x
z_?(|NoAaIhb~rwS4_|*D+3FqtqWx(9HmXtEulDKF+1e*R(ox^+(5gsApo_P%8i9-k
zU&&q3o}C|KdfeF4IX>C^ih-5~@L$kNdu=<n_WtpYk?zU^cv~VUUqlEP$;fA?%<kyy
z_iofEmMG11+>P?irU(14yn!I+mt%2b;d6X+4*|1cQ=k@*CEUuw$z97mJFyL^VZQ;k
z$h4-F5&0;3wr$xoYKpvM+;*C1fs4Wwu57f)nZYKK)mSzL`x5DqO9px7O;=tspUUo7
zB@~mDmCTZ>EOZ{uU*d687!hp|$x+R;(Lx)|!ZmHO05_z!P!@UVMo=!WnfWTqrco2p
zjjyuPL<?LLBCch1X}{U0%{`(W>VY}$@I5|%IL6b<!}-I@<I5=qd&trQ*aLkos=2~N
zbl;9yDS3RZI(a9T{}KcmO5U^I$|7fdsaEU{v~Jp`OkXAmBkhvxtpxoT|9!UmPyG$)
z?9pus2jA+WI@mlNPG^634EJZ8FvY%v{hhq0JTdI&uHS|E`6~aG<+b!H&^yU@j^0Ur
z&Ul&OZBKgY8ni2qx<7SIT{ex)cbr^}vFdEDr&;ssn=>TRcS+V-Ve)xdh3}hfe*V+I
zty{9i^@Q`rj8vAro91%}q|IYJ4H&BXRy}S&>WHDbukY}EF=MD4DIIAR<LDVFjvN>P
zF9^!Zlqm+ZjhV6_Z9Jn3Y+TeWZJ(dH=||8d&YQZaTTkPx!eQ`nWH@`t^Q^WjuNSOU
zExh39<mxU9+GqmEMzXreS6$bc_HSo}I#SChZ5Py(NuHy#MIS?X<O0l7la;1qRlJ^?
zMRcFj$IM%?b5T0zu2**{tVwohXY!T%WtnLkuq@vJz~+hD1YNC_n6|0gcDr=xBg@f;
zKP^V@(qq5q=ewWszSZz}YpiKqTV`%7^r18PrG2n%Mi6$#YXfES@~46B<>0kWl@5gL
zk(I)UsT%&2tKm;od{GTvJ#@sk!IqiU3%Nkb5!A$O7j(6jWxcVd-P`H@o_%Eb+DAK+
zj7)4Y(zhByy(v-N*R|niHg!Ilw4L63YVo}N{qPv;xy|Y8T7W{lsRwF#boKJ+=3AKe
zfU!zu?ss1LomcS%!@7IzZLKF)Zv!tsDM@SGoXSXH?&K!uYVC`Xv`%ijUApj5<TvH!
z!SBJ+>-Xp1a?qcjaDBI$EdRsalsKZ&iJVDk_o03*FRWVVbP)os+9A1+zTx`2JFkP-
zPeJ6|>p8?1{4mXo<4f*`72cnauM%Ia<`3|!-WgaFxBXzCY#thu=yu{E8$h{pSR?29
z=IaRG+gQc7CWm!$nvdP*U;ojKX8w-R`Y+Z!#2qf{2A-}KU88khERibN71Y9TkIUBa
z*~R)!re+DD%evmpXfpfm6JiC+NDH*>!g?2vK>3uwL&|9WRf(6<ZWffEp8HR08|<j~
z_38Yd&*k?neutlb!mm=a#rrJ1JUmoKY;A;mZK&2nF(*{AR9T2L2yTs{UU})fR$Caz
z27r4bofKAB=^!YnfxBS5wn-6yEg#rGH;FKdLl&rTDoGx-5QK8aQD1sUVJioLYLZ(K
znM)>6l^6vDG(-uW0gWPZw*@koK@SRbF<K!(IaFs+IfYo3Bm*HO4kD5*L)UBoIsh~i
zkN-Fm&Jm1IBrl@0)-fSGcZo8D*8`{l<N#s-KET>s8BV>hBoLbb7!6V;8N6~j_y|#F
zb4s&0h3g2>3ulS<#3dzsa4}(e%y@w47)fgcN(L~mVi1<AXryAn8?H!7h9dD=IAFke
zTqBr)(JNtupkjhRb(Ay^p_FqLFb^IffD~{ELUD<9xWppyfwD_L&7-r4A*u`tNdlH+
z6xbS`5g<mtiV6lsE<wD-MoYqglTit-j3YJ(PdITRS&0QjLp?A#FtIWuUV=3uNUljt
zlqM~7NFK2`el+nkmzAk2=2kmxg_a3BCt&9h2ih_0PQ-yE%_{h-2nIuyCTgrmu!aR~
zjQ5VoU~n=fmbRP?oDLiYPOg}96PS;jXl<=<0s{e}baFH#0gj@%8n_&|7&w0uBw!H%
z4;J>Z36Vv?cp~1(V3oo!<d&O(>vuqyV3KiSBsDdL2$IUEO`_H~%C-UqLEZtuYDFq&
z;1XRE7M&nOb1X=(+~QE#3N{G(4u}fW5)r-5lY?k4wJ?l222KGoq_&a{5(Y^IVFsZG
up$367L=1wz7oH7D15PL^g<{4TVy*N{JB}*_x*)Uv6a2s8=g8$(6aWAsaF&h$

literal 1855
zcmV-F2f+9riwFP!00000|D9LcZX>x7eb-m$ZL<5s;++8oh@ilr0q-u5S@Z&V8IVmf
zW30!rC3z?L`xI||k>&9wfZ=Y|<y6&SvDo^{kK5B1_Y_atKjQIpe|Y@sR&Ia%VdFjy
zWPoRUQ1|QcCEo7$)4Tg;JRZvG#yy;(`{gkXP=x!1bTTR~)h7QZH#eJMzfFhZHa<^r
z;&Xo9Y|eM?+u`^SK79RsV5@ihi|(WQ+n@&RzPhJRXXl>Afe!j+hh9Z80A0M5)c|BL
z_)6}I^&I>d)8odS&hg3RS4^}#fd7I~+H2F?y8FjJ2D&Q`;BASZe32nwCIg>?GPk31
z+`B=eSfVu3aW}|2mmb`|vI0TQFUJzb!RPqs9|BgzrbHbeOQ_1iDO{^P2XPIlVZQ;k
zsI-=q5&0l`wQbofYKgp5+%!$Jz(wH-S2o(@%wQAA>MR?BeTnqQC4)TkrYo<RPvv&3
z5{kvjN@l557CH~-FY!1i%!sy(<e+BSXrYZ};hHvCfE&_VD2uvuBPegMnfWTqW>E{$
zjjy6<q6IDr5!bQ0bl=?5<{r@w?ZAA*L-64kPcIMW4=;}|rx@H}m-XNd^tl-3{Vk&V
z=2JF2K3AKp$(w%(0u3eW+_$pGHD8(){{yW`_ms)Y6k(oSlB1QBALGBzZvUyjA(=h9
zO<~|$ebfM(r^D$y9v;K}8Rtv!FKNG7^;9J${oJj)Fh5^a-)g*8d<A-^^v=*brO)*)
z>$~kGPaT7P<x%xh$JAxB*nB6*)f}tM=6ad6zOI}hk-kf^)&^6|%U$@s+vev#4cvMq
zdt5I#D`up!?7cLfK_G1w>uI=9-BtCd0jcAK>b}0i_r-jna-ejeS&U<6pg3+|0K6P1
zFB7IX&^BVqg0#_$A+T-HwlsZy=9V8omppH(Qr9ZZIHzzBd>k0gUGhAe?aJ!~Yt;%b
zH#&v7%YrtR0J4*;Ve&QCZ6^KgY*5E(8KdoTnkvaNboS^YD34o!d1A8Cl&p%^GqZ^9
zbNN_#+w8n49dy@scPXqzc4=qwRruvL(>7dLp8vq+Y1;(dtZgxE6Srx*bQvSdF~)dW
zjNN6#e#y`GKIL82@OW#iX<b`pZY+$UGx?=`ux$nqZpUi_W%BZ8f$rPE>poRF5VB`h
zHcm{tF`n{njHfET*bQDIbi}v8mX+4axIoGQ)WmHUbhB1vy{#wh?R0m~F|vFeqn$}c
zCN>%As)kT+NtE|>ZTOi@osTAMr#GKkJa2zLJjQx%bNRY%Kq21L1GPN5dU<s74a|GO
zxJzd4cV7CPSMdeIx<~D8t*20L11~=(No(9(%0OZ6<R<85?Q4>>PHx&RUBoEzn{xBu
zw_xe@`}1!(>CaENzFSR}|3Nnuj;M4ZXENG-s9(wpua-Jpq=2h-NG_yrg#NDPbrSn2
ziClX<hxmdYrI~Sj$^Edx`xEk2;j7jB@tw^(1B=aVKNcvPhsGqjop{I&Q0^So$hoe3
zo#A_mReo!7SSP2&*nR%>AKhu@?-<?q#rcQ0!(~<A>1x?ETKB~hsgm75Egbi_Y#pCN
ztnXxMmJqtE>)nhlbL>7LR<Mk;M4J}YT08>fQvweuqxlylUP`-JP=0pqKdpVRqvF@6
z^M5{<-@5n>e*Ou+NzoVYv-I-tPy?~G6Y{m8S`)>*P{~o{AkrYXGm4IClz!A|3zlpE
z_-Le;!U-om1SK_aAIzv-QUqYjEwgl!2y-}OfeNpZ<WUPjDEA!g<p?Qkr4?u<xf7B3
zWCB%*QBXiblrS=&QAF;yK&-LaDzwFHg#_i%oJHjoVmXowgp@dlNVW_^GYixLbeBki
ziZU@x!3c$!Pz=w<B!DCx#w}<I%7U~YEN}~JcQ1^?v^X1sj5;L<j$=8@XfnDOOm?R<
zyHmK1FbXdm5s4%z2;ow5!NCWS5l80u3V{*}<`N+)Zj6!A2`PO7N`P<!+USw^kp{X(
zFqY9PX#`{ev!^;r8VC~My@OGC9wC4fa0x<jiGH}mP2!faOF+$|cZngY42shcSdvj-
zYm5vNH2PImU>SKuj>ASv!hn}i39gJME{KtE;ze>2HxwPUWzsUSawMY!XGD-(lb9$?
zTIi5Q#NznT#M8X3OkHtz+G{7YOxQUAJCAtKo?&+)4kWqW)~g5xQ<Wy_(eU653)+}*
z^h^eWlQFTh<;-$wIap4vxN{TO7&+0}IcyM21c=hf(}0cXDY`4mrRBnM{w7GkO$0nx
zi82!+i-Pe)MlXX?3e%8VZY<aDfH1)%<HSg6Y7P<bh(v7?b;eV+6<`H<2LyL3Qb7Zk
z7@Dx?vDG!l4Z-8$aHwnrvx2?@q5{Q(5=WgU2hpR{!Z7L?cm>Fi+Dd9ASV^ofR%k1f
t6*xnL75u&QTu>TtLQyFcGu{yA@bGERaiu^PWcGi8{}=x0Ve?ZI005D#o;Lsh

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 8c5d4f3cc69ab8c05650352239e99e2da4c4ed21..0dc918b7cc691ea0fb7cc1329afe2bf1ade10d88 100644
GIT binary patch
literal 7531
zcmV-x9hBl9iwFP!00000|Lt5`kKMSDe(zt=Z{E!l@0W#R#2C0C1I7%n2(*s_T{q5-
zZ|z%le*Jz$QWB{n>6~t#-ULCAoUz19Rk2vC`pBaC-~Mp>`7h1K;q&dc;r{d65AXlu
z*4+N#-*1|C!@FA4{AGGzukK=*swEzWcOSp}@2{cfP4ma*PqnRG^XL1oLu~JA^Xhdf
z_o4iCDEGC#ySu4>x*b2<-+ub~;r{EpU*Ep}0?s$h+xOpU&T7tU4!*MHiYWZ~>&M>)
zy{bUlw_pD2!~Jjlo43tf^V{bk@Yo=6wjS^Jar^{+@(q=3Go9sr`@a8pKlCJVctATy
zivKQR-QE1uJV%j2@2CgPBUKR!b&%)o<+_SkB{jalTgQI+dELa++)llT1sY9tb@Q(I
z8`|E@qD><a=;dp{YQbwE-s}|P<qh8OgFfh8m^aPm;Y-b3Euvg#<6h4L7wTp6`Ac*E
z<=6WUU*Gq?4)5FFs1&UiCAyr)ti-Gv8Bq2bd!+8fzF_h0^M6kbXh#3~;qCiho9=&7
zdGqo9!^aPwhw1g(hcEMUKXh-&z>5*k^XUizgG`ILbYUc!3fLBb(1?uS#UDw@BAD`@
z7IB1#<CD--XppA#HBG6|%anenDMe5GZ)iUL<?XM3y|0C@C95T`rT7%chX2*V<u#EW
z7zGY07-TI?E%nP%6e%ZBqzVmeTCXqgwz932Akx>0)r!}u5JbAXCJ7=VeVtZ@vb8c8
zZFpFVq-K$n3Ju((ofqhJtQ^g1&1)@cEpwTa&ufxQDl*Wg>&2Mb*xJC2`P#DAKVf-W
zbaxPxinI+6uGS_z*xKswU}_DQ5`G3hi=TUg%D9ZQj`UTneQj86MQx{LHPu1WwOL$H
zDahT+pT3-sPo!(7YA083czRRvbi8)t0BG^#4Dov%X2z@9C!b}+)PxEPpOsbN|BKJ^
zi_glMnA+z)%jZ5TjF$YCfy2RXHJ{$YvBD2CIAT_qnRlzoG^>Wkp)PCGAc_S?kuTAy
z*{o`<NN*ZbXrb2GQ7s*BCZ9a{UD8tYxP=2pgo{pF&BbtoCWsgN>a1_si29NXV8Js5
zDt2lRoJt&IB;ztNbF1jP?nqc6=gAQBWC(Km(|U@Xv&!HrlKf)fOs*x$|MRLU_?s2E
zvR@jK)bIguNOI;!g-Mu1IjghqBqimnlH5rYG<VLy?;M4W)Zip^NMD2wye<yXFQG&F
z#j5D})bj@hJE0@^!-at2TLeNQnm#y52j}$q$Ty;a&mspo$E2&ZTTGr0R-Uh+%qOB|
z<rXJhD+4E-jA9XFa#%7f8Ms0}#|`cF#K596qBatXJ{JRiDXU3hOp9?6Bk%~u6#Stj
zPG*;r<<Y&?w%`OWp4ChqBl+2hQ*gJ*Y#ll{3RLu9SAojTI<STsIKBibyDOTL!8^l8
zn_M&}@|q-?)kNCPqFGm4ALn9mOtl00cC}kT)5_|d4U3_$cxR`;5W3c$)jo<}tOPWh
zhl}TVB{;i1I4@(cfYUFWwa9DI;7YMY6ya`JAjIRuZ%>`FHI`|@+ZY!XB7Td=)GR1+
zHHeQ>Ji!mRpB46#g`2554yO6u+&7=nNI>v!{3h%PEPfj9dU}K@bwnbWQa&Xhk!FN5
z)7+;X`L>G6KiwVo^r5GQ07XaNe0udV@z$??A=x+!u`E8kJ|fBm5e?fRp6%wS{1XAX
z!WgGGx@U~=GbhHV)r?Y>5PWKkXtwwtwHTwGgXk7a&AdzD`+QzAIh`cIVn14K*w55#
z+X#({E+s=CTSTU2+eSEHKKQG`RocAf$o8y)pQHH=57F+dIx-%B(fiO^XQqR~W0SLF
zt5%c-hr-F;tO(|2ZL~J}_sG~R8L$PScA2H2@Kf~1X)y4ws$>7Zg8@%~zE=Tz{lF*!
z%BJwc!!YF5Fy>%HqooO7!c`JUP>4G2s6$6YJC=7usgHx<^I*)@U~*C}kcxq58BPe3
z$?U$Lth|pgBF4B@#9*J-OffjwHD-BQ@nMxj+a`MsUO$RCE&NH}GQ><9LP;3uP9wxR
z#OVYoiKge%W+(SEQ;!&tL`HMB5ua)9wwkw4C8Arzn*wA`YNM6U_EYIp4Mpzm)t+uB
zW-VP_-QE1WLplaF8Ny7Y{ye>l<CrtWLlq)V>PpcMYjk%YF}!(-D@nu8<2!S-Fz|T1
zz*BfEXdH}<PV(sJjb~#E?;<d!BR;Oeu^Zo9l6g2JQX=)yXBk6GP9nNYGu+Rb*<pfx
z8mIF)f$m}g0WVS+d%4Rl^h2Z;B9H%}RK0rrGX;J@8&w&G9a{1O<3=qt&IWn^thxUs
z{d?1V{yf}&fw|p8%0AS^hoyNO==W)xOl9BVirK0Wa}64O69Gp_NFmco{l09svHRpQ
zU!d!{1XqG^l95cLkLG=FDbzmgC>4qTaj>oAQZ42v5ky|yL|abqjV#k{`fRMT48Wyj
zu>s*|v23~SqQ6i5^$am*BuD*&2S@GX!gnxSL6c0DXl~)SAkzk-|CknuriDYcT!7)Y
zX!7dh&5Ki+G#?QyhrP>Wg1a7z)=Or1dk&q`VMk`{iFQ~y2VNa3fm)pN>#><W>)Ek9
zgTWv9_Oy)WcKcp2m|$kQafU*vIPmdO72S@!yo7!v#7PGs!4uNEG>2X<bi*V|j6(X%
zmq{0V8K@}AlLT~z$1_e;acZ0Ts544Y;H^mH$%hh$%~hClpiZXfc%T&plhbqxrxvY*
zcNRQ>=JXm?o#y8l6DgMZ$a9Rbk>J?xaBVW3YI`m|7<4uCFC812B|cD@cKh*x`e{s|
z$x&gXCQ^LBwusZ2>GRl9`=dpIZ4??WgT$LnL4Y3OlEi+6TXy2Uf%y20PB-d|&)m0h
zky`Gx(Vdgu1{~&AE`A#b{{B^3I%x4J9EWn+GDL4lPut!On4Mb^3lck4cspy>)f?L{
zqK%(Ul9t2)K)Iuo7$~{Yl{&eu-Xspx%$>-Nk{#b0iGzrMrW_cTdr>lT>*@n$ao@!~
z1oO#bmyA4}I8%y`;a6-{xwq@;O-6zCbPgQ3$(>;dgb@LtDG(V2E6$h%6YJ`2Zcw#X
z@r0a0c|3Vuu|Y@_2yX)6O>kYX0sLE4Z?O>w)MA3A+d}~|6qH(}{HS0h53{b`=7A>6
zZP}WjEG(V%Q+81lwkGJ5zpUOQ9ul@9JN933045WXat4&eEKbP;BGIaPn*&BC{E><f
za0FtLkd%S;B@ex>J{Uzxt03SA#WsvsAXo@RnOaa&u3)6px_XmQpe^%c#)^fe<O`Ic
zK~I+^g-Efg-ev(y(1#|4KqBC?1-!B_rAcYCuHNQ>sZ)IWOiCCuFqE-|jHVod;p^)C
z!>Q-ZJ=}H(iGcXwxT^5#!a!C7SrG(;nKt#*i;7ch`#xtv(3}W<%g=16?9;PXC-H(1
zeL_omi5IZXIbKLPpVCCEW44@L3114Q2Munbo0S{Na8%k2tT@cjg%Cx_L9eT~IS^X2
z3pAj7{+49|q!8{&P^9pw5dsy}o2(+-$?v5cULN>3A&UuYlsxUaI_J54WM9Ief}9bX
zXleV{w6qr3U;-i;PziR3;uAXzfM;cgRJLV@o0MNfl*1oHnU3G@htFSs`+^QH=NI05
zSIe7dKE7MtBqUkhRP#ODz*rsBKZ~``zP|tZdFWG{9E`3T1d<ctTvrBJrhUu0GKl?o
z__8XGB7b}r@&(x$0Zr!&8Z%V7CY#PRF48)g$E0?ZseLk=Qt@O&6IdpTiiar%UgYk`
z<|9m<AYutF`MP>-^Vzm9Wmcx?n<jOd>d63-Rm8zG?|EiIS0RWBF(22Y>k?@?PPfaC
zU?ENfz6wE+5u7(jkJCV)cWwEuH$iK1KQvm}{44~g%@ys3%w0GmYwmyV*v6jq5zJJS
z{r>k^{O92yk*~MWkJZbw=G(JOG1rp!*(~o1yiD4-hO~tmo;{0CSJlX(k}FaCy|BF;
z-2r`Cz)bi&Va4o)Lzyuf@Xk+&umE^e>Y^8>s=tL3i+}|KdOZpZH=A)~%KF{xM5CL7
z5T<Spf}gxO7dme)h`%>kpwC`->b?Z}<xM8ubD&pe{M2eT#cH<ItgFTGCp0f6I3G^z
z57*RXOkgMohQiXn*nL@(!!H!CkGLMeg2>C$tpjC=`6*<Bd1hgH0S{ERu`3DfBjCuv
zLn!sH<}<Bmw)0upRTP&H#B^j;;8v@zqByWPMWiU3757x5coDGCjFF#s6h9u&MF}{5
zIMS@oAv3kub85Lf(w}aqsqAQSV~TmXm3x$?jmaw)63d(NZWEhw#^NL=Mx_%Vk6GxL
zO%7?N)6?rCCR3(ry6*fi`9f+~hMQ4YvR8KO!GzS5InL76^d3hRvu!b5Z8p;pXJ(~H
z+qwJ{;!+7?-Yv_~Jx}l9UJD){BUa2u7la?GxtQF`GIGz;yMBZ?QzCvz!pA8Ul%IK+
zz8;j=J4b7s?R&6|XJ<pNA2tjfKGj;ImA!74X!`=O&q;Siap4ONN=m!%2?q*Y_=JOU
z6HJ9CTf6WL2YNd7CjK;j7C%RyiK+N)g)@^5ou9utK%1C6MW1Df71{B{@rAN<gJZsi
zD^vR=H=lf4^d`x-aUL(@giD)r2{y^{y{`T8(a37>@vD*5fYMl|t0^b%cz%-)l-oCp
zvE-wSW=KXHj!u`uMq0)8bd=P-xYH7s0hLaui1Os*+@6P)F5Po0nA++5bWUSOrc|aj
znA+8uZ)6&h-iaxtw-ZyeT&otp*Xff!I??4(4Su=ZkRSBEJgE$)!HbxR&mU&wt-`5p
zeuhfz=JTX5!}Jw|7jNjdJ}!27;<-F7w(IJ2O~dne^ZP`<I!<~#_+8vP-W?|C<a4Qi
zt+s!ywtua*Ct7V$dz$W<(pV`4Ln)GE8uR){_ehq@6eo2iyG%h}2>O7mLaN32U*@Om
z0}PM7X>l7jjUnV5QbqQ~O5AFke0-u-AD+bf|HVfp^ZosBk2lDfeRh)F^q*U9-ZxHP
zvDD>thwS^7={E1(EOqv^iF&;n?9?W^<v$I2x~rS%O0K(4ZO}c8WxCJ&zPWF{-6R*u
z8Q;6pMP4Ob1I#YSY_u}buTB?W1Kn`d?&t<wv4=X-OwN?|+tH=QO*ENZ_tiza{mWj#
z?S>6w4wS>riXGg53zry|ZbvuZ;>F$kN^W{T{5)a_G0RoQw81k+_nha;jAB{a;hn{e
z(z)wop+75V9E?rKwB5<Z7T#5494<%3o5cDIV=?Wf!Vc&xW1m73%QPeTxqEDf!R6$5
z;CmTlM0Q<wBgljp6oX8Nmq(@^He$tP&vo+UJDs%B0pGWGOOEi8wAxO`t@IfUbob<G
zi_S$kvi*)nxv-1Jdr`*_lb4=pRfjtg{O;h)aEq8qQc#M4ALT6ehj2jx=#cZXN2p+8
z{8*9CWoY)h{+>%a#jtRDIy#rV*i9a?yibmTb@UEyG_9gQPOJhrFaG*Q{ILBrIX-)u
z@X<p7sR~DA7H4!igz19?k)fEtu?)>wzm4FYE^3o2%czJ`DoeW<cjFc5{X5zs`6P1~
z(W4hF-O=PDk79c8eg14rj}G^IOwVBSZcJaUI-QB>;kMEO+Nae|rTQSI2Q0mGJBsN9
zxdYsmOWdP(<&W=bPe?u7@6IBZ=F_eAfVbn9AA0+&bs@K0lbXT!zEa{f?D>9E;9%G}
z4jUJv_O%l3KIxENnzd5gSfST+Z~P47;u@7X%h*k+u1u$vokIirxedy*?W2Lvk7s$g
zl(L{?Q9=XpW=*^v9<q2xizMXu)ZQXF4y#8QpJk+uO&6@`^7k@Q$2YP#%Rn7F&CH<e
zQy64SzrLI@vik$PC@r-a|2A)_Pq{_6ms{LH1a2eyhO$o&g#$a<OhWDD#P)>R)9{0Z
z+PDNd38i)tU%S|ep9+PtYYFutp|htJYB?;6Tfr<J<?@YAc6>*tVe(uGsGyd<3(LOF
zoDTQGN!N6^7tRTbZ$HnaPzo-h&OawTo1|JxD5merWab}*x*$<_LP<v;vh2GOFfr4a
z9$w>yZ~Kd>b5m1%iCSD(zF5W?(G=fS#!otFuebfN*g3(LgV34sgSGddkKxV=bohzf
z19hfUU1G4fzNl25%@>{!(*?0h5{7GQFTTG!H<HV8gcFO4lzfS-XO(+SVW+41Qw2)!
zv-pMl1pU=Wmi|1V_sb#I{HI}3rXv0+niExo)3?=^x~kk&vFwkX(95!eq8!R{qL^+x
z%#3#v6Z>hKryczCM=~EPb-Y)1y4-iRtdg%3i-JP2c&9DwqFl+#E!yHvGNsGxk3NQ%
zd@QACnWmHElV1p1ubhrv(J2~&&Tm6=|GqpqrrY2X`R`{AoDi)0#~f4@{R*@QHGb(n
zyzk$JkN(dh<Au<}4yxAuE;^?=Gulh~g+Oq6N<~>Wf6*z`LhIp&RBQPkaz?em_tGP(
z4YrSz_u>Ppb<f`)X&DdM#bg?qPMbG!h3o<pT-XcZ{0Rs~+2K9NZJAW@&3YyiIR*b9
zq0}_Q5}OC?knnFDc|>AC8GDFeQ}s!E;s|u@$>yemnf$bc?IPbDGU32R<)6)`cQGYT
z@fyF^KSGx~a}ke&5*dAfdH1BV(<x1s&!uCg__uBJ_TRQS7OD6u?h%SNJRRU<8jIik
zKU9=JNfe((#c4EZ59jX4w7MhxI=>^m19JB$@q*Gm!rigwcs#TZZ}-@iU1Nqmo?^W|
z0>LYC=XHN}Ajk3^DsjeG8Ti`6SKgHH3hz0(!fOGpyqQ$B5H5g~&r<O8oWY??niEJ>
z{vE~~X0j4el?_io@LCZoh@5T{Pnl~vHh6PX7j7<5X++3W{w8(`e@C6U1uXmG{t-3J
zks+5abMO}rDV9Ez?%o%KEq}f^(4hGZ4_i%lf%JoSC^Yf;E@c^Onffm_1+U9tZVhFg
zlxYlw8b~!cMZcza()up@)BRlMN>}t3d58Ir9u*CX*)icS{>O^|@iCk&-QDF~1Uu|P
zM_rt*+a#9Z1T0TD@#F3^9(VULbpQ3w|5?ZT;jR#Y+7>jH#(~m$g!e<!{iSJt3)#WD
zo10dQV(dLaXx}Q+NZqxp6+&{`xV};PR#d!VH{IB(wi%$~Q8kX6rdP7#y6tW6B$nN+
zs$^*BeCNleYyH@ojt!t}wCQ!%!48>_{jI5VYT9&UFP)I19jxYF+rH^^XZh%wt~c_Q
zv&vVlvQvA;1;oVON%aE5>zT8C+qhO}&zgpjsA!4*@~oHlMk~jL4oDOcUku7y-Kf56
zfRNfoQZKdDQMSzKaS%#$LvQ-A?OE?e$2#6)aNbi#z0+5?ad5J=+$+}@)wDvjgBOO6
znvJ|Mx7=3T?Dw}q^>%Em)EJ-?zB9aY+_eVIM5!<<(pM6iRQp5}K!^qyaOm22C`w3e
zF#N7-g;!D$5m!lbjt(1|(Tfh`9QV?6dJw+#gByj`q8%HeV=thi{UEe;tsXS&4XW&#
zp=~S_s$Fk&kVjS$|K*irmGG5tm9UjCmC%(?m5`MXmEe_N755d-Oar6xfS6t5McWR-
zNv(&L!TS8*NAGSu*@n76X-qU+C|IF`vBPS+-t`{yt%U1L%bQ3^UO;J3n#o>tTJu53
zwr!p9W-u7A9|mhxq;$zd_Vl-NELNH7TXcq1S;rcZw0F+8<E`eEW|i`la+R``GL_Pm
zQk9aG5|!eWVi&M!8LU(a=9!VE6;`p)3aLC(L)$jW1~yo}y3(rBveM#*S&~ao(h7~e
z0+U^*m26=g;{dnfAVpy5EA1+6ufb0{Eyk{eElY(FnW1YMY22v#25!#|#Lv0PiOS)@
zR8Ch;{S)vO%#NKlShpPvhXFJ3c7z}BaLuiEZQyO6hPUL3eC{w9(<4qBi~Vnh4Gv?D
zW;>XblM`=NSzlT7wv{!N)s<D1m6a8h<&|ZX@s)9vv6V5E(Unn^k(CjZ3DOw$2<Pz+
zFQC_0jbdob&<HFI4RIUU^u{9yO6v@H5-d#5E6*zDuRD8WCQ8F{MnoQ1Do1F?e%qta
zc-2h2RpsTid3z<KXoT@2ocSO*BG_OV>ov1*dnSzAgSWmmW7Q#cj|iN7J4(k|**n08
zk%DL6j50EImABVttQx_LfcHa?9F^@6f+Qw>lzj{5A7TchAIA^y$X{E620%jtC;|Jm
zEl`piTEm)g9IfqotduALaYuJ{^(k+?@Y31Fv|UFbm$61VVTaBR4w$8n?DbQz_Y8=%
z2SQ<R1_P7Q19O7E=cD(!w~@WW5BQClC)2{v`fhA`Ef9SP(<muM&U>z47mX584F3ev
z4^Exujm9K+!Lh)Zl589_@Q3$9t0QQ^^uuQXC*k?(9tUt!8Rxm}IU76gL_f4p#)#d7
z^`nUv2=_UQAczK)ky!AZ<UHX$Ibm!9*~E!h5wF0E+SzM|ImC=k*v@F+GT*upQC<$f
zPYxaoAwSL;T>d|p*nr0XAI@M8Xqgh&t|7*>inSU*-3$>qBS!s@*x1PZJ>up+^Vo#*
z*rW_x!_Jsj8ark_GTSv07)G-0mMdzHZrGS{GJ^A7r?--M4*1_m1#i>$L#Ld=HVxrk
zbbTa=kzP)+?}WiR=v*TaKOA$s8}#T}Zad`#Q;DQ|07*V7ib=W~d$^{irwz6Rla5*2
zVx|H~AQJdW{4jBfo{1XBVQp|l8-7fjBHhqnh`W7&1PW+G3eb{3i9m?JVnWhZU$~a=
z$t(eIBgek%`Vw>oK&)>D-3ts}4+dJ01MAu7JMNv1Y9-cMJOTTW({|K#BUY8|M%8#N
zIx{vcaKkX@WP4gZk^X((do?gR3lfbT@i>TKREQMJHI3$py^c5qdsT$V>q{Zw(;c=7
zQeczs`vIuQ_(8zm_@U#I5+<Y+4D#xR2vm-hAh|KxIPB`A$KtmVaR*+Ymq`)!2}RH&
zY<~oA_)vu@vHdtS-W$`kSf#_5L|7rFr_qK1!)|a!`@v|{4cIPmF*vI*FQaXfDE?{8
z0r(J*trNO$0osOfRLr(83f6Lu9h*;{&Mv{mKFQMj#}K1!u~i+6kVdp)*9^@twhYoR
zX|=J+CNazti(!~yL)ZCHK!#pQZGj}EFm1zHqs$c1bSVa6Hb>9~`o#|{4V~43B_cQc
zJ$@i=L=*)PoSVmP>scpxI|wlf1<%!Ytnp@ac4)e;A2>_WkyP^UBcU*s+p+COEry=<
zpvp+*90STF$E$9!S4A&S!5&D^zVza$aXkZGR-<>^BAmB~<PO_S)$kS@FY;XuB9gOk
z^plTZA+&EtB?bn%y!Xz@9&V|{9;zAp#tw-E{{a@gaae55(+&+j*EfT4S~j|OrWcxg
z&WZ(hpy2oqPK)pTI7-#~p+^KZEr4I&^t~JmBr#p$%C5^*HH{Q)%T#9!hh}>wurZg|
z7iuS&jAJFw?&znl%iKFQ^sVtDTs)%7D7=T2vtG3rXV;7ibL!@<tZ(dvO~ZPuv9`m4
z>{UOi(P-Xj3k(zuDRA{y*7-R0t+!3%3;=UytV4YFy@q{Z+HET$XV0&%a0aJo9UGl6
zPN<GjX4V4vBD^4u@IG;t5#rE!n7^_B+9}l_fT>Yyu<u*A9Dq(Z4Q3l{q5u=V^6JXm
z`wnZ{E6=nrOu2DvTg^?YtnvsVlj8N$a35L6VcEQ4)(Ln=1ytW+4>bxs3ZU=A-IS>6
z+EO&eVGE-h*&4}tX9oDv4tCdd*lsedlN9#qQ}3M}wNgq*Y-i+Xbvw4rz;x>gZHmeE
zvLhgW<rOa(2Y&7Nfcb7sqXyqQAWH=_DTlFZZ_$l`9s@yU9}zePCWUT0gi)+(X?&w8
z&npekNyibbhynjmCLS&us85fb7JUPi_9Mr#R$?4H93=}(*bg#kN9$BaTR+bPP)jQr
z_Vx&da1#bmDKOzb$fUt+caBM|P1C6s=I#b;c&&xf=v*f-kylXJ{{bsY`ZX?t006YV
B>7f7s

literal 7296
zcmV-`9Dm~<iwFP!00000|Lt5^j~uy?e(zt=Z`$<}?_(hg76xjR0AU7L7`cywJlFD$
zuGZz9U%y}Q$Rx8etEyYou-7nVN?pk#A{Zniz91v(-~Mp>`7iCq@$>Ds@&5DM5AXlu
z*4+N#-*4J?<GV&Q{AK#WUfsnq)ku6D-+lb@zrTi_H|-zWKQ*>-?Vs<zj<LOK%&XU_
z+=uelq1-q6?(U}f>2~^XfBWg{hx@PZetrA?3pn4jZ{L4wIBPg>IQYtjE28k{uOELK
z^{N7G-+uY85BI+fZ{D_d?QfsQz+;2N*?K(V!|@UL$Tw8B&2*Og?fc>5{Wy@s;S1V9
zQvAD!b$9bq`y53Iy`vsDk5ok{)IpxRm+LBGmDKnGPd)qP=XDd)aGQG*3pC1gP5Z9>
z8`|E@qUDhY^zw~hjo^(CZ+43D@CHx#Kp*rh%$xS}_@&{l5m7F*aj)lr3-z-7{H4AB
z^6UMFukVLn$M@ZDREpM%5?#q-R$|eO7EtjRd!+8fzGCt2^MB_CG^2n0@b>+$ZT~;1
zy#09p;p2zTV}AVh;miDe82h)hz^f6^_u~-+289+&>B2|~6|gM=p%E>D7k?xri?Edc
zw1^`_9G`@yLW4A=uW3q!UZ(UrO(}Zfzp?%Jm$$$E^}Z3lk*txtk>XPz8~$sAD{CS>
zFbW)0Sdfi0jnpq|QKZbGNEI5`v|nG~X|=Xif=J&e)+pYnN)YMFnk0yf^mW=9$~MYi
zwBgHIBsGhqRA}I`c3z;@Y2|3vXx?biXj#gnd|8uZQjvi^-Y>>9#x@3K%r}<3{t4UL
zqPv5jRHSYA;u>wj7u#4JzL-YCq=b*b$KvDOpfYYFts{NaXx|vtSkc(Lt#TbS-I&D$
z)q>o;{OQXP`9!*Ls&R7lgl}(Zo{l$;3;=DOk|92?!_0Wq_++z;$W5rQvROqH{$FgC
zUu;&<#5BINS-!McVYFno3=9rFtNHXEh81?0!4R`*nR&OWOtWfu9O|-14ZK(|6y+Ap
z&1O|=MS9biLJPIdhHB}EmHWqn&fH-(RVy>4Rj^)_i9%VPj)hm8jnZ_X*}NO@eKuXW
z`}Tgs^kP&-G^SenapH4L(oz<F(UOLdI?_^ZR&0?%14cE5)@Y&XEh4#D+WS^EmeXFg
zvS)GYS2{8_>j)bJOP|`S0$fn3zdPMghmIV3rtFAP|B9BW<vn}#OArS3<n>8XE|4;f
zwFQu&Qh%2w<NMKMd~96WYS@M4Tv%V$<Q1ECIFy_hK~P-#y}fTg!96z4HO@yd^IAY<
zGLjCv9q`Mik?u5tJusjXSrSdp^F}Y1UhaWi%TQm?+-<~Xn!BxL^HKZ3MLaJ{8*{VQ
z$``gIAxadvyH|U<A@i_w0dW0!hjg?d^w%Wn&(pIwUTL|T%BBY&`ku!~xQwZu?GA)9
ziw~?9&+GGfd}fX|2EK0XjFK(&cNL8jV<Qwxu#*>K3(q1jCV0zLfSi1DOBRd+DUtf<
zvy34oClOtt8SZDz>@X34jf71Fx(hcumsrML?y?L0;17f-c6}^WuU`L5AYBm3mSNbT
zB|ovaQA>@BLEb-W?|(^uZ`#kF$NMi>Za0y#4|Va&(mW3Idj{}S_ATz1tr{`cpwTx$
z`;-IEahZ1N_azVj(&Mt+pzFHGB@SCMl8N-uz7Hma+9wCCP;`$bP@q)Has)8Ee|3}N
zkQ{4}7%|GIf|k2Dp%k0tVrV@sx7b$~ed|WlmtZdoXgpA{xj_KZaRMS4SCE-oMZA7T
z!U{P95HSM~L7`5@kg;=78SrtEUo4ynPDlBFUR4E*y&_llOGA<xxHk?-&itq_36m%n
zbr$Hkrd(7KgpPui0ZG8xr^2Pw;3!;@zQP=MT!I3>U=HaQ_fFrBqn*HDCtM0Kz(PRr
zEdrqtO&<aS2SC1xmg;x_4SW$TDKoE#btsU~K0r(bhgey&3I(#Rl|kTfx3b?eNS6V+
z0siN+jTd;@6C(pJz@So$0+OL7qp}1FvlxL#SWE#SSmI=MIT79w5iV7jgOxQIbEMcJ
zbBX{YE?XcJ>&Qva7rP41?5qP|qJU+V;LPrd<{|<CQZc1y0R_!9Ni@K;1h=ASz*^SF
zxhSwFK^_-S&o=sY_85J;8P$cZ1$wD=0-DXk#rJt9IJ-T#3|@dVssKflHED3Q*a<-0
zEgOV*90BOuX&Z%m8)Kn`h~FZTo5eYf2tr4+VK;F&u+xG!OoBQAca+{W)QBxOUiJ5>
zKb@+nsz23;fXY#uVL3p}CN3{&lH(zo;h2sWm@w9eyN%iUn1GKaFhuyIoUjCh%IY+0
zRg{^0P5_6|9%opwi$Vzl6<}fyq;qm)1%OGk0~$Jk)PZiO#W}1Vn^h2dr=1HR<`iB}
z&}?qEk8}g9DBwt(p-?JL;C891Zl{nt94d$7<jKhebW6|DoJ6vr8zxy|6f%#NmY#G0
zpMr{_b6*kmh&l(1;lt22^-*V(qQF~`$ZmEZcs|F0I+?2D39TqBIZX&lEm{fBETB8M
zKs<(Br};U?M2e+8@*HFMFs>n@Hib^LJ%{<>2DzcX1PSw6ei6&G+sFLW4{nm1GSZLK
zM8f=VwVcj?p2wEjpV}naQ{!cjc(MuD)0em<4H{W?1j*q<`F!HAQD=Ms$&HKDN+gc%
zoUk~YHMiMTJf~-1@w9c&;!}XS+^P)B>D#uovzQ4>VnJfZDr;xWx;l<J9y`o}TarpA
zNo(S8+}zO-KPb7{l)|mAsyB%{EGZ|7Fv0P?k-%SbcuVfl#fzGmTUVc8mi!-_GWW@1
z*Ni+x6Le*P*n{zk5q#*XdXrJ0oiTpoCU=G<;6?;f_#j4M6@Cy*tgE-VLDgQx=!aZ+
zj4D=a;1UJgn}B;0Tvu!m(yyww*a$dkk&ha-hk|Hd&{YxL_Xt+=Fzf1V9%#bc)>;#E
zt3+`e-Ij=ItqF?Y>grA6;Q~q&A>E1t;%p%)9;92D3PB5aqE+=a2aHbmQ!0YP5%5hy
z(v6z0dFXZZiBY7G84gD%wy}r>oP|(y^8{+jRg4hmtg1H|1=_L<R97rC1=di820dLb
zDR_!i^)?Hv1buQz!I22qYyqn*OueKKD6Oiud0^@k4@>HpJi;$w=mrilntBKb&Q{eM
z<U#On98=NW!)yna_>G5>+NukLTEak9I00euK`r&7;^f=D&rvR#6Tx&$ly2Zr_UYNH
zBY#1sGzl%~;_OB({sJvN<@@M>b<CF0tKmy!^q|2_bh9!;1&&J5z>32RT?kRs9Q3++
zn**UWyFdfFpWIrR04aof5)`RyYJ@;l^(LzbcglPAlb4|%GqT8FqvmPX)g{l(mAQgL
z6*(g|(bDG1T&)(Y!30DKpc2+0ijUS|06eR8NM&2=aFg<jh;sOYDAO(5{rLIoZ(q>i
z<@~_g?`nAx?Z<b^lY}J8lWM<*8|BrBz_VEU?CbllpAkUEHYFHcHwYv%;#^k-S#sR6
zt_)&-9>1*0qsSlMg@cLW+?S?v28{(OU6V~`)fZ`<mPb~*D%75rO|5uZL>Vm8ii!v1
z23F+m)S8blHABQ2T=I4Gdd(MMUpm6c)0ZbTPjy}ZX;s9*wC{Pbgswsm6=FVuPuIU`
zI*!BTN3ak_0$+uoC<x90(&ID`=v`aB>rK#_+z*YGf}e$84z4I3GIy^CUbXkX_iQ6(
zeFQTVWxxM@7XNv;9OCOR`muU>)_!|dDCS!7KAYuzfrqS(Ye-wE;n}nJ?W!7CRB|PX
zzgKIoM0Y@+7BCYwPgpTq;ZSDG2E6kb5mo??N?o+VRQ0!TViB-lK(D79!_B5&0f|}Q
zEpK#l!iA}u6V6ZGoO7Kw7x>?s!qFEGJau0j{qiIe@7d9-Gj?h<n_@NFYSz_a_!F8J
z8P11W*pqweGA39kaE8LtUqoNll<*71>m#m5upsjCICMbSCw>gsusjPly?_TQ+lWd+
z`v^En@DNJ<tNBbTF5CI6>?(>&2qGU@Rk+pat0)dEju9!!X2m_#C|(3?G-Ko^9>tG4
zbWsD2ANDlsbI3w1_MBQS_w>gBHI<#3+?Y1BWEn13S;wh2@$$-rWT8!Yw~6IEAaQgj
zMx_~$$IPObAr!8ij!&;oG08VoIeqhC@`ZFC`YXx=9@(=86H+-Fs7OJg=Qy%>+ZI!h
z%;t5(nOUi>?Ob^ZajAsy-mSQ!d!C*{t|GoZMy!})R1tot=HlgEaU=IUJ?lq^las5K
z#Hu)@g6?M?rmqKG?46^vzU_PP8ZXX<UO#LYI=p(aMk{;WF46V{VxN=ljN(E@I$cV;
zkdlr<7gEycZi1=s%{DINq@$-(Z{kPeWASnH+KY<0;?86pIzMMoqfNX#MW1DhRk!1d
z;R|IcD{oG*kg5H0H=k@<v?j^6aUK&apNE#N$f#}nk_5jRe9VGh4JeHzryCwU<NKR(
zpxnM$7E3wGxD06#hojTwu#tALJsu^suksY*HlWgsis+u4jN9|j(xu$ximA=#r}H&-
zWJ+afgQ;De`9`MU(mOGw>+Qr8E!V2W=XH8TiB5ERRD)l#8_I*;mq(T1G<XqH@j2<P
zY!yy*%QIAJH=iek8Kw+3FW%5+eO&Cyi|6{d*siNnnug~wtLI3+I!<~#_+899o*gFX
z==G0(?Y4jIwtwxmC)#aMdzw<;XsmPvLsukeY0Ud0<&iAO6i0QYNT#4So_s)7;i|>?
zU*>N`a-BzPTD@VB#t`ltQbm!C7(<Pt#6q=7DvYoBR0)K0f^&E`Bgk2#6c#V^%q=(H
zAxRmEO`Yyg<SynnH11}pi%dfGdNtVGrbr{qgU*SHg|6hfdv1g7VJ!I_mG|v^`|T!~
zNY40PP8V5~kOo*J$ZWJS(XQr~8Uo#rYIiCFu8N_~G?O#s{dSbpxQQl<S2%RlZa>*8
znB5RCmOwc~R_sIuTu5SEx}C~^i!Wo8uUVvLb^2Y7>|&Nw#}we1Q}3?K$&6yz+u@nT
zK<QjMS?JFy8YjjkWD0kRv4v+98HeP^_;!ds!&u~KDnvkM8T;g#SfLro&*ib5bS_87
z1K(>WBZ^lrHk?fGLD9(se|c)Dhd``K_FP}Se5aFEI^g^EZn-18<XUZ~<JR>V4RrV9
zX^YN9cVzn=Pu+!GJl=~s2A{n2OuIVdNbtK8XNFtERFZ<O82G6>i~S*7Z~=6Z^Rq{&
zATxff$meco_PhRGN}GLH$exbIWzTn$g{<?*QLy&j!HlL|6v&B{1LxJR3B;F{jxWb&
zOA}sXs~}Znh|FS)j)#z6LK6jw2^?$JT=d&;?kQ25Oj$ui98+1^MZX(Ur1x{QMY2ie
zq(_fdv^GcCMxOHN!S?yHK0O-T^FF<R(Yro<Np(8o(?hn>0^0NLr&4{wrw1&(bUWqK
z333OxEf>E>&&r?9)y_yg<aZaIOY@x79`JU2^Fwc+wJzkAG^rVk?<*yyVbA$ZfrDY^
zIBX<F?Q13EKIw41G;5{GSfR(1H-3h3l}2UGGIsf@tI(-s=g`3Z-3HyW?W2Lvj~DlH
z>B@pGixL`$nKdyzJlx`)+9ctQPwj1z({A<Djn6Vt$8v%-C4Vm?b$sI%XBntt$2T)5
z`xFKluU}v08`=E<UUV(B>Hjvf)brh<+q+xbK?H8&_6=p99tsC`w3&q3yA#_JYEQ!t
z7HT62Gz+D6F1~iL6F(LTW!DnwMM7s!E!1*Y7DK_}KFXDWPH}ukr(yEk6;MSjy%$!z
zai0(O!bw*?+zaP~)%*PCu23p2qA7nO;Or&UT0)WEFO!9R6zYPD!XrvL0+A)|O2EYA
zGd(=UfN%SasdH0P{klMvuzazMGoq>9mv6#r`V{MJzbtl6u;n0hru<;-J?Le)vjUxb
zMecz*Q>v*kSlnM!D$m{*9ud<Ou}dxt*Q>pH|L)vKF1sVlEG|;=C9<AX?m2}WpX%od
zl;C6W3HKB9D|jsZ+?)5yAy@u+ll(hX@ipTkRfN;G)tkDij;dJkn@04oL{M~xvYaTU
zjE9-=?#0CZwawEGKL6<7W2KIHb;sL%CuEg;rC1bHip4X9u#0jfuS2xOoD@oz#gEv9
zhjJ{nXoaSe<k>ES(5s}QS9Gd|p!3_<-oLL;jwu^FlmC9^zzNQJc+5dn)vrQ}P~(^W
z!~5ZF_#v0G$ao?2u!E{~zl+YP&W!ewe!&qOpHk7So4@FkYN7S;L#nm>4>_aS;Cty2
z)dt%~%6stv)w<{Jk6alKiDC*3<<sVkyFzvW3a-`*{QMCJM%l?c$ZeTa_0D=B6Bz~n
zAfZ$qVvWrMc1ZX)jyxi<po~34u&Mf_J#h+j?aAiy!AyDD!gi7G4w-OZqsrIj)3eBz
zr+AF->z_iGJ980_gAy5i0`u-kXY(mdai2@aO!4>1^!D$SoffHjEAA1BH#{BS6dH@~
z{XbNcKuJ`uM#X6~Y7gh`$h69leqH8B?||GrO1z@9k8pR^b37i}hqrrd>#p&JKAvK|
zJ_UkT<j(8<>_AS-ds2xr#wx(q9=`IXhF5ql(G?ymaOF)_)k3%eR=&7`r|$(EDx^7r
zRLc*{5PB?OCaWP;-S7wmuNAR^$SIpR-(1tN!JAWcA#;gJBSNO~H?dRrU1;VOu<Wb+
zBWhYALoQ#I;4dChEPd#@dtVT?{2XhbLGv5FY&G2l(hrVMXyVH#Wf^OI^<M=Auj^rM
z4P~B`JcddQq?(eVUsF74eOLSxIoGAq75&=UIREHT)v%f!6Mn%wCIZB-;cV&duIwV%
z$u4x%#VOq;u?#0*<%JVJ-JQnc?p}uOzyA3@o0uQ&DiNq{MPq3kD6L0$Keqi}+U~b-
zJ9u|<(}_t;gNF+pI%Qg^`;K)&NN!s<v`XKK13$2ve(F@$j?nR>TE|U0DA{w}4R&x6
z+wN8!WN7Go@29r!{M4DAji79_8Fb%c9Wo(@TXWE<Y1`9!>4lu^Xf^lR4sEY{%O}_N
zgORtK9sI!^Y;MoEfS8D#)F3dtfjK*Lt?PvLtZf;IikA477rneUS~)iMK%(&YVpQJh
zRt<d%gw(Z?da13BvSUt9qfnwB2Qy6Fzy>!t*7E^_^PW2DoxZ|Nqm!NGUb)t&wiBuw
zy)b;zY~roC<@UhMet#>}V5infjR8vGd&7IjU1wlSlnS#V*n#^4cl$(Ig}DIk>RT_m
zZWK;xJ$4LJ;zvJuck3X8@E1^GqUAziY8+Morm`R0;GqO1TyHwwMoR7iN~6+D4x-nZ
zk3x1`=ZrU_X)W{PXswEr>;;qt`av0srKg4touO*$SWA))&iQV-mEs`zL9zo45wd}(
zIS73a>LBDnK!f}OHXXy%Nx?ib(saTqHd!H+XKL)aR@uM?jm<$~U1Jx>A7)AWL`f?&
z05p?*ua)ey$5O;zbC7~qDt3_mAl)_iX{W{1cfHb5VMJ!^+g2JksiB1}up{wv@?h=3
znu9}6cCh~pyalsUuZ{3skA=ekBzQOVFkP@$op)W}EuMzA<cbW@I2tp+c^QkKum|dA
z%+YLzWo2FBZS}#bgM}JU$Pbnsj6WE6F!o@~!RUig2O|$g91K4gcF_Ky-9g)fHYAPK
z2dxfT9<(@UJhFrG2jvdR9+WvKeNgJ4<UwIo@&7*pdX3#E#@39jz}C<Zx0UT+JUoN6
z&X6U+#&noEeQ@f!vq#HBX{?+H<`^rL!`~qY^(Zu6wV5}(m%BD^uY?q>Fn)qDA0=;{
z7%gLiW)^18gmHU*@a)=*RS$<Y83&*+Nyj=lIQZ1bV3`c<BqL*a@Z$Q6RV$bguzsWV
zld=O`ki^7Ka_C_E17rMe4qhL;x;Fb3u2%y(01b5=aDyB>MCa2qS=$fTCV@S8`-8vw
zWOrV8>1=Ddz9(nPSSy{dV{b?270?v9OU9mtxo3c9L#IauBQP>4JpdTEdp>!u2OF8A
zEkj4fpGX5^=liK0w1CegB%`F5I3KveYG{>+LZ~O0cW~-GZ#5>s3yy8glw{MWfjYb&
zI~}14Kpc@GTH@+<hGB%pd2R>JrrtX-j2)CQ0a#l<nS_?qA_5U3Xi3<Ts1jMC8whiJ
z(2k)ULpw%_Bk{$xof|wwFKll#(3tPs1m7-4pe6^q1xFv}OvryUu>pz!Ih;W_WSJ6(
zT;N$c#X9XeZN`L``HzXs^xwr>{xgqFIFHa|<QnUYd8H9N@`>5Ll|U|%^|u_oI3(kU
z2RN;g^HyiDl6el$-%AB+GYn&|oN|2&ColRTkyH;LIrPF{AM~!3a2$>~-j8~69k;#m
zf~iDOK7b@*adJkwpAd~Rgye`dEtvGo+77c9NCJm&sEjL$b3qxA14rn<v1d5dA#&l8
zbVDqNyLf;E3K&ER(3il5z=c3yLQ>Q#Tt}#6kpNtjegX-41Nb$xqaFkXuSWwd$dL_f
z@;&!XN3{ml_6gWeoPto-PuNwqpH%C$=*`r201V@()7rxdej5GzVeo2XbSxrTJK^gn
z#!10bFxR%4NA}o8p7ig@OI}|H36t&+A4q}7-VY<tlJTQ}x$$GqlMW(6;+j9jDg+S6
zHjvyHZ5#qQ>9O;zgwufu7-Z6dcsdF6gmpiGH9&yEbl71UTknnOJM7SLN)l99>4|h<
zz^@;j(S9^q^&{dVE=Fe+=47&6l0-etQUEXnTI+=#I^eZ&niR7g76j|KM~LQ=krRub
zF;B89|1reqI>e@<5z>fm>f5m$r;b4yCapGB*(3&kVlfOeZ0vhK3CJ)=sVzXH6sBug
zXOzj#jMZYmU32(rn00(W2riq$XLC4hu4(lWM;k@abd;$d8OO6;@@^Dj5(-9Z=vnK{
z<m}k?{V?+ALIA(<aep5Pg|XaD-7sk}4it1MBbjpy0GDj8x)qGzCCvjkdi#K>aRUQX
zR+D$!!jpG!;tnCEYI%o<i!7Hz4>A^(KJF1Lg!bK}#K=IG58gRBz$$eJpW10??U-1Y
zA7C*Uht1|Z1!u6hz8#Izvekn#gV1Di)+{W@Tl0g{;s-xXQVo6_;CxL7%r~^dAV&j9
zOrN;w>vC0XD@E5a)f>a1*?|ef;}RjEc9O|BR@$-%PB@~It1|bFjYDVr1QQSEG70ao
z^4Xv|EWf^;7Uq~IC$Fq;gu$j|1NL3l1N#nYnABu6@3jT|NehX%x-08^nugBXwsi(r
zxi{9qyZb?7ePP;dClY6KeT6d^P3zd?gmFUkba7-YKrh@2{0JWsXBY4lodc;W^Vd$P
z7XC|3T7&!0!QudJ!e%hrY7_V;XyyEsc@I4{wpX5MVVH8$)ODJhPFdyQL6X)zdlKdo
z>p506Z<%!hmQexBcL<#(p(g>*otX0qP+ePy);NGP-OA2L&U-V$jP_V^eUBiMX`O@+
zSD$w8?4*@aLL!KflhxhSwIkD=C!8tLvh&5kkH7L}my83s_I$)_ccxXN9~?lX0+5vB
z)OX<mQsE=<5s&a0Ba=dRJv=D3v^2iebkQjdfJx8cr~(7~gG@ZEH2|NUdM$<)Djg<{
z9j(MPdaM=}nCKs5(oNQ>o&rA41OQ7X86tZ4L0AX_hZLBYA7s)31oVzctxemjj$=QL
a2y?B4(&#iNFmYE<+5Z6oLhsrCegFVzR5|Ye

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