updated new sessions with separate files for shapes

89e5b66e · MARCHE Claude · fde8d81f · 89e5b66e · 89e5b66e · 89e5b66e
Commit 89e5b66e authored Jun 26, 2014 by MARCHE Claude
75 changed files
--- 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">
+<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
+"http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="4">
- <prover
-  id="0"
-  name="Alt-Ergo"
-  version="0.95.1"/>
- <prover
-  id="1"
-  name="CVC3"
-  version="2.4.1"/>
- <prover
-  id="2"
-  name="Z3"
-  version="3.2"/>
- <file
-  name="../add_list.mlw"
-  verified="true"
+ <prover id="0" name="CVC3" version="2.4.1" timelimit="5" memlimit="1000"/>
+ <prover id="1" name="Alt-Ergo" version="0.95.1" timelimit="5"
+  memlimit="1000"/>
+ <prover id="2" name="Z3" version="3.2" timelimit="5" memlimit="1000"/>
+ <file name="../add_list.mlw"
  expanded="true">
-  <theory
-   name="SumList"
-   locfile="../add_list.mlw"
-   loclnum="1" loccnumb="7" loccnume="14"
-   verified="true"
-   expanded="false">
+  <theory name="SumList">
  </theory>
-  <theory
-   name="AddListRec"
-   locfile="../add_list.mlw"
-   loclnum="28" loccnumb="7" loccnume="17"
-   verified="true"
+  <theory name="AddListRec"
   expanded="true">
-   <goal
-    name="WP_parameter sum"
-    locfile="../add_list.mlw"
-    loclnum="32" loccnumb="8" loccnume="11"
-    expl="VC for sum"
+   <goal name="WP_parameter sum" expl="VC for sum"
    sum="0ad629c2956d434cdf621a03e0b7c7ba"
-    proved="true"
-    expanded="true"
-    shape="Cainfix =c0.0aadd_realV0Aainfix =c0aadd_intV0aNilCainfix =V4aadd_realV0Aainfix =ainfix +V5V3aadd_intV0aIntegerVainfix =ainfix +.V6V4aadd_realV0Aainfix =V3aadd_intV0aRealVV1Iainfix =V4aadd_realV2Aainfix =V3aadd_intV2FACfaNilainfix =V7V2aConswVV0aConsVVV0F">
-    <label
-     name="expl:VC for sum"/>
-    <proof
-     prover="0"
-     timelimit="5"
-     memlimit="1000"
-     obsolete="false"
-     archived="false">
-     <result status="valid" time="0.02"/>
-    </proof>
-    <proof
-     prover="1"
-     timelimit="5"
-     memlimit="1000"
-     obsolete="false"
-     archived="false">
+    expanded="true">
+    <label name="expl:VC for sum"/>
+    <proof prover="0">
     <result status="valid" time="0.01"/>
    </proof>
-    <proof
-     prover="2"
-     timelimit="5"
-     memlimit="1000"
-     obsolete="false"
-     archived="false">
+    <proof prover="1">
+     <result status="valid" time="0.02"/>
+    </proof>
+    <proof prover="2">
     <result status="valid" time="0.02"/>
    </proof>
   </goal>
-   <goal
-    name="WP_parameter main"
-    locfile="../add_list.mlw"
-    loclnum="45" loccnumb="4" loccnume="8"
-    expl="VC for main"
+   <goal name="WP_parameter main" expl="VC for main"
    sum="6b4e350cd7d1b4015bab61dc01e96aec"
-    proved="true"
-    expanded="true"
-    shape="ainfix =V2c4.7Aainfix =V1c22Iainfix =V2aadd_realV0Aainfix =V1aadd_intV0FLaConsaIntegerc5aConsaRealc3.3aConsaIntegerc8aConsaRealc1.4aConsaIntegerc9aNil">
-    <label
-     name="expl:VC for main"/>
-    <proof
-     prover="1"
-     timelimit="5"
-     memlimit="1000"
-     obsolete="false"
-     archived="false">
+    expanded="true">
+    <label name="expl:VC for main"/>
+    <proof prover="0">
     <result status="valid" time="0.02"/>
    </proof>
-    <proof
-     prover="2"
-     timelimit="5"
-     memlimit="1000"
-     obsolete="false"
-     archived="false">
+    <proof prover="2">
     <result status="valid" time="0.02"/>
    </proof>
   </goal>
  </theory>
-  <theory
-   name="AddListImp"
-   locfile="../add_list.mlw"
-   loclnum="57" loccnumb="7" loccnume="17"
-   verified="true"
+  <theory name="AddListImp"
   expanded="true">
-   <goal
-    name="WP_parameter sum"
-    locfile="../add_list.mlw"
-    loclnum="64" loccnumb="4" loccnume="7"
-    expl="VC for sum"
+   <goal name="WP_parameter sum" expl="VC for sum"
    sum="82f58e47d4e58d15d59a87efee2a6ad8"
-    proved="true"
-    expanded="true"
-    shape="ifCainfix =V2aadd_realV0Aainfix =V3aadd_intV0aNilCfaNilainfix =V8V7aConswVV1Aainfix =ainfix +.V2aadd_realV7aadd_realV0Aainfix =ainfix +V6aadd_intV7aadd_intV0Iainfix =V7V5FIainfix =V6ainfix +V3V4FaConsaIntegerVVCfaNilainfix =V13V12aConswVV1Aainfix =ainfix +.V11aadd_realV12aadd_realV0Aainfix =ainfix +V3aadd_intV12aadd_intV0Iainfix =V12V10FIainfix =V11ainfix +.V2V9FaConsaRealVVV1tIainfix =ainfix +.V2aadd_realV1aadd_realV0Aainfix =ainfix +V3aadd_intV1aadd_intV0FAainfix =ainfix +.c0.0aadd_realV0aadd_realV0Aainfix =ainfix +c0aadd_intV0aadd_intV0F">
-    <label
-     name="expl:VC for sum"/>
-    <proof
-     prover="1"
-     timelimit="5"
-     memlimit="1000"
-     obsolete="false"
-     archived="false">
+    expanded="true">
+    <label name="expl:VC for sum"/>
+    <proof prover="0">
     <result status="valid" time="0.02"/>
    </proof>
-    <proof
-     prover="2"
-     timelimit="5"
-     memlimit="1000"
-     obsolete="false"
-     archived="false">
+    <proof prover="2">
     <result status="valid" time="0.02"/>
    </proof>
   </goal>
-   <goal
-    name="WP_parameter main"
-    locfile="../add_list.mlw"
-    loclnum="88" loccnumb="4" loccnume="8"
-    expl="VC for main"
+   <goal name="WP_parameter main" expl="VC for main"
    sum="9051692e9ac1a4d1f56386a0fd7d440f"
-    proved="true"
-    expanded="true"
-    shape="ainfix =V2c4.7Aainfix =V1c22Iainfix =V2aadd_realV0Aainfix =V1aadd_intV0FLaConsaIntegerc5aConsaRealc3.3aConsaIntegerc8aConsaRealc1.4aConsaIntegerc9aNil">
-    <label
-     name="expl:VC for main"/>
-    <proof
-     prover="1"
-     timelimit="5"
-     memlimit="1000"
-     obsolete="false"
-     archived="false">
+    expanded="true">
+    <label name="expl:VC for main"/>
+    <proof prover="0">
     <result status="valid" time="0.02"/>
    </proof>
-    <proof
-     prover="2"
-     timelimit="5"
-     memlimit="1000"
-     obsolete="false"
-     archived="false">
+    <proof prover="2">
     <result status="valid" time="0.02"/>
    </proof>
   </goal>

--- a/examples/add_list/why3shapes.dat
+++ b/examples/add_list/why3shapes.dat
+0ad629c2956d434cdf621a03e0b7c7ba Cainfix =c0.0aadd_realV0Aainfix =c0aadd_intV0aNilCainfix =V4aadd_realV0Aainfix =ainfix +V5V3aadd_intV0aIntegerVainfix =ainfix +.V6V4aadd_realV0Aainfix =V3aadd_intV0aRealVV1Iainfix =V4aadd_realV2Aainfix =V3aadd_intV2FACfaNilainfix =V7V2aConswVV0aConsVVV0F
+6b4e350cd7d1b4015bab61dc01e96aec ainfix =V2c4.7Aainfix =V1c22Iainfix =V2aadd_realV0Aainfix =V1aadd_intV0FLaConsaIntegerc5aConsaRealc3.3aConsaIntegerc8aConsaRealc1.4aConsaIntegerc9aNil
+82f58e47d4e58d15d59a87efee2a6ad8 ifCainfix =V2aadd_realV0Aainfix =V3aadd_intV0aNilCfaNilainfix =V8V7aConswVV1Aainfix =ainfix +.V2aadd_realV7aadd_realV0Aainfix =ainfix +V6aadd_intV7aadd_intV0Iainfix =V7V5FIainfix =V6ainfix +V3V4FaConsaIntegerVVCfaNilainfix =V13V12aConswVV1Aainfix =ainfix +.V11aadd_realV12aadd_realV0Aainfix =ainfix +V3aadd_intV12aadd_intV0Iainfix =V12V10FIainfix =V11ainfix +.V2V9FaConsaRealVVV1tIainfix =ainfix +.V2aadd_realV1aadd_realV0Aainfix =ainfix +V3aadd_intV1aadd_intV0FAainfix =ainfix +.c0.0aadd_realV0aadd_realV0Aainfix =ainfix +c0aadd_intV0aadd_intV0F
+9051692e9ac1a4d1f56386a0fd7d440f ainfix =V2c4.7Aainfix =V1c22Iainfix =V2aadd_realV0Aainfix =V1aadd_intV0FLaConsaIntegerc5aConsaRealc3.3aConsaIntegerc8aConsaRealc1.4aConsaIntegerc9aNil
--- a/examples/algo63/why3session.xml
+++ b/examples/algo63/why3session.xml
--- a/examples/algo63/why3shapes.dat
+++ b/examples/algo63/why3shapes.dat
--- a/examples/algo64/why3session.xml
+++ b/examples/algo64/why3session.xml
--- a/examples/algo64/why3shapes.dat
+++ b/examples/algo64/why3shapes.dat
+b3c80285a2f93720ffbeec07fe9484f7 iasorted_subV1V2ainfix +V3c1Aapermut_subV4V4V2ainfix +V3c1asorted_subV11V2ainfix +V3c1Aapermut_subV4V12V2ainfix +V3c1Aaqs_partitionV10V12V2V3V6V5c42Iasorted_subV11V6ainfix +V3c1Aapermut_subV10V12V6ainfix +V3c1Aainfix <=c0V0Lamk arrayV0V11FAainfix <V3V0Aainfix <=V6V3Aainfix <=c0V6Aainfix <ainfix -V3V6ainfix -V3V2Aainfix <=c0ainfix -V3V2Aaqs_partitionV8V10V2V3V6V5c42Iasorted_subV9V2ainfix +V5c1Aapermut_subV8V10V2ainfix +V5c1Aainfix <=c0V0Lamk arrayV0V9FAainfix <V5V0Aainfix <=V2V5Aainfix <=c0V2Aainfix <ainfix -V5V2ainfix -V3V2Aainfix <=c0ainfix -V3V2Iainfix >=agetV7V13c42Iainfix <=V13V3Aainfix <=V6V13FAainfix =agetV7V14c42Iainfix <V14V6Aainfix <V5V14FAainfix <=agetV7V15c42Iainfix <=V15V5Aainfix <=V2V15FAapermut_subV4V8V2ainfix +V3c1Aainfix <=V6V3Aainfix <V5V6Aainfix <=V2V5Aainfix <=c0V0Lamk arrayV0V7FAainfix <V3V0Aainfix <V2V3Aainfix <=c0V2ainfix <V2V3Iainfix <V3V0Aainfix <=V2V3Aainfix <=c0V2Aainfix <=c0V0Lamk arrayV0V1F
+60641f0dd6fd791e2eb04365466e4b67 preconditionainfix <V3V0Aainfix <V2V3Aainfix <=c0V2Iainfix <V2V3Iainfix <V3V0Aainfix <=V2V3Aainfix <=c0V2Aainfix <=c0V0Lamk arrayV0V1F
+d044cdfb327536252d9d35d6c8c8d779 variant decreaseainfix <ainfix -V5V2ainfix -V3V2Aainfix <=c0ainfix -V3V2Iainfix >=agetV7V9c42Iainfix <=V9V3Aainfix <=V6V9FAainfix =agetV7V10c42Iainfix <V10V6Aainfix <V5V10FAainfix <=agetV7V11c42Iainfix <=V11V5Aainfix <=V2V11FAapermut_subV4V8V2ainfix +V3c1Aainfix <=V6V3Aainfix <V5V6Aainfix <=V2V5Aainfix <=c0V0Lamk arrayV0V7FIainfix <V3V0Aainfix <V2V3Aainfix <=c0V2Iainfix <V2V3Iainfix <V3V0Aainfix <=V2V3Aainfix <=c0V2Aainfix <=c0V0Lamk arrayV0V1F
+c51bbed49cb41b5186ee449ca22b5d0f preconditionainfix <V5V0Aainfix <=V2V5Aainfix <=c0V2Iainfix >=agetV7V9c42Iainfix <=V9V3Aainfix <=V6V9FAainfix =agetV7V10c42Iainfix <V10V6Aainfix <V5V10FAainfix <=agetV7V11c42Iainfix <=V11V5Aainfix <=V2V11FAapermut_subV4V8V2ainfix +V3c1Aainfix <=V6V3Aainfix <V5V6Aainfix <=V2V5Aainfix <=c0V0Lamk arrayV0V7FIainfix <V3V0Aainfix <V2V3Aainfix <=c0V2Iainfix <V2V3Iainfix <V3V0Aainfix <=V2V3Aainfix <=c0V2Aainfix <=c0V0Lamk arrayV0V1F
+a62cc8ba874159b234bb59428fe08b3c assertionaqs_partitionV8V10V2V3V6V5c42Iasorted_subV9V2ainfix +V5c1Aapermut_subV8V10V2ainfix +V5c1Aainfix <=c0V0Lamk arrayV0V9FIainfix <V5V0Aainfix <=V2V5Aainfix <=c0V2Iainfix >=agetV7V11c42Iainfix <=V11V3Aainfix <=V6V11FAainfix =agetV7V12c42Iainfix <V12V6Aainfix <V5V12FAainfix <=agetV7V13c42Iainfix <=V13V5Aainfix <=V2V13FAapermut_subV4V8V2ainfix +V3c1Aainfix <=V6V3Aainfix <V5V6Aainfix <=V2V5Aainfix <=c0V0Lamk arrayV0V7FIainfix <V3V0Aainfix <V2V3Aainfix <=c0V2Iainfix <V2V3Iainfix <V3V0Aainfix <=V2V3Aainfix <=c0V2Aainfix <=c0V0Lamk arrayV0V1F
+cbc7bedb98f7451986a3718eda496a7c variant decreaseainfix <ainfix -V3V6ainfix -V3V2Aainfix <=c0ainfix -V3V2Iaqs_partitionV8V10V2V3V6V5c42Iasorted_subV9V2ainfix +V5c1Aapermut_subV8V10V2ainfix +V5c1Aainfix <=c0V0Lamk arrayV0V9FIainfix <V5V0Aainfix <=V2V5Aainfix <=c0V2Iainfix >=agetV7V11c42Iainfix <=V11V3Aainfix <=V6V11FAainfix =agetV7V12c42Iainfix <V12V6Aainfix <V5V12FAainfix <=agetV7V13c42Iainfix <=V13V5Aainfix <=V2V13FAapermut_subV4V8V2ainfix +V3c1Aainfix <=V6V3Aainfix <V5V6Aainfix <=V2V5Aainfix <=c0V0Lamk arrayV0V7FIainfix <V3V0Aainfix <V2V3Aainfix <=c0V2Iainfix <V2V3Iainfix <V3V0Aainfix <=V2V3Aainfix <=c0V2Aainfix <=c0V0Lamk arrayV0V1F
+fff053c1414e1610d034118e841c6500 preconditionainfix <V3V0Aainfix <=V6V3Aainfix <=c0V6Iaqs_partitionV8V10V2V3V6V5c42Iasorted_subV9V2ainfix +V5c1Aapermut_subV8V10V2ainfix +V5c1Aainfix <=c0V0Lamk arrayV0V9FIainfix <V5V0Aainfix <=V2V5Aainfix <=c0V2Iainfix >=agetV7V11c42Iainfix <=V11V3Aainfix <=V6V11FAainfix =agetV7V12c42Iainfix <V12V6Aainfix <V5V12FAainfix <=agetV7V13c42Iainfix <=V13V5Aainfix <=V2V13FAapermut_subV4V8V2ainfix +V3c1Aainfix <=V6V3Aainfix <V5V6Aainfix <=V2V5Aainfix <=c0V0Lamk arrayV0V7FIainfix <V3V0Aainfix <V2V3Aainfix <=c0V2Iainfix <V2V3Iainfix <V3V0Aainfix <=V2V3Aainfix <=c0V2Aainfix <=c0V0Lamk arrayV0V1F
+c286faac90136a80939022ab618896af assertionaqs_partitionV10V12V2V3V6V5c42Iasorted_subV11V6ainfix +V3c1Aapermut_subV10V12V6ainfix +V3c1Aainfix <=c0V0Lamk arrayV0V11FIainfix <V3V0Aainfix <=V6V3Aainfix <=c0V6Iaqs_partitionV8V10V2V3V6V5c42Iasorted_subV9V2ainfix +V5c1Aapermut_subV8V10V2ainfix +V5c1Aainfix <=c0V0Lamk arrayV0V9FIainfix <V5V0Aainfix <=V2V5Aainfix <=c0V2Iainfix >=agetV7V13c42Iainfix <=V13V3Aainfix <=V6V13FAainfix =agetV7V14c42Iainfix <V14V6Aainfix <V5V14FAainfix <=agetV7V15c42Iainfix <=V15V5Aainfix <=V2V15FAapermut_subV4V8V2ainfix +V3c1Aainfix <=V6V3Aainfix <V5V6Aainfix <=V2V5Aainfix <=c0V0Lamk arrayV0V7FIainfix <V3V0Aainfix <V2V3Aainfix <=c0V2Iainfix <V2V3Iainfix <V3V0Aainfix <=V2V3Aainfix <=c0V2Aainfix <=c0V0Lamk arrayV0V1F
+bf52bb94f3ce94cc8aeb29cfbd99aba5 postconditionapermut_subV4V12V2ainfix +V3c1Iaqs_partitionV10V12V2V3V6V5c42Iasorted_subV11V6ainfix +V3c1Aapermut_subV10V12V6ainfix +V3c1Aainfix <=c0V0Lamk arrayV0V11FIainfix <V3V0Aainfix <=V6V3Aainfix <=c0V6Iaqs_partitionV8V10V2V3V6V5c42Iasorted_subV9V2ainfix +V5c1Aapermut_subV8V10V2ainfix +V5c1Aainfix <=c0V0Lamk arrayV0V9FIainfix <V5V0Aainfix <=V2V5Aainfix <=c0V2Iainfix >=agetV7V13c42Iainfix <=V13V3Aainfix <=V6V13FAainfix =agetV7V14c42Iainfix <V14V6Aainfix <V5V14FAainfix <=agetV7V15c42Iainfix <=V15V5Aainfix <=V2V15FAapermut_subV4V8V2ainfix +V3c1Aainfix <=V6V3Aainfix <V5V6Aainfix <=V2V5Aainfix <=c0V0Lamk arrayV0V7FIainfix <V3V0Aainfix <V2V3Aainfix <=c0V2Iainfix <V2V3Iainfix <V3V0Aainfix <=V2V3Aainfix <=c0V2Aainfix <=c0V0Lamk arrayV0V1F
+97cc3e363dcba7833cc03add00eca267 postconditionasorted_subV11V2ainfix +V3c1Iaqs_partitionV10V12V2V3V6V5c42Iasorted_subV11V6ainfix +V3c1Aapermut_subV10V12V6ainfix +V3c1Aainfix <=c0V0Lamk arrayV0V11FIainfix <V3V0Aainfix <=V6V3Aainfix <=c0V6Iaqs_partitionV8V10V2V3V6V5c42Iasorted_subV9V2ainfix +V5c1Aapermut_subV8V10V2ainfix +V5c1Aainfix <=c0V0Lamk arrayV0V9FIainfix <V5V0Aainfix <=V2V5Aainfix <=c0V2Iainfix >=agetV7V13c42Iainfix <=V13V3Aainfix <=V6V13FAainfix =agetV7V14c42Iainfix <V14V6Aainfix <V5V14FAainfix <=agetV7V15c42Iainfix <=V15V5Aainfix <=V2V15FAapermut_subV4V8V2ainfix +V3c1Aainfix <=V6V3Aainfix <V5V6Aainfix <=V2V5Aainfix <=c0V0Lamk arrayV0V7FIainfix <V3V0Aainfix <V2V3Aainfix <=c0V2Iainfix <V2V3Iainfix <V3V0Aainfix <=V2V3Aainfix <=c0V2Aainfix <=c0V0Lamk arrayV0V1F
+16dcef28364b3606b5af7ea67b96d36c postconditionapermut_subV4V4V2ainfix +V3c1INainfix <V2V3Iainfix <V3V0Aainfix <=V2V3Aainfix <=c0V2Aainfix <=c0V0Lamk arrayV0V1F
+a2af1e38ef1266733de9df088d4b57d3 postconditionasorted_subV1V2ainfix +V3c1INainfix <V2V3Iainfix <V3V0Aainfix <=V2V3Aainfix <=c0V2Aainfix <=c0V0Lamk arrayV0V1F
+c020ba36a9f1cbc706a81299d7e67dc5 iasorted_subV1c0V0Aapermut_allV2V2asorted_subV4c0V0Aapermut_allV2V5Iasorted_subV4c0ainfix +V3c1Aapermut_subV2V5c0ainfix +V3c1Aainfix <=c0V0Lamk arrayV0V4FAainfix <V3V0Aainfix <=c0V3Aainfix <=c0c0Lainfix -V0c1ainfix >V0c0Iainfix <=c0V0Lamk arrayV0V1F
+af20b26413ca9ad74cd53bb91ad9bf58 preconditionainfix <V3V0Aainfix <=c0V3Aainfix <=c0c0Lainfix -V0c1Iainfix >V0c0Iainfix <=c0V0Lamk arrayV0V1F
+8c72e4401654ed269af73c95614802d2 postconditionapermut_allV2V5Iasorted_subV4c0ainfix +V3c1Aapermut_subV2V5c0ainfix +V3c1Aainfix <=c0V0Lamk arrayV0V4FIainfix <V3V0Aainfix <=c0V3Aainfix <=c0c0Lainfix -V0c1Iainfix >V0c0Iainfix <=c0V0Lamk arrayV0V1F
+abf810b8c32150c26b4a3f3e6aacac6e postconditionasorted_subV4c0V0Iasorted_subV4c0ainfix +V3c1Aapermut_subV2V5c0ainfix +V3c1Aainfix <=c0V0Lamk arrayV0V4FIainfix <V3V0Aainfix <=c0V3Aainfix <=c0c0Lainfix -V0c1Iainfix >V0c0Iainfix <=c0V0Lamk arrayV0V1F
+ba4a3b43dca6859d783d70d4c5b16669 postconditionapermut_allV2V2INainfix >V0c0Iainfix <=c0V0Lamk arrayV0V1F
+8532155787a9b770710dad8ca4324c1f postconditionasorted_subV1c0V0INainfix >V0c0Iainfix <=c0V0Lamk arrayV0V1F
--- a/examples/algo65/why3session.xml
+++ b/examples/algo65/why3session.xml
--- a/examples/algo65/why3shapes.dat
+++ b/examples/algo65/why3shapes.dat
--- a/examples/all_distinct/why3session.xml
+++ b/examples/all_distinct/why3session.xml
 <?xml version="1.0" encoding="UTF-8"?>
-<!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
+<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
+"http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="4">
- <prover
-  id="0"
-  name="Alt-Ergo"
-  version="0.95.2"/>
- <file
-  name="../all_distinct.mlw"
-  verified="true"
+ <prover id="0" name="Alt-Ergo" version="0.95.2" timelimit="6"
+  memlimit="1000"/>
+ <file name="../all_distinct.mlw"
  expanded="true">
-  <theory
-   name="AllDistinct"
-   locfile="../all_distinct.mlw"
-   loclnum="5" loccnumb="7" loccnume="18"
-   verified="true"
+  <theory name="AllDistinct"
   expanded="true">
-   <goal
-    name="WP_parameter all_distinct"
-    locfile="../all_distinct.mlw"
-    loclnum="13" loccnumb="6" loccnume="18"
-    expl="VC for all_distinct"
+   <goal name="WP_parameter all_distinct" expl="VC for all_distinct"
    sum="9cd8ab30056665aa598b63118511deb6"
-    proved="true"
-    expanded="true"
-    shape="Nainfix =agetV1V5agetV1V6INainfix =V5V6Iainfix &lt;V6V0Aainfix &lt;=c0V6Iainfix &lt;V5V0Aainfix &lt;=c0V5FIainfix =agetV1V8V7Aainfix &lt;V8ainfix +V3c1Aainfix &lt;=c0V8Eqainfix =agetV4V7aTrueIainfix &lt;V7V2Aainfix &lt;=c0V7FANainfix =agetV1V9agetV1V10INainfix =V9V10Iainfix &lt;V10ainfix +V3c1Aainfix &lt;=c0V10Iainfix &lt;V9ainfix +V3c1Aainfix &lt;=c0V9FAiainfix =agetV1V15V14Aainfix &lt;V15ainfix +V11c1Aainfix &lt;=c0V15Eqainfix =agetV13V14aTrueIainfix &lt;V14V2Aainfix &lt;=c0V14FANainfix =agetV1V16agetV1V17INainfix =V16V17Iainfix &lt;V17ainfix +V11c1Aainfix &lt;=c0V17Iainfix &lt;V16ainfix +V11c1Aainfix &lt;=c0V16FIainfix =V13asetV4V12aTrueAainfix &lt;=c0V2FAainfix &lt;V12V2Aainfix &lt;=c0V12NNainfix =agetV1V18agetV1V19INainfix =V18V19Iainfix &lt;V19V0Aainfix &lt;=c0V19Iainfix &lt;V18V0Aainfix &lt;=c0V18Fainfix =agetV4V12aTrueAainfix &lt;V12V2Aainfix &lt;=c0V12Aainfix &lt;=c0V2LagetV1V11Aainfix &lt;V11V0Aainfix &lt;=c0V11Iainfix =agetV1V21V20Aainfix &lt;V21V11Aainfix &lt;=c0V21Eqainfix =agetV4V20aTrueIainfix &lt;V20V2Aainfix &lt;=c0V20FANainfix =agetV1V22agetV1V23INainfix =V22V23Iainfix &lt;V23V11Aainfix &lt;=c0V23Iainfix &lt;V22V11Aainfix &lt;=c0V22FIainfix &lt;=V11V3Aainfix &lt;=c0V11FFAainfix =agetV1V25V24Aainfix &lt;V25c0Aainfix &lt;=c0V25Eqainfix =agetaconstaFalseV24aTrueIainfix &lt;V24V2Aainfix &lt;=c0V24FANainfix =agetV1V26agetV1V27INainfix =V26V27Iainfix &lt;V27c0Aainfix &lt;=c0V27Iainfix &lt;V26c0Aainfix &lt;=c0V26FIainfix &lt;=c0V3ANainfix =agetV1V28agetV1V29INainfix =V28V29Iainfix &lt;V29V0Aainfix &lt;=c0V29Iainfix &lt;V28V0Aainfix &lt;=c0V28FIainfix &gt;c0V3Lainfix -V0c1Iainfix &lt;=c0V2Aainfix &gt;=V2c0Iainfix &lt;agetV1V30V2Aainfix &lt;=c0agetV1V30Iainfix &lt;V30V0Aainfix &lt;=c0V30FAainfix &lt;=c0V2Aainfix &lt;=c0V0F">
-    <label
-     name="expl:VC for all_distinct"/>
-    <transf
-     name="split_goal_wp"
-     proved="true"
+    expanded="true">
+    <label name="expl:VC for all_distinct"/>
+    <transf name="split_goal_wp"
     expanded="true">
-     <goal
-      name="WP_parameter all_distinct.1"
-      locfile="../all_distinct.mlw"
-      loclnum="13" loccnumb="6" loccnume="18"
-      expl="1. array creation size"
+     <goal name="WP_parameter all_distinct.1" expl="1. array creation size"
      sum="169dead4ca86d70a93945d7a849a4ddf"
-      proved="true"
-      expanded="true"
-      shape="array creation sizeainfix &gt;=V2c0Iainfix &lt;agetV1V3V2Aainfix &lt;=c0agetV1V3Iainfix &lt;V3V0Aainfix &lt;=c0V3FAainfix &lt;=c0V2Aainfix &lt;=c0V0F">
-      <label
-       name="expl:VC for all_distinct"/>
-      <proof
-       prover="0"
-       timelimit="6"
-       memlimit="1000"
-       obsolete="false"
-       archived="false">
+      expanded="true">
+      <label name="expl:VC for all_distinct"/>
+      <proof prover="0">
       <result status="valid" time="0.02"/>
      </proof>
     </goal>
-     <goal
-      name="WP_parameter all_distinct.2"
-      locfile="../all_distinct.mlw"
-      loclnum="13" loccnumb="6" loccnume="18"
-      expl="2. postcondition"
+     <goal name="WP_parameter all_distinct.2" expl="2. postcondition"
      sum="8d038b937a7ed02cbabc2d03293374eb"
-      proved="true"
-      expanded="true"
-      shape="postconditionNainfix =agetV1V4agetV1V5INainfix =V4V5Iainfix &lt;V5V0Aainfix &lt;=c0V5Iainfix &lt;V4V0Aainfix &lt;=c0V4FIainfix &gt;c0V3Lainfix -V0c1Iainfix &lt;=c0V2Iainfix &gt;=V2c0Iainfix &lt;agetV1V6V2Aainfix &lt;=c0agetV1V6Iainfix &lt;V6V0Aainfix &lt;=c0V6FAainfix &lt;=c0V2Aainfix &lt;=c0V0F">
-      <label
-       name="expl:VC for all_distinct"/>
-      <proof
-       prover="0"
-       timelimit="6"
-       memlimit="1000"
-       obsolete="false"
-       archived="false">
+      expanded="true">
+      <label name="expl:VC for all_distinct"/>
+      <proof prover="0">
       <result status="valid" time="0.02"/>
      </proof>
     </goal>
-     <goal
-      name="WP_parameter all_distinct.3"
-      locfile="../all_distinct.mlw"
-      loclnum="13" loccnumb="6" loccnume="18"
-      expl="3. loop invariant init"
+     <goal name="WP_parameter all_distinct.3" expl="3. loop invariant init"
      sum="f2a72af703403a88e25a697c4ddfa52a"
-      proved="true"
-      expanded="true"
-      shape="loop invariant initNainfix =agetV1V4agetV1V5INainfix =V4V5Iainfix &lt;V5c0Aainfix &lt;=c0V5Iainfix &lt;V4c0Aainfix &lt;=c0V4FIainfix &lt;=c0V3Lainfix -V0c1Iainfix &lt;=c0V2Iainfix &gt;=V2c0Iainfix &lt;agetV1V6V2Aainfix &lt;=c0agetV1V6Iainfix &lt;V6V0Aainfix &lt;=c0V6FAainfix &lt;=c0V2Aainfix &lt;=c0V0F">
-      <label
-       name="expl:VC for all_distinct"/>
-      <proof
-       prover="0"
-       timelimit="6"
-       memlimit="1000"
-       obsolete="false"
-       archived="false">
+      expanded="true">
+      <label name="expl:VC for all_distinct"/>
+      <proof prover="0">
       <result status="valid" time="0.02"/>
      </proof>
     </goal>
-     <goal
-      name="WP_parameter all_distinct.4"
-      locfile="../all_distinct.mlw"
-      loclnum="13" loccnumb="6" loccnume="18"
-      expl="4. loop invariant init"
+     <goal name="WP_parameter all_distinct.4" expl="4. loop invariant init"
      sum="ce1590976f77ddc643d8fbdac4674fb8"
-      proved="true"
-      expanded="true"
-      shape="loop invariant initainfix =agetV1V5V4Aainfix &lt;V5c0Aainfix &lt;=c0V5Eqainfix =agetaconstaFalseV4aTrueIainfix &lt;V4V2Aainfix &lt;=c0V4FIainfix &lt;=c0V3Lainfix -V0c1Iainfix &lt;=c0V2Iainfix &gt;=V2c0Iainfix &lt;agetV1V6V2Aainfix &lt;=c0agetV1V6Iainfix &lt;V6V0Aainfix &lt;=c0V6FAainfix &lt;=c0V2Aainfix &lt;=c0V0F">
-      <label
-       name="expl:VC for all_distinct"/>
-      <proof
-       prover="0"
-       timelimit="6"
-       memlimit="1000"
-       obsolete="false"
-       archived="false">
+      expanded="true">
+      <label name="expl:VC for all_distinct"/>
+      <proof prover="0">
       <result status="valid" time="0.02"/>
      </proof>
     </goal>
-     <goal
-      name="WP_parameter all_distinct.5"
-      locfile="../all_distinct.mlw"
-      loclnum="13" loccnumb="6" loccnume="18"
-      expl="5. index in array bounds"
+     <goal name="WP_parameter all_distinct.5" expl="5. index in array bounds"
      sum="f1a081032a623863f610a04ad56ba8cb"
-      proved="true"
-      expanded="true"
-      shape="index in array boundsainfix &lt;V5V0Aainfix &lt;=c0V5Iainfix =agetV1V7V6Aainfix &lt;V7V5Aainfix &lt;=c0V7Eqainfix =agetV4V6aTrueIainfix &lt;V6V2Aainfix &lt;=c0V6FANainfix =agetV1V8agetV1V9INainfix =V8V9Iainfix &lt;V9V5Aainfix &lt;=c0V9Iainfix &lt;V8V5Aainfix &lt;=c0V8FIainfix &lt;=V5V3Aainfix &lt;=c0V5FFIainfix &lt;=c0V3Lainfix -V0c1Iainfix &lt;=c0V2Iainfix &gt;=V2c0Iainfix &lt;agetV1V10V2Aainfix &lt;=c0agetV1V10Iainfix &lt;V10V0Aainfix &lt;=c0V10FAainfix &lt;=c0V2Aainfix &lt;=c0V0F">
-      <label
-       name="expl:VC for all_distinct"/>
-      <proof
-       prover="0"
-       timelimit="6"
-       memlimit="1000"
-       obsolete="false"
-       archived="false">
+      expanded="true">
+      <label name="expl:VC for all_distinct"/>
+      <proof prover="0">
       <result status="valid" time="0.01"/>
      </proof>
     </goal>
-     <goal
-      name="WP_parameter all_distinct.6"
-      locfile="../all_distinct.mlw"
-      loclnum="13" loccnumb="6" loccnume="18"
-      expl="6. type invariant"
+     <goal name="WP_parameter all_distinct.6" expl="6. type invariant"
      sum="0a3d6cdd22086870ccdd20acf950acb1"
-      proved="true"
-      expanded="true"
-      shape="type invariantainfix &lt;=c0V2LagetV1V5Iainfix &lt;V5V0Aainfix &lt;=c0V5Iainfix =agetV1V8V7Aainfix &lt;V8V5Aainfix &lt;=c0V8Eqainfix =agetV4V7aTrueIainfix &lt;V7V2Aainfix &lt;=c0V7FANainfix =agetV1V9agetV1V10INainfix =V9V10Iainfix &lt;V10V5Aainfix &lt;=c0V10Iainfix &lt;V9V5Aainfix &lt;=c0V9FIainfix &lt;=V5V3Aainfix &lt;=c0V5FFIainfix &lt;=c0V3Lainfix -V0c1Iainfix &lt;=c0V2Iainfix &gt;=V2c0Iainfix &lt;agetV1V11V2Aainfix &lt;=c0agetV1V11Iainfix &lt;V11V0Aainfix &lt;=c0V11FAainfix &lt;=c0V2Aainfix &lt;=c0V0F">
-      <label
-       name="expl:VC for all_distinct"/>
-      <proof
-       prover="0"
-       timelimit="6"
-       memlimit="1000"
-       obsolete="false"
-       archived="false">
+      expanded="true">
+      <label name="expl:VC for all_distinct"/>
+      <proof prover="0">
       <result status="valid" time="0.02"/>
      </proof>
     </goal>
-     <goal
-      name="WP_parameter all_distinct.7"
-      locfile="../all_distinct.mlw"
-      loclnum="13" loccnumb="6" loccnume="18"
-      expl="7. index in array bounds"
+     <goal name="WP_parameter all_distinct.7" expl="7. index in array bounds"
      sum="025eb7e13690ff51b15e41ac95352a8f"
-      proved="true"
-      expanded="true"
-      shape="index in array boundsainfix &lt;V6V2Aainfix &lt;=c0V6Iainfix &lt;=c0V2LagetV1V5Iainfix &lt;V5V0Aainfix &lt;=c0V5Iainfix =agetV1V8V7Aainfix &lt;V8V5Aainfix &lt;=c0V8Eqainfix =agetV4V7aTrueIainfix &lt;V7V2Aainfix &lt;=c0V7FANainfix =agetV1V9agetV1V10INainfix =V9V10Iainfix &lt;V10V5Aainfix &lt;=c0V10Iainfix &lt;V9V5Aainfix &lt;=c0V9FIainfix &lt;=V5V3Aainfix &lt;=c0V5FFIainfix &lt;=c0V3Lainfix -V0c1Iainfix &lt;=c0V2Iainfix &gt;=V2c0Iainfix &lt;agetV1V11V2Aainfix &lt;=c0agetV1V11Iainfix &lt;V11V0Aainfix &lt;=c0V11FAainfix &lt;=c0V2Aainfix &lt;=c0V0F">
-      <label
-       name="expl:VC for all_distinct"/>
-      <proof
-       prover="0"
-       timelimit="6"
-       memlimit="1000"
-       obsolete="false"
-       archived="false">
+      expanded="true">
+      <label name="expl:VC for all_distinct"/>
+      <proof prover="0">
       <result status="valid" time="0.02"/>
      </proof>
     </goal>
-     <goal
-      name="WP_parameter all_distinct.8"
-      locfile="../all_distinct.mlw"
-      loclnum="13" loccnumb="6" loccnume="18"
-      expl="8. postcondition"
+     <goal name="WP_parameter all_distinct.8" expl="8. postcondition"
      sum="abed04285d21c6c786ac5473f4cbb8fe"
-      proved="true"
-      expanded="true"
-      shape="postconditionNNainfix =agetV1V7agetV1V8INainfix =V7V8Iainfix &lt;V8V0Aainfix &lt;=c0V8Iainfix &lt;V7V0Aainfix &lt;=c0V7FIainfix =agetV4V6aTrueIainfix &lt;V6V2Aainfix &lt;=c0V6Aainfix &lt;=c0V2LagetV1V5Iainfix &lt;V5V0Aainfix &lt;=c0V5Iainfix =agetV1V10V9Aainfix &lt;V10V5Aainfix &lt;=c0V10Eqainfix =agetV4V9aTrueIainfix &lt;V9V2Aainfix &lt;=c0V9FANainfix =agetV1V11agetV1V12INainfix =V11V12Iainfix &lt;V12V5Aainfix &lt;=c0V12Iainfix &lt;V11V5Aainfix &lt;=c0V11FIainfix &lt;=V5V3Aainfix &lt;=c0V5FFIainfix &lt;=c0V3Lainfix -V0c1Iainfix &lt;=c0V2Iainfix &gt;=V2c0Iainfix &lt;agetV1V13V2Aainfix &lt;=c0agetV1V13Iainfix &lt;V13V0Aainfix &lt;=c0V13FAainfix &lt;=c0V2Aainfix &lt;=c0V0F">
-      <label
-       name="expl:VC for all_distinct"/>
-      <proof
-       prover="0"
-       timelimit="6"
-       memlimit="1000"
-       obsolete="false"
-       archived="false">
+      expanded="true">
+      <label name="expl:VC for all_distinct"/>
+      <proof prover="0">
       <result status="valid" time="0.01"/>
      </proof>
     </goal>
-     <goal
-      name="WP_parameter all_distinct.9"
-      locfile="../all_distinct.mlw"
-      loclnum="13" loccnumb="6" loccnume="18"
-      expl="9. index in array bounds"
+     <goal name="WP_parameter all_distinct.9" expl="9. index in array bounds"
      sum="bd4aee6919c6b60b4e0886f97d37c2c3"
-      proved="true"
-      expanded="true"
-      shape="index in array boundsainfix &lt;V6V2Aainfix &lt;=c0V6INainfix =agetV4V6aTrueIainfix &lt;V6V2Aainfix &lt;=c0V6Aainfix &lt;=c0V2LagetV1V5Iainfix &lt;V5V0Aainfix &lt;=c0V5Iainfix =agetV1V8V7Aainfix &lt;V8V5Aainfix &lt;=c0V8Eqainfix =agetV4V7aTrueIainfix &lt;V7V2Aainfix &lt;=c0V7FANainfix =agetV1V9agetV1V10INainfix =V9V10Iainfix &lt;V10V5Aainfix &lt;=c0V10Iainfix &lt;V9V5Aainfix &lt;=c0V9FIainfix &lt;=V5V3Aainfix &lt;=c0V5FFIainfix &lt;=c0V3Lainfix -V0c1Iainfix &lt;=c0V2Iainfix &gt;=V2c0Iainfix &lt;agetV1V11V2Aainfix &lt;=c0agetV1V11Iainfix &lt;V11V0Aainfix &lt;=c0V11FAainfix &lt;=c0V2Aainfix &lt;=c0V0F">
-      <label
-       name="expl:VC for all_distinct"/>
-      <proof
-       prover="0"
-       timelimit="6"
-       memlimit="1000"
-       obsolete="false"
-       archived="false">
+      expanded="true">
+      <label name="expl:VC for all_distinct"/>
+      <proof prover="0">
       <result status="valid" time="0.02"/>
      </proof>
     </goal>
-     <goal
-      name="WP_parameter all_distinct.10"
-      locfile="../all_distinct.mlw"
-      loclnum="13" loccnumb="6" loccnume="18"
+     <goal name="WP_parameter all_distinct.10"
      expl="10. loop invariant preservation"
      sum="b5160b76e1b3e97ac33d9a4547eb9ad5"
-      proved="true"
-      expanded="true"
-      shape="loop invariant preservationNainfix =agetV1V8agetV1V9INainfix =V8V9Iainfix &lt;V9ainfix +V5c1Aainfix &lt;=c0V9Iainfix &lt;V8ainfix +V5c1Aainfix &lt;=c0V8FIainfix =V7asetV4V6aTrueAainfix &lt;=c0V2FIainfix &lt;V6V2Aainfix &lt;=c0V6INainfix =agetV4V6aTrueIainfix &lt;V6V2Aainfix &lt;=c0V6Aainfix &lt;=c0V2LagetV1V5Iainfix &lt;V5V0Aainfix &lt;=c0V5Iainfix =agetV1V11V10Aainfix &lt;V11V5Aainfix &lt;=c0V11Eqainfix =agetV4V10aTrueIainfix &lt;V10V2Aainfix &lt;=c0V10FANainfix =agetV1V12agetV1V13INainfix =V12V13Iainfix &lt;V13V5Aainfix &lt;=c0V13Iainfix &lt;V12V5Aainfix &lt;=c0V12FIainfix &lt;=V5V3Aainfix &lt;=c0V5FFIainfix &lt;=c0V3Lainfix -V0c1Iainfix &lt;=c0V2Iainfix &gt;=V2c0Iainfix &lt;agetV1V14V2Aainfix &lt;=c0agetV1V14Iainfix &lt;V14V0Aainfix &lt;=c0V14FAainfix &lt;=c0V2Aainfix &lt;=c0V0F">
-      <label
-       name="expl:VC for all_distinct"/>
-      <proof
-       prover="0"
-       timelimit="6"
-       memlimit="1000"
-       obsolete="false"
-       archived="false">
+      expanded="true">
+      <label name="expl:VC for all_distinct"/>
+      <proof prover="0">
       <result status="valid" time="0.02"/>
      </proof>
     </goal>
-     <goal
-      name="WP_parameter all_distinct.11"
-      locfile="../all_distinct.mlw"
-      loclnum="13" loccnumb="6" loccnume="18"
+     <goal name="WP_parameter all_distinct.11"
      expl="11. loop invariant preservation"
      sum="646cfed7474750745a5a8bffbd5d0672"
-      proved="true"
-      expanded="true"
-      shape="loop invariant preservationainfix =agetV1V9V8Aainfix &lt;V9ainfix +V5c1Aainfix &lt;=c0V9Eqainfix =agetV7V8aTrueIainfix &lt;V8V2Aainfix &lt;=c0V8FIainfix =V7asetV4V6aTrueAainfix &lt;=c0V2FIainfix &lt;V6V2Aainfix &lt;=c0V6INainfix =agetV4V6aTrueIainfix &lt;V6V2Aainfix &lt;=c0V6Aainfix &lt;=c0V2LagetV1V5Iainfix &lt;V5V0Aainfix &lt;=c0V5Iainfix =agetV1V11V10Aainfix &lt;V11V5Aainfix &lt;=c0V11Eqainfix =agetV4V10aTrueIainfix &lt;V10V2Aainfix &lt;=c0V10FANainfix =agetV1V12agetV1V13INainfix =V12V13Iainfix &lt;V13V5Aainfix &lt;=c0V13Iainfix &lt;V12V5Aainfix &lt;=c0V12FIainfix &lt;=V5V3Aainfix &lt;=c0V5FFIainfix &lt;=c0V3Lainfix -V0c1Iainfix &lt;=c0V2Iainfix &gt;=V2c0Iainfix &lt;agetV1V14V2Aainfix &lt;=c0agetV1V14Iainfix &lt;V14V0Aainfix &lt;=c0V14FAainfix &lt;=c0V2Aainfix &lt;=c0V0F">
-      <label
-       name="expl:VC for all_distinct"/>
-      <proof
-       prover="0"
-       timelimit="6"
-       memlimit="1000"
-       obsolete="false"
-       archived="false">
+      expanded="true">
+      <label name="expl:VC for all_distinct"/>
+      <proof prover="0">
       <result status="valid" time="0.02"/>
      </proof>
     </goal>
-     <goal
-      name="WP_parameter all_distinct.12"
-      locfile="../all_distinct.mlw"
-      loclnum="13" loccnumb="6" loccnume="18"
-      expl="12. postcondition"
+     <goal name="WP_parameter all_distinct.12" expl="12. postcondition"
      sum="3010bad4861a5d4b8f8591549feced61"
-      proved="true"
-      expanded="true"
-      shape="postconditionNainfix =agetV1V5agetV1V6INainfix =V5V6Iainfix &lt;V6V0Aainfix &lt;=c0V6Iainfix &lt;V5V0Aainfix &lt;=c0V5FIainfix =agetV1V8V7Aainfix &lt;V8ainfix +V3c1Aainfix &lt;=c0V8Eqainfix =agetV4V7aTrueIainfix &lt;V7V2Aainfix &lt;=c0V7FANainfix =agetV1V9agetV1V10INainfix =V9V10Iainfix &lt;V10ainfix +V3c1Aainfix &lt;=c0V10Iainfix &lt;V9ainfix +V3c1Aainfix &lt;=c0V9FFIainfix &lt;=c0V3Lainfix -V0c1Iainfix &lt;=c0V2Iainfix &gt;=V2c0Iainfix &lt;agetV1V11V2Aainfix &lt;=c0agetV1V11Iainfix &lt;V11V0Aainfix &lt;=c0V11FAainfix &lt;=c0V2Aainfix &lt;=c0V0F">
-      <label
-       name="expl:VC for all_distinct"/>
-      <proof
-       prover="0"
-       timelimit="6"
-       memlimit="1000"
-       obsolete="false"
-       archived="false">
+      expanded="true">
+      <label name="expl:VC for all_distinct"/>
+      <proof prover="0">
       <result status="valid" time="0.01"/>
      </proof>
     </goal>

--- a/examples/all_distinct/why3shapes.dat
+++ b/examples/all_distinct/why3shapes.dat
+9cd8ab30056665aa598b63118511deb6 Nainfix =agetV1V5agetV1V6INainfix =V5V6Iainfix <V6V0Aainfix <=c0V6Iainfix <V5V0Aainfix <=c0V5FIainfix =agetV1V8V7Aainfix <V8ainfix +V3c1Aainfix <=c0V8Eqainfix =agetV4V7aTrueIainfix <V7V2Aainfix <=c0V7FANainfix =agetV1V9agetV1V10INainfix =V9V10Iainfix <V10ainfix +V3c1Aainfix <=c0V10Iainfix <V9ainfix +V3c1Aainfix <=c0V9FAiainfix =agetV1V15V14Aainfix <V15ainfix +V11c1Aainfix <=c0V15Eqainfix =agetV13V14aTrueIainfix <V14V2Aainfix <=c0V14FANainfix =agetV1V16agetV1V17INainfix =V16V17Iainfix <V17ainfix +V11c1Aainfix <=c0V17Iainfix <V16ainfix +V11c1Aainfix <=c0V16FIainfix =V13asetV4V12aTrueAainfix <=c0V2FAainfix <V12V2Aainfix <=c0V12NNainfix =agetV1V18agetV1V19INainfix =V18V19Iainfix <V19V0Aainfix <=c0V19Iainfix <V18V0Aainfix <=c0V18Fainfix =agetV4V12aTrueAainfix <V12V2Aainfix <=c0V12Aainfix <=c0V2LagetV1V11Aainfix <V11V0Aainfix <=c0V11Iainfix =agetV1V21V20Aainfix <V21V11Aainfix <=c0V21Eqainfix =agetV4V20aTrueIainfix <V20V2Aainfix <=c0V20FANainfix =agetV1V22agetV1V23INainfix =V22V23Iainfix <V23V11Aainfix <=c0V23Iainfix <V22V11Aainfix <=c0V22FIainfix <=V11V3Aainfix <=c0V11FFAainfix =agetV1V25V24Aainfix <V25c0Aainfix <=c0V25Eqainfix =agetaconstaFalseV24aTrueIainfix <V24V2Aainfix <=c0V24FANainfix =agetV1V26agetV1V27INainfix =V26V27Iainfix <V27c0Aainfix <=c0V27Iainfix <V26c0Aainfix <=c0V26FIainfix <=c0V3ANainfix =agetV1V28agetV1V29INainfix =V28V29Iainfix <V29V0Aainfix <=c0V29Iainfix <V28V0Aainfix <=c0V28FIainfix >c0V3Lainfix -V0c1Iainfix <=c0V2Aainfix >=V2c0Iainfix <agetV1V30V2Aainfix <=c0agetV1V30Iainfix <V30V0Aainfix <=c0V30FAainfix <=c0V2Aainfix <=c0V0F
+169dead4ca86d70a93945d7a849a4ddf array creation sizeainfix >=V2c0Iainfix <agetV1V3V2Aainfix <=c0agetV1V3Iainfix <V3V0Aainfix <=c0V3FAainfix <=c0V2Aainfix <=c0V0F
+8d038b937a7ed02cbabc2d03293374eb postconditionNainfix =agetV1V4agetV1V5INainfix =V4V5Iainfix <V5V0Aainfix <=c0V5Iainfix <V4V0Aainfix <=c0V4FIainfix >c0V3Lainfix -V0c1Iainfix <=c0V2Iainfix >=V2c0Iainfix <agetV1V6V2Aainfix <=c0agetV1V6Iainfix <V6V0Aainfix <=c0V6FAainfix <=c0V2Aainfix <=c0V0F
+f2a72af703403a88e25a697c4ddfa52a loop invariant initNainfix =agetV1V4agetV1V5INainfix =V4V5Iainfix <V5c0Aainfix <=c0V5Iainfix <V4c0Aainfix <=c0V4FIainfix <=c0V3Lainfix -V0c1Iainfix <=c0V2Iainfix >=V2c0Iainfix <agetV1V6V2Aainfix <=c0agetV1V6Iainfix <V6V0Aainfix <=c0V6FAainfix <=c0V2Aainfix <=c0V0F
+ce1590976f77ddc643d8fbdac4674fb8 loop invariant initainfix =agetV1V5V4Aainfix <V5c0Aainfix <=c0V5Eqainfix =agetaconstaFalseV4aTrueIainfix <V4V2Aainfix <=c0V4FIainfix <=c0V3Lainfix -V0c1Iainfix <=c0V2Iainfix >=V2c0Iainfix <agetV1V6V2Aainfix <=c0agetV1V6Iainfix <V6V0Aainfix <=c0V6FAainfix <=c0V2Aainfix <=c0V0F
+f1a081032a623863f610a04ad56ba8cb index in array boundsainfix <V5V0Aainfix <=c0V5Iainfix =agetV1V7V6Aainfix <V7V5Aainfix <=c0V7Eqainfix =agetV4V6aTrueIainfix <V6V2Aainfix <=c0V6FANainfix =agetV1V8agetV1V9INainfix =V8V9Iainfix <V9V5Aainfix <=c0V9Iainfix <V8V5Aainfix <=c0V8FIainfix <=V5V3Aainfix <=c0V5FFIainfix <=c0V3Lainfix -V0c1Iainfix <=c0V2Iainfix >=V2c0Iainfix <agetV1V10V2Aainfix <=c0agetV1V10Iainfix <V10V0Aainfix <=c0V10FAainfix <=c0V2Aainfix <=c0V0F
+0a3d6cdd22086870ccdd20acf950acb1 type invariantainfix <=c0V2LagetV1V5Iainfix <V5V0Aainfix <=c0V5Iainfix =agetV1V8V7Aainfix <V8V5Aainfix <=c0V8Eqainfix =agetV4V7aTrueIainfix <V7V2Aainfix <=c0V7FANainfix =agetV1V9agetV1V10INainfix =V9V10Iainfix <V10V5Aainfix <=c0V10Iainfix <V9V5Aainfix <=c0V9FIainfix <=V5V3Aainfix <=c0V5FFIainfix <=c0V3Lainfix -V0c1Iainfix <=c0V2Iainfix >=V2c0Iainfix <agetV1V11V2Aainfix <=c0agetV1V11Iainfix <V11V0Aainfix <=c0V11FAainfix <=c0V2Aainfix <=c0V0F
+025eb7e13690ff51b15e41ac95352a8f index in array boundsainfix <V6V2Aainfix <=c0V6Iainfix <=c0V2LagetV1V5Iainfix <V5V0Aainfix <=c0V5Iainfix =agetV1V8V7Aainfix <V8V5Aainfix <=c0V8Eqainfix =agetV4V7aTrueIainfix <V7V2Aainfix <=c0V7FANainfix =agetV1V9agetV1V10INainfix =V9V10Iainfix <V10V5Aainfix <=c0V10Iainfix <V9V5Aainfix <=c0V9FIainfix <=V5V3Aainfix <=c0V5FFIainfix <=c0V3Lainfix -V0c1Iainfix <=c0V2Iainfix >=V2c0Iainfix <agetV1V11V2Aainfix <=c0agetV1V11Iainfix <V11V0Aainfix <=c0V11FAainfix <=c0V2Aainfix <=c0V0F
+abed04285d21c6c786ac5473f4cbb8fe postconditionNNainfix =agetV1V7agetV1V8INainfix =V7V8Iainfix <V8V0Aainfix <=c0V8Iainfix <V7V0Aainfix <=c0V7FIainfix =agetV4V6aTrueIainfix <V6V2Aainfix <=c0V6Aainfix <=c0V2LagetV1V5Iainfix <V5V0Aainfix <=c0V5Iainfix =agetV1V10V9Aainfix <V10V5Aainfix <=c0V10Eqainfix =agetV4V9aTrueIainfix <V9V2Aainfix <=c0V9FANainfix =agetV1V11agetV1V12INainfix =V11V12Iainfix <V12V5Aainfix <=c0V12Iainfix <V11V5Aainfix <=c0V11FIainfix <=V5V3Aainfix <=c0V5FFIainfix <=c0V3Lainfix -V0c1Iainfix <=c0V2Iainfix >=V2c0Iainfix <agetV1V13V2Aainfix <=c0agetV1V13Iainfix <V13V0Aainfix <=c0V13FAainfix <=c0V2Aainfix <=c0V0F
+bd4aee6919c6b60b4e0886f97d37c2c3 index in array boundsainfix <V6V2Aainfix <=c0V6INainfix =agetV4V6aTrueIainfix <V6V2Aainfix <=c0V6Aainfix <=c0V2LagetV1V5Iainfix <V5V0Aainfix <=c0V5Iainfix =agetV1V8V7Aainfix <V8V5Aainfix <=c0V8Eqainfix =agetV4V7aTrueIainfix <V7V2Aainfix <=c0V7FANainfix =agetV1V9agetV1V10INainfix =V9V10Iainfix <V10V5Aainfix <=c0V10Iainfix <V9V5Aainfix <=c0V9FIainfix <=V5V3Aainfix <=c0V5FFIainfix <=c0V3Lainfix -V0c1Iainfix <=c0V2Iainfix >=V2c0Iainfix <agetV1V11V2Aainfix <=c0agetV1V11Iainfix <V11V0Aainfix <=c0V11FAainfix <=c0V2Aainfix <=c0V0F
+b5160b76e1b3e97ac33d9a4547eb9ad5 loop invariant preservationNainfix =agetV1V8agetV1V9INainfix =V8V9Iainfix <V9ainfix +V5c1Aainfix <=c0V9Iainfix <V8ainfix +V5c1Aainfix <=c0V8FIainfix =V7asetV4V6aTrueAainfix <=c0V2FIainfix <V6V2Aainfix <=c0V6INainfix =agetV4V6aTrueIainfix <V6V2Aainfix <=c0V6Aainfix <=c0V2LagetV1V5Iainfix <V5V0Aainfix <=c0V5Iainfix =agetV1V11V10Aainfix <V11V5Aainfix <=c0V11Eqainfix =agetV4V10aTrueIainfix <V10V2Aainfix <=c0V10FANainfix =agetV1V12agetV1V13INainfix =V12V13Iainfix <V13V5Aainfix <=c0V13Iainfix <V12V5Aainfix <=c0V12FIainfix <=V5V3Aainfix <=c0V5FFIainfix <=c0V3Lainfix -V0c1Iainfix <=c0V2Iainfix >=V2c0Iainfix <agetV1V14V2Aainfix <=c0agetV1V14Iainfix <V14V0Aainfix <=c0V14FAainfix <=c0V2Aainfix <=c0V0F
+646cfed7474750745a5a8bffbd5d0672 loop invariant preservationainfix =agetV1V9V8Aainfix <V9ainfix +V5c1Aainfix <=c0V9Eqainfix =agetV7V8aTrueIainfix <V8V2Aainfix <=c0V8FIainfix =V7asetV4V6aTrueAainfix <=c0V2FIainfix <V6V2Aainfix <=c0V6INainfix =agetV4V6aTrueIainfix <V6V2Aainfix <=c0V6Aainfix <=c0V2LagetV1V5Iainfix <V5V0Aainfix <=c0V5Iainfix =agetV1V11V10Aainfix <V11V5Aainfix <=c0V11Eqainfix =agetV4V10aTrueIainfix <V10V2Aainfix <=c0V10FANainfix =agetV1V12agetV1V13INainfix =V12V13Iainfix <V13V5Aainfix <=c0V13Iainfix <V12V5Aainfix <=c0V12FIainfix <=V5V3Aainfix <=c0V5FFIainfix <=c0V3Lainfix -V0c1Iainfix <=c0V2Iainfix >=V2c0Iainfix <agetV1V14V2Aainfix <=c0agetV1V14Iainfix <V14V0Aainfix <=c0V14FAainfix <=c0V2Aainfix <=c0V0F
+3010bad4861a5d4b8f8591549feced61 postconditionNainfix =agetV1V5agetV1V6INainfix =V5V6Iainfix <V6V0Aainfix <=c0V6Iainfix <V5V0Aainfix <=c0V5FIainfix =agetV1V8V7Aainfix <V8ainfix +V3c1Aainfix <=c0V8Eqainfix =agetV4V7aTrueIainfix <V7V2Aainfix <=c0V7FANainfix =agetV1V9agetV1V10INainfix =V9V10Iainfix <V10ainfix +V3c1Aainfix <=c0V10Iainfix <V9ainfix +V3c1Aainfix <=c0V9FFIainfix <=c0V3Lainfix -V0c1Iainfix <=c0V2Iainfix >=V2c0Iainfix <agetV1V11V2Aainfix <=c0agetV1V11Iainfix <V11V0Aainfix <=c0V11FAainfix <=c0V2Aainfix <=c0V0F
--- a/examples/arm/why3session.xml
+++ b/examples/arm/why3session.xml
--- a/examples/arm/why3shapes.dat
+++ b/examples/arm/why3shapes.dat
+12ad10e0643d819dcdf614beb2a7db7f iainfix <=V6c45Aainfix =V7c9Aainfix <=c0V0iainfix <ainfix -c10V16ainfix -c10V5Aainfix <=c0ainfix -c10V5Aainfix <=ainfix *c2V12ainfix *ainfix -V16c2ainfix -V16c1Aainfix =V10ainfix -V16c2AainvV14Aainfix <=V16c11Aainfix <=c2V16Iainfix =V16ainfix +V5c1Fainfix <V22V11Aainfix <=c0V11Aainfix <=ainfix *c2V17ainfix +ainfix *ainfix -V5c2ainfix -V5c1ainfix *c2ainfix -V5V22Aainvamk arrayV0V21Aainfix <=V22V5Aainfix <=c1V22Iainfix =V22ainfix -V11c1FIainfix =V21asetV19V20agetV13V11Aainfix <=c0V0FAainfix <V20V0Aainfix <=c0V20Lainfix -V11c1Iainfix =V19asetV13V11agetV13V18Aainfix <=c0V0FAainfix <V11V0Aainfix <=c0V11Aainfix <V18V0Aainfix <=c0V18Lainfix -V11c1Aainfix <V11V0Aainfix <=c0V11Iainfix =V17ainfix +V12c1Fainfix <agetV13V11agetV13V15Aainfix <V11V0Aainfix <=c0V11Aainfix <V15V0Aainfix <=c0V15Aainfix <=c0V0Lainfix -V11c1Iainfix <=ainfix *c2V12ainfix +ainfix *ainfix -V5c2ainfix -V5c1ainfix *c2ainfix -V5V11AainvV14Aainfix <=V11V5Aainfix <=c1V11Lamk arrayV0V13FAainfix <=ainfix *c2V6ainfix +ainfix *ainfix -V5c2ainfix -V5c1ainfix *c2ainfix -V5V5AainvV9Aainfix <=V5V5Aainfix <=c1V5Iainfix =V10ainfix +V7c1Fainfix <=V5c10Iainfix <=ai