From 15182b9602c44ca1c90e910b47f4f484f5a36fe8 Mon Sep 17 00:00:00 2001
From: Jorge Sousa Pinto <jsp@di.uminho.pt>
Date: Tue, 16 Apr 2024 18:37:34 +0100
Subject: [PATCH] updated selfstab-ring proofs

---
 .../selfstab-ring/why3session.xml              | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

diff --git a/examples/mutualExclusionToken/selfstab-ring/why3session.xml b/examples/mutualExclusionToken/selfstab-ring/why3session.xml
index 3ef5669..a0e850e 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="10000"/>
+<prover id="0" name="Z3" version="4.11.2" timelimit="2000" steplimit="0" memlimit="10000"/>
 <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"/>
@@ -20,28 +20,28 @@
    <goal name="trans&#39;vc.0.0" expl="VC for trans" proved="true">
    <transf name="split_all_full" proved="true" >
     <goal name="trans&#39;vc.0.0.0" expl="postcondition" proved="true">
-    <proof prover="1" timelimit="1"><result status="valid" time="0.684964" steps="32013"/></proof>
+    <proof prover="1" timelimit="2000" memlimit="10000"><result status="valid" time="0.677646" steps="32013"/></proof>
     </goal>
     <goal name="trans&#39;vc.0.0.1" expl="postcondition" proved="true">
-    <proof prover="1" timelimit="1"><result status="valid" time="0.006760" steps="8"/></proof>
+    <proof prover="1" timelimit="2000" memlimit="10000"><result status="valid" time="0.006451" steps="8"/></proof>
     </goal>
     <goal name="trans&#39;vc.0.0.2" expl="postcondition" proved="true">
-    <proof prover="0" timelimit="2000"><result status="valid" time="0.268627" steps="1869273"/></proof>
+    <proof prover="0"><result status="valid" time="0.249825" steps="1869273"/></proof>
     </goal>
     <goal name="trans&#39;vc.0.0.3" expl="postcondition" proved="true">
-    <proof prover="1" timelimit="1"><result status="valid" time="0.642479" steps="24855"/></proof>
+    <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="0" memlimit="1000"><result status="valid" time="0.019313" steps="79453"/></proof>
+    <proof prover="1" timelimit="2000" memlimit="10000"><result status="valid" time="30.207880" steps="631027"/></proof>
     </goal>
     <goal name="trans&#39;vc.0.0.5" expl="postcondition" proved="true">
-    <proof prover="0" memlimit="1000"><result status="valid" time="0.068119" steps="356952"/></proof>
+    <proof prover="0"><result status="valid" time="0.061491" steps="356952"/></proof>
     </goal>
     <goal name="trans&#39;vc.0.0.6" expl="postcondition" proved="true">
-    <proof prover="0" timelimit="2000"><result status="valid" time="3.269355" steps="36850612"/></proof>
+    <proof prover="0"><result status="valid" time="3.168135" steps="36850612"/></proof>
     </goal>
     <goal name="trans&#39;vc.0.0.7" expl="postcondition" proved="true">
-    <proof prover="1" timelimit="1"><result status="valid" time="0.826097" steps="18109"/></proof>
+    <proof prover="1" timelimit="2000" memlimit="10000"><result status="valid" time="0.931713" steps="18109"/></proof>
     </goal>
    </transf>
    </goal>