update sessions after the time limit fix

761a246b · MARCHE Claude · 92cb6ec2 · 761a246b · 761a246b · 761a246b
Commit 761a246b authored Dec 01, 2011 by MARCHE Claude
4 changed files
--- a/examples/bts/12475/why3session.xml
+++ b/examples/bts/12475/why3session.xml
@@ -6,6 +6,10 @@
  id="alt-ergo"
  name="Alt-Ergo"
  version="0.93"/>
+ <prover
+  id="alt-ergo-0.93.1"
+  name="Alt-Ergo"
+  version="0.93.1"/>
 <prover
  id="coq"
  name="Coq"
@@ -14,6 +18,10 @@
  id="cvc3"
  name="CVC3"
  version="2.2"/>
+ <prover
+  id="cvc3-2.4"
+  name="CVC3"
+  version="2.4.1"/>
 <prover
  id="eprover"
  name="Eprover"
@@ -46,6 +54,10 @@
  id="z3"
  name="Z3"
  version="2.19"/>
+ <prover
+  id="z3-3"
+  name="Z3"
+  version="3.2"/>
 <file
  name="../12475.why"
  verified="true"
@@ -56,7 +68,7 @@
   expanded="true">
   <goal
    name="toto"
-    sum="842520fa657072446b91f650bcc58bdd"
+    sum="59cafced2f6bc3b8459444b6a68d53c8"
    proved="true"
    expanded="true"
    shape="ainfix <V0ainfix +aroundaUpV0c1.F">
@@ -72,7 +84,7 @@
     timelimit="2"
     edited=""
     obsolete="false">
-     <result status="valid" time="0.02"/>
+     <result status="valid" time="0.01"/>
    </proof>
    <proof
     prover="z3"

--- a/examples/check-builtin/floats/why3session.xml
+++ b/examples/check-builtin/floats/why3session.xml
@@ -6,6 +6,10 @@
  id="alt-ergo"
  name="Alt-Ergo"
  version="0.93"/>
+ <prover
+  id="alt-ergo-0.93.1"
+  name="Alt-Ergo"
+  version="0.93.1"/>
 <prover
  id="coq"
  name="Coq"
@@ -14,6 +18,10 @@
  id="cvc3"
  name="CVC3"
  version="2.2"/>
+ <prover
+  id="cvc3-2.4"
+  name="CVC3"
+  version="2.4.1"/>
 <prover
  id="eprover"
  name="Eprover"
@@ -46,6 +54,10 @@
  id="z3"
  name="Z3"
  version="2.19"/>
+ <prover
+  id="z3-3"
+  name="Z3"
+  version="3.2"/>
 <file
  name="../floats.why"
  verified="true"
@@ -56,7 +68,7 @@
   expanded="true">
   <goal
    name="Round_single_01"
-    sum="1f37810fcd1edad41454751a0c27522e"
+    sum="08e575aa0e76fc87133a6c5c469e35c7"
    proved="true"
    expanded="true"
    shape="ainfix =aroundaNearestTiesToEvenc0.1c0x1.99999ap-4">
@@ -70,7 +82,7 @@
   </goal>
   <goal
    name="Round_double_01"
-    sum="5c9766988706b798158bb24be3621620"
+    sum="670055059267b4361b761fe1388692d1"
    proved="true"
    expanded="true"
    shape="ainfix =aroundaNearestTiesToEvenc0.1c0x1.999999999999ap-4">
@@ -84,7 +96,7 @@
   </goal>
   <goal
    name="Test00"
-    sum="06ca4a49618b8cde48a492c8e65a9788"
+    sum="e3955674c25843b943eb3cb509d1211d"
    proved="true"
    expanded="true"
    shape="ainfix <=aprefix -c3.0V0Iainfix <=aabsV0c2.0F">
@@ -100,7 +112,7 @@
     timelimit="5"
     edited=""
     obsolete="false">
-     <result status="valid" time="0.02"/>
+     <result status="valid" time="0.01"/>
    </proof>
    <proof
     prover="z3"
@@ -119,7 +131,7 @@
   </goal>
   <goal
    name="Test01"
-    sum="b0e61c210d8a6c52b23743ce5c8c7823"
+    sum="36a3ee4f3505945e50abd89d988f45c3"
    proved="true"
    expanded="true"
    shape="ainfix <=aabsainfix -ainfix *avalueV0avalueV0aroundaNearestTiesToEvenainfix *avalueV0avalueV0c0x1.p-52Iainfix <=avalueV0c2.0Aainfix <=aprefix -c2.0avalueV0F">
@@ -133,7 +145,7 @@
   </goal>
   <goal
    name="Test02"
-    sum="1b95e5abb53beb3bf679820c5ed7ca89"
+    sum="fda6f380d63383695418d32003c3a025"
    proved="true"
    expanded="true"
    shape="ainfix <=aabsainfix -ainfix *avalueV1avalueV1aroundaNearestTiesToEvenainfix *avalueV0avalueV0c0x1.p-52Iainfix =V1V0Iainfix <=aabsavalueV0c2.0F">
@@ -147,7 +159,7 @@
   </goal>
   <goal
    name="Test03"
-    sum="87fd186418a343a100367a521ecc7305"
+    sum="8a89e5eb9ccfd12bb0241ad10f84b005"
    proved="true"
    expanded="true"
    shape="ainfix <=asqrtainfix *ainfix -avalueV2ainfix *avalueV0avalueV0ainfix -avalueV1ainfix *avalueV0avalueV0c0x1.p-52Iainfix =V2V1Iainfix =avalueV1aroundaNearestTiesToEvenainfix *avalueV0avalueV0Iainfix <=aabsavalueV0c2.0F">

--- a/examples/my_cosine/why3session.xml
+++ b/examples/my_cosine/why3session.xml
@@ -6,6 +6,10 @@
  id="alt-ergo"
  name="Alt-Ergo"
  version="0.93"/>
+ <prover
+  id="alt-ergo-0.93.1"
+  name="Alt-Ergo"
+  version="0.93.1"/>
 <prover
  id="coq"
  name="Coq"
@@ -14,6 +18,10 @@
  id="cvc3"
  name="CVC3"
  version="2.2"/>
+ <prover
+  id="cvc3-2.4"
+  name="CVC3"
+  version="2.4.1"/>
 <prover
  id="eprover"
  name="Eprover"
@@ -46,6 +54,10 @@
  id="z3"
  name="Z3"
  version="2.19"/>
+ <prover
+  id="z3-3"
+  name="Z3"
+  version="3.2"/>
 <file
  name="../my_cosine.why"
  verified="true"
@@ -56,7 +68,7 @@
   expanded="true">
   <goal
    name="MethodError"
-    sum="378e94b2f05330ca744a6c0e6ce30dc5"
+    sum="d47842bb20df32b89d2c1ddfebb256cf"
    proved="true"
    expanded="true"
    shape="ainfix <=aabsainfix -ainfix -c1.0ainfix *c0.5ainfix *V0V0acosV0c0x1.p-24Iainfix <=aabsV0c0x1.p-5F">
@@ -65,12 +77,12 @@
     timelimit="2"
     edited="my_cosine_CosineSingle_MethodError_1.v"
     obsolete="false">
-     <result status="valid" time="3.54"/>
+     <result status="valid" time="3.60"/>
    </proof>
   </goal>
   <goal
    name="TotalErrorFullyExpanded"
-    sum="b1a20eb4f29a8d6ccc1e739521c2dc03"
+    sum="2bd1cf125c7159ffafd8145891e0d6a0"
    proved="true"
    expanded="true"
    shape="ainfix <=aabsainfix -V3acosavalueV0c0x1.p-23Iainfix =V3aroundaNearestTiesToEvenainfix -c1.0V2Iainfix =V2aroundaNearestTiesToEvenainfix *c0.5V1Iainfix =V1aroundaNearestTiesToEvenainfix *avalueV0avalueV0FIainfix <=aabsainfix -ainfix -c1.0ainfix *c0.5ainfix *avalueV0avalueV0acosavalueV0c0x1.p-24Iainfix <=aabsavalueV0c0x1.p-5F">
@@ -84,7 +96,7 @@
   </goal>
   <goal
    name="TotalErrorExpanded"
-    sum="b316f68d551fe648c8b945b55c383697"
+    sum="c158687efdb17a8ac23f612d3a6081d0"
    proved="true"
    expanded="true"
    shape="LaroundaNearestTiesToEvenainfix *avalueV0avalueV0LaroundaNearestTiesToEvenainfix *c0.5V1LaroundaNearestTiesToEvenainfix -c1.0V2ainfix <=aabsainfix -V3acosavalueV0c0x1.p-23Iainfix <=aabsavalueV0c0x1.p-5F">
@@ -93,12 +105,12 @@
     timelimit="2"
     edited=""
     obsolete="false">
-     <result status="valid" time="0.72"/>
+     <result status="valid" time="0.70"/>
    </proof>
   </goal>
   <goal
    name="TotalError"
-    sum="e61c038dc9dad5a1a60a5c909eb8a4bd"
+    sum="dfd5fec597f2a85697ebccc2a69e02bc"
    proved="true"
    expanded="true"
    shape="Lacos_singleV0ainfix <=aabsainfix -avalueV1acosavalueV0c0x1.p-23Iainfix <=aabsavalueV0c0x1.p-5F">
@@ -107,7 +119,7 @@
     timelimit="10"
     edited=""
     obsolete="false">
-     <result status="valid" time="2.53"/>
+     <result status="valid" time="2.52"/>
    </proof>
   </goal>
  </theory>

--- a/examples/programs/my_cosine/why3session.xml
+++ b/examples/programs/my_cosine/why3session.xml
@@ -6,6 +6,10 @@
  id="alt-ergo"
  name="Alt-Ergo"
  version="0.93"/>
+ <prover
+  id="alt-ergo-0.93.1"
+  name="Alt-Ergo"
+  version="0.93.1"/>
 <prover
  id="coq"
  name="Coq"
@@ -14,6 +18,10 @@
  id="cvc3"
  name="CVC3"
  version="2.2"/>
+ <prover
+  id="cvc3-2.4"
+  name="CVC3"
+  version="2.4.1"/>
 <prover
  id="eprover"
  name="Eprover"
@@ -46,6 +54,10 @@
  id="z3"
  name="Z3"
  version="2.19"/>
+ <prover
+  id="z3-3"
+  name="Z3"
+  version="3.2"/>
 <file
  name="../my_cosine.mlw"
  verified="true"
@@ -57,7 +69,7 @@
   <goal
    name="WP_parameter my_cosine"
    expl="parameter my_cosine"
-    sum="a26a40699ff93a71959d0e4f8fb44279"
+    sum="c72e4c575347019fa0b03b2724963570"
    proved="true"
    expanded="true"
    shape="ainfix <=.aabsainfix -.avalueV5acosavalueV0c0x1.p-23Iainfix =avalueV5aroundaNearestTiesToEvenainfix -.avalueV1avalueV4FAainfix <=aabsaroundaNearestTiesToEvenainfix -.avalueV1avalueV4amax_singleIainfix =avalueV4aroundaNearestTiesToEvenainfix *.avalueV2avalueV3FAainfix <=aabsaroundaNearestTiesToEvenainfix *.avalueV2avalueV3amax_singleIainfix =avalueV3c0.5FIainfix =avalueV2aroundaNearestTiesToEvenainfix *.avalueV0avalueV0FAainfix <=aabsaroundaNearestTiesToEvenainfix *.avalueV0avalueV0amax_singleIainfix =avalueV1c1.0FAainfix <=.aabsainfix -.ainfix -.c1.0ainfix *.ainfix *.avalueV0avalueV0c0.5acosavalueV0c0x1.p-24Iainfix <=.aabsavalueV0c0x1.p-5F">
@@ -68,7 +80,7 @@
     <goal
      name="WP_parameter my_cosine.1"
      expl="assertion"
-      sum="f6badae9f5c3abc2ac1539d8566dda4d"
+      sum="d007264e064bd5fd78550511f81170f3"
      proved="true"
      expanded="true"
      shape="ainfix <=.aabsainfix -.ainfix -.c1.0ainfix *.ainfix *.avalueV0avalueV0c0.5acosavalueV0c0x1.p-24Iainfix <=.aabsavalueV0c0x1.p-5F">
@@ -77,13 +89,13 @@
       timelimit="2"
       edited="my_cosine_M_WP_parameter_my_cosine_1.v"
       obsolete="false">
-       <result status="valid" time="3.69"/>
+       <result status="valid" time="3.66"/>
      </proof>
     </goal>
     <goal
      name="WP_parameter my_cosine.2"
      expl="precondition"
-      sum="1f7f696639952ed7ece2a5fc463a4972"
+      sum="f18511e3e96df6788e167c546f07558d"
      proved="true"
      expanded="true"
      shape="ainfix <=aabsaroundaNearestTiesToEvenainfix *.avalueV0avalueV0amax_singleIainfix =avalueV1c1.0FIainfix <=.aabsainfix -.ainfix -.c1.0ainfix *.ainfix *.avalueV0avalueV0c0.5acosavalueV0c0x1.p-24Iainfix <=.aabsavalueV0c0x1.p-5F">
@@ -98,7 +110,7 @@
     <goal
      name="WP_parameter my_cosine.3"
      expl="precondition"
-      sum="2316a06d099159aba755caf1ef802874"
+      sum="10b405e5953e9b7dafa54e51a54ae28a"
      proved="true"
      expanded="true"
      shape="ainfix <=aabsaroundaNearestTiesToEvenainfix *.avalueV2avalueV3amax_singleIainfix =avalueV3c0.5FIainfix =avalueV2aroundaNearestTiesToEvenainfix *.avalueV0avalueV0FIainfix <=aabsaroundaNearestTiesToEvenainfix *.avalueV0avalueV0amax_singleIainfix =avalueV1c1.0FIainfix <=.aabsainfix -.ainfix -.c1.0ainfix *.ainfix *.avalueV0avalueV0c0.5acosavalueV0c0x1.p-24Iainfix <=.aabsavalueV0c0x1.p-5F">
@@ -113,7 +125,7 @@
     <goal
      name="WP_parameter my_cosine.4"
      expl="precondition"
-      sum="42b0def796a2014ab64ebe65ab4bc210"
+      sum="3de8e95e7ef082087a8ef1355d4924b3"
      proved="true"
      expanded="true"
      shape="ainfix <=aabsaroundaNearestTiesToEvenainfix -.avalueV1avalueV4amax_singleIainfix =avalueV4aroundaNearestTiesToEvenainfix *.avalueV2avalueV3FIainfix <=aabsaroundaNearestTiesToEvenainfix *.avalueV2avalueV3amax_singleIainfix =avalueV3c0.5FIainfix =avalueV2aroundaNearestTiesToEvenainfix *.avalueV0avalueV0FIainfix <=aabsaroundaNearestTiesToEvenainfix *.avalueV0avalueV0amax_singleIainfix =avalueV1c1.0FIainfix <=.aabsainfix -.ainfix -.c1.0ainfix *.ainfix *.avalueV0avalueV0c0.5acosavalueV0c0x1.p-24Iainfix <=.aabsavalueV0c0x1.p-5F">
@@ -128,7 +140,7 @@
     <goal
      name="WP_parameter my_cosine.5"
      expl="normal postcondition"
-      sum="19749f0f800fc253e060790e081d492d"
+      sum="27267d4d4a0943eb3f906da58e6c7746"
      proved="true"
      expanded="true"
      shape="ainfix <=.aabsainfix -.avalueV5acosavalueV0c0x1.p-23Iainfix =avalueV5aroundaNearestTiesToEvenainfix -.avalueV1avalueV4FIainfix <=aabsaroundaNearestTiesToEvenainfix -.avalueV1avalueV4amax_singleIainfix =avalueV4aroundaNearestTiesToEvenainfix *.avalueV2avalueV3FIainfix <=aabsaroundaNearestTiesToEvenainfix *.avalueV2avalueV3amax_singleIainfix =avalueV3c0.5FIainfix =avalueV2aroundaNearestTiesToEvenainfix *.avalueV0avalueV0FIainfix <=aabsaroundaNearestTiesToEvenainfix *.avalueV0avalueV0amax_singleIainfix =avalueV1c1.0FIainfix <=.aabsainfix -.ainfix -.c1.0ainfix *.ainfix *.avalueV0avalueV0c0.5acosavalueV0c0x1.p-24Iainfix <=.aabsavalueV0c0x1.p-5F">
@@ -137,7 +149,7 @@
       timelimit="2"
       edited=""
       obsolete="false">
-       <result status="valid" time="0.00"/>
+       <result status="valid" time="0.01"/>
      </proof>
     </goal>
    </transf>