replay obsolete sessions

examples/add_list/why3session.xml

@@ -7,9 +7,9 @@
 <file name="../add_list.mlw">
 <theory name="SumList" sum="d41d8cd98f00b204e9800998ecf8427e">
 </theory>
-<theory name="AddListRec" sum="b22282c439ddd5fa9976e2048ec06a22">
+<theory name="AddListRec" sum="33def14244e48e7a03216981ac5000bf">
  <goal name="VC sum" expl="VC for sum">
- <proof prover="1"><result status="valid" time="0.02" steps="200"/></proof>
+ <proof prover="1"><result status="valid" time="0.02" steps="93"/></proof>
  </goal>
  <goal name="VC main" expl="VC for main">
  <proof prover="4"><result status="valid" time="0.02"/></proof>

examples/add_list_vc_sp/why3session.xml

@@ -6,7 +6,7 @@
 <file name="../add_list.mlw" expanded="true">
 <theory name="SumList" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
 </theory>
-<theory name="AddListRec" sum="b22282c439ddd5fa9976e2048ec06a22" expanded="true">
+<theory name="AddListRec" sum="33def14244e48e7a03216981ac5000bf" expanded="true">
  <goal name="VC sum" expl="VC for sum" expanded="true">
  <proof prover="0"><result status="valid" time="0.01"/></proof>
  </goal>

examples/avl/avl/why3session.xml

@@ -18,7 +18,7 @@
  <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
  </goal>
 </theory>
-<theory name="AVL" sum="5c4f65ebf2e6b589c75fa1089472090c">
+<theory name="AVL" sum="685a6c3f9ca1d8850254333db1860c27">
  <goal name="M.M.assoc">
  <proof prover="0"><result status="valid" time="0.00" steps="3"/></proof>
  </goal>
@@ -51,22 +51,22 @@
  </transf>
  </goal>
  <goal name="VC height" expl="VC for height">
- <proof prover="0"><result status="valid" time="0.02" steps="38"/></proof>
+ <proof prover="0"><result status="valid" time="0.02" steps="30"/></proof>
  </goal>
  <goal name="VC total" expl="VC for total">
- <proof prover="0"><result status="valid" time="0.02" steps="53"/></proof>
+ <proof prover="0"><result status="valid" time="0.02" steps="36"/></proof>
  </goal>
  <goal name="VC empty" expl="VC for empty">
  <proof prover="0"><result status="valid" time="0.01" steps="11"/></proof>
  </goal>
  <goal name="VC node" expl="VC for node">
- <proof prover="0"><result status="valid" time="0.19" steps="735"/></proof>
+ <proof prover="0"><result status="valid" time="0.19" steps="736"/></proof>
  </goal>
  <goal name="VC singleton" expl="VC for singleton">
  <proof prover="0"><result status="valid" time="0.04" steps="133"/></proof>
  </goal>
  <goal name="VC is_empty" expl="VC for is_empty">
- <proof prover="0"><result status="valid" time="0.05" steps="188"/></proof>
+ <proof prover="0"><result status="valid" time="0.05" steps="78"/></proof>
  </goal>
  <goal name="VC view" expl="VC for view">
  <proof prover="0"><result status="valid" time="0.15" steps="648"/></proof>
@@ -152,13 +152,13 @@
  <proof prover="0"><result status="valid" time="0.05" steps="292"/></proof>
  </goal>
  <goal name="VC front_node" expl="VC for front_node">
- <proof prover="0"><result status="valid" time="0.49" steps="1375"/></proof>
+ <proof prover="0"><result status="valid" time="0.26" steps="893"/></proof>
  </goal>
  <goal name="VC front" expl="VC for front">
  <proof prover="0"><result status="valid" time="0.08" steps="362"/></proof>
  </goal>
  <goal name="VC back_node" expl="VC for back_node">
- <proof prover="0"><result status="valid" time="0.47" steps="1827"/></proof>
+ <proof prover="0"><result status="valid" time="0.18" steps="715"/></proof>
  </goal>
  <goal name="VC back" expl="VC for back">
  <proof prover="0"><result status="valid" time="0.07" steps="289"/></proof>

examples/avl/ral/why3session.xml

@@ -4,7 +4,7 @@
 <why3session shape_version="4">
 <prover id="0" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
 <file name="../ral.mlw">
-<theory name="RAL" sum="769655d14c868c857a9fda205481fb0e">
+<theory name="RAL" sum="8eef46a79b8f7e645bf03e91400b9f70">
  <goal name="VC balancing" expl="VC for balancing">
  <proof prover="0"><result status="valid" time="0.01" steps="2"/></proof>
  </goal>
@@ -114,7 +114,7 @@
  <proof prover="0"><result status="valid" time="0.38" steps="359"/></proof>
  </goal>
  <goal name="VC cut" expl="VC for cut">
- <proof prover="0"><result status="valid" time="0.09" steps="160"/></proof>
+ <proof prover="0"><result status="valid" time="0.09" steps="176"/></proof>
  </goal>
  <goal name="VC split" expl="VC for split">
  <proof prover="0"><result status="valid" time="0.15" steps="352"/></proof>

examples/balance/why3session.xml

@@ -6,17 +6,17 @@
 <file name="../balance.mlw" expanded="true">
 <theory name="Roberval" sum="d41d8cd98f00b204e9800998ecf8427e">
 </theory>
-<theory name="Puzzle8" sum="529d834734aa7045534ccf52130e5eb9">
+<theory name="Puzzle8" sum="acd846f51dd7305d4e569d48197b6c46">
  <goal name="VC solve3" expl="VC for solve3">
- <proof prover="0"><result status="valid" time="0.02" steps="43"/></proof>
+ <proof prover="0"><result status="valid" time="0.02" steps="47"/></proof>
  </goal>
  <goal name="VC solve8" expl="VC for solve8">
- <proof prover="0"><result status="valid" time="0.13" steps="316"/></proof>
+ <proof prover="0"><result status="valid" time="0.13" steps="291"/></proof>
  </goal>
 </theory>
-<theory name="Puzzle12" sum="f0a7106c4fceecb1b95ba5be2438a922" expanded="true">
+<theory name="Puzzle12" sum="3d382d4e673bb394fa271044f818889c" expanded="true">
  <goal name="VC solve12" expl="VC for solve12" expanded="true">
- <proof prover="0"><result status="valid" time="0.53" steps="1365"/></proof>
+ <proof prover="0"><result status="valid" time="0.53" steps="1379"/></proof>
  </goal>
 </theory>
 </file>

examples/binomial_heap/why3session.xml

@@ -7,7 +7,7 @@
 <prover id="3" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/>
 <prover id="4" name="Z3" version="4.5.0" timelimit="10" steplimit="0" memlimit="1000"/>
 <file name="../binomial_heap.mlw" expanded="true">
-<theory name="BinomialHeap" sum="45554a82ba10188a7d3dfa00cfdf7286" expanded="true">
+<theory name="BinomialHeap" sum="a4b20c3f0b661937cb05ebc19298c2ba" expanded="true">
  <goal name="VC size_nonnneg" expl="VC for size_nonnneg">
  <proof prover="4"><result status="valid" time="0.02"/></proof>
  </goal>
@@ -109,7 +109,7 @@
  <proof prover="3"><result status="valid" time="0.00" steps="7"/></proof>
  </goal>
  <goal name="VC is_empty" expl="VC for is_empty">
- <proof prover="3"><result status="valid" time="0.00" steps="10"/></proof>
+ <proof prover="3"><result status="valid" time="0.00" steps="9"/></proof>
  </goal>
  <goal name="VC get_min" expl="VC for get_min" expanded="true">
  <transf name="split_goal_wp" expanded="true">
@@ -117,16 +117,16 @@
   <proof prover="3"><result status="valid" time="0.01" steps="6"/></proof>
   </goal>
   <goal name="VC get_min.2" expl="2. variant decrease">
-  <proof prover="3"><result status="valid" time="0.01" steps="35"/></proof>
+  <proof prover="3"><result status="valid" time="0.01" steps="39"/></proof>
   </goal>
   <goal name="VC get_min.3" expl="3. precondition">
-  <proof prover="3"><result status="valid" time="0.01" steps="28"/></proof>
+  <proof prover="3"><result status="valid" time="0.01" steps="30"/></proof>
   </goal>
   <goal name="VC get_min.4" expl="4. postcondition">
-  <proof prover="3"><result status="valid" time="0.05" steps="267"/></proof>
+  <proof prover="3"><result status="valid" time="0.05" steps="268"/></proof>
   </goal>
   <goal name="VC get_min.5" expl="5. postcondition">
-  <proof prover="3"><result status="valid" time="0.01" steps="66"/></proof>
+  <proof prover="3"><result status="valid" time="0.01" steps="68"/></proof>
   </goal>
   <goal name="VC get_min.6" expl="6. postcondition">
   <proof prover="0"><result status="valid" time="0.17"/></proof>

examples/bitwalker/why3session.xml

@@ -13,7 +13,7 @@
 <prover id="8" name="Z3" version="4.4.1" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="10" name="Z3" version="4.4.1" alternative="noBV" timelimit="5" steplimit="0" memlimit="1000"/>
 <file name="../bitwalker.mlw" expanded="true">
-<theory name="Bitwalker" sum="93070dfac506ec3d4f12e20b1e0b9066" expanded="true">
+<theory name="Bitwalker" sum="9e2086079d345ddc6500bd6ac11fac30" expanded="true">
  <goal name="nth64">
  <proof prover="0"><result status="valid" time="0.10" steps="93"/></proof>
  </goal>
@@ -118,7 +118,7 @@
   <proof prover="3"><result status="valid" time="0.04"/></proof>
   </goal>
   <goal name="VC peek_8bit_array.4" expl="4. precondition">
-  <proof prover="0"><result status="valid" time="0.41" steps="235"/></proof>
+  <proof prover="0"><result status="valid" time="0.26" steps="235"/></proof>
   <proof prover="1"><result status="valid" time="0.04"/></proof>
   <proof prover="3"><result status="valid" time="1.86"/></proof>
   </goal>

examples/braun_trees/why3session.xml

@@ -4,7 +4,7 @@
 <why3session shape_version="4">
 <prover id="1" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/>
 <file name="../braun_trees.mlw" expanded="true">
-<theory name="BraunHeaps" sum="f177abc1e5a75c4bf82a7c9f28ad6ac1" expanded="true">
+<theory name="BraunHeaps" sum="320a27ff6d5b9e231da1e9f9dee7818c" expanded="true">
  <goal name="VC le_root" expl="VC for le_root">
  <proof prover="1"><result status="valid" time="0.00" steps="1"/></proof>
  </goal>
@@ -154,13 +154,7 @@
   <proof prover="1"><result status="valid" time="0.01" steps="29"/></proof>
   </goal>
   <goal name="VC inv_height.6" expl="6. postcondition">
-  <proof prover="1"><result status="valid" time="0.00" steps="12"/></proof>
-  </goal>
-  <goal name="VC inv_height.7" expl="7. postcondition">
-  <proof prover="1"><result status="valid" time="0.04" steps="159"/></proof>
-  </goal>
-  <goal name="VC inv_height.8" expl="8. postcondition">
-  <proof prover="1"><result status="valid" time="0.44" steps="655"/></proof>
+  <proof prover="1"><result status="valid" time="4.97" steps="860"/></proof>
   </goal>
  </transf>
  </goal>

examples/defunctionalization/why3session.xml

@@ -83,7 +83,7 @@
  <proof prover="7"><result status="valid" time="0.00" steps="3"/></proof>
  </goal>
 </theory>
-<theory name="Defunctionalization2" sum="452f3010cc715691d650a4d90535b500">
+<theory name="Defunctionalization2" sum="1ae50e29b78cebd4b83add8b50c6c1b9">
  <goal name="VC continue_2" expl="VC for continue_2">
  <proof prover="7"><result status="valid" time="0.01" steps="107"/></proof>
  </goal>
@@ -96,10 +96,7 @@
   <proof prover="5"><result status="valid" time="0.02"/></proof>
   </goal>
   <goal name="VC eval_2.3" expl="3. postcondition">
-  <proof prover="7"><result status="valid" time="0.00" steps="6"/></proof>
-  </goal>
-  <goal name="VC eval_2.4" expl="4. postcondition">
-  <proof prover="7"><result status="valid" time="0.01" steps="44"/></proof>
+  <proof prover="7"><result status="valid" time="0.00" steps="49"/></proof>
   </goal>
  </transf>
  </goal>
@@ -110,7 +107,7 @@
  <proof prover="7"><result status="valid" time="0.00" steps="3"/></proof>
  </goal>
 </theory>
-<theory name="SemWithError" sum="b86f86d1abcb9f97e04b692072fcf03b">
+<theory name="SemWithError" sum="f788ff531e8c29e783e8622c79efd2b2">
  <goal name="cps_correct_expr">
  <transf name="induction_ty_lex">
   <goal name="cps_correct_expr.1" expl="1.">
@@ -171,10 +168,14 @@
   <proof prover="7"><result status="valid" time="0.00" steps="4"/></proof>
   </goal>
   <goal name="VC cps3_correct_expr.4" expl="4. postcondition">
-  <proof prover="7"><result status="valid" time="0.01" steps="63"/></proof>
-  </goal>
-  <goal name="VC cps3_correct_expr.5" expl="5. postcondition">
-  <proof prover="8"><result status="valid" time="0.02"/></proof>
+  <transf name="split_goal_wp">
+   <goal name="VC cps3_correct_expr.4.1" expl="1. postcondition">
+   <proof prover="7" timelimit="1"><result status="valid" time="0.01" steps="63"/></proof>
+   </goal>
+   <goal name="VC cps3_correct_expr.4.2" expl="2. postcondition">
+   <proof prover="8" timelimit="1"><result status="valid" time="0.02"/></proof>
+   </goal>
+  </transf>
   </goal>
  </transf>
  </goal>
@@ -211,7 +212,7 @@
  <proof prover="7"><result status="valid" time="0.01" steps="6"/></proof>
  </goal>
 </theory>
-<theory name="ReductionSemantics" sum="9befb0000a357d06f2d94c2dd253a939">
+<theory name="ReductionSemantics" sum="15be8583204c6ed0a3ea83deeb164c25">
  <goal name="VC contract" expl="VC for contract">
  <proof prover="7"><result status="valid" time="0.01" steps="44"/></proof>
  </goal>
@@ -269,10 +270,10 @@
  <proof prover="7"><result status="valid" time="0.00" steps="6"/></proof>
  </goal>
  <goal name="VC eval_1" expl="VC for eval_1">
- <proof prover="7"><result status="valid" time="0.05" steps="256"/></proof>
+ <proof prover="7"><result status="valid" time="0.05" steps="51"/></proof>
  </goal>
  <goal name="VC eval_2" expl="VC for eval_2">
- <proof prover="7"><result status="valid" time="0.04" steps="309"/></proof>
+ <proof prover="7"><result status="valid" time="0.04" steps="111"/></proof>
  </goal>
  <goal name="VC interpret" expl="VC for interpret">
  <proof prover="7"><result status="valid" time="0.00" steps="6"/></proof>
@@ -281,7 +282,7 @@
  <proof prover="7"><result status="valid" time="0.00" steps="5"/></proof>
  </goal>
 </theory>
-<theory name="RWithError" sum="cfcdc98bfe63794ead6150e4c6560971">
+<theory name="RWithError" sum="b06c96afc6649d4980932257e8e75eda">
  <goal name="size_c_pos">
  <transf name="induction_ty_lex">
   <goal name="size_c_pos.1" expl="1.">

examples/esterel/why3session.xml

@@ -6,12 +6,12 @@
 <prover id="1" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="4000" memlimit="4000"/>
 <prover id="2" name="Z3" version="4.4.1" timelimit="5" steplimit="4000" memlimit="4000"/>
 <file name="../esterel.mlw" expanded="true">
-<theory name="Esterel" sum="1b203f09cfa5ce87bbfdb875a8522626" expanded="true">
+<theory name="Esterel" sum="fa333b2c6770e50cc56ebdc816c82165" expanded="true">
  <goal name="VC union" expl="VC for union">
- <proof prover="1"><result status="valid" time="0.16" steps="197"/></proof>
+ <proof prover="1"><result status="valid" time="0.16" steps="268"/></proof>
  </goal>
  <goal name="VC intersection" expl="VC for intersection">
- <proof prover="1"><result status="valid" time="0.18" steps="175"/></proof>
+ <proof prover="1"><result status="valid" time="0.18" steps="194"/></proof>
  </goal>
  <goal name="VC aboveMin" expl="VC for aboveMin">
  <transf name="split_goal_wp">
@@ -23,13 +23,13 @@
   </goal>
   <goal name="VC aboveMin.3" expl="3. assertion">
   <proof prover="0"><result status="valid" time="0.22"/></proof>
-  <proof prover="2"><result status="valid" time="0.52"/></proof>
+  <proof prover="2"><result status="valid" time="0.31"/></proof>
   </goal>
   <goal name="VC aboveMin.4" expl="4. assertion">
-  <proof prover="0"><result status="valid" time="0.42"/></proof>
+  <proof prover="0"><result status="valid" time="0.19"/></proof>
   </goal>
   <goal name="VC aboveMin.5" expl="5. precondition">
-  <proof prover="1"><result status="valid" time="0.30" steps="303"/></proof>
+  <proof prover="1"><result status="valid" time="0.30" steps="305"/></proof>
   </goal>
   <goal name="VC aboveMin.6" expl="6. postcondition">
   <proof prover="0"><result status="valid" time="0.03"/></proof>
@@ -52,11 +52,10 @@
   </goal>
   <goal name="VC maxUnion.3" expl="3. assertion">
   <proof prover="0"><result status="valid" time="0.25"/></proof>
-  <proof prover="2"><result status="valid" time="0.60"/></proof>
+  <proof prover="2"><result status="valid" time="0.40"/></proof>
   </goal>
   <goal name="VC maxUnion.4" expl="4. postcondition">
-  <proof prover="0"><result status="valid" time="0.27"/></proof>
-  <proof prover="1"><result status="valid" time="1.54" steps="1796"/></proof>
+  <proof prover="1"><result status="valid" time="1.54" steps="2018"/></proof>
   </goal>
   <goal name="VC maxUnion.5" expl="5. postcondition">
   <transf name="split_goal_wp">
@@ -64,8 +63,8 @@
    <proof prover="0"><result status="valid" time="0.06"/></proof>
    </goal>
    <goal name="VC maxUnion.5.2" expl="2. postcondition">
-   <proof prover="0"><result status="valid" time="0.34"/></proof>
-   <proof prover="1"><result status="valid" time="0.52" steps="531"/></proof>
+   <proof prover="0"><result status="valid" time="0.06"/></proof>
+   <proof prover="1"><result status="valid" time="0.28" steps="334"/></proof>
    </goal>
   </transf>
   </goal>

examples/fact/why3session.xml

@@ -4,9 +4,9 @@
 <why3session shape_version="4">
 <prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
 <file name="../fact.mlw" expanded="true">
-<theory name="FactRecursive" sum="c39fb2621594abeb3f19e95ac1288b76" expanded="true">
+<theory name="FactRecursive" sum="a92ceed0d292e759dd1b722f5be697f6" expanded="true">
  <goal name="VC fact_rec" expl="VC for fact_rec" expanded="true">
- <proof prover="1"><result status="valid" time="0.01" steps="9"/></proof>
+ <proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
  </goal>
  <goal name="VC test0" expl="VC for test0" expanded="true">
  <proof prover="1"><result status="valid" time="0.00" steps="0"/></proof>

examples/fact_vc_sp/why3session.xml

@@ -4,9 +4,9 @@
 <why3session shape_version="4">
 <prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
 <file name="../fact.mlw" expanded="true">
-<theory name="FactRecursive" sum="c39fb2621594abeb3f19e95ac1288b76" expanded="true">
+<theory name="FactRecursive" sum="a92ceed0d292e759dd1b722f5be697f6" expanded="true">
  <goal name="VC fact_rec" expl="VC for fact_rec" expanded="true">
- <proof prover="0"><result status="valid" time="0.02" steps="9"/></proof>
+ <proof prover="0"><result status="valid" time="0.02" steps="16"/></proof>
  </goal>
  <goal name="VC test0" expl="VC for test0" expanded="true">
  <proof prover="0"><result status="valid" time="0.01" steps="0"/></proof>

examples/fibonacci/why3session.xml

@@ -2,36 +2,32 @@
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="4">
+<prover id="0" name="Z3" version="4.5.0" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="1" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
-<prover id="2" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="0"/>
-<prover id="4" name="Spass" version="3.7" timelimit="5" steplimit="0" memlimit="0"/>
 <prover id="5" name="Z3" version="4.4.1" timelimit="1" steplimit="0" memlimit="1000"/>
-<prover id="7" name="Vampire" version="0.6" timelimit="5" steplimit="0" memlimit="0"/>
-<prover id="8" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="0"/>
 <prover id="9" name="CVC4" version="1.4" timelimit="1" steplimit="0" memlimit="1000"/>
-<prover id="10" name="Eprover" version="1.8-001" timelimit="5" steplimit="0" memlimit="0"/>
 <file name="../fibonacci.mlw" expanded="true">
 <theory name="FibonacciTest" sum="9fccb254fa2218a4d5027f25371577ce">
  <goal name="isfib_2_1">
- <proof prover="2"><result status="valid" time="0.00"/></proof>
+ <proof prover="0"><result status="valid" time="0.01"/></proof>
+ <proof prover="9" timelimit="5"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="isfib_6_8">
- <proof prover="2"><result status="valid" time="0.00"/></proof>
+ <proof prover="0"><result status="valid" time="0.01"/></proof>
+ <proof prover="9" timelimit="5"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="not_isfib_2_2">
- <proof prover="2"><result status="valid" time="0.00"/></proof>
- <proof prover="4"><result status="valid" time="0.02"/></proof>
- <proof prover="7"><result status="valid" time="0.03"/></proof>
- <proof prover="8"><result status="valid" time="0.01" steps="4"/></proof>
- <proof prover="10"><result status="valid" time="0.01"/></proof>
+ <proof prover="0"><result status="valid" time="0.01"/></proof>
+ <proof prover="1"><result status="valid" time="0.00" steps="5"/></proof>
+ <proof prover="9" timelimit="5"><result status="valid" time="0.00"/></proof>
  </goal>
 </theory>
-<theory name="FibonacciLinear" sum="c9e19a22319be9ef88c46d978d0995ed">
+<theory name="FibonacciLinear" sum="477dec7d3a1032ce41e6959cb270849b">
  <goal name="VC fib" expl="VC for fib">
  <proof prover="5"><result status="valid" time="0.01"/></proof>
  </goal>
 </theory>
-<theory name="FibRecGhost" sum="f718edddcf68c63fea7b9d428fbfcd58">
+<theory name="FibRecGhost" sum="3534a72ab694e460197a46dfd750efa2">
  <goal name="VC fib_aux" expl="VC for fib_aux">
  <proof prover="5"><result status="valid" time="0.01"/></proof>
  </goal>
@@ -58,7 +54,7 @@
  <proof prover="5"><result status="valid" time="0.12"/></proof>
  </goal>
 </theory>
-<theory name="Zeckendorf" sum="5ddad8520526669f3f6943865980d5ec">
+<theory name="Zeckendorf" sum="ded49788e228303bcb5c25257ccddedf">
  <goal name="VC fib_nonneg" expl="VC for fib_nonneg">
  <proof prover="1"><result status="valid" time="0.00" steps="21"/></proof>
  </goal>
@@ -107,7 +103,7 @@
   <proof prover="5"><result status="valid" time="0.01"/></proof>
   </goal>
   <goal name="VC zeckendorf_unique.11" expl="11. precondition">
-  <proof prover="5"><result status="valid" time="0.01"/></proof>
+  <proof prover="5"><result status="valid" time="0.02"/></proof>
   </goal>
   <goal name="VC zeckendorf_unique.12" expl="12. unreachable point">
   <proof prover="5"><result status="valid" time="0.01"/></proof>
@@ -116,7 +112,7 @@
   <proof prover="5"><result status="valid" time="0.01"/></proof>
   </goal>
   <goal name="VC zeckendorf_unique.14" expl="14. precondition">
-  <proof prover="5"><result status="valid" time="0.01"/></proof>
+  <proof prover="5"><result status="valid" time="0.02"/></proof>
   </goal>
   <goal name="VC zeckendorf_unique.15" expl="15. precondition">
   <proof prover="5"><result status="valid" time="0.02"/></proof>
@@ -131,13 +127,13 @@
   <proof prover="5"><result status="valid" time="0.01"/></proof>
   </goal>
   <goal name="VC zeckendorf_unique.19" expl="19. precondition">
-  <proof prover="5"><result status="valid" time="0.02"/></proof>
+  <proof prover="5"><result status="valid" time="0.01"/></proof>
   </goal>
   <goal name="VC zeckendorf_unique.20" expl="20. precondition">
   <proof prover="5"><result status="valid" time="0.01"/></proof>
   </goal>
   <goal name="VC zeckendorf_unique.21" expl="21. precondition">
-  <proof prover="5"><result status="valid" time="0.02"/></proof>
+  <proof prover="5"><result status="valid" time="0.01"/></proof>
   </goal>
   <goal name="VC zeckendorf_unique.22" expl="22. precondition">
   <proof prover="5"><result status="valid" time="0.02"/></proof>
@@ -154,9 +150,6 @@
   <goal name="VC zeckendorf_unique.26" expl="26. postcondition">
   <proof prover="5"><result status="valid" time="0.02"/></proof>
   </goal>
-  <goal name="VC zeckendorf_unique.27" expl="27. postcondition">
-  <proof prover="5"><result status="valid" time="0.02"/></proof>
-  </goal>
  </transf>
  </goal>
 </theory>
@@ -171,7 +164,7 @@
  <proof prover="1"><result status="valid" time="0.00" steps="2"/></proof>
  </goal>
 </theory>
-<theory name="FibonacciLogarithmic" sum="72613a172df1afd4bbe89937f60d1bde" expanded="true">
+<theory name="FibonacciLogarithmic" sum="6997a4bbb411ae9d62554c252c4c4b21">
  <goal name="VC m1110" expl="VC for m1110">
  <proof prover="1"><result status="valid" time="0.00" steps="3"/></proof>
  </goal>
@@ -199,13 +192,7 @@
   <proof prover="1"><result status="valid" time="0.00" steps="8"/></proof>
   </goal>
   <goal name="VC logfib.8" expl="8. postcondition">
-  <proof prover="1"><result status="valid" time="0.01" steps="8"/></proof>
-  </goal>
-  <goal name="VC logfib.9" expl="9. postcondition">
-  <proof prover="1"><result status="valid" time="0.03" steps="31"/></proof>
-  </goal>
-  <goal name="VC logfib.10" expl="10. postcondition">
-  <proof prover="1"><result status="valid" time="0.17" steps="63"/></proof>
+  <proof prover="1"><result status="valid" time="0.29" steps="90"/></proof>
   </goal>
  </transf>
  </goal>
@@ -213,7 +200,7 @@
  <proof prover="5"><result status="valid" time="0.02"/></proof>
  </goal>
  <goal name="VC fibo" expl="VC for fibo">
- <proof prover="1"><result status="valid" time="0.00" steps="6"/></proof>
+ <proof prover="1"><result status="valid" time="0.00" steps="7"/></proof>
  </goal>
  <goal name="VC test0" expl="VC for test0">
  <proof prover="1"><result status="valid" time="0.00" steps="3"/></proof>

examples/finger_trees/why3session.xml

@@ -4,12 +4,12 @@
 <why3session shape_version="4">
 <prover id="3" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
 <file name="../finger_trees.mlw">
-<theory name="FingerTrees" sum="bc4cfeb4a57bb9b172602a713c4bf5ce">
+<theory name="FingerTrees" sum="972ee04a0205e46808ba090f45d7e401">
  <goal name="VC node_cons_app" expl="VC for node_cons_app">
- <proof prover="3"><result status="valid" time="0.05" steps="300"/></proof>
+ <proof prover="3"><result status="valid" time="0.05" steps="165"/></proof>
  </goal>
  <goal name="VC d_cons" expl="VC for d_cons">
- <proof prover="3"><result status="valid" time="0.32" steps="2032"/></proof>
+ <proof prover="3"><result status="valid" time="0.12" steps="1042"/></proof>
  </goal>
  <goal name="VC cons" expl="VC for cons">
  <proof prover="3"><result status="valid" time="0.30" steps="1665"/></proof>

examples/flag2/why3session.xml

@@ -4,9 +4,9 @@
 <why3session shape_version="4">
 <prover id="4" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
 <file name="../flag2.mlw" expanded="true">
-<theory name="Flag" sum="9757fb3372f54b9b756af254a3e55b6b" expanded="true">
+<theory name="Flag" sum="f3fc9a0195561c4dfc306fc66bb7d2c3" expanded="true">
  <goal name="VC eq_color" expl="VC for eq_color">
- <proof prover="4"><result status="valid" time="0.00" steps="6"/></proof>
+ <proof prover="4"><result status="valid" time="0.00" steps="11"/></proof>
  </goal>
  <goal name="VC nb_occ" expl="VC for nb_occ">
  <proof prover="4"><result status="valid" time="0.00" steps="4"/></proof>

examples/gcd/why3session.xml

@@ -7,9 +7,9 @@
 <prover id="8" name="Spass" version="3.7" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="9" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
 <file name="../gcd.mlw" expanded="true">
-<theory name="EuclideanAlgorithm" sum="06c09424aee65c6f411f277cd3f59aaf">
+<theory name="EuclideanAlgorithm" sum="b19fdaf810947d1effcb1fb33e3d7e49">
  <goal name="VC euclid" expl="VC for euclid">
- <proof prover="8"><result status="valid" time="4.32"/></proof>
+ <proof prover="8"><result status="valid" time="8.35"/></proof>
  </goal>
 </theory>
 <theory name="EuclideanAlgorithmIterative" sum="4841a879f96158e78cf1e196ec0e2c3b">
@@ -17,7 +17,7 @@
  <proof prover="4"><result status="valid" time="0.02"/></proof>
  </goal>
 </theory>
-<theory name="BinaryGcd" sum="a78066797db663add80796b90f60375c" expanded="true">
+<theory name="BinaryGcd" sum="bd104d3dd00bc2d7a3faa1d20c49e676" expanded="true">
  <goal name="even1">
  <proof prover="9"><result status="valid" time="0.01" steps="19"/></proof>
  </goal>
@@ -101,44 +101,13 @@
   <goal name="VC binary_gcd.18" expl="18. precondition">
   <proof prover="9"><result status="valid" time="0.01" steps="12"/></proof>
   </goal>
-  <goal name="VC binary_gcd.19" expl="19. postcondition">
-  <proof prover="9"><result status="valid" time="0.01" steps="8"/></proof>
-  </goal>
-  <goal name="VC binary_gcd.20" expl="20. postcondition">
-  <proof prover="9"><result status="valid" time="0.01" steps="16"/></proof>
-  </goal>
-  <goal name="VC binary_gcd.21" expl="21. postcondition" expanded="true">
-  </goal>
-  <goal name="VC binary_gcd.22" expl="22. postcondition" expanded="true">
+  <goal name="VC binary_gcd.19" expl="19. postcondition" expanded="true">
   </goal>
  </transf>
  </goal>
 </theory>
-<theory name="EuclideanAlgorithm31" sum="9daace546ea2d1640762b559418142ef">
- <goal name="VC euclid" expl="VC for euclid">
- <transf name="split_goal_wp">
-  <goal name="VC euclid.1" expl="1. integer overflow">
-  <proof prover="9"><result status="valid" time="0.00" steps="4"/></proof>
-  </goal>
-  <goal name="VC euclid.2" expl="2. division by zero">
-  <proof prover="9"><result status="valid" time="0.00" steps="6"/></proof>
-  </goal>
-  <goal name="VC euclid.3" expl="3. integer overflow">
-  <proof prover="9"><result status="valid" time="0.04" steps="49"/></proof>
-  </goal>
-  <goal name="VC euclid.4" expl="4. variant decrease">
-  <proof prover="9"><result status="valid" time="0.05" steps="54"/></proof>
-  </goal>
-  <goal name="VC euclid.5" expl="5. precondition">
-  <proof prover="9"><result status="valid" time="0.00" steps="15"/></proof>
-  </goal>
-  <goal name="VC euclid.6" expl="6. postcondition">
-  <proof prover="9"><result status="valid" time="0.01" steps="13"/></proof>
-  </goal>
-  <goal name="VC euclid.7" expl="7. postcondition">
-  <proof prover="9"><result status="valid" time="0.02" steps="29"/></proof>
-  </goal>
- </transf>
+<theory name="EuclideanAlgorithm63" sum="f64eaee885c2c0c2efa1917cecd2eaf2" expanded="true">
+ <goal name="VC euclid" expl="VC for euclid" expanded="true">
  </goal>
 </theory>
 </file>

examples/kmp/why3session.xml

@@ -7,7 +7,7 @@
 <prover id="6" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="7" name="Z3" version="4.5.0" timelimit="5" steplimit="0" memlimit="1000"/>
 <file name="../kmp.mlw" expanded="true">
-<theory name="KnuthMorrisPratt" sum="992003785c920e9f6d507a64c4e4f98d" expanded="true">
+<theory name="KnuthMorrisPratt" sum="f276d11fbb35618780dbe50cca350ace" expanded="true">
  <goal name="matches_empty">
  <proof prover="6"><result status="valid" time="0.00" steps="7"/></proof>
  </goal>
@@ -37,7 +37,7 @@
  <proof prover="7"><result status="valid" time="0.02"/></proof>
  </goal>
  <goal name="next_is_maximal">
- <proof prover="0" edited="kmp_WP_KnuthMorrisPratt_next_is_maximal_1.v"><result status="valid" time="0.36"/></proof>
+ <proof prover="0" edited="kmp_WP_KnuthMorrisPratt_next_is_maximal_1.v"><result status="valid" time="0.20"/></proof>
  </goal>
  <goal name="next_1_0">
  <proof prover="6"><result status="valid" time="0.00" steps="8"/></proof>
@@ -187,7 +187,7 @@
   <goal name="VC kmp.19" expl="19. loop invariant preservation" expanded="true">
   </goal>
   <goal name="VC kmp.20" expl="20. postcondition">
-  <proof prover="6"><result status="valid" time="0.02" steps="107"/></proof>
+  <proof prover="6"><result status="valid" time="0.02" steps="71"/></proof>
   <proof prover="7"><result status="valid" time="0.02"/></proof>
   </goal>
  </transf>

examples/leftist_heap/why3session.xml

@@ -37,7 +37,7 @@
  </transf>
  </goal>
 </theory>
-<theory name="LeftistHeap" sum="4b29c9f09b718ff373a4f107f510eee4">
+<theory name="LeftistHeap" sum="53b5fc576f978ed69cac60e05557921c">
  <goal name="le_root_trans">
  <proof prover="2"><result status="valid" time="0.00" steps="17"/></proof>
  </goal>
@@ -48,13 +48,13 @@
  <proof prover="2"><result status="valid" time="0.00" steps="11"/></proof>
  </goal>
  <goal name="VC is_empty" expl="VC for is_empty">
- <proof prover="2"><result status="valid" time="0.00" steps="10"/></proof>
+ <proof prover="2"><result status="valid" time="0.00" steps="14"/></proof>
  </goal>
  <goal name="VC rank" expl="VC for rank">
- <proof prover="2"><result status="valid" time="0.01" steps="39"/></proof>
+ <proof prover="2"><result status="valid" time="0.01" steps="24"/></proof>
  </goal>
  <goal name="VC make_n" expl="VC for make_n">
- <proof prover="2"><result status="valid" time="0.06" steps="239"/></proof>
+ <proof prover="2"><result status="valid" time="0.06" steps="199"/></proof>
  </goal>
  <goal name="VC merge" expl="VC for merge">
  <transf name="split_goal_wp">

examples/mccarthy/why3session.xml

@@ -4,9 +4,9 @@
 <why3session shape_version="4">
 <prover id="1" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/>
 <file name="../mccarthy.mlw" expanded="true">
-<theory name="McCarthy91" sum="5b1f487792b978b7733e7ca6ae2116f9" expanded="true">
+<theory name="McCarthy91" sum="4bf37421b34f376a63d8dd5cb7d4186f" expanded="true">
  <goal name="VC f91" expl="VC for f91" expanded="true">
- <proof prover="1"><result status="valid" time="0.00" steps="17"/></proof>
+ <proof prover="1"><resul