diff --git a/examples/binary_search/why3session.xml b/examples/binary_search/why3session.xml
index 96b9d69d48f69aa222270a85a96b4c85c0767b33..5a992e911d9759933dc9d4aff0e71f9a196afeef 100644
--- a/examples/binary_search/why3session.xml
+++ b/examples/binary_search/why3session.xml
@@ -22,87 +22,87 @@
  <proof prover="4"><result status="valid" time="0.03"/></proof>
  </goal>
 </theory>
-<theory name="BinarySearchInt32" sum="3bccc1a191f702802bbee521528e559c" expanded="true">
+<theory name="BinarySearchInt32" sum="2089995b9d71a591dc8d378af11dce53" expanded="true">
  <goal name="WP_parameter binary_search" expl="VC for binary_search" expanded="true">
  <transf name="split_goal_wp" expanded="true">
   <goal name="WP_parameter binary_search.1" expl="1. integer overflow">
-  <proof prover="3"><result status="valid" time="0.02" steps="5"/></proof>
+  <proof prover="3"><result status="valid" time="0.02" steps="70"/></proof>
   </goal>
   <goal name="WP_parameter binary_search.2" expl="2. integer overflow">
-  <proof prover="3"><result status="valid" time="0.01" steps="7"/></proof>
+  <proof prover="3"><result status="valid" time="0.01" steps="72"/></proof>
   </goal>
   <goal name="WP_parameter binary_search.3" expl="3. integer overflow">
-  <proof prover="3"><result status="valid" time="0.01" steps="25"/></proof>
+  <proof prover="3"><result status="valid" time="0.12" steps="88"/></proof>
   </goal>
   <goal name="WP_parameter binary_search.4" expl="4. loop invariant init">
-  <proof prover="3"><result status="valid" time="0.01" steps="10"/></proof>
+  <proof prover="3"><result status="valid" time="0.01" steps="75"/></proof>
   </goal>
   <goal name="WP_parameter binary_search.5" expl="5. loop invariant init">
-  <proof prover="3"><result status="valid" time="0.01" steps="13"/></proof>
+  <proof prover="3"><result status="valid" time="0.01" steps="78"/></proof>
   </goal>
   <goal name="WP_parameter binary_search.6" expl="6. integer overflow">
-  <proof prover="3"><result status="valid" time="0.02" steps="15"/></proof>
+  <proof prover="3"><result status="valid" time="0.02" steps="80"/></proof>
   </goal>
   <goal name="WP_parameter binary_search.7" expl="7. integer overflow">
-  <proof prover="3"><result status="valid" time="0.02" steps="21"/></proof>
+  <proof prover="3"><result status="valid" time="0.02" steps="86"/></proof>
   </goal>
   <goal name="WP_parameter binary_search.8" expl="8. division by zero">
-  <proof prover="3"><result status="valid" time="0.01" steps="18"/></proof>
+  <proof prover="3"><result status="valid" time="0.01" steps="83"/></proof>
   </goal>
   <goal name="WP_parameter binary_search.9" expl="9. integer overflow">
-  <proof prover="3"><result status="valid" time="0.04" steps="34"/></proof>
+  <proof prover="3"><result status="valid" time="0.04" steps="99"/></proof>
   </goal>
   <goal name="WP_parameter binary_search.10" expl="10. integer overflow">
-  <proof prover="3"><result status="valid" time="0.52" steps="51"/></proof>
+  <proof prover="3"><result status="valid" time="0.52" steps="114"/></proof>
   </goal>
   <goal name="WP_parameter binary_search.11" expl="11. assertion">
-  <proof prover="3"><result status="valid" time="0.91" steps="72"/></proof>
+  <proof prover="3"><result status="valid" time="1.48" steps="133"/></proof>
   </goal>
   <goal name="WP_parameter binary_search.12" expl="12. index in array bounds">
-  <proof prover="3"><result status="valid" time="0.01" steps="25"/></proof>
+  <proof prover="3"><result status="valid" time="0.01" steps="90"/></proof>
   </goal>
   <goal name="WP_parameter binary_search.13" expl="13. integer overflow">
-  <proof prover="3"><result status="valid" time="0.01" steps="29"/></proof>
+  <proof prover="3"><result status="valid" time="0.01" steps="94"/></proof>
   </goal>
   <goal name="WP_parameter binary_search.14" expl="14. integer overflow">
-  <proof prover="3"><result status="valid" time="0.03" steps="46"/></proof>
+  <proof prover="3"><result status="valid" time="0.03" steps="111"/></proof>
   </goal>
   <goal name="WP_parameter binary_search.15" expl="15. loop invariant preservation">
-  <proof prover="3"><result status="valid" time="0.02" steps="33"/></proof>
+  <proof prover="3"><result status="valid" time="0.02" steps="98"/></proof>
   </goal>
   <goal name="WP_parameter binary_search.16" expl="16. loop invariant preservation">
   <proof prover="0"><result status="valid" time="0.04"/></proof>
   <proof prover="2"><result status="valid" time="0.02"/></proof>
-  <proof prover="3"><result status="valid" time="6.24" steps="115"/></proof>
+  <proof prover="3"><result status="valid" time="8.76" steps="176"/></proof>
   </goal>
   <goal name="WP_parameter binary_search.17" expl="17. loop variant decrease">
-  <proof prover="3"><result status="valid" time="0.02" steps="33"/></proof>
+  <proof prover="3"><result status="valid" time="0.02" steps="98"/></proof>
   </goal>
   <goal name="WP_parameter binary_search.18" expl="18. index in array bounds">
-  <proof prover="3"><result status="valid" time="0.01" steps="29"/></proof>
+  <proof prover="3"><result status="valid" time="0.01" steps="94"/></proof>
   </goal>
   <goal name="WP_parameter binary_search.19" expl="19. integer overflow">
-  <proof prover="3"><result status="valid" time="0.01" steps="31"/></proof>
+  <proof prover="3"><result status="valid" time="0.01" steps="96"/></proof>
   </goal>
   <goal name="WP_parameter binary_search.20" expl="20. integer overflow">
-  <proof prover="3"><result status="valid" time="0.02" steps="35"/></proof>
+  <proof prover="3"><result status="valid" time="0.02" steps="100"/></proof>
   </goal>
   <goal name="WP_parameter binary_search.21" expl="21. loop invariant preservation">
-  <proof prover="3"><result status="valid" time="0.02" steps="35"/></proof>
+  <proof prover="3"><result status="valid" time="0.02" steps="100"/></proof>
   </goal>
   <goal name="WP_parameter binary_search.22" expl="22. loop invariant preservation">
   <proof prover="0"><result status="valid" time="0.04"/></proof>
   <proof prover="2"><result status="valid" time="0.02"/></proof>
-  <proof prover="3" timelimit="60"><result status="valid" time="9.69" steps="116"/></proof>
+  <proof prover="3" timelimit="60"><result status="valid" time="14.15" steps="177"/></proof>
   </goal>
   <goal name="WP_parameter binary_search.23" expl="23. loop variant decrease">
-  <proof prover="3"><result status="valid" time="0.02" steps="35"/></proof>
+  <proof prover="3"><result status="valid" time="0.02" steps="100"/></proof>
   </goal>
   <goal name="WP_parameter binary_search.24" expl="24. postcondition">
-  <proof prover="3"><result status="valid" time="1.22" steps="63"/></proof>
+  <proof prover="3"><result status="valid" time="2.32" steps="126"/></proof>
   </goal>
   <goal name="WP_parameter binary_search.25" expl="25. exceptional postcondition">
-  <proof prover="3"><result status="valid" time="0.01" steps="24"/></proof>
+  <proof prover="3"><result status="valid" time="0.01" steps="89"/></proof>
   </goal>
  </transf>
  </goal>
diff --git a/examples/binary_search/why3shapes.gz b/examples/binary_search/why3shapes.gz
index 1d494a305fc2b124cfeff8a08fc06cc4f72e412b..a45ce81e3e606d8b0fa19d6b434612da9a4cf2a8 100644
Binary files a/examples/binary_search/why3shapes.gz and b/examples/binary_search/why3shapes.gz differ
diff --git a/examples/bitvector_examples/why3session.xml b/examples/bitvector_examples/why3session.xml
index 0fe95426252f96762a96dc160d4e3f67fc85d453..3fcfc3ac33161c95d2390dbdc3d25bb490ac578f 100644
--- a/examples/bitvector_examples/why3session.xml
+++ b/examples/bitvector_examples/why3session.xml
@@ -7,7 +7,7 @@
 <prover id="2" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
 <prover id="3" name="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
 <file name="../bitvector_examples.mlw" expanded="true">
-<theory name="Test_proofinuse" sum="809c0c60af055a2ddd0161813cbbe3c7" expanded="true">
+<theory name="Test_proofinuse" sum="ee2b0706c948b7fbb0dceccdae7fcbb8" expanded="true">
  <goal name="WP_parameter shift_is_div" expl="VC for shift_is_div" expanded="true">
  <transf name="split_goal_wp" expanded="true">
   <goal name="WP_parameter shift_is_div.1" expl="1. assertion">
@@ -19,7 +19,7 @@
   <proof prover="1"><result status="valid" time="0.18"/></proof>
   </goal>
   <goal name="WP_parameter shift_is_div.3" expl="3. assertion">
-  <proof prover="1"><result status="valid" time="2.10"/></proof>
+  <proof prover="1"><result status="valid" time="1.39"/></proof>
   <proof prover="2"><result status="valid" time="0.01"/></proof>
   <proof prover="3"><result status="valid" time="0.00"/></proof>
   </goal>
@@ -37,11 +37,11 @@
  <proof prover="2"><result status="valid" time="0.04"/></proof>
  </goal>
  <goal name="ttt">
- <proof prover="0"><result status="valid" time="1.18" steps="655"/></proof>
+ <proof prover="0"><result status="valid" time="0.71" steps="655"/></proof>
  <proof prover="2"><result status="valid" time="0.08"/></proof>
  </goal>
 </theory>
-<theory name="Hackers_delight" sum="09bf674159d27624afdfd7d2cba2c409">
+<theory name="Hackers_delight" sum="f6b9335c83a49e64cc1c287e49abcc67">
  <goal name="DM1">
  <proof prover="2"><result status="valid" time="0.04"/></proof>
  <proof prover="3"><result status="valid" time="0.00"/></proof>
@@ -104,7 +104,7 @@
  <proof prover="2"><result status="valid" time="0.04"/></proof>
  </goal>
 </theory>
-<theory name="Hackers_delight_mod" sum="27a2b34ec9e81b08a0a2230fa3edb0ac" expanded="true">
+<theory name="Hackers_delight_mod" sum="358ae27e3c7dd0ffc3bad38307e7ee71" expanded="true">
  <goal name="WP_parameter dm1" expl="VC for dm1">
  <proof prover="2"><result status="valid" time="0.04"/></proof>
  <proof prover="3"><result status="valid" time="0.01"/></proof>
@@ -173,7 +173,7 @@
  <proof prover="2"><result status="valid" time="0.07"/></proof>
  </goal>
 </theory>
-<theory name="Test_imperial_violet" sum="dc79d81e99715d5b91e15217b2914718" expanded="true">
+<theory name="Test_imperial_violet" sum="9d49ecf681253b01c1150fab4a271ed5" expanded="true">
  <goal name="bv32_bounds_bv">
  <proof prover="0"><result status="valid" time="0.13" steps="141"/></proof>
  <proof prover="1"><result status="valid" time="0.25"/></proof>
@@ -197,10 +197,10 @@
  <proof prover="1"><result status="valid" time="0.12"/></proof>
  </goal>
  <goal name="WP_parameter add" expl="VC for add">
- <proof prover="1"><result status="valid" time="5.19"/></proof>
+ <proof prover="1"><result status="valid" time="3.15"/></proof>
  </goal>
 </theory>
-<theory name="Test_from_bitvector_example" sum="8658e639f605682142cf03f4b58cbf30" expanded="true">
+<theory name="Test_from_bitvector_example" sum="2ebd89b51a2ede04c66611b03895c2c2" expanded="true">
  <goal name="Test1">
  <proof prover="0"><result status="valid" time="0.14" steps="93"/></proof>
  <proof prover="1"><result status="valid" time="0.22"/></proof>
@@ -215,7 +215,7 @@
  </goal>
  <goal name="Test3">
  <proof prover="0"><result status="valid" time="0.06" steps="83"/></proof>
- <proof prover="1"><result status="valid" time="0.39"/></proof>
+ <proof prover="1"><result status="valid" time="0.19"/></proof>
  <proof prover="2"><result status="valid" time="0.03"/></proof>
  <proof prover="3"><result status="valid" time="0.00"/></proof>
  </goal>
@@ -227,7 +227,7 @@
  </goal>
  <goal name="Test5">
  <proof prover="0"><result status="valid" time="0.06" steps="89"/></proof>
- <proof prover="1"><result status="valid" time="0.46"/></proof>
+ <proof prover="1"><result status="valid" time="0.24"/></proof>
  <proof prover="2"><result status="valid" time="0.04"/></proof>
  <proof prover="3"><result status="valid" time="0.00"/></proof>
  </goal>
@@ -238,24 +238,24 @@
  <proof prover="3"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="WP_parameter lsr31" expl="VC for lsr31">
- <proof prover="1"><result status="valid" time="0.50"/></proof>
+ <proof prover="1"><result status="valid" time="0.24"/></proof>
  <proof prover="2"><result status="valid" time="0.04"/></proof>
  <proof prover="3"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="WP_parameter lsr30" expl="VC for lsr30">
- <proof prover="1"><result status="valid" time="2.47"/></proof>
+ <proof prover="1"><result status="valid" time="1.38"/></proof>
  <proof prover="2"><result status="valid" time="0.04"/></proof>
  <proof prover="3"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="WP_parameter lsr29" expl="VC for lsr29">
  <proof prover="0"><result status="valid" time="0.24" steps="192"/></proof>
- <proof prover="1"><result status="valid" time="1.72"/></proof>
+ <proof prover="1"><result status="valid" time="0.74"/></proof>
  <proof prover="2"><result status="valid" time="0.04"/></proof>
  <proof prover="3"><result status="valid" time="0.01"/></proof>
  </goal>
  <goal name="WP_parameter lsr28" expl="VC for lsr28">
  <proof prover="0"><result status="valid" time="0.24" steps="196"/></proof>
- <proof prover="1"><result status="valid" time="1.37"/></proof>
+ <proof prover="1"><result status="valid" time="0.76"/></proof>
  <proof prover="2"><result status="valid" time="0.04"/></proof>
  <proof prover="3"><result status="valid" time="0.00"/></proof>
  </goal>
@@ -267,151 +267,151 @@
  </goal>
  <goal name="WP_parameter lsr26" expl="VC for lsr26">
  <proof prover="0"><result status="valid" time="0.16" steps="196"/></proof>
- <proof prover="1"><result status="valid" time="1.26"/></proof>
+ <proof prover="1"><result status="valid" time="0.71"/></proof>
  <proof prover="2"><result status="valid" time="0.03"/></proof>
  <proof prover="3"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="WP_parameter lsr20" expl="VC for lsr20">
  <proof prover="0"><result status="valid" time="0.24" steps="196"/></proof>
- <proof prover="1"><result status="valid" time="1.08"/></proof>
+ <proof prover="1"><result status="valid" time="0.72"/></proof>
  <proof prover="2"><result status="valid" time="0.04"/></proof>
  <proof prover="3"><result status="valid" time="0.01"/></proof>
  </goal>
  <goal name="WP_parameter lsr13" expl="VC for lsr13">
  <proof prover="0"><result status="valid" time="0.24" steps="196"/></proof>
- <proof prover="1"><result status="valid" time="1.35"/></proof>
+ <proof prover="1"><result status="valid" time="0.72"/></proof>
  <proof prover="2"><result status="valid" time="0.04"/></proof>
  <proof prover="3"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="WP_parameter lsr8" expl="VC for lsr8">
  <proof prover="0"><result status="valid" time="0.25" steps="196"/></proof>
- <proof prover="1"><result status="valid" time="1.17"/></proof>
+ <proof prover="1"><result status="valid" time="0.72"/></proof>
  <proof prover="2"><result status="valid" time="0.04"/></proof>
  <proof prover="3"><result status="valid" time="0.01"/></proof>
  </goal>
  <goal name="to_int_0x00000001">
- <proof prover="0"><result status="valid" time="0.48" steps="227"/></proof>
- <proof prover="1"><result status="valid" time="0.42"/></proof>
+ <proof prover="0"><result status="valid" time="0.20" steps="227"/></proof>
+ <proof prover="1"><result status="valid" time="0.20"/></proof>
  <proof prover="2"><result status="valid" time="0.03"/></proof>
  <proof prover="3"><result status="valid" time="0.01"/></proof>
  </goal>
  <goal name="to_int_0x00000003">
  <proof prover="0"><result status="valid" time="0.14" steps="196"/></proof>
- <proof prover="1"><result status="valid" time="0.73"/></proof>
+ <proof prover="1"><result status="valid" time="0.54"/></proof>
  <proof prover="2"><result status="valid" time="0.04"/></proof>
  <proof prover="3"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="to_int_0x00000007">
  <proof prover="0"><result status="valid" time="0.14" steps="192"/></proof>
- <proof prover="1"><result status="valid" time="1.56"/></proof>
+ <proof prover="1"><result status="valid" time="0.74"/></proof>
  <proof prover="2"><result status="valid" time="0.04"/></proof>
  <proof prover="3"><result status="valid" time="0.01"/></proof>
  </goal>
  <goal name="to_int_0x0000000F">
  <proof prover="0"><result status="valid" time="0.14" steps="196"/></proof>
- <proof prover="1"><result status="valid" time="1.51"/></proof>
+ <proof prover="1"><result status="valid" time="0.75"/></proof>
  <proof prover="2"><result status="valid" time="0.03"/></proof>
  <proof prover="3"><result status="valid" time="0.01"/></proof>
  </goal>
  <goal name="to_int_0x0000001F">
  <proof prover="0"><result status="valid" time="0.20" steps="196"/></proof>
- <proof prover="1"><result status="valid" time="1.30"/></proof>
+ <proof prover="1"><result status="valid" time="0.71"/></proof>
  <proof prover="2"><result status="valid" time="0.03"/></proof>
  <proof prover="3"><result status="valid" time="0.01"/></proof>
  </goal>
  <goal name="to_int_0x0000003F">
- <proof prover="0"><result status="valid" time="0.32" steps="196"/></proof>
- <proof prover="1"><result status="valid" time="1.29"/></proof>
+ <proof prover="0"><result status="valid" time="0.14" steps="196"/></proof>
+ <proof prover="1"><result status="valid" time="0.71"/></proof>
  <proof prover="2"><result status="valid" time="0.03"/></proof>
  <proof prover="3"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="to_int_0x0000007F">
  <proof prover="0"><result status="valid" time="0.21" steps="196"/></proof>
- <proof prover="1"><result status="valid" time="1.22"/></proof>
+ <proof prover="1"><result status="valid" time="0.73"/></proof>
  <proof prover="2"><result status="valid" time="0.04"/></proof>
  <proof prover="3"><result status="valid" time="0.01"/></proof>
  </goal>
  <goal name="to_int_0x000000FF">
  <proof prover="0"><result status="valid" time="0.22" steps="192"/></proof>
- <proof prover="1"><result status="valid" time="1.26"/></proof>
+ <proof prover="1"><result status="valid" time="0.73"/></proof>
  <proof prover="2"><result status="valid" time="0.03"/></proof>
  <proof prover="3"><result status="valid" time="0.01"/></proof>
  </goal>
  <goal name="to_int_0x000001FF">
- <proof prover="0"><result status="valid" time="0.27" steps="196"/></proof>
- <proof prover="1"><result status="valid" time="1.74"/></proof>
+ <proof prover="0"><result status="valid" time="0.14" steps="196"/></proof>
+ <proof prover="1"><result status="valid" time="0.73"/></proof>
  <proof prover="2"><result status="valid" time="0.04"/></proof>
  <proof prover="3"><result status="valid" time="0.01"/></proof>
  </goal>
  <goal name="to_int_0x000003FF">
- <proof prover="0"><result status="valid" time="0.28" steps="196"/></proof>
- <proof prover="1"><result status="valid" time="1.70"/></proof>
+ <proof prover="0"><result status="valid" time="0.14" steps="196"/></proof>
+ <proof prover="1"><result status="valid" time="0.73"/></proof>
  <proof prover="2"><result status="valid" time="0.04"/></proof>
  <proof prover="3"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="to_int_0x000007FF">
- <proof prover="0"><result status="valid" time="0.29" steps="196"/></proof>
- <proof prover="1"><result status="valid" time="1.26"/></proof>
+ <proof prover="0"><result status="valid" time="0.14" steps="196"/></proof>
+ <proof prover="1"><result status="valid" time="0.74"/></proof>
  <proof prover="2"><result status="valid" time="0.04"/></proof>
  <proof prover="3"><result status="valid" time="0.01"/></proof>
  </goal>
  <goal name="to_int_0x00000FFF">
  <proof prover="0"><result status="valid" time="0.24" steps="196"/></proof>
- <proof prover="1"><result status="valid" time="1.45"/></proof>
+ <proof prover="1"><result status="valid" time="0.72"/></proof>
  <proof prover="2"><result status="valid" time="0.04"/></proof>
  <proof prover="3"><result status="valid" time="0.01"/></proof>
  </goal>
  <goal name="to_int_0x00001FFF">
- <proof prover="0"><result status="valid" time="0.32" steps="196"/></proof>
- <proof prover="1"><result status="valid" time="1.26"/></proof>
+ <proof prover="0"><result status="valid" time="0.14" steps="196"/></proof>
+ <proof prover="1"><result status="valid" time="0.71"/></proof>
  <proof prover="2"><result status="valid" time="0.02"/></proof>
  <proof prover="3"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="to_int_0x00003FFF">
  <proof prover="0"><result status="valid" time="0.21" steps="196"/></proof>
- <proof prover="1"><result status="valid" time="1.51"/></proof>
+ <proof prover="1"><result status="valid" time="0.73"/></proof>
  <proof prover="2"><result status="valid" time="0.02"/></proof>
  <proof prover="3"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="to_int_0x00007FFF">
  <proof prover="0"><result status="valid" time="0.18" steps="196"/></proof>
- <proof prover="1"><result status="valid" time="1.74"/></proof>
+ <proof prover="1"><result status="valid" time="0.72"/></proof>
  <proof prover="2"><result status="valid" time="0.02"/></proof>
  <proof prover="3"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="to_int_0x0000FFFF">
  <proof prover="0"><result status="valid" time="0.19" steps="196"/></proof>
- <proof prover="1"><result status="valid" time="1.76"/></proof>
+ <proof prover="1"><result status="valid" time="0.72"/></proof>
  <proof prover="2"><result status="valid" time="0.02"/></proof>
  <proof prover="3"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="to_int_0x0001FFFF">
- <proof prover="0"><result status="valid" time="0.34" steps="196"/></proof>
- <proof prover="1"><result status="valid" time="1.29"/></proof>
+ <proof prover="0"><result status="valid" time="0.14" steps="196"/></proof>
+ <proof prover="1"><result status="valid" time="0.72"/></proof>
  <proof prover="2"><result status="valid" time="0.02"/></proof>
  <proof prover="3"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="to_int_0x0003FFFF">
- <proof prover="0"><result status="valid" time="0.30" steps="196"/></proof>
- <proof prover="1"><result status="valid" time="1.79"/></proof>
+ <proof prover="0"><result status="valid" time="0.13" steps="196"/></proof>
+ <proof prover="1"><result status="valid" time="0.73"/></proof>
  <proof prover="2"><result status="valid" time="0.02"/></proof>
  <proof prover="3"><result status="valid" time="0.01"/></proof>
  </goal>
  <goal name="to_int_0x0007FFFF">
  <proof prover="0"><result status="valid" time="0.18" steps="196"/></proof>
- <proof prover="1"><result status="valid" time="1.39"/></proof>
+ <proof prover="1"><result status="valid" time="0.72"/></proof>
  <proof prover="2"><result status="valid" time="0.02"/></proof>
  <proof prover="3"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="to_int_0x000FFFFF">
- <proof prover="0"><result status="valid" time="0.34" steps="196"/></proof>
- <proof prover="1"><result status="valid" time="1.38"/></proof>
+ <proof prover="0"><result status="valid" time="0.14" steps="196"/></proof>
+ <proof prover="1"><result status="valid" time="0.73"/></proof>
  <proof prover="2"><result status="valid" time="0.02"/></proof>
  <proof prover="3"><result status="valid" time="0.01"/></proof>
  </goal>
  <goal name="to_int_0x00FFFFFF">
- <proof prover="0"><result status="valid" time="0.27" steps="196"/></proof>
- <proof prover="1"><result status="valid" time="1.04"/></proof>
+ <proof prover="0"><result status="valid" time="0.14" steps="196"/></proof>
+ <proof prover="1"><result status="valid" time="0.72"/></proof>
  <proof prover="2"><result status="valid" time="0.02"/></proof>
  <proof prover="3"><result status="valid" time="0.00"/></proof>
  </goal>
diff --git a/examples/bitvector_examples/why3shapes.gz b/examples/bitvector_examples/why3shapes.gz
index 8c135ce6d8def21dc6d7f6cca9841e92a035d3d0..cb090348331f028f39c85d33c2c1de84d442e305 100644
Binary files a/examples/bitvector_examples/why3shapes.gz and b/examples/bitvector_examples/why3shapes.gz differ
diff --git a/examples/check-builtin/real/why3session.xml b/examples/check-builtin/real/why3session.xml
index 2dd4564ecbb5afc5a43427db78da4c916f5fb253..d37ba8867c21b531dbf64744075a57f86e478372 100644
--- a/examples/check-builtin/real/why3session.xml
+++ b/examples/check-builtin/real/why3session.xml
@@ -17,7 +17,7 @@
 <file name="../real.why" expanded="true">
 <theory name="Test" sum="cf206e9b789e3b16bbeee98ff5359bb7" expanded="true">
  <goal name="G1" expanded="true">
- <proof prover="1" memlimit="0"><result status="valid" time="0.01"/></proof>
+ <proof prover="1" memlimit="0"><result status="valid" time="0.01" steps="0"/></proof>
  <proof prover="2"><result status="valid" time="0.00"/></proof>
  <proof prover="4" memlimit="0"><result status="valid" time="0.00"/></proof>
  <proof prover="6"><result status="valid" time="0.00"/></proof>
@@ -26,7 +26,7 @@
  <proof prover="9"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="G2" expanded="true">
- <proof prover="1" memlimit="0"><result status="valid" time="0.01"/></proof>
+ <proof prover="1" memlimit="0"><result status="valid" time="0.01" steps="0"/></proof>
  <proof prover="2"><result status="valid" time="0.00"/></proof>
  <proof prover="4" memlimit="0"><result status="valid" time="0.00"/></proof>
  <proof prover="6"><result status="valid" time="0.00"/></proof>
@@ -34,7 +34,7 @@
  <proof prover="9"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="G3" expanded="true">
- <proof prover="1" memlimit="0"><result status="valid" time="0.00"/></proof>
+ <proof prover="1" memlimit="0"><result status="valid" time="0.00" steps="0"/></proof>
  <proof prover="2"><result status="valid" time="0.00"/></proof>
  <proof prover="4" memlimit="0"><result status="valid" time="0.00"/></proof>
  <proof prover="6"><result status="valid" time="0.00"/></proof>
@@ -43,7 +43,7 @@
 </theory>
 <theory name="TestInfix" sum="9929e0fb7685505424762277d915662a" expanded="true">
  <goal name="Add" expanded="true">
- <proof prover="1" memlimit="0"><result status="valid" time="0.00"/></proof>
+ <proof prover="1" memlimit="0"><result status="valid" time="0.00" steps="0"/></proof>
  <proof prover="2"><result status="valid" time="0.00"/></proof>
  <proof prover="4" memlimit="0"><result status="valid" time="0.00"/></proof>
  <proof prover="6"><result status="valid" time="0.00"/></proof>
@@ -51,7 +51,7 @@
  <proof prover="9"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="Sub" expanded="true">
- <proof prover="1" memlimit="0"><result status="valid" time="0.00"/></proof>
+ <proof prover="1" memlimit="0"><result status="valid" time="0.00" steps="0"/></proof>
  <proof prover="2"><result status="valid" time="0.00"/></proof>
  <proof prover="4" memlimit="0"><result status="valid" time="0.00"/></proof>
  <proof prover="6"><result status="valid" time="0.00"/></proof>
@@ -59,7 +59,7 @@
  <proof prover="9"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="Neg" expanded="true">
- <proof prover="1" memlimit="0"><result status="valid" time="0.01"/></proof>
+ <proof prover="1" memlimit="0"><result status="valid" time="0.01" steps="0"/></proof>
  <proof prover="2"><result status="valid" time="0.00"/></proof>
  <proof prover="4" memlimit="0"><result status="valid" time="0.00"/></proof>
  <proof prover="6"><result status="valid" time="0.00"/></proof>
@@ -67,7 +67,7 @@
  <proof prover="9"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="Mul" expanded="true">
- <proof prover="1" memlimit="0"><result status="valid" time="0.01"/></proof>
+ <proof prover="1" memlimit="0"><result status="valid" time="0.01" steps="0"/></proof>
  <proof prover="2"><result status="valid" time="0.00"/></proof>
  <proof prover="4" memlimit="0"><result status="valid" time="0.00"/></proof>
  <proof prover="6"><result status="valid" time="0.00"/></proof>
@@ -75,7 +75,7 @@
  <proof prover="9"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="Div" expanded="true">
- <proof prover="1" memlimit="0"><result status="valid" time="0.00"/></proof>
+ <proof prover="1" memlimit="0"><result status="valid" time="0.00" steps="0"/></proof>
  <proof prover="2"><result status="valid" time="0.00"/></proof>
  <proof prover="4" memlimit="0"><result status="valid" time="0.00"/></proof>
  <proof prover="6"><result status="valid" time="0.00"/></proof>
@@ -83,7 +83,7 @@
  <proof prover="9"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="Inv" expanded="true">
- <proof prover="1" memlimit="0"><result status="valid" time="0.01"/></proof>
+ <proof prover="1" memlimit="0"><result status="valid" time="0.01" steps="0"/></proof>
  <proof prover="2"><result status="valid" time="0.00"/></proof>
  <proof prover="4" memlimit="0"><result status="valid" time="0.00"/></proof>
  <proof prover="6"><result status="valid" time="0.00"/></proof>
@@ -92,7 +92,7 @@
 </theory>
 <theory name="SquareTest" sum="b399f090ec659c1b880d355f5452fbc9" expanded="true">
  <goal name="Sqrt_zero" expanded="true">
- <proof prover="1" memlimit="0"><result status="valid" time="0.01"/></proof>
+ <proof prover="1" memlimit="0"><result status="valid" time="0.01" steps="3"/></proof>
  <proof prover="2"><result status="valid" time="0.01"/></proof>
  <proof prover="4" timelimit="60"><result status="valid" time="0.02"/></proof>
  <proof prover="6"><result status="valid" time="0.00"/></proof>
@@ -100,7 +100,7 @@
  <proof prover="9"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="Sqrt_one" expanded="true">
- <proof prover="1" memlimit="0"><result status="valid" time="0.01"/></proof>
+ <proof prover="1" memlimit="0"><result status="valid" time="0.01" steps="4"/></proof>
  <proof prover="2"><result status="valid" time="0.00"/></proof>
  <proof prover="4" memlimit="0"><result status="valid" time="0.01"/></proof>
  <proof prover="6"><result status="valid" time="0.00"/></proof>
@@ -108,17 +108,17 @@
  <proof prover="9"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="Sqrt_four" expanded="true">
- <proof prover="1" timelimit="5"><result status="valid" time="0.00"/></proof>
+ <proof prover="1" timelimit="5"><result status="valid" time="0.00" steps="8"/></proof>
  <proof prover="2"><result status="valid" time="0.00"/></proof>
  <proof prover="4" memlimit="0"><result status="valid" time="1.27"/></proof>
  <proof prover="6"><result status="valid" time="0.00"/></proof>
- <proof prover="8" timelimit="67"><result status="valid" time="32.60"/></proof>
+ <proof prover="8" timelimit="67"><result status="valid" time="26.09"/></proof>
  <proof prover="9"><result status="valid" time="0.00"/></proof>
  </goal>
 </theory>
 <theory name="ExpLogTest" sum="b87cf6a8ae7e92621e77bacb7a1fd605" expanded="true">
  <goal name="Log_e" expanded="true">
- <proof prover="1" memlimit="0"><result status="valid" time="0.01"/></proof>
+ <proof prover="1" memlimit="0"><result status="valid" time="0.01" steps="3"/></proof>
  <proof prover="2"><result status="valid" time="0.00"/></proof>
  <proof prover="4" memlimit="0"><result status="valid" time="0.01"/></proof>
  <proof prover="6"><result status="valid" time="0.00"/></proof>
@@ -127,7 +127,7 @@
 </theory>
 <theory name="PowerIntTest" sum="a44ed7f266568491fd1a5efcfad78047" expanded="true">
  <goal name="Pow_2_2" expanded="true">
- <proof prover="1" timelimit="60"><result status="valid" time="0.02"/></proof>
+ <proof prover="1" timelimit="60"><result status="valid" time="0.02" steps="6"/></proof>
  <proof prover="2"><result status="valid" time="0.00"/></proof>
  <proof prover="4" memlimit="0"><result status="valid" time="0.01"/></proof>
  <proof prover="6"><result status="valid" time="0.00"/></proof>
@@ -135,23 +135,23 @@
  <proof prover="9"><result status="unknown" time="0.00"/></proof>
  </goal>
 </theory>
-<theory name="PowerRealTest" sum="747061f2b592f0feb89bb09cb7faca73" expanded="true">
+<theory name="PowerRealTest" sum="eb0bbfff015add810d5cc4a17172919b" expanded="true">
  <goal name="Pow_2_2" expanded="true">
- <proof prover="1" memlimit="0"><result status="valid" time="0.01"/></proof>
+ <proof prover="1" memlimit="0"><result status="valid" time="0.01" steps="6"/></proof>
  <proof prover="4" memlimit="0"><result status="valid" time="0.01"/></proof>
  <proof prover="8" memlimit="0"><result status="valid" time="0.01"/></proof>
  </goal>
 </theory>
 <theory name="TrigonometryTest" sum="dd9fe92c2a107d45cbcce7b6e297404f" expanded="true">
  <goal name="Cos_2_pi" expanded="true">
- <proof prover="1" memlimit="0"><result status="valid" time="0.12"/></proof>
+ <proof prover="1" memlimit="0"><result status="valid" time="0.12" steps="42"/></proof>
  <proof prover="2"><result status="valid" time="0.00"/></proof>
  <proof prover="4" memlimit="0"><result status="valid" time="0.11"/></proof>
  <proof prover="6"><result status="valid" time="0.00"/></proof>
  <proof prover="8" memlimit="0"><result status="valid" time="0.09"/></proof>
  </goal>
  <goal name="Sin_2_pi" expanded="true">
- <proof prover="1" timelimit="60"><result status="valid" time="0.60"/></proof>
+ <proof prover="1" timelimit="60"><result status="valid" time="0.60" steps="181"/></proof>
  <proof prover="2"><result status="valid" time="0.01"/></proof>
  <proof prover="4" memlimit="0"><result status="valid" time="0.04"/></proof>
  <proof prover="6"><result status="valid" time="0.01"/></proof>
@@ -161,7 +161,7 @@
  <proof prover="0" edited="real_TrigonometryTest_Tan_pi_4_1.v"><result status="valid" time="1.47"/></proof>
  <proof prover="3"><result status="unknown" time="0.26"/></proof>
  <proof prover="5"><result status="timeout" time="4.99"/></proof>
- <proof prover="10"><result status="timeout" time="4.98"/></proof>
+ <proof prover="10"><result status="timeout" time="5.99"/></proof>
  <proof prover="11"><result status="timeout" time="5.00"/></proof>
  </goal>
  <goal name="Tan_pi_3" expanded="true">
diff --git a/examples/check-builtin/real/why3shapes.gz b/examples/check-builtin/real/why3shapes.gz
index 1bad16cbeeb5cfb3886c5849b151f1e88f1f6162..42e2a562f5763e918f95461b8d0d9867e42e682f 100644
Binary files a/examples/check-builtin/real/why3shapes.gz and b/examples/check-builtin/real/why3shapes.gz differ
diff --git a/examples/gcd/why3session.xml b/examples/gcd/why3session.xml
index 29d44cd099686c00c199e5f39457a6546bb457f9..ece9c236245a1a08494f14b77ce49f3ab01864c1 100644
--- a/examples/gcd/why3session.xml
+++ b/examples/gcd/why3session.xml
@@ -171,29 +171,29 @@
  </transf>
  </goal>
 </theory>
-<theory name="EuclideanAlgorithm31" sum="82e091181a4d11848b760d8549c12df1" expanded="true">
+<theory name="EuclideanAlgorithm31" sum="91fea75d1ece6ac0571a9d40b9bdc3dc" expanded="true">
  <goal name="WP_parameter euclid" expl="VC for euclid">
  <transf name="split_goal_wp">
   <goal name="WP_parameter euclid.1" expl="1. integer overflow">
-  <proof prover="5" timelimit="5"><result status="valid" time="0.01" steps="6"/></proof>
+  <proof prover="5" timelimit="5"><result status="valid" time="0.01" steps="3"/></proof>
   </goal>
   <goal name="WP_parameter euclid.2" expl="2. postcondition">
-  <proof prover="5" timelimit="5"><result status="valid" time="0.02" steps="16"/></proof>
+  <proof prover="5" timelimit="5"><result status="valid" time="0.02" steps="13"/></proof>
   </goal>
   <goal name="WP_parameter euclid.3" expl="3. division by zero">
-  <proof prover="5" timelimit="5"><result status="valid" time="0.02" steps="9"/></proof>
+  <proof prover="5" timelimit="5"><result status="valid" time="0.02" steps="6"/></proof>
   </goal>
   <goal name="WP_parameter euclid.4" expl="4. integer overflow">
-  <proof prover="5" timelimit="5"><result status="valid" time="0.10" steps="52"/></proof>
+  <proof prover="5" timelimit="5"><result status="valid" time="0.10" steps="47"/></proof>
   </goal>
   <goal name="WP_parameter euclid.5" expl="5. variant decrease">
-  <proof prover="5" timelimit="5"><result status="valid" time="0.80" steps="185"/></proof>
+  <proof prover="5" timelimit="5"><result status="valid" time="0.49" steps="114"/></proof>
   </goal>
   <goal name="WP_parameter euclid.6" expl="6. precondition">
-  <proof prover="5" timelimit="5"><result status="valid" time="0.03" steps="27"/></proof>
+  <proof prover="5" timelimit="5"><result status="valid" time="0.03" steps="21"/></proof>
   </goal>
   <goal name="WP_parameter euclid.7" expl="7. postcondition">
-  <proof prover="5" timelimit="5"><result status="valid" time="0.52" steps="45"/></proof>
+  <proof prover="5" timelimit="5"><result status="valid" time="0.52" steps="42"/></proof>
   </goal>
  </transf>
  </goal>
diff --git a/examples/gcd/why3shapes.gz b/examples/gcd/why3shapes.gz
index c83a48ac46ef2ff83bdafe4be05df099f88f7b4d..214bbcffb0ad5f40d9812638dd4dcd298b10c0cf 100644
Binary files a/examples/gcd/why3shapes.gz and b/examples/gcd/why3shapes.gz differ
diff --git a/examples/hackers-delight/why3session.xml b/examples/hackers-delight/why3session.xml
index da73f94c4a952b851c3ffe47211ecb90150f6fa0..17d030f836fff9b649aad4d311d715cfe8275e72 100644
--- a/examples/hackers-delight/why3session.xml
+++ b/examples/hackers-delight/why3session.xml
@@ -6,13 +6,13 @@
 <prover id="1" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
 <prover id="2" name="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
 <file name="../hackers-delight.mlw" expanded="true">
-<theory name="Hackers_delight" sum="820a4c97e42cff42b083e7359e8c7425" expanded="true">
+<theory name="Hackers_delight" sum="f68afbb08101be54ae51e015e4048def" expanded="true">
  <goal name="countZero" expanded="true">
  <proof prover="1"><result status="valid" time="0.05"/></proof>
  <proof prover="2"><result status="valid" time="0.09"/></proof>
  </goal>
  <goal name="countStep" expanded="true">
- <proof prover="1"><result status="valid" time="7.86"/></proof>
+ <proof prover="1"><result status="valid" time="4.98"/></proof>
  </goal>
  <goal name="symmetric" expanded="true">
  <proof prover="1"><result status="valid" time="0.02"/></proof>
@@ -27,16 +27,16 @@
  <proof prover="2"><result status="timeout" time="5.00"/></proof>
  </goal>
  <goal name="WP_parameter ascii" expl="VC for ascii" expanded="true">
- <proof prover="1"><result status="valid" time="0.18"/></proof>
+ <proof prover="1"><result status="valid" time="0.04"/></proof>
  </goal>
  <goal name="asciiProp" expanded="true">
- <proof prover="1"><result status="valid" time="1.95"/></proof>
+ <proof prover="1"><result status="valid" time="1.41"/></proof>
  </goal>
  <goal name="iso" expanded="true">
  <proof prover="1"><result status="valid" time="0.40"/></proof>
  </goal>
  <goal name="grayIsGray" expanded="true">
- <proof prover="1"><result status="valid" time="0.17"/></proof>
+ <proof prover="1"><result status="valid" time="0.05"/></proof>
  </goal>
  <goal name="nthGray" expanded="true">
  <proof prover="1"><result status="valid" time="0.05"/></proof>
@@ -45,13 +45,13 @@
  <proof prover="1"><result status="valid" time="0.04"/></proof>
  </goal>
  <goal name="nthBinary" expanded="true">
- <proof prover="1"><result status="valid" time="0.84"/></proof>
+ <proof prover="1"><result status="valid" time="0.48"/></proof>
  </goal>
  <goal name="evenOdd" expanded="true">
  <proof prover="1"><result status="valid" time="0.14"/></proof>
  </goal>
  <goal name="DM1" expanded="true">
- <proof prover="1"><result status="valid" time="0.15"/></proof>
+ <proof prover="1"><result status="valid" time="0.01"/></proof>
  <proof prover="2"><result status="valid" time="0.01"/></proof>
  </goal>
  <goal name="DM2" expanded="true">
@@ -108,7 +108,7 @@
  <proof prover="1"><result status="valid" time="0.12"/></proof>
  </goal>
  <goal name="Ao" expanded="true">
- <proof prover="1"><result status="valid" time="0.14"/></proof>
+ <proof prover="1"><result status="valid" time="0.02"/></proof>
  </goal>
  <goal name="Aq" expanded="true">
  <proof prover="1"><result status="valid" time="0.08"/></proof>
diff --git a/examples/hackers-delight/why3shapes.gz b/examples/hackers-delight/why3shapes.gz
index c23f241a2f630451a0934c51f393366a733cf98c..765ee59af224d3994c777165c82f033bbca47698 100644
Binary files a/examples/hackers-delight/why3shapes.gz and b/examples/hackers-delight/why3shapes.gz differ
diff --git a/examples/logic/bitvectors/why3session.xml b/examples/logic/bitvectors/why3session.xml
index 683073f2399d8df3c1ae7f2234b18dd36bfb0af4..529418dca12f6da6f0b6b6b6ee70cbc0adb6b76b 100644
--- a/examples/logic/bitvectors/why3session.xml
+++ b/examples/logic/bitvectors/why3session.xml
@@ -7,7 +7,7 @@
 <prover id="2" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
 <prover id="3" name="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
 <file name="../bitvectors.why" expanded="true">
-<theory name="TestBV" sum="fa2ee38ac18722cb5bafd96ed112adc3" expanded="true">
+<theory name="TestBV" sum="362573c1d9c043dd414d1edaaa78f89f" expanded="true">
  <goal name="g1" expanded="true">
  <proof prover="2"><result status="valid" time="0.01"/></proof>
  <proof prover="3"><result status="valid" time="0.01"/></proof>
@@ -67,7 +67,7 @@
  <proof prover="3"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="g4b" expanded="true">
- <proof prover="0"><result status="valid" time="0.35" steps="159"/></proof>
+ <proof prover="0"><result status="valid" time="0.19" steps="159"/></proof>
  <proof prover="2"><result status="valid" time="0.02"/></proof>
  <proof prover="3"><result status="valid" time="0.00"/></proof>
  </goal>
diff --git a/examples/logic/bitvectors/why3shapes.gz b/examples/logic/bitvectors/why3shapes.gz
index c7ae85e355a71e8e7f9afd33ffc53dfdb3df4aa1..2e95a993b9f642cf5436997acde6c72697a8f11c 100644
Binary files a/examples/logic/bitvectors/why3shapes.gz and b/examples/logic/bitvectors/why3shapes.gz differ
diff --git a/examples/mergesort_array/why3session.xml b/examples/mergesort_array/why3session.xml
index c158786aadac4c7cd7b58aa1e307df3dbfbf4654..92d499da809c74e7011d14aee3f53b2d86a47726 100644
--- a/examples/mergesort_array/why3session.xml
+++ b/examples/mergesort_array/why3session.xml
@@ -320,37 +320,37 @@
   <transf name="inline_goal">
    <goal name="WP_parameter merge.53.1" expl="1. postcondition">
    <transf name="split_goal_wp">
-    <goal name="WP_parameter merge.53.1.1" expl="1.">
+    <goal name="WP_parameter merge.53.1.1" expl="1. VC for merge">
     <proof prover="2"><result status="valid" time="0.01" steps="2"/></proof>
     <proof prover="4"><result status="valid" time="0.04"/></proof>
     <proof prover="8" timelimit="40"><result status="valid" time="0.03" steps="2"/></proof>
     <proof prover="9"><result status="valid" time="0.02"/></proof>
     </goal>
-    <goal name="WP_parameter merge.53.1.2" expl="2.">
+    <goal name="WP_parameter merge.53.1.2" expl="2. VC for merge">
     <proof prover="2"><result status="valid" time="0.02" steps="3"/></proof>
     <proof prover="4"><result status="valid" time="0.03"/></proof>
     <proof prover="8" timelimit="40"><result status="valid" time="0.05" steps="3"/></proof>
     <proof prover="9"><result status="valid" time="0.02"/></proof>
     </goal>
-    <goal name="WP_parameter merge.53.1.3" expl="3.">
+    <goal name="WP_parameter merge.53.1.3" expl="3. VC for merge">
     <proof prover="2"><result status="valid" time="0.03" steps="20"/></proof>
     <proof prover="4"><result status="valid" time="0.04"/></proof>
     <proof prover="8" timelimit="40"><result status="valid" time="0.04" steps="8"/></proof>
     <proof prover="9"><result status="valid" time="0.02"/></proof>
     </goal>
-    <goal name="WP_parameter merge.53.1.4" expl="4.">
+    <goal name="WP_parameter merge.53.1.4" expl="4. VC for merge">
     <proof prover="2"><result status="valid" time="0.02" steps="6"/></proof>
     <proof prover="4"><result status="valid" time="0.03"/></proof>
     <proof prover="8" timelimit="40"><result status="valid" time="0.05" steps="8"/></proof>
     <proof prover="9"><result status="valid" time="0.02"/></proof>
     </goal>
-    <goal name="WP_parameter merge.53.1.5" expl="5.">
+    <goal name="WP_parameter merge.53.1.5" expl="5. VC for merge">
     <proof prover="2"><result status="valid" time="0.02" steps="3"/></proof>
     <proof prover="4"><result status="valid" time="0.04"/></proof>
     <proof prover="8" timelimit="40"><result status="valid" time="0.04" steps="3"/></proof>
     <proof prover="9"><result status="valid" time="0.02"/></proof>
     </goal>
-    <goal name="WP_parameter merge.53.1.6" expl="6.">
+    <goal name="WP_parameter merge.53.1.6" expl="6. VC for merge">
     <proof prover="4"><result status="valid" time="0.24"/></proof>
     <proof prover="6" timelimit="40"><result status="valid" time="0.06"/></proof>
     <proof prover="9"><result status="valid" time="0.02"/></proof>
@@ -435,20 +435,20 @@
   <transf name="inline_goal">
    <goal name="WP_parameter merge_using.11.1" expl="1. assertion">
    <transf name="split_goal_wp">
-    <goal name="WP_parameter merge_using.11.1.1" expl="1.">
+    <goal name="WP_parameter merge_using.11.1.1" expl="1. VC for merge_using">
     <proof prover="2"><result status="valid" time="0.03" steps="21"/></proof>
     <proof prover="4"><result status="valid" time="0.05"/></proof>
     <proof prover="8" timelimit="20"><result status="valid" time="0.08" steps="21"/></proof>
     <proof prover="9"><result status="valid" time="0.02"/></proof>
     </goal>
-    <goal name="WP_parameter merge_using.11.1.2" expl="2.">
+    <goal name="WP_parameter merge_using.11.1.2" expl="2. VC for merge_using">
     <proof prover="1"><result status="valid" time="0.26"/></proof>
     <proof prover="2"><result status="valid" time="1.15" steps="379"/></proof>
     <proof prover="4"><result status="valid" time="0.12"/></proof>
     <proof prover="6"><result status="valid" time="1.15"/></proof>
     <proof prover="9"><result status="valid" time="0.03"/></proof>
     </goal>
-    <goal name="WP_parameter merge_using.11.1.3" expl="3.">
+    <goal name="WP_parameter merge_using.11.1.3" expl="3. VC for merge_using">
     <proof prover="2"><result status="valid" time="0.02" steps="21"/></proof>
     <proof prover="4"><result status="valid" time="0.06"/></proof>
     <proof prover="8" timelimit="20"><result status="valid" time="0.05" steps="21"/></proof>
@@ -1008,13 +1008,13 @@
   </goal>
   <goal name="WP_parameter natural_mergesort.13" expl="13. loop variant decrease">
   <transf name="split_goal_wp">
-   <goal name="WP_parameter natural_mergesort.13.1" expl="1.">
+   <goal name="WP_parameter natural_mergesort.13.1" expl="1. VC for natural_mergesort">
    <proof prover="2"><result status="valid" time="0.02" steps="23"/></proof>
    <proof prover="4"><result status="valid" time="0.03"/></proof>
    <proof prover="8"><result status="valid" time="0.02" steps="23"/></proof>
    <proof prover="9"><result status="valid" time="0.02"/></proof>
    </goal>
-   <goal name="WP_parameter natural_mergesort.13.2" expl="2.">
+   <goal name="WP_parameter natural_mergesort.13.2" expl="2. VC for natural_mergesort">
    <proof prover="2"><result status="valid" time="0.02" steps="23"/></proof>
    <proof prover="4"><result status="valid" time="0.03"/></proof>
    <proof prover="8"><result status="valid" time="0.06" steps="23"/></proof>
@@ -1110,7 +1110,6 @@
   <goal name="WP_parameter natural_mergesort.29" expl="29. loop invariant preservation">
   <proof prover="2"><result status="valid" time="0.18" steps="267"/></proof>
   <proof prover="4"><result status="valid" time="0.37"/></proof>
-  <proof prover="8"><result status="valid" time="5.30" steps="2461"/></proof>
   <proof prover="9"><result status="valid" time="0.29"/></proof>
   </goal>
   <goal name="WP_parameter natural_mergesort.30" expl="30. loop invariant preservation">
@@ -1145,13 +1144,13 @@
   </goal>
   <goal name="WP_parameter natural_mergesort.35" expl="35. loop variant decrease">
   <transf name="split_goal_wp">
-   <goal name="WP_parameter natural_mergesort.35.1" expl="1.">
+   <goal name="WP_parameter natural_mergesort.35.1" expl="1. VC for natural_mergesort">
    <proof prover="2"><result status="valid" time="0.01" steps="15"/></proof>
    <proof prover="4"><result status="valid" time="0.03"/></proof>
    <proof prover="8"><result status="valid" time="0.05" steps="15"/></proof>
    <proof prover="9"><result status="valid" time="0.02"/></proof>
    </goal>
-   <goal name="WP_parameter natural_mergesort.35.2" expl="2.">
+   <goal name="WP_parameter natural_mergesort.35.2" expl="2. VC for natural_mergesort">
    <proof prover="2"><result status="valid" time="0.02" steps="21"/></proof>
    <proof prover="4"><result status="valid" time="0.03"/></proof>
    <proof prover="8"><result status="valid" time="0.06" steps="21"/></proof>
@@ -1287,31 +1286,31 @@
   </goal>
   <goal name="WP_parameter naturalrec.20" expl="20. precondition">
   <transf name="split_goal_wp">
-   <goal name="WP_parameter naturalrec.20.1" expl="1.">
+   <goal name="WP_parameter naturalrec.20.1" expl="1. VC for naturalrec">
    <proof prover="2"><result status="valid" time="0.02" steps="25"/></proof>
    <proof prover="4"><result status="valid" time="0.03"/></proof>
    <proof prover="8"><result status="valid" time="0.02" steps="25"/></proof>
    <proof prover="9"><result status="valid" time="0.01"/></proof>
    </goal>
-   <goal name="WP_parameter naturalrec.20.2" expl="2.">
+   <goal name="WP_parameter naturalrec.20.2" expl="2. VC for naturalrec">
    <proof prover="2"><result status="valid" time="0.02" steps="25"/></proof>
    <proof prover="4"><result status="valid" time="0.03"/></proof>
    <proof prover="8"><result status="valid" time="0.03" steps="25"/></proof>
    <proof prover="9"><result status="valid" time="0.02"/></proof>
    </goal>
-   <goal name="WP_parameter naturalrec.20.3" expl="3.">
+   <goal name="WP_parameter naturalrec.20.3" expl="3. VC for naturalrec">
    <proof prover="2"><result status="valid" time="0.02" steps="35"/></proof>
    <proof prover="4"><result status="valid" time="0.03"/></proof>
    <proof prover="8"><result status="valid" time="0.03" steps="35"/></proof>
    <proof prover="9"><result status="valid" time="0.02"/></proof>
    </goal>
-   <goal name="WP_parameter naturalrec.20.4" expl="4.">
+   <goal name="WP_parameter naturalrec.20.4" expl="4. VC for naturalrec">
    <proof prover="2"><result status="valid" time="0.02" steps="36"/></proof>
    <proof prover="4"><result status="valid" time="0.03"/></proof>
    <proof prover="8"><result status="valid" time="0.02" steps="36"/></proof>
    <proof prover="9"><result status="valid" time="0.02"/></proof>
    </goal>
-   <goal name="WP_parameter naturalrec.20.5" expl="5.">
+   <goal name="WP_parameter naturalrec.20.5" expl="5. VC for naturalrec">
    <proof prover="2"><result status="valid" time="0.02" steps="25"/></proof>
    <proof prover="4"><result status="valid" time="0.03"/></proof>
    <proof prover="8"><result status="valid" time="0.02" steps="25"/></proof>
diff --git a/examples/mergesort_array/why3shapes.gz b/examples/mergesort_array/why3shapes.gz
index 2bb7d304ee862b9cc26bb8dfa25f99c8435569e7..c229d462072fafd5d69036111cd519097e57d9d8 100644
Binary files a/examples/mergesort_array/why3shapes.gz and b/examples/mergesort_array/why3shapes.gz differ
diff --git a/examples/queens/why3session.xml b/examples/queens/why3session.xml
index deb80111a2bdbba44f2feeb3ffaf8c7cafaa27b2..5c145f7f690eefab264723729db50a93a20498b8 100644
--- a/examples/queens/why3session.xml
+++ b/examples/queens/why3session.xml
@@ -57,7 +57,7 @@
  <proof prover="6"><result status="valid" time="0.00"/></proof>
  </goal>
 </theory>
-<theory name="NQueensSets" sum="21ba9f04704df48b44f79a7e140ea9f4" expanded="true">
+<theory name="NQueensSets" sum="9c0bbd6174a933f1b5286251b86db37a" expanded="true">
  <goal name="WP_parameter t3" expl="VC for t3" expanded="true">
  <transf name="split_goal_wp" expanded="true">
   <goal name="WP_parameter t3.1" expl="1. loop invariant init" expanded="true">
@@ -107,7 +107,7 @@
    <proof prover="10"><result status="valid" time="2.23" steps="409"/></proof>
    </goal>
    <goal name="WP_parameter t3.3.7" expl="7. VC for t3" expanded="true">
-   <proof prover="0" memlimit="1000" edited="queens_WP_NQueensSets_WP_parameter_t3_1.v"><result status="valid" time="2.07"/></proof>
+   <proof prover="0" memlimit="1000" edited="queens_WP_NQueensSets_WP_parameter_t3_1.v"><result status="valid" time="1.76"/></proof>
    <proof prover="3"><result status="valid" time="5.43" steps="618"/></proof>
    <proof prover="10"><result status="valid" time="2.08" steps="562"/></proof>
    </goal>
@@ -137,7 +137,7 @@
      <proof prover="10"><result status="valid" time="1.68" steps="285"/></proof>
      </goal>
      <goal name="WP_parameter t3.3.12.1.3" expl="3. VC for t3" expanded="true">
-     <proof prover="1"><result status="valid" time="9.75"/></proof>
+     <proof prover="1"><result status="valid" time="0.23"/></proof>
      </goal>
      <goal name="WP_parameter t3.3.12.1.4" expl="4. VC for t3" expanded="true">
      <metas
@@ -819,8 +819,8 @@
       <goal name="WP_parameter t3.3.12.1.4" expl="4. VC for t3" expanded="true">
       <transf name="eliminate_builtin" expanded="true">
        <goal name="WP_parameter t3.3.12.1.4.1" expl="1. VC for t3" expanded="true">
-       <proof prover="5" timelimit="25" obsolete="true"><result status="valid" time="0.12"/></proof>
-       <proof prover="9" obsolete="true"><result status="valid" time="0.01"/></proof>
+       <proof prover="5" timelimit="25"><result status="valid" time="0.12"/></proof>
+       <proof prover="9"><result status="valid" time="0.01"/></proof>
        </goal>
       </transf>
       </goal>
@@ -868,7 +868,7 @@
    <proof prover="7"><result status="valid" time="0.04"/></proof>
    </goal>
    <goal name="WP_parameter t3.4.6" expl="6. VC for t3" expanded="true">
-   <proof prover="0" timelimit="10" edited="queens_WP_NQueensSets_WP_parameter_t3_5.v"><result status="valid" time="3.32"/></proof>
+   <proof prover="0" timelimit="10" edited="queens_WP_NQueensSets_WP_parameter_t3_5.v"><result status="valid" time="2.87"/></proof>
    </goal>
    <goal name="WP_parameter t3.4.7" expl="7. VC for t3" expanded="true">
    <proof prover="0" timelimit="10" edited="queens_WP_NQueensSets_WP_parameter_t3_6.v"><result status="valid" time="1.60"/></proof>
@@ -877,7 +877,7 @@
    <proof prover="6" timelimit="55"><result status="valid" time="1.92"/></proof>
    </goal>
    <goal name="WP_parameter t3.4.9" expl="9. VC for t3" expanded="true">
-   <proof prover="1"><result status="valid" time="0.20"/></proof>
+   <proof prover="1"><result status="valid" time="0.08"/></proof>
    <proof prover="6"><result status="valid" time="0.21"/></proof>
    </goal>
    <goal name="WP_parameter t3.4.10" expl="10. VC for t3" expanded="true">
@@ -1032,30 +1032,30 @@
 </theory>
 <theory name="Bits" sum="87ba23b038d8da5026df22be3839311c" expanded="true">
  <goal name="WP_parameter zero" expl="VC for zero" expanded="true">
- <proof prover="11" obsolete="true"><result status="valid" time="0.03" steps="80"/></proof>
+ <proof prover="11"><result status="valid" time="0.03" steps="80"/></proof>
  </goal>
  <goal name="WP_parameter remove_singleton" expl="VC for remove_singleton" expanded="true">
- <proof prover="11" obsolete="true"><result status="valid" time="1.25" steps="578"/></proof>
+ <proof prover="11"><result status="valid" time="0.80" steps="578"/></proof>
  </goal>
  <goal name="WP_parameter add_singleton" expl="VC for add_singleton" expanded="true">
- <proof prover="2" obsolete="true"><result status="valid" time="1.30"/></proof>
+ <proof prover="2"><result status="valid" time="1.30"/></proof>
  </goal>
  <goal name="WP_parameter mul2" expl="VC for mul2" expanded="true">
- <proof prover="11" obsolete="true"><result status="valid" time="0.48" steps="218"/></proof>
+ <proof prover="11"><result status="valid" time="0.27" steps="218"/></proof>
  </goal>
  <goal name="WP_parameter div2" expl="VC for div2" expanded="true">
- <proof prover="11" obsolete="true"><result status="valid" time="0.31" steps="109"/></proof>
+ <proof prover="11"><result status="valid" time="0.18" steps="109"/></proof>
  </goal>
  <goal name="WP_parameter diff" expl="VC for diff" expanded="true">
- <proof prover="11" obsolete="true"><result status="valid" time="0.46" steps="228"/></proof>
+ <proof prover="11"><result status="valid" time="0.27" steps="228"/></proof>
  </goal>
  <goal name="WP_parameter rightmost_bit_trick" expl="VC for rightmost_bit_trick" expanded="true">
- <proof prover="2" timelimit="20" obsolete="true"><result status="timeout" time="19.98"/></proof>
- <proof prover="5" obsolete="true"><result status="timeout" time="5.05"/></proof>
- <proof prover="11" obsolete="true"><result status="timeout" time="4.98"/></proof>
+ <proof prover="2" timelimit="20"><result status="timeout" time="19.98"/></proof>
+ <proof prover="5"><result status="timeout" time="5.05"/></proof>
+ <proof prover="11"><result status="timeout" time="4.98"/></proof>
  </goal>
  <goal name="WP_parameter below" expl="VC for below" expanded="true">
- <proof prover="11" obsolete="true"><result status="valid" time="0.18" steps="118"/></proof>
+ <proof prover="11"><result status="valid" time="0.18" steps="118"/></proof>
  </goal>
 </theory>
 </file>
diff --git a/examples/queens/why3shapes.gz b/examples/queens/why3shapes.gz
index de0e1b32dd4a8adc9e7bbc7088ee8e3124dd34d0..7f6749f274248421f454e8433a0652137f45d248 100644
Binary files a/examples/queens/why3shapes.gz and b/examples/queens/why3shapes.gz differ
diff --git a/examples/vstte10_queens/why3session.xml b/examples/vstte10_queens/why3session.xml
index f8b8a0a8c5263744fceebb8e72bdd698fd587abd..e1468510588756aa81d9b0814533e79d1a1ddc0a 100644
--- a/examples/vstte10_queens/why3session.xml
+++ b/examples/vstte10_queens/why3session.xml
@@ -50,9 +50,9 @@
  <proof prover="4" memlimit="1000"><result status="valid" time="0.01" steps="0"/></proof>
  </goal>
 </theory>
-<theory name="MachineArithmetic" sum="5cefdde670c8babce2b61c2fb35e26ba" expanded="true">
+<theory name="MachineArithmetic" sum="b8c9688f207f76a2a08d9e9c133a76ab" expanded="true">
  <goal name="WP_parameter mcheck_is_consistent" expl="VC for mcheck_is_consistent" expanded="true">
- <proof prover="0"><result status="valid" time="0.27"/></proof>
+ <proof prover="0"><result status="valid" time="0.09"/></proof>
  </goal>
  <goal name="WP_parameter mcount_bt_queens" expl="VC for mcount_bt_queens" expanded="true">
  <transf name="split_goal_wp" expanded="true">
@@ -60,120 +60,120 @@
   <proof prover="5"><result status="valid" time="0.02"/></proof>
   </goal>
   <goal name="WP_parameter mcount_bt_queens.2" expl="2. postcondition">
-  <proof prover="4" memlimit="1000"><result status="valid" time="0.02" steps="15"/></proof>
+  <proof prover="4" memlimit="1000"><result status="valid" time="0.02" steps="12"/></proof>
   </goal>
   <goal name="WP_parameter mcount_bt_queens.3" expl="3. postcondition">
-  <proof prover="4" memlimit="1000"><result status="valid" time="0.02" steps="15"/></proof>
+  <proof prover="4" memlimit="1000"><result status="valid" time="0.02" steps="12"/></proof>
   </goal>
   <goal name="WP_parameter mcount_bt_queens.4" expl="4. index in array bounds">
-  <proof prover="4" memlimit="1000"><result status="valid" time="0.02" steps="18"/></proof>
+  <proof prover="4" memlimit="1000"><result status="valid" time="0.02" steps="15"/></proof>
   </goal>
   <goal name="WP_parameter mcount_bt_queens.5" expl="5. precondition">
-  <proof prover="4" memlimit="1000"><result status="valid" time="0.02" steps="20"/></proof>
+  <proof prover="4" memlimit="1000"><result status="valid" time="0.02" steps="17"/></proof>
   </goal>
   <goal name="WP_parameter mcount_bt_queens.6" expl="6. precondition">
   <proof prover="0"><result status="valid" time="0.05"/></proof>
   </goal>
   <goal name="WP_parameter mcount_bt_queens.7" expl="7. integer overflow">
-  <proof prover="4" memlimit="1000"><result status="valid" time="0.02" steps="23"/></proof>
+  <proof prover="4" memlimit="1000"><result status="valid" time="0.02" steps="20"/></proof>
   </goal>
   <goal name="WP_parameter mcount_bt_queens.8" expl="8. integer overflow">
-  <proof prover="4" memlimit="1000"><result status="valid" time="0.04" steps="50"/></proof>
+  <proof prover="4" memlimit="1000"><result status="valid" time="0.04" steps="43"/></proof>
   </goal>
   <goal name="WP_parameter mcount_bt_queens.9" expl="9. variant decrease">
-  <proof prover="4" memlimit="1000"><result status="valid" time="0.02" steps="26"/></proof>
+  <proof prover="4" memlimit="1000"><result status="valid" time="0.02" steps="23"/></proof>
   </goal>
   <goal name="WP_parameter mcount_bt_queens.10" expl="10. precondition">
-  <proof prover="4" memlimit="1000"><result status="valid" time="0.02" steps="26"/></proof>
+  <proof prover="4" memlimit="1000"><result status="valid" time="0.02" steps="23"/></proof>
   </goal>
   <goal name="WP_parameter mcount_bt_queens.11" expl="11. precondition">
-  <proof prover="4" memlimit="1000"><result status="valid" time="0.02" steps="26"/></proof>
+  <proof prover="4" memlimit="1000"><result status="valid" time="0.02" steps="23"/></proof>
   </goal>
   <goal name="WP_parameter mcount_bt_queens.12" expl="12. precondition">
-  <proof prover="4" memlimit="1000"><result status="valid" time="0.01" steps="26"/></proof>
+  <proof prover="4" memlimit="1000"><result status="valid" time="0.01" steps="23"/></proof>
   </goal>
   <goal name="WP_parameter mcount_bt_queens.13" expl="13. precondition" expanded="true">
-  <proof prover="4" memlimit="1000"><result status="valid" time="0.02" steps="31"/></proof>
+  <proof prover="4" memlimit="1000"><result status="valid" time="0.02" steps="28"/></proof>
   </goal>
   <goal name="WP_parameter mcount_bt_queens.14" expl="14. integer overflow">
-  <proof prover="4" memlimit="1000"><result status="valid" time="0.02" steps="37"/></proof>
+  <proof prover="4" memlimit="1000"><result status="valid" time="0.02" steps="34"/></proof>
   </goal>
   <goal name="WP_parameter mcount_bt_queens.15" expl="15. integer overflow">
-  <proof prover="4" memlimit="1000"><result status="valid" time="0.08" steps="71"/></proof>
+  <proof prover="4" memlimit="1000"><result status="valid" time="0.08" steps="64"/></proof>
   </goal>
   <goal name="WP_parameter mcount_bt_queens.16" expl="16. variant decrease">
-  <proof prover="4" memlimit="1000"><result status="valid" time="0.02" steps="40"/></proof>
+  <proof prover="4" memlimit="1000"><result status="valid" time="0.02" steps="37"/></proof>
   </goal>
   <goal name="WP_parameter mcount_bt_queens.17" expl="17. precondition">
-  <proof prover="4" memlimit="1000"><result status="valid" time="0.02" steps="40"/></proof>
+  <proof prover="4" memlimit="1000"><result status="valid" time="0.02" steps="37"/></proof>
   </goal>
   <goal name="WP_parameter mcount_bt_queens.18" expl="18. precondition">
-  <proof prover="4" memlimit="1000"><result status="valid" time="0.03" steps="40"/></proof>
+  <proof prover="4" memlimit="1000"><result status="valid" time="0.03" steps="37"/></proof>
   </goal>
   <goal name="WP_parameter mcount_bt_queens.19" expl="19. precondition">
   <proof prover="0"><result status="valid" time="0.05"/></proof>
   </goal>
   <goal name="WP_parameter mcount_bt_queens.20" expl="20. postcondition">
-  <proof prover="4" memlimit="1000"><result status="valid" time="0.02" steps="45"/></proof>
+  <proof prover="4" memlimit="1000"><result status="valid" time="0.02" steps="42"/></proof>
   </goal>
   <goal name="WP_parameter mcount_bt_queens.21" expl="21. postcondition">
-  <proof prover="4" memlimit="1000"><result status="valid" time="0.02" steps="45"/></proof>
+  <proof prover="4" memlimit="1000"><result status="valid" time="0.02" steps="42"/></proof>
   </goal>
   <goal name="WP_parameter mcount_bt_queens.22" expl="22. integer overflow">
-  <proof prover="4" memlimit="1000"><result status="valid" time="0.01" steps="23"/></proof>
+  <proof prover="4" memlimit="1000"><result status="valid" time="0.01" steps="20"/></proof>
   </goal>
   <goal name="WP_parameter mcount_bt_queens.23" expl="23. integer overflow">
-  <proof prover="4" memlimit="1000"><result status="valid" time="0.15" steps="50"/></proof>
+  <proof prover="4" memlimit="1000"><result status="valid" time="0.02" steps="43"/></proof>
   </goal>
   <goal name="WP_parameter mcount_bt_queens.24" expl="24. variant decrease">
-  <proof prover="4" memlimit="1000"><result status="valid" time="0.02" steps="26"/></proof>
+  <proof prover="4" memlimit="1000"><result status="valid" time="0.02" steps="23"/></proof>
   </goal>
   <goal name="WP_parameter mcount_bt_queens.25" expl="25. precondition">
-  <proof prover="4" memlimit="1000"><result status="valid" time="0.02" steps="26"/></proof>
+  <proof prover="4" memlimit="1000"><result status="valid" time="0.02" steps="23"/></proof>
   </goal>
   <goal name="WP_parameter mcount_bt_queens.26" expl="26. precondition">
-  <proof prover="4" memlimit="1000"><result status="valid" time="0.02" steps="26"/></proof>
+  <proof prover="4" memlimit="1000"><result status="valid" time="0.02" steps="23"/></proof>
   </goal>
   <goal name="WP_parameter mcount_bt_queens.27" expl="27. precondition">
-  <proof prover="4" memlimit="1000"><result status="valid" time="0.48" steps="107"/></proof>
+  <proof prover="4" memlimit="1000"><result status="valid" time="0.08" steps="42"/></proof>
   </goal>
   <goal name="WP_parameter mcount_bt_queens.28" expl="28. postcondition">
-  <proof prover="4" memlimit="1000"><result status="valid" time="0.02" steps="31"/></proof>
+  <proof prover="4" memlimit="1000"><result status="valid" time="0.02" steps="28"/></proof>
   </goal>
   <goal name="WP_parameter mcount_bt_queens.29" expl="29. postcondition">
-  <proof prover="4" memlimit="1000"><result status="valid" time="0.02" steps="31"/></proof>
+  <proof prover="4" memlimit="1000"><result status="valid" time="0.02" steps="28"/></proof>
   </goal>
   <goal name="WP_parameter mcount_bt_queens.30" expl="30. postcondition">
-  <proof prover="4" memlimit="1000"><result status="valid" time="0.02" steps="18"/></proof>
+  <proof prover="4" memlimit="1000"><result status="valid" time="0.02" steps="15"/></proof>
   </goal>
   <goal name="WP_parameter mcount_bt_queens.31" expl="31. postcondition">
-  <proof prover="4" memlimit="1000"><result status="valid" time="0.02" steps="18"/></proof>
+  <proof prover="4" memlimit="1000"><result status="valid" time="0.02" steps="15"/></proof>
   </goal>
   <goal name="WP_parameter mcount_bt_queens.32" expl="32. integer overflow">
-  <proof prover="4" memlimit="1000"><result status="valid" time="0.02" steps="13"/></proof>
+  <proof prover="4" memlimit="1000"><result status="valid" time="0.02" steps="10"/></proof>
   </goal>
   <goal name="WP_parameter mcount_bt_queens.33" expl="33. precondition">
-  <proof prover="4" memlimit="1000"><result status="valid" time="0.02" steps="14"/></proof>
+  <proof prover="4" memlimit="1000"><result status="valid" time="0.02" steps="11"/></proof>
   </goal>
   <goal name="WP_parameter mcount_bt_queens.34" expl="34. precondition">
-  <proof prover="4" memlimit="1000"><result status="valid" time="0.02" steps="14"/></proof>
+  <proof prover="4" memlimit="1000"><result status="valid" time="0.02" steps="11"/></proof>
   </goal>
   <goal name="WP_parameter mcount_bt_queens.35" expl="35. precondition">
-  <proof prover="4" memlimit="1000"><result status="valid" time="0.02" steps="14"/></proof>
+  <proof prover="4" memlimit="1000"><result status="valid" time="0.02" steps="11"/></proof>
   </goal>
   <goal name="WP_parameter mcount_bt_queens.36" expl="36. postcondition">
-  <proof prover="4" memlimit="1000"><result status="valid" time="0.02" steps="18"/></proof>
+  <proof prover="4" memlimit="1000"><result status="valid" time="0.02" steps="15"/></proof>
   </goal>
   <goal name="WP_parameter mcount_bt_queens.37" expl="37. postcondition">
-  <proof prover="4" memlimit="1000"><result status="valid" time="0.01" steps="18"/></proof>
+  <proof prover="4" memlimit="1000"><result status="valid" time="0.01" steps="15"/></proof>
   </goal>
  </transf>
  </goal>
  <goal name="WP_parameter mcount_queens" expl="VC for mcount_queens">
- <proof prover="4" memlimit="1000"><result status="valid" time="0.02" steps="14"/></proof>
+ <proof prover="4" memlimit="1000"><result status="valid" time="0.02" steps="11"/></proof>
  </goal>
  <goal name="WP_parameter test_mcount_8" expl="VC for test_mcount_8">
- <proof prover="4" memlimit="1000"><result status="valid" time="0.02" steps="10"/></proof>
+ <proof prover="4" memlimit="1000"><result status="valid" time="0.02" steps="7"/></proof>
  <proof prover="5"><result status="valid" time="0.01"/></proof>
  </goal>
 </theory>
diff --git a/examples/vstte10_queens/why3shapes.gz b/examples/vstte10_queens/why3shapes.gz
index ced9eb66d5afff09c9d1052de4dd48e3c61719f1..b49c7fac2095af9f501f5be9d99773cdb723fa7b 100644
Binary files a/examples/vstte10_queens/why3shapes.gz and b/examples/vstte10_queens/why3shapes.gz differ