Replace spurious cloned axioms with goals, update sessions

585b99a6 · Raphael Rieu-Helft · c949253c · 585b99a6 · 585b99a6 · 585b99a6
Commit 585b99a6 authored Jun 15, 2018 by Raphael Rieu-Helft
15 changed files
--- a/examples/multiprecision/add/why3session.xml
+++ b/examples/multiprecision/add/why3session.xml
@@ -55,7 +55,7 @@
  </transf>
  </goal>
  <goal name="VC add_limb.9" expl="assertion" proved="true">
-  <proof prover="0"><result status="valid" time="0.33"/></proof>
+  <proof prover="0"><result status="valid" time="0.54"/></proof>
  </goal>
  <goal name="VC add_limb.10" expl="precondition" proved="true">
  <proof prover="3"><result status="valid" time="0.03"/></proof>
@@ -70,7 +70,7 @@
    <goal name="VC add_limb.12.0.0" expl="assertion" proved="true">
    <transf name="reflection_f" proved="true" arg1="mp_decision">
     <goal name="VC add_limb.12.0.0.0" expl="assertion" proved="true">
-     <proof prover="0"><result status="valid" time="0.24"/></proof>
+     <proof prover="0"><result status="valid" time="0.48"/></proof>
     </goal>
     <goal name="VC add_limb.12.0.0.1" proved="true">
     <proof prover="3"><result status="valid" time="0.33"/></proof>
@@ -236,7 +236,7 @@
  <proof prover="5"><result status="valid" time="0.09" steps="41"/></proof>
  </goal>
  <goal name="VC add_limbs.10" expl="assertion" proved="true">
-  <proof prover="0"><result status="valid" time="1.00"/></proof>
+  <proof prover="0"><result status="valid" time="1.49"/></proof>
  </goal>
  <goal name="VC add_limbs.11" expl="precondition" proved="true">
  <proof prover="4"><result status="valid" time="0.06"/></proof>
@@ -348,7 +348,7 @@
  </transf>
  </goal>
  <goal name="VC add.10" expl="assertion" proved="true">
-  <proof prover="0"><result status="valid" time="0.93"/></proof>
+  <proof prover="0"><result status="valid" time="1.28"/></proof>
  </goal>
  <goal name="VC add.11" expl="precondition" proved="true">
  <proof prover="4"><result status="valid" time="0.01"/></proof>
@@ -366,13 +366,13 @@
    <goal name="VC add.14.0.0" expl="assertion" proved="true">
    <transf name="reflection_f" proved="true" arg1="mp_decision">
     <goal name="VC add.14.0.0.0" expl="assertion" proved="true">
-     <proof prover="0"><result status="valid" time="0.39"/></proof>
+     <proof prover="0"><result status="valid" time="0.55"/></proof>
     </goal>
     <goal name="VC add.14.0.0.1" proved="true">
     <proof prover="3"><result status="valid" time="0.27"/></proof>
     </goal>
     <goal name="VC add.14.0.0.2" proved="true">
-     <proof prover="3"><result status="valid" time="0.19"/></proof>
+     <proof prover="3"><result status="valid" time="0.32"/></proof>
     </goal>
    </transf>
    </goal>
@@ -454,7 +454,7 @@
  <proof prover="4"><result status="valid" time="0.03"/></proof>
  </goal>
  <goal name="VC add.37" expl="assertion" proved="true">
-  <proof prover="0" timelimit="10"><result status="valid" time="1.05"/></proof>
+  <proof prover="0" timelimit="10"><result status="valid" time="1.32"/></proof>
  </goal>
  <goal name="VC add.38" expl="assertion" proved="true">
  <transf name="introduce_premises" proved="true" >
@@ -463,10 +463,10 @@
    <goal name="VC add.38.0.0" expl="assertion" proved="true">
    <transf name="reflection_f" proved="true" arg1="mp_decision">
     <goal name="VC add.38.0.0.0" expl="assertion" proved="true">
-     <proof prover="0"><result status="valid" time="0.42"/></proof>
+     <proof prover="0"><result status="valid" time="0.62"/></proof>
     </goal>
     <goal name="VC add.38.0.0.1" proved="true">
-     <proof prover="3"><result status="valid" time="0.20"/></proof>
+     <proof prover="3"><result status="valid" time="0.36"/></proof>
     </goal>
     <goal name="VC add.38.0.0.2" proved="true">
     <proof prover="5" timelimit="1"><result status="valid" time="0.32" steps="188"/></proof>
@@ -516,7 +516,7 @@
  <goal name="VC add.51" expl="precondition" proved="true">
  <transf name="split_goal_right" proved="true" >
   <goal name="VC add.51.0" expl="VC for add" proved="true">
-   <proof prover="0"><result status="valid" time="5.70"/></proof>
+   <proof prover="0"><result status="valid" time="7.86"/></proof>
   </goal>
   <goal name="VC add.51.1" expl="VC for add" proved="true">
   <proof prover="3"><result status="valid" time="0.04"/></proof>
@@ -542,10 +542,10 @@
     <proof prover="0"><result status="valid" time="0.43"/></proof>
     </goal>
     <goal name="VC add.55.0.0.1" proved="true">
-     <proof prover="3"><result status="valid" time="0.19"/></proof>
+     <proof prover="3"><result status="valid" time="0.34"/></proof>
     </goal>
     <goal name="VC add.55.0.0.2" proved="true">
-     <proof prover="2"><result status="valid" time="0.17"/></proof>
+     <proof prover="2"><result status="valid" time="0.38"/></proof>
     </goal>
    </transf>
    </goal>
@@ -612,7 +612,7 @@
  <proof prover="4"><result status="valid" time="0.02"/></proof>
  </goal>
  <goal name="VC add.73" expl="assertion" proved="true">
-  <proof prover="0" timelimit="10"><result status="valid" time="1.10"/></proof>
+  <proof prover="0" timelimit="10"><result status="valid" time="1.40"/></proof>
  </goal>
  <goal name="VC add.74" expl="assertion" proved="true">
  <transf name="introduce_premises" proved="true" >
@@ -925,7 +925,7 @@
  <proof prover="3"><result status="valid" time="0.05"/></proof>
  </goal>
  <goal name="VC add_in_place.57" expl="loop invariant preservation" proved="true">
-  <proof prover="0" timelimit="10"><result status="valid" time="0.43"/></proof>
+  <proof prover="0" timelimit="10"><result status="valid" time="0.61"/></proof>
  </goal>
  <goal name="VC add_in_place.58" expl="loop invariant preservation" proved="true">
  <proof prover="2"><result status="valid" time="0.10"/></proof>
@@ -989,7 +989,7 @@
  <proof prover="5" timelimit="1"><result status="valid" time="0.02" steps="51"/></proof>
  </goal>
  <goal name="VC incr.14" expl="assertion" proved="true">
-  <proof prover="0"><result status="valid" time="1.06"/></proof>
+  <proof prover="0"><result status="valid" time="1.42"/></proof>
  </goal>
  <goal name="VC incr.15" expl="precondition" proved="true">
  <proof prover="3"><result status="valid" time="0.01"/></proof>
@@ -1019,7 +1019,7 @@
  </transf>
  </goal>
  <goal name="VC incr.18" expl="integer overflow" proved="true">
-  <proof prover="3"><result status="valid" time="0.25"/></proof>
+  <proof prover="3"><result status="valid" time="0.50"/></proof>
  </goal>
  <goal name="VC incr.19" expl="assertion" proved="true">
  <transf name="split_goal_right" proved="true" >

--- a/examples/multiprecision/add/why3shapes.gz
+++ b/examples/multiprecision/add/why3shapes.gz
--- a/examples/multiprecision/div/why3session.xml
+++ b/examples/multiprecision/div/why3session.xml
--- a/examples/multiprecision/div/why3shapes.gz
+++ b/examples/multiprecision/div/why3shapes.gz
--- a/examples/multiprecision/lineardecision.mlw
+++ b/examples/multiprecision/lineardecision.mlw
@@ -986,8 +986,7 @@ use import RationalCoeffs
 use import real.RealInfix
 use import real.FromInt

-clone export LinearEquationsDecision with type  C.a = real, function C.(+) = (+.), function C.( * ) = ( *. ), function C.(-_) = (-._), function C.(-) = (-.), type coeff = t, type C.cvars=int -> real, function C.interp=rinterp, exception C.Unknown = QError, constant C.azero = Real.zero, constant C.aone = Real.one, predicate C.ale = (<=.), val C.czero=rzero, val C.cone=rone, lemma C.sub_def, lemma C.zero_def, lemma C.one_def, val C.add=radd, val C.mul=rmul, val C.opp=ropp, val C.eq=req, val C.inv=rinv, goal C.A.ZeroLessOne, goal C.A.CompatOrderAdd, goal C.A.CompatOrderMult, goal C.A.Unitary, goal C.A.NonTrivialRing, goal C.A.Mul_distr_l, goal C.A.Mul_distr_r, goal C.A.Inv_def_l, goal C.A.Inv_def_r, goal C.A.MulAssoc.Assoc, goal C.A.Assoc, goal C.A.MulComm.Comm, goal C.A.Comm, goal C.A.Unit_def_l, goal C.A.Unit_def_r,
-  axiom . (* FIXME: replace with "goal" and prove *)
+clone export LinearEquationsDecision with type  C.a = real, function C.(+) = (+.), function C.( * ) = ( *. ), function C.(-_) = (-._), function C.(-) = (-.), type coeff = t, type C.cvars=int -> real, function C.interp=rinterp, exception C.Unknown = QError, constant C.azero = Real.zero, constant C.aone = Real.one, predicate C.ale = (<=.), val C.czero=rzero, val C.cone=rone, lemma C.sub_def, lemma C.zero_def, lemma C.one_def, val C.add=radd, val C.mul=rmul, val C.opp=ropp, val C.eq=req, val C.inv=rinv, goal C.A.ZeroLessOne, goal C.A.CompatOrderAdd, goal C.A.CompatOrderMult, goal C.A.Unitary, goal C.A.NonTrivialRing, goal C.A.Mul_distr_l, goal C.A.Mul_distr_r, goal C.A.Inv_def_l, goal C.A.Inv_def_r, goal C.A.MulAssoc.Assoc, goal C.A.Assoc, goal C.A.MulComm.Comm, goal C.A.Comm, goal C.A.Unit_def_l, goal C.A.Unit_def_r, goal .

 end

@@ -1032,8 +1031,7 @@ let iinv (t:t') : t'
  raises { NError -> true }
 = raise NError

-clone export LinearEquationsDecision with type C.a = int, function C.(+)=(+), function C.(*) = (*), function C.(-_) = (-_), function C.(-) = (-), type coeff = t', type C.cvars = int->int,function C.interp = interp_id, constant C.azero = zero, constant C.aone = one, predicate C.ale= (<=), val C.czero = izero, val C.cone = ione, lemma C.sub_def, lemma C.zero_def, lemma C.one_def, val C.add = iadd, val C.mul = imul, val C.opp = iopp, val C.eq = ieq, val C.inv = iinv, goal C.A.ZeroLessOne, goal C.A.CompatOrderAdd, goal C.A.CompatOrderMult, goal C.A.Unitary, goal C.A.NonTrivialRing, goal C.A.Mul_distr_l, goal C.A.Mul_distr_r, goal C.A.Inv_def_l, goal C.A.Inv_def_r, goal C.A.MulAssoc.Assoc, goal C.A.Assoc, goal C.A.MulComm.Comm, goal C.A.Comm, goal C.A.Unit_def_l, goal C.A.Unit_def_r,
-  axiom . (* FIXME: replace with "goal" and prove *)
+clone export LinearEquationsDecision with type C.a = int, function C.(+)=(+), function C.(*) = (*), function C.(-_) = (-_), function C.(-) = (-), type coeff = t', type C.cvars = int->int,function C.interp = interp_id, constant C.azero = zero, constant C.aone = one, predicate C.ale= (<=), val C.czero = izero, val C.cone = ione, lemma C.sub_def, lemma C.zero_def, lemma C.one_def, val C.add = iadd, val C.mul = imul, val C.opp = iopp, val C.eq = ieq, val C.inv = iinv, goal C.A.ZeroLessOne, goal C.A.CompatOrderAdd, goal C.A.CompatOrderMult, goal C.A.Unitary, goal C.A.NonTrivialRing, goal C.A.Mul_distr_l, goal C.A.Mul_distr_r, goal C.A.Inv_def_l, goal C.A.Inv_def_r, goal C.A.MulAssoc.Assoc, goal C.A.Assoc, goal C.A.MulComm.Comm, goal C.A.Comm, goal C.A.Unit_def_l, goal C.A.Unit_def_r, goal .


 use import real.FromInt
@@ -1404,8 +1402,7 @@ use import real.RealInfix

 type coeff = t

-clone export LinearEquationsDecision with type C.a = real, function C.(+) = (+.), function C.(*) = ( *.), function C.(-_) = (-._), function C.(-) = (-.), type coeff = t, type C.cvars=evars, function C.interp=minterp, exception C.Unknown = MPError, constant C.azero = Real.zero, constant C.aone = Real.one, predicate C.ale = (<=.), val C.czero=mzero, val C.cone=mone, lemma C.sub_def, lemma C.zero_def, lemma C.one_def, val C.add=madd, val C.mul=mmul, val C.opp=mopp, val C.eq=meq, val C.inv=minv, goal C.A.ZeroLessOne, goal C.A.CompatOrderAdd, goal C.A.CompatOrderMult, goal C.A.Unitary, goal C.A.NonTrivialRing, goal C.A.Mul_distr_l, goal C.A.Mul_distr_r, goal C.A.Inv_def_l, goal C.A.Inv_def_r, goal C.A.MulAssoc.Assoc, goal C.A.Assoc, goal C.A.MulComm.Comm, goal C.A.Comm, goal C.A.Unit_def_l, goal C.A.Unit_def_r,
-  axiom . (* FIXME: replace with "goal" and prove *)
+clone export LinearEquationsDecision with type C.a = real, function C.(+) = (+.), function C.(*) = ( *.), function C.(-_) = (-._), function C.(-) = (-.), type coeff = t, type C.cvars=evars, function C.interp=minterp, exception C.Unknown = MPError, constant C.azero = Real.zero, constant C.aone = Real.one, predicate C.ale = (<=.), val C.czero=mzero, val C.cone=mone, lemma C.sub_def, lemma C.zero_def, lemma C.one_def, val C.add=madd, val C.mul=mmul, val C.opp=mopp, val C.eq=meq, val C.inv=minv, goal C.A.ZeroLessOne, goal C.A.CompatOrderAdd, goal C.A.CompatOrderMult, goal C.A.Unitary, goal C.A.NonTrivialRing, goal C.A.Mul_distr_l, goal C.A.Mul_distr_r, goal C.A.Inv_def_l, goal C.A.Inv_def_r, goal C.A.MulAssoc.Assoc, goal C.A.Assoc, goal C.A.MulComm.Comm, goal C.A.Comm, goal C.A.Unit_def_l, goal C.A.Unit_def_r, goal .

 end
 module LinearDecisionIntMP
@@ -1455,8 +1452,7 @@ let mpinv (a:t) : t
 = raise MPError


-clone export LinearEquationsDecision with type C.a = int, function C.(+) = (+), function C.(*) = (*), function C.(-_) = (-_), function C.(-) = (-), type coeff = t, type C.cvars = int->int, function C.interp = mpinterp, constant C.azero = zero, constant C.aone = one, val C.czero = mpzero, val C.cone = mpone, predicate C.ale = (<=), lemma C.sub_def, lemma C.zero_def, lemma C.one_def, val C.add = mpadd, val C.mul = mpmul, val C.opp = mpopp, val C.eq = mpeq, val C.inv = mpinv, goal C.A.ZeroLessOne, goal C.A.CompatOrderAdd, goal C.A.CompatOrderMult, goal C.A.Unitary, goal C.A.NonTrivialRing, goal C.A.Mul_distr_l, goal C.A.Mul_distr_r, goal C.A.Inv_def_l, goal C.A.Inv_def_r, goal C.A.MulAssoc.Assoc, goal C.A.Assoc, goal C.A.MulComm.Comm, goal C.A.Comm, goal C.A.Unit_def_l, goal C.A.Unit_def_r,
-  axiom . (* FIXME: replace with "goal" and prove *)
+clone export LinearEquationsDecision with type C.a = int, function C.(+) = (+), function C.(*) = (*), function C.(-_) = (-_), function C.(-) = (-), type coeff = t, type C.cvars = int->int, function C.interp = mpinterp, constant C.azero = zero, constant C.aone = one, val C.czero = mpzero, val C.cone = mpone, predicate C.ale = (<=), lemma C.sub_def, lemma C.zero_def, lemma C.one_def, val C.add = mpadd, val C.mul = mpmul, val C.opp = mpopp, val C.eq = mpeq, val C.inv = mpinv, goal C.A.ZeroLessOne, goal C.A.CompatOrderAdd, goal C.A.CompatOrderMult, goal C.A.Unitary, goal C.A.NonTrivialRing, goal C.A.Mul_distr_l, goal C.A.Mul_distr_r, goal C.A.Inv_def_l, goal C.A.Inv_def_r, goal C.A.MulAssoc.Assoc, goal C.A.Assoc, goal C.A.MulComm.Comm, goal C.A.Comm, goal C.A.Unit_def_l, goal C.A.Unit_def_r, goal .

 use LinearDecisionRationalMP as R
 use import real.FromInt

--- a/examples/multiprecision/lineardecision/why3session.xml
+++ b/examples/multiprecision/lineardecision/why3session.xml
@@ -168,10 +168,10 @@
  <proof prover="4" timelimit="5" 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" timelimit="5" 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" timelimit="5" memlimit="2000"><result status="valid" time="0.00" steps="10"/></proof>
+  <proof prover="2"><result status="valid" time="0.01"/></proof>
  </goal>
 </transf>
 </goal>
@@ -1316,7 +1316,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>
@@ -1326,24 +1326,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>
@@ -1361,10 +1361,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>
@@ -1377,12 +1377,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>
@@ -1395,7 +1396,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>
@@ -1426,16 +1426,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>
@@ -1444,16 +1444,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>
@@ -1511,17 +1511,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>
@@ -1572,16 +1572,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>
@@ -2084,6 +2084,18 @@
 <goal name="C.A.NonTrivialRing" proved="true">
 <proof prover="2"><result status="valid" time="0.01"/></proof>
 </goal>
+ <goal name="C.A.Refl" proved="true">
+ <proof prover="2"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="C.A.Trans" proved="true">
+ <proof prover="2"><result status="valid" time="0.04"/></proof>
+ </goal>
+ <goal name="C.A.Antisymm" proved="true">
+ <proof prover="2"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="C.A.Total" proved="true">
+ <proof prover="2"><result status="valid" time="0.02"/></proof>
+ </goal>
 <goal name="C.A.ZeroLessOne" proved="true">
 <proof prover="2"><result status="valid" time="0.01"/></proof>
 </goal>
@@ -2193,6 +2205,18 @@
 <goal name="C.A.NonTrivialRing" proved="true">
 <proof prover="2"><result status="valid" time="0.01"/></proof>
 </goal>
+ <goal name="C.A.Refl" proved="true">
+ <proof prover="2"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="C.A.Trans" proved="true">
+ <proof prover="2"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="C.A.Antisymm" proved="true">
+ <proof prover="2"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="C.A.Total" proved="true">
+ <proof prover="2"><result status="valid" time="0.01"/></proof>
+ </goal>
 <goal name="C.A.ZeroLessOne" proved="true">
 <proof prover="2"><result status="valid" time="0.01"/></proof>
 </goal>
@@ -2922,6 +2946,18 @@
 <goal name="C.A.NonTrivialRing" proved="true">
 <proof prover="2"><result status="valid" time="0.01"/></proof>
 </goal>
+ <goal name="C.A.Refl" proved="true">
+ <proof prover="2"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="C.A.Trans" proved="true">
+ <proof prover="2"><result status="valid" time="0.10"/></proof>
+ </goal>
+ <goal name="C.A.Antisymm" proved="true">
+ <proof prover="2"><result status="valid" time="0.10"/></proof>
+ </goal>
+ <goal name="C.A.Total" proved="true">
+ <proof prover="2"><result status="valid" time="0.09"/></proof>
+ </goal>
 <goal name="C.A.ZeroLessOne" proved="true">
 <proof prover="2"><result status="valid" time="0.01"/></proof>
 </goal>
@@ -3020,6 +3056,18 @@
 <goal name="C.A.NonTrivialRing" proved="true">
 <proof prover="2"><result status="valid" time="0.01"/></proof>
 </goal>
+ <goal name="C.A.Refl" proved="true">
+ <proof prover="2"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="C.A.Trans" proved="true">
+ <proof prover="2"><result status="valid" time="0.11"/></proof>
+ </goal>
+ <goal name="C.A.Antisymm" proved="true">
+ <proof prover="2"><result status="valid" time="0.11"/></proof>
+ </goal>
+ <goal name="C.A.Total" proved="true">
+ <proof prover="2"><result status="valid" time="0.09"/></proof>
+ </goal>
 <goal name="C.A.ZeroLessOne" proved="true">
 <proof prover="2"><result status="valid" time="0.02"/></proof>
 </goal>
@@ -3489,7 +3537,7 @@
 <goal name="VC impl_self" expl="VC for impl_self" proved="true">
 <transf name="split_goal_right" proved="true" >
  <goal name="VC impl_self.0" expl="variant decrease" proved="true">
-  <proof prover="2"><result status="valid" time="0.16"/></proof>
+  <proof prover="2"><result status="valid" time="0.28"/></proof>
  </goal>
  <goal name="VC impl_self.1" expl="precondition" proved="true">
  <proof prover="2"><result status="valid" time="0.16"/></proof>
@@ -3665,7 +3713,7 @@
  <proof prover="2"><result status="valid" time="0.33"/></proof>
  </goal>
  <goal name="VC prop_ctx.52" expl="postcondition" proved="true">
-  <proof prover="2"><result status="valid" time="0.05"/></proof>
+  <proof prover="2"><result status="valid" time="0.04"/></proof>
  </goal>
  <goal name="VC prop_ctx.53" expl="postcondition" proved="true">
  <proof prover="4"><result status="valid" time="0.07" steps="112"/></proof>
@@ -3674,7 +3722,7 @@
  <proof prover="2"><result status="valid" time="0.22"/></proof>
  </goal>
  <goal name="VC prop_ctx.55" expl="exceptional postcondition" proved="true">
-  <proof prover="2"><result status="valid" time="0.02"/></proof>
+  <proof prover="2"><result status="valid" time="0.03"/></proof>
  </goal>
  <goal name="VC prop_ctx.56" expl="exceptional postcondition" proved="true">
  <proof prover="2"><result status="valid" time="0.02"/></proof>
@@ -3698,7 +3746,7 @@
  <proof prover="2"><result status="valid" time="0.27"/></proof>
  </goal>
  <goal name="VC prop_ctx.63" expl="postcondition" proved="true">
-  <proof prover="2"><result status="valid" time="0.04"/></proof>
+  <proof prover="2"><result status="valid" time="0.05"/></proof>
  </goal>
  <goal name="VC prop_ctx.64" expl="postcondition" proved="true">
  <proof prover="4"><result status="valid" time="0.06" steps="114"/></proof>
@@ -3707,7 +3755,7 @@
  <proof prover="2"><result status="valid" time="0.18"/></proof>
  </goal>
  <goal name="VC prop_ctx.66" expl="exceptional postcondition" proved="true">
-  <proof prover="2"><result status="valid" time="0.03"/></proof>
+  <proof prover="2"><result status="valid" time="0.02"/></proof>
  </goal>
  <goal name="VC prop_ctx.67" expl="exceptional postcondition" proved="true">
  <proof prover="2"><result status="valid" time="0.01"/></proof>
@@ -3749,7 +3797,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="1" timelimit="10" memlimit="4000"><result status="valid" time="8.84"/></proof>
+     <proof prover="1" timelimit="10" memlimit="4000"><result status="valid" time="10.26"/></proof>
     </goal>
    </transf>
    </goal>
@@ -3940,7 +3988,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.82" steps="191"/></proof>
+  <proof prover="4"><result status="valid" time="0.48" steps="191"/></proof>
  </goal>
  <goal name="VC prop_ctx.136" expl="postcondition" proved="true">
  <proof prover="2"><result status="valid" time="0.17"/></proof>
@@ -3967,7 +4015,7 @@
  <proof prover="4"><result status="valid" time="0.08" steps="39"/></proof>
  </goal>
  <goal name="VC prop_ctx.144" expl="postcondition" proved="true">
-  <proof prover="4"><result status="valid" time="0.96" steps="190"/></proof>
+  <proof prover="4"><result status="valid" time="0.54" steps="190"/></proof>
  </goal>
  <goal name="VC prop_ctx.145" expl="postcondition" proved="true">
  <proof prover="2"><result status="valid" time="0.15"/></proof>
@@ -4126,7 +4174,7 @@
  <proof prover="2"><result status="valid" time="0.25"/></proof>
  </goal>
  <goal name="VC prop_ctx.195" expl="variant decrease" proved="true">
-  <proof prover="2"><result status="valid" time="0.18"/></proof>
+  <proof prover="2"><result status="valid" time="0.30"/></proof>
  </goal>
  <goal name="VC prop_ctx.196" expl="precondition" proved="true">
  <proof prover="4"><result status="valid" time="0.10" steps="85"/></proof>

--- a/examples/multiprecision/lineardecision/why3shapes.gz
+++ b/examples/multiprecision/lineardecision/why3shapes.gz
--- a/examples/multiprecision/logical/why3session.xml
+++ b/examples/multiprecision/logical/why3session.xml
@@ -129,7 +129,7 @@
   <proof prover="2" timelimit="1"><result status="valid" time="0.06"/></proof>
   </goal>
   <goal name="VC lsld_ext.9.7" expl="VC for lsld_ext" proved="true">
-   <proof prover="0"><result status="valid" time="0.67"/></proof>
+   <proof prover="0"><result status="valid" time="0.84"/></proof>
   </goal>
   <goal name="VC lsld_ext.9.8" expl="VC for lsld_ext" proved="true">
   <proof prover="3"><result status="valid" time="0.02"/></proof>
@@ -222,7 +222,7 @@
   <proof prover="5" memlimit="2000"><result status="valid" time="0.02" steps="15"/></proof>
   </goal>
   <goal name="VC clz_ext.1.4" expl="VC for clz_ext" proved="true">
-   <proof prover="1"><result status="valid" time="0.66"/></proof>
+   <proof prover="1"><result status="valid" time="1.14"/></proof>
   </goal>
   <goal name="VC clz_ext.1.5" expl="VC for clz_ext" proved="true">
   <proof prover="1"><result status="valid" time="0.10"/></proof>
@@ -365,7 +365,7 @@
  <proof prover="4"><result status="valid" time="0.03"/></proof>
  </goal>
  <goal name="VC lshift.21" expl="precondition" proved="true">
-  <proof prover="4"><result status="valid" time="0.21"/></proof>
+  <proof prover="4"><result status="valid" time="0.40"/></proof>
  </goal>
  <goal name="VC lshift.22" expl="precondition" proved="true">
  <proof prover="5" timelimit="1"><result status="valid" time="0.05" steps="74"/></proof>
@@ -396,7 +396,7 @@
  <proof prover="2" timelimit="1"><result status="valid" time="0.11"/></proof>
  </goal>
  <goal name="VC lshift.30" expl="precondition" proved="true">
-  <proof prover="3"><result status="valid" time="0.25"/></proof>
+  <proof prover="3"><result status="valid" time="0.45"/></proof>
  </goal>
  <goal name="VC lshift.31" expl="integer overflow" proved="true">
  <proof prover="4"><result status="valid" time="0.04"/></proof>
@@ -466,7 +466,7 @@
   <proof prover="3"><result status="valid" time="0.01"/></proof>
   </goal>
   <goal name="VC lshift.34.16" expl="VC for lshift" proved="true">
-   <proof prover="1"><result status="valid" time="2.00"/></proof>
+   <proof prover="1"><result status="valid" time="2.36"/></proof>
   </goal>
   <goal name="VC lshift.34.17" expl="VC for lshift" proved="true">
   <proof prover="3"><result status="valid" time="0.01"/></proof>
@@ -490,7 +490,7 @@
  <proof prover="2" timelimit="1"><result status="valid" time="0.07"/></proof>
  </goal>
  <goal name="VC lshift.37" expl="loop invariant preservation" proved="true">
-  <proof prover="0"><result status="valid" time="2.16"/></proof>
+  <proof prover="0"><result status="valid" time="2.99"/></proof>
  </goal>
  <goal name="VC lshift.38" expl="loop invariant preservation" proved="true">
  <proof prover="2" timelimit="1"><result status="valid" time="0.10"/></proof>
@@ -645,7 +645,7 @@
    <goal name="VC rshift.24.1.0" expl="VC for rshift" proved="true">
    <transf name="inline_goal" proved="true" >
     <goal name="VC rshift.24.1.0.0" expl="VC for rshift" proved="true">
-     <proof prover="0"><result status="valid" time="4.17"/></proof>
+     <proof prover="0"><result status="valid" time="4.83"/></proof>
     </goal>
    </transf>
    </goal>
@@ -676,13 +676,13 @@
  <proof prover="2"><result status="valid" time="0.19"/></proof>
  </goal>
  <goal name="VC rshift.31" expl="assertion" proved="true">
-  <proof prover="0"><result status="valid" time="0.29"/></proof>
+  <proof prover="0"><result status="valid" time="0.46"/></proof>
  </goal>
  <goal name="VC rshift.32" expl="precondition" proved="true">
  <proof prover="4"><result status="valid" time="0.02"/></proof>
  </goal>
  <goal name="VC rshift.33" expl="integer overflow" proved="true">
-  <proof prover="2"><result status="valid" time="0.09"/></proof>
+  <proof prover="2"><result status="valid" time="0.20"/></proof>
  <proof prover="4"><result status="valid" time="0.07"/></proof>
  </goal>
  <goal name="VC rshift.34" expl="precondition" proved="true">
@@ -703,7 +703,7 @@
   <proof prover="3"><result status="valid" time="0.03"/></proof>
   </goal>
   <goal name="VC rshift.36.3" expl="VC for rshift" proved="true">
-   <proof prover="1" timelimit="10"><result status="valid" time="1.00"/></proof>
+   <proof prover="1" timelimit="10"><result status="valid" time="1.33"/></proof>
   </goal>
  </transf>
  </goal>
@@ -720,7 +720,7 @@
     <proof prover="3"><result status="valid" time="0.28"/></proof>
     </goal>
     <goal name="VC rshift.37.0.0.2" proved="true">
-     <proof prover="3"><result status="valid" time="0.27"/></proof>
+     <proof prover="3"><result status="valid" time="0.42"/></proof>
     </goal>
    </transf>
    </goal>
@@ -732,7 +732,7 @@
  <proof prover="3"><result status="valid" time="0.05"/></proof>
  </goal>
  <goal name="VC rshift.39" expl="precondition" proved="true">
-  <proof prover="4"><result status="valid" time="0.47"/></proof>
+  <proof prover="4"><result status="valid" time="0.68"/></proof>
  </goal>
  <goal name="VC rshift.40" expl="loop variant decrease" proved="true">
  <proof prover="2"><result status="valid" time="0.08"/></proof>
@@ -767,7 +767,7 @@
  </transf>
  </goal>
  <goal name="VC rshift.43" expl="loop invariant preservation" proved="true">
-  <proof prover="0"><result status="valid" time="3.35"/></proof>
+  <proof prover="0"><result status="valid" time="5.62"/></proof>
  <proof prover="2" memlimit="2000"><result status="valid" time="0.17"/></proof>
  </goal>
  <goal name="VC rshift.44" expl="loop invariant preservation" proved="true">