more sessions fixed after change of shape version

288df6db · MARCHE Claude · 7ac40586 · 288df6db · 288df6db · 288df6db
Commit 288df6db authored Jul 17, 2013 by MARCHE Claude
95 changed files
--- a/CHANGES
+++ b/CHANGES
 * marks an incompatible change

+  o shape algorithm modified (see VSTTE'13 paper) but should be
+    backward compatible
  * [emacs] why.el renamed to why3.el
-  * [GTK sourceview] why.lang renamed to why3.lang
+  o [GTK sourceview] why.lang renamed to why3.lang

 version 0.81, March 25, 2013
 ============================

--- a/ROADMAP
+++ b/ROADMAP
@@ -74,8 +74,14 @@

 ==================== Roadmap for release 0.82 ========================

+Scheduled for August 2013 ?
+
 == New Features to announce ==

+* improved shape mecanism for session updates (see VSTTE'13 paper).
+  Compatibility with session files from version 0.81 and earlier is
+  assured.
+
 == Final preparation ==

 * faire une passe sur le BTS

--- a/examples/add_list/why3session.xml
+++ b/examples/add_list/why3session.xml
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="2">
+<why3session shape_version="3">
 <prover
  id="0"
  name="Alt-Ergo"
@@ -38,7 +38,7 @@
    sum="98a5545af1ab7e2f135821ad2fe70910"
    proved="true"
    expanded="true"
-    shape="CV0aNilainfix =c0.0aadd_realV0Aainfix =c0aadd_intV0aConsVVCV1aIntegerVainfix =V4aadd_realV0Aainfix =ainfix +V5V3aadd_intV0aRealVainfix =ainfix +.V6V4aadd_realV0Aainfix =V3aadd_intV0Iainfix =V4aadd_realV2Aainfix =V3aadd_intV2FF">
+    shape="Cainfix =c0.0aadd_realV0Aainfix =c0aadd_intV0aNilCainfix =V4aadd_realV0Aainfix =ainfix +V5V3aadd_intV0aIntegerVainfix =ainfix +.V6V4aadd_realV0Aainfix =V3aadd_intV0aRealVV1Iainfix =V4aadd_realV2Aainfix =V3aadd_intV2FaConsVVV0F">
    <label
     name="expl:VC for sum"/>
    <proof
@@ -109,7 +109,7 @@
    sum="113394ababdb929cb6daae79f2cf228e"
    proved="true"
    expanded="true"
-    shape="itCV1aNilainfix =V2aadd_realV0Aainfix =V3aadd_intV0aConsaIntegerVVainfix =ainfix +.V2aadd_realV7aadd_realV0Aainfix =ainfix +V6aadd_intV7aadd_intV0Iainfix =V7V5FIainfix =V6ainfix +V3V4FaConsaRealVVainfix =ainfix +.V10aadd_realV11aadd_realV0Aainfix =ainfix +V3aadd_intV11aadd_intV0Iainfix =V11V9FIainfix =V10ainfix +.V2V8FfIainfix =ainfix +.V2aadd_realV1aadd_realV0Aainfix =ainfix +V3aadd_intV1aadd_intV0FAainfix =ainfix +.c0.0aadd_realV0aadd_realV0Aainfix =ainfix +c0aadd_intV0aadd_intV0F">
+    shape="ifCainfix =V2aadd_realV0Aainfix =V3aadd_intV0aNilainfix =ainfix +.V2aadd_realV7aadd_realV0Aainfix =ainfix +V6aadd_intV7aadd_intV0Iainfix =V7V5FIainfix =V6ainfix +V3V4FaConsaIntegerVVainfix =ainfix +.V10aadd_realV11aadd_realV0Aainfix =ainfix +V3aadd_intV11aadd_intV0Iainfix =V11V9FIainfix =V10ainfix +.V2V8FaConsaRealVVV1tIainfix =ainfix +.V2aadd_realV1aadd_realV0Aainfix =ainfix +V3aadd_intV1aadd_intV0FAainfix =ainfix +.c0.0aadd_realV0aadd_realV0Aainfix =ainfix +c0aadd_intV0aadd_intV0F">
    <label
     name="expl:VC for sum"/>
    <proof

--- a/examples/algo63/why3session.xml
+++ b/examples/algo63/why3session.xml
--- a/examples/algo64/why3session.xml
+++ b/examples/algo64/why3session.xml
--- a/examples/algo65/why3session.xml
+++ b/examples/algo65/why3session.xml
--- a/examples/arm/why3session.xml
+++ b/examples/arm/why3session.xml
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="2">
+<why3session shape_version="3">
 <prover
  id="0"
  name="Alt-Ergo"
@@ -27,7 +27,7 @@
    sum="5677a170e9f6faf600b34c4281eebd63"
    proved="false"
    expanded="false"
-    shape="iainfix &lt;=V5c10iainfix &lt;agetV13V11agetV13V15ainfix &lt;V21V11Aainfix &lt;=c0V11Aainfix &lt;=ainfix *c2V16ainfix +ainfix *ainfix -V5c2ainfix -V5c1ainfix *c2ainfix -V5V21Aainvamk arrayV0V20Aainfix &lt;=V21V5Aainfix &lt;=c1V21Iainfix =V21ainfix -V11c1FIainfix =V20asetV18V19agetV13V11Aainfix &lt;=c0V0FAainfix &lt;V19V0Aainfix &lt;=c0V19Lainfix -V11c1Iainfix =V18asetV13V11agetV13V17Aainfix &lt;=c0V0FAainfix &lt;V11V0Aainfix &lt;=c0V11Aainfix &lt;V17V0Aainfix &lt;=c0V17Lainfix -V11c1Aainfix &lt;V11V0Aainfix &lt;=c0V11Iainfix =V16ainfix +V12c1Fainfix &lt;ainfix -c10V22ainfix -c10V5Aainfix &lt;=c0ainfix -c10V5Aainfix &lt;=ainfix *c2V12ainfix *ainfix -V22c2ainfix -V22c1Aainfix =V10ainfix -V22c2AainvV14Aainfix &lt;=V22c11Aainfix &lt;=c2V22Iainfix =V22ainfix +V5c1FAainfix &lt;V11V0Aainfix &lt;=c0V11Aainfix &lt;V15V0Aainfix &lt;=c0V15Aainfix &lt;=c0V0Lainfix -V11c1Iainfix &lt;=ainfix *c2V12ainfix +ainfix *ainfix -V5c2ainfix -V5c1ainfix *c2ainfix -V5V11AainvV14Aainfix &lt;=V11V5Aainfix &lt;=c1V11Lamk arrayV0V13FAainfix &lt;=ainfix *c2V6ainfix +ainfix *ainfix -V5c2ainfix -V5c1ainfix *c2ainfix -V5V5AainvV9Aainfix &lt;=V5V5Aainfix &lt;=c1V5Iainfix =V10ainfix +V7c1Fainfix &lt;=V6c45Aainfix =V7c9Aainfix &lt;=c0V0Iainfix &lt;=ainfix *c2V6ainfix *ainfix -V5c2ainfix -V5c1Aainfix =V7ainfix -V5c2AainvV9Aainfix &lt;=V5c11Aainfix &lt;=c2V5Lamk arrayV0V8FAainfix &lt;=ainfix *c2V1ainfix *ainfix -c2c2ainfix -c2c1Aainfix =V2ainfix -c2c2AainvV4Aainfix &lt;=c2c11Aainfix &lt;=c2c2Iainfix =V1c0Aainfix =V2c0AainvV4Aainfix &lt;=c0V0Lamk arrayV0V3FF">
+    shape="iainfix &lt;=V6c45Aainfix =V7c9Aainfix &lt;=c0V0iainfix &lt;ainfix -c10V16ainfix -c10V5Aainfix &lt;=c0ainfix -c10V5Aainfix &lt;=ainfix *c2V12ainfix *ainfix -V16c2ainfix -V16c1Aainfix =V10ainfix -V16c2AainvV14Aainfix &lt;=V16c11Aainfix &lt;=c2V16Iainfix =V16ainfix +V5c1Fainfix &lt;V22V11Aainfix &lt;=c0V11Aainfix &lt;=ainfix *c2V17ainfix +ainfix *ainfix -V5c2ainfix -V5c1ainfix *c2ainfix -V5V22Aainvamk arrayV0V21Aainfix &lt;=V22V5Aainfix &lt;=c1V22Iainfix =V22ainfix -V11c1FIainfix =V21asetV19V20agetV13V11Aainfix &lt;=c0V0FAainfix &lt;V20V0Aainfix &lt;=c0V20Lainfix -V11c1Iainfix =V19asetV13V11agetV13V18Aainfix &lt;=c0V0FAainfix &lt;V11V0Aainfix &lt;=c0V11Aainfix &lt;V18V0Aainfix &lt;=c0V18Lainfix -V11c1Aainfix &lt;V11V0Aainfix &lt;=c0V11Iainfix =V17ainfix +V12c1Fainfix &lt;agetV13V11agetV13V15Aainfix &lt;V11V0Aainfix &lt;=c0V11Aainfix &lt;V15V0Aainfix &lt;=c0V15Aainfix &lt;=c0V0Lainfix -V11c1Iainfix &lt;=ainfix *c2V12ainfix +ainfix *ainfix -V5c2ainfix -V5c1ainfix *c2ainfix -V5V11AainvV14Aainfix &lt;=V11V5Aainfix &lt;=c1V11Lamk arrayV0V13FAainfix &lt;=ainfix *c2V6ainfix +ainfix *ainfix -V5c2ainfix -V5c1ainfix *c2ainfix -V5V5AainvV9Aainfix &lt;=V5V5Aainfix &lt;=c1V5Iainfix =V10ainfix +V7c1Fainfix &lt;=V5c10Iainfix &lt;=ainfix *c2V6ainfix *ainfix -V5c2ainfix -V5c1Aainfix =V7ainfix -V5c2AainvV9Aainfix &lt;=V5c11Aainfix &lt;=c2V5Lamk arrayV0V8FAainfix &lt;=ainfix *c2V1ainfix *ainfix -c2c2ainfix -c2c1Aainfix =V2ainfix -c2c2AainvV4Aainfix &lt;=c2c11Aainfix &lt;=c2c2Iainfix =V1c0Aainfix =V2c0AainvV4Aainfix &lt;=c0V0Lamk arrayV0V3FF">
    <label
     name="expl:VC for insertion_sort"/>
   </goal>

--- a/examples/assigning_meanings_to_programs/why3session.xml
+++ b/examples/assigning_meanings_to_programs/why3session.xml
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="2">
+<why3session shape_version="3">
 <prover
  id="0"
  name="Alt-Ergo"
@@ -27,7 +27,7 @@
    sum="17bf6dcb57a723007ce152bd4c333f35"
    proved="true"
    expanded="true"
-    shape="iainfix &lt;=V4V1ainfix &lt;ainfix -V1V6ainfix -V1V4Aainfix &lt;=c0ainfix -V1V4Aainfix =V5asumV2c1V6Aainfix &lt;=V6ainfix +V1c1Aainfix &lt;=c1V6Iainfix =V6ainfix +V4c1FIainfix =V5ainfix +V3agetV2V4FAainfix &lt;V4V0Aainfix &lt;=c0V4ainfix =V3asumV2c1ainfix +V1c1Iainfix =V3asumV2c1V4Aainfix &lt;=V4ainfix +V1c1Aainfix &lt;=c1V4FAainfix =c0asumV2c1c1Aainfix &lt;=c1ainfix +V1c1Aainfix &lt;=c1c1Iainfix &lt;V1V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
+    shape="iainfix =V3asumV2c1ainfix +V1c1ainfix &lt;ainfix -V1V6ainfix -V1V4Aainfix &lt;=c0ainfix -V1V4Aainfix =V5asumV2c1V6Aainfix &lt;=V6ainfix +V1c1Aainfix &lt;=c1V6Iainfix =V6ainfix +V4c1FIainfix =V5ainfix +V3agetV2V4FAainfix &lt;V4V0Aainfix &lt;=c0V4ainfix &lt;=V4V1Iainfix =V3asumV2c1V4Aainfix &lt;=V4ainfix +V1c1Aainfix &lt;=c1V4FAainfix =c0asumV2c1c1Aainfix &lt;=c1ainfix +V1c1Aainfix &lt;=c1c1Iainfix &lt;V1V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
    <label
     name="expl:VC for sum"/>
    <proof
@@ -54,7 +54,7 @@
    sum="4177aab49b97cc922d533db26f687096"
    proved="true"
    expanded="true"
-    shape="iainfix &gt;=V2V1ainfix &lt;V4V2Aainfix &lt;=c0V2Aainfix =V0ainfix +ainfix *V5V1V4Aainfix &lt;=c0V4Iainfix =V5ainfix +V3c1FIainfix =V4ainfix -V2V1Fainfix =V0ainfix +ainfix *V3V1V2Aainfix &lt;V2V1Aainfix &lt;=c0V2Iainfix =V0ainfix +ainfix *V3V1V2Aainfix &lt;=c0V2FAainfix =V0ainfix +ainfix *c0V1V0Aainfix &lt;=c0V0Iainfix &lt;c0V1Aainfix &lt;=c0V0F">
+    shape="iainfix =V0ainfix +ainfix *V3V1V2Aainfix &lt;V2V1Aainfix &lt;=c0V2ainfix &lt;V4V2Aainfix &lt;=c0V2Aainfix =V0ainfix +ainfix *V5V1V4Aainfix &lt;=c0V4Iainfix =V5ainfix +V3c1FIainfix =V4ainfix -V2V1Fainfix &gt;=V2V1Iainfix =V0ainfix +ainfix *V3V1V2Aainfix &lt;=c0V2FAainfix =V0ainfix +ainfix *c0V1V0Aainfix &lt;=c0V0Iainfix &lt;c0V1Aainfix &lt;=c0V0F">
    <label
     name="expl:VC for division"/>
    <proof

--- a/examples/binary_search/why3session.xml
+++ b/examples/binary_search/why3session.xml
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="2">
+<why3session shape_version="3">
 <prover
  id="0"
  name="Alt-Ergo"
@@ -27,7 +27,7 @@
    sum="58d7f9baa3142a5765eb3ebc3538afbb"
    proved="true"
    expanded="true"
-    shape="iainfix &lt;=V4V3iainfix &lt;agetV2V5V1ainfix &lt;ainfix -V3V6ainfix -V3V4Aainfix &lt;=c0ainfix -V3V4Aainfix &lt;=V7V3Aainfix &lt;=V6V7Iainfix =agetV2V7V1Iainfix &lt;V7V0Aainfix &lt;=c0V7FAainfix &lt;V3V0Aainfix &lt;=c0V6Iainfix =V6ainfix +V5c1Fiainfix &gt;agetV2V5V1ainfix &lt;ainfix -V8V4ainfix -V3V4Aainfix &lt;=c0ainfix -V3V4Aainfix &lt;=V9V8Aainfix &lt;=V4V9Iainfix =agetV2V9V1Iainfix &lt;V9V0Aainfix &lt;=c0V9FAainfix &lt;V8V0Aainfix &lt;=c0V4Iainfix =V8ainfix -V5c1Fainfix =agetV2V5V1Aainfix &lt;V5V0Aainfix &lt;=c0V5Aainfix &lt;V5V0Aainfix &lt;=c0V5Aainfix &lt;V5V0Aainfix &lt;=c0V5Aainfix &lt;=V5V3Aainfix &lt;=V4V5Lainfix +V4adivainfix -V3V4c2ainfix =agetV2V10V1NIainfix &lt;V10V0Aainfix &lt;=c0V10FIainfix &lt;=V11V3Aainfix &lt;=V4V11Iainfix =agetV2V11V1Iainfix &lt;V11V0Aainfix &lt;=c0V11FAainfix &lt;V3V0Aainfix &lt;=c0V4FAainfix &lt;=V12ainfix -V0c1Aainfix &lt;=c0V12Iainfix =agetV2V12V1Iainfix &lt;V12V0Aainfix &lt;=c0V12FAainfix &lt;ainfix -V0c1V0Aainfix &lt;=c0c0Iainfix &lt;=agetV2V13agetV2V14Iainfix &lt;V14V0Aainfix &lt;=V13V14Aainfix &lt;=c0V13FAainfix &lt;=c0V0FF">
+    shape="iNainfix =agetV2V5V1Iainfix &lt;V5V0Aainfix &lt;=c0V5Fiiainfix =agetV2V6V1Aainfix &lt;V6V0Aainfix &lt;=c0V6ainfix &lt;ainfix -V7V4ainfix -V3V4Aainfix &lt;=c0ainfix -V3V4Aainfix &lt;=V8V7Aainfix &lt;=V4V8Iainfix =agetV2V8V1Iainfix &lt;V8V0Aainfix &lt;=c0V8FAainfix &lt;V7V0Aainfix &lt;=c0V4Iainfix =V7ainfix -V6c1Fainfix &gt;agetV2V6V1Aainfix &lt;V6V0Aainfix &lt;=c0V6ainfix &lt;ainfix -V3V9ainfix -V3V4Aainfix &lt;=c0ainfix -V3V4Aainfix &lt;=V10V3Aainfix &lt;=V9V10Iainfix =agetV2V10V1Iainfix &lt;V10V0Aainfix &lt;=c0V10FAainfix &lt;V3V0Aainfix &lt;=c0V9Iainfix =V9ainfix +V6c1Fainfix &lt;agetV2V6V1Aainfix &lt;V6V0Aainfix &lt;=c0V6Aainfix &lt;=V6V3Aainfix &lt;=V4V6Lainfix +V4adivainfix -V3V4c2ainfix &lt;=V4V3Iainfix &lt;=V11V3Aainfix &lt;=V4V11Iainfix =agetV2V11V1Iainfix &lt;V11V0Aainfix &lt;=c0V11FAainfix &lt;V3V0Aainfix &lt;=c0V4FAainfix &lt;=V12ainfix -V0c1Aainfix &lt;=c0V12Iainfix =agetV2V12V1Iainfix &lt;V12V0Aainfix &lt;=c0V12FAainfix &lt;ainfix -V0c1V0Aainfix &lt;=c0c0Iainfix &lt;=agetV2V13agetV2V14Iainfix &lt;V14V0Aainfix &lt;=V13V14Aainfix &lt;=c0V13FAainfix &lt;=c0V0FF">
    <label
     name="expl:VC for binary_search"/>
    <proof
@@ -62,7 +62,7 @@
    sum="5954021440d95809176c18fd90076bd1"
    proved="true"
    expanded="true"
-    shape="iainfix &lt;=V4V3iainfix &lt;agetV2V5V1ainfix &lt;ainfix -V3V6ainfix -V3V4Aainfix &lt;=c0ainfix -V3V4Aainfix &lt;=V7V3Aainfix &lt;=V6V7Iainfix =agetV2V7V1Iainfix &lt;V7V0Aainfix &lt;=c0V7FAainfix &lt;V3V0Aainfix &lt;=c0V6Iainfix =V6ainfix +V5c1Fiainfix &gt;agetV2V5V1ainfix &lt;ainfix -V8V4ainfix -V3V4Aainfix &lt;=c0ainfix -V3V4Aainfix &lt;=V9V8Aainfix &lt;=V4V9Iainfix =agetV2V9V1Iainfix &lt;V9V0Aainfix &lt;=c0V9FAainfix &lt;V8V0Aainfix &lt;=c0V4Iainfix =V8ainfix -V5c1Fainfix =agetV2V5V1Aainfix &lt;V5V0Aainfix &lt;=c0V5Aainfix &lt;V5V0Aainfix &lt;=c0V5Aainfix &lt;V5V0Aainfix &lt;=c0V5Iainfix &lt;=V5V3Aainfix &lt;=V4V5FAainfix &lt;=V4V3ainfix =agetV2V10V1NIainfix &lt;V10V0Aainfix &lt;=c0V10FIainfix &lt;=V11V3Aainfix &lt;=V4V11Iainfix =agetV2V11V1Iainfix &lt;V11V0Aainfix &lt;=c0V11FAainfix &lt;V3V0Aainfix &lt;=c0V4FAainfix &lt;=V12ainfix -V0c1Aainfix &lt;=c0V12Iainfix =agetV2V12V1Iainfix &lt;V12V0Aainfix &lt;=c0V12FAainfix &lt;ainfix -V0c1V0Aainfix &lt;=c0c0Iainfix &lt;=agetV2V13agetV2V14Iainfix &lt;V14V0Aainfix &lt;=V13V14Aainfix &lt;=c0V13FAainfix &lt;=c0V0FF">
+    shape="iNainfix =agetV2V5V1Iainfix &lt;V5V0Aainfix &lt;=c0V5Fiiainfix =agetV2V6V1Aainfix &lt;V6V0Aainfix &lt;=c0V6ainfix &lt;ainfix -V7V4ainfix -V3V4Aainfix &lt;=c0ainfix -V3V4Aainfix &lt;=V8V7Aainfix &lt;=V4V8Iainfix =agetV2V8V1Iainfix &lt;V8V0Aainfix &lt;=c0V8FAainfix &lt;V7V0Aainfix &lt;=c0V4Iainfix =V7ainfix -V6c1Fainfix &gt;agetV2V6V1Aainfix &lt;V6V0Aainfix &lt;=c0V6ainfix &lt;ainfix -V3V9ainfix -V3V4Aainfix &lt;=c0ainfix -V3V4Aainfix &lt;=V10V3Aainfix &lt;=V9V10Iainfix =agetV2V10V1Iainfix &lt;V10V0Aainfix &lt;=c0V10FAainfix &lt;V3V0Aainfix &lt;=c0V9Iainfix =V9ainfix +V6c1Fainfix &lt;agetV2V6V1Aainfix &lt;V6V0Aainfix &lt;=c0V6Iainfix &lt;=V6V3Aainfix &lt;=V4V6FAainfix &lt;=V4V3ainfix &lt;=V4V3Iainfix &lt;=V11V3Aainfix &lt;=V4V11Iainfix =agetV2V11V1Iainfix &lt;V11V0Aainfix &lt;=c0V11FAainfix &lt;V3V0Aainfix &lt;=c0V4FAainfix &lt;=V12ainfix -V0c1Aainfix &lt;=c0V12Iainfix =agetV2V12V1Iainfix &lt;V12V0Aainfix &lt;=c0V12FAainfix &lt;ainfix -V0c1V0Aainfix &lt;=c0c0Iainfix &lt;=agetV2V13agetV2V14Iainfix &lt;V14V0Aainfix &lt;=V13V14Aainfix &lt;=c0V13FAainfix &lt;=c0V0FF">
    <label
     name="expl:VC for binary_search"/>
    <proof
@@ -89,7 +89,7 @@
    sum="c1b8b598df35a36bdae0936e15ba8379"
    proved="true"
    expanded="true"
-    shape="iainfix &lt;=V4V3iainfix &lt;agetV2V6V1ainfix &lt;ainfix -V3V7ainfix -V3V4Aainfix &lt;=c0ainfix -V3V4Aainfix &lt;=V8V3Aainfix &lt;=V7V8Iainfix =agetV2V8V1Iainfix &lt;V8V0Aainfix &lt;=c0V8FAainfix &lt;V3V0Aainfix &lt;=c0V7Iainfix =V7ainfix +V6c1FAainfix &lt;=ainfix +V6c1amax_intAainfix &lt;=amin_intainfix +V6c1iainfix &gt;agetV2V6V1ainfix &lt;ainfix -V9V4ainfix -V3V4Aainfix &lt;=c0ainfix -V3V4Aainfix &lt;=V10V9Aainfix &lt;=V4V10Iainfix =agetV2V10V1Iainfix &lt;V10V0Aainfix &lt;=c0V10FAainfix &lt;V9V0Aainfix &lt;=c0V4Iainfix =V9ainfix -V6c1FAainfix &lt;=ainfix -V6c1amax_intAainfix &lt;=amin_intainfix -V6c1ainfix =agetV2V6V1Aainfix &lt;V6V0Aainfix &lt;=c0V6Aainfix &lt;V6V0Aainfix &lt;=c0V6Aainfix &lt;V6V0Aainfix &lt;=c0V6Aainfix &lt;=V6V3Aainfix &lt;=V4V6Lainfix +V4V5Aainfix &lt;=ainfix +V4V5amax_intAainfix &lt;=amin_intainfix +V4V5Ladivainfix -V3V4c2Aainfix &lt;=ainfix -V3V4amax_intAainfix &lt;=amin_intainfix -V3V4ainfix =agetV2V11V1NIainfix &lt;V11V0Aainfix &lt;=c0V11FIainfix &lt;=V12V3Aainfix &lt;=V4V12Iainfix =agetV2V12V1Iainfix &lt;V12V0Aainfix &lt;=c0V12FAainfix &lt;V3V0Aainfix &lt;=c0V4FAainfix &lt;=V13ainfix -V0c1Aainfix &lt;=c0V13Iainfix =agetV2V13V1Iainfix &lt;V13V0Aainfix &lt;=c0V13FAainfix &lt;ainfix -V0c1V0Aainfix &lt;=c0c0Aainfix &lt;=ainfix -V0c1amax_intAainfix &lt;=amin_intainfix -V0c1Iainfix &lt;=agetV2V14agetV2V15Iainfix &lt;V15V0Aainfix &lt;=V14V15Aainfix &lt;=c0V14FAainfix &lt;=V0amax_intAainfix &lt;=c0V0FF">
+    shape="iNainfix =agetV2V5V1Iainfix &lt;V5V0Aainfix &lt;=c0V5Fiiainfix =agetV2V7V1Aainfix &lt;V7V0Aainfix &lt;=c0V7ainfix &lt;ainfix -V8V4ainfix -V3V4Aainfix &lt;=c0ainfix -V3V4Aainfix &lt;=V9V8Aainfix &lt;=V4V9Iainfix =agetV2V9V1Iainfix &lt;V9V0Aainfix &lt;=c0V9FAainfix &lt;V8V0Aainfix &lt;=c0V4Iainfix =V8ainfix -V7c1FAainfix &lt;=ainfix -V7c1amax_intAainfix &lt;=amin_intainfix -V7c1ainfix &gt;agetV2V7V1Aainfix &lt;V7V0Aainfix &lt;=c0V7ainfix &lt;ainfix -V3V10ainfix -V3V4Aainfix &lt;=c0ainfix -V3V4Aainfix &lt;=V11V3Aainfix &lt;=V10V11Iainfix =agetV2V11V1Iainfix &lt;V11V0Aainfix &lt;=c0V11FAainfix &lt;V3V0Aainfix &lt;=c0V10Iainfix =V10ainfix +V7c1FAainfix &lt;=ainfix +V7c1amax_intAainfix &lt;=amin_intainfix +V7c1ainfix &lt;agetV2V7V1Aainfix &lt;V7V0Aainfix &lt;=c0V7Aainfix &lt;=V7V3Aainfix &lt;=V4V7Lainfix +V4V6Aainfix &lt;=ainfix +V4V6amax_intAainfix &lt;=amin_intainfix +V4V6Ladivainfix -V3V4c2Aainfix &lt;=ainfix -V3V4amax_intAainfix &lt;=amin_intainfix -V3V4ainfix &lt;=V4V3Iainfix &lt;=V12V3Aainfix &lt;=V4V12Iainfix =agetV2V12V1Iainfix &lt;V12V0Aainfix &lt;=c0V12FAainfix &lt;V3V0Aainfix &lt;=c0V4FAainfix &lt;=V13ainfix -V0c1Aainfix &lt;=c0V13Iainfix =agetV2V13V1Iainfix &lt;V13V0Aainfix &lt;=c0V13FAainfix &lt;ainfix -V0c1V0Aainfix &lt;=c0c0Aainfix &lt;=ainfix -V0c1amax_intAainfix &lt;=amin_intainfix -V0c1Iainfix &lt;=agetV2V14agetV2V15Iainfix &lt;V15V0Aainfix &lt;=V14V15Aainfix &lt;=c0V14FAainfix &lt;=V0amax_intAainfix &lt;=c0V0FF">
    <label
     name="expl:VC for binary_search"/>
    <proof

--- a/examples/binary_sqrt/why3session.xml
+++ b/examples/binary_sqrt/why3session.xml
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="2">
+<why3session shape_version="3">
 <prover
  id="0"
  name="CVC3"
@@ -27,7 +27,7 @@
    sum="ee4d0c4370d8430ea37857ad245206cf"
    proved="true"
    expanded="true"
-    shape="iainfix &lt;c1.V1Aainfix &lt;V0V1ainfix &lt;V0ainfix *ainfix +c0.V1ainfix +c0.V1Aainfix &lt;=ainfix *c0.c0.V0ainfix &lt;V0ainfix *ainfix +iainfix &lt;=ainfix *ainfix +V3V1ainfix +V3V1V0ainfix +V3V1V3V1ainfix +iainfix &lt;=ainfix *ainfix +V3V1ainfix +V3V1V0ainfix +V3V1V3V1Aainfix &lt;=ainfix *iainfix &lt;=ainfix *ainfix +V3V1ainfix +V3V1V0ainfix +V3V1V3iainfix &lt;=ainfix *ainfix +V3V1ainfix +V3V1V0ainfix +V3V1V3V0Iainfix &lt;V0ainfix *ainfix +V3V2ainfix +V3V2Aainfix &lt;=ainfix *V3V3V0FAainfix &lt;c0.V2Aainfix &lt;=c0.V0Lainfix *c2.V1Iainfix &lt;c0.V1Aainfix &lt;=c0.V0F">
+    shape="iainfix &lt;V0ainfix *ainfix +iV3ainfix +V3V1ainfix &lt;=ainfix *ainfix +V3V1ainfix +V3V1V0V1ainfix +iV3ainfix +V3V1ainfix &lt;=ainfix *ainfix +V3V1ainfix +V3V1V0V1Aainfix &lt;=ainfix *iV3ainfix +V3V1ainfix &lt;=ainfix *ainfix +V3V1ainfix +V3V1V0iV3ainfix +V3V1ainfix &lt;=ainfix *ainfix +V3V1ainfix +V3V1V0V0Iainfix &lt;V0ainfix *ainfix +V3V2ainfix +V3V2Aainfix &lt;=ainfix *V3V3V0FAainfix &lt;c0.V2Aainfix &lt;=c0.V0Lainfix *c2.V1ainfix &lt;V0ainfix *ainfix +c0.V1ainfix +c0.V1Aainfix &lt;=ainfix *c0.c0.V0ainfix &lt;c1.V1Aainfix &lt;V0V1Iainfix &lt;c0.V1Aainfix &lt;=c0.V0F">
    <label
     name="expl:VC for sqrt"/>
    <transf
@@ -42,7 +42,7 @@
      sum="79254120c3e4af8106f3cdeac0a909e2"
      proved="true"
      expanded="true"
-      shape="ainfix &lt;V0ainfix *ainfix +c0.V1ainfix +c0.V1Aainfix &lt;=ainfix *c0.c0.V0Iainfix &lt;c1.V1Aainfix &lt;V0V1Iainfix &lt;c0.V1Aainfix &lt;=c0.V0F">
+      shape="postconditionainfix &lt;V0ainfix *ainfix +c0.V1ainfix +c0.V1Aainfix &lt;=ainfix *c0.c0.V0Iainfix &lt;c1.V1Aainfix &lt;V0V1Iainfix &lt;c0.V1Aainfix &lt;=c0.V0F">
      <label
       name="expl:VC for sqrt"/>
      <proof
@@ -62,7 +62,7 @@
      sum="410ef2bf07ae4a93d6f968fb373d25f7"
      proved="true"
      expanded="true"
-      shape="ainfix &lt;c0.V2Aainfix &lt;=c0.V0Lainfix *c2.V1Iainfix &lt;c1.V1Aainfix &lt;V0V1NIainfix &lt;c0.V1Aainfix &lt;=c0.V0F">
+      shape="preconditionainfix &lt;c0.V2Aainfix &lt;=c0.V0Lainfix *c2.V1INainfix &lt;c1.V1Aainfix &lt;V0V1Iainfix &lt;c0.V1Aainfix &lt;=c0.V0F">
      <label
       name="expl:VC for sqrt"/>
      <proof
@@ -82,7 +82,7 @@
      sum="5321731dc9e8211f2d0331853bb464f7"
      proved="true"
      expanded="true"
-      shape="ainfix &lt;V0ainfix *ainfix +iainfix &lt;=ainfix *ainfix +V3V1ainfix +V3V1V0ainfix +V3V1V3V1ainfix +iainfix &lt;=ainfix *ainfix +V3V1ainfix +V3V1V0ainfix +V3V1V3V1Aainfix &lt;=ainfix *iainfix &lt;=ainfix *ainfix +V3V1ainfix +V3V1V0ainfix +V3V1V3iainfix &lt;=ainfix *ainfix +V3V1ainfix +V3V1V0ainfix +V3V1V3V0Iainfix &lt;V0ainfix *ainfix +V3V2ainfix +V3V2Aainfix &lt;=ainfix *V3V3V0FIainfix &lt;c0.V2Aainfix &lt;=c0.V0Lainfix *c2.V1Iainfix &lt;c1.V1Aainfix &lt;V0V1NIainfix &lt;c0.V1Aainfix &lt;=c0.V0F">
+      shape="postconditionainfix &lt;V0ainfix *ainfix +iV3ainfix +V3V1ainfix &lt;=ainfix *ainfix +V3V1ainfix +V3V1V0V1ainfix +iV3ainfix +V3V1ainfix &lt;=ainfix *ainfix +V3V1ainfix +V3V1V0V1Aainfix &lt;=ainfix *iV3ainfix +V3V1ainfix &lt;=ainfix *ainfix +V3V1ainfix +V3V1V0iV3ainfix +V3V1ainfix &lt;=ainfix *ainfix +V3V1ainfix +V3V1V0V0Iainfix &lt;V0ainfix *ainfix +V3V2ainfix +V3V2Aainfix &lt;=ainfix *V3V3V0FIainfix &lt;c0.V2Aainfix &lt;=c0.V0Lainfix *c2.V1INainfix &lt;c1.V1Aainfix &lt;V0V1Iainfix &lt;c0.V1Aainfix &lt;=c0.V0F">
      <label
       name="expl:VC for sqrt"/>
      <proof

--- a/examples/bitvectors/bitvector/why3session.xml
+++ b/examples/bitvectors/bitvector/why3session.xml
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="2">
+<why3session shape_version="3">
 <prover
  id="0"
  name="Alt-Ergo"
@@ -279,7 +279,7 @@
    sum="1bbd5b442bf57f164e68cd02baff256d"
    proved="true"
    expanded="true"
-    shape="ainfix =anthafrom_intV0c0aTrueIainfix =amodV0c2c0NF">
+    shape="ainfix =anthafrom_intV0c0aTrueINainfix =amodV0c2c0F">
    <proof
     prover="0"
     timelimit="5"
@@ -378,7 +378,7 @@
    sum="c3a466a2dab42d03c150558fd4ca2915"
    proved="true"
    expanded="true"
-    shape="ainfix =anthafrom_int2cV0c0aTrueIainfix =amodV0c2c0NF">
+    shape="ainfix =anthafrom_int2cV0c0aTrueINainfix =amodV0c2c0F">
    <proof
     prover="0"
     timelimit="5"
@@ -1472,7 +1472,7 @@
     memlimit="1000"
     obsolete="false"
     archived="false">
-     <result status="timeout" time="3.45"/>
+     <result status="timeout" time="2.99"/>
    </proof>
    <proof
     prover="6"
@@ -2065,7 +2065,7 @@
     memlimit="1000"
     obsolete="false"
     archived="false">
-     <result status="timeout" time="3.43"/>
+     <result status="timeout" time="2.97"/>
    </proof>
    <proof
     prover="7"

--- a/examples/bitvectors/double/why3session.xml
+++ b/examples/bitvectors/double/why3session.xml
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="2">
+<why3session shape_version="3">
 <prover
  id="0"
  name="Alt-Ergo"

--- a/examples/bitvectors/double_of_int/why3session.xml
+++ b/examples/bitvectors/double_of_int/why3session.xml
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="2">
+<why3session shape_version="3">
 <prover
  id="0"
  name="Alt-Ergo"
@@ -535,7 +535,7 @@
     memlimit="1000"
     obsolete="false"
     archived="false">
-     <result status="valid" time="2.97"/>
+     <result status="valid" time="3.48"/>
    </proof>
   </goal>
   <goal
@@ -848,7 +848,7 @@
     memlimit="1000"
     obsolete="false"
     archived="false">
-     <result status="valid" time="6.82"/>
+     <result status="valid" time="8.87"/>
    </proof>
    <proof
     prover="3"
@@ -956,7 +956,7 @@
     edited="double_of_int_DoubleOfInt_from_int2c_to_nat_sub_pos_1.v"
     obsolete="false"
     archived="false">
-     <result status="valid" time="2.54"/>
+     <result status="valid" time="2.94"/>
    </proof>
   </goal>
   <goal
@@ -1051,7 +1051,7 @@
     edited="double_of_int_DoubleOfInt_lemma1_neg_1.v"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.69"/>
+     <result status="valid" time="0.87"/>
    </proof>
   </goal>
   <goal
@@ -1117,7 +1117,7 @@
     memlimit="1000"
     obsolete="false"
     archived="false">
-     <result status="valid" time="35.51"/>
+     <result status="valid" time="39.51"/>
    </proof>
   </goal>
   <goal
@@ -1135,7 +1135,7 @@
     edited="double_of_int_DoubleOfInt_to_nat_bv32_bv64_aux_1.v"
     obsolete="false"
     archived="false">
-     <result status="valid" time="4.44"/>
+     <result status="valid" time="5.76"/>
    </proof>
   </goal>
   <goal
@@ -1251,7 +1251,7 @@
     memlimit="1000"
     obsolete="false"
     archived="false">
-     <result status="valid" time="1.40"/>
+     <result status="valid" time="1.72"/>
    </proof>
   </goal>
   <goal
@@ -1269,7 +1269,7 @@
     edited="double_of_int_DoubleOfInt_lemma2_1.v"
     obsolete="false"
     archived="false">
-     <result status="valid" time="3.29"/>
+     <result status="valid" time="4.53"/>
    </proof>
   </goal>
   <goal
@@ -1303,7 +1303,7 @@
     memlimit="1000"
     obsolete="false"
     archived="false">
-     <result status="valid" time="1.50"/>
+     <result status="valid" time="1.77"/>
    </proof>
   </goal>
   <goal
@@ -1320,7 +1320,7 @@
     memlimit="1000"
     obsolete="false"
     archived="false">
-     <result status="valid" time="1.40"/>
+     <result status="valid" time="1.80"/>
    </proof>
   </goal>
   <goal
@@ -1337,7 +1337,7 @@
     memlimit="1000"
     obsolete="false"
     archived="false">
-     <result status="valid" time="1.47"/>
+     <result status="valid" time="1.72"/>
    </proof>
   </goal>
   <goal
@@ -1404,7 +1404,7 @@
     edited="double_of_int_DoubleOfInt_lemma3_1.v"
     obsolete="false"
     archived="false">
-     <result status="valid" time="2.09"/>
+     <result status="valid" time="2.62"/>
    </proof>
   </goal>
   <goal

--- a/examples/bitvectors/neg_as_xor/why3session.xml
+++ b/examples/bitvectors/neg_as_xor/why3session.xml
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="2">
+<why3session shape_version="3">
 <prover
  id="0"
  name="Alt-Ergo"

--- a/examples/bitvectors/power2/why3session.xml
+++ b/examples/bitvectors/power2/why3session.xml
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="2">
+<why3session shape_version="3">
 <prover
  id="0"
  name="Alt-Ergo"
@@ -3601,7 +3601,7 @@
    sum="b8f09a9e8cb7b784d44bc8323b47614b"
    proved="true"
    expanded="false"
-    shape="ainfix =apow2V0c0.0NIainfix &gt;=V0c0F">
+    shape="Nainfix =apow2V0c0.0Iainfix &gt;=V0c0F">
    <proof
     prover="4"
     timelimit="5"
@@ -3637,7 +3637,7 @@
    sum="ee98fc95a3eecb3e492b2ebb8d386046"
    proved="true"
    expanded="false"
-    shape="ainfix =apow2V0c0.0NF">
+    shape="Nainfix =apow2V0c0.0F">
    <proof
     prover="4"
     timelimit="5"

--- a/examples/bresenham/why3session.xml
+++ b/examples/bresenham/why3session.xml
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="2">
+<why3session shape_version="3">
 <prover
  id="0"
  name="Alt-Ergo"

--- a/examples/bts/12475/why3session.xml
+++ b/examples/bts/12475/why3session.xml
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="2">
+<why3session shape_version="3">
 <prover
  id="0"
  name="Alt-Ergo"

--- a/examples/bts/12934/why3session.xml
+++ b/examples/bts/12934/why3session.xml
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="2">
+<why3session shape_version="3">
 <prover
  id="0"
  name="Coq"

--- a/examples/bts/13375/why3session.xml
+++ b/examples/bts/13375/why3session.xml
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="2">
+<why3session shape_version="3">
 <prover
  id="0"
  name="Alt-Ergo"

--- a/examples/bts/13849/why3session.xml
+++ b/examples/bts/13849/why3session.xml
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="2">
+<why3session shape_version="3">
 <prover
  id="0"
  name="Coq"

--- a/examples/bts/13853/why3session.xml
+++ b/examples/bts/13853/why3session.xml
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="2">
+<why3session shape_version="3">
 <prover
  id="0"
  name="Alt-Ergo"

--- a/examples/bts/13854/why3session.xml
+++ b/examples/bts/13854/why3session.xml
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="2">
+<why3session shape_version="3">
 <prover
  id="0"
  name="Coq"
@@ -40,7 +40,7 @@
    sum="435ec01d268249598a20febc4e71aa3b"
    proved="true"
    expanded="true"
-    shape="ainfix =aAaTuple0aBN">
+    shape="Nainfix =aAaTuple0aB">
    <proof
     prover="0"
     timelimit="5"

--- a/examples/check-builtin/real/why3session.xml
+++ b/examples/check-builtin/real/why3session.xml
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="2">
+<why3session shape_version="3">
 <prover
  id="0"
  name="Alt-Ergo"

--- a/examples/checking_a_large_routine/why3session.xml
+++ b/examples/checking_a_large_routine/why3session.xml
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="2">
+<why3session shape_version="3">
 <prover
  id="0"
  name="Alt-Ergo"
@@ -27,7 +27,7 @@
    sum="48400da3e3deb2305085d98a53ea7653"
    proved="true"
    expanded="true"
-    shape="iainfix &lt;V2V0iainfix &lt;=V3V2ainfix &lt;ainfix -V2V6ainfix -V2V3Aainfix &lt;=c0ainfix -V2V3Aainfix =V5ainfix *V6afactV2Aainfix &lt;=V6ainfix +V2c1Aainfix &lt;=c1V6Iainfix =V6ainfix +V3c1FIainfix =V5ainfix +V4V1Fainfix &lt;ainfix -V0V7ainfix -V0V2Aainfix &lt;=c0ainfix -V0V2Aainfix =V4afactV7Aainfix &lt;=V7V0Aainfix &lt;=c0V7Iainfix =V7ainfix +V2c1FIainfix =V4ainfix *V3afactV2Aainfix &lt;=V3ainfix +V2c1Aainfix &lt;=c1V3FAainfix =V1ainfix *c1afactV2Aainfix &lt;=c1ainfix +V2c1Aainfix &lt;=c1c1ainfix =V1afactV0Iainfix =V1afactV2Aainfix &lt;=V2V0Aainfix &lt;=c0V2FAainfix =c1afactc0Aainfix &lt;=c0V0Aainfix &lt;=c0c0Iainfix &gt;=V0c0F">
+    shape="iainfix =V1afactV0iainfix &lt;ainfix -V0V5ainfix -V0V2Aainfix &lt;=c0ainfix -V0V2Aainfix =V4afactV5Aainfix &lt;=V5V0Aainfix &lt;=c0V5Iainfix =V5ainfix +V2c1Fainfix &lt;ainfix -V2V7ainfix -V2V3Aainfix &lt;=c0ainfix -V2V3Aainfix =V6ainfix *V7afactV2Aainfix &lt;=V7ainfix +V2c1Aainfix &lt;=c1V7Iainfix =V7ainfix +V3c1FIainfix =V6ainfix +V4V1Fainfix &lt;=V3V2Iainfix =V4ainfix *V3afactV2Aainfix &lt;=V3ainfix +V2c1Aainfix &lt;=c1V3FAainfix =V1ainfix *c1afactV2Aainfix &lt;=c1ainfix +V2c1Aainfix &lt;=c1c1ainfix &lt;V2V0Iainfix =V1afactV2Aainfix &lt;=V2V0Aainfix &lt;=c0V2FAainfix =c1afactc0Aainfix &lt;=c0V0Aainfix &lt;=c0c0Iainfix &gt;=V0c0F">
    <label
     name="expl:VC for routine"/>
    <transf
@@ -42,7 +42,7 @@
      sum="79233ab0ec941c7fb8d5212796d41379"
      proved="true"
      expanded="true"
-      shape="ainfix =c1afactc0Aainfix &lt;=c0V0Aainfix &lt;=c0c0Iainfix &gt;=V0c0F">
+      shape="loop invariant initainfix =c1afactc0Aainfix &lt;=c0V0Aainfix &lt;=c0c0Iainfix &gt;=V0c0F">
      <label
       name="expl:VC for routine"/>
      <proof
@@ -62,7 +62,7 @@
      sum="052f5c48b5de4bcf9338097364324345"
      proved="true"
      expanded="true"
-      shape="ainfix =V1ainfix *c1afactV2Aainfix &lt;=c1ainfix +V2c1Aainfix &lt;=c1c1Iainfix &lt;V2V0Iainfix =V1afactV2Aainfix &lt;=V2V0Aainfix &lt;=c0V2FIainfix &gt;=V0c0F">
+      shape="loop invariant initainfix =V1ainfix *c1afactV2Aainfix &lt;=c1ainfix +V2c1Aainfix &lt;=c1c1Iainfix &lt;V2V0Iainfix =V1afactV2Aainfix &lt;=V2V0Aainfix &lt;=c0V2FIainfix &gt;=V0c0F">
      <label
       name="expl:VC for routine"/>
      <proof
@@ -82,7 +82,7 @@
      sum="d1763ab1163bb7a90fd5db17abe029fb"
      proved="true"
      expanded="true"
-      shape="ainfix =V5ainfix *V6afactV2Aainfix &lt;=V6ainfix +V2c1Aainfix &lt;=c1V6Iainfix =V6ainfix +V3c1FIainfix =V5ainfix +V4V1FIainfix &lt;=V3V2Iainfix =V4ainfix *V3afactV2Aainfix &lt;=V3ainfix +V2c1Aainfix &lt;=c1V3FIainfix &lt;V2V0Iainfix =V1afactV2Aainfix &lt;=V2V0Aainfix &lt;=c0V2FIainfix &gt;=V0c0F">
+      shape="loop invariant preservationainfix =V5ainfix *V6afactV2Aainfix &lt;=V6ainfix +V2c1Aainfix &lt;=c1V6Iainfix =V6ainfix +V3c1FIainfix =V5ainfix +V4V1FIainfix &lt;=V3V2Iainfix =V4ainfix *V3afactV2Aainfix &lt;=V3ainfix +V2c1Aainfix &lt;=c1V3FIainfix &lt;V2V0Iainfix =V1afactV2Aainfix &lt;=V2V0Aainfix &lt;=c0V2FIainfix &gt;=V0c0F">
      <label
       name="expl:VC for routine"/>
      <proof
@@ -102,7 +102,7 @@
      sum="263ba8d04b61ad4b82d36882a88e490e"
      proved="true"
      expanded="true"
-      shape="ainfix &lt;ainfix -V2V6ainfix -V2V3Aainfix &lt;=c0ainfix -V2V3Iainfix =V6ainfix +V3c1FIainfix =V5ainfix +V4V1FIainfix &lt;=V3V2Iainfix =V4ainfix *V3afactV2Aainfix &lt;=V3ainfix +V2c1Aainfix &lt;=c1V3FIainfix &lt;V2V0Iainfix =V1afactV2Aainfix &lt;=V2V0Aainfix &lt;=c0V2FIainfix &gt;=V0c0F">
+      shape="loop variant decreaseainfix &lt;ainfix -V2V6ainfix -V2V3Aainfix &lt;=c0ainfix -V2V3Iainfix =V6ainfix +V3c1FIainfix =V5ainfix +V4V1FIainfix &lt;=V3V2Iainfix =V4ainfix *V3afactV2Aainfix &lt;=V3ainfix +V2c1Aainfix &lt;=c1V3FIainfix &lt;V2V0Iainfix =V1afactV2Aainfix &lt;=V2V0Aainfix &lt;=c0V2FIainfix &gt;=V0c0F">
      <label
       name="expl:VC for routine"/>
      <proof
@@ -122,7 +122,7 @@
      sum="7fc16f770b4e11359f0b428f3ba55754"
      proved="true"
      expanded="true"
-      shape="ainfix =V4afactV5Aainfix &lt;=V5V0Aainfix &lt;=c0V5Iainfix =V5ainfix +V2c1FIainfix &lt;=V3V2NIainfix =V4ainfix *V3afactV2Aainfix &lt;=V3ainfix +V2c1Aainfix &lt;=c1V3FIainfix &lt;V2V0Iainfix =V1afactV2Aainfix &lt;=V2V0Aainfix &lt;=c0V2FIainfix &gt;=V0c0F">
+      shape="loop invariant preservationainfix =V4afactV5Aainfix &lt;=V5V0Aainfix &lt;=c0V5Iainfix =V5ainfix +V2c1FINainfix &lt;=V3V2Iainfix =V4ainfix *V3afactV2Aainfix &lt;=V3ainfix +V2c1Aainfix &lt;=c1V3FIainfix &lt;V2V0Iainfix =V1afactV2Aainfix &lt;=V2V0Aainfix &lt;=c0V2FIainfix &gt;=V0c0F">
      <label
       name="expl:VC for routine"/>
      <proof
@@ -142,7 +142,7 @@
      sum="16b01109cf2c68f4e872a9f54276bdc6"
      proved="true"
      expanded="true"
-      shape="ainfix &lt;ainfix -V0V5ainfix -V0V2Aainfix &lt;=c0ainfix -V0V2Iainfix =V5ainfix +V2c1FIainfix &lt;=V3V2NIainfix =V4ainfix *V3afactV2Aainfix &lt;=V3ainfix +V2c1Aainfix &lt;=c1V3FIainfix &lt;V2V0Iainfix =V1afactV2Aainfix &lt;=V2V0Aainfix &lt;=c0V2FIainfix &gt;=V0c0F">
+      shape="loop variant decreaseainfix &lt;ainfix -V0V5ainfix -V0V2Aainfix &lt;=c0ainfix -V0V2Iainfix =V5ainfix +V2c1FINainfix &lt;=V3V2Iainfix =V4ainfix *V3afactV2Aainfix &lt;=V3ainfix +V2c1Aainfix &lt;=c1V3FIainfix &lt;V2V0Iainfix =V1afactV2Aainfix &lt;=V2V0Aainfix &lt;=c0V2FIainfix &gt;=V0c0F">
      <label
       name="expl:VC for routine"/>
      <proof
@@ -162,7 +162,7 @@
      sum="9e6e7f742e43d692f532206d02dfbbed"
      proved="true"
      expanded="true"
-      shape="ainfix =V1afactV0Iainfix &lt;V2V0NIainfix =V1afactV2Aainfix &lt;=V2V0Aainfix &lt;=c0V2FIainfix &gt;=V0c0F">
+      shape="postconditionainfix =V1afactV0INainfix &lt;V2V0Iainfix =V1afactV2Aainfix &lt;=V2V0Aainfix &lt;=c0V2FIainfix &gt;=V0c0F">
      <label
       name="expl:VC for routine"/>
      <proof
@@ -199,7 +199,7 @@
      sum="70fcc73588c9f950ad6c1c7f0a533801"
      proved="true"
      expanded="true"
-      shape="ainfix =c1afactV0Iainfix &gt;c0V1Lainfix -V0c1Iainfix &gt;=V0c0F">
+      shape="postconditionainfix =c1afactV0Iainfix &gt;c0V1Lainfix -V0c1Iainfix &gt;=V0c0F">
      <label
       name="expl:VC for routine2"/>
      <proof
@@ -219,7 +219,7 @@
      sum="0c3b1de4f7c34597d2b7fd88819dbee0"
      proved="true"
      expanded="true"
-      shape="ainfix =c1afactc0Iainfix &lt;=c0V1Lainfix -V0c1Iainfix &gt;=V0c0F">
+      shape="loop invariant initainfix =c1afactc0Iainfix &lt;=c0V1Lainfix -V0c1Iainfix &gt;=V0c0F">
      <label
       name="expl:VC for routine2"/>
      <proof
@@ -239,7 +239,7 @@
      sum="d44d4728ca0885cde09a2058d1138815"
      proved="true"
      expanded="true"
-      shape="ainfix =V2afactainfix +V3c1Iainfix &gt;c1V3Iainfix =V2afactV3Iainfix &lt;=V3V1Aainfix &lt;=c0V3FFIainfix &lt;=c0V1Lainfix -V0c1Iainfix &gt;=V0c0F">
+      shape="loop invariant preservationainfix =V2afactainfix +V3c1Iainfix &gt;c1V3Iainfix =V2afactV3Iainfix &lt;=V3V1Aainfix &lt;=c0V3FFIainfix &lt;=c0V1Lainfix -V0c1Iainfix &gt;=V0c0F">
      <label
       name="expl:VC for routine2"/>
      <proof
@@ -259,7 +259,7 @@
      sum="2cec2913c5a5ec9fe52e1d99754d18c6"
      proved="true"
      expanded="true"
-      shape="ainfix =V2ainfix *c1afactV3Iainfix &lt;=c1V3Iainfix =V2afactV3Iainfix &lt;=V3V1Aainfix &lt;=c0V3FFIainfix &lt;=c0V1Lainfix -V0c1Iainfix &gt;=V0c0F">
+      shape="loop invariant initainfix =V2ainfix *c1afactV3Iainfix &lt;=c1V3Iainfix =V2afactV3Iainfix &lt;=V3V1Aainfix &lt;=c0V3FFIainfix &lt;=c0V1Lainfix -V0c1Iainfix &gt;=V0c0F">
      <label
       name="expl:VC for routine2"/>
      <proof
@@ -279,7 +279,7 @@
      sum="cde579f5571a4bdcdb5210a8cf8b7c7a"
      proved="true"
      expanded="true"
-      shape="ainfix =V6ainfix *ainfix +V5c1afactV3Iainfix =V6ainfix +V4V2FIainfix =V4ainfix *V5afactV3Iainfix &lt;=V5V3Aainfix &lt;=c1V5FFIainfix &lt;=c1V3Iainfix =V2afactV3Iainfix &lt;=V3V1Aainfix &lt;=c0V3FFIainfix &lt;=c0V1Lainfix -V0c1Iainfix &gt;=V0c0F">
+      shape="loop invariant preservationainfix =V6ainfix *ainfix +V5c1afactV3Iainfix =V6ainfix +V4V2FIainfix =V4ainfix *V5afactV3Iainfix &lt;=V5V3Aainfix &lt;=c1V5FFIainfix &lt;=c1V3Iainfix =V2afactV3Iainfix &lt;=V3V1Aainfix &lt;=c0V3FFIainfix &lt;=c0V1Lainfix -V0c1Iainfix &gt;=V0c0F">
      <label
       name="expl:VC for routine2"/>
      <proof
@@ -299,7 +299,7 @@
      sum="debea5df85ca500994bce0bdad4782fc"
      proved="true"
      expanded="true"
-      shape="ainfix =V4afactainfix +V3c1Iainfix =V4ainfix *ainfix +V3c1afactV3FIainfix &lt;=c1V3Iainfix =V2afactV3Iainfix &lt;=V3V1Aainfix &lt;=c0V3FFIainfix &lt;=c0V1Lainfix -V0c1Iainfix &gt;=V0c0F">
+      shape="loop invariant preservationainfix =V4afactainfix +V3c1Iainfix =V4ainfix *ainfix +V3c1afactV3FIainfix &lt;=c1V3Iainfix =V2afactV3Iainfix &lt;=V3V1Aainfix &lt;=c0V3FFIainfix &lt;=c0V1Lainfix -V0c1Iainfix &gt;=V0c0F">
      <label
       name="expl:VC for routine2"/>
      <proof
@@ -319,7 +319,7 @@
      sum="3bd2912de1470db80c28e60238428849"
      proved="true"
      expanded="true"
-      shape="ainfix =V2afactV0Iainfix =V2afactainfix +V1c1FIainfix &lt;=c0V1Lainfix -V0c1Iainfix &gt;=V0c0F">
+      shape="postconditionainfix =V2afactV0Iainfix =V2afactainfix +V1c1FIainfix &lt;=c0V1Lainfix -V0c1Iainfix &gt;=V0c0F">
      <label
       name="expl:VC for routine2"/>
      <proof

--- a/examples/conjugate/why3session.xml
+++ b/examples/conjugate/why3session.xml
--- a/examples/counting_sort/why3session.xml
+++ b/examples/counting_sort/why3session.xml
--- a/examples/decrease1/why3session.xml
+++ b/examples/decrease1/why3session.xml
--- a/examples/dfa_example/why3session.xml
+++ b/examples/dfa_example/why3session.xml
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="2">
+<why3session shape_version="3">
 <prover
  id="0"
  name="Alt-Ergo"
@@ -30,7 +30,7 @@
    sum="f9cfc1853e8a0f3be3bad705fd3e75f1"
    proved="true"
    expanded="false"
-    shape="amemaNilar1N">
+    shape="NamemaNilar1">
    <proof
     prover="2"
     timelimit="8"
@@ -94,7 +94,7 @@
    sum="07b99b61c7a88b686dc092af44652f40"
    proved="true"
    expanded="false"
-    shape="CV2aNoneamemV0aConcataStaraAltaCharaZeroaCharaOneaCharaOneAainfix =V1aNilNaSomeaZeroamemV0aConcataStaraAltaCharaZeroaCharaOneaCharaOneAainfix =V3aNilqainfix =V4aTrueIamemV1aConcataStaraAltaCharaZeroaCharaOneaCharaOneAainfix =V3aNilqainfix =V4aTrueFFaSomeaOneamemV0aConcataStaraAltaCharaZeroaCharaOneaCharaOneAainfix =V5aNilqainfix =V6aTrueIamemV1aAltaEpsilonaConcataStaraAltaCharaZeroaCharaOneaCharaOneAainfix =V5aNilqainfix =V6aTrueFFICV0aConsVVainfix =V2aSomeV7Aainfix =V1V8aNilainfix =V2aNoneAainfix =V1aNilAainfix =V0V1FFF">
+    shape="CNamemV0aConcataStaraAltaCharaZeroaCharaOneaCharaOneAainfix =V1aNilaNoneamemV0aConcataStaraAltaCharaZeroaCharaOneaCharaOneAainfix =V3aNilqainfix =V4aTrueIamemV1aConcataStaraAltaCharaZeroaCharaOneaCharaOneAainfix =V3aNilqainfix =V4aTrueFFaSomeaZeroamemV0aConcataStaraAltaCharaZeroaCharaOneaCharaOneAainfix =V5aNilqainfix =V6aTrueIamemV1aAltaEpsilonaConcataStaraAltaCharaZeroaCharaOneaCharaOneAainfix =V5aNilqainfix =V6aTrueFFaSomeaOneV2ICainfix =V2aSomeV7Aainfix =V1V8aConsVVainfix =V2aNoneAainfix =V1aNilAainfix =V0V1aNilV0FFF">
    <label
     name="expl:VC for astate1"/>
    <transf
@@ -109,7 +109,7 @@