diff --git a/examples/binomial_heap/why3session.xml b/examples/binomial_heap/why3session.xml
index 9bd9fb727d9213c02458c63eed49773b24ab7022..ca838122b70ca0c25b71eff42592ae3fe13729f6 100644
--- a/examples/binomial_heap/why3session.xml
+++ b/examples/binomial_heap/why3session.xml
@@ -6,7 +6,7 @@
 <prover id="1" name="Alt-Ergo" version="1.01" timelimit="6" steplimit="0" memlimit="1000"/>
 <prover id="2" name="Eprover" version="1.8-001" timelimit="6" steplimit="0" memlimit="1000"/>
 <file name="../binomial_heap.mlw" expanded="true">
-<theory name="BinomialHeap" sum="5b1dd2e701903b8fba3c565ace8f367e" expanded="true">
+<theory name="BinomialHeap" sum="1a8c8f52e3a5b2c123edd808bf508cd1" expanded="true">
  <goal name="WP_parameter size_nonnneg" expl="VC for size_nonnneg">
  <proof prover="0"><result status="valid" time="0.09"/></proof>
  </goal>
diff --git a/examples/binomial_heap/why3shapes.gz b/examples/binomial_heap/why3shapes.gz
index ed26f75cf73f02e4dc64a569ef7a85e0570d8aef..6721d3a83f8a6c00bdb0646e2e107c5c2d9da46f 100644
Binary files a/examples/binomial_heap/why3shapes.gz and b/examples/binomial_heap/why3shapes.gz differ
diff --git a/examples/bitvector_examples/why3session.xml b/examples/bitvector_examples/why3session.xml
index ddd72aa0466c3cc9e18fbe906519a0cba4dc4a3b..e6ae2239ca6753bd613c171c28c1cf9a9ec2d0fb 100644
--- a/examples/bitvector_examples/why3session.xml
+++ b/examples/bitvector_examples/why3session.xml
@@ -6,7 +6,7 @@
 <prover id="2" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="4" name="CVC4" version="1.4" alternative="noBV" timelimit="5" steplimit="0" memlimit="1000"/>
 <file name="../bitvector_examples.mlw" expanded="true">
-<theory name="Test_proofinuse" sum="ab759a44e440a5696e3be5d5c1002f13">
+<theory name="Test_proofinuse" sum="3b40d0771ade481dca5e21ab1783e7b0">
  <goal name="WP_parameter shift_is_div" expl="VC for shift_is_div">
  <transf name="split_goal_wp">
   <goal name="WP_parameter shift_is_div.1" expl="assertion">
diff --git a/examples/bitvector_examples/why3shapes.gz b/examples/bitvector_examples/why3shapes.gz
index e84624dc181eb649df001d610d02d211ac1c6136..38f51245bf3a7c7105e0c6af95321a3d14ed0ba9 100644
Binary files a/examples/bitvector_examples/why3shapes.gz and b/examples/bitvector_examples/why3shapes.gz differ
diff --git a/examples/braun_trees/why3session.xml b/examples/braun_trees/why3session.xml
index dccb786067df8e5104fd84e97ddbaf1786bb98b0..b676f8b1e8b0437b6c2e61c819a046191ef2a62e 100644
--- a/examples/braun_trees/why3session.xml
+++ b/examples/braun_trees/why3session.xml
@@ -5,7 +5,7 @@
 <prover id="0" name="CVC4" version="1.4" timelimit="6" steplimit="0" memlimit="1000"/>
 <prover id="2" name="Alt-Ergo" version="0.99.1" timelimit="6" steplimit="0" memlimit="1000"/>
 <file name="../braun_trees.mlw" expanded="true">
-<theory name="BraunHeaps" sum="e88a215097d30ab497fc4242af794eb6" expanded="true">
+<theory name="BraunHeaps" sum="01ce4495e1108eea8a986b97a904ef17" expanded="true">
  <goal name="WP_parameter root_is_min" expl="VC for root_is_min">
  <proof prover="0"><result status="valid" time="0.10"/></proof>
  </goal>
@@ -385,7 +385,7 @@
   <proof prover="2"><result status="valid" time="0.02" steps="30"/></proof>
   </goal>
   <goal name="WP_parameter inv_height.6" expl="variant decrease">
-  <proof prover="2"><result status="valid" time="0.00" steps="38"/></proof>
+  <proof prover="2"><result status="valid" time="0.00" steps="37"/></proof>
   </goal>
   <goal name="WP_parameter inv_height.7" expl="precondition">
   <proof prover="2"><result status="valid" time="0.02" steps="29"/></proof>
diff --git a/examples/braun_trees/why3shapes.gz b/examples/braun_trees/why3shapes.gz
index 40271c9d200d526ef3bb712d851f0a7c13a3df6b..d47c936037862d9a3317b59c4c9c039a6922d46a 100644
Binary files a/examples/braun_trees/why3shapes.gz and b/examples/braun_trees/why3shapes.gz differ
diff --git a/examples/bts/33_reload_trans/why3shapes.gz b/examples/bts/33_reload_trans/why3shapes.gz
new file mode 100644
index 0000000000000000000000000000000000000000..da6d30c6d8796be4117767beb2bf77adb76531d7
Binary files /dev/null and b/examples/bts/33_reload_trans/why3shapes.gz differ
diff --git a/examples/check-builtin/real/why3session.xml b/examples/check-builtin/real/why3session.xml
index 60bdc33d3b992fd5da1a22a4492c90f6593536ef..a401e9103523a7db19ef51fd0abab193d9f4187c 100644
--- a/examples/check-builtin/real/why3session.xml
+++ b/examples/check-builtin/real/why3session.xml
@@ -106,7 +106,7 @@
  <proof prover="14"><result status="valid" time="0.01"/></proof>
  </goal>
 </theory>
-<theory name="PowerIntTest" sum="cd11768ecfe24cfa9c0b61d85ea97e9c" expanded="true">
+<theory name="PowerIntTest" sum="f226939a990c795aae51223e358ddf04" expanded="true">
  <goal name="Pow_2_2" expl="" expanded="true">
  <proof prover="2"><result status="valid" time="0.00"/></proof>
  <proof prover="8"><result status="valid" time="0.01"/></proof>
diff --git a/examples/check-builtin/real/why3shapes.gz b/examples/check-builtin/real/why3shapes.gz
index 8a03adbbf786a580a624d230cd7953102f57885f..0bb2a17af977c20913c8278986a4185f1a4da9f7 100644
Binary files a/examples/check-builtin/real/why3shapes.gz and b/examples/check-builtin/real/why3shapes.gz differ
diff --git a/examples/fibonacci/why3session.xml b/examples/fibonacci/why3session.xml
index 64601f864511ad402e7f9ce8e1cc8cf121aa215f..6ccbf9a8a4e8586da2e08d4fd916116b24861924 100644
--- a/examples/fibonacci/why3session.xml
+++ b/examples/fibonacci/why3session.xml
@@ -442,7 +442,7 @@
  <proof prover="1"><result status="valid" time="0.00" steps="2"/></proof>
  </goal>
 </theory>
-<theory name="FibonacciLogarithmic" sum="86110d7a411b6691bf6c2b80e6051309">
+<theory name="FibonacciLogarithmic" sum="08625b1d5d1914cd59aef8c8eab6754c">
  <goal name="WP_parameter logfib" expl="VC for logfib">
  <transf name="split_goal_wp">
   <goal name="WP_parameter logfib.1" expl="postcondition">
diff --git a/examples/fibonacci/why3shapes.gz b/examples/fibonacci/why3shapes.gz
index aaf6ae769b4c1cc9e6f5dc80533c0aa81c865031..fa54fa2fb5de905146491ad6c95e0f5f66f342e3 100644
Binary files a/examples/fibonacci/why3shapes.gz and b/examples/fibonacci/why3shapes.gz differ
diff --git a/examples/power/why3session.xml b/examples/power/why3session.xml
index 5262372165c219b5d37ee4c356a0b638873fa9eb..c70ef72fef0423cefbff1e81d7b4d06c4d688132 100644
--- a/examples/power/why3session.xml
+++ b/examples/power/why3session.xml
@@ -2,67 +2,65 @@
 <!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="1.01" timelimit="6" steplimit="0" memlimit="1000"/>
-<prover id="1" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="0"/>
-<prover id="3" name="CVC4" version="1.4" timelimit="6" steplimit="0" memlimit="1000"/>
-<prover id="4" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="0"/>
-<prover id="6" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="0"/>
+<prover id="2" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
+<prover id="5" name="Z3" version="4.5.0" timelimit="5" steplimit="0" memlimit="1000"/>
+<prover id="7" name="CVC4" version="1.5" timelimit="5" steplimit="0" memlimit="1000"/>
 <file name="../power.mlw" expanded="true">
-<theory name="FastExponentiation" sum="372e3fedff8ee241c0b52de2f675ae3a" expanded="true">
- <goal name="WP_parameter fast_exp" expl="VC for fast_exp" expanded="true">
- <proof prover="4" timelimit="3"><result status="valid" time="0.57" steps="55"/></proof>
+<theory name="FastExponentiation" sum="b571612c8c075ebc18bdee600ab0d856" expanded="true">
+ <goal name="WP_parameter fast_exp" expl="VC for fast_exp">
+ <proof prover="2"><result status="valid" time="0.13" steps="44"/></proof>
  </goal>
  <goal name="WP_parameter fast_exp_imperative" expl="VC for fast_exp_imperative" expanded="true">
  <transf name="split_goal_wp" expanded="true">
-  <goal name="WP_parameter fast_exp_imperative.1" expl="loop invariant init" expanded="true">
-  <proof prover="1" timelimit="10"><result status="valid" time="0.00"/></proof>
-  <proof prover="4"><result status="valid" time="0.00" steps="1"/></proof>
-  <proof prover="6"><result status="valid" time="0.00"/></proof>
+  <goal name="WP_parameter fast_exp_imperative.1" expl="loop invariant init">
+  <proof prover="2"><result status="valid" time="0.00" steps="2"/></proof>
+  <proof prover="5"><result status="valid" time="0.01"/></proof>
+  <proof prover="7"><result status="valid" time="0.01"/></proof>
   </goal>
-  <goal name="WP_parameter fast_exp_imperative.2" expl="assertion" expanded="true">
-  <proof prover="0"><result status="valid" time="0.19" steps="14"/></proof>
-  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  <goal name="WP_parameter fast_exp_imperative.2" expl="assertion">
+  <proof prover="7"><result status="valid" time="0.02"/></proof>
   </goal>
-  <goal name="WP_parameter fast_exp_imperative.3" expl="loop invariant preservation" expanded="true">
-  <transf name="split_goal_wp" expanded="true">
-   <goal name="WP_parameter fast_exp_imperative.3.1" expl="VC for fast_exp_imperative" expanded="true">
-   <proof prover="4" timelimit="10" memlimit="1000"><result status="valid" time="0.13" steps="13"/></proof>
+  <goal name="WP_parameter fast_exp_imperative.3" expl="loop invariant preservation">
+  <transf name="split_goal_wp">
+   <goal name="WP_parameter fast_exp_imperative.3.1" expl="VC for fast_exp_imperative">
+   <proof prover="2"><result status="valid" time="0.04" steps="11"/></proof>
+   <proof prover="5"><result status="valid" time="0.02"/></proof>
+   <proof prover="7"><result status="valid" time="0.02"/></proof>
    </goal>
-   <goal name="WP_parameter fast_exp_imperative.3.2" expl="VC for fast_exp_imperative" expanded="true">
-   <proof prover="0"><result status="valid" time="0.80" steps="19"/></proof>
+   <goal name="WP_parameter fast_exp_imperative.3.2" expl="VC for fast_exp_imperative">
+   <proof prover="2"><result status="valid" time="0.50" steps="20"/></proof>
    </goal>
   </transf>
   </goal>
-  <goal name="WP_parameter fast_exp_imperative.4" expl="loop variant decrease" expanded="true">
-  <proof prover="1"><result status="valid" time="0.01"/></proof>
-  <proof prover="4" timelimit="10"><result status="valid" time="0.09" steps="13"/></proof>
-  <proof prover="6"><result status="valid" time="0.01"/></proof>
+  <goal name="WP_parameter fast_exp_imperative.4" expl="loop variant decrease">
+  <proof prover="2"><result status="valid" time="0.56" steps="11"/></proof>
+  <proof prover="5"><result status="valid" time="0.02"/></proof>
+  <proof prover="7"><result status="valid" time="0.02"/></proof>
   </goal>
   <goal name="WP_parameter fast_exp_imperative.5" expl="assertion">
-  <proof prover="0"><result status="valid" time="0.10" steps="21"/></proof>
+  <proof prover="7"><result status="valid" time="0.02"/></proof>
   </goal>
-  <goal name="WP_parameter fast_exp_imperative.6" expl="loop invariant preservation" expanded="true">
-  <transf name="split_goal_wp" expanded="true">
-   <goal name="WP_parameter fast_exp_imperative.6.1" expl="VC for fast_exp_imperative" expanded="true">
-   <proof prover="0"><result status="valid" time="0.08" steps="16"/></proof>
-   <proof prover="1"><result status="valid" time="0.01"/></proof>
-   <proof prover="4"><result status="valid" time="0.02" steps="16"/></proof>
-   <proof prover="6"><result status="valid" time="0.02"/></proof>
+  <goal name="WP_parameter fast_exp_imperative.6" expl="loop invariant preservation">
+  <transf name="split_goal_wp">
+   <goal name="WP_parameter fast_exp_imperative.6.1" expl="VC for fast_exp_imperative">
+   <proof prover="2"><result status="valid" time="0.02" steps="17"/></proof>
+   <proof prover="5"><result status="valid" time="0.02"/></proof>
+   <proof prover="7"><result status="valid" time="0.02"/></proof>
    </goal>
-   <goal name="WP_parameter fast_exp_imperative.6.2" expl="VC for fast_exp_imperative" expanded="true">
-   <proof prover="0"><result status="valid" time="1.81" steps="25"/></proof>
+   <goal name="WP_parameter fast_exp_imperative.6.2" expl="VC for fast_exp_imperative">
+   <proof prover="2"><result status="valid" time="0.49" steps="24"/></proof>
    </goal>
   </transf>
   </goal>
-  <goal name="WP_parameter fast_exp_imperative.7" expl="loop variant decrease" expanded="true">
-  <proof prover="1"><result status="valid" time="0.01"/></proof>
-  <proof prover="4" timelimit="10"><result status="valid" time="1.15" steps="21"/></proof>
-  <proof prover="6"><result status="valid" time="0.02"/></proof>
+  <goal name="WP_parameter fast_exp_imperative.7" expl="loop variant decrease">
+  <proof prover="2"><result status="valid" time="0.29" steps="22"/></proof>
+  <proof prover="5"><result status="valid" time="0.02"/></proof>
+  <proof prover="7"><result status="valid" time="0.02"/></proof>
   </goal>
-  <goal name="WP_parameter fast_exp_imperative.8" expl="postcondition" expanded="true">
-  <transf name="split_goal_wp" expanded="true">
-   <goal name="WP_parameter fast_exp_imperative.8.1" expl="postcondition" expanded="true">
-   <proof prover="4"><result status="valid" time="0.01" steps="5"/></proof>
+  <goal name="WP_parameter fast_exp_imperative.8" expl="postcondition">
+  <transf name="split_goal_wp">
+   <goal name="WP_parameter fast_exp_imperative.8.1" expl="postcondition">
+   <proof prover="2"><result status="valid" time="0.00" steps="6"/></proof>
    </goal>
   </transf>
   </goal>
diff --git a/examples/power/why3shapes.gz b/examples/power/why3shapes.gz
index 01ef89cf6b31d40286ec1dbc7c31ff08604c93c9..38ff6274af4a8182299fa2ccb714b05e7d9cec39 100644
Binary files a/examples/power/why3shapes.gz and b/examples/power/why3shapes.gz differ
diff --git a/examples/sum_of_digits/why3session.xml b/examples/sum_of_digits/why3session.xml
index 215f6eb2e7d9f58d059dcb2f674e674bcaff329a..65a407c55da2b78636f97c89d272f82a3c124f94 100644
--- a/examples/sum_of_digits/why3session.xml
+++ b/examples/sum_of_digits/why3session.xml
@@ -7,7 +7,7 @@
 <prover id="4" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="5" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
 <file name="../sum_of_digits.mlw" expanded="true">
-<theory name="Euler290" sum="c10df07cf9c0b00877454e7d2b02e8f5" expanded="true">
+<theory name="Euler290" sum="6bdd74e0dcf213c8f4a8f4697c6635e6" expanded="true">
  <goal name="Base" expl="">
  <proof prover="4" timelimit="10"><result status="valid" time="0.01" steps="5"/></proof>
  </goal>
diff --git a/examples/sum_of_digits/why3shapes.gz b/examples/sum_of_digits/why3shapes.gz
index 14bd1587117305b852922336a9ead4d917e3f5ea..46fef3cefc1b10155258042168a4e814b7179e5e 100644
Binary files a/examples/sum_of_digits/why3shapes.gz and b/examples/sum_of_digits/why3shapes.gz differ
diff --git a/examples/tests-provers/coq-interval/why3session.xml b/examples/tests-provers/coq-interval/why3session.xml
index d4af3aa947f3c0beff57ea41cf9a07648c7ff236..391a69cc143d7435c4344056f2cce571c6616036 100644
--- a/examples/tests-provers/coq-interval/why3session.xml
+++ b/examples/tests-provers/coq-interval/why3session.xml
@@ -4,7 +4,7 @@
 <why3session shape_version="4">
 <prover id="1" name="Coq" version="8.6.1" timelimit="5" steplimit="0" memlimit="1000"/>
 <file name="../coq-interval.why" expanded="true">
-<theory name="P" sum="43519115242b2f2ec5062978bb1601e1" expanded="true">
+<theory name="P" sum="58d29be40886499ae9897b7609f72f6b" expanded="true">
  <goal name="pow_eps2_max_int" expl="" expanded="true">
  <proof prover="1" edited="coqmninterval_P_pow_eps2_max_int_1.v"><result status="valid" time="1.21"/></proof>
  </goal>
diff --git a/examples/tests-provers/coq-interval/why3shapes.gz b/examples/tests-provers/coq-interval/why3shapes.gz
index af80bb98d5afdca8b2166070ba89d1e27e3d0680..a0db0bfe55a1e8c7aa8d63d7b059591eb6d07631 100644
Binary files a/examples/tests-provers/coq-interval/why3shapes.gz and b/examples/tests-provers/coq-interval/why3shapes.gz differ
diff --git a/examples/tree_of_array/why3session.xml b/examples/tree_of_array/why3session.xml
index ac7ee31b64fc23a4968792ab216389cd404b3cf8..938b7531775846b9db75d9d2817071c512c9bdea 100644
--- a/examples/tree_of_array/why3session.xml
+++ b/examples/tree_of_array/why3session.xml
@@ -4,8 +4,9 @@
 <why3session shape_version="4">
 <prover id="0" name="Alt-Ergo" version="1.30" timelimit="6" steplimit="0" memlimit="1000"/>
 <prover id="1" name="CVC4" version="1.4" timelimit="6" steplimit="0" memlimit="1000"/>
+<prover id="2" name="CVC4" version="1.5" timelimit="5" steplimit="0" memlimit="1000"/>
 <file name="../tree_of_array.mlw" expanded="true">
-<theory name="TreeOfArray" sum="e6cc07771b58c81603582477098238ac" expanded="true">
+<theory name="TreeOfArray" sum="415ae15d24148530a5b2281791ece1b0" expanded="true">
  <goal name="WP_parameter tree_of_array_aux" expl="VC for tree_of_array_aux" expanded="true">
  <transf name="split_goal_wp" expanded="true">
   <goal name="WP_parameter tree_of_array_aux.1" expl="postcondition">
@@ -26,16 +27,16 @@
   <goal name="WP_parameter tree_of_array_aux.6" expl="index in array bounds">
   <proof prover="0"><result status="valid" time="0.01" steps="14"/></proof>
   </goal>
-  <goal name="WP_parameter tree_of_array_aux.7" expl="postcondition" expanded="true">
-  <transf name="split_goal_wp" expanded="true">
+  <goal name="WP_parameter tree_of_array_aux.7" expl="postcondition">
+  <transf name="split_goal_wp">
    <goal name="WP_parameter tree_of_array_aux.7.1" expl="postcondition">
    <proof prover="0"><result status="valid" time="0.01" steps="17"/></proof>
    </goal>
    <goal name="WP_parameter tree_of_array_aux.7.2" expl="postcondition">
-   <proof prover="0"><result status="valid" time="0.17" steps="274"/></proof>
+   <proof prover="0"><result status="valid" time="0.17" steps="270"/></proof>
    </goal>
    <goal name="WP_parameter tree_of_array_aux.7.3" expl="postcondition">
-   <proof prover="0"><result status="valid" time="2.41" steps="1188"/></proof>
+   <proof prover="2"><result status="valid" time="0.16"/></proof>
    </goal>
    <goal name="WP_parameter tree_of_array_aux.7.4" expl="postcondition">
    <proof prover="1"><result status="valid" time="0.13"/></proof>
@@ -44,7 +45,7 @@
   </goal>
  </transf>
  </goal>
- <goal name="WP_parameter tree_of_array" expl="VC for tree_of_array" expanded="true">
+ <goal name="WP_parameter tree_of_array" expl="VC for tree_of_array">
  <proof prover="0"><result status="valid" time="0.01" steps="7"/></proof>
  </goal>
 </theory>
diff --git a/examples/tree_of_array/why3shapes.gz b/examples/tree_of_array/why3shapes.gz
index 9f94bba8dbe0d593635ab0082cd04d9d76ec47b2..d8d74d23c5339b1dea528f09b9a1be4e47d89d61 100644
Binary files a/examples/tree_of_array/why3shapes.gz and b/examples/tree_of_array/why3shapes.gz differ
diff --git a/examples/tree_of_list/why3session.xml b/examples/tree_of_list/why3session.xml
index 4eec1201f8a428de6a3ed8f3085707283d4347da..6de5511408c49d1c66b89b933bded1ebaca7d6b9 100644
--- a/examples/tree_of_list/why3session.xml
+++ b/examples/tree_of_list/why3session.xml
@@ -5,7 +5,7 @@
 <prover id="0" name="CVC4" version="1.4" timelimit="6" steplimit="0" memlimit="1000"/>
 <prover id="2" name="Alt-Ergo" version="0.99.1" timelimit="6" steplimit="0" memlimit="1000"/>
 <file name="../tree_of_list.mlw">
-<theory name="TreeOfList" sum="12d1a0ff628823b4f6f62c68ba956168">
+<theory name="TreeOfList" sum="3f48d5a018203de070ba283a1f39f87a">
  <goal name="WP_parameter tree_of_list_aux" expl="VC for tree_of_list_aux">
  <transf name="split_goal_wp">
   <goal name="WP_parameter tree_of_list_aux.1" expl="postcondition">
diff --git a/examples/tree_of_list/why3shapes.gz b/examples/tree_of_list/why3shapes.gz
index b2b3ed8a39ece7b819f0efc375d7c003c487d9c2..4bde460fa636989003fddbdbb24c16f92d3b9935 100644
Binary files a/examples/tree_of_list/why3shapes.gz and b/examples/tree_of_list/why3shapes.gz differ
diff --git a/examples/verifythis_PrefixSumRec/why3session.xml b/examples/verifythis_PrefixSumRec/why3session.xml
index a79a915585d37c5137ebbfcb722a1781ea861b99..4b00646ef52b38af9cf3f88c676bb5c3a4dfc8ed 100644
--- a/examples/verifythis_PrefixSumRec/why3session.xml
+++ b/examples/verifythis_PrefixSumRec/why3session.xml
@@ -8,7 +8,7 @@
 <prover id="6" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="4000"/>
 <prover id="7" name="Z3" version="4.3.2" timelimit="10" steplimit="0" memlimit="1000"/>
 <file name="../verifythis_PrefixSumRec.mlw" expanded="true">
-<theory name="PrefixSumRec" sum="c290986a5a94ad666d3e6cf1f064bcdd" expanded="true">
+<theory name="PrefixSumRec" sum="dc9d2193d04034059a14474fc3bb5c44" expanded="true">
  <goal name="Div_mod_2" expl="">
  <proof prover="0"><result status="valid" time="0.02"/></proof>
  <proof prover="1"><result status="valid" time="0.03"/></proof>
@@ -348,7 +348,7 @@
   <proof prover="3" timelimit="30"><result status="valid" time="1.28"/></proof>
   </goal>
   <goal name="WP_parameter downsweep.18" expl="assertion">
-  <proof prover="0" timelimit="30"><result status="valid" time="7.83"/></proof>
+  <proof prover="0" timelimit="30"><result status="valid" time="4.92"/></proof>
   <proof prover="1" timelimit="30"><result status="valid" time="3.47"/></proof>
   </goal>
   <goal name="WP_parameter downsweep.19" expl="variant decrease">
@@ -459,7 +459,7 @@
   <goal name="WP_parameter compute_sums.4" expl="assertion">
   <proof prover="0"><result status="valid" time="0.28"/></proof>
   <proof prover="1"><result status="valid" time="0.38"/></proof>
-  <proof prover="6"><result status="valid" time="0.61" steps="141"/></proof>
+  <proof prover="6"><result status="valid" time="0.61" steps="129"/></proof>
   </goal>
   <goal name="WP_parameter compute_sums.5" expl="index in array bounds">
   <proof prover="0"><result status="valid" time="0.03"/></proof>
diff --git a/examples/verifythis_PrefixSumRec/why3shapes.gz b/examples/verifythis_PrefixSumRec/why3shapes.gz
index 444760772c170695a3413a931430609e96cb53ca..5273a06f9d00f91b89f686c862bba6c47fdff7f6 100644
Binary files a/examples/verifythis_PrefixSumRec/why3shapes.gz and b/examples/verifythis_PrefixSumRec/why3shapes.gz differ