diff --git a/examples/binomial_heap/why3session.xml b/examples/binomial_heap/why3session.xml
index a52440e5aea11bd7690fe60ac588afc1ba12e408..3fbebf884a110668b06252d4fd635f222d729c3a 100644
--- a/examples/binomial_heap/why3session.xml
+++ b/examples/binomial_heap/why3session.xml
@@ -179,7 +179,7 @@
  <goal name="VC merge" expl="VC for merge" proved="true">
  <transf name="split_goal_right" proved="true" >
   <goal name="VC merge.0" expl="variant decrease" proved="true">
-  <proof prover="1"><result status="valid" time="0.01" steps="39"/></proof>
+  <proof prover="1"><result status="valid" time="0.01" steps="38"/></proof>
   </goal>
   <goal name="VC merge.1" expl="precondition" proved="true">
   <proof prover="1"><result status="valid" time="0.01" steps="60"/></proof>
@@ -194,7 +194,7 @@
   <proof prover="1"><result status="valid" time="0.01" steps="74"/></proof>
   </goal>
   <goal name="VC merge.5" expl="variant decrease" proved="true">
-  <proof prover="1"><result status="valid" time="0.01" steps="41"/></proof>
+  <proof prover="1"><result status="valid" time="0.01" steps="39"/></proof>
   </goal>
   <goal name="VC merge.6" expl="precondition" proved="true">
   <proof prover="1"><result status="valid" time="0.01" steps="12"/></proof>
diff --git a/examples/binomial_heap/why3shapes.gz b/examples/binomial_heap/why3shapes.gz
index c1adf123bf2c5cfc8e3a7c5c9f3d5bb3a615622a..65e0441946adfe835e73075fea834b5c6f5fd9d1 100644
Binary files a/examples/binomial_heap/why3shapes.gz and b/examples/binomial_heap/why3shapes.gz differ
diff --git a/examples/coincidence_count_list/why3session.xml b/examples/coincidence_count_list/why3session.xml
index 76154de7b5ff4e10def89f0363fc99e85f75729a..1c973191f96af28835e2d2a3f30b2f9f7fb0b4e8 100644
--- a/examples/coincidence_count_list/why3session.xml
+++ b/examples/coincidence_count_list/why3session.xml
@@ -9,7 +9,7 @@
  <proof prover="0"><result status="valid" time="0.00" steps="3"/></proof>
  </goal>
  <goal name="VC coincidence_count" expl="VC for coincidence_count" proved="true">
- <proof prover="0"><result status="valid" time="2.20" steps="9039"/></proof>
+ <proof prover="0"><result status="valid" time="2.20" steps="9025"/></proof>
  </goal>
 </theory>
 <theory name="CoincidenceCountAnyType" proved="true">
@@ -17,7 +17,7 @@
  <proof prover="0"><result status="valid" time="0.00" steps="4"/></proof>
  </goal>
  <goal name="VC coincidence_count" expl="VC for coincidence_count" proved="true">
- <proof prover="0"><result status="valid" time="0.65" steps="4378"/></proof>
+ <proof prover="0"><result status="valid" time="0.65" steps="4363"/></proof>
  </goal>
 </theory>
 <theory name="CoincidenceCountList" proved="true">
@@ -25,7 +25,7 @@
  <proof prover="0"><result status="valid" time="0.00" steps="3"/></proof>
  </goal>
  <goal name="VC coincidence_count" expl="VC for coincidence_count" proved="true">
- <proof prover="0"><result status="valid" time="0.15" steps="1018"/></proof>
+ <proof prover="0"><result status="valid" time="0.15" steps="991"/></proof>
  </goal>
 </theory>
 </file>
diff --git a/examples/coincidence_count_list/why3shapes.gz b/examples/coincidence_count_list/why3shapes.gz
index 39299431cf0dfd6d4a293dc1e429e71f6063038e..5e086b0d518ad9e990f0e907d6a67ec8c5105eb6 100644
Binary files a/examples/coincidence_count_list/why3shapes.gz and b/examples/coincidence_count_list/why3shapes.gz differ
diff --git a/examples/gcd/why3session.xml b/examples/gcd/why3session.xml
index 2584abb9fb645889a97ed72919e6b743d7335f18..3dedb4ed51d8419c8f58a33d649a05d845801506 100644
--- a/examples/gcd/why3session.xml
+++ b/examples/gcd/why3session.xml
@@ -89,7 +89,7 @@
   <proof prover="6"><result status="valid" time="0.01" steps="10"/></proof>
   </goal>
   <goal name="VC binary_gcd.9" expl="variant decrease" proved="true">
-  <proof prover="6"><result status="valid" time="0.02" steps="15"/></proof>
+  <proof prover="6"><result status="valid" time="0.01" steps="15"/></proof>
   </goal>
   <goal name="VC binary_gcd.10" expl="precondition" proved="true">
   <proof prover="6"><result status="valid" time="0.01" steps="15"/></proof>
@@ -110,7 +110,7 @@
   <proof prover="6"><result status="valid" time="0.01" steps="10"/></proof>
   </goal>
   <goal name="VC binary_gcd.16" expl="variant decrease" proved="true">
-  <proof prover="6"><result status="valid" time="0.01" steps="17"/></proof>
+  <proof prover="6"><result status="valid" time="0.02" steps="17"/></proof>
   </goal>
   <goal name="VC binary_gcd.17" expl="precondition" proved="true">
   <proof prover="6"><result status="valid" time="0.01" steps="15"/></proof>
diff --git a/examples/gcd/why3shapes.gz b/examples/gcd/why3shapes.gz
index f8faa78effc6d32c641cfe33163dc0286a6d8d5d..0d6f5d306f62a6c77656f72600109232bed4cef5 100644
Binary files a/examples/gcd/why3shapes.gz and b/examples/gcd/why3shapes.gz differ
diff --git a/examples/gcd_vc_sp/why3session.xml b/examples/gcd_vc_sp/why3session.xml
index 069c0e3ab58516a8e3a71dae174f65a58e83cbff..63f37331165a0dfb751b7c86089b07ffd6194c39 100644
--- a/examples/gcd_vc_sp/why3session.xml
+++ b/examples/gcd_vc_sp/why3session.xml
@@ -75,7 +75,7 @@
   <proof prover="2"><result status="valid" time="0.02"/></proof>
   </goal>
   <goal name="VC binary_gcd.9" expl="variant decrease" proved="true">
-  <proof prover="2"><result status="valid" time="0.05"/></proof>
+  <proof prover="2"><result status="valid" time="0.04"/></proof>
   </goal>
   <goal name="VC binary_gcd.10" expl="precondition" proved="true">
   <proof prover="2"><result status="valid" time="0.04"/></proof>
@@ -96,7 +96,7 @@
   <proof prover="2"><result status="valid" time="0.02"/></proof>
   </goal>
   <goal name="VC binary_gcd.16" expl="variant decrease" proved="true">
-  <proof prover="2"><result status="valid" time="0.04"/></proof>
+  <proof prover="2"><result status="valid" time="0.05"/></proof>
   </goal>
   <goal name="VC binary_gcd.17" expl="precondition" proved="true">
   <proof prover="2"><result status="valid" time="0.03"/></proof>
diff --git a/examples/gcd_vc_sp/why3shapes.gz b/examples/gcd_vc_sp/why3shapes.gz
index 433c08d2322b96ab9568009f2ed43bbe7ca81f19..df6840b412c863c2b163054087787fcc7a8013a9 100644
Binary files a/examples/gcd_vc_sp/why3shapes.gz and b/examples/gcd_vc_sp/why3shapes.gz differ
diff --git a/examples/prover/ISet/why3session.xml b/examples/prover/ISet/why3session.xml
index 0e09d53d0ae29a8f066458bccede5b58e507e0c9..dfa1798afb6f3f4b30657ee25b9c249fb51b3b68 100644
--- a/examples/prover/ISet/why3session.xml
+++ b/examples/prover/ISet/why3session.xml
@@ -74,7 +74,7 @@
   <proof prover="1"><result status="valid" time="0.04" steps="32"/></proof>
   </goal>
   <goal name="VC merge.3" expl="variant decrease" proved="true">
-  <proof prover="1"><result status="valid" time="0.01" steps="21"/></proof>
+  <proof prover="1"><result status="valid" time="0.01" steps="20"/></proof>
   </goal>
   <goal name="VC merge.4" expl="precondition" proved="true">
   <proof prover="1"><result status="valid" time="0.02" steps="15"/></proof>
@@ -86,7 +86,7 @@
   <proof prover="1"><result status="valid" time="0.04" steps="33"/></proof>
   </goal>
   <goal name="VC merge.7" expl="variant decrease" proved="true">
-  <proof prover="1"><result status="valid" time="0.01" steps="23"/></proof>
+  <proof prover="1"><result status="valid" time="0.01" steps="21"/></proof>
   </goal>
   <goal name="VC merge.8" expl="precondition" proved="true">
   <proof prover="1"><result status="valid" time="0.01" steps="8"/></proof>
diff --git a/examples/prover/ISet/why3shapes.gz b/examples/prover/ISet/why3shapes.gz
index 88f42772d6becb45e6a0511b21eda8a1737d1c8e..82bafdd5bd4e00c15d5c38d474d923bfd76632da 100644
Binary files a/examples/prover/ISet/why3shapes.gz and b/examples/prover/ISet/why3shapes.gz differ
diff --git a/examples/verifythis_2016_tree_traversal/why3shapes.gz b/examples/verifythis_2016_tree_traversal/why3shapes.gz
index 101702833ff142c7ec98d413680881cb2e439881..91299536654ca1d64f192069d6f4102e97ef8df1 100644
Binary files a/examples/verifythis_2016_tree_traversal/why3shapes.gz and b/examples/verifythis_2016_tree_traversal/why3shapes.gz differ
diff --git a/examples/vstte12_tree_reconstruction/why3session.xml b/examples/vstte12_tree_reconstruction/why3session.xml
index d79cafc89f145ac2e8ede18bf9332da05928775e..9c702e2b5dd6852693b6771c6a2832e5d3ad412b 100644
--- a/examples/vstte12_tree_reconstruction/why3session.xml
+++ b/examples/vstte12_tree_reconstruction/why3session.xml
@@ -49,7 +49,7 @@
   <proof prover="0"><result status="valid" time="0.01" steps="32"/></proof>
   </goal>
   <goal name="VC build_rec.3" expl="variant decrease" proved="true">
-  <proof prover="0"><result status="valid" time="0.02" steps="9"/></proof>
+  <proof prover="0"><result status="valid" time="0.02" steps="6"/></proof>
   </goal>
   <goal name="VC build_rec.4" expl="variant decrease" proved="true">
   <proof prover="0"><result status="valid" time="0.03" steps="61"/></proof>
diff --git a/examples/vstte12_tree_reconstruction/why3shapes.gz b/examples/vstte12_tree_reconstruction/why3shapes.gz
index cb0ae7766119174c73a087be83079cf6dce02fb7..59310f1712bea86dd7117ddc2c46d9b3e9a63037 100644
Binary files a/examples/vstte12_tree_reconstruction/why3shapes.gz and b/examples/vstte12_tree_reconstruction/why3shapes.gz differ