updated sessions after upgrade Alt-Ergo 0.95 -> 0.95.1 and Z3 4.2 -> 4.3.1

2c89a558 · MARCHE Claude · 0bf9e3cb · 2c89a558 · 2c89a558 · 2c89a558
Commit 2c89a558 authored Mar 11, 2013 by MARCHE Claude
67 changed files
--- a/examples/assigning_meanings_to_programs/why3session.xml
+++ b/examples/assigning_meanings_to_programs/why3session.xml
@@ -8,7 +8,7 @@
 <prover
  id="1"
  name="CVC3"
-  version="2.2"/>
+  version="2.4.1"/>
 <file
  name="../assigning_meanings_to_programs.mlw"
  verified="true"

--- a/examples/binary_sqrt/why3session.xml
+++ b/examples/binary_sqrt/why3session.xml
@@ -8,7 +8,7 @@
 <prover
  id="1"
  name="Z3"
-  version="4.2"/>
+  version="4.3.1"/>
 <file
  name="../binary_sqrt.mlw"
  verified="true"

--- a/examples/bitvectors/double_of_int/why3session.xml
+++ b/examples/bitvectors/double_of_int/why3session.xml
@@ -8,7 +8,7 @@
 <prover
  id="1"
  name="Alt-Ergo"
-  version="0.95"/>
+  version="0.95.1"/>
 <prover
  id="2"
  name="CVC3"
@@ -36,13 +36,13 @@
 <file
  name="../double_of_int.why"
  verified="true"
-  expanded="false">
+  expanded="true">
  <theory
   name="DoubleOfInt"
   locfile="../double_of_int.why"
   loclnum="3" loccnumb="7" loccnume="18"
   verified="true"
-   expanded="false">
+   expanded="true">
   <goal
    name="nth_j1"
    locfile="../double_of_int.why"
@@ -65,7 +65,7 @@
     memlimit="1000"
     obsolete="false"
     archived="false">
-     <result status="valid" time="1.06"/>
+     <result status="valid" time="0.43"/>
    </proof>
   </goal>
   <goal
@@ -90,7 +90,7 @@
     memlimit="1000"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.57"/>
+     <result status="valid" time="0.26"/>
    </proof>
   </goal>
   <goal
@@ -115,7 +115,7 @@
     memlimit="1000"
     obsolete="false"
     archived="false">
-     <result status="valid" time="1.08"/>
+     <result status="valid" time="0.42"/>
    </proof>
   </goal>
   <goal
@@ -140,7 +140,7 @@
     memlimit="1000"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.55"/>
+     <result status="valid" time="0.26"/>
    </proof>
   </goal>
   <goal
@@ -165,7 +165,7 @@
     memlimit="1000"
     obsolete="false"
     archived="false">
-     <result status="valid" time="1.25"/>
+     <result status="valid" time="0.41"/>
    </proof>
   </goal>
   <goal
@@ -215,7 +215,7 @@
     memlimit="1000"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.92"/>
+     <result status="valid" time="0.27"/>
    </proof>
   </goal>
   <goal
@@ -240,7 +240,7 @@
     memlimit="1000"
     obsolete="false"
     archived="false">
-     <result status="valid" time="1.09"/>
+     <result status="valid" time="0.54"/>
    </proof>
   </goal>
   <goal
@@ -265,7 +265,7 @@
     memlimit="1000"
     obsolete="false"
     archived="false">
-     <result status="valid" time="32.13"/>
+     <result status="valid" time="11.53"/>
    </proof>
   </goal>
   <goal
@@ -290,7 +290,7 @@
     memlimit="1000"
     obsolete="false"
     archived="false">
-     <result status="valid" time="7.94"/>
+     <result status="valid" time="3.93"/>
    </proof>
   </goal>
   <goal
@@ -720,7 +720,7 @@
     memlimit="1000"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.31"/>
+     <result status="valid" time="0.53"/>
    </proof>
    <proof
     prover="2"
@@ -875,7 +875,7 @@
     memlimit="1000"
     obsolete="false"
     archived="false">
-     <result status="valid" time="13.18"/>
+     <result status="valid" time="0.08"/>
    </proof>
   </goal>
   <goal
@@ -900,7 +900,7 @@
     memlimit="1000"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.32"/>
+     <result status="valid" time="0.55"/>
    </proof>
    <proof
     prover="2"
@@ -1048,7 +1048,7 @@
    loclnum="112" loccnumb="8" loccnume="17"
    sum="e22085e8f3ba93ee49bb2395a10e30bb"
    proved="true"
-    expanded="false"
+    expanded="true"
    shape="ainfix =anthajpxorV0c31anotbanthafrom_int2cV0c31F">
    <proof
     prover="0"
@@ -1058,14 +1058,6 @@
     archived="false">
     <result status="valid" time="0.59"/>
    </proof>
-    <proof
-     prover="1"
-     timelimit="3"
-     memlimit="1000"
-     obsolete="false"
-     archived="false">
-     <result status="valid" time="0.74"/>
-    </proof>
   </goal>
   <goal
    name="to_nat_sub_0_30"
@@ -1083,14 +1075,6 @@
     archived="false">
     <result status="valid" time="0.15"/>
    </proof>
-    <proof
-     prover="1"
-     timelimit="3"
-     memlimit="1000"
-     obsolete="false"
-     archived="false">
-     <result status="valid" time="0.23"/>
-    </proof>
    <proof
     prover="6"
     timelimit="5"
@@ -1130,7 +1114,7 @@
     memlimit="1000"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.33"/>
+     <result status="valid" time="1.82"/>
    </proof>
    <proof
     prover="2"
@@ -1357,7 +1341,7 @@
     memlimit="1000"
     obsolete="false"
     archived="false">
-     <result status="valid" time="1.90"/>
+     <result status="valid" time="35.51"/>
    </proof>
   </goal>
   <goal
@@ -1466,7 +1450,7 @@
    loclnum="195" loccnumb="8" loccnume="21"
    sum="d70afd68b851ef6c395e8be6f2d5f5b3"
    proved="true"
-    expanded="false"
+    expanded="true"
    shape="ainfix =anthavarV0V1anthajainfix -V1c32Iainfix &lt;=V1c63Aainfix &lt;=c32V1F">
    <proof
     prover="0"
@@ -1476,14 +1460,6 @@
     archived="false">
     <result status="valid" time="5.91"/>
    </proof>
-    <proof
-     prover="1"
-     timelimit="60"
-     memlimit="1000"
-     obsolete="false"
-     archived="false">
-     <result status="valid" time="5.87"/>
-    </proof>
   </goal>
   <goal
    name="nth_var3"
@@ -1507,7 +1483,7 @@
     memlimit="1000"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.39"/>
+     <result status="valid" time="1.40"/>
    </proof>
   </goal>
   <goal
@@ -1550,7 +1526,7 @@
     memlimit="1000"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.34"/>
+     <result status="valid" time="1.48"/>
    </proof>
   </goal>
   <goal
@@ -1575,7 +1551,7 @@
     memlimit="1000"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.31"/>
+     <result status="valid" time="1.50"/>
    </proof>
   </goal>
   <goal
@@ -1600,7 +1576,7 @@
     memlimit="1000"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.26"/>
+     <result status="valid" time="1.48"/>
    </proof>
   </goal>
   <goal
@@ -1625,7 +1601,7 @@
     memlimit="1000"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.19"/>
+     <result status="valid" time="1.47"/>
    </proof>
   </goal>
   <goal

--- a/examples/bitvectors/neg_as_xor/why3session.xml
+++ b/examples/bitvectors/neg_as_xor/why3session.xml
@@ -8,7 +8,7 @@
 <prover
  id="1"
  name="Alt-Ergo"
-  version="0.95"/>
+  version="0.95.1"/>
 <prover
  id="2"
  name="Coq"
@@ -53,7 +53,7 @@
     memlimit="1000"
     obsolete="false"
     archived="false">
-     <result status="valid" time="1.02"/>
+     <result status="valid" time="0.34"/>
    </proof>
   </goal>
   <goal
@@ -370,7 +370,7 @@
     edited="neg_as_xor_TestNegAsXOR_MainResult_1.v"
     obsolete="false"
     archived="false">
-     <result status="valid" time="1.46"/>
+     <result status="valid" time="1.20"/>
    </proof>
   </goal>
  </theory>

--- a/examples/bresenham/why3session.xml
+++ b/examples/bresenham/why3session.xml
@@ -8,7 +8,7 @@
 <prover
  id="1"
  name="CVC3"
-  version="2.2"/>
+  version="2.4.1"/>
 <prover
  id="2"
  name="Coq"

--- a/examples/bts/12475/why3session.xml
+++ b/examples/bts/12475/why3session.xml
@@ -8,7 +8,7 @@
 <prover
  id="1"
  name="CVC3"
-  version="2.2"/>
+  version="2.4.1"/>
 <prover
  id="2"
  name="Gappa"

--- a/examples/check-builtin/ac/why3session.xml
+++ b/examples/check-builtin/ac/why3session.xml
@@ -8,7 +8,7 @@
 <prover
  id="1"
  name="CVC3"
-  version="2.2"/>
+  version="2.4.1"/>
 <prover
  id="2"
  name="Spass"

--- a/examples/check-builtin/bool/why3session.xml
+++ b/examples/check-builtin/bool/why3session.xml
@@ -8,7 +8,7 @@
 <prover
  id="1"
  name="CVC3"
-  version="2.2"/>
+  version="2.4.1"/>
 <prover
  id="2"
  name="Spass"

--- a/examples/check-builtin/euclideandivision/why3session.xml
+++ b/examples/check-builtin/euclideandivision/why3session.xml
@@ -8,11 +8,11 @@
 <prover
  id="1"
  name="Alt-Ergo"
-  version="0.95"/>
+  version="0.95.1"/>
 <prover
  id="2"
  name="CVC3"
-  version="2.2"/>
+  version="2.4.1"/>
 <prover
  id="3"
  name="Spass"

--- a/examples/check-builtin/floats/why3session.xml
+++ b/examples/check-builtin/floats/why3session.xml
@@ -8,7 +8,7 @@
 <prover
  id="1"
  name="CVC3"
-  version="2.2"/>
+  version="2.4.1"/>
 <prover
  id="2"
  name="Gappa"

--- a/examples/check-builtin/int/why3session.xml
+++ b/examples/check-builtin/int/why3session.xml
@@ -8,7 +8,7 @@
 <prover
  id="1"
  name="CVC3"
-  version="2.2"/>
+  version="2.4.1"/>
 <prover
  id="2"
  name="Simplify"

--- a/examples/check-builtin/minmax/why3session.xml
+++ b/examples/check-builtin/minmax/why3session.xml
@@ -8,7 +8,7 @@
 <prover
  id="1"
  name="CVC3"
-  version="2.2"/>
+  version="2.4.1"/>
 <prover
  id="2"
  name="Spass"

--- a/examples/check-builtin/propositional/why3session.xml
+++ b/examples/check-builtin/propositional/why3session.xml
@@ -8,7 +8,7 @@
 <prover
  id="1"
  name="CVC3"
-  version="2.2"/>
+  version="2.4.1"/>
 <prover
  id="2"
  name="Spass"

--- a/examples/checking_a_large_routine/why3session.xml
+++ b/examples/checking_a_large_routine/why3session.xml
@@ -8,7 +8,7 @@
 <prover
  id="1"
  name="CVC3"
-  version="2.2"/>
+  version="2.4.1"/>
 <file
  name="../checking_a_large_routine.mlw"
  verified="true"

--- a/examples/counting_sort/why3session.xml
+++ b/examples/counting_sort/why3session.xml
--- a/examples/edit_distance/why3session.xml
+++ b/examples/edit_distance/why3session.xml
@@ -8,7 +8,7 @@
 <prover
  id="1"
  name="Alt-Ergo"
-  version="0.95"/>
+  version="0.95.1"/>
 <prover
  id="2"
  name="CVC3"

--- a/examples/f_puzzle/why3session.xml
+++ b/examples/f_puzzle/why3session.xml
@@ -28,7 +28,7 @@
 <prover
  id="6"
  name="Z3"
-  version="4.2"/>
+  version="4.3.1"/>
 <file
  name="../f_puzzle.why"
  verified="true"
@@ -52,7 +52,7 @@
    loclnum="421" loccnumb="8" loccnume="12"
    sum="9fcf6bf15f06d92c3f1b7a29cbd4fad8"
    proved="true"
-    expanded="true"
+    expanded="false"
    shape="apc0">
    <proof
     prover="0"
@@ -117,7 +117,7 @@
    loclnum="423" loccnumb="8" loccnume="22"
    sum="39b97b15c2a355ba6892ba4f2f114896"
    proved="true"
-    expanded="true"
+    expanded="false"
    shape="apainfix +V0c1IapV0Iainfix &lt;=c0V0F">
    <proof
     prover="5"
@@ -381,14 +381,6 @@
     archived="false">
     <result status="valid" time="0.14"/>
    </proof>
-    <proof
-     prover="6"
-     timelimit="5"
-     memlimit="4000"
-     obsolete="false"
-     archived="false">
-     <result status="valid" time="0.16"/>
-    </proof>
   </goal>
  </theory>
 </file>

--- a/examples/fib_memo/why3session.xml
+++ b/examples/fib_memo/why3session.xml
@@ -8,7 +8,7 @@
 <prover
  id="1"
  name="CVC3"
-  version="2.2"/>
+  version="2.4.1"/>
 <file
  name="../fib_memo.mlw"
  verified="true"

--- a/examples/fibonacci/why3session.xml
+++ b/examples/fibonacci/why3session.xml
@@ -8,7 +8,7 @@
 <prover
  id="1"
  name="CVC3"
-  version="2.2"/>
+  version="2.4.1"/>
 <prover
  id="2"
  name="Coq"

--- a/examples/find/why3session.xml
+++ b/examples/find/why3session.xml
@@ -8,11 +8,11 @@
 <prover
  id="1"
  name="Alt-Ergo"
-  version="0.95"/>
+  version="0.95.1"/>
 <prover
  id="2"
  name="CVC3"
-  version="2.2"/>
+  version="2.4.1"/>
 <prover
  id="3"
  name="Coq"

--- a/examples/flag/why3session.xml
+++ b/examples/flag/why3session.xml
@@ -8,17 +8,13 @@
 <prover
  id="1"
  name="Alt-Ergo"
-  version="0.95"/>
+  version="0.95.1"/>
 <prover
  id="2"
  name="CVC3"
-  version="2.2"/>
- <prover
-  id="3"
-  name="CVC3"
  version="2.4.1"/>
 <prover
-  id="4"
+  id="3"
  name="Z3"
  version="2.19"/>
 <file
@@ -238,7 +234,7 @@
      <label
       name="expl:VC for dutch_flag"/>
      <proof
-       prover="4"
+       prover="3"
       timelimit="60"
       memlimit="1000"
       obsolete="false"
@@ -258,7 +254,7 @@
      <label
       name="expl:VC for dutch_flag"/>
      <proof
-       prover="4"
+       prover="3"
       timelimit="60"
       memlimit="1000"
       obsolete="false"
@@ -278,7 +274,7 @@
      <label
       name="expl:VC for dutch_flag"/>
      <proof
-       prover="4"
+       prover="3"
       timelimit="60"
       memlimit="1000"
       obsolete="false"
@@ -498,7 +494,7 @@
      <label
       name="expl:VC for dutch_flag"/>
      <proof
-       prover="4"
+       prover="3"
       timelimit="10"
       memlimit="0"
       obsolete="false"
@@ -518,7 +514,7 @@
      <label
       name="expl:VC for dutch_flag"/>
      <proof
-       prover="4"
+       prover="3"
       timelimit="8"
       memlimit="1000"
       obsolete="false"
@@ -538,7 +534,7 @@
      <label
       name="expl:VC for dutch_flag"/>
      <proof
-       prover="4"
+       prover="3"
       timelimit="60"
       memlimit="1000"
       obsolete="false"
@@ -578,7 +574,7 @@
      <label
       name="expl:VC for dutch_flag"/>
      <proof
-       prover="3"
+       prover="2"
       timelimit="8"
       memlimit="1000"
       obsolete="false"

--- a/examples/flag2/flag2_WP_Flag_nb_occ_store_eq_neq_1.v
+++ b/examples/flag2/flag2_WP_Flag_nb_occ_store_eq_neq_1.v
@@ -64,7 +64,7 @@ Axiom nb_occ_store_eq_eq : forall (a:(map.Map.map Z color)) (i:Z) (j:Z) (k:Z)

 Open Scope Z_scope.
 Require Import Why3.
-Ltac ae := why3 "Alt-Ergo,0.95," timelimit 15.
+Ltac ae := why3 "Alt-Ergo,0.95.1," timelimit 15.

 (* Why3 goal *)
 Theorem nb_occ_store_eq_neq : forall (a:(map.Map.map Z color)) (i:Z) (j:Z)

--- a/examples/foveoos11-cm/array_max/why3session.xml
+++ b/examples/foveoos11-cm/array_max/why3session.xml
@@ -8,7 +8,7 @@
 <prover
  id="1"
  name="CVC3"
-  version="2.2"/>
+  version="2.4.1"/>
 <prover
  id="2"
  name="Z3"

--- a/examples/foveoos11-cm/duplets/why3session.xml
+++ b/examples/foveoos11-cm/duplets/why3session.xml
@@ -8,7 +8,7 @@
 <prover
  id="1"
  name="CVC3"
-  version="2.2"/>
+  version="2.4.1"/>
 <prover
  id="2"
  name="Z3"

--- a/examples/foveoos11_challenge3/why3session.xml
+++ b/examples/foveoos11_challenge3/why3session.xml
@@ -8,11 +8,11 @@
 <prover
  id="1"
  name="Alt-Ergo"
-  version="0.95"/>
+  version="0.95.1"/>
 <prover
  id="2"
  name="CVC3"
-  version="2.2"/>
+  version="2.4.1"/>
 <prover
  id="3"
  name="Coq"

--- a/examples/gcd/why3session.xml
+++ b/examples/gcd/why3session.xml
@@ -8,17 +8,13 @@
 <prover
  id="1"
  name="CVC3"
-  version="2.2"/>
- <prover
-  id="2"
-  name="CVC3"
  version="2.4.1"/>
 <prover
-  id="3"
+  id="2"
  name="Coq"
  version="8.3pl4"/>
 <prover
-  id="4"
+  id="3"
  name="Z3"
  version="2.19"/>
 <file
@@ -74,7 +70,7 @@
       <result status="valid" time="0.02"/>
      </proof>
      <proof
-       prover="4"
+       prover="3"
       timelimit="10"
       memlimit="0"
       obsolete="false"
@@ -102,7 +98,7 @@
       <result status="valid" time="0.24"/>
      </proof>
      <proof
-       prover="2"
+       prover="1"