diff --git a/examples/multiprecision/lineardecision/why3session.xml b/examples/multiprecision/lineardecision/why3session.xml
index 45d419958d772365f78ff66d841ad63deda82c55..87b4cc0d88509b73c8eb25732f9a60acadbf49b7 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="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>
@@ -579,10 +579,10 @@
   <goal name="VC add_expr.4" expl="postcondition" proved="true">
   <transf name="split_vc" proved="true" >
    <goal name="VC add_expr.4.0" expl="postcondition" proved="true">
-   <proof prover="3" memlimit="1000"><result status="valid" time="0.46"/></proof>
+   <proof prover="3"><result status="valid" time="1.05"/></proof>
    </goal>
    <goal name="VC add_expr.4.1" expl="postcondition" proved="true">
-   <proof prover="3"><result status="valid" time="0.25"/></proof>
+   <proof prover="0" timelimit="1"><result status="valid" time="0.07"/></proof>
    </goal>
   </transf>
   </goal>
@@ -643,10 +643,10 @@
     <goal name="VC add_expr.17.0.0" expl="postcondition" proved="true">
     <transf name="split_vc" proved="true" >
      <goal name="VC add_expr.17.0.0.0" expl="postcondition" proved="true">
-     <proof prover="3"><result status="valid" time="0.38"/></proof>
+     <proof prover="3"><result status="valid" time="1.18"/></proof>
      </goal>
      <goal name="VC add_expr.17.0.0.1" expl="postcondition" proved="true">
-     <proof prover="3"><result status="valid" time="0.25"/></proof>
+     <proof prover="0" timelimit="1"><result status="valid" time="0.14"/></proof>
      </goal>
     </transf>
     </goal>
@@ -1070,7 +1070,7 @@
    <goal name="VC gauss_jordan.27.0" expl="assertion" proved="true">
    <transf name="split_vc" proved="true" >
     <goal name="VC gauss_jordan.27.0.0" expl="assertion" proved="true">
-    <proof prover="0"><result status="valid" time="0.11"/></proof>
+    <proof prover="0"><result status="valid" time="0.23"/></proof>
     </goal>
     <goal name="VC gauss_jordan.27.0.1" expl="VC for gauss_jordan" proved="true">
     <proof prover="2"><result status="valid" time="0.04"/></proof>
@@ -1083,14 +1083,14 @@
      <goal name="VC gauss_jordan.27.0.3.0" expl="VC for gauss_jordan" proved="true">
      <transf name="split_vc" proved="true" >
       <goal name="VC gauss_jordan.27.0.3.0.0" expl="VC for gauss_jordan" proved="true">
-      <proof prover="4"><result status="valid" time="0.27" steps="554"/></proof>
+      <proof prover="4"><result status="valid" time="0.27" steps="529"/></proof>
       </goal>
      </transf>
      </goal>
     </transf>
     </goal>
     <goal name="VC gauss_jordan.27.0.4" expl="VC for gauss_jordan" proved="true">
-    <proof prover="0"><result status="valid" time="0.16"/></proof>
+    <proof prover="0"><result status="valid" time="0.29"/></proof>
     </goal>
    </transf>
    </goal>
@@ -1137,7 +1137,7 @@
    <proof prover="2"><result status="valid" time="0.13"/></proof>
    </goal>
    <goal name="VC gauss_jordan.37.3" expl="VC for gauss_jordan" proved="true">
-   <proof prover="4"><result status="valid" time="0.26" steps="544"/></proof>
+   <proof prover="4"><result status="valid" time="0.26" steps="520"/></proof>
    </goal>
    <goal name="VC gauss_jordan.37.4" expl="VC for gauss_jordan" proved="true">
    <proof prover="0"><result status="valid" time="0.15"/></proof>
@@ -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.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>
@@ -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.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>
@@ -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.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>
@@ -1357,12 +1357,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>
@@ -1375,7 +1376,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>
@@ -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.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>
@@ -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.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>
@@ -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.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>
@@ -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.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>
@@ -3712,7 +3712,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.85"/></proof>
+     <proof prover="0" timelimit="15" memlimit="2000"><result status="valid" time="1.10"/></proof>
      </goal>
     </transf>
     </goal>
diff --git a/examples/multiprecision/lineardecision/why3shapes.gz b/examples/multiprecision/lineardecision/why3shapes.gz
index d044fa799224f2e1bd428d95ff204d6395e518fa..592a17b4507c1b4b6bd64d1b8f88050775cc4c84 100644
Binary files a/examples/multiprecision/lineardecision/why3shapes.gz and b/examples/multiprecision/lineardecision/why3shapes.gz differ