update sessions, CVC4 option --inst-when=full-last-call not really convincing

examples/bitvectors/bitvector.why

@@ -509,6 +509,6 @@ end
 
 (*
 Local Variables:
-compile-command: "why3ide -L . bitvector.why"
+compile-command: "why3 ide -L . bitvector.why"
 End:
 *)

examples/linear_probing/why3session.xml

@@ -462,7 +462,6 @@
   <proof prover="3"><result status="valid" time="0.09"/></proof>
   </goal>
   <goal name="WP_parameter add.15" expl="15. type invariant">
-  <proof prover="2" timelimit="10" memlimit="1000"><result status="valid" time="0.54"/></proof>
   <proof prover="3" timelimit="10"><result status="valid" time="0.66"/></proof>
   <proof prover="4"><result status="valid" time="0.44"/></proof>
   </goal>
@@ -1404,10 +1403,10 @@
   <proof prover="5"><result status="valid" time="0.03"/></proof>
   </goal>
   <goal name="WP_parameter remove.13" expl="13. precondition">
-  <proof prover="5"><result status="valid" time="0.04"/></proof>
+  <proof prover="5"><result status="valid" time="0.02"/></proof>
   </goal>
   <goal name="WP_parameter remove.14" expl="14. precondition">
-  <proof prover="5"><result status="valid" time="0.02"/></proof>
+  <proof prover="5"><result status="valid" time="0.04"/></proof>
   </goal>
   <goal name="WP_parameter remove.15" expl="15. precondition">
   <proof prover="5"><result status="valid" time="0.03"/></proof>

examples/logic/bitvectors/why3session.xml

@@ -9,74 +9,61 @@
 <file name="../bitvectors.why" expanded="true">
 <theory name="TestBV" sum="d318f02c83a7261b5dc501a4a7f36ac8" expanded="true">
  <goal name="g1">
- <proof prover="0"><result status="timeout" time="4.81"/></proof>
  <proof prover="2"><result status="valid" time="0.00"/></proof>
  <proof prover="3"><result status="valid" time="0.01"/></proof>
  </goal>
- <goal name="f1" expanded="true">
- <proof prover="0"><result status="timeout" time="4.98"/></proof>
- <proof prover="2"><result status="timeout" time="4.91"/></proof>
+ <goal name="f1">
+ <proof prover="0"><result status="timeout" time="3.80"/></proof>
+ <proof prover="2"><result status="timeout" time="5.97"/></proof>
  <proof prover="3"><result status="timeout" time="4.97"/></proof>
  </goal>
  <goal name="g2">
- <proof prover="0"><result status="timeout" time="4.97"/></proof>
  <proof prover="2"><result status="valid" time="0.00"/></proof>
  <proof prover="3"><result status="valid" time="0.01"/></proof>
  </goal>
- <goal name="f2" expanded="true">
- <proof prover="0"><result status="timeout" time="4.94"/></proof>
+ <goal name="f2">
+ <proof prover="0"><result status="timeout" time="3.57"/></proof>
  <proof prover="2"><result status="timeout" time="5.99"/></proof>
  <proof prover="3"><result status="timeout" time="5.01"/></proof>
  </goal>
  <goal name="g3">
- <proof prover="0"><result status="timeout" time="4.98"/></proof>
  <proof prover="2"><result status="valid" time="0.01"/></proof>
  <proof prover="3"><result status="valid" time="0.01"/></proof>
  </goal>
  <goal name="g4">
- <proof prover="0"><result status="timeout" time="4.91"/></proof>
  <proof prover="2"><result status="valid" time="0.01"/></proof>
  <proof prover="3"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="g3a">
- <proof prover="0"><result status="timeout" time="4.89"/></proof>
  <proof prover="2"><result status="valid" time="0.00"/></proof>
  <proof prover="3"><result status="valid" time="0.01"/></proof>
  </goal>
  <goal name="g3b">
- <proof prover="0"><result status="timeout" time="4.98"/></proof>
  <proof prover="2"><result status="valid" time="0.00"/></proof>
  <proof prover="3"><result status="valid" time="0.01"/></proof>
  </goal>
  <goal name="g3c">
- <proof prover="0"><result status="timeout" time="4.97"/></proof>
  <proof prover="2"><result status="valid" time="0.00"/></proof>
  <proof prover="3"><result status="valid" time="0.01"/></proof>
  </goal>
  <goal name="g4a">
- <proof prover="0"><result status="timeout" time="4.94"/></proof>
  <proof prover="2"><result status="valid" time="0.00"/></proof>
  <proof prover="3"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="g4b">
- <proof prover="0"><result status="timeout" time="4.90"/></proof>
  <proof prover="2"><result status="valid" time="0.00"/></proof>
  <proof prover="3"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="g5a">
- <proof prover="0"><result status="timeout" time="4.96"/></proof>
  <proof prover="2"><result status="valid" time="0.01"/></proof>
  <proof prover="3"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="g5b">
- <proof prover="0"><result status="timeout" time="5.00"/></proof>
  <proof prover="2"><result status="valid" time="0.01"/></proof>
  <proof prover="3"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="g6a">
  <proof prover="0"><result status="valid" time="0.03" steps="15"/></proof>
- <proof prover="2"><result status="timeout" time="6.01"/></proof>
- <proof prover="3"><result status="timeout" time="5.01"/></proof>
  </goal>
  <goal name="g6b">
  <proof prover="0"><result status="valid" time="0.02" steps="3"/></proof>
@@ -85,21 +72,19 @@
  </goal>
  <goal name="g7a">
  <proof prover="0"><result status="valid" time="0.02" steps="13"/></proof>
- <proof prover="2"><result status="timeout" time="6.00"/></proof>
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
  </goal>
  <goal name="g7b" expanded="true">
- <proof prover="0"><result status="timeout" time="4.76"/></proof>
+ <proof prover="0"><result status="timeout" time="3.69"/></proof>
  <proof prover="2"><result status="timeout" time="6.00"/></proof>
  <proof prover="3"><result status="timeout" time="5.00"/></proof>
  </goal>
  <goal name="g8a" expanded="true">
- <proof prover="0"><result status="timeout" time="4.96"/></proof>
+ <proof prover="0"><result status="timeout" time="3.80"/></proof>
  <proof prover="2"><result status="timeout" time="5.98"/></proof>
  <proof prover="3"><result status="timeout" time="5.01"/></proof>
  </goal>
  <goal name="g8b" expanded="true">
- <proof prover="0"><result status="timeout" time="4.98"/></proof>
+ <proof prover="0"><result status="timeout" time="3.83"/></proof>
  <proof prover="2"><result status="timeout" time="5.98"/></proof>
  <proof prover="3"><result status="timeout" time="5.00"/></proof>
  </goal>
@@ -124,44 +109,36 @@
  <proof prover="3"><result status="valid" time="0.01"/></proof>
  </goal>
  <goal name="not_not">
- <proof prover="0"><result status="timeout" time="4.91"/></proof>
  <proof prover="2"><result status="valid" time="0.00"/></proof>
  <proof prover="3"><result status="valid" time="0.00"/></proof>
  </goal>
  <goal name="not_and">
- <proof prover="0"><result status="timeout" time="4.93"/></proof>
  <proof prover="2"><result status="valid" time="0.00"/></proof>
  <proof prover="3"><result status="valid" time="0.01"/></proof>
  </goal>
- <goal name="Lsr_nth_low" expanded="true">
+ <goal name="Lsr_nth_low">
  <proof prover="0"><result status="valid" time="0.02" steps="12"/></proof>
- <proof prover="2"><result status="timeout" time="5.98"/></proof>
  <proof prover="3"><result status="valid" time="0.00"/></proof>
  </goal>
- <goal name="Lsr_nth_high" expanded="true">
+ <goal name="Lsr_nth_high">
  <proof prover="0"><result status="valid" time="0.02" steps="9"/></proof>
  <proof prover="1"><result status="valid" time="0.01"/></proof>
- <proof prover="2"><result status="timeout" time="5.98"/></proof>
  <proof prover="3"><result status="valid" time="0.00"/></proof>
  </goal>
- <goal name="Asr_nth_low" expanded="true">
+ <goal name="Asr_nth_low">
  <proof prover="0"><result status="valid" time="0.02" steps="14"/></proof>
- <proof prover="2"><result status="timeout" time="6.00"/></proof>
  <proof prover="3"><result status="valid" time="0.01"/></proof>
  </goal>
- <goal name="Asr_nth_high" expanded="true">
+ <goal name="Asr_nth_high">
  <proof prover="0"><result status="valid" time="0.04" steps="13"/></proof>
- <proof prover="2"><result status="timeout" time="5.99"/></proof>
  <proof prover="3"><result status="valid" time="0.00"/></proof>
  </goal>
- <goal name="Lsl_nth_high" expanded="true">
+ <goal name="Lsl_nth_high">
  <proof prover="0"><result status="valid" time="0.04" steps="13"/></proof>
- <proof prover="2"><result status="timeout" time="5.99"/></proof>
  <proof prover="3"><result status="valid" time="0.00"/></proof>
  </goal>
- <goal name="Lsl_nth_low" expanded="true">
+ <goal name="Lsl_nth_low">
  <proof prover="0"><result status="valid" time="0.02" steps="9"/></proof>
- <proof prover="2"><result status="timeout" time="6.00"/></proof>
  <proof prover="3"><result status="valid" time="0.00"/></proof>
  </goal>
 </theory>

share/provers-detection-data.conf

@@ -98,6 +98,7 @@ version_ok  = "1.5-prerelease"
 version_ok  = "1.4"
 driver = "drivers/cvc4.drv"
 # --random-seed=42 is not needed as soon as --random-freq=0.0 by default
+# to try: --inst-when=full-last-call 
 command = "%l/why3-cpulimit %T %m -s %e --tlimit-per=%t000 --lang=smt2 %f"
 
 # CVC4 version 1.0 to 1.3