diff --git a/examples/WP_revisited/blocking_semantics5/why3session.xml b/examples/WP_revisited/blocking_semantics5/why3session.xml
index 9c947c8a272764f753b006c6d59ec5ee38c274e0..b36221e707bcf84f27fda717b3e85d8c09a31263 100644
--- a/examples/WP_revisited/blocking_semantics5/why3session.xml
+++ b/examples/WP_revisited/blocking_semantics5/why3session.xml
@@ -442,7 +442,7 @@
<proof prover="2"><result status="valid" time="0.02" steps="13"/></proof>
</goal>
<goal name="if_rule.0.1" proved="true">
- <proof prover="10" timelimit="10" memlimit="4000"><result status="valid" time="2.72"/></proof>
+ <proof prover="10" timelimit="10" memlimit="4000"><result status="valid" time="3.10"/></proof>
<transf name="inversion_pr" proved="true" >
<goal name="if_rule.0.1.0" proved="true">
<proof prover="10"><result status="valid" time="0.08"/></proof>
diff --git a/examples/avl/priority_queue/why3session.xml b/examples/avl/priority_queue/why3session.xml
index 7e5bd7ba02bb577ab475390760dee7bdcef2b2c0..3c225a7f8dea24f5d38e6c91decf48366cdb007b 100644
--- a/examples/avl/priority_queue/why3session.xml
+++ b/examples/avl/priority_queue/why3session.xml
@@ -507,7 +507,7 @@
<proof prover="4"><result status="valid" time="0.03" steps="67"/></proof>
</goal>
<goal name="VC remove_count.1" expl="postcondition" proved="true">
- <proof prover="1" timelimit="10"><result status="valid" time="4.68"/></proof>
+ <proof prover="1" timelimit="10"><result status="valid" time="5.42"/></proof>
</goal>
<goal name="VC remove_count.2" expl="postcondition" proved="true">
<proof prover="1" timelimit="10"><result status="valid" time="0.47"/></proof>
diff --git a/examples/bitcount/why3session.xml b/examples/bitcount/why3session.xml
index 472499ebd707b01aa8ba931347f943d0f965e0bf..c22eb0a1b2f8f615e925f0a7524895ae8751f348 100644
--- a/examples/bitcount/why3session.xml
+++ b/examples/bitcount/why3session.xml
@@ -683,7 +683,7 @@
<proof prover="6"><result status="valid" time="0.03" steps="79"/></proof>
</goal>
<goal name="VC triangleInequalityInt.0.1" expl="VC for triangleInequalityInt" proved="true">
- <proof prover="0" timelimit="10"><result status="valid" time="4.92"/></proof>
+ <proof prover="0" timelimit="10"><result status="valid" time="5.72"/></proof>
</goal>
</transf>
</goal>
diff --git a/examples/bitvectors/bitvector/why3session.xml b/examples/bitvectors/bitvector/why3session.xml
index 149b29d9d388ab64c3c0e58247362bf4baeba815..5177ea90e60a872f7a745586986f358fd696ed08 100644
--- a/examples/bitvectors/bitvector/why3session.xml
+++ b/examples/bitvectors/bitvector/why3session.xml
@@ -181,7 +181,7 @@
<proof prover="4" timelimit="30"><result status="valid" time="6.45" steps="2706"/></proof>
</goal>
<goal name="to_nat_0x00000003" proved="true">
- <proof prover="6" timelimit="120"><result status="valid" time="53.64"/></proof>
+ <proof prover="6" timelimit="120"><result status="valid" time="68.07"/></proof>
</goal>
<goal name="to_nat_0x00000007" proved="true">
<proof prover="4" timelimit="30"><result status="valid" time="9.99" steps="2976"/></proof>
diff --git a/examples/bitvectors/power2/why3session.xml b/examples/bitvectors/power2/why3session.xml
index 02d9648d3b597b64b8bc5e39967b1327df7c4a3c..a0a6e4a4834363178c00d34d7864b7276a3941b5 100644
--- a/examples/bitvectors/power2/why3session.xml
+++ b/examples/bitvectors/power2/why3session.xml
@@ -581,7 +581,7 @@
</transf>
</goal>
<goal name="Power_sum" proved="true">
- <proof prover="1"><result status="valid" time="3.21"/></proof>
+ <proof prover="1"><result status="valid" time="3.92"/></proof>
</goal>
<goal name="Pow2_int_real" proved="true">
<transf name="introduce_premises" proved="true" >
diff --git a/examples/dijkstra/why3session.xml b/examples/dijkstra/why3session.xml
index 06d3f187c7a4d5bb32440621866c46894059385c..6301bda9a02d37648cbfc07a6660990677232660 100644
--- a/examples/dijkstra/why3session.xml
+++ b/examples/dijkstra/why3session.xml
@@ -108,7 +108,7 @@
<proof prover="7"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC shortest_path_code.6" expl="loop invariant init" proved="true">
- <proof prover="2"><result status="valid" time="3.52"/></proof>
+ <proof prover="2"><result status="valid" time="2.45"/></proof>
<proof prover="5"><result status="valid" time="1.46"/></proof>
</goal>
<goal name="VC shortest_path_code.7" expl="loop invariant init" proved="true">
diff --git a/examples/edit_distance/why3session.xml b/examples/edit_distance/why3session.xml
index 99fd80662358c60eeb8944f2a6df4c6f5abfc665..66d8e2ffd12a070e83972bb0143d59bf08b4c09c 100644
--- a/examples/edit_distance/why3session.xml
+++ b/examples/edit_distance/why3session.xml
@@ -78,7 +78,7 @@
</transf>
</goal>
<goal name="min_dist_diff" proved="true">
- <proof prover="2" edited="edit_distance_Word_min_dist_diff_1.v"><result status="valid" time="0.47"/></proof>
+ <proof prover="2" edited="edit_distance_Word_min_dist_diff_1.v"><result status="valid" time="0.28"/></proof>
</goal>
<goal name="min_dist_eps" proved="true">
<transf name="inline_goal" proved="true" >
@@ -144,10 +144,10 @@
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC distance.5" expl="index in array bounds" proved="true">
- <proof prover="11"><result status="valid" time="0.03"/></proof>
+ <proof prover="11"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC distance.6" expl="index in array bounds" proved="true">
- <proof prover="11"><result status="valid" time="0.02"/></proof>
+ <proof prover="11"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC distance.7" expl="index in array bounds" proved="true">
<proof prover="11"><result status="valid" time="0.03"/></proof>
diff --git a/examples/gcd_bezout/why3session.xml b/examples/gcd_bezout/why3session.xml
index 8aa40b0e6a5f066328904555f17804b9804de076..6a5c7fb3c103d311b6663b0f29706fd8a282e118 100644
--- a/examples/gcd_bezout/why3session.xml
+++ b/examples/gcd_bezout/why3session.xml
@@ -21,10 +21,10 @@
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC gcd.4" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.03"/></proof>
+ <proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC gcd.5" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.04"/></proof>
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC gcd.6" expl="loop variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.06"/></proof>
diff --git a/examples/isqrt_von_neumann/why3session.xml b/examples/isqrt_von_neumann/why3session.xml
index 5de0b32166d599b85f78f67b476d0635a08f0881..9ec4dcd41c03fd2b67b7289f515203e24c4cd145 100644
--- a/examples/isqrt_von_neumann/why3session.xml
+++ b/examples/isqrt_von_neumann/why3session.xml
@@ -587,7 +587,7 @@
<proof prover="4" timelimit="10" memlimit="4000"><result status="valid" time="2.80" steps="571"/></proof>
</goal>
<goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0.1.1.1.0.0.1.0.0.0.0.1.0.0.0.1" proved="true">
- <proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="1.84"/></proof>
+ <proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="2.16"/></proof>
</goal>
</transf>
</goal>
@@ -611,7 +611,7 @@
</transf>
</goal>
<goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0.1.1.1.0.0.1.0.0.1" proved="true">
- <proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="1.87"/></proof>
+ <proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="2.37"/></proof>
</goal>
</transf>
</goal>
@@ -650,7 +650,7 @@
</transf>
</goal>
<goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0.1.1.1.0.0.1.0.1.0.0.1.0.0.0.0.1" proved="true">
- <proof prover="3" timelimit="5"><result status="valid" time="1.86"/></proof>
+ <proof prover="3" timelimit="5"><result status="valid" time="2.32"/></proof>
</goal>
</transf>
</goal>
@@ -674,12 +674,12 @@
</transf>
</goal>
<goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0.1.1.1.0.0.1.0.1.0.1" proved="true">
- <proof prover="3" timelimit="5"><result status="valid" time="1.21"/></proof>
+ <proof prover="3" timelimit="5"><result status="valid" time="1.47"/></proof>
</goal>
</transf>
</goal>
<goal name="VC isqrt64.40.0.0.0.1.0.0.1.0.1.1.0.0.1.1.1.0.0.1.0.1.1" proved="true">
- <proof prover="3" timelimit="5"><result status="valid" time="1.87"/></proof>
+ <proof prover="3" timelimit="5"><result status="valid" time="2.25"/></proof>
</goal>
</transf>
</goal>
diff --git a/examples/koda_ruskey/why3session.xml b/examples/koda_ruskey/why3session.xml
index c022117dc043ffdb07aa2cca360f0fbbb3f5f224..3bf0b82418133a945652c3bca153c1b3fe963ab8 100644
--- a/examples/koda_ruskey/why3session.xml
+++ b/examples/koda_ruskey/why3session.xml
@@ -509,7 +509,7 @@
</transf>
</goal>
<goal name="VC sub_valid_coloring_white.8.1.0.1.0.2" expl="VC for sub_valid_coloring_white" proved="true">
- <proof prover="4" timelimit="10" memlimit="4000"><result status="valid" time="6.68"/></proof>
+ <proof prover="4" timelimit="10" memlimit="4000"><result status="valid" time="7.51"/></proof>
</goal>
</transf>
</goal>
diff --git a/examples/linear_probing/why3session.xml b/examples/linear_probing/why3session.xml
index b4d4d81def91d2df44a0107b7f661972a6568ba1..02e4d0f14c67a4731aecc54aaca5f2dc8bc564c9 100644
--- a/examples/linear_probing/why3session.xml
+++ b/examples/linear_probing/why3session.xml
@@ -19,7 +19,7 @@
<proof prover="6"><result status="valid" time="0.01" steps="13"/></proof>
</goal>
<goal name="NumOfDummy.VC numof_eq" expl="VC for numof_eq" proved="true">
- <proof prover="2"><result status="valid" time="3.49"/></proof>
+ <proof prover="2"><result status="valid" time="3.96"/></proof>
</goal>
<goal name="NumOfDummy.VC dummy_const" expl="VC for dummy_const" proved="true">
<proof prover="6"><result status="valid" time="0.22" steps="356"/></proof>
@@ -346,7 +346,7 @@
</transf>
</goal>
<goal name="VC copy" expl="VC for copy" proved="true">
- <proof prover="2"><result status="valid" time="2.03"/></proof>
+ <proof prover="2"><result status="valid" time="2.38"/></proof>
</goal>
<goal name="VC find_dummy" expl="VC for find_dummy" proved="true">
<proof prover="6"><result status="valid" time="1.02" steps="1301"/></proof>
diff --git a/examples/linked_list_rev/why3session.xml b/examples/linked_list_rev/why3session.xml
index f7d122c13fd38c675dfed267dd0be032dc6cbb83..acd2f2007128b459319346091d7659c87ad28ad5 100644
--- a/examples/linked_list_rev/why3session.xml
+++ b/examples/linked_list_rev/why3session.xml
@@ -378,7 +378,7 @@
</goal>
<goal name="VC list_seg_no_repet.9" expl="assertion" proved="true">
<proof prover="2" timelimit="10"><result status="valid" time="1.27"/></proof>
- <proof prover="4"><result status="valid" time="6.55"/></proof>
+ <proof prover="4"><result status="valid" time="9.06"/></proof>
</goal>
<goal name="VC list_seg_no_repet.10" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.20"/></proof>
diff --git a/examples/logic/ffx/why3session.xml b/examples/logic/ffx/why3session.xml
index 70411066a12f5c112c006757a0aabd755e4e0511..0fc251ef6dc7f44dc245b5c94672768440a208e6 100644
--- a/examples/logic/ffx/why3session.xml
+++ b/examples/logic/ffx/why3session.xml
@@ -65,7 +65,7 @@
<proof prover="4"><result status="valid" time="0.03"/></proof>
<proof prover="5"><result status="unknown" time="0.00"/></proof>
<proof prover="7"><result status="unknown" time="0.00"/></proof>
- <proof prover="8"><result status="valid" time="5.80"/></proof>
+ <proof prover="8"><result status="valid" time="6.80"/></proof>
<proof prover="9"><result status="valid" time="0.04"/></proof>
<proof prover="10"><result status="valid" time="0.00"/></proof>
<proof prover="11"><result status="valid" time="0.01"/></proof>
diff --git a/examples/logic/triangle_inequality/why3session.xml b/examples/logic/triangle_inequality/why3session.xml
index a2ff76eb63720d3fa4b1dab5040bb311b40ca80c..c67ac9a0542cf9c6b5ff0b9fc500e0e5a5fc6aa1 100644
--- a/examples/logic/triangle_inequality/why3session.xml
+++ b/examples/logic/triangle_inequality/why3session.xml
@@ -62,7 +62,7 @@
</goal>
<goal name="CauchySchwarz_aux_non_null" proved="true">
<proof prover="4"><result status="valid" time="0.03"/></proof>
- <proof prover="8" edited="triangle_inequality_CauchySchwarzInequality_CauchySchwarz_aux_non_null_1.v"><result status="valid" time="0.42"/></proof>
+ <proof prover="8" edited="triangle_inequality_CauchySchwarzInequality_CauchySchwarz_aux_non_null_1.v"><result status="valid" time="0.23"/></proof>
</goal>
<goal name="norm_null" proved="true">
<proof prover="4"><result status="valid" time="0.06"/></proof>
diff --git a/examples/mergesort_list/why3session.xml b/examples/mergesort_list/why3session.xml
index b261296f31731cd3ece396f1bcf8f1f6553c5412..85236c8396b427a5b9c7f7c8f0e8d1662804d6fe 100644
--- a/examples/mergesort_list/why3session.xml
+++ b/examples/mergesort_list/why3session.xml
@@ -314,7 +314,7 @@
<proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.48"/></proof>
</goal>
<goal name="VC sort.16.7" expl="postcondition" proved="true">
- <proof prover="0"><result status="valid" time="4.93"/></proof>
+ <proof prover="0"><result status="valid" time="5.66"/></proof>
</goal>
<goal name="VC sort.16.8" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.02" steps="27"/></proof>
diff --git a/examples/multiprecision/add/why3session.xml b/examples/multiprecision/add/why3session.xml
index 69b711d874ca82d46d0846a75d0829dfa5d341b7..990c04d1a5cc3dc99bc5e9f96a6869b57798709b 100644
--- a/examples/multiprecision/add/why3session.xml
+++ b/examples/multiprecision/add/why3session.xml
@@ -857,7 +857,7 @@
<proof prover="5" timelimit="1"><result status="valid" time="0.02" steps="62"/></proof>
</goal>
<goal name="VC wmpn_add_in_place.13" expl="assertion" proved="true">
- <proof prover="0"><result status="valid" time="0.84"/></proof>
+ <proof prover="0"><result status="valid" time="0.65"/></proof>
</goal>
<goal name="VC wmpn_add_in_place.14" expl="precondition" proved="true">
<proof prover="5" memlimit="2000"><result status="valid" time="0.08" steps="38"/></proof>
diff --git a/examples/multiprecision/div/why3session.xml b/examples/multiprecision/div/why3session.xml
index 9e16f22780964fb3bfc6345a5c557c7c75b85ca5..3fb0f74cfe5943750cb793628dbe9f78f0929c62 100644
--- a/examples/multiprecision/div/why3session.xml
+++ b/examples/multiprecision/div/why3session.xml
@@ -3003,7 +3003,7 @@
<goal name="VC submul_limb.22" expl="assertion" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC submul_limb.22.0" expl="VC for submul_limb" proved="true">
- <proof prover="0" timelimit="10"><result status="valid" time="3.80"/></proof>
+ <proof prover="0" timelimit="10"><result status="valid" time="4.32"/></proof>
</goal>
<goal name="VC submul_limb.22.1" expl="VC for submul_limb" proved="true">
<proof prover="0"><result status="valid" time="0.06"/></proof>
@@ -3308,7 +3308,7 @@
<proof prover="5"><result status="valid" time="0.03" steps="94"/></proof>
</goal>
<goal name="VC div_sb_qr.39.1" expl="VC for div_sb_qr" proved="true">
- <proof prover="2" timelimit="5"><result status="valid" time="0.26"/></proof>
+ <proof prover="2" timelimit="5"><result status="valid" time="0.13"/></proof>
</goal>
</transf>
</goal>
@@ -3357,7 +3357,7 @@
<proof prover="1"><result status="valid" time="2.45"/></proof>
</goal>
<goal name="VC div_sb_qr.44.9" expl="VC for div_sb_qr" proved="true">
- <proof prover="1"><result status="valid" time="2.38"/></proof>
+ <proof prover="1"><result status="valid" time="2.72"/></proof>
</goal>
<goal name="VC div_sb_qr.44.10" expl="VC for div_sb_qr" proved="true">
<proof prover="1"><result status="valid" time="0.33"/></proof>
@@ -4220,7 +4220,7 @@
<proof prover="5"><result status="valid" time="0.38" steps="152"/></proof>
</goal>
<goal name="VC div_sb_qr.122.3" expl="VC for div_sb_qr" proved="true">
- <proof prover="5"><result status="valid" time="0.44" steps="158"/></proof>
+ <proof prover="5"><result status="valid" time="0.29" steps="158"/></proof>
</goal>
<goal name="VC div_sb_qr.122.4" expl="VC for div_sb_qr" proved="true">
<proof prover="2"><result status="valid" time="0.32"/></proof>
@@ -4304,7 +4304,7 @@
<goal name="VC div_sb_qr.134.0.0.0" expl="precondition" proved="true">
<transf name="inline_goal" proved="true" >
<goal name="VC div_sb_qr.134.0.0.0.0" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="3.78"/></proof>
+ <proof prover="3"><result status="valid" time="4.32"/></proof>
</goal>
</transf>
</goal>
@@ -4539,7 +4539,7 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC div_sb_qr.157.0.0.0.31" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC div_sb_qr.157.0.0.0.32" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
@@ -4563,7 +4563,7 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC div_sb_qr.157.0.0.0.39" proved="true">
- <proof prover="3"><result status="valid" time="0.03"/></proof>
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC div_sb_qr.157.0.0.0.40" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
@@ -6890,7 +6890,7 @@
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC div_sb_qr.239.0.0.0.86" proved="true">
- <proof prover="3"><result status="valid" time="0.33"/></proof>
+ <proof prover="3"><result status="valid" time="0.18"/></proof>
</goal>
<goal name="VC div_sb_qr.239.0.0.0.87" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof>
@@ -7627,7 +7627,7 @@
<goal name="VC div_sb_qr.271" expl="postcondition" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC div_sb_qr.271.0" expl="postcondition" proved="true">
- <proof prover="5"><result status="valid" time="0.61" steps="157"/></proof>
+ <proof prover="5"><result status="valid" time="0.41" steps="157"/></proof>
</goal>
<goal name="VC div_sb_qr.271.1" expl="postcondition" proved="true">
<proof prover="5"><result status="valid" time="0.20" steps="157"/></proof>
@@ -9473,7 +9473,7 @@
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC div_qr.148" expl="assertion" proved="true">
- <proof prover="0"><result status="valid" time="3.20"/></proof>
+ <proof prover="0"><result status="valid" time="3.64"/></proof>
</goal>
<goal name="VC div_qr.149" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.24"/></proof>
diff --git a/examples/multiprecision/lineardecision/why3session.xml b/examples/multiprecision/lineardecision/why3session.xml
index 4b398b57b96838233b70c4d55303755b59e09b3a..45d419958d772365f78ff66d841ad63deda82c55 100644
--- a/examples/multiprecision/lineardecision/why3session.xml
+++ b/examples/multiprecision/lineardecision/why3session.xml
@@ -149,10 +149,10 @@
<proof prover="4" memlimit="2000"><result status="valid" time="0.00" steps="15"/></proof>
</goal>
<goal name="VC sprod.3" expl="exceptional postcondition" proved="true">
- <proof prover="4" memlimit="2000"><result status="valid" time="0.00" steps="10"/></proof>
+ <proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC sprod.4" expl="exceptional postcondition" proved="true">
- <proof prover="2"><result status="valid" time="0.01"/></proof>
+ <proof prover="4" memlimit="2000"><result status="valid" time="0.00" steps="10"/></proof>
</goal>
</transf>
</goal>
@@ -1296,7 +1296,7 @@
</goal>
<goal name="VC linear_decision.17" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
- <proof prover="4"><result status="valid" time="0.02" steps="32"/></proof>
+ <proof prover="4"><result status="valid" time="0.01" steps="32"/></proof>
</goal>
<goal name="VC linear_decision.18" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="82"/></proof>
@@ -1306,24 +1306,24 @@
</goal>
<goal name="VC linear_decision.20" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
- <proof prover="4"><result status="valid" time="0.01" steps="32"/></proof>
+ <proof prover="4"><result status="valid" time="0.02" steps="32"/></proof>
</goal>
<goal name="VC linear_decision.21" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="82"/></proof>
</goal>
<goal name="VC linear_decision.22" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
+ <proof prover="4"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="VC linear_decision.23" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
+ <proof prover="4"><result status="valid" time="0.02" steps="10"/></proof>
</goal>
<goal name="VC linear_decision.24" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
- <proof prover="4"><result status="valid" time="0.02" steps="10"/></proof>
</goal>
<goal name="VC linear_decision.25" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
- <proof prover="4"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="VC linear_decision.26" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
@@ -1341,10 +1341,10 @@
<proof prover="4"><result status="valid" time="0.02" steps="96"/></proof>
</goal>
<goal name="VC linear_decision.31" expl="integer overflow" proved="true">
- <proof prover="4"><result status="valid" time="0.02" steps="37"/></proof>
+ <proof prover="4"><result status="valid" time="0.03" steps="37"/></proof>
</goal>
<goal name="VC linear_decision.32" expl="variant decrease" proved="true">
- <proof prover="4"><result status="valid" time="0.02" steps="37"/></proof>
+ <proof prover="4"><result status="valid" time="0.01" steps="37"/></proof>
</goal>
<goal name="VC linear_decision.33" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="94"/></proof>
@@ -1357,13 +1357,12 @@
</goal>
<goal name="VC linear_decision.36" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
- <proof prover="4"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="VC linear_decision.37" expl="integer overflow" proved="true">
- <proof prover="4"><result status="valid" time="0.03" steps="37"/></proof>
+ <proof prover="4"><result status="valid" time="0.02" steps="37"/></proof>
</goal>
<goal name="VC linear_decision.38" expl="variant decrease" proved="true">
- <proof prover="4"><result status="valid" time="0.01" steps="37"/></proof>
+ <proof prover="4"><result status="valid" time="0.02" steps="37"/></proof>
</goal>
<goal name="VC linear_decision.39" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="94"/></proof>
@@ -1376,6 +1375,7 @@
</goal>
<goal name="VC linear_decision.42" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
+ <proof prover="4"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="VC linear_decision.43" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
@@ -1406,16 +1406,16 @@
<proof prover="4"><result status="valid" time="0.02" steps="92"/></proof>
</goal>
<goal name="VC linear_decision.52" expl="integer overflow" proved="true">
- <proof prover="4"><result status="valid" time="0.03" steps="35"/></proof>
+ <proof prover="4"><result status="valid" time="0.02" steps="35"/></proof>
</goal>
<goal name="VC linear_decision.53" expl="variant decrease" proved="true">
- <proof prover="4"><result status="valid" time="0.01" steps="35"/></proof>
+ <proof prover="4"><result status="valid" time="0.02" steps="35"/></proof>
</goal>
<goal name="VC linear_decision.54" expl="precondition" proved="true">
- <proof prover="4"><result status="valid" time="0.02" steps="90"/></proof>
+ <proof prover="4"><result status="valid" time="0.03" steps="90"/></proof>
</goal>
<goal name="VC linear_decision.55" expl="precondition" proved="true">
- <proof prover="4"><result status="valid" time="0.02" steps="40"/></proof>
+ <proof prover="4"><result status="valid" time="0.03" steps="40"/></proof>
</goal>
<goal name="VC linear_decision.56" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="37"/></proof>
@@ -1424,16 +1424,16 @@
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC linear_decision.58" expl="integer overflow" proved="true">
- <proof prover="4"><result status="valid" time="0.02" steps="35"/></proof>
+ <proof prover="4"><result status="valid" time="0.03" steps="35"/></proof>
</goal>
<goal name="VC linear_decision.59" expl="variant decrease" proved="true">
- <proof prover="4"><result status="valid" time="0.02" steps="35"/></proof>
+ <proof prover="4"><result status="valid" time="0.01" steps="35"/></proof>
</goal>
<goal name="VC linear_decision.60" expl="precondition" proved="true">
- <proof prover="4"><result status="valid" time="0.03" steps="90"/></proof>
+ <proof prover="4"><result status="valid" time="0.02" steps="90"/></proof>
</goal>
<goal name="VC linear_decision.61" expl="precondition" proved="true">
- <proof prover="4"><result status="valid" time="0.03" steps="40"/></proof>
+ <proof prover="4"><result status="valid" time="0.02" steps="40"/></proof>
</goal>
<goal name="VC linear_decision.62" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="37"/></proof>
@@ -1491,17 +1491,17 @@
</goal>
<goal name="VC linear_decision.80" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
- <proof prover="4"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="VC linear_decision.81" expl="exceptional postcondition" proved="true">
- <proof prover="2"><result status="valid" time="0.01"/></proof>
- <proof prover="4"><result status="valid" time="0.02" steps="10"/></proof>
+ <proof prover="2"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="VC linear_decision.82" expl="exceptional postcondition" proved="true">
- <proof prover="2"><result status="valid" time="0.00"/></proof>
+ <proof prover="2"><result status="valid" time="0.01"/></proof>
+ <proof prover="4"><result status="valid" time="0.02" steps="10"/></proof>
</goal>
<goal name="VC linear_decision.83" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
+ <proof prover="4"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="VC linear_decision.84" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
@@ -1552,16 +1552,16 @@
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC linear_decision.99" expl="exceptional postcondition" proved="true">
- <proof prover="2"><result status="valid" time="0.02"/></proof>
+ <proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC linear_decision.100" expl="exceptional postcondition" proved="true">
- <proof prover="2"><result status="valid" time="0.01"/></proof>
+ <proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC linear_decision.101" expl="exceptional postcondition" proved="true">
- <proof prover="2"><result status="valid" time="0.01"/></proof>
+ <proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC linear_decision.102" expl="exceptional postcondition" proved="true">
- <proof prover="2"><result status="valid" time="0.02"/></proof>
+ <proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
@@ -3097,13 +3097,13 @@
<proof prover="2"><result status="valid" time="0.23"/></proof>
</goal>
<goal name="VC mp_decision.4" expl="exceptional postcondition" proved="true">
- <proof prover="2"><result status="valid" time="0.01"/></proof>
+ <proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC mp_decision.5" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC mp_decision.6" expl="exceptional postcondition" proved="true">
- <proof prover="2"><result status="valid" time="0.02"/></proof>
+ <proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
@@ -3610,7 +3610,7 @@
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC prop_ctx.46" expl="variant decrease" proved="true">
- <proof prover="4"><result status="valid" time="0.20" steps="288"/></proof>
+ <proof prover="4"><result status="valid" time="0.08" steps="288"/></proof>
</goal>
<goal name="VC prop_ctx.47" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.11"/></proof>
@@ -4057,7 +4057,7 @@
<proof prover="2"><result status="valid" time="0.27"/></proof>
</goal>
<goal name="VC prop_ctx.185" expl="postcondition" proved="true">
- <proof prover="2"><result status="valid" time="0.27"/></proof>
+ <proof prover="2"><result status="valid" time="0.14"/></proof>
</goal>
<goal name="VC prop_ctx.186" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
diff --git a/examples/multiprecision/logical/why3session.xml b/examples/multiprecision/logical/why3session.xml
index e8ea734d3a42eb9dd0cf367543f1857f876e94a2..2d50576007a3e0845aec9f0afb4800c97a4039d2 100644
--- a/examples/multiprecision/logical/why3session.xml
+++ b/examples/multiprecision/logical/why3session.xml
@@ -1043,7 +1043,7 @@
<proof prover="0"><result status="valid" time="0.30"/></proof>
</goal>
<goal name="VC wmpn_lshift_in_place.43.1" expl="assertion" proved="true">
- <proof prover="0"><result status="valid" time="0.43"/></proof>
+ <proof prover="0"><result status="valid" time="0.28"/></proof>
</goal>
<goal name="VC wmpn_lshift_in_place.43.2" expl="VC for wmpn_lshift_in_place" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
diff --git a/examples/multiprecision/mul/why3session.xml b/examples/multiprecision/mul/why3session.xml
index c82c6393997d5aef66034ce6d7bc700f7b540aaa..4b4c7984be0ea1a5c8759c773d89cee0a87bcff1 100644
--- a/examples/multiprecision/mul/why3session.xml
+++ b/examples/multiprecision/mul/why3session.xml
@@ -606,7 +606,7 @@
<proof prover="5" timelimit="20"><result status="valid" time="0.02" steps="29"/></proof>
</goal>
<goal name="VC wmpn_addmul_n.3" expl="precondition" proved="true">
- <proof prover="5" timelimit="20"><result status="valid" time="0.12" steps="29"/></proof>
+ <proof prover="5" timelimit="20"><result status="valid" time="0.00" steps="29"/></proof>
</goal>
<goal name="VC wmpn_addmul_n.4" expl="integer overflow" proved="true">
<proof prover="5" timelimit="20"><result status="valid" time="0.04" steps="37"/></proof>
@@ -1153,7 +1153,7 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC wmpn_mul_basecase.41.0.0.0.0.0.0.29" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC wmpn_mul_basecase.41.0.0.0.0.0.0.30" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
@@ -1165,7 +1165,7 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC wmpn_mul_basecase.41.0.0.0.0.0.0.33" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC wmpn_mul_basecase.41.0.0.0.0.0.0.34" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
diff --git a/examples/multiprecision/sub/why3session.xml b/examples/multiprecision/sub/why3session.xml
index 49cad42f72c3d8362bd715b9c4bd1b2b98b3c7da..8613350e7999ad88e24e67052335f79411309ebb 100644
--- a/examples/multiprecision/sub/why3session.xml
+++ b/examples/multiprecision/sub/why3session.xml
@@ -1138,7 +1138,7 @@
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC wmpn_decr.24.2" expl="VC for wmpn_decr" proved="true">
- <proof prover="5" timelimit="1"><result status="valid" time="0.52" steps="76"/></proof>
+ <proof prover="5" timelimit="1"><result status="valid" time="0.68" steps="76"/></proof>
</goal>
<goal name="VC wmpn_decr.24.3" expl="VC for wmpn_decr" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
diff --git a/examples/multiprecision/toom/why3session.xml b/examples/multiprecision/toom/why3session.xml
index aa86e9880e42ece272d88dd6822d6d91a66bdc69..201edcd467fbf1ae84f296a651a81b7d1617eb5b 100644
--- a/examples/multiprecision/toom/why3session.xml
+++ b/examples/multiprecision/toom/why3session.xml
@@ -100,7 +100,7 @@
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC wmpn_toom22_mul.15" expl="integer overflow" proved="true">
- <proof prover="0"><result status="valid" time="3.00"/></proof>
+ <proof prover="0"><result status="valid" time="3.44"/></proof>
</goal>
<goal name="VC wmpn_toom22_mul.16" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof>
@@ -341,7 +341,7 @@
<proof prover="5"><result status="valid" time="0.60" steps="194"/></proof>
</goal>
<goal name="VC wmpn_toom22_mul.81" expl="integer overflow" proved="true">
- <proof prover="4" timelimit="20" memlimit="1000"><result status="valid" time="5.70"/></proof>
+ <proof prover="4" timelimit="20" memlimit="1000"><result status="valid" time="6.50"/></proof>
<proof prover="5" timelimit="20"><result status="valid" time="12.04" steps="380"/></proof>
</goal>
<goal name="VC wmpn_toom22_mul.82" expl="precondition" proved="true">
@@ -1889,7 +1889,7 @@
<goal name="VC wmpn_toom22_mul.319.0.0.0.0.0" expl="precondition" proved="true">
<transf name="apply" proved="true" arg1="H6">
<goal name="VC wmpn_toom22_mul.319.0.0.0.0.0.0" proved="true">
- <proof prover="1" memlimit="2000"><result status="valid" time="0.23"/></proof>
+ <proof prover="1" memlimit="2000"><result status="valid" time="0.10"/></proof>
</goal>
</transf>
</goal>
@@ -2117,10 +2117,10 @@
</transf>
</goal>
<goal name="VC wmpn_toom22_mul.335.3.1" proved="true">
- <proof prover="3"><result status="valid" time="0.04"/></proof>
+ <proof prover="3"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC wmpn_toom22_mul.335.3.2" proved="true">
- <proof prover="3"><result status="valid" time="0.06"/></proof>
+ <proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
</transf>
</goal>
@@ -3296,7 +3296,7 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC wmpn_toom22_mul.353.8" expl="VC for wmpn_toom22_mul" proved="true">
- <proof prover="4"><result status="valid" time="0.48"/></proof>
+ <proof prover="4"><result status="valid" time="0.30"/></proof>
</goal>
<goal name="VC wmpn_toom22_mul.353.9" expl="VC for wmpn_toom22_mul" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
@@ -5041,7 +5041,7 @@
<proof prover="3" timelimit="1"><result status="valid" time="0.16"/></proof>
</goal>
<goal name="VC wmpn_toom32_mul.121.2" expl="VC for wmpn_toom32_mul" proved="true">
- <proof prover="3"><result status="valid" time="0.49"/></proof>
+ <proof prover="3"><result status="valid" time="0.32"/></proof>
</goal>
</transf>
</goal>
@@ -5403,7 +5403,7 @@
<proof prover="1"><result status="valid" time="0.24"/></proof>
</goal>
<goal name="VC wmpn_toom32_mul.188" expl="integer overflow" proved="true">
- <proof prover="1"><result status="valid" time="0.30"/></proof>
+ <proof prover="1"><result status="valid" time="0.16"/></proof>
</goal>
<goal name="VC wmpn_toom32_mul.189" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.12"/></proof>
@@ -5475,7 +5475,7 @@
<proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC wmpn_toom32_mul.197.13" expl="VC for wmpn_toom32_mul" proved="true">
- <proof prover="4"><result status="valid" time="0.33"/></proof>
+ <proof prover="4"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="VC wmpn_toom32_mul.197.14" expl="VC for wmpn_toom32_mul" proved="true">
<proof prover="1"><result status="valid" time="0.06"/></proof>
@@ -5647,13 +5647,13 @@
<proof prover="1"><result status="valid" time="0.17"/></proof>
</goal>
<goal name="VC wmpn_toom32_mul.237" expl="postcondition" proved="true">
- <proof prover="1"><result status="valid" time="0.06"/></proof>
+ <proof prover="1"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="VC wmpn_toom32_mul.238" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC wmpn_toom32_mul.239" expl="postcondition" proved="true">
- <proof prover="1"><result status="valid" time="0.09"/></proof>
+ <proof prover="1"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC wmpn_toom32_mul.240" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
@@ -5905,13 +5905,13 @@
<proof prover="0" timelimit="1"><result status="valid" time="0.24"/></proof>
</goal>
<goal name="VC wmpn_toom32_mul.253.15" expl="VC for wmpn_toom32_mul" proved="true">
- <proof prover="1"><result status="valid" time="0.24"/></proof>
+ <proof prover="1"><result status="valid" time="0.11"/></proof>
</goal>
<goal name="VC wmpn_toom32_mul.253.16" expl="VC for wmpn_toom32_mul" proved="true">
<proof prover="1"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="VC wmpn_toom32_mul.253.17" expl="VC for wmpn_toom32_mul" proved="true">
- <proof prover="1"><result status="valid" time="0.24"/></proof>
+ <proof prover="1"><result status="valid" time="0.11"/></proof>
</goal>
</transf>
</goal>
@@ -6069,7 +6069,7 @@
<proof prover="1"><result status="valid" time="0.11"/></proof>
</goal>
<goal name="VC wmpn_toom32_mul.272.10" expl="VC for wmpn_toom32_mul" proved="true">
- <proof prover="1"><result status="valid" time="0.24"/></proof>
+ <proof prover="1"><result status="valid" time="0.10"/></proof>
</goal>
<goal name="VC wmpn_toom32_mul.272.11" expl="VC for wmpn_toom32_mul" proved="true">
<proof prover="1"><result status="valid" time="0.33"/></proof>
@@ -6725,7 +6725,7 @@
<proof prover="1"><result status="valid" time="0.11"/></proof>
</goal>
<goal name="VC wmpn_toom32_mul.357.5" expl="VC for wmpn_toom32_mul" proved="true">
- <proof prover="1"><result status="valid" time="0.26"/></proof>
+ <proof prover="1"><result status="valid" time="0.13"/></proof>
</goal>
</transf>
</goal>
@@ -6735,10 +6735,10 @@
<proof prover="1"><result status="valid" time="0.23"/></proof>
</goal>
<goal name="VC wmpn_toom32_mul.358.1" expl="VC for wmpn_toom32_mul" proved="true">
- <proof prover="1"><result status="valid" time="0.09"/></proof>
+ <proof prover="1"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="VC wmpn_toom32_mul.358.2" expl="VC for wmpn_toom32_mul" proved="true">
- <proof prover="1"><result status="valid" time="0.08"/></proof>
+ <proof prover="1"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="VC wmpn_toom32_mul.358.3" expl="VC for wmpn_toom32_mul" proved="true">
<proof prover="1"><result status="valid" time="0.09"/></proof>
@@ -6843,7 +6843,7 @@
<proof prover="4"><result status="valid" time="0.32"/></proof>
</goal>
<goal name="VC wmpn_toom32_mul.366" expl="postcondition" proved="true">
- <proof prover="1"><result status="valid" time="0.25"/></proof>
+ <proof prover="1"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="VC wmpn_toom32_mul.367" expl="postcondition" proved="true">
<proof prover="1" timelimit="1"><result status="valid" time="0.06"/></proof>
@@ -7122,7 +7122,7 @@
<proof prover="1" timelimit="1"><result status="valid" time="0.16"/></proof>
</goal>
<goal name="VC wmpn_toom32_mul.421" expl="assertion" proved="true">
- <proof prover="0" timelimit="10"><result status="valid" time="8.46"/></proof>
+ <proof prover="0" timelimit="10"><result status="valid" time="9.63"/></proof>
</goal>
<goal name="VC wmpn_toom32_mul.422" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.04"/></proof>
@@ -7131,7 +7131,7 @@
<proof prover="4"><result status="valid" time="0.26"/></proof>
</goal>
<goal name="VC wmpn_toom32_mul.424" expl="precondition" proved="true">
- <proof prover="1" timelimit="1"><result status="valid" time="0.25"/></proof>
+ <proof prover="1" timelimit="1"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="VC wmpn_toom32_mul.425" expl="precondition" proved="true">
<transf name="inline_goal" proved="true" >
@@ -7472,10 +7472,10 @@
<proof prover="1" timelimit="1"><result status="valid" time="0.16"/></proof>
</goal>
<goal name="VC wmpn_toom32_mul.473.0.0.0.1" proved="true">
- <proof prover="1" timelimit="1"><result status="valid" time="0.26"/></proof>
+ <proof prover="1" timelimit="1"><result status="valid" time="0.15"/></proof>
</goal>
<goal name="VC wmpn_toom32_mul.473.0.0.0.2" proved="true">
- <proof prover="1" timelimit="1"><result status="valid" time="0.28"/></proof>
+ <proof prover="1" timelimit="1"><result status="valid" time="0.26"/></proof>
</goal>
</transf>
</goal>
diff --git a/examples/prover/BacktrackArray/why3session.xml b/examples/prover/BacktrackArray/why3session.xml
index 418da05a7c81e91fbaed92979c8c5644d16e589f..e1864593b9e10c92440595ce09c4b7fd140e1506 100644
--- a/examples/prover/BacktrackArray/why3session.xml
+++ b/examples/prover/BacktrackArray/why3session.xml
@@ -446,7 +446,7 @@
<goal name="VC backtrack.40" expl="postcondition" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="VC backtrack.40.0" expl="postcondition" proved="true">
- <proof prover="0" memlimit="2000"><result status="valid" time="0.78"/></proof>
+ <proof prover="0" memlimit="2000"><result status="valid" time="1.08"/></proof>
</goal>
</transf>
</goal>
diff --git a/examples/prover/Firstorder_formula_impl/why3session.xml b/examples/prover/Firstorder_formula_impl/why3session.xml
index 902cb1e89d41728584297816b7bace96a0ad29c2..b752a3ad5b8f874cafd62a6dfa88fc30472d216e 100644
--- a/examples/prover/Firstorder_formula_impl/why3session.xml
+++ b/examples/prover/Firstorder_formula_impl/why3session.xml
@@ -255,7 +255,7 @@
<proof prover="0"><result status="valid" time="0.14" steps="73"/></proof>
</goal>
<goal name="VC bound_depth_of_fo_term_in_fo_formula_nonnegative.9" expl="precondition" proved="true">
- <proof prover="0"><result status="valid" time="0.16" steps="29"/></proof>
+ <proof prover="0"><result status="valid" time="0.04" steps="29"/></proof>
</goal>
<goal name="VC bound_depth_of_fo_term_in_fo_formula_nonnegative.10" expl="variant decrease" proved="true">
<proof prover="0"><result status="valid" time="0.14" steps="78"/></proof>
@@ -487,7 +487,7 @@
<proof prover="0"><result status="valid" time="0.05" steps="13"/></proof>
</goal>
<goal name="VC bind_var_symbol_in_fo_formula.16" expl="assertion" proved="true">
- <proof prover="0"><result status="valid" time="0.16" steps="13"/></proof>
+ <proof prover="0"><result status="valid" time="0.04" steps="13"/></proof>
</goal>
<goal name="VC bind_var_symbol_in_fo_formula.17" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.11" steps="13"/></proof>
@@ -671,7 +671,7 @@
<proof prover="0"><result status="valid" time="0.08" steps="46"/></proof>
</goal>
<goal name="VC bind_var_fo_term_in_fo_formula.20" expl="precondition" proved="true">
- <proof prover="0"><result status="valid" time="0.18" steps="77"/></proof>
+ <proof prover="0"><result status="valid" time="0.06" steps="77"/></proof>
</goal>
<goal name="VC bind_var_fo_term_in_fo_formula.21" expl="variant decrease" proved="true">
<proof prover="0"><result status="valid" time="0.14" steps="120"/></proof>
@@ -864,7 +864,7 @@
<proof prover="0"><result status="valid" time="0.14" steps="20"/></proof>
</goal>
<goal name="VC unbind_var_symbol_in_fo_formula.32" expl="precondition" proved="true">
- <proof prover="0"><result status="valid" time="0.17" steps="70"/></proof>
+ <proof prover="0"><result status="valid" time="0.05" steps="70"/></proof>
</goal>
<goal name="VC unbind_var_symbol_in_fo_formula.33" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.16" steps="98"/></proof>
@@ -918,7 +918,7 @@
<proof prover="0"><result status="valid" time="0.14" steps="20"/></proof>
</goal>
<goal name="VC unbind_var_symbol_in_fo_formula.50" expl="precondition" proved="true">
- <proof prover="0"><result status="valid" time="0.16" steps="70"/></proof>
+ <proof prover="0"><result status="valid" time="0.04" steps="70"/></proof>
</goal>
<goal name="VC unbind_var_symbol_in_fo_formula.51" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.10" steps="98"/></proof>
@@ -1219,7 +1219,7 @@
<proof prover="0"><result status="valid" time="0.15" steps="19"/></proof>
</goal>
<goal name="VC unbind_var_fo_term_in_fo_formula.66" expl="precondition" proved="true">
- <proof prover="0"><result status="valid" time="0.17" steps="20"/></proof>
+ <proof prover="0"><result status="valid" time="0.05" steps="20"/></proof>
</goal>
<goal name="VC unbind_var_fo_term_in_fo_formula.67" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.13" steps="20"/></proof>
@@ -1258,7 +1258,7 @@
<proof prover="0"><result status="valid" time="0.13" steps="20"/></proof>
</goal>
<goal name="VC unbind_var_fo_term_in_fo_formula.79" expl="precondition" proved="true">
- <proof prover="0"><result status="valid" time="0.16" steps="20"/></proof>
+ <proof prover="0"><result status="valid" time="0.04" steps="20"/></proof>
</goal>
<goal name="VC unbind_var_fo_term_in_fo_formula.80" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.12" steps="20"/></proof>
@@ -1292,7 +1292,7 @@
<proof prover="0" timelimit="5"><result status="valid" time="0.15" steps="14"/></proof>
</goal>
<goal name="VC subst_base_symbol_in_fo_formula.3" expl="variant decrease" proved="true">
- <proof prover="0" timelimit="5"><result status="valid" time="0.17" steps="22"/></proof>
+ <proof prover="0" timelimit="5"><result status="valid" time="0.05" steps="22"/></proof>
</goal>
<goal name="VC subst_base_symbol_in_fo_formula.4" expl="precondition" proved="true">
<proof prover="0" timelimit="5"><result status="valid" time="0.05" steps="15"/></proof>
@@ -1485,7 +1485,7 @@
<proof prover="0" timelimit="5"><result status="valid" time="0.14" steps="13"/></proof>
</goal>
<goal name="VC subst_base_fo_term_in_fo_formula.1" expl="assertion" proved="true">
- <proof prover="0" timelimit="5"><result status="valid" time="0.17" steps="65"/></proof>
+ <proof prover="0" timelimit="5"><result status="valid" time="0.05" steps="65"/></proof>
</goal>
<goal name="VC subst_base_fo_term_in_fo_formula.2" expl="assertion" proved="true">
<proof prover="0" timelimit="5"><result status="valid" time="0.14" steps="15"/></proof>
@@ -2303,7 +2303,7 @@
<proof prover="0" timelimit="5"><result status="valid" time="0.10" steps="138"/></proof>
</goal>
<goal name="VC destruct_fo_formula.19.3" expl="assertion" proved="true">
- <proof prover="0" timelimit="5"><result status="valid" time="0.18" steps="38"/></proof>
+ <proof prover="0" timelimit="5"><result status="valid" time="0.06" steps="38"/></proof>
</goal>
<goal name="VC destruct_fo_formula.19.4" expl="assertion" proved="true">
<proof prover="0" timelimit="5"><result status="valid" time="0.10" steps="146"/></proof>
@@ -2334,7 +2334,7 @@
<proof prover="0" timelimit="5"><result status="valid" time="0.17" steps="38"/></proof>
</goal>
<goal name="VC destruct_fo_formula.23.4" expl="assertion" proved="true">
- <proof prover="0" timelimit="5"><result status="valid" time="0.19" steps="132"/></proof>
+ <proof prover="0" timelimit="5"><result status="valid" time="0.06" steps="132"/></proof>
</goal>
<goal name="VC destruct_fo_formula.23.5" expl="assertion" proved="true">
<proof prover="0" timelimit="5"><result status="valid" time="0.28" steps="662"/></proof>
@@ -2814,7 +2814,7 @@
<proof prover="0"><result status="valid" time="0.05" steps="21"/></proof>
</goal>
<goal name="VC destruct_fo_formula.166" expl="unreachable point" proved="true">
- <proof prover="0"><result status="valid" time="0.17" steps="21"/></proof>
+ <proof prover="0"><result status="valid" time="0.05" steps="21"/></proof>
</goal>
<goal name="VC destruct_fo_formula.167" expl="unreachable point" proved="true">
<proof prover="0"><result status="valid" time="0.08" steps="23"/></proof>
diff --git a/examples/prover/Firstorder_formula_list_impl/why3session.xml b/examples/prover/Firstorder_formula_list_impl/why3session.xml
index a7a028f66938083cd68f38a7bb28fff525b4f187..df6114663a9a794dfcc9cf46e033deea40544ba2 100644
--- a/examples/prover/Firstorder_formula_list_impl/why3session.xml
+++ b/examples/prover/Firstorder_formula_list_impl/why3session.xml
@@ -526,7 +526,7 @@
<proof prover="0"><result status="valid" time="0.16" steps="18"/></proof>
</goal>
<goal name="VC construct_fo_formula_list.24" expl="assertion" proved="true">
- <proof prover="1"><result status="valid" time="0.26"/></proof>
+ <proof prover="1"><result status="valid" time="0.13"/></proof>
</goal>
<goal name="VC construct_fo_formula_list.25" expl="precondition" proved="true">
<proof prover="0" timelimit="1"><result status="valid" time="0.11" steps="8"/></proof>
diff --git a/examples/prover/Firstorder_tableau_impl/why3session.xml b/examples/prover/Firstorder_tableau_impl/why3session.xml
index ca40cec589fb298b335cc638a2acdccaf7c4c9e9..1ac95fd67f1f8efcd155dbcffb8d848e61ec0f6d 100644
--- a/examples/prover/Firstorder_tableau_impl/why3session.xml
+++ b/examples/prover/Firstorder_tableau_impl/why3session.xml
@@ -166,10 +166,10 @@
<proof prover="1"><result status="valid" time="0.18" steps="41"/></proof>
</goal>
<goal name="VC construct_tableau.7" expl="postcondition" proved="true">
- <proof prover="1"><result status="valid" time="0.19" steps="45"/></proof>
+ <proof prover="1"><result status="valid" time="0.07" steps="45"/></proof>
</goal>
<goal name="VC construct_tableau.8" expl="postcondition" proved="true">
- <proof prover="1"><result status="valid" time="0.07" steps="45"/></proof>
+ <proof prover="1"><result status="valid" time="0.19" steps="45"/></proof>
</goal>
<goal name="VC construct_tableau.9" expl="assertion" proved="true">
<proof prover="1"><result status="valid" time="0.15" steps="90"/></proof>
@@ -341,7 +341,7 @@
<proof prover="1"><result status="valid" time="0.08" steps="87"/></proof>
</goal>
<goal name="VC destruct_tableau.18" expl="assertion" proved="true">
- <proof prover="1"><result status="valid" time="0.19" steps="35"/></proof>
+ <proof prover="1"><result status="valid" time="0.07" steps="35"/></proof>
</goal>
<goal name="VC destruct_tableau.19" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.18" steps="22"/></proof>
@@ -525,7 +525,7 @@
<proof prover="1"><result status="valid" time="0.06" steps="14"/></proof>
</goal>
<goal name="VC nlsubst_fo_term_in_tableau.5" expl="postcondition" proved="true">
- <proof prover="1"><result status="valid" time="0.18" steps="31"/></proof>
+ <proof prover="1"><result status="valid" time="0.06" steps="31"/></proof>
</goal>
<goal name="VC nlsubst_fo_term_in_tableau.6" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.18" steps="33"/></proof>
diff --git a/examples/prover/FormulaTransformations/why3session.xml b/examples/prover/FormulaTransformations/why3session.xml
index 4edde8afc8e3adf06108c97c5118dac68dcdac0d..84998d4ba7ff2becad29dd83fb9270e1455d040f 100644
--- a/examples/prover/FormulaTransformations/why3session.xml
+++ b/examples/prover/FormulaTransformations/why3session.xml
@@ -322,7 +322,7 @@
<proof prover="4"><result status="valid" time="0.09" steps="17"/></proof>
</goal>
<goal name="VC smart_or.4" expl="assertion" proved="true">
- <proof prover="4"><result status="valid" time="0.27" steps="655"/></proof>
+ <proof prover="4"><result status="valid" time="0.14" steps="655"/></proof>
</goal>
<goal name="VC smart_or.5" expl="assertion" proved="true">
<proof prover="4"><result status="valid" time="0.18" steps="662"/></proof>
@@ -1213,7 +1213,7 @@
<proof prover="4"><result status="valid" time="0.09" steps="27"/></proof>
</goal>
<goal name="VC nnf_simpl_list.23" expl="postcondition" proved="true">
- <proof prover="4"><result status="valid" time="0.23" steps="138"/></proof>
+ <proof prover="4"><result status="valid" time="0.10" steps="138"/></proof>
</goal>
<goal name="VC nnf_simpl_list.24" expl="postcondition" proved="true">
<proof prover="4"><result status="valid" time="0.15" steps="405"/></proof>
@@ -1293,7 +1293,7 @@
<proof prover="4"><result status="valid" time="0.08" steps="16"/></proof>
</goal>
<goal name="VC term_list_free_vars.8" expl="precondition" proved="true">
- <proof prover="4"><result status="valid" time="0.20" steps="16"/></proof>
+ <proof prover="4"><result status="valid" time="0.08" steps="16"/></proof>
</goal>
<goal name="VC term_list_free_vars.9" expl="postcondition" proved="true">
<proof prover="4"><result status="valid" time="0.10" steps="133"/></proof>
@@ -1309,7 +1309,7 @@
<goal name="VC skolem_parameters" expl="VC for skolem_parameters" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC skolem_parameters.0" expl="precondition" proved="true">
- <proof prover="4"><result status="valid" time="0.20" steps="23"/></proof>
+ <proof prover="4"><result status="valid" time="0.08" steps="23"/></proof>
</goal>
<goal name="VC skolem_parameters.1" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.09" steps="39"/></proof>
@@ -1386,7 +1386,7 @@
<proof prover="4"><result status="valid" time="0.11" steps="72"/></proof>
</goal>
<goal name="VC skolemize.7" expl="precondition" proved="true">
- <proof prover="4"><result status="valid" time="0.24" steps="120"/></proof>
+ <proof prover="4"><result status="valid" time="0.11" steps="120"/></proof>
</goal>
<goal name="VC skolemize.8" expl="unreachable point" proved="true">
<proof prover="4"><result status="valid" time="0.21" steps="826"/></proof>
@@ -1673,7 +1673,7 @@
<proof prover="4"><result status="valid" time="0.08" steps="26"/></proof>
</goal>
<goal name="VC skolemize.73" expl="assertion" proved="true">
- <proof prover="3"><result status="valid" time="0.78"/></proof>
+ <proof prover="3"><result status="valid" time="0.60"/></proof>
</goal>
<goal name="VC skolemize.74" expl="assertion" proved="true">
<transf name="split_goal_right" proved="true" >
@@ -1926,7 +1926,7 @@
<proof prover="4"><result status="valid" time="0.17" steps="179"/></proof>
</goal>
<goal name="VC skolemize.116.4" expl="assertion" proved="true">
- <proof prover="2"><result status="valid" time="3.16"/></proof>
+ <proof prover="2"><result status="valid" time="3.60"/></proof>
</goal>
<goal name="VC skolemize.116.5" expl="assertion" proved="true">
<proof prover="4"><result status="valid" time="0.34" steps="816"/></proof>
@@ -1967,7 +1967,7 @@
<proof prover="4"><result status="valid" time="0.15" steps="96"/></proof>
</goal>
<goal name="VC skolemize.118.1" expl="assertion" proved="true">
- <proof prover="4"><result status="valid" time="0.24" steps="103"/></proof>
+ <proof prover="4"><result status="valid" time="0.11" steps="103"/></proof>
</goal>
<goal name="VC skolemize.118.2" expl="assertion" proved="true">
<proof prover="4"><result status="valid" time="0.15" steps="96"/></proof>
@@ -2674,7 +2674,7 @@
<proof prover="4"><result status="valid" time="0.09" steps="142"/></proof>
</goal>
<goal name="VC preprocessing.11" expl="precondition" proved="true">
- <proof prover="4"><result status="valid" time="0.22" steps="163"/></proof>
+ <proof prover="4"><result status="valid" time="0.09" steps="163"/></proof>
</goal>
<goal name="VC preprocessing.12" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.10" steps="147"/></proof>
diff --git a/examples/prover/Prover/why3session.xml b/examples/prover/Prover/why3session.xml
index 999c620364b23bbdfb7904750f4c6d44073f6aab..fd5d4832ed54b6ae1ef99838af17ffd7390c24c5 100644
--- a/examples/prover/Prover/why3session.xml
+++ b/examples/prover/Prover/why3session.xml
@@ -1198,7 +1198,7 @@
<proof prover="2" timelimit="5"><result status="valid" time="0.16" steps="92"/></proof>
</goal>
<goal name="VC decompose.99" expl="precondition" proved="true">
- <proof prover="2" timelimit="5"><result status="valid" time="0.24" steps="88"/></proof>
+ <proof prover="2" timelimit="5"><result status="valid" time="0.11" steps="88"/></proof>
</goal>
<goal name="VC decompose.100" expl="precondition" proved="true">
<proof prover="2" timelimit="5"><result status="valid" time="0.24" steps="140"/></proof>
@@ -1239,7 +1239,7 @@
<proof prover="2" timelimit="5"><result status="valid" time="0.25" steps="265"/></proof>
</goal>
<goal name="VC decompose.107.5" expl="assertion" proved="true">
- <proof prover="6" timelimit="20"><result status="valid" time="5.07"/></proof>
+ <proof prover="6" timelimit="20"><result status="valid" time="5.72"/></proof>
</goal>
</transf>
</goal>
@@ -3343,7 +3343,7 @@
<proof prover="2"><result status="valid" time="0.12" steps="60"/></proof>
</goal>
<goal name="VC contradiction_neg_atom.117" expl="precondition" proved="true">
- <proof prover="2"><result status="valid" time="0.28" steps="277"/></proof>
+ <proof prover="2"><result status="valid" time="0.15" steps="277"/></proof>
</goal>
<goal name="VC contradiction_neg_atom.118" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.15" steps="60"/></proof>
@@ -3407,7 +3407,7 @@
<proof prover="2"><result status="valid" time="0.12" steps="69"/></proof>
</goal>
<goal name="VC contradiction_neg_atom.133.0.4" expl="VC for contradiction_neg_atom" proved="true">
- <proof prover="1"><result status="valid" time="2.80"/></proof>
+ <proof prover="1"><result status="valid" time="3.22"/></proof>
</goal>
<goal name="VC contradiction_neg_atom.133.0.5" expl="VC for contradiction_neg_atom" proved="true">
<proof prover="1"><result status="valid" time="1.86"/></proof>
diff --git a/examples/prover/Unification/why3session.xml b/examples/prover/Unification/why3session.xml
index 7c353f68b5a4e16b4fab7017e1e6bbf9eba27df3..fd8a3f36d23536e829b69b501dbdb53768a3b131 100644
--- a/examples/prover/Unification/why3session.xml
+++ b/examples/prover/Unification/why3session.xml
@@ -1110,7 +1110,7 @@
<proof prover="6"><result status="valid" time="0.46"/></proof>
</goal>
<goal name="VC unification_term.131" expl="postcondition" proved="true">
- <proof prover="12"><result status="valid" time="0.16" steps="61"/></proof>
+ <proof prover="12"><result status="valid" time="0.04" steps="61"/></proof>
</goal>
<goal name="VC unification_term.132" expl="postcondition" proved="true">
<proof prover="12"><result status="valid" time="0.10" steps="38"/></proof>
@@ -1134,7 +1134,7 @@
<proof prover="12"><result status="valid" time="0.10" steps="22"/></proof>
</goal>
<goal name="VC unification_term.139" expl="precondition" proved="true">
- <proof prover="1"><result status="valid" time="2.79"/></proof>
+ <proof prover="1"><result status="valid" time="3.25"/></proof>
</goal>
<goal name="VC unification_term.140" expl="assertion" proved="true">
<proof prover="12"><result status="valid" time="0.14" steps="102"/></proof>
@@ -1180,7 +1180,7 @@
<proof prover="12"><result status="valid" time="0.09" steps="84"/></proof>
</goal>
<goal name="VC unification_term.154" expl="postcondition" proved="true">
- <proof prover="12"><result status="valid" time="0.16" steps="66"/></proof>
+ <proof prover="12"><result status="valid" time="0.04" steps="66"/></proof>
</goal>
<goal name="VC unification_term.155" expl="postcondition" proved="true">
<proof prover="12"><result status="valid" time="0.09" steps="42"/></proof>
@@ -1453,7 +1453,7 @@
<proof prover="12"><result status="valid" time="0.12" steps="19"/></proof>
</goal>
<goal name="VC unification_term.244" expl="precondition" proved="true">
- <proof prover="1"><result status="valid" time="2.76"/></proof>
+ <proof prover="1"><result status="valid" time="3.15"/></proof>
</goal>
<goal name="VC unification_term.245" expl="assertion" proved="true">
<proof prover="6"><result status="valid" time="0.42"/></proof>
@@ -1570,7 +1570,7 @@
<proof prover="12"><result status="valid" time="0.11" steps="24"/></proof>
</goal>
<goal name="VC unification_term.283" expl="precondition" proved="true">
- <proof prover="1"><result status="valid" time="3.16"/></proof>
+ <proof prover="1"><result status="valid" time="3.60"/></proof>
</goal>
<goal name="VC unification_term.284" expl="precondition" proved="true">
<proof prover="12"><result status="valid" time="0.10" steps="21"/></proof>
@@ -2140,7 +2140,7 @@
<goal name="VC conflict.16" expl="assertion" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC conflict.16.0" expl="VC for conflict" proved="true">
- <proof prover="1"><result status="valid" time="2.62"/></proof>
+ <proof prover="1"><result status="valid" time="3.06"/></proof>
</goal>
<goal name="VC conflict.16.1" expl="VC for conflict" proved="true">
<proof prover="12"><result status="valid" time="0.08" steps="62"/></proof>
diff --git a/examples/queens_bv/why3session.xml b/examples/queens_bv/why3session.xml
index f1616cb3d41ce35806bae30d45b16fff8ac0ae86..2ac059e74031797c63a56c2c982b076230be379e 100644
--- a/examples/queens_bv/why3session.xml
+++ b/examples/queens_bv/why3session.xml
@@ -231,7 +231,7 @@
<proof prover="3"><result status="valid" time="1.62"/></proof>
</goal>
<goal name="VC t.33" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="1.76"/></proof>
+ <proof prover="3"><result status="valid" time="2.04"/></proof>
</goal>
<goal name="VC t.34" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="2.42"/></proof>
@@ -277,7 +277,7 @@
<proof prover="10" timelimit="1"><result status="valid" time="0.08" steps="174"/></proof>
</goal>
<goal name="VC t.45.1" expl="loop invariant preservation" proved="true">
- <proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="8.33"/></proof>
+ <proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="10.17"/></proof>
</goal>
<goal name="VC t.45.2" expl="loop invariant preservation" proved="true">
<proof prover="3" timelimit="1"><result status="valid" time="0.62"/></proof>
@@ -296,8 +296,8 @@
<proof prover="3"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="VC t.46.2" expl="loop invariant preservation" proved="true">
- <proof prover="3" timelimit="60"><result status="valid" time="17.31"/></proof>
- <proof prover="6" timelimit="60"><result status="valid" time="13.21"/></proof>
+ <proof prover="3" timelimit="60"><result status="valid" time="20.80"/></proof>
+ <proof prover="6" timelimit="60"><result status="valid" time="14.69"/></proof>
</goal>
</transf>
</goal>
diff --git a/examples/tests-provers/ieee_float/why3session.xml b/examples/tests-provers/ieee_float/why3session.xml
index 88a8d2ae9e91f9ef37a8c967d87d16c8fd320594..fbdca81d384f72992dfa48b8c9ac1fc02f5fe9c7 100644
--- a/examples/tests-provers/ieee_float/why3session.xml
+++ b/examples/tests-provers/ieee_float/why3session.xml
@@ -76,7 +76,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="3.82"/></proof>
+ <proof prover="6"><result status="valid" time="4.36"/></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/verifythis_2016_matrix_multiplication/strassen/why3session.xml b/examples/verifythis_2016_matrix_multiplication/strassen/why3session.xml
index 02617ec5b269435b5bc1ac2651e45683e9e32eef..7cc3ebf48b3ae718f27dbe6423d4f13bb0e13ec9 100644
--- a/examples/verifythis_2016_matrix_multiplication/strassen/why3session.xml
+++ b/examples/verifythis_2016_matrix_multiplication/strassen/why3session.xml
@@ -219,7 +219,7 @@
<proof prover="2"><result status="valid" time="1.64"/></proof>
</goal>
<goal name="VC padding.6" expl="assertion" proved="true">
- <proof prover="2" timelimit="20"><result status="valid" time="10.38"/></proof>
+ <proof prover="2" timelimit="20"><result status="valid" time="1.67"/></proof>
</goal>
<goal name="VC padding.7" expl="assertion" proved="true">
<proof prover="1" timelimit="5"><result status="valid" time="0.78" steps="919"/></proof>
@@ -262,10 +262,10 @@
<proof prover="1"><result status="valid" time="0.03" steps="14"/></proof>
</goal>
<goal name="VC strassen.6" expl="precondition" proved="true">
- <proof prover="1"><result status="valid" time="0.03" steps="12"/></proof>
+ <proof prover="1"><result status="valid" time="0.04" steps="12"/></proof>
</goal>
<goal name="VC strassen.7" expl="precondition" proved="true">
- <proof prover="1"><result status="valid" time="0.04" steps="12"/></proof>
+ <proof prover="1"><result status="valid" time="0.03" steps="12"/></proof>
</goal>
<goal name="VC strassen.8" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.04" steps="12"/></proof>
@@ -658,7 +658,7 @@
<goal name="VC strassen.124.0.0" expl="precondition" proved="true">
<transf name="compute_specified" proved="true" >
<goal name="VC strassen.124.0.0.0" expl="precondition" proved="true">
- <proof prover="1"><result status="valid" time="0.24" steps="206"/></proof>
+ <proof prover="1"><result status="valid" time="0.11" steps="206"/></proof>
</goal>
</transf>
</goal>
diff --git a/examples/verifythis_fm2012_treedel/why3session.xml b/examples/verifythis_fm2012_treedel/why3session.xml
index 067428e35a8d7aeabdaa47e78b8b952960ee8548..54874172b3d60cc4807a78d0926bccc8a42ad3ec 100644
--- a/examples/verifythis_fm2012_treedel/why3session.xml
+++ b/examples/verifythis_fm2012_treedel/why3session.xml
@@ -173,10 +173,10 @@
<proof prover="6"><result status="valid" time="0.01" steps="5"/></proof>
</goal>
<goal name="VC search_tree_delete_min.1" expl="precondition" proved="true">
- <proof prover="6"><result status="valid" time="0.01" steps="7"/></proof>
+ <proof prover="6"><result status="valid" time="0.00" steps="7"/></proof>
</goal>
<goal name="VC search_tree_delete_min.2" expl="precondition" proved="true">
- <proof prover="6"><result status="valid" time="0.00" steps="7"/></proof>
+ <proof prover="6"><result status="valid" time="0.01" steps="7"/></proof>
</goal>
<goal name="VC search_tree_delete_min.3" expl="unreachable point" proved="true">
<proof prover="6"><result status="valid" time="0.00" steps="13"/></proof>
diff --git a/examples/vstte10_queens/why3session.xml b/examples/vstte10_queens/why3session.xml
index f5734965bd44ffaf03c743a490f1b36a64e9b43f..4fc72fc4943f0a534d146606c11124b4faf48d43 100644
--- a/examples/vstte10_queens/why3session.xml
+++ b/examples/vstte10_queens/why3session.xml
@@ -49,7 +49,7 @@
<proof prover="4"><result status="valid" time="0.01" steps="15"/></proof>
</goal>
<goal name="VC bt_queens.6" expl="precondition" proved="true">
- <proof prover="3" timelimit="5"><result status="valid" time="0.04"/></proof>
+ <proof prover="3" timelimit="5"><result status="valid" time="0.16"/></proof>
</goal>
<goal name="VC bt_queens.7" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.08"/></proof>