diff --git a/examples/mutualExclusionConcurrent/BakeryAtomic/why3session.xml b/examples/mutualExclusionConcurrent/BakeryAtomic/why3session.xml
index 1f64a09..b644310 100644
--- a/examples/mutualExclusionConcurrent/BakeryAtomic/why3session.xml
+++ b/examples/mutualExclusionConcurrent/BakeryAtomic/why3session.xml
@@ -6,7 +6,6 @@
 <prover id="1" name="CVC4" version="1.8" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="2" name="Alt-Ergo" version="2.4.2" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="3" name="Eprover" version="2.6" timelimit="1" steplimit="0" memlimit="1000"/>
-<prover id="4" name="Alt-Ergo" version="2.5.3" timelimit="1" steplimit="0" memlimit="1000"/>
 <file format="whyml" proved="true">
 <path name=".."/><path name="BakeryAtomic.mlw"/>
 <theory name="BakeryAtomic" proved="true">
@@ -44,7 +43,6 @@
    <transf name="split_vc" proved="true" >
     <goal name="a2&#39;vc.0.3.0" expl="postcondition" proved="true">
     <proof prover="1" timelimit="2000" memlimit="5000"><result status="valid" time="0.041926" steps="18798"/></proof>
-    <proof prover="2" timelimit="2000" memlimit="5000"><undone/></proof>
     </goal>
     <goal name="a2&#39;vc.0.3.1" expl="postcondition" proved="true">
     <proof prover="2"><result status="valid" time="0.051642" steps="737"/></proof>
@@ -72,7 +70,7 @@
     <proof prover="1"><result status="valid" time="0.156518" steps="59020"/></proof>
     </goal>
     <goal name="a2&#39;vc.0.5.3" expl="postcondition" proved="true">
-    <proof prover="4"><result status="valid" time="0.751849" steps="11805"/></proof>
+    <proof prover="2" timelimit="2000" memlimit="5000"><result status="valid" time="5.765631" steps="129190"/></proof>
     </goal>
    </transf>
    </goal>