session update

examples/binary_search/why3session.xml

@@ -4,106 +4,105 @@
 <why3session shape_version="4">
 <prover id="0" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
 <prover id="1" name="Z3" version="4.3.1" timelimit="10" memlimit="1000"/>
-<prover id="2" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
-<prover id="3" name="CVC4" version="1.3" timelimit="10" memlimit="1000"/>
+<prover id="2" name="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
+<prover id="3" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
+<prover id="4" name="CVC4" version="1.3" timelimit="10" memlimit="1000"/>
 <file name="../binary_search.mlw" expanded="true">
 <theory name="BinarySearch" sum="6edf021e1310395e54f253f514978225" expanded="true">
  <goal name="WP_parameter binary_search" expl="VC for binary_search" expanded="true">
  <proof prover="1"><result status="valid" time="0.02"/></proof>
- <proof prover="2" timelimit="10"><result status="valid" time="0.17"/></proof>
- <proof prover="3"><result status="valid" time="0.03"/></proof>
+ <proof prover="3" timelimit="10"><result status="valid" time="0.17"/></proof>
+ <proof prover="4"><result status="valid" time="0.03"/></proof>
  </goal>
 </theory>
 <theory name="BinarySearchAnyMidPoint" sum="cf35a6556f511e3fa459bea0349c2cf8" expanded="true">
  <goal name="WP_parameter binary_search" expl="VC for binary_search" expanded="true">
  <proof prover="1"><result status="valid" time="0.02"/></proof>
- <proof prover="2" timelimit="10"><result status="valid" time="0.02"/></proof>
- <proof prover="3"><result status="valid" time="0.03"/></proof>
+ <proof prover="3" timelimit="10"><result status="valid" time="0.02"/></proof>
+ <proof prover="4"><result status="valid" time="0.03"/></proof>
  </goal>
 </theory>
-<theory name="BinarySearchInt32" sum="b925c06b9515754650453539b3a5bc0f" expanded="true">
+<theory name="BinarySearchInt32" sum="642f4f476a562fd749a936e9ac849abb" expanded="true">
  <goal name="WP_parameter binary_search" expl="VC for binary_search" expanded="true">
- <proof prover="1"><result status="valid" time="0.01"/></proof>
- <proof prover="3"><result status="valid" time="0.22"/></proof>
  <transf name="split_goal_wp" expanded="true">
   <goal name="WP_parameter binary_search.1" expl="1. integer overflow">
-  <proof prover="2"><result status="valid" time="0.02" steps="2"/></proof>
+  <proof prover="3"><result status="valid" time="0.02" steps="5"/></proof>
   </goal>
   <goal name="WP_parameter binary_search.2" expl="2. integer overflow">
-  <proof prover="2"><result status="valid" time="0.01" steps="4"/></proof>
+  <proof prover="3"><result status="valid" time="0.01" steps="7"/></proof>
   </goal>
   <goal name="WP_parameter binary_search.3" expl="3. integer overflow">
-  <proof prover="2"><result status="valid" time="0.01" steps="19"/></proof>
+  <proof prover="3"><result status="valid" time="0.01" steps="24"/></proof>
   </goal>
   <goal name="WP_parameter binary_search.4" expl="4. loop invariant init">
-  <proof prover="2"><result status="valid" time="0.01" steps="7"/></proof>
+  <proof prover="3"><result status="valid" time="0.01" steps="10"/></proof>
   </goal>
   <goal name="WP_parameter binary_search.5" expl="5. loop invariant init">
-  <proof prover="2"><result status="valid" time="0.01" steps="10"/></proof>
+  <proof prover="3"><result status="valid" time="0.01" steps="13"/></proof>
   </goal>
   <goal name="WP_parameter binary_search.6" expl="6. integer overflow">
-  <proof prover="2"><result status="valid" time="0.02" steps="12"/></proof>
+  <proof prover="3"><result status="valid" time="0.02" steps="15"/></proof>
   </goal>
   <goal name="WP_parameter binary_search.7" expl="7. integer overflow">
-  <proof prover="2"><result status="valid" time="0.02" steps="18"/></proof>
+  <proof prover="3"><result status="valid" time="0.02" steps="21"/></proof>
   </goal>
   <goal name="WP_parameter binary_search.8" expl="8. division by zero">
-  <proof prover="2"><result status="valid" time="0.01" steps="15"/></proof>
+  <proof prover="3"><result status="valid" time="0.01" steps="18"/></proof>
   </goal>
   <goal name="WP_parameter binary_search.9" expl="9. integer overflow">
-  <proof prover="2"><result status="valid" time="0.04" steps="31"/></proof>
+  <proof prover="3"><result status="valid" time="0.04" steps="34"/></proof>
   </goal>
   <goal name="WP_parameter binary_search.10" expl="10. integer overflow">
-  <proof prover="2"><result status="valid" time="0.56" steps="45"/></proof>
+  <proof prover="3"><result status="valid" time="0.85" steps="50"/></proof>
   </goal>
   <goal name="WP_parameter binary_search.11" expl="11. assertion">
-  <proof prover="2"><result status="valid" time="0.92" steps="63"/></proof>
+  <proof prover="3"><result status="valid" time="1.55" steps="70"/></proof>
   </goal>
   <goal name="WP_parameter binary_search.12" expl="12. index in array bounds">
-  <proof prover="2"><result status="valid" time="0.01" steps="22"/></proof>
+  <proof prover="3"><result status="valid" time="0.01" steps="25"/></proof>
   </goal>
   <goal name="WP_parameter binary_search.13" expl="13. integer overflow">
-  <proof prover="2"><result status="valid" time="0.01" steps="26"/></proof>
+  <proof prover="3"><result status="valid" time="0.01" steps="29"/></proof>
   </goal>
   <goal name="WP_parameter binary_search.14" expl="14. integer overflow">
-  <proof prover="2"><result status="valid" time="0.03" steps="43"/></proof>
+  <proof prover="3"><result status="valid" time="0.03" steps="46"/></proof>
   </goal>
   <goal name="WP_parameter binary_search.15" expl="15. loop invariant preservation">
-  <proof prover="2"><result status="valid" time="0.02" steps="30"/></proof>
+  <proof prover="3"><result status="valid" time="0.02" steps="33"/></proof>
   </goal>
   <goal name="WP_parameter binary_search.16" expl="16. loop invariant preservation">
   <proof prover="0"><result status="valid" time="0.04"/></proof>
-  <proof prover="1" timelimit="5"><result status="valid" time="0.02"/></proof>
-  <proof prover="2"><result status="valid" time="6.82" steps="106"/></proof>
+  <proof prover="2"><result status="valid" time="0.02"/></proof>
+  <proof prover="3"><result status="valid" time="9.67" steps="113"/></proof>
   </goal>
   <goal name="WP_parameter binary_search.17" expl="17. loop variant decrease">
-  <proof prover="2"><result status="valid" time="0.02" steps="30"/></proof>
+  <proof prover="3"><result status="valid" time="0.02" steps="33"/></proof>
   </goal>
   <goal name="WP_parameter binary_search.18" expl="18. index in array bounds">
-  <proof prover="2"><result status="valid" time="0.01" steps="26"/></proof>
+  <proof prover="3"><result status="valid" time="0.01" steps="29"/></proof>
   </goal>
   <goal name="WP_parameter binary_search.19" expl="19. integer overflow">
-  <proof prover="2"><result status="valid" time="0.01" steps="28"/></proof>
+  <proof prover="3"><result status="valid" time="0.01" steps="31"/></proof>
   </goal>
   <goal name="WP_parameter binary_search.20" expl="20. integer overflow">
-  <proof prover="2"><result status="valid" time="0.02" steps="32"/></proof>
+  <proof prover="3"><result status="valid" time="0.02" steps="35"/></proof>
   </goal>
   <goal name="WP_parameter binary_search.21" expl="21. loop invariant preservation">
-  <proof prover="2"><result status="valid" time="0.02" steps="32"/></proof>
+  <proof prover="3"><result status="valid" time="0.02" steps="35"/></proof>
   </goal>
   <goal name="WP_parameter binary_search.22" expl="22. loop invariant preservation">
   <proof prover="0"><result status="valid" time="0.04"/></proof>
-  <proof prover="1" timelimit="5"><result status="valid" time="0.02"/></proof>
-  <proof prover="2" timelimit="60"><result status="valid" time="9.98" steps="107"/></proof>
+  <proof prover="2"><result status="valid" time="0.02"/></proof>
+  <proof prover="3" timelimit="60"><result status="valid" time="12.11" steps="114"/></proof>
   </goal>
   <goal name="WP_parameter binary_search.23" expl="23. loop variant decrease">
-  <proof prover="2"><result status="valid" time="0.02" steps="32"/></proof>
+  <proof prover="3"><result status="valid" time="0.02" steps="35"/></proof>
   </goal>
   <goal name="WP_parameter binary_search.24" expl="24. postcondition">
-  <proof prover="2"><result status="valid" time="1.37" steps="57"/></proof>
+  <proof prover="3"><result status="valid" time="2.32" steps="62"/></proof>
   </goal>
   <goal name="WP_parameter binary_search.25" expl="25. exceptional postcondition">
-  <proof prover="2"><result status="valid" time="0.01" steps="21"/></proof>
+  <proof prover="3"><result status="valid" time="0.01" steps="24"/></proof>
   </goal>
  </transf>
  </goal>

examples/logic/bitvectors/why3session.xml

@@ -5,18 +5,16 @@
 <prover id="0" name="CVC3" version="2.4.1" timelimit="23" memlimit="1000"/>
 <prover id="1" name="CVC4" version="1.4" timelimit="3" memlimit="1000"/>
 <file name="../bitvectors.why" expanded="true">
-<theory name="TestBV" sum="a3a3c64f3ddb46c570b66630b2934e91" expanded="true">
+<theory name="TestBV" sum="9c3a1e0f691b7f969589746c99343436" expanded="true">
  <goal name="g1">
  <proof prover="1"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="f1" expanded="true">
- <proof prover="1" timelimit="98"><result status="unknown" time="0.00"/></proof>
  </goal>
  <goal name="g2">
  <proof prover="1"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="f2" expanded="true">
- <proof prover="1" timelimit="98"><result status="unknown" time="0.00"/></proof>
  </goal>
  <goal name="g3">
  <proof prover="1"><result status="valid" time="0.01"/></proof>
@@ -54,14 +52,14 @@
  <goal name="g7a">
  <proof prover="1"><result status="valid" time="0.01"/></proof>
  </goal>
- <goal name="g7b">
- <proof prover="1"><result status="valid" time="0.01"/></proof>
+ <goal name="g7b" expanded="true">
+ <proof prover="1"><result status="timeout" time="2.96"/></proof>
  </goal>
- <goal name="g8a">
- <proof prover="1"><result status="valid" time="0.01"/></proof>
+ <goal name="g8a" expanded="true">
+ <proof prover="1"><result status="timeout" time="2.93"/></proof>
  </goal>
- <goal name="g8b">
- <proof prover="1"><result status="valid" time="0.00"/></proof>
+ <goal name="g8b" expanded="true">
+ <proof prover="1"><result status="timeout" time="3.01"/></proof>
  </goal>
  <goal name="Nth_bw_and">
  <proof prover="1"><result status="valid" time="0.16"/></proof>
@@ -70,10 +68,10 @@
  <proof prover="1"><result status="valid" time="0.16"/></proof>
  </goal>
  <goal name="Nth_bw_xor">
- <proof prover="1"><result status="valid" time="0.17"/></proof>
+ <proof prover="1"><result status="valid" time="0.04"/></proof>
  </goal>
  <goal name="Nth_bw_not">
- <proof prover="1" timelimit="5"><result status="valid" time="1.15"/></proof>
+ <proof prover="1" timelimit="5"><result status="valid" time="0.04"/></proof>
  </goal>
  <goal name="not_not">
  <proof prover="1"><result status="valid" time="0.00"/></proof>
@@ -83,19 +81,16 @@
  </goal>
  <goal name="Lsr_nth_low" expanded="true">
  </goal>
- <goal name="Lsr_nth_high">
- <proof prover="0"><result status="valid" time="0.01"/></proof>
- <proof prover="1" timelimit="98"><result status="valid" time="6.43"/></proof>
+ <goal name="Lsr_nth_high" expanded="true">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.01"/></proof>
  </goal>
  <goal name="Asr_nth_low" expanded="true">
  </goal>
- <goal name="Asr_nth_high">
- <proof prover="1" timelimit="98"><result status="valid" time="6.67"/></proof>
+ <goal name="Asr_nth_high" expanded="true">
  </goal>
  <goal name="Lsl_nth_high" expanded="true">
  </goal>
- <goal name="Lsl_nth_low">
- <proof prover="1" timelimit="98"><result status="valid" time="5.83"/></proof>
+ <goal name="Lsl_nth_low" expanded="true">
  </goal>
 </theory>
 </file>