diff --git a/examples/multiprecision/compare/why3shapes.gz b/examples/multiprecision/compare/why3shapes.gz
index 5b1e8fe46d1e6864980e3e62a3dfd328832421e8..e0961f344dcc58b512111b8811897d8b51c779d9 100644
Binary files a/examples/multiprecision/compare/why3shapes.gz and b/examples/multiprecision/compare/why3shapes.gz differ
diff --git a/examples/multiprecision/lineardecision/why3session.xml b/examples/multiprecision/lineardecision/why3session.xml
index 0b34eec4c3d01ba8e7731887b45563ba71672fdd..b36d2da7f07b82c195621df2efb49841062bf254 100644
--- a/examples/multiprecision/lineardecision/why3session.xml
+++ b/examples/multiprecision/lineardecision/why3session.xml
@@ -168,10 +168,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="2"><result status="valid" time="0.01"/></proof>
+ <proof prover="4" memlimit="2000"><result status="valid" time="0.00" steps="10"/></proof>
</goal>
<goal name="VC sprod.4" 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>
</transf>
</goal>
@@ -278,7 +278,7 @@
<proof prover="4" memlimit="2000"><result status="valid" time="0.22" steps="440"/></proof>
</goal>
<goal name="VC v_append.8" expl="loop invariant preservation" proved="true">
- <proof prover="4" memlimit="2000"><result status="valid" time="0.01" steps="177"/></proof>
+ <proof prover="4" memlimit="2000"><result status="valid" time="0.14" steps="177"/></proof>
</goal>
<goal name="VC v_append.9" expl="postcondition" proved="true">
<proof prover="4" memlimit="2000"><result status="valid" time="0.01" steps="17"/></proof>
@@ -601,7 +601,7 @@
<proof prover="3" memlimit="1000"><result status="valid" time="0.46"/></proof>
</goal>
<goal name="VC add_expr.4.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.26"/></proof>
+ <proof prover="3"><result status="valid" time="0.39"/></proof>
</goal>
</transf>
</goal>
@@ -683,7 +683,7 @@
<proof prover="4"><result status="valid" time="0.02" steps="66"/></proof>
</goal>
<goal name="VC add_expr.21" expl="postcondition" proved="true">
- <proof prover="4"><result status="valid" time="0.20" steps="268"/></proof>
+ <proof prover="4"><result status="valid" time="0.34" steps="268"/></proof>
</goal>
<goal name="VC add_expr.22" expl="variant decrease" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
@@ -967,7 +967,7 @@
<proof prover="4"><result status="valid" time="0.02" steps="10"/></proof>
</goal>
<goal name="VC check_combination.18" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.24"/></proof>
+ <proof prover="3"><result status="valid" time="1.67"/></proof>
</goal>
<goal name="VC check_combination.19" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
@@ -1315,7 +1315,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.01" steps="32"/></proof>
+ <proof prover="4"><result status="valid" time="0.02" 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>
@@ -1325,24 +1325,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.02" steps="32"/></proof>
+ <proof prover="4"><result status="valid" time="0.01" 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>
@@ -1360,10 +1360,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.03" steps="37"/></proof>
+ <proof prover="4"><result status="valid" time="0.02" steps="37"/></proof>
</goal>
<goal name="VC linear_decision.32" 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.33" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="94"/></proof>
@@ -1376,12 +1376,13 @@
</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.02" steps="37"/></proof>
+ <proof prover="4"><result status="valid" time="0.03" steps="37"/></proof>
</goal>
<goal name="VC linear_decision.38" 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.39" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="94"/></proof>
@@ -1394,7 +1395,6 @@
</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>
@@ -1425,16 +1425,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.02" steps="35"/></proof>
+ <proof prover="4"><result status="valid" time="0.03" steps="35"/></proof>
</goal>
<goal name="VC linear_decision.53" 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.54" 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.55" 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.56" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="37"/></proof>
@@ -1443,16 +1443,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.03" steps="35"/></proof>
+ <proof prover="4"><result status="valid" time="0.02" steps="35"/></proof>
</goal>
<goal name="VC linear_decision.59" 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.60" 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.61" 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.62" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="37"/></proof>
@@ -1510,17 +1510,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.00"/></proof>
- </goal>
- <goal name="VC linear_decision.82" 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.82" expl="exceptional postcondition" proved="true">
+ <proof prover="2"><result status="valid" time="0.00"/></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>
@@ -1571,16 +1571,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.01"/></proof>
+ <proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC linear_decision.100" 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.101" 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.102" 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>
</transf>
</goal>
@@ -1703,7 +1703,7 @@
</transf>
</goal>
<goal name="VC simp_eq" expl="VC for simp_eq" proved="true">
- <proof prover="2"><result status="valid" time="0.34"/></proof>
+ <proof prover="2"><result status="valid" time="0.49"/></proof>
</goal>
<goal name="VC simp_ctx" expl="VC for simp_ctx" proved="true">
<proof prover="4"><result status="valid" time="0.28" steps="978"/></proof>
@@ -2625,7 +2625,7 @@
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC add_sub_exp.75" expl="variant decrease" proved="true">
- <proof prover="2"><result status="valid" time="0.04"/></proof>
+ <proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC add_sub_exp.76" expl="postcondition" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="36"/></proof>
@@ -2652,7 +2652,7 @@
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC add_sub_exp.84" expl="variant decrease" proved="true">
- <proof prover="2"><result status="valid" time="0.03"/></proof>
+ <proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC add_sub_exp.85" expl="postcondition" proved="true">
<proof prover="4"><result status="valid" time="0.03" steps="36"/></proof>
@@ -3173,13 +3173,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.02"/></proof>
+ <proof prover="2"><result status="valid" time="0.01"/></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.01"/></proof>
+ <proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
@@ -3582,7 +3582,7 @@
<proof prover="4"><result status="valid" time="0.15" steps="265"/></proof>
</goal>
<goal name="VC prop_ctx.11" expl="postcondition" proved="true">
- <proof prover="4"><result status="valid" time="0.33" steps="738"/></proof>
+ <proof prover="4"><result status="valid" time="0.33" steps="570"/></proof>
</goal>
<goal name="VC prop_ctx.12" expl="postcondition" proved="true">
<proof prover="4"><result status="valid" time="0.14" steps="173"/></proof>
@@ -3594,7 +3594,7 @@
<proof prover="4"><result status="valid" time="0.18" steps="267"/></proof>
</goal>
<goal name="VC prop_ctx.15" expl="postcondition" proved="true">
- <proof prover="4" memlimit="2000"><result status="valid" time="1.34" steps="2919"/></proof>
+ <proof prover="4" memlimit="2000"><result status="valid" time="1.72" steps="3006"/></proof>
</goal>
<goal name="VC prop_ctx.16" expl="postcondition" proved="true">
<proof prover="4" memlimit="2000"><result status="valid" time="0.11" steps="173"/></proof>
@@ -3606,7 +3606,7 @@
<proof prover="4"><result status="valid" time="0.10" steps="267"/></proof>
</goal>
<goal name="VC prop_ctx.19" expl="postcondition" proved="true">
- <proof prover="4" memlimit="2000"><result status="valid" time="1.35" steps="2919"/></proof>
+ <proof prover="4" memlimit="2000"><result status="valid" time="1.68" steps="2905"/></proof>
</goal>
<goal name="VC prop_ctx.20" expl="postcondition" proved="true">
<proof prover="4"><result status="valid" time="0.15" steps="263"/></proof>
@@ -3667,7 +3667,7 @@
<proof prover="2"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="VC prop_ctx.37" expl="postcondition" proved="true">
- <proof prover="4"><result status="valid" time="0.70" steps="606"/></proof>
+ <proof prover="4"><result status="valid" time="0.92" steps="606"/></proof>
</goal>
<goal name="VC prop_ctx.38" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.21"/></proof>
@@ -3796,7 +3796,7 @@
<goal name="VC prop_ctx.75.3.0" expl="VC for prop_ctx" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="VC prop_ctx.75.3.0.0" expl="VC for prop_ctx" proved="true">
- <proof prover="0" timelimit="15" memlimit="2000"><result status="valid" time="0.88"/></proof>
+ <proof prover="0" timelimit="15" memlimit="2000"><result status="valid" time="1.36"/></proof>
</goal>
</transf>
</goal>
@@ -3987,7 +3987,7 @@
<proof prover="4"><result status="valid" time="0.10" steps="39"/></proof>
</goal>
<goal name="VC prop_ctx.135" expl="postcondition" proved="true">
- <proof prover="4"><result status="valid" time="0.45" steps="189"/></proof>
+ <proof prover="4"><result status="valid" time="0.62" steps="189"/></proof>
</goal>
<goal name="VC prop_ctx.136" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.16"/></proof>
diff --git a/examples/multiprecision/lineardecision/why3shapes.gz b/examples/multiprecision/lineardecision/why3shapes.gz
index 782be90d96d650c6263ca4476d7c439c5b25fde8..e197ecdde53de5044fc921efa816dd9a0b17e8fc 100644
Binary files a/examples/multiprecision/lineardecision/why3shapes.gz and b/examples/multiprecision/lineardecision/why3shapes.gz differ
diff --git a/examples/multiprecision/logical/why3session.xml b/examples/multiprecision/logical/why3session.xml
index 24d720dd3e6de52d3b1e4b602ec3e79f97b672d9..a00d093d98333763934855332485a465237e4ba1 100644
--- a/examples/multiprecision/logical/why3session.xml
+++ b/examples/multiprecision/logical/why3session.xml
@@ -475,7 +475,7 @@
<proof prover="2" timelimit="1"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="VC wmpn_lshift.37" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="1.56"/></proof>
+ <proof prover="0"><result status="valid" time="2.18"/></proof>
</goal>
<goal name="VC wmpn_lshift.38" expl="loop invariant preservation" proved="true">
<proof prover="2" timelimit="1"><result status="valid" time="0.10"/></proof>
@@ -626,7 +626,7 @@
<goal name="VC wmpn_rshift.24.1.0" expl="VC for wmpn_rshift" proved="true">
<transf name="inline_goal" proved="true" >
<goal name="VC wmpn_rshift.24.1.0.0" expl="VC for wmpn_rshift" proved="true">
- <proof prover="0"><result status="valid" time="2.84"/></proof>
+ <proof prover="0"><result status="valid" time="3.80"/></proof>
</goal>
</transf>
</goal>
@@ -748,7 +748,7 @@
</transf>
</goal>
<goal name="VC wmpn_rshift.43" expl="loop invariant preservation" proved="true">
- <proof prover="0"><result status="valid" time="2.51"/></proof>
+ <proof prover="0"><result status="valid" time="3.32"/></proof>
<proof prover="2" memlimit="2000"><result status="valid" time="0.17"/></proof>
</goal>
<goal name="VC wmpn_rshift.44" expl="loop invariant preservation" proved="true">
@@ -807,7 +807,7 @@
<proof prover="0" memlimit="1000"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC wmpn_rshift.61" expl="precondition" proved="true">
- <proof prover="0" memlimit="1000"><result status="valid" time="2.24"/></proof>
+ <proof prover="0" memlimit="1000"><result status="valid" time="2.90"/></proof>
<proof prover="2"><result status="valid" time="0.14"/></proof>
<proof prover="3"><result status="valid" time="0.05"/></proof>
</goal>
@@ -1296,7 +1296,7 @@
<proof prover="2"><result status="valid" time="0.34"/></proof>
</goal>
<goal name="VC wmpn_rshift_in_place.41.0.2" proved="true">
- <proof prover="2"><result status="valid" time="0.22"/></proof>
+ <proof prover="2"><result status="valid" time="0.38"/></proof>
</goal>
</transf>
</goal>
@@ -1311,7 +1311,7 @@
<proof prover="0"><result status="valid" time="0.25"/></proof>
</goal>
<goal name="VC wmpn_rshift_in_place.43.1" expl="assertion" proved="true">
- <proof prover="0"><result status="valid" time="0.44"/></proof>
+ <proof prover="0"><result status="valid" time="0.65"/></proof>
</goal>
<goal name="VC wmpn_rshift_in_place.43.2" expl="VC for wmpn_rshift_in_place" proved="true">
<proof prover="2"><result status="valid" time="0.06"/></proof>
@@ -1392,7 +1392,7 @@
<proof prover="2"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC wmpn_rshift_in_place.66" expl="assertion" proved="true">
- <proof prover="0"><result status="valid" time="2.42"/></proof>
+ <proof prover="0"><result status="valid" time="2.96"/></proof>
</goal>
<goal name="VC wmpn_rshift_in_place.67" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
diff --git a/examples/multiprecision/logical/why3shapes.gz b/examples/multiprecision/logical/why3shapes.gz
index 7a3e57e282799c731f0d413c4101f37f2c73730d..c2242491ddd18ea87f7eb83ca5fe32eb8202bbd0 100644
Binary files a/examples/multiprecision/logical/why3shapes.gz and b/examples/multiprecision/logical/why3shapes.gz differ