Update obsolete sessions.

af50ea2e · Guillaume Melquiond · 1e2d3f3a · af50ea2e · af50ea2e · af50ea2e
Commit af50ea2e authored Feb 19, 2018 by Guillaume Melquiond
51 changed files
--- a/examples/avl/tables/why3session.xml
+++ b/examples/avl/tables/why3session.xml
--- a/examples/avl/tables/why3shapes.gz
+++ b/examples/avl/tables/why3shapes.gz
--- a/examples/binary_search/why3session.xml
+++ b/examples/binary_search/why3session.xml
@@ -5,27 +5,27 @@
 <prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="3" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/>
 <file name="../binary_search.mlw" proved="true">
-<theory name="BinarySearch" proved="true" sum="d31e4317db720e4fcc15037002211036">
+<theory name="BinarySearch" proved="true">
 <goal name="VC binary_search" expl="VC for binary_search" proved="true">
 <proof prover="3"><result status="valid" time="0.05" steps="88"/></proof>
 </goal>
 </theory>
-<theory name="BinarySearchAnyMidPoint" proved="true" sum="6ddfd27f10cde251a7e1595797c95b78">
+<theory name="BinarySearchAnyMidPoint" proved="true">
 <goal name="VC binary_search" expl="VC for binary_search" proved="true">
 <proof prover="3"><result status="valid" time="0.01" steps="63"/></proof>
 </goal>
 </theory>
-<theory name="BinarySearchBranchless" proved="true" sum="2a9abf885782d1699240f4f90a15db6f">
+<theory name="BinarySearchBranchless" proved="true">
 <goal name="VC binary_search" expl="VC for binary_search" proved="true">
 <proof prover="0"><result status="valid" time="0.06" steps="147"/></proof>
 </goal>
 </theory>
-<theory name="BinarySearchInt32" proved="true" sum="189de117608870d3dac4a21f7234eef5">
+<theory name="BinarySearchInt32" proved="true">
 <goal name="VC binary_search" expl="VC for binary_search" proved="true">
- <proof prover="3"><result status="valid" time="8.18" steps="11481"/></proof>
+ <proof prover="3"><result status="valid" time="1.27" steps="8288"/></proof>
 </goal>
 </theory>
-<theory name="BinarySearchBoolean" proved="true" sum="30b8723bec4ae48757a979bd59ddcac1">
+<theory name="BinarySearchBoolean" proved="true">
 <goal name="VC binary_search" expl="VC for binary_search" proved="true">
 <proof prover="3"><result status="valid" time="0.08" steps="194"/></proof>
 </goal>

--- a/examples/binary_search/why3shapes.gz
+++ b/examples/binary_search/why3shapes.gz
--- a/examples/binary_search_vc_sp/why3session.xml
+++ b/examples/binary_search_vc_sp/why3session.xml
@@ -4,22 +4,22 @@
 <why3session shape_version="4">
 <prover id="0" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
 <file name="../binary_search_vc_sp.mlw" proved="true">
-<theory name="BinarySearch" proved="true" sum="986e3c732646924bbc22bb3d4ec369ee">
+<theory name="BinarySearch" proved="true">
 <goal name="VC binary_search" expl="VC for binary_search" proved="true">
 <proof prover="0"><result status="valid" time="0.04"/></proof>
 </goal>
 </theory>
-<theory name="BinarySearchAnyMidPoint" proved="true" sum="1706e9372b3999d5866c48e66a5223f9">
+<theory name="BinarySearchAnyMidPoint" proved="true">
 <goal name="VC binary_search" expl="VC for binary_search" proved="true">
 <proof prover="0"><result status="valid" time="0.03"/></proof>
 </goal>
 </theory>
-<theory name="BinarySearchInt32" proved="true" sum="0aeaeda1d3225a20418f2d07e713896a">
+<theory name="BinarySearchInt32" proved="true">
 <goal name="VC binary_search" expl="VC for binary_search" proved="true">
 <proof prover="0"><result status="valid" time="0.10"/></proof>
 </goal>
 </theory>
-<theory name="BinarySearchBoolean" proved="true" sum="30b8723bec4ae48757a979bd59ddcac1">
+<theory name="BinarySearchBoolean" proved="true">
 <goal name="VC binary_search" expl="VC for binary_search" proved="true">
 <proof prover="0"><result status="valid" time="0.06"/></proof>
 </goal>

--- a/examples/binary_search_vc_sp/why3shapes.gz
+++ b/examples/binary_search_vc_sp/why3shapes.gz
--- a/examples/binary_sqrt/why3session.xml
+++ b/examples/binary_sqrt/why3session.xml
@@ -4,48 +4,48 @@
 <why3session shape_version="4">
 <prover id="0" name="Z3" version="4.4.1" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="1" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/>
-<file name="../binary_sqrt.mlw" expanded="true">
-<theory name="BinarySqrt" sum="68be46510357f2113d6ed3a229a54ea8" expanded="true">
- <goal name="VC sqrt" expl="VC for sqrt" expanded="true">
- <transf name="split_goal_wp" expanded="true">
-  <goal name="VC sqrt.1" expl="assertion" expanded="true">
+<file name="../binary_sqrt.mlw" proved="true">
+<theory name="BinarySqrt" proved="true">
+ <goal name="VC sqrt" expl="VC for sqrt" proved="true">
+ <transf name="split_goal_wp" proved="true" >
+  <goal name="VC sqrt.0" expl="assertion" proved="true">
  <proof prover="1"><result status="valid" time="0.00" steps="13"/></proof>
  </goal>
-  <goal name="VC sqrt.2" expl="assertion" expanded="true">
+  <goal name="VC sqrt.1" expl="assertion" proved="true">
  <proof prover="1"><result status="valid" time="0.00" steps="8"/></proof>
  </goal>
-  <goal name="VC sqrt.3" expl="assertion" expanded="true">
+  <goal name="VC sqrt.2" expl="assertion" proved="true">
  <proof prover="1"><result status="valid" time="0.00" steps="10"/></proof>
  </goal>
-  <goal name="VC sqrt.4" expl="assertion" expanded="true">
+  <goal name="VC sqrt.3" expl="assertion" proved="true">
  <proof prover="1"><result status="valid" time="0.02" steps="26"/></proof>
  </goal>
-  <goal name="VC sqrt.5" expl="assertion" expanded="true">
+  <goal name="VC sqrt.4" expl="assertion" proved="true">
  <proof prover="1"><result status="valid" time="0.02" steps="27"/></proof>
  </goal>
-  <goal name="VC sqrt.6" expl="variant decrease" expanded="true">
+  <goal name="VC sqrt.5" expl="variant decrease" proved="true">
  <proof prover="1"><result status="valid" time="0.02" steps="33"/></proof>
  </goal>
-  <goal name="VC sqrt.7" expl="precondition" expanded="true">
+  <goal name="VC sqrt.6" expl="precondition" proved="true">
  <proof prover="1"><result status="valid" time="0.00" steps="12"/></proof>
  </goal>
-  <goal name="VC sqrt.8" expl="precondition" expanded="true">
+  <goal name="VC sqrt.7" expl="precondition" proved="true">
  <proof prover="1"><result status="valid" time="0.00" steps="12"/></proof>
  </goal>
-  <goal name="VC sqrt.9" expl="precondition" expanded="true">
-  <proof prover="1"><result status="valid" time="0.22" steps="127"/></proof>
+  <goal name="VC sqrt.8" expl="precondition" proved="true">
+  <proof prover="1"><result status="valid" time="0.22" steps="135"/></proof>
  </goal>
-  <goal name="VC sqrt.10" expl="postcondition" expanded="true">
-  <transf name="split_goal_wp" expanded="true">
-   <goal name="VC sqrt.10.1" expl="VC for sqrt" expanded="true">
+  <goal name="VC sqrt.9" expl="postcondition" proved="true">
+  <transf name="split_goal_wp" proved="true" >
+   <goal name="VC sqrt.9.0" expl="VC for sqrt" proved="true">
   <proof prover="1" timelimit="5"><result status="valid" time="0.01" steps="16"/></proof>
   </goal>
-   <goal name="VC sqrt.10.2" expl="VC for sqrt" expanded="true">
-   <transf name="split_goal_wp" expanded="true">
-    <goal name="VC sqrt.10.2.1" expl="VC for sqrt" expanded="true">
+   <goal name="VC sqrt.9.1" expl="VC for sqrt" proved="true">
+   <transf name="split_goal_wp" proved="true" >
+    <goal name="VC sqrt.9.1.0" expl="VC for sqrt" proved="true">
    <proof prover="0"><result status="valid" time="0.02"/></proof>
    </goal>
-    <goal name="VC sqrt.10.2.2" expl="VC for sqrt" expanded="true">
+    <goal name="VC sqrt.9.1.1" expl="VC for sqrt" proved="true">
    <proof prover="1" timelimit="5"><result status="valid" time="0.00" steps="16"/></proof>
    </goal>
   </transf>
@@ -54,7 +54,7 @@
  </goal>
 </transf>
 </goal>
- <goal name="VC sqrt_main" expl="VC for sqrt_main" expanded="true">
+ <goal name="VC sqrt_main" expl="VC for sqrt_main" proved="true">
 <proof prover="1"><result status="valid" time="0.00" steps="5"/></proof>
 </goal>
 </theory>

--- a/examples/binary_sqrt/why3shapes.gz
+++ b/examples/binary_sqrt/why3shapes.gz
--- a/examples/bitcount/why3session.xml
+++ b/examples/bitcount/why3session.xml
@@ -9,7 +9,7 @@
 <prover id="4" name="CVC4" version="1.4" alternative="noBV" timelimit="5" steplimit="0" memlimit="4000"/>
 <prover id="5" name="Z3" version="4.4.1" timelimit="5" steplimit="0" memlimit="4000"/>
 <file name="../bitcount.mlw" proved="true">
-<theory name="BitCount8bit_fact" proved="true" sum="efb7c951014c6f701cd5a5b6603d09fd">
+<theory name="BitCount8bit_fact" proved="true">
 <goal name="nth_as_bv_is_int" proved="true">
 <proof prover="0"><result status="valid" time="0.05"/></proof>
 <proof prover="3"><result status="valid" time="0.16" steps="166"/></proof>
@@ -234,7 +234,7 @@
 </transf>
 </goal>
 </theory>
-<theory name="BitCounting32" proved="true" sum="36a25c3680ec5f18a9c1df70600fed22">
+<theory name="BitCounting32" proved="true">
 <goal name="VC proof0" expl="VC for proof0" proved="true">
 <transf name="split_goal_wp" proved="true" >
  <goal name="VC proof0.0" expl="assertion" proved="true">
@@ -700,7 +700,7 @@
 </transf>
 </goal>
 </theory>
-<theory name="Hamming" proved="true" sum="37fb69ba48c96019a185e0ef310cb658">
+<theory name="Hamming" proved="true">
 <goal name="VC hammingD" expl="VC for hammingD" proved="true">
 <transf name="split_goal_wp" proved="true" >
  <goal name="VC hammingD.0" expl="assertion" proved="true">
@@ -710,7 +710,7 @@
  </goal>
  <goal name="VC hammingD.1" expl="postcondition" proved="true">
  <proof prover="3"><result status="valid" time="1.12" steps="837"/></proof>
-  <proof prover="5"><result status="valid" time="0.08"/></proof>
+  <proof prover="5"><result status="valid" time="0.19"/></proof>
  </goal>
 </transf>
 </goal>
@@ -788,7 +788,7 @@
 <proof prover="5"><result status="valid" time="0.03"/></proof>
 </goal>
 </theory>
-<theory name="AsciiCode" proved="true" sum="8984a858936e4964cb9643d8ffed3278">
+<theory name="AsciiCode" proved="true">
 <goal name="VC bv_even" expl="VC for bv_even" proved="true">
 <transf name="split_goal_wp" proved="true" >
  <goal name="VC bv_even.0" expl="assertion" proved="true">
@@ -806,7 +806,7 @@
  <goal name="VC bv_even.3" expl="assertion" proved="true">
  <transf name="split_goal_wp" proved="true" >
   <goal name="VC bv_even.3.0" expl="VC for bv_even" proved="true">
-   <proof prover="3"><result status="valid" time="1.08" steps="933"/></proof>
+   <proof prover="3"><result status="valid" time="1.45" steps="1341"/></proof>
   </goal>
   <goal name="VC bv_even.3.1" expl="VC for bv_even" proved="true">
   <proof prover="3"><result status="valid" time="0.06" steps="142"/></proof>

--- a/examples/bitcount/why3shapes.gz
+++ b/examples/bitcount/why3shapes.gz
--- a/examples/bitvectors/double/why3session.xml
+++ b/examples/bitvectors/double/why3session.xml
@@ -8,9 +8,9 @@
 <prover id="4" name="Coq" version="8.7.1" timelimit="30" steplimit="0" memlimit="1000"/>
 <prover id="5" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="1000"/>
 <file name="../double.why" proved="true">
-<theory name="BV_double" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e">
+<theory name="BV_double" proved="true">
 </theory>
-<theory name="TestDouble" proved="true" sum="4120bd89e05ca08e761d40884b9d0621">
+<theory name="TestDouble" proved="true">
 <goal name="nth_one1" proved="true">
 <proof prover="0" timelimit="3"><result status="valid" time="0.05" steps="77"/></proof>
 </goal>
@@ -32,7 +32,7 @@
 </goal>
 <goal name="mantissa_one" proved="true">
 <proof prover="0"><result status="valid" time="0.09" steps="87"/></proof>
- <proof prover="3"><result status="valid" time="0.84"/></proof>
+ <proof prover="3"><result status="valid" time="1.04"/></proof>
 <proof prover="5" timelimit="11"><result status="valid" time="2.72"/></proof>
 </goal>
 <goal name="double_value_of_1" proved="true">

--- a/examples/bitvectors/double/why3shapes.gz
+++ b/examples/bitvectors/double/why3shapes.gz
--- a/examples/bitvectors/double_of_int/why3session.xml
+++ b/examples/bitvectors/double_of_int/why3session.xml
--- a/examples/bitvectors/double_of_int/why3shapes.gz
+++ b/examples/bitvectors/double_of_int/why3shapes.gz
--- a/examples/bitvectors/neg_as_xor/why3session.xml
+++ b/examples/bitvectors/neg_as_xor/why3session.xml
@@ -6,69 +6,69 @@
 <prover id="3" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="5" name="Z3" version="3.2" timelimit="10" steplimit="0" memlimit="1000"/>
 <prover id="9" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
-<file name="../neg_as_xor.why" expanded="true">
-<theory name="TestNegAsXOR" sum="692831fdefa67c6dc694b2674e2744e5" expanded="true">
- <goal name="Nth_j" expl="">
+<file name="../neg_as_xor.why" proved="true">
+<theory name="TestNegAsXOR" proved="true">
+ <goal name="Nth_j" proved="true">
 <proof prover="1"><result status="valid" time="0.05" steps="77"/></proof>
 </goal>
- <goal name="sign_of_j" expl="">
+ <goal name="sign_of_j" proved="true">
 <proof prover="1"><result status="valid" time="0.02" steps="76"/></proof>
- <proof prover="3"><result status="valid" time="2.70"/></proof>
+ <proof prover="3"><result status="valid" time="4.87"/></proof>
 </goal>
- <goal name="mantissa_of_j" expl="">
+ <goal name="mantissa_of_j" proved="true">
 <proof prover="1"><result status="valid" time="0.16" steps="121"/></proof>
- <proof prover="3"><result status="valid" time="0.87"/></proof>
+ <proof prover="3"><result status="valid" time="1.54"/></proof>
 <proof prover="5"><result status="valid" time="2.61"/></proof>
 <proof prover="9"><result status="valid" time="0.78"/></proof>
 </goal>
- <goal name="exp_of_j" expl="">
+ <goal name="exp_of_j" proved="true">
 <proof prover="1"><result status="valid" time="0.17" steps="122"/></proof>
- <proof prover="3"><result status="valid" time="1.08"/></proof>
- <proof prover="5" timelimit="11"><result status="valid" time="2.63"/></proof>
+ <proof prover="3"><result status="valid" time="1.53"/></proof>
+ <proof prover="5" timelimit="11"><result status="valid" time="3.00"/></proof>
 <proof prover="9"><result status="valid" time="0.70"/></proof>
 </goal>
- <goal name="int_of_bv" expl="">
+ <goal name="int_of_bv" proved="true">
 <proof prover="1"><result status="valid" time="0.06" steps="94"/></proof>
 <proof prover="3"><result status="valid" time="0.05"/></proof>
 <proof prover="5" timelimit="5"><result status="valid" time="0.10"/></proof>
 <proof prover="9"><result status="valid" time="0.11"/></proof>
 </goal>
- <goal name="MainResultBits" expl="">
+ <goal name="MainResultBits" proved="true">
 <proof prover="1"><result status="valid" time="0.15" steps="130"/></proof>
- <proof prover="3"><result status="valid" time="0.78"/></proof>
+ <proof prover="3"><result status="valid" time="1.06"/></proof>
 </goal>
- <goal name="MainResultSign" expl="">
+ <goal name="MainResultSign" proved="true">
 <proof prover="1"><result status="valid" time="0.04" steps="102"/></proof>
 <proof prover="3"><result status="valid" time="0.06"/></proof>
 </goal>
- <goal name="Sign_of_xor_j" expl="">
+ <goal name="Sign_of_xor_j" proved="true">
 <proof prover="1"><result status="valid" time="0.04" steps="85"/></proof>
 <proof prover="3"><result status="valid" time="0.05"/></proof>
 <proof prover="5" timelimit="5"><result status="valid" time="0.00"/></proof>
 <proof prover="9"><result status="valid" time="0.00"/></proof>
 </goal>
- <goal name="Exp_of_xor_j" expl="">
+ <goal name="Exp_of_xor_j" proved="true">
 <proof prover="1"><result status="valid" time="1.72" steps="492"/></proof>
- <proof prover="3"><result status="valid" time="0.96"/></proof>
+ <proof prover="3"><result status="valid" time="1.64"/></proof>
 <proof prover="5"><result status="valid" time="2.98"/></proof>
 <proof prover="9"><result status="valid" time="0.88"/></proof>
 </goal>
- <goal name="Mantissa_of_xor_j" expl="">
- <proof prover="3"><result status="valid" time="0.99"/></proof>
- <proof prover="5"><result status="valid" time="2.74"/></proof>
+ <goal name="Mantissa_of_xor_j" proved="true">
+ <proof prover="3"><result status="valid" time="1.72"/></proof>
+ <proof prover="5"><result status="valid" time="3.22"/></proof>
 <proof prover="9"><result status="valid" time="0.75"/></proof>
 </goal>
- <goal name="MainResultZero" expl="">
+ <goal name="MainResultZero" proved="true">
 <proof prover="1"><result status="valid" time="0.07" steps="104"/></proof>
 <proof prover="3"><result status="valid" time="0.06"/></proof>
- <proof prover="5"><result status="valid" time="3.77"/></proof>
+ <proof prover="5"><result status="valid" time="3.06"/></proof>
 <proof prover="9"><result status="valid" time="1.30"/></proof>
 </goal>
- <goal name="sign_neg" expl="">
+ <goal name="sign_neg" proved="true">
 <proof prover="1"><result status="valid" time="0.07" steps="107"/></proof>
 <proof prover="3"><result status="valid" time="0.04"/></proof>
 </goal>
- <goal name="MainResult" expl="">
+ <goal name="MainResult" proved="true">
 <proof prover="1"><result status="valid" time="1.90" steps="320"/></proof>
 </goal>
 </theory>

--- a/examples/bitvectors/neg_as_xor/why3shapes.gz
+++ b/examples/bitvectors/neg_as_xor/why3shapes.gz
--- a/examples/bitvectors/power2/why3session.xml
+++ b/examples/bitvectors/power2/why3session.xml
@@ -10,7 +10,7 @@
 <prover id="9" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="10" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
 <file name="../power2.why" proved="true">
-<theory name="Pow2int" proved="true" sum="89a88024fb38dcd933a68112fe649faf">
+<theory name="Pow2int" proved="true">
 <goal name="Power_1" proved="true">
 <proof prover="2"><result status="valid" time="0.00"/></proof>
 <proof prover="6"><result status="valid" time="0.00"/></proof>
@@ -434,7 +434,7 @@
 <proof prover="4" edited="power2_Pow2int_Mod_pow2_gen_1.v"><result status="valid" time="0.86"/></proof>
 </goal>
 </theory>
-<theory name="Pow2real" proved="true" sum="e31a44730ea8985818a40fb1e9374bf0">
+<theory name="Pow2real" proved="true">
 <goal name="Power_s_all" proved="true">
 <proof prover="2"><result status="valid" time="0.00"/></proof>
 <proof prover="6"><result status="valid" time="0.00"/></proof>

--- a/examples/bitvectors/power2/why3shapes.gz
+++ b/examples/bitvectors/power2/why3shapes.gz
--- a/examples/bts/12475/why3session.xml
+++ b/examples/bts/12475/why3session.xml
@@ -6,9 +6,9 @@
 <prover id="2" name="CVC3" version="2.4.1" timelimit="2" steplimit="0" memlimit="0"/>
 <prover id="3" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="4" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
-<file name="../12475.why" expanded="true">
-<theory name="Stmt" sum="0e2404171b03ea1ac9328dfdd4b535ce" expanded="true">
- <goal name="toto" expl="" expanded="true">
+<file name="../12475.why" proved="true">
+<theory name="Stmt" proved="true">
+ <goal name="toto" proved="true">
 <proof prover="0"><result status="valid" time="0.01" steps="3"/></proof>
 <proof prover="2"><result status="valid" time="0.00"/></proof>
 <proof prover="3"><result status="valid" time="0.01"/></proof>

--- a/examples/bts/12475/why3shapes.gz
+++ b/examples/bts/12475/why3shapes.gz
--- a/examples/check-builtin/floats/why3session.xml
+++ b/examples/check-builtin/floats/why3session.xml
@@ -6,27 +6,27 @@
 <prover id="1" name="Gappa" version="1.3.0" timelimit="5" steplimit="0" memlimit="0"/>
 <prover id="4" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="0"/>
 <prover id="5" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="0"/>
-<file name="../floats.why" expanded="true">
-<theory name="TestGappa" sum="4c8d897018b3c9f444fd4dfcf625015e" expanded="true">
- <goal name="Round_single_01" expl="" expanded="true">
+<file name="../floats.why" proved="true">
+<theory name="TestGappa" proved="true">
+ <goal name="Round_single_01" proved="true">
 <proof prover="1"><result status="valid" time="0.00"/></proof>
 </goal>
- <goal name="Round_double_01" expl="" expanded="true">
+ <goal name="Round_double_01" proved="true">
 <proof prover="1"><result status="valid" time="0.00"/></proof>
 </goal>
- <goal name="Test00" expl="" expanded="true">
+ <goal name="Test00" proved="true">
 <proof prover="0"><result status="valid" time="0.02"/></proof>
 <proof prover="1"><result status="valid" time="0.00"/></proof>
- <proof prover="4"><result status="valid" time="0.01" steps="5"/></proof>
+ <proof prover="4"><result status="valid" time="0.01" steps="6"/></proof>
 <proof prover="5"><result status="valid" time="0.02"/></proof>
 </goal>
- <goal name="Test01" expl="" expanded="true">
+ <goal name="Test01" proved="true">
 <proof prover="1"><result status="valid" time="0.00"/></proof>
 </goal>
- <goal name="Test02" expl="" expanded="true">
+ <goal name="Test02" proved="true">
 <proof prover="1"><result status="valid" time="0.00"/></proof>
 </goal>
- <goal name="Test03" expl="" expanded="true">
+ <goal name="Test03" proved="true">
 <proof prover="1"><result status="valid" time="0.00"/></proof>
 </goal>
 </theory>

--- a/examples/check-builtin/floats/why3shapes.gz
+++ b/examples/check-builtin/floats/why3shapes.gz
--- a/examples/check-builtin/intreal/why3session.xml
+++ b/examples/check-builtin/intreal/why3session.xml
@@ -8,48 +8,48 @@
 <prover id="6" name="Z3" version="3.2" timelimit="10" steplimit="0" memlimit="0"/>
 <prover id="8" name="Alt-Ergo" version="0.99.1" timelimit="10" steplimit="0" memlimit="0"/>
 <prover id="9" name="Z3" version="4.3.2" timelimit="10" steplimit="0" memlimit="0"/>
-<file name="../intreal.why" expanded="true">
-<theory name="IntReal" sum="e7d16ffd7fad54478d1870f95f4ad0db" expanded="true">
- <goal name="G1" expl="" expanded="true">
+<file name="../intreal.why" proved="true">
+<theory name="IntReal" proved="true">
+ <goal name="G1" proved="true">
 <proof prover="0"><result status="valid" time="0.00"/></proof>
 <proof prover="1"><result status="valid" time="0.00"/></proof>
 <proof prover="6"><result status="valid" time="0.00"/></proof>
- <proof prover="8"><result status="valid" time="0.06" steps="36"/></proof>
+ <proof prover="8"><result status="valid" time="0.06" steps="39"/></proof>
 <proof prover="9"><result status="valid" time="0.00"/></proof>
 </goal>
- <goal name="G2" expl="" expanded="true">
+ <goal name="G2" proved="true">
 <proof prover="1"><result status="valid" time="0.00"/></proof>
 <proof prover="6"><result status="valid" time="0.01"/></proof>
- <proof prover="8"><result status="valid" time="0.14" steps="84"/></proof>
+ <proof prover="8"><result status="valid" time="0.14" steps="87"/></proof>
 <proof prover="9"><result status="valid" time="0.02"/></proof>
 </goal>
- <goal name="G3" expl="" expanded="true">
+ <goal name="G3" proved="true">
 <proof prover="1"><result status="valid" time="0.00"/></proof>
 <proof prover="6"><result status="valid" time="0.01"/></proof>
- <proof prover="8"><result status="valid" time="0.17" steps="84"/></proof>
+ <proof prover="8"><result status="valid" time="0.17" steps="87"/></proof>
 <proof prover="9"><result status="valid" time="0.01"/></proof>
 </goal>
- <goal name="G4" expl="" expanded="true">
+ <goal name="G4" proved="true">
 <proof prover="1"><result status="valid" time="0.00"/></proof>
 <proof prover="6"><result status="valid" time="0.01"/></proof>
- <proof prover="8"><result status="valid" time="0.14" steps="83"/></proof>
+ <proof prover="8"><result status="valid" time="0.14" steps="87"/></proof>
 <proof prover="9"><result status="valid" time="0.01"/></proof>
 </goal>
- <goal name="G5" expl="" expanded="true">
+ <goal name="G5" proved="true">
 <proof prover="1"><result status="valid" time="0.00"/></proof>
 <proof prover="6"><result status="valid" time="0.01"/></proof>
- <proof prover="8"><result status="valid" time="0.14" steps="83"/></proof>
+ <proof prover="8"><result status="valid" time="0.14" steps="87"/></proof>
 <proof prover="9"><result status="valid" time="0.01"/></proof>
 </goal>
- <goal name="G6" expl="" expanded="true">
+ <goal name="G6" proved="true">
 <proof prover="0"><result status="valid" time="0.00"/></proof>
 <proof prover="1"><result status="valid" time="0.00"/></proof>
 <proof prover="3"><result status="valid" time="0.10"/></proof>
 <proof prover="6"><result status="valid" time="0.01"/></proof>
- <proof prover="8"><result status="valid" time="0.06" steps="29"/></proof>
+ <proof prover="8"><result status="valid" time="0.06" steps="30"/></proof>
 <proof prover="9"><result status="valid" time="0.01"/></proof>
 </goal>
- <goal name="G7" expl="" expanded="true">
+ <goal name="G7" proved="true">
 <proof prover="0"><result status="valid" time="0.00"/></proof>
 <proof prover="1"><result status="valid" time="0.00"/></proof>
 <proof prover="6"><result status="valid" time="0.01"/></proof>

--- a/examples/check-builtin/intreal/why3shapes.gz
+++ b/examples/check-builtin/intreal/why3shapes.gz
--- a/examples/check-builtin/real/why3session.xml
+++ b/examples/check-builtin/real/why3session.xml
@@ -10,7 +10,7 @@
 <prover id="12" name="Alt-Ergo" version="0.99.1" timelimit="3" steplimit="0" memlimit="0"/>
 <prover id="14" name="Z3" version="4.3.2" timelimit="3" steplimit="0" memlimit="0"/>
 <file name="../real.why" proved="true">
-<theory name="Test" proved="true" sum="fa766792600f8b59ffb54deaecae5fd5">
+<theory name="Test" proved="true">
 <goal name="G1" proved="true">
 <proof prover="2"><result status="valid" time="0.00"/></proof>
 <proof prover="7"><result status="valid" time="0.01"/></proof>
@@ -33,7 +33,7 @@
 <proof prover="14"><result status="valid" time="0.00"/></proof>
 </goal>
 </theory>
-<theory name="TestInfix" proved="true" sum="f9e4b7c6b90d06ca8e54ccb21378b7c3">
+<theory name="TestInfix" proved="true">
 <goal name="Add" proved="true">
 <proof prover="2"><result status="valid" time="0.00"/></proof>
 <proof prover="8"><result status="valid" time="0.00"/></proof>
@@ -76,7 +76,7 @@
 <proof prover="14"><result status="valid" time="0.00"/></proof>
 </goal>
 </theory>
-<theory name="SquareTest" proved="true" sum="f5ea8549d8b1f79c2129c56632f38b01">
+<theory name="SquareTest" proved="true">
 <goal name="Sqrt_zero" proved="true">
 <proof prover="2"><result status="valid" time="0.01"/></proof>
 <proof prover="8" timelimit="60" memlimit="1000"><result status="valid" time="0.02"/></proof>
@@ -98,7 +98,7 @@
 <proof prover="12" timelimit="5" memlimit="1000"><result status="valid" time="0.00" steps="8"/></proof>
 </goal>
 </theory>
-<theory name="ExpLogTest" proved="true" sum="cd1e6835a7a21f47ea5fa0d7580d1c27">
+<theory name="ExpLogTest" proved="true">
 <goal name="Log_e" proved="true">
 <proof prover="2"><result status="valid" time="0.00"/></proof>
 <proof prover="8"><result status="valid" time="0.01"/></proof>
@@ -106,7 +106,7 @@
 <proof prover="14"><result status="valid" time="0.01"/></proof>
 </goal>
 </theory>
-<theory name="PowerIntTest" proved="true" sum="1e54cdf0224cce818e1516659037b62e">
+<theory name="PowerIntTest" proved="true">
 <goal name="Pow_2_2" proved="true">
 <proof prover="2"><result status="valid" time="0.00"/></proof>
 <proof prover="8"><result status="valid" time="0.01"/></proof>
@@ -114,14 +114,14 @@
 <proof prover="14"><result status="valid" time="0.01"/></proof>
 </goal>
 </theory>
-<theory name="PowerRealTest" proved="true" sum="180a4360503699539283c0e3683511ef">
+<theory name="PowerRealTest" proved="true">
 <goal name="Pow_2_2" proved="true">
 <proof prover="8"><result status="valid" time="0.01"/></proof>
- <proof prover="12"><result status="valid" time="0.01" steps="6"/></proof>
+ <proof prover="12"><result status="valid" time="0.01" steps="8"/></proof>
 <proof prover="14"><result status="valid" time="0.01"/></proof>
 </goal>
 </theory>
-<theory name="TrigonometryTest" proved="true" sum="d294ff286e37b3974b0eafb6adbbf485">
+<theory name="TrigonometryTest" proved="true">
 <goal name="Cos_2_pi" proved="true">
 <proof prover="2"><result status="valid" time="0.00"/></proof>
 <proof prover="8"><result status="valid" time="0.09"/></proof>

--- a/examples/check-builtin/real/why3shapes.gz
+++ b/examples/check-builtin/real/why3shapes.gz
--- a/examples/cursor_examples/why3session.xml
+++ b/examples/cursor_examples/why3session.xml
@@ -6,12 +6,12 @@
 <prover id="1" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="2" name="Z3" version="4.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
 <file name="../cursor_examples.mlw" proved="true">
-<theory name="TestCursor" proved="true" sum="4c6babb04c51cb21c0e11617bac06fa4">
+<theory name="TestCursor" proved="true">
 <goal name="VC sum" expl="VC for sum" proved="true">
 <proof prover="1"><result status="valid" time="2.86" steps="906"/></proof>
 </goal>
 </theory>
-<theory name="ListCursorImpl" proved="true" sum="5c9d2123d18fe945b303f391ec90daed">
+<theory name="ListCursorImpl" proved="true">
 <goal name="VC cursor" expl="VC for cursor" proved="true">
 <proof prover="1"><result status="valid" time="0.02" steps="33"/></proof>
 </goal>
@@ -37,7 +37,7 @@
 <proof prover="1"><result status="valid" time="0.02" steps="12"/></proof>
 </goal>
 </theory>
-<theory name="TestListCursor" proved="true" sum="5e03d6040df40972278e1bab8d1137ac">
+<theory name="TestListCursor" proved="true">
 <goal name="sum_of_list" proved="true">
 <transf name="induction_ty_lex" proved="true" >
  <goal name="sum_of_list.0" proved="true">
@@ -75,7 +75,7 @@
  <goal name="VC list_sum.6" expl="loop invariant preservation" proved="true">
  <transf name="simplify_trivial_quantification" proved="true" >
   <goal name="VC list_sum.6.0" expl="loop invariant preservation" proved="true">
-   <proof prover="1"><result status="valid" time="4.55" steps="1488"/></proof>
+   <proof prover="1"><result status="valid" time="4.55" steps="1512"/></proof>
   </goal>
  </transf>
  </goal>
@@ -88,7 +88,7 @@
 </transf>
 </goal>
 </theory>
-<theory name="TestListCursorLink" proved="true" sum="57ad90333a0eff06c751d7979b07b08c">
+<theory name="TestListCursorLink" proved="true">
 <goal name="TestListCursor.ListCursor.VC create" expl="VC for create" proved="true">
 <proof prover="1"><result status="valid" time="0.02" steps="38"/></proof>
 </goal>
@@ -99,7 +99,7 @@
 <proof prover="1"><result status="valid" time="0.01" steps="13"/></proof>
 </goal>
 </theory>
-<theory name="ArrayCursorImpl" proved="true" sum="06468482e282d9cf2035e73ba7373228">
+<theory name="ArrayCursorImpl" proved="true">
 <goal name="VC cursor" expl="VC for cursor" proved="true">
 <proof prover="1"><result status="valid" time="0.02" steps="3"/></proof>
 </goal>
@@ -136,7 +136,7 @@
 <proof prover="1"><result status="valid" time="0.02" steps="12"/></proof>
 </goal>
 </theory>
-<theory name="TestArrayCursor" proved="true" sum="e8bf3a2e2fb131431b5954f022a066e5">
+<theory name="TestArrayCursor" proved="true">
 <goal name="VC array_sum" expl="VC for array_sum" proved="true">
 <transf name="split_goal_wp" proved="true" >
  <goal name="VC array_sum.0" expl="loop invariant init" proved="true">
@@ -172,7 +172,7 @@
 <proof prover="0"><result status="valid" time="0.16"/></proof>
 </goal>
 </theory>
-<theory name="TestArrayCursorLink" proved="true" sum="bd5b8257a304b6e001c68fe1ad36299a">
+<theory name="TestArrayCursorLink" proved="true">
 <goal name="TestArrayCursor.ArrayCursor.VC create" expl="VC for create" proved="true">
 <proof prover="1"><result status="valid" time="0.02" steps="27"/></proof>
 </goal>

--- a/examples/cursor_examples/why3shapes.gz
+++ b/examples/cursor_examples/why3shapes.gz
--- a/examples/double_wp/specs/why3session.xml
+++ b/examples/double_wp/specs/why3session.xml
--- a/examples/double_wp/specs/why3shapes.gz
+++ b/examples/double_wp/specs/why3shapes.gz
--- a/examples/hackers-delight/why3session.xml
+++ b/examples/hackers-delight/why3session.xml
@@ -7,7 +7,7 @@
 <prover id="8" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="9" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
 <file name="../hackers-delight.mlw" proved="true">
-<theory name="Utils" proved="true" sum="972c3075733fe9f31d38e91fcbaf519e">
+<theory name="Utils" proved="true">
 <goal name="VC one" expl="VC for one" proved="true">
 <proof prover="9"><result status="valid" time="0.01"/></proof>
 </goal>
@@ -21,7 +21,7 @@
 <proof prover="9"><result status="valid" time="0.00"/></proof>
 </goal>
 </theory>
-<theory name="Utils_Spec" proved="true" sum="1a44322a4c14c032381964bab04cbb16">
+<theory name="Utils_Spec" proved="true">
 <goal name="countZero" proved="true">
 <proof prover="9"><result status="valid" time="0.01"/></proof>
 </goal>
@@ -120,7 +120,7 @@
 <proof prover="3"><result status="valid" time="0.55" steps="635"/></proof>
 </goal>
 </theory>
-<theory name="Hackers_delight" proved="true" sum="8e10c18280320677d8bd71ff4ab7a3a7">
+<theory name="Hackers_delight" proved="true">
 <goal name="VC ascii" expl="VC for ascii" proved="true">
 <proof prover="9"><result status="valid" time="0.03"/></proof>
 </goal>

--- a/examples/hackers-delight/why3shapes.gz
+++ b/examples/hackers-delight/why3shapes.gz
--- a/examples/logic/my_cosine/why3session.xml
+++ b/examples/logic/my_cosine/why3session.xml
@@ -7,7 +7,7 @@
 <prover id="3" name="MetiTarski" version="2.4" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="5" name="Alt-Ergo" version="0.99.1" timelimit="3" steplimit="0" memlimit="0"/>
 <file name="../my_cosine.why" proved="true">
-<theory name="CosineSingle" proved="true" sum="f993602bc7dfd9a1a0a5ab763a7ed8f0">
+<theory name="CosineSingle" proved="true">
 <goal name="MethodError" proved="true">
 <proof prover="2" edited="my_cosine_CosineSingle_MethodError_1.v"><result status="valid" time="1.77"/></proof>
 <proof prover="3"><result status="valid" time="0.24"/></proof>

--- a/examples/logic/my_cosine/why3shapes.gz
+++ b/examples/logic/my_cosine/why3shapes.gz
--- a/examples/my_cosine/why3session.xml
+++ b/examples/my_cosine/why3session.xml
@@ -7,7 +7,7 @@
 <prover id="2" name="MetiTarski" version="2.4" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="3" name="Coq" version="8.7.1" timelimit="5" steplimit="0" memlimit="1000"/>
 <file name="../my_cosine.mlw" proved="true">
-<theory name="M" proved="true" sum="d6caf7544f00612e4560de6d360dd49a">
+<theory name="M" proved="true">
 <goal name="VC my_cosine" expl="VC for my_cosine" proved="true">
 <transf name="split_goal_wp" proved="true" >
  <goal name="VC my_cosine.0" expl="assertion" proved="true">

--- a/examples/my_cosine/why3shapes.gz
+++ b/examples/my_cosine/why3shapes.gz
--- a/examples/queens_bv/why3session.xml
+++ b/examples/queens_bv/why3session.xml
@@ -13,9 +13,9 @@