From b5db1999453613418dd3fb33d50b0a0caa05c191 Mon Sep 17 00:00:00 2001
From: Raphael Rieu-Helft <raphael.rieu-helft@lri.fr>
Date: Fri, 26 Oct 2018 10:09:22 +0200
Subject: [PATCH] Update sessions

---
 .../multiprecision/compare/why3session.xml    | 40 +++++++++----------
 examples/multiprecision/util/why3session.xml  | 18 ++++-----
 2 files changed, 29 insertions(+), 29 deletions(-)

diff --git a/examples/multiprecision/compare/why3session.xml b/examples/multiprecision/compare/why3session.xml
index 181803b22..2a9c872d9 100644
--- a/examples/multiprecision/compare/why3session.xml
+++ b/examples/multiprecision/compare/why3session.xml
@@ -20,40 +20,40 @@
   <proof prover="5"><result status="valid" time="0.03" steps="11"/></proof>
   </goal>
   <goal name="VC wmpn_cmp.2" expl="assertion" proved="true">
-  <proof prover="5"><result status="valid" time="0.05" steps="40"/></proof>
+  <proof prover="5"><result status="valid" time="0.05" steps="39"/></proof>
   </goal>
   <goal name="VC wmpn_cmp.3" expl="precondition" proved="true">
-  <proof prover="5"><result status="valid" time="0.03" steps="47"/></proof>
+  <proof prover="5"><result status="valid" time="0.03" steps="46"/></proof>
   </goal>
   <goal name="VC wmpn_cmp.4" expl="integer overflow" proved="true">
-  <proof prover="5"><result status="valid" time="0.04" steps="26"/></proof>
+  <proof prover="5"><result status="valid" time="0.04" steps="25"/></proof>
   </goal>
   <goal name="VC wmpn_cmp.5" expl="assertion" proved="true">
-  <proof prover="5"><result status="valid" time="0.03" steps="16"/></proof>
+  <proof prover="5"><result status="valid" time="0.03" steps="15"/></proof>
   </goal>
   <goal name="VC wmpn_cmp.6" expl="precondition" proved="true">
-  <proof prover="5"><result status="valid" time="0.03" steps="28"/></proof>
+  <proof prover="5"><result status="valid" time="0.03" steps="27"/></proof>
   </goal>
   <goal name="VC wmpn_cmp.7" expl="precondition" proved="true">
-  <proof prover="5"><result status="valid" time="0.06" steps="28"/></proof>
+  <proof prover="5"><result status="valid" time="0.06" steps="27"/></proof>
   </goal>
   <goal name="VC wmpn_cmp.8" expl="precondition" proved="true">
   <proof prover="3"><result status="valid" time="0.02"/></proof>
-  <proof prover="5"><result status="valid" time="0.05" steps="20"/></proof>
+  <proof prover="5"><result status="valid" time="0.05" steps="19"/></proof>
   </goal>
   <goal name="VC wmpn_cmp.9" expl="precondition" proved="true">
-  <proof prover="5"><result status="valid" time="0.06" steps="21"/></proof>
+  <proof prover="5"><result status="valid" time="0.06" steps="20"/></proof>
   </goal>
   <goal name="VC wmpn_cmp.10" expl="assertion" proved="true">
-  <proof prover="5"><result status="valid" time="0.04" steps="51"/></proof>
+  <proof prover="5"><result status="valid" time="0.04" steps="50"/></proof>
   </goal>
   <goal name="VC wmpn_cmp.11" expl="precondition" proved="true">
   <proof prover="3"><result status="valid" time="0.02"/></proof>
-  <proof prover="5"><result status="valid" time="0.05" steps="23"/></proof>
+  <proof prover="5"><result status="valid" time="0.05" steps="22"/></proof>
   </goal>
   <goal name="VC wmpn_cmp.12" expl="precondition" proved="true">
   <proof prover="3"><result status="valid" time="0.02"/></proof>
-  <proof prover="5"><result status="valid" time="0.07" steps="24"/></proof>
+  <proof prover="5"><result status="valid" time="0.07" steps="23"/></proof>
   </goal>
   <goal name="VC wmpn_cmp.13" expl="precondition" proved="true">
   <proof prover="1"><result status="valid" time="0.06"/></proof>
@@ -61,7 +61,7 @@
   <goal name="VC wmpn_cmp.14" expl="assertion" proved="true">
   <transf name="inline_goal" proved="true" >
    <goal name="VC wmpn_cmp.14.0" expl="assertion" proved="true">
-   <proof prover="5"><result status="valid" time="0.04" steps="36"/></proof>
+   <proof prover="5"><result status="valid" time="0.04" steps="35"/></proof>
    </goal>
   </transf>
   </goal>
@@ -76,11 +76,11 @@
   </transf>
   </goal>
   <goal name="VC wmpn_cmp.16" expl="postcondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.16"/></proof>
+  <proof prover="3"><result status="valid" time="0.03"/></proof>
   </goal>
   <goal name="VC wmpn_cmp.17" expl="assertion" proved="true">
   <proof prover="3"><result status="valid" time="0.03"/></proof>
-  <proof prover="5"><result status="valid" time="0.05" steps="26"/></proof>
+  <proof prover="5"><result status="valid" time="0.05" steps="25"/></proof>
   </goal>
   <goal name="VC wmpn_cmp.18" expl="precondition" proved="true">
   <proof prover="1"><result status="valid" time="0.10"/></proof>
@@ -88,7 +88,7 @@
   <goal name="VC wmpn_cmp.19" expl="assertion" proved="true">
   <transf name="inline_goal" proved="true" >
    <goal name="VC wmpn_cmp.19.0" expl="assertion" proved="true">
-   <proof prover="5"><result status="valid" time="0.04" steps="37"/></proof>
+   <proof prover="5"><result status="valid" time="0.04" steps="36"/></proof>
    </goal>
   </transf>
   </goal>
@@ -103,20 +103,20 @@
   </transf>
   </goal>
   <goal name="VC wmpn_cmp.21" expl="postcondition" proved="true">
-  <proof prover="3"><result status="valid" time="0.03"/></proof>
+  <proof prover="0"><result status="valid" time="0.16"/></proof>
   </goal>
   <goal name="VC wmpn_cmp.22" expl="loop variant decrease" proved="true">
   <proof prover="3"><result status="valid" time="0.03"/></proof>
-  <proof prover="5"><result status="valid" time="0.03" steps="20"/></proof>
+  <proof prover="5"><result status="valid" time="0.03" steps="19"/></proof>
   </goal>
   <goal name="VC wmpn_cmp.23" expl="loop invariant preservation" proved="true">
-  <proof prover="5"><result status="valid" time="0.04" steps="20"/></proof>
+  <proof prover="5"><result status="valid" time="0.04" steps="19"/></proof>
   </goal>
   <goal name="VC wmpn_cmp.24" expl="loop invariant preservation" proved="true">
-  <proof prover="5"><result status="valid" time="0.03" steps="44"/></proof>
+  <proof prover="5"><result status="valid" time="0.03" steps="43"/></proof>
   </goal>
   <goal name="VC wmpn_cmp.25" expl="precondition" proved="true">
-  <proof prover="5"><result status="valid" time="0.04" steps="44"/></proof>
+  <proof prover="5"><result status="valid" time="0.04" steps="43"/></proof>
   </goal>
   <goal name="VC wmpn_cmp.26" expl="postcondition" proved="true">
   <proof prover="3"><result status="valid" time="0.03"/></proof>
diff --git a/examples/multiprecision/util/why3session.xml b/examples/multiprecision/util/why3session.xml
index 4357be82d..775961db5 100644
--- a/examples/multiprecision/util/why3session.xml
+++ b/examples/multiprecision/util/why3session.xml
@@ -72,13 +72,13 @@
   <proof prover="1"><result status="valid" time="0.04"/></proof>
   </goal>
   <goal name="VC wmpn_copyi.20" expl="loop invariant preservation" proved="true">
-  <proof prover="0"><result status="valid" time="0.06" steps="212"/></proof>
+  <proof prover="0"><result status="valid" time="0.06" steps="198"/></proof>
   </goal>
   <goal name="VC wmpn_copyi.21" expl="loop invariant preservation" proved="true">
   <proof prover="1"><result status="valid" time="0.02"/></proof>
   </goal>
   <goal name="VC wmpn_copyi.22" expl="loop invariant preservation" proved="true">
-  <proof prover="0"><result status="valid" time="0.05" steps="98"/></proof>
+  <proof prover="0"><result status="valid" time="0.05" steps="96"/></proof>
   </goal>
   <goal name="VC wmpn_copyi.23" expl="loop invariant preservation" proved="true">
   <proof prover="1"><result status="valid" time="0.03"/></proof>
@@ -99,7 +99,7 @@
   <proof prover="1"><result status="valid" time="0.02"/></proof>
   </goal>
   <goal name="VC wmpn_copyi.29" expl="loop invariant preservation" proved="true">
-  <proof prover="0"><result status="valid" time="0.02" steps="106"/></proof>
+  <proof prover="0"><result status="valid" time="0.02" steps="104"/></proof>
   </goal>
   <goal name="VC wmpn_copyi.30" expl="postcondition" proved="true">
   <proof prover="1"><result status="valid" time="0.02"/></proof>
@@ -121,10 +121,10 @@
   <proof prover="1"><result status="valid" time="0.02"/></proof>
   </goal>
   <goal name="VC wmpn_zero_p.3" expl="assertion" proved="true">
-  <proof prover="0"><result status="valid" time="0.01" steps="14"/></proof>
+  <proof prover="0"><result status="valid" time="0.01" steps="13"/></proof>
   </goal>
   <goal name="VC wmpn_zero_p.4" expl="precondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.01" steps="22"/></proof>
+  <proof prover="0"><result status="valid" time="0.01" steps="21"/></proof>
   </goal>
   <goal name="VC wmpn_zero_p.5" expl="precondition" proved="true">
   <proof prover="1"><result status="valid" time="0.02"/></proof>
@@ -136,7 +136,7 @@
   <proof prover="1"><result status="valid" time="0.02"/></proof>
   </goal>
   <goal name="VC wmpn_zero_p.8" expl="postcondition" proved="true">
-  <proof prover="2"><result status="valid" time="0.03" steps="47"/></proof>
+  <proof prover="2"><result status="valid" time="0.03" steps="45"/></proof>
   </goal>
   <goal name="VC wmpn_zero_p.9" expl="assertion" proved="true">
   <proof prover="1"><result status="valid" time="0.01"/></proof>
@@ -148,7 +148,7 @@
   <proof prover="1"><result status="valid" time="0.02"/></proof>
   </goal>
   <goal name="VC wmpn_zero_p.12" expl="loop invariant preservation" proved="true">
-  <proof prover="0"><result status="valid" time="0.01" steps="36"/></proof>
+  <proof prover="0"><result status="valid" time="0.01" steps="35"/></proof>
   </goal>
   <goal name="VC wmpn_zero_p.13" expl="postcondition" proved="true">
   <proof prover="1"><result status="valid" time="0.01"/></proof>
@@ -185,10 +185,10 @@
   <proof prover="1"><result status="valid" time="0.03"/></proof>
   </goal>
   <goal name="VC wmpn_zero.8" expl="loop invariant preservation" proved="true">
-  <proof prover="0"><result status="valid" time="0.10" steps="106"/></proof>
+  <proof prover="0"><result status="valid" time="0.10" steps="102"/></proof>
   </goal>
   <goal name="VC wmpn_zero.9" expl="loop invariant preservation" proved="true">
-  <proof prover="0"><result status="valid" time="0.02" steps="50"/></proof>
+  <proof prover="0"><result status="valid" time="0.02" steps="49"/></proof>
   </goal>
   <goal name="VC wmpn_zero.10" expl="postcondition" proved="true">
   <proof prover="1"><result status="valid" time="0.03"/></proof>
-- 
GitLab