From a674190887a5e086f7a4be86d16397a356655be6 Mon Sep 17 00:00:00 2001
From: Jorge Sousa Pinto <jsp@di.uminho.pt>
Date: Wed, 17 Apr 2024 10:22:45 +0100
Subject: [PATCH] fixed some obsolete proof sessions

---
 .../mutualExclusionConcurrent/BakeryAtomic/why3session.xml    | 4 ++--
 examples/mutualExclusionToken/selfstab-ring/why3session.xml   | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/examples/mutualExclusionConcurrent/BakeryAtomic/why3session.xml b/examples/mutualExclusionConcurrent/BakeryAtomic/why3session.xml
index 7053474..bd39627 100644
--- a/examples/mutualExclusionConcurrent/BakeryAtomic/why3session.xml
+++ b/examples/mutualExclusionConcurrent/BakeryAtomic/why3session.xml
@@ -42,7 +42,7 @@
       <proof prover="1" timelimit="2000" memlimit="10000"><result status="valid" time="0.042073" steps="18777"/></proof>
       </goal>
       <goal name="a2&#39;vc.1.1.0.0.1" expl="postcondition" proved="true">
-      <proof prover="2"><result status="valid" time="0.040254" steps="730"/></proof>
+      <proof prover="1" timelimit="2000" memlimit="10000"><result status="valid" time="0.046505" steps="21138"/></proof>
       </goal>
       <goal name="a2&#39;vc.1.1.0.0.2" expl="postcondition" proved="true">
       <proof prover="1"><result status="valid" time="0.336939" steps="93037"/></proof>
@@ -62,7 +62,7 @@
       <proof prover="1" timelimit="2000" memlimit="10000"><result status="valid" time="0.040211" steps="17576"/></proof>
       </goal>
       <goal name="a2&#39;vc.1.1.1.0.1" expl="postcondition" proved="true">
-      <proof prover="2"><result status="valid" time="0.042947" steps="719"/></proof>
+      <proof prover="1" timelimit="2000" memlimit="10000"><result status="valid" time="0.050864" steps="21801"/></proof>
       </goal>
       <goal name="a2&#39;vc.1.1.1.0.2" expl="postcondition" proved="true">
       <proof prover="1"><result status="valid" time="0.159719" steps="58956"/></proof>
diff --git a/examples/mutualExclusionToken/selfstab-ring/why3session.xml b/examples/mutualExclusionToken/selfstab-ring/why3session.xml
index a0e850e..c8f5d85 100644
--- a/examples/mutualExclusionToken/selfstab-ring/why3session.xml
+++ b/examples/mutualExclusionToken/selfstab-ring/why3session.xml
@@ -32,7 +32,7 @@
     <proof prover="1" timelimit="2000" memlimit="10000"><result status="valid" time="0.629224" steps="24855"/></proof>
     </goal>
     <goal name="trans&#39;vc.0.0.4" expl="postcondition" proved="true">
-    <proof prover="1" timelimit="2000" memlimit="10000"><result status="valid" time="30.207880" steps="631027"/></proof>
+    <proof prover="0" memlimit="5000"><result status="valid" time="0.021162" steps="79453"/></proof>
     </goal>
     <goal name="trans&#39;vc.0.0.5" expl="postcondition" proved="true">
     <proof prover="0"><result status="valid" time="0.061491" steps="356952"/></proof>