From 589f029747709b25009ff3cb15199193b26c5b4f Mon Sep 17 00:00:00 2001
From: Jean-Christophe <Jean-Christophe.Filliatre@lri.fr>
Date: Mon, 4 Mar 2013 14:31:38 +0100
Subject: [PATCH] more use of module array.ArraySwap in examples

---
 examples/quicksort.mlw                        |   8 +-
 examples/quicksort/why3session.xml            | 176 +++++++--------
 examples/selection_sort.mlw                   |   8 +-
 examples/selection_sort/why3session.xml       | 209 +++++++++++-------
 examples/vstte12_two_way_sort.mlw             |   8 +-
 examples/vstte12_two_way_sort/why3session.xml |  98 ++++----
 6 files changed, 243 insertions(+), 264 deletions(-)

diff --git a/examples/quicksort.mlw b/examples/quicksort.mlw
index ccd43381d..6222317b8 100644
--- a/examples/quicksort.mlw
+++ b/examples/quicksort.mlw
@@ -11,16 +11,10 @@ module Quicksort
   use import ref.Ref
   use import array.Array
   use import array.ArraySorted
+  use import array.ArraySwap
   use import array.ArrayPermut
   use import array.ArrayEq
 
-  let swap (t:array int) (i:int) (j:int)
-    requires { 0 <= i < length t /\ 0 <= j < length t }
-    ensures { exchange (old t) t i j }
-  = let v = t[i] in
-    t[i] <- t[j];
-    t[j] <- v
-
   let rec quick_rec (t:array int) (l:int) (r:int) : unit variant { 1+r-l }
     requires { 0 <= l /\ r < length t }
     ensures { sorted_sub t l (r+1) /\ permut_sub (old t) t l (r+1) }
diff --git a/examples/quicksort/why3session.xml b/examples/quicksort/why3session.xml
index 6103a5059..d802b913b 100644
--- a/examples/quicksort/why3session.xml
+++ b/examples/quicksort/why3session.xml
@@ -24,39 +24,19 @@
  <file
   name="../quicksort.mlw"
   verified="true"
-  expanded="true">
+  expanded="false">
   <theory
    name="Quicksort"
    locfile="../quicksort.mlw"
    loclnum="8" loccnumb="7" loccnume="16"
    verified="true"
-   expanded="true">
-   <goal
-    name="WP_parameter swap"
-    locfile="../quicksort.mlw"
-    loclnum="17" loccnumb="6" loccnume="10"
-    expl="VC for swap"
-    sum="a0e6aa0a260c53425d59522095d19ea6"
-    proved="true"
-    expanded="false"
-    shape="aexchangeV3V5V1V2Iainfix =V5asetV4V2agetV3V1Aainfix &lt;=c0V0FAainfix &lt;V2V0Aainfix &lt;=c0V2Iainfix =V4asetV3V1agetV3V2Aainfix &lt;=c0V0FAainfix &lt;V1V0Aainfix &lt;=c0V1Aainfix &lt;V2V0Aainfix &lt;=c0V2Aainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V2V0Aainfix &lt;=c0V2Aainfix &lt;V1V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
-    <label
-     name="expl:VC for swap"/>
-    <proof
-     prover="0"
-     timelimit="29"
-     memlimit="0"
-     obsolete="false"
-     archived="false">
-     <result status="valid" time="0.02"/>
-    </proof>
-   </goal>
+   expanded="false">
    <goal
     name="WP_parameter quick_rec"
     locfile="../quicksort.mlw"
-    loclnum="24" loccnumb="10" loccnume="19"
+    loclnum="18" loccnumb="10" loccnume="19"
     expl="VC for quick_rec"
-    sum="4ddc5e699aa1031a1ecbbcd81c53fc78"
+    sum="34f53c514e404f0a819c420edb3b6bc6"
     proved="true"
     expanded="false"
     shape="iainfix &lt;V1V2apermut_subV3V9V1ainfix +V2c1Aasorted_subV9V1ainfix +V2c1Iapermut_subV8V9ainfix +V5c1ainfix +V2c1Aasorted_subV9ainfix +V5c1ainfix +V2c1Aainfix &lt;=c0V0FAainfix &lt;V2V0Aainfix &lt;=c0ainfix +V5c1Aainfix &lt;ainfix -ainfix +c1V2ainfix +V5c1ainfix -ainfix +c1V2V1Aainfix &lt;=c0ainfix -ainfix +c1V2V1Iapermut_subV7V8V1ainfix +ainfix -V5c1c1Aasorted_subV8V1ainfix +ainfix -V5c1c1Aainfix &lt;=c0V0FAainfix &lt;ainfix -V5c1V0Aainfix &lt;=c0V1Aainfix &lt;ainfix -ainfix +c1ainfix -V5c1V1ainfix -ainfix +c1V2V1Aainfix &lt;=c0ainfix -ainfix +c1V2V1IaexchangeV6V7V1V5Aainfix &lt;=c0V0FAainfix &lt;V5V0Aainfix &lt;=c0V5Aainfix &lt;V1V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0Iainfix &lt;V5ainfix +V2c1Aainfix &lt;=V1V5Aainfix =agetV6V1V4Aapermut_subV3V6V1ainfix +V2c1Aainfix &gt;=agetV6V10V4Iainfix &lt;V10ainfix +V2c1Aainfix &lt;V5V10FAainfix &lt;agetV6V11V4Iainfix &lt;=V11V5Aainfix &lt;V1V11FAiainfix &lt;agetV6V12V4ainfix &lt;V13ainfix +V12c1Aainfix &lt;=V1V13Aainfix =agetV14V1V4Aapermut_subV3V14V1ainfix +V2c1Aainfix &gt;=agetV14V15V4Iainfix &lt;V15ainfix +V12c1Aainfix &lt;V13V15FAainfix &lt;agetV14V16V4Iainfix &lt;=V16V13Aainfix &lt;V1V16FIaexchangeV6V14V12V13Aainfix &lt;=c0V0FAainfix &lt;V13V0Aainfix &lt;=c0V13Aainfix &lt;V12V0Aainfix &lt;=c0V12Iainfix =V13ainfix +V5c1Fainfix &lt;V5ainfix +V12c1Aainfix &lt;=V1V5Aainfix =agetV6V1V4Aapermut_subV3V6V1ainfix +V2c1Aainfix &gt;=agetV6V17V4Iainfix &lt;V17ainfix +V12c1Aainfix &lt;V5V17FAainfix &lt;agetV6V18V4Iainfix &lt;=V18V5Aainfix &lt;V1V18FAainfix &lt;V12V0Aainfix &lt;=c0V12Aainfix &lt;=c0V0Iainfix &lt;V5V12Aainfix &lt;=V1V5Aainfix =agetV6V1V4Aapermut_subV3V6V1ainfix +V2c1Aainfix &gt;=agetV6V19V4Iainfix &lt;V19V12Aainfix &lt;V5V19FAainfix &lt;agetV6V20V4Iainfix &lt;=V20V5Aainfix &lt;V1V20FIainfix &lt;=V12V2Aainfix &lt;=ainfix +V1c1V12FFAainfix &lt;V1ainfix +V1c1Aainfix &lt;=V1V1Aainfix =agetV3V1V4Aapermut_subV3V3V1ainfix +V2c1Aainfix &gt;=agetV3V21V4Iainfix &lt;V21ainfix +V1c1Aainfix &lt;V1V21FAainfix &lt;agetV3V22V4Iainfix &lt;=V22V1Aainfix &lt;V1V22FIainfix &lt;=ainfix +V1c1V2Aapermut_subV3V25V1ainfix +V2c1Aasorted_subV25V1ainfix +V2c1Iapermut_subV24V25ainfix +V1c1ainfix +V2c1Aasorted_subV25ainfix +V1c1ainfix +V2c1Aainfix &lt;=c0V0FAainfix &lt;V2V0Aainfix &lt;=c0ainfix +V1c1Aainfix &lt;ainfix -ainfix +c1V2ainfix +V1c1ainfix -ainfix +c1V2V1Aainfix &lt;=c0ainfix -ainfix +c1V2V1Iapermut_subV23V24V1ainfix +ainfix -V1c1c1Aasorted_subV24V1ainfix +ainfix -V1c1c1Aainfix &lt;=c0V0FAainfix &lt;ainfix -V1c1V0Aainfix &lt;=c0V1Aainfix &lt;ainfix -ainfix +c1ainfix -V1c1V1ainfix -ainfix +c1V2V1Aainfix &lt;=c0ainfix -ainfix +c1V2V1IaexchangeV3V23V1V1Aainfix &lt;=c0V0FAainfix &lt;V1V0Aainfix &lt;=c0V1Aainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &gt;ainfix +V1c1V2LagetV3V1Aainfix &lt;V1V0Aainfix &lt;=c0V1apermut_subV3V3V1ainfix +V2c1Aasorted_subV3V1ainfix +V2c1Iainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
@@ -69,9 +49,9 @@
      <goal
       name="WP_parameter quick_rec.1"
       locfile="../quicksort.mlw"
-      loclnum="24" loccnumb="10" loccnume="19"
+      loclnum="18" loccnumb="10" loccnume="19"
       expl="1. precondition"
-      sum="7d7d458ce0222f4ca64b04957075c924"
+      sum="ae55f23d05a29688d2376eef9e4a7ddd"
       proved="true"
       expanded="false"
       shape="ainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
@@ -89,9 +69,9 @@
      <goal
       name="WP_parameter quick_rec.2"
       locfile="../quicksort.mlw"
-      loclnum="24" loccnumb="10" loccnume="19"
+      loclnum="18" loccnumb="10" loccnume="19"
       expl="2. precondition"
-      sum="dc7f7efa7c91b9e6087c61384e786bed"
+      sum="9bb991b2cba89d0983fceaa804cb4a3d"
       proved="true"
       expanded="false"
       shape="ainfix &lt;V1V0Aainfix &lt;=c0V1Aainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &gt;ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
@@ -109,9 +89,9 @@
      <goal
       name="WP_parameter quick_rec.3"
       locfile="../quicksort.mlw"
-      loclnum="24" loccnumb="10" loccnume="19"
+      loclnum="18" loccnumb="10" loccnume="19"
       expl="3. variant decrease"
-      sum="3bb71daf7aad1d4e72e29acdd4a0a2d7"
+      sum="4d6cd8629305d4e566e1b967232e839a"
       proved="true"
       expanded="false"
       shape="ainfix &lt;ainfix -ainfix +c1ainfix -V1c1V1ainfix -ainfix +c1V2V1Aainfix &lt;=c0ainfix -ainfix +c1V2V1IaexchangeV3V5V1V1Aainfix &lt;=c0V0FIainfix &lt;V1V0Aainfix &lt;=c0V1Aainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &gt;ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
@@ -129,9 +109,9 @@
      <goal
       name="WP_parameter quick_rec.4"
       locfile="../quicksort.mlw"
-      loclnum="24" loccnumb="10" loccnume="19"
+      loclnum="18" loccnumb="10" loccnume="19"
       expl="4. precondition"
-      sum="227a6856b93965c5253c9a3946c401a8"
+      sum="9d3fd54e6e00ff8e7d4335d746a5d93b"
       proved="true"
       expanded="false"
       shape="ainfix &lt;ainfix -V1c1V0Aainfix &lt;=c0V1IaexchangeV3V5V1V1Aainfix &lt;=c0V0FIainfix &lt;V1V0Aainfix &lt;=c0V1Aainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &gt;ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
@@ -149,9 +129,9 @@
      <goal
       name="WP_parameter quick_rec.5"
       locfile="../quicksort.mlw"
-      loclnum="24" loccnumb="10" loccnume="19"
+      loclnum="18" loccnumb="10" loccnume="19"
       expl="5. variant decrease"
-      sum="b1e47fd51ce8162d443cd8b19edb9e69"
+      sum="dbadbbbfd52f6334807dfe528a3077cf"
       proved="true"
       expanded="false"
       shape="ainfix &lt;ainfix -ainfix +c1V2ainfix +V1c1ainfix -ainfix +c1V2V1Aainfix &lt;=c0ainfix -ainfix +c1V2V1Iapermut_subV5V6V1ainfix +ainfix -V1c1c1Aasorted_subV6V1ainfix +ainfix -V1c1c1Aainfix &lt;=c0V0FIainfix &lt;ainfix -V1c1V0Aainfix &lt;=c0V1IaexchangeV3V5V1V1Aainfix &lt;=c0V0FIainfix &lt;V1V0Aainfix &lt;=c0V1Aainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &gt;ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
@@ -169,9 +149,9 @@
      <goal
       name="WP_parameter quick_rec.6"
       locfile="../quicksort.mlw"
-      loclnum="24" loccnumb="10" loccnume="19"
+      loclnum="18" loccnumb="10" loccnume="19"
       expl="6. precondition"
-      sum="1b31473ddc0425cae989434e70307100"
+      sum="1d26d35a1ba8bc7e55f513ec21e2a46f"
       proved="true"
       expanded="false"
       shape="ainfix &lt;V2V0Aainfix &lt;=c0ainfix +V1c1Iapermut_subV5V6V1ainfix +ainfix -V1c1c1Aasorted_subV6V1ainfix +ainfix -V1c1c1Aainfix &lt;=c0V0FIainfix &lt;ainfix -V1c1V0Aainfix &lt;=c0V1IaexchangeV3V5V1V1Aainfix &lt;=c0V0FIainfix &lt;V1V0Aainfix &lt;=c0V1Aainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &gt;ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
@@ -189,9 +169,9 @@
      <goal
       name="WP_parameter quick_rec.7"
       locfile="../quicksort.mlw"
-      loclnum="24" loccnumb="10" loccnume="19"
+      loclnum="18" loccnumb="10" loccnume="19"
       expl="7. postcondition"
-      sum="e2d09e139c07441a5c7257b1f5b07316"
+      sum="b9e3ed951bc33fce945efb3635bfb3c3"
       proved="true"
       expanded="false"
       shape="apermut_subV3V7V1ainfix +V2c1Aasorted_subV7V1ainfix +V2c1Iapermut_subV6V7ainfix +V1c1ainfix +V2c1Aasorted_subV7ainfix +V1c1ainfix +V2c1Aainfix &lt;=c0V0FIainfix &lt;V2V0Aainfix &lt;=c0ainfix +V1c1Iapermut_subV5V6V1ainfix +ainfix -V1c1c1Aasorted_subV6V1ainfix +ainfix -V1c1c1Aainfix &lt;=c0V0FIainfix &lt;ainfix -V1c1V0Aainfix &lt;=c0V1IaexchangeV3V5V1V1Aainfix &lt;=c0V0FIainfix &lt;V1V0Aainfix &lt;=c0V1Aainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &gt;ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
@@ -209,9 +189,9 @@
      <goal
       name="WP_parameter quick_rec.8"
       locfile="../quicksort.mlw"
-      loclnum="24" loccnumb="10" loccnume="19"
+      loclnum="18" loccnumb="10" loccnume="19"
       expl="8. loop invariant init"
-      sum="8497b9d2e41db1c18c3a1de43e8d399e"
+      sum="73882fdadcde4e2c0cf821f71a5c9aa1"
       proved="true"
       expanded="false"
       shape="ainfix &lt;V1ainfix +V1c1Aainfix &lt;=V1V1Aainfix =agetV3V1V4Aapermut_subV3V3V1ainfix +V2c1Aainfix &gt;=agetV3V5V4Iainfix &lt;V5ainfix +V1c1Aainfix &lt;V1V5FAainfix &lt;agetV3V6V4Iainfix &lt;=V6V1Aainfix &lt;V1V6FIainfix &lt;=ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
@@ -229,9 +209,9 @@
      <goal
       name="WP_parameter quick_rec.9"
       locfile="../quicksort.mlw"
-      loclnum="24" loccnumb="10" loccnume="19"
+      loclnum="18" loccnumb="10" loccnume="19"
       expl="9. type invariant"
-      sum="923d48918d92090b10b016a9c93ce591"
+      sum="1d09049de88433625160180763d59f29"
       proved="true"
       expanded="false"
       shape="ainfix &lt;=c0V0Iainfix &lt;V5V7Aainfix &lt;=V1V5Aainfix =agetV6V1V4Aapermut_subV3V6V1ainfix +V2c1Aainfix &gt;=agetV6V8V4Iainfix &lt;V8V7Aainfix &lt;V5V8FAainfix &lt;agetV6V9V4Iainfix &lt;=V9V5Aainfix &lt;V1V9FIainfix &lt;=V7V2Aainfix &lt;=ainfix +V1c1V7FFIainfix &lt;=ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
@@ -249,9 +229,9 @@
      <goal
       name="WP_parameter quick_rec.10"
       locfile="../quicksort.mlw"
-      loclnum="24" loccnumb="10" loccnume="19"
+      loclnum="18" loccnumb="10" loccnume="19"
       expl="10. precondition"
-      sum="f3383493ceefcd497194f12d4ea1eadc"
+      sum="de2809145aaedc84dc3b7fef0347c3f2"
       proved="true"
       expanded="false"
       shape="ainfix &lt;V7V0Aainfix &lt;=c0V7Iainfix &lt;=c0V0Iainfix &lt;V5V7Aainfix &lt;=V1V5Aainfix =agetV6V1V4Aapermut_subV3V6V1ainfix +V2c1Aainfix &gt;=agetV6V8V4Iainfix &lt;V8V7Aainfix &lt;V5V8FAainfix &lt;agetV6V9V4Iainfix &lt;=V9V5Aainfix &lt;V1V9FIainfix &lt;=V7V2Aainfix &lt;=ainfix +V1c1V7FFIainfix &lt;=ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
@@ -269,9 +249,9 @@
      <goal
       name="WP_parameter quick_rec.11"
       locfile="../quicksort.mlw"
-      loclnum="24" loccnumb="10" loccnume="19"
+      loclnum="18" loccnumb="10" loccnume="19"
       expl="11. precondition"
-      sum="73f2b27977492b17e040e2b68904a39e"
+      sum="b58126fc9aaa0d3d70e0c6159fce3eae"
       proved="true"
       expanded="false"
       shape="ainfix &lt;V8V0Aainfix &lt;=c0V8Aainfix &lt;V7V0Aainfix &lt;=c0V7Iainfix =V8ainfix +V5c1FIainfix &lt;agetV6V7V4Iainfix &lt;V7V0Aainfix &lt;=c0V7Aainfix &lt;=c0V0Iainfix &lt;V5V7Aainfix &lt;=V1V5Aainfix =agetV6V1V4Aapermut_subV3V6V1ainfix +V2c1Aainfix &gt;=agetV6V9V4Iainfix &lt;V9V7Aainfix &lt;V5V9FAainfix &lt;agetV6V10V4Iainfix &lt;=V10V5Aainfix &lt;V1V10FIainfix &lt;=V7V2Aainfix &lt;=ainfix +V1c1V7FFIainfix &lt;=ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
@@ -289,9 +269,9 @@
      <goal
       name="WP_parameter quick_rec.12"
       locfile="../quicksort.mlw"
-      loclnum="24" loccnumb="10" loccnume="19"
+      loclnum="18" loccnumb="10" loccnume="19"
       expl="12. loop invariant preservation"
-      sum="6b35c535b227eded0e988b507d79590f"
+      sum="95889a61eecb6c9cb769f913c8ffee67"
       proved="true"
       expanded="false"
       shape="ainfix &lt;V8ainfix +V7c1Aainfix &lt;=V1V8Aainfix =agetV9V1V4Aapermut_subV3V9V1ainfix +V2c1Aainfix &gt;=agetV9V10V4Iainfix &lt;V10ainfix +V7c1Aainfix &lt;V8V10FAainfix &lt;agetV9V11V4Iainfix &lt;=V11V8Aainfix &lt;V1V11FIaexchangeV6V9V7V8Aainfix &lt;=c0V0FIainfix &lt;V8V0Aainfix &lt;=c0V8Aainfix &lt;V7V0Aainfix &lt;=c0V7Iainfix =V8ainfix +V5c1FIainfix &lt;agetV6V7V4Iainfix &lt;V7V0Aainfix &lt;=c0V7Aainfix &lt;=c0V0Iainfix &lt;V5V7Aainfix &lt;=V1V5Aainfix =agetV6V1V4Aapermut_subV3V6V1ainfix +V2c1Aainfix &gt;=agetV6V12V4Iainfix &lt;V12V7Aainfix &lt;V5V12FAainfix &lt;agetV6V13V4Iainfix &lt;=V13V5Aainfix &lt;V1V13FIainfix &lt;=V7V2Aainfix &lt;=ainfix +V1c1V7FFIainfix &lt;=ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
@@ -304,9 +284,9 @@
        <goal
         name="WP_parameter quick_rec.12.1"
         locfile="../quicksort.mlw"
-        loclnum="24" loccnumb="10" loccnume="19"
+        loclnum="18" loccnumb="10" loccnume="19"
         expl="1."
-        sum="befd4786b53ca3e49b83c96878fd826c"
+        sum="1d45e9be4f3306bc1a448e91a350c5e4"
         proved="true"
         expanded="false"
         shape="ainfix &lt;agetV9V10V4Iainfix &lt;=V10V8Aainfix &lt;V1V10FIaexchangeV6V9V7V8Aainfix &lt;=c0V0FIainfix &lt;V8V0Aainfix &lt;=c0V8Aainfix &lt;V7V0Aainfix &lt;=c0V7Iainfix =V8ainfix +V5c1FIainfix &lt;agetV6V7V4Iainfix &lt;V7V0Aainfix &lt;=c0V7Aainfix &lt;=c0V0Iainfix &lt;V5V7Aainfix &lt;=V1V5Aainfix =agetV6V1V4Aapermut_subV3V6V1ainfix +V2c1Aainfix &gt;=agetV6V11V4Iainfix &lt;V11V7Aainfix &lt;V5V11FAainfix &lt;agetV6V12V4Iainfix &lt;=V12V5Aainfix &lt;V1V12FIainfix &lt;=V7V2Aainfix &lt;=ainfix +V1c1V7FFIainfix &lt;=ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
@@ -324,9 +304,9 @@
        <goal
         name="WP_parameter quick_rec.12.2"
         locfile="../quicksort.mlw"
-        loclnum="24" loccnumb="10" loccnume="19"
+        loclnum="18" loccnumb="10" loccnume="19"
         expl="2."
-        sum="7db9a46260f71e4d3ae6ee618bfb91ba"
+        sum="d63df8c1733cf7fdd665dc752264e88d"
         proved="true"
         expanded="false"
         shape="ainfix &gt;=agetV9V10V4Iainfix &lt;V10ainfix +V7c1Aainfix &lt;V8V10FIaexchangeV6V9V7V8Aainfix &lt;=c0V0FIainfix &lt;V8V0Aainfix &lt;=c0V8Aainfix &lt;V7V0Aainfix &lt;=c0V7Iainfix =V8ainfix +V5c1FIainfix &lt;agetV6V7V4Iainfix &lt;V7V0Aainfix &lt;=c0V7Aainfix &lt;=c0V0Iainfix &lt;V5V7Aainfix &lt;=V1V5Aainfix =agetV6V1V4Aapermut_subV3V6V1ainfix +V2c1Aainfix &gt;=agetV6V11V4Iainfix &lt;V11V7Aainfix &lt;V5V11FAainfix &lt;agetV6V12V4Iainfix &lt;=V12V5Aainfix &lt;V1V12FIainfix &lt;=V7V2Aainfix &lt;=ainfix +V1c1V7FFIainfix &lt;=ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
@@ -344,9 +324,9 @@
        <goal
         name="WP_parameter quick_rec.12.3"
         locfile="../quicksort.mlw"
-        loclnum="24" loccnumb="10" loccnume="19"
+        loclnum="18" loccnumb="10" loccnume="19"
         expl="3."
-        sum="1aaf168e515a0d857ce78f26563485b7"
+        sum="595f447c4093a4fab71d6f9c0e23c7e0"
         proved="true"
         expanded="false"
         shape="apermut_subV3V9V1ainfix +V2c1IaexchangeV6V9V7V8Aainfix &lt;=c0V0FIainfix &lt;V8V0Aainfix &lt;=c0V8Aainfix &lt;V7V0Aainfix &lt;=c0V7Iainfix =V8ainfix +V5c1FIainfix &lt;agetV6V7V4Iainfix &lt;V7V0Aainfix &lt;=c0V7Aainfix &lt;=c0V0Iainfix &lt;V5V7Aainfix &lt;=V1V5Aainfix =agetV6V1V4Aapermut_subV3V6V1ainfix +V2c1Aainfix &gt;=agetV6V10V4Iainfix &lt;V10V7Aainfix &lt;V5V10FAainfix &lt;agetV6V11V4Iainfix &lt;=V11V5Aainfix &lt;V1V11FIainfix &lt;=V7V2Aainfix &lt;=ainfix +V1c1V7FFIainfix &lt;=ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
@@ -359,15 +339,15 @@
          edited="quicksort_WP_Quicksort_WP_parameter_quick_rec_1.v"
          obsolete="false"
          archived="false">
-         <result status="valid" time="0.57"/>
+         <result status="valid" time="1.93"/>
         </proof>
        </goal>
        <goal
         name="WP_parameter quick_rec.12.4"
         locfile="../quicksort.mlw"
-        loclnum="24" loccnumb="10" loccnume="19"
+        loclnum="18" loccnumb="10" loccnume="19"
         expl="4."
-        sum="8222a141c6f2a6e34f6e5c6537506687"
+        sum="c79f4b989159b6ce2c8c377ddd1aae0a"
         proved="true"
         expanded="false"
         shape="ainfix =agetV9V1V4IaexchangeV6V9V7V8Aainfix &lt;=c0V0FIainfix &lt;V8V0Aainfix &lt;=c0V8Aainfix &lt;V7V0Aainfix &lt;=c0V7Iainfix =V8ainfix +V5c1FIainfix &lt;agetV6V7V4Iainfix &lt;V7V0Aainfix &lt;=c0V7Aainfix &lt;=c0V0Iainfix &lt;V5V7Aainfix &lt;=V1V5Aainfix =agetV6V1V4Aapermut_subV3V6V1ainfix +V2c1Aainfix &gt;=agetV6V10V4Iainfix &lt;V10V7Aainfix &lt;V5V10FAainfix &lt;agetV6V11V4Iainfix &lt;=V11V5Aainfix &lt;V1V11FIainfix &lt;=V7V2Aainfix &lt;=ainfix +V1c1V7FFIainfix &lt;=ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
@@ -385,9 +365,9 @@
        <goal
         name="WP_parameter quick_rec.12.5"
         locfile="../quicksort.mlw"
-        loclnum="24" loccnumb="10" loccnume="19"
+        loclnum="18" loccnumb="10" loccnume="19"
         expl="5."
-        sum="32e820638e5c84864f26323b16cd9a59"
+        sum="8c671be21dd714f551823c2a8325c566"
         proved="true"
         expanded="false"
         shape="ainfix &lt;=V1V8IaexchangeV6V9V7V8Aainfix &lt;=c0V0FIainfix &lt;V8V0Aainfix &lt;=c0V8Aainfix &lt;V7V0Aainfix &lt;=c0V7Iainfix =V8ainfix +V5c1FIainfix &lt;agetV6V7V4Iainfix &lt;V7V0Aainfix &lt;=c0V7Aainfix &lt;=c0V0Iainfix &lt;V5V7Aainfix &lt;=V1V5Aainfix =agetV6V1V4Aapermut_subV3V6V1ainfix +V2c1Aainfix &gt;=agetV6V10V4Iainfix &lt;V10V7Aainfix &lt;V5V10FAainfix &lt;agetV6V11V4Iainfix &lt;=V11V5Aainfix &lt;V1V11FIainfix &lt;=V7V2Aainfix &lt;=ainfix +V1c1V7FFIainfix &lt;=ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
@@ -405,9 +385,9 @@
        <goal
         name="WP_parameter quick_rec.12.6"
         locfile="../quicksort.mlw"
-        loclnum="24" loccnumb="10" loccnume="19"
+        loclnum="18" loccnumb="10" loccnume="19"
         expl="6."
-        sum="be9b5da54df54578675dc2b34bc3d3fd"
+        sum="bc2e10a4a5d5cba20d3544d9bfc4403f"
         proved="true"
         expanded="false"
         shape="ainfix &lt;V8ainfix +V7c1IaexchangeV6V9V7V8Aainfix &lt;=c0V0FIainfix &lt;V8V0Aainfix &lt;=c0V8Aainfix &lt;V7V0Aainfix &lt;=c0V7Iainfix =V8ainfix +V5c1FIainfix &lt;agetV6V7V4Iainfix &lt;V7V0Aainfix &lt;=c0V7Aainfix &lt;=c0V0Iainfix &lt;V5V7Aainfix &lt;=V1V5Aainfix =agetV6V1V4Aapermut_subV3V6V1ainfix +V2c1Aainfix &gt;=agetV6V10V4Iainfix &lt;V10V7Aainfix &lt;V5V10FAainfix &lt;agetV6V11V4Iainfix &lt;=V11V5Aainfix &lt;V1V11FIainfix &lt;=V7V2Aainfix &lt;=ainfix +V1c1V7FFIainfix &lt;=ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
@@ -427,9 +407,9 @@
      <goal
       name="WP_parameter quick_rec.13"
       locfile="../quicksort.mlw"
-      loclnum="24" loccnumb="10" loccnume="19"
+      loclnum="18" loccnumb="10" loccnume="19"
       expl="13. loop invariant preservation"
-      sum="fa6637c8f4b8d011a06d0dbe0c60933e"
+      sum="b902f8b5c2369745284d3e4cc6acfc50"
       proved="true"
       expanded="false"
       shape="ainfix &lt;V5ainfix +V7c1Aainfix &lt;=V1V5Aainfix =agetV6V1V4Aapermut_subV3V6V1ainfix +V2c1Aainfix &gt;=agetV6V8V4Iainfix &lt;V8ainfix +V7c1Aainfix &lt;V5V8FAainfix &lt;agetV6V9V4Iainfix &lt;=V9V5Aainfix &lt;V1V9FIainfix &lt;agetV6V7V4NIainfix &lt;V7V0Aainfix &lt;=c0V7Aainfix &lt;=c0V0Iainfix &lt;V5V7Aainfix &lt;=V1V5Aainfix =agetV6V1V4Aapermut_subV3V6V1ainfix +V2c1Aainfix &gt;=agetV6V10V4Iainfix &lt;V10V7Aainfix &lt;V5V10FAainfix &lt;agetV6V11V4Iainfix &lt;=V11V5Aainfix &lt;V1V11FIainfix &lt;=V7V2Aainfix &lt;=ainfix +V1c1V7FFIainfix &lt;=ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
@@ -447,9 +427,9 @@
      <goal
       name="WP_parameter quick_rec.14"
       locfile="../quicksort.mlw"
-      loclnum="24" loccnumb="10" loccnume="19"
+      loclnum="18" loccnumb="10" loccnume="19"
       expl="14. type invariant"
-      sum="5d875a08da7310ecaa75bdd83734e17a"
+      sum="db6ae382fccf4d1dafe7783f06496638"
       proved="true"
       expanded="false"
       shape="ainfix &lt;=c0V0Iainfix &lt;V5ainfix +V2c1Aainfix &lt;=V1V5Aainfix =agetV6V1V4Aapermut_subV3V6V1ainfix +V2c1Aainfix &gt;=agetV6V7V4Iainfix &lt;V7ainfix +V2c1Aainfix &lt;V5V7FAainfix &lt;agetV6V8V4Iainfix &lt;=V8V5Aainfix &lt;V1V8FFIainfix &lt;=ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
@@ -467,9 +447,9 @@
      <goal
       name="WP_parameter quick_rec.15"
       locfile="../quicksort.mlw"
-      loclnum="24" loccnumb="10" loccnume="19"
+      loclnum="18" loccnumb="10" loccnume="19"
       expl="15. precondition"
-      sum="63a366347d0e2ac0735db16d000c4e10"
+      sum="ddb72d17faf5a91da1edad9489f0d34f"
       proved="true"
       expanded="false"
       shape="ainfix &lt;V5V0Aainfix &lt;=c0V5Aainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;=c0V0Iainfix &lt;V5ainfix +V2c1Aainfix &lt;=V1V5Aainfix =agetV6V1V4Aapermut_subV3V6V1ainfix +V2c1Aainfix &gt;=agetV6V7V4Iainfix &lt;V7ainfix +V2c1Aainfix &lt;V5V7FAainfix &lt;agetV6V8V4Iainfix &lt;=V8V5Aainfix &lt;V1V8FFIainfix &lt;=ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
@@ -482,9 +462,9 @@
        <goal
         name="WP_parameter quick_rec.15.1"
         locfile="../quicksort.mlw"
-        loclnum="24" loccnumb="10" loccnume="19"
+        loclnum="18" loccnumb="10" loccnume="19"
         expl="1."
-        sum="bef114c4ff3b3300dd85ce346fb49498"
+        sum="f28a60ac715732d093431611b5653bca"
         proved="true"
         expanded="false"
         shape="ainfix &lt;=c0V1Iainfix &lt;=c0V0Iainfix &lt;V5ainfix +V2c1Aainfix &lt;=V1V5Aainfix =agetV6V1V4Aapermut_subV3V6V1ainfix +V2c1Aainfix &gt;=agetV6V7V4Iainfix &lt;V7ainfix +V2c1Aainfix &lt;V5V7FAainfix &lt;agetV6V8V4Iainfix &lt;=V8V5Aainfix &lt;V1V8FFIainfix &lt;=ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
@@ -502,9 +482,9 @@
        <goal
         name="WP_parameter quick_rec.15.2"
         locfile="../quicksort.mlw"
-        loclnum="24" loccnumb="10" loccnume="19"
+        loclnum="18" loccnumb="10" loccnume="19"
         expl="2."
-        sum="2cf9c9b34f4ec9a84034c02bffc1d5c6"
+        sum="b7c0bed51260822bebe8aa68f0dc40cf"
         proved="true"
         expanded="false"
         shape="ainfix &lt;V1V0Iainfix &lt;=c0V0Iainfix &lt;V5ainfix +V2c1Aainfix &lt;=V1V5Aainfix =agetV6V1V4Aapermut_subV3V6V1ainfix +V2c1Aainfix &gt;=agetV6V7V4Iainfix &lt;V7ainfix +V2c1Aainfix &lt;V5V7FAainfix &lt;agetV6V8V4Iainfix &lt;=V8V5Aainfix &lt;V1V8FFIainfix &lt;=ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
@@ -522,9 +502,9 @@
        <goal
         name="WP_parameter quick_rec.15.3"
         locfile="../quicksort.mlw"
-        loclnum="24" loccnumb="10" loccnume="19"
+        loclnum="18" loccnumb="10" loccnume="19"
         expl="3."
-        sum="bffbcc5961922ed4dfca616fbf48f397"
+        sum="05cc1f6ece42cdd219a0ba82cc27cd81"
         proved="true"
         expanded="false"
         shape="ainfix &lt;=c0V5Iainfix &lt;=c0V0Iainfix &lt;V5ainfix +V2c1Aainfix &lt;=V1V5Aainfix =agetV6V1V4Aapermut_subV3V6V1ainfix +V2c1Aainfix &gt;=agetV6V7V4Iainfix &lt;V7ainfix +V2c1Aainfix &lt;V5V7FAainfix &lt;agetV6V8V4Iainfix &lt;=V8V5Aainfix &lt;V1V8FFIainfix &lt;=ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
@@ -542,9 +522,9 @@
        <goal
         name="WP_parameter quick_rec.15.4"
         locfile="../quicksort.mlw"
-        loclnum="24" loccnumb="10" loccnume="19"
+        loclnum="18" loccnumb="10" loccnume="19"
         expl="4."
-        sum="3f4e824534358868f8c7f600af3c4652"
+        sum="115df8ce22b7d8a5f7ac3f91dad7d931"
         proved="true"
         expanded="false"
         shape="ainfix &lt;V5V0Iainfix &lt;=c0V0Iainfix &lt;V5ainfix +V2c1Aainfix &lt;=V1V5Aainfix =agetV6V1V4Aapermut_subV3V6V1ainfix +V2c1Aainfix &gt;=agetV6V7V4Iainfix &lt;V7ainfix +V2c1Aainfix &lt;V5V7FAainfix &lt;agetV6V8V4Iainfix &lt;=V8V5Aainfix &lt;V1V8FFIainfix &lt;=ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
@@ -564,9 +544,9 @@
      <goal
       name="WP_parameter quick_rec.16"
       locfile="../quicksort.mlw"
-      loclnum="24" loccnumb="10" loccnume="19"
+      loclnum="18" loccnumb="10" loccnume="19"
       expl="16. variant decrease"
-      sum="e0792cb57e1cc385befecfdc6f50c9e7"
+      sum="737ffc650218694bcc57a9d1ae9ddd35"
       proved="true"
       expanded="false"
       shape="ainfix &lt;ainfix -ainfix +c1ainfix -V5c1V1ainfix -ainfix +c1V2V1Aainfix &lt;=c0ainfix -ainfix +c1V2V1IaexchangeV6V7V1V5Aainfix &lt;=c0V0FIainfix &lt;V5V0Aainfix &lt;=c0V5Aainfix &lt;V1V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0Iainfix &lt;V5ainfix +V2c1Aainfix &lt;=V1V5Aainfix =agetV6V1V4Aapermut_subV3V6V1ainfix +V2c1Aainfix &gt;=agetV6V8V4Iainfix &lt;V8ainfix +V2c1Aainfix &lt;V5V8FAainfix &lt;agetV6V9V4Iainfix &lt;=V9V5Aainfix &lt;V1V9FFIainfix &lt;=ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
@@ -584,9 +564,9 @@
      <goal
       name="WP_parameter quick_rec.17"
       locfile="../quicksort.mlw"
-      loclnum="24" loccnumb="10" loccnume="19"
+      loclnum="18" loccnumb="10" loccnume="19"
       expl="17. precondition"
-      sum="3cc6b6642ce915be9b41186729e66da3"
+      sum="9303d0dcf8380a2624871249c87e63fc"
       proved="true"
       expanded="false"
       shape="ainfix &lt;ainfix -V5c1V0Aainfix &lt;=c0V1IaexchangeV6V7V1V5Aainfix &lt;=c0V0FIainfix &lt;V5V0Aainfix &lt;=c0V5Aainfix &lt;V1V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0Iainfix &lt;V5ainfix +V2c1Aainfix &lt;=V1V5Aainfix =agetV6V1V4Aapermut_subV3V6V1ainfix +V2c1Aainfix &gt;=agetV6V8V4Iainfix &lt;V8ainfix +V2c1Aainfix &lt;V5V8FAainfix &lt;agetV6V9V4Iainfix &lt;=V9V5Aainfix &lt;V1V9FFIainfix &lt;=ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
@@ -604,9 +584,9 @@
      <goal
       name="WP_parameter quick_rec.18"
       locfile="../quicksort.mlw"
-      loclnum="24" loccnumb="10" loccnume="19"
+      loclnum="18" loccnumb="10" loccnume="19"
       expl="18. variant decrease"
-      sum="1ab79307c5c52f070c1cb3f6a74bdbe8"
+      sum="83e621fe3643e6c4f2ff6746404f618f"
       proved="true"
       expanded="false"
       shape="ainfix &lt;ainfix -ainfix +c1V2ainfix +V5c1ainfix -ainfix +c1V2V1Aainfix &lt;=c0ainfix -ainfix +c1V2V1Iapermut_subV7V8V1ainfix +ainfix -V5c1c1Aasorted_subV8V1ainfix +ainfix -V5c1c1Aainfix &lt;=c0V0FIainfix &lt;ainfix -V5c1V0Aainfix &lt;=c0V1IaexchangeV6V7V1V5Aainfix &lt;=c0V0FIainfix &lt;V5V0Aainfix &lt;=c0V5Aainfix &lt;V1V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0Iainfix &lt;V5ainfix +V2c1Aainfix &lt;=V1V5Aainfix =agetV6V1V4Aapermut_subV3V6V1ainfix +V2c1Aainfix &gt;=agetV6V9V4Iainfix &lt;V9ainfix +V2c1Aainfix &lt;V5V9FAainfix &lt;agetV6V10V4Iainfix &lt;=V10V5Aainfix &lt;V1V10FFIainfix &lt;=ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
@@ -624,9 +604,9 @@
      <goal
       name="WP_parameter quick_rec.19"
       locfile="../quicksort.mlw"
-      loclnum="24" loccnumb="10" loccnume="19"
+      loclnum="18" loccnumb="10" loccnume="19"
       expl="19. precondition"
-      sum="3348dada82d7da56fbafe89a2f77ebff"
+      sum="548e6b4c6de6a3d686e2ba43d2197426"
       proved="true"
       expanded="false"
       shape="ainfix &lt;V2V0Aainfix &lt;=c0ainfix +V5c1Iapermut_subV7V8V1ainfix +ainfix -V5c1c1Aasorted_subV8V1ainfix +ainfix -V5c1c1Aainfix &lt;=c0V0FIainfix &lt;ainfix -V5c1V0Aainfix &lt;=c0V1IaexchangeV6V7V1V5Aainfix &lt;=c0V0FIainfix &lt;V5V0Aainfix &lt;=c0V5Aainfix &lt;V1V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0Iainfix &lt;V5ainfix +V2c1Aainfix &lt;=V1V5Aainfix =agetV6V1V4Aapermut_subV3V6V1ainfix +V2c1Aainfix &gt;=agetV6V9V4Iainfix &lt;V9ainfix +V2c1Aainfix &lt;V5V9FAainfix &lt;agetV6V10V4Iainfix &lt;=V10V5Aainfix &lt;V1V10FFIainfix &lt;=ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
@@ -644,9 +624,9 @@
      <goal
       name="WP_parameter quick_rec.20"
       locfile="../quicksort.mlw"
-      loclnum="24" loccnumb="10" loccnume="19"
+      loclnum="18" loccnumb="10" loccnume="19"
       expl="20. postcondition"
-      sum="616cb0b075b543129a65e3b6a40d9f35"
+      sum="25298083d253829fe468ee94d253c22e"
       proved="true"
       expanded="false"
       shape="apermut_subV3V9V1ainfix +V2c1Aasorted_subV9V1ainfix +V2c1Iapermut_subV8V9ainfix +V5c1ainfix +V2c1Aasorted_subV9ainfix +V5c1ainfix +V2c1Aainfix &lt;=c0V0FIainfix &lt;V2V0Aainfix &lt;=c0ainfix +V5c1Iapermut_subV7V8V1ainfix +ainfix -V5c1c1Aasorted_subV8V1ainfix +ainfix -V5c1c1Aainfix &lt;=c0V0FIainfix &lt;ainfix -V5c1V0Aainfix &lt;=c0V1IaexchangeV6V7V1V5Aainfix &lt;=c0V0FIainfix &lt;V5V0Aainfix &lt;=c0V5Aainfix &lt;V1V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0Iainfix &lt;V5ainfix +V2c1Aainfix &lt;=V1V5Aainfix =agetV6V1V4Aapermut_subV3V6V1ainfix +V2c1Aainfix &gt;=agetV6V10V4Iainfix &lt;V10ainfix +V2c1Aainfix &lt;V5V10FAainfix &lt;agetV6V11V4Iainfix &lt;=V11V5Aainfix &lt;V1V11FFIainfix &lt;=ainfix +V1c1V2LagetV3V1Iainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
@@ -659,15 +639,15 @@
        edited="quicksort_WP_Quicksort_WP_parameter_quick_rec_2.v"
        obsolete="false"
        archived="false">
-       <result status="valid" time="1.54"/>
+       <result status="valid" time="5.26"/>
       </proof>
      </goal>
      <goal
       name="WP_parameter quick_rec.21"
       locfile="../quicksort.mlw"
-      loclnum="24" loccnumb="10" loccnume="19"
+      loclnum="18" loccnumb="10" loccnume="19"
       expl="21. postcondition"
-      sum="c5a1e7c20769ef45f89992930442d82e"
+      sum="3ed4b87a24f191766178e9165c896a74"
       proved="true"
       expanded="false"
       shape="apermut_subV3V3V1ainfix +V2c1Aasorted_subV3V1ainfix +V2c1Iainfix &lt;V1V2NIainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
@@ -680,9 +660,9 @@
        <goal
         name="WP_parameter quick_rec.21.1"
         locfile="../quicksort.mlw"
-        loclnum="24" loccnumb="10" loccnume="19"
+        loclnum="18" loccnumb="10" loccnume="19"
         expl="1."
-        sum="0b53241d282f56c733b2a6ac339a2f47"
+        sum="a33e2c171c6bbb2e3bc6574e614d8970"
         proved="true"
         expanded="false"
         shape="asorted_subV3V1ainfix +V2c1Iainfix &lt;V1V2NIainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
@@ -700,9 +680,9 @@
        <goal
         name="WP_parameter quick_rec.21.2"
         locfile="../quicksort.mlw"
-        loclnum="24" loccnumb="10" loccnume="19"
+        loclnum="18" loccnumb="10" loccnume="19"
         expl="2."
-        sum="0b87a20ff03a37864fa9be1beffff1e1"
+        sum="a2f76e3daa62b13a53a9375c22557c1e"
         proved="true"
         expanded="false"
         shape="apermut_subV3V3V1ainfix +V2c1Iainfix &lt;V1V2NIainfix &lt;V2V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
@@ -724,9 +704,9 @@
    <goal
     name="WP_parameter quicksort"
     locfile="../quicksort.mlw"
-    loclnum="42" loccnumb="6" loccnume="15"
+    loclnum="36" loccnumb="6" loccnume="15"
     expl="VC for quicksort"
-    sum="2f88e6d7cc71b4b729ddbf2a7da15cce"
+    sum="2b3422cbaca575d9ab3d2440337ffa9a"
     proved="true"
     expanded="false"
     shape="apermutamk arrayV0V1amk arrayV0V2Aasorted_subV2c0V0Iapermut_subV1V2c0ainfix +ainfix -V0c1c1Aasorted_subV2c0ainfix +ainfix -V0c1c1Aainfix &lt;=c0V0FAainfix &lt;ainfix -V0c1V0Aainfix &lt;=c0c0Iainfix &lt;=c0V0FF">
@@ -739,9 +719,9 @@
      <goal
       name="WP_parameter quicksort.1"
       locfile="../quicksort.mlw"
-      loclnum="42" loccnumb="6" loccnume="15"
+      loclnum="36" loccnumb="6" loccnume="15"
       expl="1. precondition"
-      sum="7b8d37bb459cde5602e168c003588571"
+      sum="5393c9438f88776ff208e12eff1ebbd2"
       proved="true"
       expanded="false"
       shape="ainfix &lt;ainfix -V0c1V0Aainfix &lt;=c0c0Iainfix &lt;=c0V0FF">
@@ -775,9 +755,9 @@
      <goal
       name="WP_parameter quicksort.2"
       locfile="../quicksort.mlw"
-      loclnum="42" loccnumb="6" loccnume="15"
+      loclnum="36" loccnumb="6" loccnume="15"
       expl="2. postcondition"
-      sum="6a9ec9fa966fedeb71742ad86d71fa3b"
+      sum="4a0ecc70082b1037004b6481a0899df7"
       proved="true"
       expanded="false"
       shape="apermutamk arrayV0V1amk arrayV0V2Aasorted_subV2c0V0Iapermut_subV1V2c0ainfix +ainfix -V0c1c1Aasorted_subV2c0ainfix +ainfix -V0c1c1Aainfix &lt;=c0V0FIainfix &lt;ainfix -V0c1V0Aainfix &lt;=c0c0Iainfix &lt;=c0V0FF">
diff --git a/examples/selection_sort.mlw b/examples/selection_sort.mlw
index b1ad5faea..44798f025 100644
--- a/examples/selection_sort.mlw
+++ b/examples/selection_sort.mlw
@@ -7,16 +7,10 @@ module SelectionSort
   use import ref.Ref
   use import array.Array
   use import array.ArraySorted
+  use import array.ArraySwap
   use import array.ArrayPermut
   use import array.ArrayEq
 
-  let swap (a: array int) (i: int) (j: int)
-    requires { 0 <= i < length a /\ 0 <= j < length a }
-    ensures { exchange (old a) a i j }
-  = let v = a[i] in
-    a[i] <- a[j];
-    a[j] <- v
-
   let selection_sort (a: array int)
     ensures { sorted a /\ permut (old a) a } =
 'L:
diff --git a/examples/selection_sort/why3session.xml b/examples/selection_sort/why3session.xml
index f902252fe..e345ea7e7 100644
--- a/examples/selection_sort/why3session.xml
+++ b/examples/selection_sort/why3session.xml
@@ -19,32 +19,12 @@
    loclnum="4" loccnumb="7" loccnume="20"
    verified="true"
    expanded="true">
-   <goal
-    name="WP_parameter swap"
-    locfile="../selection_sort.mlw"
-    loclnum="13" loccnumb="6" loccnume="10"
-    expl="VC for swap"
-    sum="a0e6aa0a260c53425d59522095d19ea6"
-    proved="true"
-    expanded="true"
-    shape="aexchangeV3V5V1V2Iainfix =V5asetV4V2agetV3V1Aainfix &lt;=c0V0FAainfix &lt;V2V0Aainfix &lt;=c0V2Iainfix =V4asetV3V1agetV3V2Aainfix &lt;=c0V0FAainfix &lt;V1V0Aainfix &lt;=c0V1Aainfix &lt;V2V0Aainfix &lt;=c0V2Aainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V2V0Aainfix &lt;=c0V2Aainfix &lt;V1V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
-    <label
-     name="expl:VC for swap"/>
-    <proof
-     prover="0"
-     timelimit="10"
-     memlimit="0"
-     obsolete="false"
-     archived="false">
-     <result status="valid" time="0.02"/>
-    </proof>
-   </goal>
    <goal
     name="WP_parameter selection_sort"
     locfile="../selection_sort.mlw"
-    loclnum="20" loccnumb="6" loccnume="20"
+    loclnum="14" loccnumb="6" loccnume="20"
     expl="VC for selection_sort"
-    sum="e4c8e8b6008074245574dd34437b1be4"
+    sum="fb250d5b3364bc18e3201530a9b1f43e"
     proved="true"
     expanded="true"
     shape="apermutV2V4Aasorted_subV3c0V0Aainfix &lt;=c0V0Iainfix &lt;=agetV3V5agetV3V6Iainfix &lt;V6V0Aainfix &lt;=ainfix +ainfix -V0c1c1V6Aainfix &lt;V5ainfix +ainfix -V0c1c1Aainfix &lt;=c0V5FAapermutV2V4Aasorted_subV3c0ainfix +ainfix -V0c1c1Aiainfix =V8V7Nainfix &lt;=agetV9V11agetV9V12Iainfix &lt;V12V0Aainfix &lt;=ainfix +V7c1V12Aainfix &lt;V11ainfix +V7c1Aainfix &lt;=c0V11FAapermutV2V10Aasorted_subV9c0ainfix +V7c1AapermutV4V10IaexchangeV3V9V8V7Aainfix &lt;=c0V0Lamk arrayV0V9FAainfix &lt;V7V0Aainfix &lt;=c0V7Aainfix &lt;V8V0Aainfix &lt;=c0V8ainfix &lt;=agetV3V13agetV3V14Iainfix &lt;V14V0Aainfix &lt;=ainfix +V7c1V14Aainfix &lt;V13ainfix +V7c1Aainfix &lt;=c0V13FAapermutV2V4Aasorted_subV3c0ainfix +V7c1AapermutV4V4Iainfix &lt;=agetV3V8agetV3V15Iainfix &lt;V15ainfix +ainfix -V0c1c1Aainfix &lt;=V7V15FAainfix &lt;V8ainfix +ainfix -V0c1c1Aainfix &lt;=V7V8Aiainfix &lt;agetV3V16agetV3V8ainfix &lt;=agetV3V17agetV3V18Iainfix &lt;V18ainfix +V16c1Aainfix &lt;=V7V18FAainfix &lt;V17ainfix +V16c1Aainfix &lt;=V7V17Iainfix =V17V16Fainfix &lt;=agetV3V8agetV3V19Iainfix &lt;V19ainfix +V16c1Aainfix &lt;=V7V19FAainfix &lt;V8ainfix +V16c1Aainfix &lt;=V7V8Aainfix &lt;V16V0Aainfix &lt;=c0V16Aainfix &lt;V8V0Aainfix &lt;=c0V8Iainfix &lt;=agetV3V8agetV3V20Iainfix &lt;V20V16Aainfix &lt;=V7V20FAainfix &lt;V8V16Aainfix &lt;=V7V8Iainfix &lt;=V16ainfix -V0c1Aainfix &lt;=ainfix +V7c1V16FFAainfix &lt;=agetV3V7agetV3V21Iainfix &lt;V21ainfix +V7c1Aainfix &lt;=V7V21FAainfix &lt;V7ainfix +V7c1Aainfix &lt;=V7V7Iainfix &lt;=ainfix +V7c1ainfix -V0c1Aiainfix =V7V7Nainfix &lt;=agetV22V24agetV22V25Iainfix &lt;V25V0Aainfix &lt;=ainfix +V7c1V25Aainfix &lt;V24ainfix +V7c1Aainfix &lt;=c0V24FAapermutV2V23Aasorted_subV22c0ainfix +V7c1AapermutV4V23IaexchangeV3V22V7V7Aainfix &lt;=c0V0Lamk arrayV0V22FAainfix &lt;V7V0Aainfix &lt;=c0V7Aainfix &lt;V7V0Aainfix &lt;=c0V7ainfix &lt;=agetV3V26agetV3V27Iainfix &lt;V27V0Aainfix &lt;=ainfix +V7c1V27Aainfix &lt;V26ainfix +V7c1Aainfix &lt;=c0V26FAapermutV2V4Aasorted_subV3c0ainfix +V7c1AapermutV4V4Iainfix &gt;ainfix +V7c1ainfix -V0c1Aainfix &lt;=c0V0Iainfix &lt;=agetV3V28agetV3V29Iainfix &lt;V29V0Aainfix &lt;=V7V29Aainfix &lt;V28V7Aainfix &lt;=c0V28FAapermutV2V4Aasorted_subV3c0V7Iainfix &lt;=V7ainfix -V0c1Aainfix &lt;=c0V7FLamk arrayV0V3FAainfix &lt;=agetV1V30agetV1V31Iainfix &lt;V31V0Aainfix &lt;=c0V31Aainfix &lt;V30c0Aainfix &lt;=c0V30FAapermutV2V2Aasorted_subV1c0c0Iainfix &lt;=c0ainfix -V0c1AapermutV2V2Aasorted_subV1c0V0Iainfix &gt;c0ainfix -V0c1Iainfix &lt;=c0V0Lamk arrayV0V1FF">
@@ -57,11 +37,11 @@
      <goal
       name="WP_parameter selection_sort.1"
       locfile="../selection_sort.mlw"
-      loclnum="20" loccnumb="6" loccnume="20"
+      loclnum="14" loccnumb="6" loccnume="20"
       expl="1. postcondition"
-      sum="ca4addc2f0684b810463d843491d8209"
+      sum="d5603b2e01b07c07d1da8df2f4e341d7"
       proved="true"
-      expanded="true"
+      expanded="false"
       shape="apermutV2V2Aasorted_subV1c0V0Iainfix &gt;c0ainfix -V0c1Iainfix &lt;=c0V0Lamk arrayV0V1FF">
       <label
        name="expl:VC for selection_sort"/>
@@ -77,11 +57,11 @@
      <goal
       name="WP_parameter selection_sort.2"
       locfile="../selection_sort.mlw"
-      loclnum="20" loccnumb="6" loccnume="20"
+      loclnum="14" loccnumb="6" loccnume="20"
       expl="2. loop invariant init"
-      sum="4a0cceb43b1dbdf006dd01fa6fc5ff97"
+      sum="162e12ec71e8921dc98fbe70f38ea50e"
       proved="true"
-      expanded="true"
+      expanded="false"
       shape="ainfix &lt;=agetV1V3agetV1V4Iainfix &lt;V4V0Aainfix &lt;=c0V4Aainfix &lt;V3c0Aainfix &lt;=c0V3FAapermutV2V2Aasorted_subV1c0c0Iainfix &lt;=c0ainfix -V0c1Iainfix &lt;=c0V0Lamk arrayV0V1FF">
       <label
        name="expl:VC for selection_sort"/>
@@ -97,9 +77,9 @@
      <goal
       name="WP_parameter selection_sort.3"
       locfile="../selection_sort.mlw"
-      loclnum="20" loccnumb="6" loccnume="20"
+      loclnum="14" loccnumb="6" loccnume="20"
       expl="3. type invariant"
-      sum="06ab73e335b59abf46228bcd4a6fda75"
+      sum="10062dd2f2a6421903735a818555dcc6"
       proved="true"
       expanded="false"
       shape="ainfix &lt;=c0V0Iainfix &lt;=agetV3V6agetV3V7Iainfix &lt;V7V0Aainfix &lt;=V5V7Aainfix &lt;V6V5Aainfix &lt;=c0V6FAapermutV2V4Aasorted_subV3c0V5Iainfix &lt;=V5ainfix -V0c1Aainfix &lt;=c0V5FLamk arrayV0V3FIainfix &lt;=c0ainfix -V0c1Iainfix &lt;=c0V0Lamk arrayV0V1FF">
@@ -117,11 +97,11 @@
      <goal
       name="WP_parameter selection_sort.4"
       locfile="../selection_sort.mlw"
-      loclnum="20" loccnumb="6" loccnume="20"
+      loclnum="14" loccnumb="6" loccnume="20"
       expl="4. precondition"
-      sum="6da27c14e9f9b9828ca3a46da9cc0a38"
+      sum="fac34059cb8168ba10feab73e1b1430c"
       proved="true"
-      expanded="true"
+      expanded="false"
       shape="ainfix &lt;V5V0Aainfix &lt;=c0V5Aainfix &lt;V5V0Aainfix &lt;=c0V5Iainfix =V5V5NIainfix &gt;ainfix +V5c1ainfix -V0c1Iainfix &lt;=c0V0Iainfix &lt;=agetV3V6agetV3V7Iainfix &lt;V7V0Aainfix &lt;=V5V7Aainfix &lt;V6V5Aainfix &lt;=c0V6FAapermutV2V4Aasorted_subV3c0V5Iainfix &lt;=V5ainfix -V0c1Aainfix &lt;=c0V5FLamk arrayV0V3FIainfix &lt;=c0ainfix -V0c1Iainfix &lt;=c0V0Lamk arrayV0V1FF">
       <label
        name="expl:VC for selection_sort"/>
@@ -137,11 +117,11 @@
      <goal
       name="WP_parameter selection_sort.5"
       locfile="../selection_sort.mlw"
-      loclnum="20" loccnumb="6" loccnume="20"
+      loclnum="14" loccnumb="6" loccnume="20"
       expl="5. assertion"
-      sum="59bd7bcd22319d568925a9b2b69f15c6"
+      sum="bfae1bce6420af6349c332fc4c1c4b8a"
       proved="true"
-      expanded="true"
+      expanded="false"
       shape="apermutV4V7IaexchangeV3V6V5V5Aainfix &lt;=c0V0Lamk arrayV0V6FIainfix &lt;V5V0Aainfix &lt;=c0V5Aainfix &lt;V5V0Aainfix &lt;=c0V5Iainfix =V5V5NIainfix &gt;ainfix +V5c1ainfix -V0c1Iainfix &lt;=c0V0Iainfix &lt;=agetV3V8agetV3V9Iainfix &lt;V9V0Aainfix &lt;=V5V9Aainfix &lt;V8V5Aainfix &lt;=c0V8FAapermutV2V4Aasorted_subV3c0V5Iainfix &lt;=V5ainfix -V0c1Aainfix &lt;=c0V5FLamk arrayV0V3FIainfix &lt;=c0ainfix -V0c1Iainfix &lt;=c0V0Lamk arrayV0V1FF">
       <label
        name="expl:VC for selection_sort"/>
@@ -157,11 +137,11 @@
      <goal
       name="WP_parameter selection_sort.6"
       locfile="../selection_sort.mlw"
-      loclnum="20" loccnumb="6" loccnume="20"
+      loclnum="14" loccnumb="6" loccnume="20"
       expl="6. loop invariant preservation"
-      sum="323b675790a18c07d41f29cc6c525284"
+      sum="6316be2d386c486479b029643e05810b"
       proved="true"
-      expanded="true"
+      expanded="false"
       shape="ainfix &lt;=agetV6V8agetV6V9Iainfix &lt;V9V0Aainfix &lt;=ainfix +V5c1V9Aainfix &lt;V8ainfix +V5c1Aainfix &lt;=c0V8FAapermutV2V7Aasorted_subV6c0ainfix +V5c1IapermutV4V7IaexchangeV3V6V5V5Aainfix &lt;=c0V0Lamk arrayV0V6FIainfix &lt;V5V0Aainfix &lt;=c0V5Aainfix &lt;V5V0Aainfix &lt;=c0V5Iainfix =V5V5NIainfix &gt;ainfix +V5c1ainfix -V0c1Iainfix &lt;=c0V0Iainfix &lt;=agetV3V10agetV3V11Iainfix &lt;V11V0Aainfix &lt;=V5V11Aainfix &lt;V10V5Aainfix &lt;=c0V10FAapermutV2V4Aasorted_subV3c0V5Iainfix &lt;=V5ainfix -V0c1Aainfix &lt;=c0V5FLamk arrayV0V3FIainfix &lt;=c0ainfix -V0c1Iainfix &lt;=c0V0Lamk arrayV0V1FF">
       <label
        name="expl:VC for selection_sort"/>
@@ -177,11 +157,11 @@
      <goal
       name="WP_parameter selection_sort.7"
       locfile="../selection_sort.mlw"
-      loclnum="20" loccnumb="6" loccnume="20"
+      loclnum="14" loccnumb="6" loccnume="20"
       expl="7. assertion"
-      sum="955eeae27c6c77502b2e23bfac3fcf6b"
+      sum="9ce0cbbf836443a469664fc4447d923f"
       proved="true"
-      expanded="true"
+      expanded="false"
       shape="apermutV4V4Iainfix =V5V5NNIainfix &gt;ainfix +V5c1ainfix -V0c1Iainfix &lt;=c0V0Iainfix &lt;=agetV3V6agetV3V7Iainfix &lt;V7V0Aainfix &lt;=V5V7Aainfix &lt;V6V5Aainfix &lt;=c0V6FAapermutV2V4Aasorted_subV3c0V5Iainfix &lt;=V5ainfix -V0c1Aainfix &lt;=c0V5FLamk arrayV0V3FIainfix &lt;=c0ainfix -V0c1Iainfix &lt;=c0V0Lamk arrayV0V1FF">
       <label
        name="expl:VC for selection_sort"/>
@@ -197,11 +177,11 @@
      <goal
       name="WP_parameter selection_sort.8"
       locfile="../selection_sort.mlw"
-      loclnum="20" loccnumb="6" loccnume="20"
+      loclnum="14" loccnumb="6" loccnume="20"
       expl="8. loop invariant preservation"
-      sum="b136ef5c3b1098ef34a2a21a253f99de"
+      sum="09052b68513907549e21ae82a736c9d3"
       proved="true"
-      expanded="true"
+      expanded="false"
       shape="ainfix &lt;=agetV3V6agetV3V7Iainfix &lt;V7V0Aainfix &lt;=ainfix +V5c1V7Aainfix &lt;V6ainfix +V5c1Aainfix &lt;=c0V6FAapermutV2V4Aasorted_subV3c0ainfix +V5c1IapermutV4V4Iainfix =V5V5NNIainfix &gt;ainfix +V5c1ainfix -V0c1Iainfix &lt;=c0V0Iainfix &lt;=agetV3V8agetV3V9Iainfix &lt;V9V0Aainfix &lt;=V5V9Aainfix &lt;V8V5Aainfix &lt;=c0V8FAapermutV2V4Aasorted_subV3c0V5Iainfix &lt;=V5ainfix -V0c1Aainfix &lt;=c0V5FLamk arrayV0V3FIainfix &lt;=c0ainfix -V0c1Iainfix &lt;=c0V0Lamk arrayV0V1FF">
       <label
        name="expl:VC for selection_sort"/>
@@ -217,11 +197,11 @@
      <goal
       name="WP_parameter selection_sort.9"
       locfile="../selection_sort.mlw"
-      loclnum="20" loccnumb="6" loccnume="20"
+      loclnum="14" loccnumb="6" loccnume="20"
       expl="9. loop invariant init"
-      sum="25133c11ae39b45c7f9635f0e3935eaa"
+      sum="b693394a9bdaa0009eadc432fbb77306"
       proved="true"
-      expanded="true"
+      expanded="false"
       shape="ainfix &lt;=agetV3V5agetV3V6Iainfix &lt;V6ainfix +V5c1Aainfix &lt;=V5V6FAainfix &lt;V5ainfix +V5c1Aainfix &lt;=V5V5Iainfix &lt;=ainfix +V5c1ainfix -V0c1Iainfix &lt;=c0V0Iainfix &lt;=agetV3V7agetV3V8Iainfix &lt;V8V0Aainfix &lt;=V5V8Aainfix &lt;V7V5Aainfix &lt;=c0V7FAapermutV2V4Aasorted_subV3c0V5Iainfix &lt;=V5ainfix -V0c1Aainfix &lt;=c0V5FLamk arrayV0V3FIainfix &lt;=c0ainfix -V0c1Iainfix &lt;=c0V0Lamk arrayV0V1FF">
       <label
        name="expl:VC for selection_sort"/>
@@ -237,11 +217,11 @@
      <goal
       name="WP_parameter selection_sort.10"
       locfile="../selection_sort.mlw"
-      loclnum="20" loccnumb="6" loccnume="20"
+      loclnum="14" loccnumb="6" loccnume="20"
       expl="10. precondition"
-      sum="1d9da5d59305b8f6916f596453835050"
+      sum="e28ed97705ca5622324046968b3818a6"
       proved="true"
-      expanded="true"
+      expanded="false"
       shape="ainfix &lt;V6V0Aainfix &lt;=c0V6Iainfix &lt;=agetV3V6agetV3V8Iainfix &lt;V8V7Aainfix &lt;=V5V8FAainfix &lt;V6V7Aainfix &lt;=V5V6Iainfix &lt;=V7ainfix -V0c1Aainfix &lt;=ainfix +V5c1V7FFIainfix &lt;=ainfix +V5c1ainfix -V0c1Iainfix &lt;=c0V0Iainfix &lt;=agetV3V9agetV3V10Iainfix &lt;V10V0Aainfix &lt;=V5V10Aainfix &lt;V9V5Aainfix &lt;=c0V9FAapermutV2V4Aasorted_subV3c0V5Iainfix &lt;=V5ainfix -V0c1Aainfix &lt;=c0V5FLamk arrayV0V3FIainfix &lt;=c0ainfix -V0c1Iainfix &lt;=c0V0Lamk arrayV0V1FF">
       <label
        name="expl:VC for selection_sort"/>
@@ -257,11 +237,11 @@
      <goal
       name="WP_parameter selection_sort.11"
       locfile="../selection_sort.mlw"
-      loclnum="20" loccnumb="6" loccnume="20"
+      loclnum="14" loccnumb="6" loccnume="20"
       expl="11. precondition"
-      sum="d96185415b48a28c6ddff12cfca7c3bc"
+      sum="478cf5b63cb6d61167cfbb2abd9106ba"
       proved="true"
-      expanded="true"
+      expanded="false"
       shape="ainfix &lt;V7V0Aainfix &lt;=c0V7Iainfix &lt;V6V0Aainfix &lt;=c0V6Iainfix &lt;=agetV3V6agetV3V8Iainfix &lt;V8V7Aainfix &lt;=V5V8FAainfix &lt;V6V7Aainfix &lt;=V5V6Iainfix &lt;=V7ainfix -V0c1Aainfix &lt;=ainfix +V5c1V7FFIainfix &lt;=ainfix +V5c1ainfix -V0c1Iainfix &lt;=c0V0Iainfix &lt;=agetV3V9agetV3V10Iainfix &lt;V10V0Aainfix &lt;=V5V10Aainfix &lt;V9V5Aainfix &lt;=c0V9FAapermutV2V4Aasorted_subV3c0V5Iainfix &lt;=V5ainfix -V0c1Aainfix &lt;=c0V5FLamk arrayV0V3FIainfix &lt;=c0ainfix -V0c1Iainfix &lt;=c0V0Lamk arrayV0V1FF">
       <label
        name="expl:VC for selection_sort"/>
@@ -277,11 +257,11 @@
      <goal
       name="WP_parameter selection_sort.12"
       locfile="../selection_sort.mlw"
-      loclnum="20" loccnumb="6" loccnume="20"
+      loclnum="14" loccnumb="6" loccnume="20"
       expl="12. loop invariant preservation"
-      sum="d9c683105bb4ef7cd45f97c62b3b7986"
+      sum="e748632b98af871a6e21dc77e3684a73"
       proved="true"
-      expanded="true"
+      expanded="false"
       shape="ainfix &lt;=agetV3V8agetV3V9Iainfix &lt;V9ainfix +V7c1Aainfix &lt;=V5V9FAainfix &lt;V8ainfix +V7c1Aainfix &lt;=V5V8Iainfix =V8V7FIainfix &lt;agetV3V7agetV3V6Iainfix &lt;V7V0Aainfix &lt;=c0V7Iainfix &lt;V6V0Aainfix &lt;=c0V6Iainfix &lt;=agetV3V6agetV3V10Iainfix &lt;V10V7Aainfix &lt;=V5V10FAainfix &lt;V6V7Aainfix &lt;=V5V6Iainfix &lt;=V7ainfix -V0c1Aainfix &lt;=ainfix +V5c1V7FFIainfix &lt;=ainfix +V5c1ainfix -V0c1Iainfix &lt;=c0V0Iainfix &lt;=agetV3V11agetV3V12Iainfix &lt;V12V0Aainfix &lt;=V5V12Aainfix &lt;V11V5Aainfix &lt;=c0V11FAapermutV2V4Aasorted_subV3c0V5Iainfix &lt;=V5ainfix -V0c1Aainfix &lt;=c0V5FLamk arrayV0V3FIainfix &lt;=c0ainfix -V0c1Iainfix &lt;=c0V0Lamk arrayV0V1FF">
       <label
        name="expl:VC for selection_sort"/>
@@ -291,17 +271,17 @@
        memlimit="1000"
        obsolete="false"
        archived="false">
-       <result status="valid" time="0.06"/>
+       <result status="valid" time="0.18"/>
       </proof>
      </goal>
      <goal
       name="WP_parameter selection_sort.13"
       locfile="../selection_sort.mlw"
-      loclnum="20" loccnumb="6" loccnume="20"
+      loclnum="14" loccnumb="6" loccnume="20"
       expl="13. loop invariant preservation"
-      sum="3a2fd52f48880fea77e596fa51ef55ef"
+      sum="ae0e5bce6ae0437347ce74d02f39854b"
       proved="true"
-      expanded="true"
+      expanded="false"
       shape="ainfix &lt;=agetV3V6agetV3V8Iainfix &lt;V8ainfix +V7c1Aainfix &lt;=V5V8FAainfix &lt;V6ainfix +V7c1Aainfix &lt;=V5V6Iainfix &lt;agetV3V7agetV3V6NIainfix &lt;V7V0Aainfix &lt;=c0V7Iainfix &lt;V6V0Aainfix &lt;=c0V6Iainfix &lt;=agetV3V6agetV3V9Iainfix &lt;V9V7Aainfix &lt;=V5V9FAainfix &lt;V6V7Aainfix &lt;=V5V6Iainfix &lt;=V7ainfix -V0c1Aainfix &lt;=ainfix +V5c1V7FFIainfix &lt;=ainfix +V5c1ainfix -V0c1Iainfix &lt;=c0V0Iainfix &lt;=agetV3V10agetV3V11Iainfix &lt;V11V0Aainfix &lt;=V5V11Aainfix &lt;V10V5Aainfix &lt;=c0V10FAapermutV2V4Aasorted_subV3c0V5Iainfix &lt;=V5ainfix -V0c1Aainfix &lt;=c0V5FLamk arrayV0V3FIainfix &lt;=c0ainfix -V0c1Iainfix &lt;=c0V0Lamk arrayV0V1FF">
       <label
        name="expl:VC for selection_sort"/>
@@ -317,11 +297,11 @@
      <goal
       name="WP_parameter selection_sort.14"
       locfile="../selection_sort.mlw"
-      loclnum="20" loccnumb="6" loccnume="20"
+      loclnum="14" loccnumb="6" loccnume="20"
       expl="14. precondition"
-      sum="cfe39494bbf2167e659b510ea4f04d6a"
+      sum="44782505b4388577346f034024a11c9a"
       proved="true"
-      expanded="true"
+      expanded="false"
       shape="ainfix &lt;V5V0Aainfix &lt;=c0V5Aainfix &lt;V6V0Aainfix &lt;=c0V6Iainfix =V6V5NIainfix &lt;=agetV3V6agetV3V7Iainfix &lt;V7ainfix +ainfix -V0c1c1Aainfix &lt;=V5V7FAainfix &lt;V6ainfix +ainfix -V0c1c1Aainfix &lt;=V5V6FIainfix &lt;=ainfix +V5c1ainfix -V0c1Iainfix &lt;=c0V0Iainfix &lt;=agetV3V8agetV3V9Iainfix &lt;V9V0Aainfix &lt;=V5V9Aainfix &lt;V8V5Aainfix &lt;=c0V8FAapermutV2V4Aasorted_subV3c0V5Iainfix &lt;=V5ainfix -V0c1Aainfix &lt;=c0V5FLamk arrayV0V3FIainfix &lt;=c0ainfix -V0c1Iainfix &lt;=c0V0Lamk arrayV0V1FF">
       <label
        name="expl:VC for selection_sort"/>
@@ -337,11 +317,11 @@
      <goal
       name="WP_parameter selection_sort.15"
       locfile="../selection_sort.mlw"
-      loclnum="20" loccnumb="6" loccnume="20"
+      loclnum="14" loccnumb="6" loccnume="20"
       expl="15. assertion"
-      sum="08feebc410be2b1657e7fe7d153ecb3a"
+      sum="04efb12ca0439869e537330c8f91773d"
       proved="true"
-      expanded="true"
+      expanded="false"
       shape="apermutV4V8IaexchangeV3V7V6V5Aainfix &lt;=c0V0Lamk arrayV0V7FIainfix &lt;V5V0Aainfix &lt;=c0V5Aainfix &lt;V6V0Aainfix &lt;=c0V6Iainfix =V6V5NIainfix &lt;=agetV3V6agetV3V9Iainfix &lt;V9ainfix +ainfix -V0c1c1Aainfix &lt;=V5V9FAainfix &lt;V6ainfix +ainfix -V0c1c1Aainfix &lt;=V5V6FIainfix &lt;=ainfix +V5c1ainfix -V0c1Iainfix &lt;=c0V0Iainfix &lt;=agetV3V10agetV3V11Iainfix &lt;V11V0Aainfix &lt;=V5V11Aainfix &lt;V10V5Aainfix &lt;=c0V10FAapermutV2V4Aasorted_subV3c0V5Iainfix &lt;=V5ainfix -V0c1Aainfix &lt;=c0V5FLamk arrayV0V3FIainfix &lt;=c0ainfix -V0c1Iainfix &lt;=c0V0Lamk arrayV0V1FF">
       <label
        name="expl:VC for selection_sort"/>
@@ -357,31 +337,88 @@
      <goal
       name="WP_parameter selection_sort.16"
       locfile="../selection_sort.mlw"
-      loclnum="20" loccnumb="6" loccnume="20"
+      loclnum="14" loccnumb="6" loccnume="20"
       expl="16. loop invariant preservation"
-      sum="fcb33e0af11c7adabce9c819675281b6"
+      sum="4e40e893fff19ce10fedce7640dcc9e7"
       proved="true"
       expanded="true"
       shape="ainfix &lt;=agetV7V9agetV7V10Iainfix &lt;V10V0Aainfix &lt;=ainfix +V5c1V10Aainfix &lt;V9ainfix +V5c1Aainfix &lt;=c0V9FAapermutV2V8Aasorted_subV7c0ainfix +V5c1IapermutV4V8IaexchangeV3V7V6V5Aainfix &lt;=c0V0Lamk arrayV0V7FIainfix &lt;V5V0Aainfix &lt;=c0V5Aainfix &lt;V6V0Aainfix &lt;=c0V6Iainfix =V6V5NIainfix &lt;=agetV3V6agetV3V11Iainfix &lt;V11ainfix +ainfix -V0c1c1Aainfix &lt;=V5V11FAainfix &lt;V6ainfix +ainfix -V0c1c1Aainfix &lt;=V5V6FIainfix &lt;=ainfix +V5c1ainfix -V0c1Iainfix &lt;=c0V0Iainfix &lt;=agetV3V12agetV3V13Iainfix &lt;V13V0Aainfix &lt;=V5V13Aainfix &lt;V12V5Aainfix &lt;=c0V12FAapermutV2V4Aasorted_subV3c0V5Iainfix &lt;=V5ainfix -V0c1Aainfix &lt;=c0V5FLamk arrayV0V3FIainfix &lt;=c0ainfix -V0c1Iainfix &lt;=c0V0Lamk arrayV0V1FF">
       <label
        name="expl:VC for selection_sort"/>
-      <proof
-       prover="0"
-       timelimit="5"
-       memlimit="1000"
-       obsolete="false"
-       archived="false">
-       <result status="valid" time="3.26"/>
-      </proof>
+      <transf
+       name="split_goal_wp"
+       proved="true"
+       expanded="true">
+       <goal
+        name="WP_parameter selection_sort.16.1"
+        locfile="../selection_sort.mlw"
+        loclnum="14" loccnumb="6" loccnume="20"
+        expl="1."
+        sum="068118a1190f596b6575e3bef7955b0d"
+        proved="true"
+        expanded="false"
+        shape="asorted_subV7c0ainfix +V5c1IapermutV4V8IaexchangeV3V7V6V5Aainfix &lt;=c0V0Lamk arrayV0V7FIainfix &lt;V5V0Aainfix &lt;=c0V5Aainfix &lt;V6V0Aainfix &lt;=c0V6Iainfix =V6V5NIainfix &lt;=agetV3V6agetV3V9Iainfix &lt;V9ainfix +ainfix -V0c1c1Aainfix &lt;=V5V9FAainfix &lt;V6ainfix +ainfix -V0c1c1Aainfix &lt;=V5V6FIainfix &lt;=ainfix +V5c1ainfix -V0c1Iainfix &lt;=c0V0Iainfix &lt;=agetV3V10agetV3V11Iainfix &lt;V11V0Aainfix &lt;=V5V11Aainfix &lt;V10V5Aainfix &lt;=c0V10FAapermutV2V4Aasorted_subV3c0V5Iainfix &lt;=V5ainfix -V0c1Aainfix &lt;=c0V5FLamk arrayV0V3FIainfix &lt;=c0ainfix -V0c1Iainfix &lt;=c0V0Lamk arrayV0V1FF">
+        <label
+         name="expl:VC for selection_sort"/>
+        <proof
+         prover="1"
+         timelimit="5"
+         memlimit="1000"
+         obsolete="false"
+         archived="false">
+         <result status="valid" time="0.27"/>
+        </proof>
+       </goal>
+       <goal
+        name="WP_parameter selection_sort.16.2"
+        locfile="../selection_sort.mlw"
+        loclnum="14" loccnumb="6" loccnume="20"
+        expl="2."
+        sum="5277a7e3b38e2c1cd78349afda99f95e"
+        proved="true"
+        expanded="false"
+        shape="apermutV2V8IapermutV4V8IaexchangeV3V7V6V5Aainfix &lt;=c0V0Lamk arrayV0V7FIainfix &lt;V5V0Aainfix &lt;=c0V5Aainfix &lt;V6V0Aainfix &lt;=c0V6Iainfix =V6V5NIainfix &lt;=agetV3V6agetV3V9Iainfix &lt;V9ainfix +ainfix -V0c1c1Aainfix &lt;=V5V9FAainfix &lt;V6ainfix +ainfix -V0c1c1Aainfix &lt;=V5V6FIainfix &lt;=ainfix +V5c1ainfix -V0c1Iainfix &lt;=c0V0Iainfix &lt;=agetV3V10agetV3V11Iainfix &lt;V11V0Aainfix &lt;=V5V11Aainfix &lt;V10V5Aainfix &lt;=c0V10FAapermutV2V4Aasorted_subV3c0V5Iainfix &lt;=V5ainfix -V0c1Aainfix &lt;=c0V5FLamk arrayV0V3FIainfix &lt;=c0ainfix -V0c1Iainfix &lt;=c0V0Lamk arrayV0V1FF">
+        <label
+         name="expl:VC for selection_sort"/>
+        <proof
+         prover="1"
+         timelimit="5"
+         memlimit="1000"
+         obsolete="false"
+         archived="false">
+         <result status="valid" time="0.04"/>
+        </proof>
+       </goal>
+       <goal
+        name="WP_parameter selection_sort.16.3"
+        locfile="../selection_sort.mlw"
+        loclnum="14" loccnumb="6" loccnume="20"
+        expl="3."
+        sum="6efbf5eb09b121f4395974d9c7b33a05"
+        proved="true"
+        expanded="false"
+        shape="ainfix &lt;=agetV7V9agetV7V10Iainfix &lt;V10V0Aainfix &lt;=ainfix +V5c1V10Aainfix &lt;V9ainfix +V5c1Aainfix &lt;=c0V9FIapermutV4V8IaexchangeV3V7V6V5Aainfix &lt;=c0V0Lamk arrayV0V7FIainfix &lt;V5V0Aainfix &lt;=c0V5Aainfix &lt;V6V0Aainfix &lt;=c0V6Iainfix =V6V5NIainfix &lt;=agetV3V6agetV3V11Iainfix &lt;V11ainfix +ainfix -V0c1c1Aainfix &lt;=V5V11FAainfix &lt;V6ainfix +ainfix -V0c1c1Aainfix &lt;=V5V6FIainfix &lt;=ainfix +V5c1ainfix -V0c1Iainfix &lt;=c0V0Iainfix &lt;=agetV3V12agetV3V13Iainfix &lt;V13V0Aainfix &lt;=V5V13Aainfix &lt;V12V5Aainfix &lt;=c0V12FAapermutV2V4Aasorted_subV3c0V5Iainfix &lt;=V5ainfix -V0c1Aainfix &lt;=c0V5FLamk arrayV0V3FIainfix &lt;=c0ainfix -V0c1Iainfix &lt;=c0V0Lamk arrayV0V1FF">
+        <label
+         name="expl:VC for selection_sort"/>
+        <proof
+         prover="1"
+         timelimit="5"
+         memlimit="1000"
+         obsolete="false"
+         archived="false">
+         <result status="valid" time="0.29"/>
+        </proof>
+       </goal>
+      </transf>
      </goal>
      <goal
       name="WP_parameter selection_sort.17"
       locfile="../selection_sort.mlw"
-      loclnum="20" loccnumb="6" loccnume="20"
+      loclnum="14" loccnumb="6" loccnume="20"
       expl="17. assertion"
-      sum="603c24d7e13fb760ec24125b84744bd3"
+      sum="339c6a9ae31f8eec187978b88658f1e2"
       proved="true"
-      expanded="true"
+      expanded="false"
       shape="apermutV4V4Iainfix =V6V5NNIainfix &lt;=agetV3V6agetV3V7Iainfix &lt;V7ainfix +ainfix -V0c1c1Aainfix &lt;=V5V7FAainfix &lt;V6ainfix +ainfix -V0c1c1Aainfix &lt;=V5V6FIainfix &lt;=ainfix +V5c1ainfix -V0c1Iainfix &lt;=c0V0Iainfix &lt;=agetV3V8agetV3V9Iainfix &lt;V9V0Aainfix &lt;=V5V9Aainfix &lt;V8V5Aainfix &lt;=c0V8FAapermutV2V4Aasorted_subV3c0V5Iainfix &lt;=V5ainfix -V0c1Aainfix &lt;=c0V5FLamk arrayV0V3FIainfix &lt;=c0ainfix -V0c1Iainfix &lt;=c0V0Lamk arrayV0V1FF">
       <label
        name="expl:VC for selection_sort"/>
@@ -397,9 +434,9 @@
      <goal
       name="WP_parameter selection_sort.18"
       locfile="../selection_sort.mlw"
-      loclnum="20" loccnumb="6" loccnume="20"
+      loclnum="14" loccnumb="6" loccnume="20"
       expl="18. loop invariant preservation"
-      sum="2203a067ed5679766bbfb9defac35fcf"
+      sum="d9247e35507d9583ec0909fa68cfb600"
       proved="true"
       expanded="true"
       shape="ainfix &lt;=agetV3V7agetV3V8Iainfix &lt;V8V0Aainfix &lt;=ainfix +V5c1V8Aainfix &lt;V7ainfix +V5c1Aainfix &lt;=c0V7FAapermutV2V4Aasorted_subV3c0ainfix +V5c1IapermutV4V4Iainfix =V6V5NNIainfix &lt;=agetV3V6agetV3V9Iainfix &lt;V9ainfix +ainfix -V0c1c1Aainfix &lt;=V5V9FAainfix &lt;V6ainfix +ainfix -V0c1c1Aainfix &lt;=V5V6FIainfix &lt;=ainfix +V5c1ainfix -V0c1Iainfix &lt;=c0V0Iainfix &lt;=agetV3V10agetV3V11Iainfix &lt;V11V0Aainfix &lt;=V5V11Aainfix &lt;V10V5Aainfix &lt;=c0V10FAapermutV2V4Aasorted_subV3c0V5Iainfix &lt;=V5ainfix -V0c1Aainfix &lt;=c0V5FLamk arrayV0V3FIainfix &lt;=c0ainfix -V0c1Iainfix &lt;=c0V0Lamk arrayV0V1FF">
@@ -417,9 +454,9 @@
      <goal
       name="WP_parameter selection_sort.19"
       locfile="../selection_sort.mlw"
-      loclnum="20" loccnumb="6" loccnume="20"
+      loclnum="14" loccnumb="6" loccnume="20"
       expl="19. type invariant"
-      sum="aa8baaec1620d14b2809fdd3eca5a588"
+      sum="38436f14c13602682613764969c8676b"
       proved="true"
       expanded="false"
       shape="ainfix &lt;=c0V0Iainfix &lt;=agetV3V5agetV3V6Iainfix &lt;V6V0Aainfix &lt;=ainfix +ainfix -V0c1c1V6Aainfix &lt;V5ainfix +ainfix -V0c1c1Aainfix &lt;=c0V5FAapermutV2V4Aasorted_subV3c0ainfix +ainfix -V0c1c1Lamk arrayV0V3FIainfix &lt;=c0ainfix -V0c1Iainfix &lt;=c0V0Lamk arrayV0V1FF">
@@ -437,9 +474,9 @@
      <goal
       name="WP_parameter selection_sort.20"
       locfile="../selection_sort.mlw"
-      loclnum="20" loccnumb="6" loccnume="20"
+      loclnum="14" loccnumb="6" loccnume="20"
       expl="20. postcondition"
-      sum="4fd7091b1822b744fa971c2b96106643"
+      sum="d3b298af16cc01ee0fcdb5f80c6d9e21"
       proved="true"
       expanded="true"
       shape="apermutV2V4Aasorted_subV3c0V0Iainfix &lt;=c0V0Iainfix &lt;=agetV3V5agetV3V6Iainfix &lt;V6V0Aainfix &lt;=ainfix +ainfix -V0c1c1V6Aainfix &lt;V5ainfix +ainfix -V0c1c1Aainfix &lt;=c0V5FAapermutV2V4Aasorted_subV3c0ainfix +ainfix -V0c1c1Lamk arrayV0V3FIainfix &lt;=c0ainfix -V0c1Iainfix &lt;=c0V0Lamk arrayV0V1FF">
diff --git a/examples/vstte12_two_way_sort.mlw b/examples/vstte12_two_way_sort.mlw
index 7eb915d0a..eb8af1aa1 100644
--- a/examples/vstte12_two_way_sort.mlw
+++ b/examples/vstte12_two_way_sort.mlw
@@ -11,6 +11,7 @@ module TwoWaySort
   use import bool.Bool
   use import ref.Refint
   use import array.Array
+  use import array.ArraySwap
   use import array.ArrayPermut
 
   predicate le (x y: bool) = x = False \/ y = True
@@ -18,13 +19,6 @@ module TwoWaySort
   predicate sorted (a: array bool) =
     forall i1 i2: int. 0 <= i1 <= i2 < a.length -> le a[i1] a[i2]
 
-  let swap (a: array bool) (i: int) (j: int)
-    requires { 0 <= i < length a /\ 0 <= j < length a }
-    ensures { exchange (old a) a i j }
-  = let v = a[i] in
-    a[i] <- a[j];
-    a[j] <- v
-
   let two_way_sort (a: array bool)
     ensures { sorted a /\ permut (old a) a }
   = 'Init:
diff --git a/examples/vstte12_two_way_sort/why3session.xml b/examples/vstte12_two_way_sort/why3session.xml
index 6abce0fe8..d9fc20501 100644
--- a/examples/vstte12_two_way_sort/why3session.xml
+++ b/examples/vstte12_two_way_sort/why3session.xml
@@ -27,32 +27,12 @@
    loclnum="8" loccnumb="7" loccnume="17"
    verified="true"
    expanded="true">
-   <goal
-    name="WP_parameter swap"
-    locfile="../vstte12_two_way_sort.mlw"
-    loclnum="21" loccnumb="6" loccnume="10"
-    expl="VC for swap"
-    sum="67eb04c719b033488a7a2e9aefae6c9b"
-    proved="true"
-    expanded="false"
-    shape="aexchangeV3V5V1V2Iainfix =V5asetV4V2agetV3V1Aainfix &lt;=c0V0FAainfix &lt;V2V0Aainfix &lt;=c0V2Iainfix =V4asetV3V1agetV3V2Aainfix &lt;=c0V0FAainfix &lt;V1V0Aainfix &lt;=c0V1Aainfix &lt;V2V0Aainfix &lt;=c0V2Aainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V2V0Aainfix &lt;=c0V2Aainfix &lt;V1V0Aainfix &lt;=c0V1Aainfix &lt;=c0V0FF">
-    <label
-     name="expl:VC for swap"/>
-    <proof
-     prover="0"
-     timelimit="10"
-     memlimit="0"
-     obsolete="false"
-     archived="false">
-     <result status="valid" time="0.02"/>
-    </proof>
-   </goal>
    <goal
     name="WP_parameter two_way_sort"
     locfile="../vstte12_two_way_sort.mlw"
-    loclnum="28" loccnumb="6" loccnume="18"
+    loclnum="22" loccnumb="6" loccnume="18"
     expl="VC for two_way_sort"
-    sum="da33e566a3302627d87d68f41a4d3c49"
+    sum="958606c45d3addd1f626be60e680474e"
     proved="true"
     expanded="true"
     shape="iainfix &lt;V4V3iainfix =agetV5V4aTrueNainfix &lt;ainfix -V3V7ainfix -V3V4Aainfix &lt;=c0ainfix -V3V4Aainfix =agetV5V8aTrueIainfix &lt;V8V0Aainfix &lt;V3V8FAainfix =agetV5V9aFalseIainfix &lt;V9V7Aainfix &lt;=c0V9FAapermutV2V6Aainfix &lt;V3V0Aainfix &lt;=c0V7Iainfix =V7ainfix +V4c1Fiainfix =agetV5V3aTrueainfix &lt;ainfix -V10V4ainfix -V3V4Aainfix &lt;=c0ainfix -V3V4Aainfix =agetV5V11aTrueIainfix &lt;V11V0Aainfix &lt;V10V11FAainfix =agetV5V12aFalseIainfix &lt;V12V4Aainfix &lt;=c0V12FAapermutV2V6Aainfix &lt;V10V0Aainfix &lt;=c0V4Iainfix =V10ainfix -V3c1Fainfix &lt;ainfix -V15V14ainfix -V3V4Aainfix &lt;=c0ainfix -V3V4Aainfix =agetV13V16aTrueIainfix &lt;V16V0Aainfix &lt;V15V16FAainfix =agetV13V17aFalseIainfix &lt;V17V14Aainfix &lt;=c0V17FAapermutV2amk arrayV0V13Aainfix &lt;V15V0Aainfix &lt;=c0V14Iainfix =V15ainfix -V3c1FIainfix =V14ainfix +V4c1FIaexchangeV5V13V4V3Aainfix &lt;=c0V0FAainfix &lt;V3V0Aainfix &lt;=c0V3Aainfix &lt;V4V0Aainfix &lt;=c0V4Aainfix &lt;V3V0Aainfix &lt;=c0V3Aainfix &lt;V4V0Aainfix &lt;=c0V4Aainfix &lt;=c0V0apermutV2V6AasortedV6Aainfix &lt;=c0V0Iainfix =agetV5V18aTrueIainfix &lt;V18V0Aainfix &lt;V3V18FAainfix =agetV5V19aFalseIainfix &lt;V19V4Aainfix &lt;=c0V19FAapermutV2V6Aainfix &lt;V3V0Aainfix &lt;=c0V4Lamk arrayV0V5FAainfix =agetV1V20aTrueIainfix &lt;V20V0Aainfix &lt;ainfix -V0c1V20FAainfix =agetV1V21aFalseIainfix &lt;V21c0Aainfix &lt;=c0V21FAapermutV2V2Aainfix &lt;ainfix -V0c1V0Aainfix &lt;=c0c0Iainfix &lt;=c0V0Lamk arrayV0V1FF">
@@ -65,9 +45,9 @@
      <goal
       name="WP_parameter two_way_sort.1"
       locfile="../vstte12_two_way_sort.mlw"
-      loclnum="28" loccnumb="6" loccnume="18"
+      loclnum="22" loccnumb="6" loccnume="18"
       expl="1. loop invariant init"
-      sum="1a1264dc58cdd1f00287c30a7bed3111"
+      sum="f718540d43bc8afe310f3b6f351cf3f9"
       proved="true"
       expanded="false"
       shape="ainfix =agetV1V3aTrueIainfix &lt;V3V0Aainfix &lt;ainfix -V0c1V3FAainfix =agetV1V4aFalseIainfix &lt;V4c0Aainfix &lt;=c0V4FAapermutV2V2Aainfix &lt;ainfix -V0c1V0Aainfix &lt;=c0c0Iainfix &lt;=c0V0Lamk arrayV0V1FF">
@@ -85,9 +65,9 @@
      <goal
       name="WP_parameter two_way_sort.2"
       locfile="../vstte12_two_way_sort.mlw"
-      loclnum="28" loccnumb="6" loccnume="18"
+      loclnum="22" loccnumb="6" loccnume="18"
       expl="2. type invariant"
-      sum="b1e5647c1ed7f49ec82fd240ece70f30"
+      sum="c48732f22206344e1cfe35e51ce5657f"
       proved="true"
       expanded="false"
       shape="ainfix &lt;=c0V0Iainfix &lt;V4V3Iainfix =agetV5V7aTrueIainfix &lt;V7V0Aainfix &lt;V3V7FAainfix =agetV5V8aFalseIainfix &lt;V8V4Aainfix &lt;=c0V8FAapermutV2V6Aainfix &lt;V3V0Aainfix &lt;=c0V4Lamk arrayV0V5FIainfix &lt;=c0V0Lamk arrayV0V1FF">
@@ -105,9 +85,9 @@
      <goal
       name="WP_parameter two_way_sort.3"
       locfile="../vstte12_two_way_sort.mlw"
-      loclnum="28" loccnumb="6" loccnume="18"
+      loclnum="22" loccnumb="6" loccnume="18"
       expl="3. precondition"
-      sum="8820759f0f3909a4d3176ade3ba82c64"
+      sum="af0541a7c5c9f60b67f3019d1de259e8"
       proved="true"
       expanded="false"
       shape="ainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix &lt;=c0V0Iainfix &lt;V4V3Iainfix =agetV5V7aTrueIainfix &lt;V7V0Aainfix &lt;V3V7FAainfix =agetV5V8aFalseIainfix &lt;V8V4Aainfix &lt;=c0V8FAapermutV2V6Aainfix &lt;V3V0Aainfix &lt;=c0V4Lamk arrayV0V5FIainfix &lt;=c0V0Lamk arrayV0V1FF">
@@ -125,9 +105,9 @@
      <goal
       name="WP_parameter two_way_sort.4"
       locfile="../vstte12_two_way_sort.mlw"
-      loclnum="28" loccnumb="6" loccnume="18"
+      loclnum="22" loccnumb="6" loccnume="18"
       expl="4. loop invariant preservation"
-      sum="21a06e7811079a74e691427ad2e0f3d1"
+      sum="f90e7ec5027581b0c4845619637191e7"
       proved="true"
       expanded="false"
       shape="ainfix =agetV5V8aTrueIainfix &lt;V8V0Aainfix &lt;V3V8FAainfix =agetV5V9aFalseIainfix &lt;V9V7Aainfix &lt;=c0V9FAapermutV2V6Aainfix &lt;V3V0Aainfix &lt;=c0V7Iainfix =V7ainfix +V4c1FIainfix =agetV5V4aTrueNIainfix &lt;V4V0Aainfix &lt;=c0V4Aainfix &lt;=c0V0Iainfix &lt;V4V3Iainfix =agetV5V10aTrueIainfix &lt;V10V0Aainfix &lt;V3V10FAainfix =agetV5V11aFalseIainfix &lt;V11V4Aainfix &lt;=c0V11FAapermutV2V6Aainfix &lt;V3V0Aainfix &lt;=c0V4Lamk arrayV0V5FIainfix &lt;=c0V0Lamk arrayV0V1FF">
@@ -145,9 +125,9 @@
      <goal
       name="WP_parameter two_way_sort.5"
       locfile="../vstte12_two_way_sort.mlw"
-      loclnum="28" loccnumb="6" loccnume="18"
+      loclnum="22" loccnumb="6" loccnume="18"
       expl="5. loop variant decrease"
-      sum="d31c1d030e7b58eb9ce025046292f0ec"
+      sum="6b9f5825d524183767354117559f5284"
       proved="true"
       expanded="false"
       shape="ainfix &lt;ainfix -V3V7ainfix -V3V4Aainfix &lt;=c0ainfix -V3V4Iainfix =V7ainfix +V4c1FIainfix =agetV5V4aTrueNIainfix &lt;V4V0Aainfix &lt;=c0V4Aainfix &lt;=c0V0Iainfix &lt;V4V3Iainfix =agetV5V8aTrueIainfix &lt;V8V0Aainfix &lt;V3V8FAainfix =agetV5V9aFalseIainfix &lt;V9V4Aainfix &lt;=c0V9FAapermutV2V6Aainfix &lt;V3V0Aainfix &lt;=c0V4Lamk arrayV0V5FIainfix &lt;=c0V0Lamk arrayV0V1FF">
@@ -165,9 +145,9 @@
      <goal
       name="WP_parameter two_way_sort.6"
       locfile="../vstte12_two_way_sort.mlw"
-      loclnum="28" loccnumb="6" loccnume="18"
+      loclnum="22" loccnumb="6" loccnume="18"
       expl="6. precondition"
-      sum="a625d1eb2156b34d86599820591ef838"
+      sum="a5630453cb0250c867639beee866dd61"
       proved="true"
       expanded="false"
       shape="ainfix &lt;V3V0Aainfix &lt;=c0V3Iainfix =agetV5V4aTrueNNIainfix &lt;V4V0Aainfix &lt;=c0V4Aainfix &lt;=c0V0Iainfix &lt;V4V3Iainfix =agetV5V7aTrueIainfix &lt;V7V0Aainfix &lt;V3V7FAainfix =agetV5V8aFalseIainfix &lt;V8V4Aainfix &lt;=c0V8FAapermutV2V6Aainfix &lt;V3V0Aainfix &lt;=c0V4Lamk arrayV0V5FIainfix &lt;=c0V0Lamk arrayV0V1FF">
@@ -185,9 +165,9 @@
      <goal
       name="WP_parameter two_way_sort.7"
       locfile="../vstte12_two_way_sort.mlw"
-      loclnum="28" loccnumb="6" loccnume="18"
+      loclnum="22" loccnumb="6" loccnume="18"
       expl="7. loop invariant preservation"
-      sum="83284344a0b6ada0f2f3326f2e089c19"
+      sum="98e480e5587a0756f4bb6b76b2d31adb"
       proved="true"
       expanded="false"
       shape="ainfix =agetV5V8aTrueIainfix &lt;V8V0Aainfix &lt;V7V8FAainfix =agetV5V9aFalseIainfix &lt;V9V4Aainfix &lt;=c0V9FAapermutV2V6Aainfix &lt;V7V0Aainfix &lt;=c0V4Iainfix =V7ainfix -V3c1FIainfix =agetV5V3aTrueIainfix &lt;V3V0Aainfix &lt;=c0V3Iainfix =agetV5V4aTrueNNIainfix &lt;V4V0Aainfix &lt;=c0V4Aainfix &lt;=c0V0Iainfix &lt;V4V3Iainfix =agetV5V10aTrueIainfix &lt;V10V0Aainfix &lt;V3V10FAainfix =agetV5V11aFalseIainfix &lt;V11V4Aainfix &lt;=c0V11FAapermutV2V6Aainfix &lt;V3V0Aainfix &lt;=c0V4Lamk arrayV0V5FIainfix &lt;=c0V0Lamk arrayV0V1FF">
@@ -205,9 +185,9 @@
      <goal
       name="WP_parameter two_way_sort.8"
       locfile="../vstte12_two_way_sort.mlw"
-      loclnum="28" loccnumb="6" loccnume="18"
+      loclnum="22" loccnumb="6" loccnume="18"
       expl="8. loop variant decrease"
-      sum="92bbd1436c05771c86f965545079929c"
+      sum="88cffa09fcd4cc5f8fa231bf5d089049"
       proved="true"
       expanded="false"
       shape="ainfix &lt;ainfix -V7V4ainfix -V3V4Aainfix &lt;=c0ainfix -V3V4Iainfix =V7ainfix -V3c1FIainfix =agetV5V3aTrueIainfix &lt;V3V0Aainfix &lt;=c0V3Iainfix =agetV5V4aTrueNNIainfix &lt;V4V0Aainfix &lt;=c0V4Aainfix &lt;=c0V0Iainfix &lt;V4V3Iainfix =agetV5V8aTrueIainfix &lt;V8V0Aainfix &lt;V3V8FAainfix =agetV5V9aFalseIainfix &lt;V9V4Aainfix &lt;=c0V9FAapermutV2V6Aainfix &lt;V3V0Aainfix &lt;=c0V4Lamk arrayV0V5FIainfix &lt;=c0V0Lamk arrayV0V1FF">
@@ -225,9 +205,9 @@
      <goal
       name="WP_parameter two_way_sort.9"
       locfile="../vstte12_two_way_sort.mlw"
-      loclnum="28" loccnumb="6" loccnume="18"
+      loclnum="22" loccnumb="6" loccnume="18"
       expl="9. precondition"
-      sum="f7d0a9220bd709c58a73e15ce38b514d"
+      sum="43526ba1bd5902cbfe76762cfda0b427"
       proved="true"
       expanded="false"
       shape="ainfix &lt;V3V0Aainfix &lt;=c0V3Aainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix =agetV5V3aTrueNIainfix &lt;V3V0Aainfix &lt;=c0V3Iainfix =agetV5V4aTrueNNIainfix &lt;V4V0Aainfix &lt;=c0V4Aainfix &lt;=c0V0Iainfix &lt;V4V3Iainfix =agetV5V7aTrueIainfix &lt;V7V0Aainfix &lt;V3V7FAainfix =agetV5V8aFalseIainfix &lt;V8V4Aainfix &lt;=c0V8FAapermutV2V6Aainfix &lt;V3V0Aainfix &lt;=c0V4Lamk arrayV0V5FIainfix &lt;=c0V0Lamk arrayV0V1FF">
@@ -245,9 +225,9 @@
      <goal
       name="WP_parameter two_way_sort.10"
       locfile="../vstte12_two_way_sort.mlw"
-      loclnum="28" loccnumb="6" loccnume="18"
+      loclnum="22" loccnumb="6" loccnume="18"
       expl="10. loop invariant preservation"
-      sum="479a1ae0b59d5d083ced427f40d017a1"
+      sum="4a3859f711897883177e66b531be48e3"
       proved="true"
       expanded="false"
       shape="ainfix =agetV7V10aTrueIainfix &lt;V10V0Aainfix &lt;V9V10FAainfix =agetV7V11aFalseIainfix &lt;V11V8Aainfix &lt;=c0V11FAapermutV2amk arrayV0V7Aainfix &lt;V9V0Aainfix &lt;=c0V8Iainfix =V9ainfix -V3c1FIainfix =V8ainfix +V4c1FIaexchangeV5V7V4V3Aainfix &lt;=c0V0FIainfix &lt;V3V0Aainfix &lt;=c0V3Aainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix =agetV5V3aTrueNIainfix &lt;V3V0Aainfix &lt;=c0V3Iainfix =agetV5V4aTrueNNIainfix &lt;V4V0Aainfix &lt;=c0V4Aainfix &lt;=c0V0Iainfix &lt;V4V3Iainfix =agetV5V12aTrueIainfix &lt;V12V0Aainfix &lt;V3V12FAainfix =agetV5V13aFalseIainfix &lt;V13V4Aainfix &lt;=c0V13FAapermutV2V6Aainfix &lt;V3V0Aainfix &lt;=c0V4Lamk arrayV0V5FIainfix &lt;=c0V0Lamk arrayV0V1FF">
@@ -260,9 +240,9 @@
        <goal
         name="WP_parameter two_way_sort.10.1"
         locfile="../vstte12_two_way_sort.mlw"
-        loclnum="28" loccnumb="6" loccnume="18"
+        loclnum="22" loccnumb="6" loccnume="18"
         expl="1."
-        sum="f7e086e0b253533453c68a34d47e928f"
+        sum="6e47fa7d84938f6f2834faae7b424c6b"
         proved="true"
         expanded="false"
         shape="ainfix &lt;=c0V8Iainfix =V9ainfix -V3c1FIainfix =V8ainfix +V4c1FIaexchangeV5V7V4V3Aainfix &lt;=c0V0FIainfix &lt;V3V0Aainfix &lt;=c0V3Aainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix =agetV5V3aTrueNIainfix &lt;V3V0Aainfix &lt;=c0V3Iainfix =agetV5V4aTrueNNIainfix &lt;V4V0Aainfix &lt;=c0V4Aainfix &lt;=c0V0Iainfix &lt;V4V3Iainfix =agetV5V10aTrueIainfix &lt;V10V0Aainfix &lt;V3V10FAainfix =agetV5V11aFalseIainfix &lt;V11V4Aainfix &lt;=c0V11FAapermutV2V6Aainfix &lt;V3V0Aainfix &lt;=c0V4Lamk arrayV0V5FIainfix &lt;=c0V0Lamk arrayV0V1FF">
@@ -280,9 +260,9 @@
        <goal
         name="WP_parameter two_way_sort.10.2"
         locfile="../vstte12_two_way_sort.mlw"
-        loclnum="28" loccnumb="6" loccnume="18"
+        loclnum="22" loccnumb="6" loccnume="18"
         expl="2."
-        sum="18896ab8f8b7997fd388cad04c6ebabf"
+        sum="977b7d989e773e916a21465b7d2b564c"
         proved="true"
         expanded="false"
         shape="ainfix &lt;V9V0Iainfix =V9ainfix -V3c1FIainfix =V8ainfix +V4c1FIaexchangeV5V7V4V3Aainfix &lt;=c0V0FIainfix &lt;V3V0Aainfix &lt;=c0V3Aainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix =agetV5V3aTrueNIainfix &lt;V3V0Aainfix &lt;=c0V3Iainfix =agetV5V4aTrueNNIainfix &lt;V4V0Aainfix &lt;=c0V4Aainfix &lt;=c0V0Iainfix &lt;V4V3Iainfix =agetV5V10aTrueIainfix &lt;V10V0Aainfix &lt;V3V10FAainfix =agetV5V11aFalseIainfix &lt;V11V4Aainfix &lt;=c0V11FAapermutV2V6Aainfix &lt;V3V0Aainfix &lt;=c0V4Lamk arrayV0V5FIainfix &lt;=c0V0Lamk arrayV0V1FF">
@@ -300,9 +280,9 @@
        <goal
         name="WP_parameter two_way_sort.10.3"
         locfile="../vstte12_two_way_sort.mlw"
-        loclnum="28" loccnumb="6" loccnume="18"
+        loclnum="22" loccnumb="6" loccnume="18"
         expl="3."
-        sum="d52874d8ef31aa186b1794cb12615a73"
+        sum="45e689e73733887524212b237ea7f346"
         proved="true"
         expanded="false"
         shape="apermutV2amk arrayV0V7Iainfix =V9ainfix -V3c1FIainfix =V8ainfix +V4c1FIaexchangeV5V7V4V3Aainfix &lt;=c0V0FIainfix &lt;V3V0Aainfix &lt;=c0V3Aainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix =agetV5V3aTrueNIainfix &lt;V3V0Aainfix &lt;=c0V3Iainfix =agetV5V4aTrueNNIainfix &lt;V4V0Aainfix &lt;=c0V4Aainfix &lt;=c0V0Iainfix &lt;V4V3Iainfix =agetV5V10aTrueIainfix &lt;V10V0Aainfix &lt;V3V10FAainfix =agetV5V11aFalseIainfix &lt;V11V4Aainfix &lt;=c0V11FAapermutV2V6Aainfix &lt;V3V0Aainfix &lt;=c0V4Lamk arrayV0V5FIainfix &lt;=c0V0Lamk arrayV0V1FF">
@@ -315,15 +295,15 @@
          edited="vstte12_two_way_sort_WP_TwoWaySort_WP_parameter_two_way_sort_2.v"
          obsolete="false"
          archived="false">
-         <result status="valid" time="0.51"/>
+         <result status="valid" time="1.75"/>
         </proof>
        </goal>
        <goal
         name="WP_parameter two_way_sort.10.4"
         locfile="../vstte12_two_way_sort.mlw"
-        loclnum="28" loccnumb="6" loccnume="18"
+        loclnum="22" loccnumb="6" loccnume="18"
         expl="4."
-        sum="838969c895df07f1d34d88eb18838f5b"
+        sum="225937e7dbd6855165035bb5af756c78"
         proved="true"
         expanded="false"
         shape="ainfix =agetV7V10aFalseIainfix &lt;V10V8Aainfix &lt;=c0V10FIainfix =V9ainfix -V3c1FIainfix =V8ainfix +V4c1FIaexchangeV5V7V4V3Aainfix &lt;=c0V0FIainfix &lt;V3V0Aainfix &lt;=c0V3Aainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix =agetV5V3aTrueNIainfix &lt;V3V0Aainfix &lt;=c0V3Iainfix =agetV5V4aTrueNNIainfix &lt;V4V0Aainfix &lt;=c0V4Aainfix &lt;=c0V0Iainfix &lt;V4V3Iainfix =agetV5V11aTrueIainfix &lt;V11V0Aainfix &lt;V3V11FAainfix =agetV5V12aFalseIainfix &lt;V12V4Aainfix &lt;=c0V12FAapermutV2V6Aainfix &lt;V3V0Aainfix &lt;=c0V4Lamk arrayV0V5FIainfix &lt;=c0V0Lamk arrayV0V1FF">
@@ -349,9 +329,9 @@
        <goal
         name="WP_parameter two_way_sort.10.5"
         locfile="../vstte12_two_way_sort.mlw"
-        loclnum="28" loccnumb="6" loccnume="18"
+        loclnum="22" loccnumb="6" loccnume="18"
         expl="5."
-        sum="76987f05a3e46d539b55f9dbb435c0cb"
+        sum="b0ed23beeca86528345f54fbae6d5f9a"
         proved="true"
         expanded="false"
         shape="ainfix =agetV7V10aTrueIainfix &lt;V10V0Aainfix &lt;V9V10FIainfix =V9ainfix -V3c1FIainfix =V8ainfix +V4c1FIaexchangeV5V7V4V3Aainfix &lt;=c0V0FIainfix &lt;V3V0Aainfix &lt;=c0V3Aainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix =agetV5V3aTrueNIainfix &lt;V3V0Aainfix &lt;=c0V3Iainfix =agetV5V4aTrueNNIainfix &lt;V4V0Aainfix &lt;=c0V4Aainfix &lt;=c0V0Iainfix &lt;V4V3Iainfix =agetV5V11aTrueIainfix &lt;V11V0Aainfix &lt;V3V11FAainfix =agetV5V12aFalseIainfix &lt;V12V4Aainfix &lt;=c0V12FAapermutV2V6Aainfix &lt;V3V0Aainfix &lt;=c0V4Lamk arrayV0V5FIainfix &lt;=c0V0Lamk arrayV0V1FF">
@@ -379,9 +359,9 @@
      <goal
       name="WP_parameter two_way_sort.11"
       locfile="../vstte12_two_way_sort.mlw"
-      loclnum="28" loccnumb="6" loccnume="18"
+      loclnum="22" loccnumb="6" loccnume="18"
       expl="11. loop variant decrease"
-      sum="e2aaddf34a33f8bbe121b039c12e032a"
+      sum="c55a2bba916d2c9704ff99c25309a2c0"
       proved="true"
       expanded="false"
       shape="ainfix &lt;ainfix -V9V8ainfix -V3V4Aainfix &lt;=c0ainfix -V3V4Iainfix =V9ainfix -V3c1FIainfix =V8ainfix +V4c1FIaexchangeV5V7V4V3Aainfix &lt;=c0V0FIainfix &lt;V3V0Aainfix &lt;=c0V3Aainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix =agetV5V3aTrueNIainfix &lt;V3V0Aainfix &lt;=c0V3Iainfix =agetV5V4aTrueNNIainfix &lt;V4V0Aainfix &lt;=c0V4Aainfix &lt;=c0V0Iainfix &lt;V4V3Iainfix =agetV5V10aTrueIainfix &lt;V10V0Aainfix &lt;V3V10FAainfix =agetV5V11aFalseIainfix &lt;V11V4Aainfix &lt;=c0V11FAapermutV2V6Aainfix &lt;V3V0Aainfix &lt;=c0V4Lamk arrayV0V5FIainfix &lt;=c0V0Lamk arrayV0V1FF">
@@ -399,9 +379,9 @@
      <goal
       name="WP_parameter two_way_sort.12"
       locfile="../vstte12_two_way_sort.mlw"
-      loclnum="28" loccnumb="6" loccnume="18"
+      loclnum="22" loccnumb="6" loccnume="18"
       expl="12. type invariant"
-      sum="0123645afce53940a178a6bd8be72d40"
+      sum="94db2f07e8255d720d7bfced48e11810"
       proved="true"
       expanded="false"
       shape="ainfix &lt;=c0V0Iainfix &lt;V4V3NIainfix =agetV5V7aTrueIainfix &lt;V7V0Aainfix &lt;V3V7FAainfix =agetV5V8aFalseIainfix &lt;V8V4Aainfix &lt;=c0V8FAapermutV2V6Aainfix &lt;V3V0Aainfix &lt;=c0V4Lamk arrayV0V5FIainfix &lt;=c0V0Lamk arrayV0V1FF">
@@ -419,9 +399,9 @@
      <goal
       name="WP_parameter two_way_sort.13"
       locfile="../vstte12_two_way_sort.mlw"
-      loclnum="28" loccnumb="6" loccnume="18"
+      loclnum="22" loccnumb="6" loccnume="18"
       expl="13. postcondition"
-      sum="33785ad8b0d5ce30dbda5da44c04f164"
+      sum="48688df10a3c073f88bdde8415426f74"
       proved="true"
       expanded="false"
       shape="apermutV2V6AasortedV6Iainfix &lt;=c0V0Iainfix &lt;V4V3NIainfix =agetV5V7aTrueIainfix &lt;V7V0Aainfix &lt;V3V7FAainfix =agetV5V8aFalseIainfix &lt;V8V4Aainfix &lt;=c0V8FAapermutV2V6Aainfix &lt;V3V0Aainfix &lt;=c0V4Lamk arrayV0V5FIainfix &lt;=c0V0Lamk arrayV0V1FF">
-- 
GitLab