updated sessions

98d1451d · MARCHE Claude · 2c89a558 · 98d1451d · 98d1451d · 98d1451d
Commit 98d1451d authored Mar 12, 2013 by MARCHE Claude
24 changed files
--- a/examples/algo63/why3session.xml
+++ b/examples/algo63/why3session.xml
@@ -8,13 +8,9 @@
 <prover
  id="1"
  name="CVC3"
-  version="2.2"/>
- <prover
-  id="2"
-  name="CVC3"
  version="2.4.1"/>
 <prover
-  id="3"
+  id="2"
  name="Spass"
  version="3.7"/>
 <file
@@ -462,7 +458,7 @@
      <label
       name="expl:VC for partition_"/>
      <proof
-       prover="2"
+       prover="1"
       timelimit="9"
       memlimit="1000"
       obsolete="false"
@@ -2612,7 +2608,7 @@
    <label
     name="expl:VC for partition"/>
    <proof
-     prover="3"
+     prover="2"
     timelimit="10"
     memlimit="1000"
     obsolete="false"

--- a/examples/alphaBeta/why3session.xml
+++ b/examples/alphaBeta/why3session.xml
@@ -12,7 +12,7 @@
 <prover
  id="2"
  name="Alt-Ergo"
-  version="0.95"/>
+  version="0.95.1"/>
 <prover
  id="3"
  name="CVC3"
@@ -36,7 +36,7 @@
 <prover
  id="8"
  name="Z3"
-  version="4.2"/>
+  version="4.3.1"/>
 <file
  name="../alphaBeta.mlw"
  verified="false"

--- a/examples/bitvectors/bitvector/why3session.xml
+++ b/examples/bitvectors/bitvector/why3session.xml
@@ -8,7 +8,7 @@
 <prover
  id="1"
  name="Alt-Ergo"
-  version="0.95"/>
+  version="0.95.1"/>
 <prover
  id="2"
  name="CVC3"
@@ -455,7 +455,7 @@
     memlimit="1000"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.04"/>
+     <result status="valid" time="0.72"/>
    </proof>
    <proof
     prover="4"

--- a/examples/bitvectors/double/why3session.xml
+++ b/examples/bitvectors/double/why3session.xml
@@ -8,7 +8,7 @@
 <prover
  id="1"
  name="Alt-Ergo"
-  version="0.95"/>
+  version="0.95.1"/>
 <prover
  id="2"
  name="CVC3"
@@ -68,7 +68,7 @@
     memlimit="1000"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.87"/>
+     <result status="valid" time="0.33"/>
    </proof>
   </goal>
   <goal
@@ -93,7 +93,7 @@
     memlimit="1000"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.48"/>
+     <result status="valid" time="0.23"/>
    </proof>
   </goal>
   <goal

--- a/examples/bitvectors/power2/why3session.xml
+++ b/examples/bitvectors/power2/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/bts/fsetint/why3session.xml
+++ b/examples/bts/fsetint/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/check-builtin/real/why3session.xml
+++ b/examples/check-builtin/real/why3session.xml
@@ -8,7 +8,7 @@
 <prover
  id="1"
  name="Alt-Ergo"
-  version="0.95"/>
+  version="0.95.1"/>
 <prover
  id="2"
  name="CVC3"
@@ -979,7 +979,7 @@
     memlimit="1000"
     obsolete="false"
     archived="false">
-     <result status="valid" time="3.36"/>
+     <result status="valid" time="1.61"/>
    </proof>
    <proof
     prover="2"

--- a/examples/decrease1/why3session.xml
+++ b/examples/decrease1/why3session.xml
@@ -32,7 +32,7 @@
 <prover
  id="7"
  name="Z3"
-  version="4.2"/>
+  version="4.3.1"/>
 <file
  name="../decrease1.mlw"
  verified="true"
@@ -1110,7 +1110,7 @@
       memlimit="1000"
       obsolete="false"
       archived="false">
-       <result status="valid" time="0.33"/>
+       <result status="valid" time="0.50"/>
      </proof>
      <proof
       prover="7"
@@ -1118,7 +1118,7 @@
       memlimit="1000"
       obsolete="false"
       archived="false">
-       <result status="valid" time="0.80"/>
+       <result status="valid" time="1.43"/>
      </proof>
     </goal>
     <goal

--- a/examples/euler001/why3session.xml
+++ b/examples/euler001/why3session.xml
@@ -8,7 +8,7 @@
 <prover
  id="1"
  name="Alt-Ergo"
-  version="0.95"/>
+  version="0.95.1"/>
 <prover
  id="2"
  name="CVC3"
@@ -246,7 +246,7 @@
     memlimit="1000"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.20"/>
+     <result status="valid" time="0.02"/>
    </proof>
    <proof
     prover="2"
@@ -678,7 +678,7 @@
     memlimit="1000"
     obsolete="false"
     archived="false">
-     <result status="valid" time="1.37"/>
+     <result status="valid" time="0.81"/>
    </proof>
    <proof
     prover="2"

--- a/examples/euler002/why3session.xml
+++ b/examples/euler002/why3session.xml
@@ -12,7 +12,7 @@
 <prover
  id="2"
  name="Alt-Ergo"
-  version="0.95"/>
+  version="0.95.1"/>
 <prover
  id="3"
  name="CVC3"
@@ -40,7 +40,7 @@
 <prover
  id="9"
  name="Z3"
-  version="4.2"/>
+  version="4.3.1"/>
 <file
  name="../euler002.mlw"
  verified="true"
@@ -1172,7 +1172,7 @@
       memlimit="1000"
       obsolete="false"
       archived="false">
-       <result status="valid" time="0.07"/>
+       <result status="valid" time="0.28"/>
      </proof>
     </goal>
     <goal

--- a/examples/generate_all_trees/why3session.xml
+++ b/examples/generate_all_trees/why3session.xml
@@ -8,7 +8,7 @@
 <prover
  id="1"
  name="Alt-Ergo"
-  version="0.95"/>
+  version="0.95.1"/>
 <prover
  id="2"
  name="CVC3"
@@ -62,7 +62,7 @@
     edited="generate_all_trees_WP_GenerateAllTrees_size_nonneg_1.v"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.48"/>
+     <result status="valid" time="0.64"/>
    </proof>
   </goal>
   <goal

--- a/examples/hash_tables/why3session.xml
+++ b/examples/hash_tables/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/hoare_logic/blocking_semantics5/why3session.xml
+++ b/examples/hoare_logic/blocking_semantics5/why3session.xml
@@ -28,7 +28,7 @@
 <prover
  id="6"
  name="Z3"
-  version="4.2"/>
+  version="4.3.1"/>
 <file
  name="../blocking_semantics5.mlw"
  verified="true"
@@ -1790,7 +1790,7 @@
         edited="blocking_semantics5_FreshVariables_eval_msubst_2.v"
         obsolete="false"
         archived="false">
-         <result status="valid" time="1.35"/>
+         <result status="valid" time="1.61"/>
        </proof>
        <proof
         prover="5"
@@ -2110,7 +2110,7 @@
         memlimit="1000"
         obsolete="false"
         archived="false">
-         <result status="valid" time="19.63"/>
+         <result status="valid" time="6.32"/>
        </proof>
        <proof
         prover="3"
@@ -2118,7 +2118,7 @@
         memlimit="1000"
         obsolete="false"
         archived="false">
-         <result status="valid" time="7.74"/>
+         <result status="valid" time="24.44"/>
        </proof>
        <proof
         prover="5"
@@ -2205,7 +2205,7 @@
         memlimit="4000"
         obsolete="false"
         archived="false">
-         <result status="valid" time="0.30"/>
+         <result status="valid" time="0.48"/>
        </proof>
        <proof
         prover="5"
@@ -2313,7 +2313,7 @@
         memlimit="4000"
         obsolete="false"
         archived="false">
-         <result status="valid" time="9.07"/>
+         <result status="valid" time="4.21"/>
        </proof>
        <proof
         prover="3"
@@ -2371,7 +2371,7 @@
         memlimit="4000"
         obsolete="false"
         archived="false">
-         <result status="valid" time="4.04"/>
+         <result status="valid" time="8.37"/>
        </proof>
        <proof
         prover="3"
@@ -2429,7 +2429,7 @@
         memlimit="4000"
         obsolete="false"
         archived="false">
-         <result status="valid" time="4.67"/>
+         <result status="valid" time="2.52"/>
        </proof>
        <proof
         prover="3"

--- a/examples/insertion_sort/why3session.xml
+++ b/examples/insertion_sort/why3session.xml
@@ -8,7 +8,7 @@
 <prover
  id="1"
  name="Alt-Ergo"
-  version="0.95"/>
+  version="0.95.1"/>
 <prover
  id="2"
  name="CVC3"
@@ -392,7 +392,7 @@
       memlimit="1000"
       obsolete="false"
       archived="false">
-       <result status="valid" time="0.51"/>
+       <result status="valid" time="0.76"/>
      </proof>
     </goal>
     <goal
@@ -572,7 +572,7 @@
       memlimit="1000"
       obsolete="false"
       archived="false">
-       <result status="valid" time="0.79"/>
+       <result status="valid" time="1.04"/>
      </proof>
     </goal>
     <goal

--- a/examples/isqrt/why3session.xml
+++ b/examples/isqrt/why3session.xml
@@ -8,7 +8,7 @@
 <prover
  id="1"
  name="Alt-Ergo"
-  version="0.95"/>
+  version="0.95.1"/>
 <prover
  id="2"
  name="CVC3"
@@ -32,7 +32,7 @@
 <prover
  id="7"
  name="Z3"
-  version="4.2"/>
+  version="4.3.1"/>
 <file
  name="../isqrt.mlw"
  verified="false"
@@ -768,7 +768,7 @@
       memlimit="4000"
       obsolete="false"
       archived="false">
-       <result status="valid" time="0.88"/>
+       <result status="valid" time="0.53"/>
      </proof>
     </goal>
    </transf>

--- a/examples/logic/explicit_subst/why3session.xml
+++ b/examples/logic/explicit_subst/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/logic/genealogy/why3session.xml
+++ b/examples/logic/genealogy/why3session.xml
@@ -40,7 +40,7 @@
 <prover
  id="9"
  name="Z3"
-  version="4.2"/>
+  version="4.3.1"/>
 <prover
  id="10"
  name="Zenon"

--- a/examples/logic/lagrange_inequality.why
+++ b/examples/logic/lagrange_inequality.why
@@ -50,9 +50,9 @@ theory CauchySchwarzInequality
  lemma norm_pos :
     forall x1 x2:real. norm x1 x2 >= 0.0

-  (** lemma to help the next one *)
+  (** 2 lemmas to help the next one *)
  lemma sqr_le_sqrt :
-    forall x y:real. 0.0 <= x /\ 0.0 <= sqr x <= y -> x <= sqrt y
+    forall x y:real. sqr x <= y -> x <= sqrt y

  lemma CauchySchwarz:
     forall x1 x2 y1 y2 : real.

--- a/examples/logic/lagrange_inequality/why3session.xml
+++ b/examples/logic/lagrange_inequality/why3session.xml
@@ -8,7 +8,7 @@
 <prover
  id="1"
  name="Alt-Ergo"
-  version="0.95"/>
+  version="0.95.1"/>
 <prover
  id="2"
  name="CVC3"
@@ -19,10 +19,14 @@
  version="2.4.1"/>
 <prover
  id="4"
+  name="Coq"
+  version="8.3pl4"/>
+ <prover
+  id="5"
  name="Z3"
  version="2.19"/>
 <prover
-  id="5"
+  id="6"
  name="Z3"
  version="3.2"/>
 <file
@@ -34,17 +38,17 @@
   locfile="../lagrange_inequality.why"
   loclnum="3" loccnumb="7" loccnume="25"
   verified="true"
-   expanded="true">
+   expanded="false">
   <goal
    name="norm2_pos"
    locfile="../lagrange_inequality.why"
    loclnum="24" loccnumb="8" loccnume="17"
    sum="c6713b13328556e5aa44d719637857fd"
    proved="true"
-    expanded="true"
+    expanded="false"
    shape="ainfix &gt;=anorm2V0V1c0.0F">
    <proof
-     prover="4"
+     prover="5"
     timelimit="3"
     memlimit="1000"
     obsolete="false"
@@ -52,7 +56,7 @@
     <result status="valid" time="0.01"/>
    </proof>
    <proof
-     prover="5"
+     prover="6"
     timelimit="3"
     memlimit="1000"
     obsolete="false"
@@ -66,10 +70,10 @@
    loclnum="28" loccnumb="8" loccnume="16"
    sum="1a74668a6a15dfafb66a489f26ce72c0"
    proved="true"
-    expanded="true"
+    expanded="false"
    shape="ainfix =ainfix *anorm2V0V1anorm2V2V3ainfix +asqradotV0V1V2V3asqrainfix -ainfix *V0V3ainfix *V1V2F">
    <proof
-     prover="4"
+     prover="5"
     timelimit="3"
     memlimit="1000"
     obsolete="false"
@@ -77,7 +81,7 @@
     <result status="valid" time="0.00"/>
    </proof>
    <proof
-     prover="5"
+     prover="6"
     timelimit="3"
     memlimit="1000"
     obsolete="false"
@@ -98,7 +102,7 @@
    loclnum="42" loccnumb="8" loccnume="25"
    sum="8ba764166645697844f18c787d612735"
    proved="true"
-    expanded="true"
+    expanded="false"
    shape="ainfix &lt;=asqradotV0V1V2V3ainfix *anorm2V0V1anorm2V2V3F">
    <proof
     prover="2"
@@ -123,7 +127,7 @@
    loclnum="50" loccnumb="8" loccnume="16"
    sum="bae896604a117b9697d08353f3ed6435"
    proved="true"
-    expanded="true"
+    expanded="false"
    shape="ainfix &gt;=anormV0V1c0.0F">
    <proof
     prover="0"
@@ -158,7 +162,7 @@
     <result status="valid" time="0.00"/>
    </proof>
    <proof
-     prover="4"
+     prover="5"
     timelimit="3"
     memlimit="1000"
     obsolete="false"
@@ -166,7 +170,7 @@
     <result status="valid" time="0.01"/>
    </proof>
    <proof
-     prover="5"
+     prover="6"
     timelimit="3"
     memlimit="1000"
     obsolete="false"
@@ -178,34 +182,27 @@
    name="sqr_le_sqrt"
    locfile="../lagrange_inequality.why"
    loclnum="54" loccnumb="8" loccnume="19"
-    sum="26fce0e82fa8078ed602400b40d3657f"
+    sum="ce3b326b0d6887f18e3115dd235b6a7a"
    proved="true"
-    expanded="true"
-    shape="ainfix &lt;=V0asqrtV1Iainfix &lt;=asqrV0V1Aainfix &lt;=c0.0asqrV0Aainfix &lt;=c0.0V0F">
+    expanded="false"
+    shape="ainfix &lt;=V0asqrtV1Iainfix &lt;=asqrV0V1F">
    <proof
-     prover="0"
-     timelimit="3"
-     memlimit="1000"
-     obsolete="false"
-     archived="false">
-     <result status="valid" time="0.03"/>
-    </proof>
-    <proof
-     prover="1"
-     timelimit="3"
-     memlimit="1000"
+     prover="4"
+     timelimit="5"
+     memlimit="4000"
+     edited="lagrange_inequality_CauchySchwarzInequality_sqr_le_sqrt_1.v"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.02"/>
+     <result status="valid" time="1.12"/>
    </proof>
   </goal>
   <goal
    name="CauchySchwarz"
    locfile="../lagrange_inequality.why"
    loclnum="57" loccnumb="8" loccnume="21"
-    sum="10e2c2fef95a5452d73824798bd90c6a"
+    sum="3027e8050a1b1b1fae27eaacfc79e36c"
    proved="true"
-    expanded="true"
+    expanded="false"
    shape="ainfix &lt;=adotV0V1V2V3ainfix *anormV0V1anormV2V3F">
    <proof
     prover="0"
@@ -216,12 +213,13 @@
     <result status="valid" time="0.22"/>
    </proof>
    <proof
-     prover="1"
-     timelimit="3"
-     memlimit="1000"
+     prover="4"
+     timelimit="5"
+     memlimit="4000"
+     edited="lagrange_inequality_CauchySchwarzInequality_CauchySchwarz_1.v"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.62"/>
+     <result status="valid" time="0.85"/>
    </proof>
   </goal>
  </theory>
@@ -235,12 +233,12 @@
    name="triangle_aux"
    locfile="../lagrange_inequality.why"
    loclnum="77" loccnumb="8" loccnume="20"
-    sum="24d5bcf4a7a38b359d635544f55ea24e"
+    sum="0d3d97f95fe13be3df20f19761742f49"
    proved="true"
-    expanded="true"
+    expanded="false"
    shape="ainfix &lt;=anorm2ainfix +V0V2ainfix +V1V3asqrainfix +anormV0V1anormV2V3F">
    <proof
-     prover="4"
+     prover="5"
     timelimit="3"
     memlimit="1000"
     obsolete="false"
@@ -248,7 +246,7 @@
     <result status="valid" time="0.02"/>
    </proof>
    <proof
-     prover="5"
+     prover="6"
     timelimit="3"
     memlimit="1000"
     obsolete="false"
@@ -260,9 +258,9 @@
    name="sqr_sqrt_le"
    locfile="../lagrange_inequality.why"
    loclnum="82" loccnumb="8" loccnume="19"
-    sum="9436583f352c0256a6cbcd18e5b37564"
+    sum="4592f000abc47d88953aaf6cc810981c"
    proved="true"
-    expanded="true"
+    expanded="false"
    shape="ainfix &lt;=asqrtV0V1Iainfix &lt;=V0asqrV1Aainfix &lt;=c0.0V0Aainfix &lt;=c0.0V1F">
    <proof
     prover="0"
@@ -301,9 +299,9 @@
    name="triangle"
    locfile="../lagrange_inequality.why"
    loclnum="85" loccnumb="8" loccnume="16"
-    sum="9dce00ff41426f7cb6b4208ab33605c1"
+    sum="c312a44ce3003ac500885e4899b0f591"
    proved="true"
-    expanded="true"
+    expanded="false"
    shape="ainfix &lt;=anormainfix +V0V2ainfix +V1V3ainfix +anormV0V1anormV2V3F">
    <proof
     prover="0"
@@ -319,7 +317,7 @@
     memlimit="1000"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.08"/>
+     <result status="timeout" time="2.99"/>
    </proof>
   </goal>
  </theory>

--- a/examples/queens/why3session.xml
+++ b/examples/queens/why3session.xml
@@ -8,7 +8,7 @@
 <prover
  id="1"