diff --git a/examples/add_list/why3shapes.gz b/examples/add_list/why3shapes.gz
index f3fb3aebe4edd8b7383fced6a01d684e96f46dda..7ca799cfd9bb1926c59dd791e6e2a9d5a4d5e0c8 100644
Binary files a/examples/add_list/why3shapes.gz and b/examples/add_list/why3shapes.gz differ
diff --git a/examples/add_list_vc_sp/why3shapes.gz b/examples/add_list_vc_sp/why3shapes.gz
index 439adc4317b37a8dc7d1ef2e03c1d9b11026a3ec..da60f42a7d61ffdacd6d76b462d03b3d7f92bcb6 100644
Binary files a/examples/add_list_vc_sp/why3shapes.gz and b/examples/add_list_vc_sp/why3shapes.gz differ
diff --git a/examples/bitvectors/double/why3session.xml b/examples/bitvectors/double/why3session.xml
index 7814590ef9f04a8c40cb4ee2a84bdd214b5653ee..8417dff63211385fdb1dd7845fed2397be471eb5 100644
--- a/examples/bitvectors/double/why3session.xml
+++ b/examples/bitvectors/double/why3session.xml
@@ -33,7 +33,7 @@
  <goal name="mantissa_one" proved="true">
  <proof prover="2"><result status="valid" time="0.09" steps="88"/></proof>
  <proof prover="3"><result status="valid" time="1.04"/></proof>
- <proof prover="5" timelimit="11"><result status="valid" time="3.11"/></proof>
+ <proof prover="5" timelimit="11"><result status="valid" time="2.58"/></proof>
  </goal>
  <goal name="double_value_of_1" proved="true">
  <proof prover="1"><result status="valid" time="0.03"/></proof>
diff --git a/examples/bitvectors/double/why3shapes.gz b/examples/bitvectors/double/why3shapes.gz
index 26fae3d7086e27c440e2e8a11b6b92c0a03c1d22..22617ff69c6e355bba08993ef7f3e0b1149b8912 100644
Binary files a/examples/bitvectors/double/why3shapes.gz and b/examples/bitvectors/double/why3shapes.gz differ
diff --git a/examples/bitvectors/double_of_int/why3session.xml b/examples/bitvectors/double_of_int/why3session.xml
index 4bd77e7d3ffa05081eadb103383a4bb6c02ba4e1..61d3ae53d24d1162f887d1944d6e94b510383c65 100644
--- a/examples/bitvectors/double_of_int/why3session.xml
+++ b/examples/bitvectors/double_of_int/why3session.xml
@@ -62,7 +62,7 @@
  <proof prover="10"><result status="valid" time="0.11" steps="101"/></proof>
  </goal>
  <goal name="nth_const6" proved="true">
- <proof prover="4"><result status="valid" time="1.72"/></proof>
+ <proof prover="4"><result status="valid" time="1.39"/></proof>
  <proof prover="8"><result status="valid" time="0.79"/></proof>
  <proof prover="10"><result status="valid" time="0.09" steps="101"/></proof>
  </goal>
@@ -94,7 +94,7 @@
  </goal>
  <goal name="to_nat_mantissa_1" proved="true">
  <proof prover="4"><result status="valid" time="1.11"/></proof>
- <proof prover="6" timelimit="10"><result status="valid" time="2.87"/></proof>
+ <proof prover="6" timelimit="10"><result status="valid" time="2.38"/></proof>
  <proof prover="8"><result status="valid" time="0.76"/></proof>
  <proof prover="10"><result status="valid" time="0.05" steps="93"/></proof>
  </goal>
@@ -142,7 +142,7 @@
  </goal>
  <goal name="nth_0_30" proved="true">
  <proof prover="2"><result status="valid" time="0.46"/></proof>
- <proof prover="4"><result status="valid" time="3.60"/></proof>
+ <proof prover="4"><result status="valid" time="3.04"/></proof>
  </goal>
  <goal name="nth_jpxor_0_30" proved="true">
  <proof prover="2"><result status="valid" time="0.06"/></proof>
@@ -363,9 +363,9 @@
  <proof prover="10"><result status="valid" time="0.07" steps="97"/></proof>
  </goal>
  <goal name="MainResult" proved="true">
- <proof prover="2"><result status="valid" time="0.26"/></proof>
- <proof prover="4"><result status="valid" time="3.62"/></proof>
- <proof prover="6" timelimit="11"><result status="valid" time="2.70"/></proof>
+ <proof prover="2"><result status="valid" time="0.07"/></proof>
+ <proof prover="4"><result status="valid" time="0.09"/></proof>
+ <proof prover="6" timelimit="11"><result status="valid" time="3.15"/></proof>
  <proof prover="8"><result status="valid" time="0.74"/></proof>
  <proof prover="10"><result status="valid" time="0.26" steps="146"/></proof>
  </goal>
diff --git a/examples/bitvectors/double_of_int/why3shapes.gz b/examples/bitvectors/double_of_int/why3shapes.gz
index 1f9b62755cc6c96ffca7f7d6ecb00c420f0f6eb8..745d3d3937c7865819ed287121bd873abe2200ba 100644
Binary files a/examples/bitvectors/double_of_int/why3shapes.gz and b/examples/bitvectors/double_of_int/why3shapes.gz differ
diff --git a/examples/bitvectors/neg_as_xor/why3session.xml b/examples/bitvectors/neg_as_xor/why3session.xml
index a9e3b46d5428b1704ec35992cbf5456827bbcbf1..e335573afa46afa524b3351237d1f5cfed43f117 100644
--- a/examples/bitvectors/neg_as_xor/why3session.xml
+++ b/examples/bitvectors/neg_as_xor/why3session.xml
@@ -15,7 +15,7 @@
  </goal>
  <goal name="sign_of_j" proved="true">
  <proof prover="0"><result status="valid" time="0.02" steps="75"/></proof>
- <proof prover="3"><result status="valid" time="4.98"/></proof>
+ <proof prover="3"><result status="valid" time="4.15"/></proof>
  </goal>
  <goal name="mantissa_of_j" proved="true">
  <proof prover="0"><result status="valid" time="0.16" steps="121"/></proof>
@@ -57,7 +57,7 @@
  </goal>
  <goal name="Mantissa_of_xor_j" proved="true">
  <proof prover="3"><result status="valid" time="1.75"/></proof>
- <proof prover="5"><result status="valid" time="3.22"/></proof>
+ <proof prover="5"><result status="valid" time="2.49"/></proof>
  <proof prover="9"><result status="valid" time="0.75"/></proof>
  </goal>
  <goal name="MainResultZero" proved="true">
diff --git a/examples/bitvectors/neg_as_xor/why3shapes.gz b/examples/bitvectors/neg_as_xor/why3shapes.gz
index cb3c9f980dca194c94b6692dc168cbfc36715d29..e71c2e788e4fa3ebb5192ebb7c4af4a8707c37dc 100644
Binary files a/examples/bitvectors/neg_as_xor/why3shapes.gz and b/examples/bitvectors/neg_as_xor/why3shapes.gz differ
diff --git a/examples/bitvectors/power2/why3session.xml b/examples/bitvectors/power2/why3session.xml
index e371b42f971bdeddff13e2b6bebf6dd24ca33e95..99b3b9e859e97c9d34c2f88763adfdd95835f423 100644
--- a/examples/bitvectors/power2/why3session.xml
+++ b/examples/bitvectors/power2/why3session.xml
@@ -583,7 +583,7 @@
  </transf>
  </goal>
  <goal name="Power_sum" proved="true">
- <proof prover="1"><result status="valid" time="1.87"/></proof>
+ <proof prover="1"><result status="valid" time="3.46"/></proof>
  </goal>
  <goal name="Pow2_int_real" proved="true">
  <transf name="introduce_premises" proved="true" >
diff --git a/examples/bitvectors/power2/why3shapes.gz b/examples/bitvectors/power2/why3shapes.gz
index 487e683871678ad4086a5f8f7959206d5e57ead7..6520e427b0002d0fa689033531e8db85087963a9 100644
Binary files a/examples/bitvectors/power2/why3shapes.gz and b/examples/bitvectors/power2/why3shapes.gz differ
diff --git a/examples/bts/71_disambiguation/why3shapes.gz b/examples/bts/71_disambiguation/why3shapes.gz
index 981c6dc90c0c2b7203c3488d1a52e8ae0d990ed2..a8834f871a34a762929c84b43e56e2b6fedeebc7 100644
Binary files a/examples/bts/71_disambiguation/why3shapes.gz and b/examples/bts/71_disambiguation/why3shapes.gz differ
diff --git a/examples/check-builtin/intreal/why3shapes.gz b/examples/check-builtin/intreal/why3shapes.gz
index ed2d743df62c08abb0aee292b2289d882b00329a..6d7c1453d35e224f482c1065b6603375647465f1 100644
Binary files a/examples/check-builtin/intreal/why3shapes.gz and b/examples/check-builtin/intreal/why3shapes.gz differ
diff --git a/examples/check-builtin/real/why3shapes.gz b/examples/check-builtin/real/why3shapes.gz
index 1d89785fe8b984b363085983e8b73a9f5f6bb5e7..ae221128b93815ce78688c05456ec158d4a9caeb 100644
Binary files a/examples/check-builtin/real/why3shapes.gz and b/examples/check-builtin/real/why3shapes.gz differ
diff --git a/examples/foveoos11_challenge1/why3session.xml b/examples/foveoos11_challenge1/why3session.xml
index 3beb04857a906d6f54026a9992f19b880fb2351d..c93383145cbfb8cc60a5ead409b0b77d02c664dc 100644
--- a/examples/foveoos11_challenge1/why3session.xml
+++ b/examples/foveoos11_challenge1/why3session.xml
@@ -1,7 +1,7 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="5">
+<why3session shape_version="6">
 <prover id="1" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
 <file proved="true">
 <path name=".."/>
diff --git a/examples/foveoos11_challenge1/why3shapes.gz b/examples/foveoos11_challenge1/why3shapes.gz
index 0a4c92477848f6e0e5231dfec916568c1d3d94ca..e82cef318a195d8dbd21b76cccc592ec633f2d7b 100644
Binary files a/examples/foveoos11_challenge1/why3shapes.gz and b/examples/foveoos11_challenge1/why3shapes.gz differ
diff --git a/examples/my_cosine/why3shapes.gz b/examples/my_cosine/why3shapes.gz
index 0357417c5c1b7aec2a0e99356f81d14f001ebc95..d6bcc99380b597c7ec63da2cd11f1fc35172c863 100644
Binary files a/examples/my_cosine/why3shapes.gz and b/examples/my_cosine/why3shapes.gz differ
diff --git a/examples/tests-provers/ceil/why3shapes.gz b/examples/tests-provers/ceil/why3shapes.gz
index ed608a559626446255c4457866304d35fee7e7e0..bb2f50cf93dd738fef47d34cefa77e7193c1dd25 100644
Binary files a/examples/tests-provers/ceil/why3shapes.gz and b/examples/tests-provers/ceil/why3shapes.gz differ
diff --git a/examples/tests-provers/coq-interval/why3shapes.gz b/examples/tests-provers/coq-interval/why3shapes.gz
index 5838c92dd8c5b5875eac523a66fdf9579663e406..277f93231e5828dab2c394b882520d075bc448d1 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/tests-provers/ieee_float/why3session.xml b/examples/tests-provers/ieee_float/why3session.xml
index d6ea60b63752efe6d252ee63be7a0f76b2645326..f5f87f4670b3f95da7a1c773a401f925b410fe19 100644
--- a/examples/tests-provers/ieee_float/why3session.xml
+++ b/examples/tests-provers/ieee_float/why3session.xml
@@ -57,7 +57,7 @@
   <proof prover="3"><result status="timeout" time="5.00"/></proof>
   <proof prover="4"><result status="valid" time="1.27"/></proof>
   <proof prover="5"><result status="timeout" time="5.00"/></proof>
-  <proof prover="6"><result status="valid" time="4.15"/></proof>
+  <proof prover="6"><result status="valid" time="2.88"/></proof>
   <proof prover="10"><result status="timeout" time="5.00"/></proof>
   </goal>
   <goal name="VC triplet.4" expl="assertion" proved="true">
@@ -78,7 +78,7 @@
   <proof prover="10"><result status="valid" time="0.08" steps="184"/></proof>
   </goal>
   <goal name="VC triplet.7" expl="assertion" proved="true">
-  <proof prover="6"><result status="valid" time="5.01"/></proof>
+  <proof prover="6"><result status="valid" time="4.01"/></proof>
   <proof prover="7"><result status="timeout" time="5.00"/></proof>
   <proof prover="8"><result status="timeout" time="5.00"/></proof>
   <proof prover="9"><result status="timeout" time="5.00"/></proof>
diff --git a/examples/tests-provers/ieee_float/why3shapes.gz b/examples/tests-provers/ieee_float/why3shapes.gz
index 10e3679803a4a8ef7d6e3fb870543a922dc13912..a9c02674a5f8d8999caca10fe3e86f6dfa9e20d9 100644
Binary files a/examples/tests-provers/ieee_float/why3shapes.gz and b/examples/tests-provers/ieee_float/why3shapes.gz differ
diff --git a/examples/tests-provers/metitarski/why3shapes.gz b/examples/tests-provers/metitarski/why3shapes.gz
index 71da0137d516de56573d04b32c61e83b8648e738..2e13cb95d91b0dabffd6729ec1890335d6b5bb3b 100644
Binary files a/examples/tests-provers/metitarski/why3shapes.gz and b/examples/tests-provers/metitarski/why3shapes.gz differ