Support for Alt-Ergo 0.95.2

d13f51ec · MARCHE Claude · f7ce2151 · d13f51ec
Commit d13f51ec authored Oct 05, 2013 by MARCHE Claude
Hide whitespace changes
Inline Side-by-side

Showing with 233 additions and 107 deletions

examples/logic/genealogy/why3session.xml examples/logic/genealogy/why3session.xml +210 -91

share/provers-detection-data.conf share/provers-detection-data.conf +23 -16

No files found.
--- a/examples/logic/genealogy/why3session.xml
+++ b/examples/logic/genealogy/why3session.xml
@@ -7,50 +7,58 @@
  version="0.95.1"/>
 <prover
  id="1"
+  name="Alt-Ergo"
+  version="0.95.2"/>
+ <prover
+  id="2"
  name="CVC3"
  version="2.2"/>
 <prover
-  id="2"
+  id="3"
  name="CVC3"
  version="2.4.1"/>
 <prover
-  id="3"
+  id="4"
+  name="CVC4"
+  version="1.2"/>
+ <prover
+  id="5"
  name="Eprover"
  version="1.6"/>
 <prover
-  id="4"
+  id="6"
  name="Metis"
  version="2.3"/>
 <prover
-  id="5"
+  id="7"
  name="Spass"
  version="3.7"/>
 <prover
-  id="6"
+  id="8"
  name="Vampire"
  version="0.6"/>
 <prover
-  id="7"
+  id="9"
  name="Yices"
-  version="1.0.38"/>
+  version="1.0.25"/>
 <prover
-  id="8"
+  id="10"
  name="Z3"
  version="2.19"/>
 <prover
-  id="9"
+  id="11"
  name="Z3"
  version="3.2"/>
 <prover
-  id="10"
+  id="12"
  name="Z3"
  version="4.3.1"/>
 <prover
-  id="11"
+  id="13"
  name="Zenon"
  version="0.7.1"/>
 <prover
-  id="12"
+  id="14"
  name="veriT"
  version="201310"/>
 <file
@@ -81,11 +89,11 @@
    </proof>
    <proof
     prover="1"
-     timelimit="5"
-     memlimit="0"
+     timelimit="60"
+     memlimit="1000"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.00"/>
+     <result status="valid" time="0.01"/>
    </proof>
    <proof
     prover="2"
@@ -105,6 +113,22 @@
    </proof>
    <proof
     prover="4"
+     timelimit="60"
+     memlimit="1000"
+     obsolete="false"
+     archived="false">
+     <result status="unknown" time="0.00"/>
+    </proof>
+    <proof
+     prover="5"
+     timelimit="5"
+     memlimit="0"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.00"/>
+    </proof>
+    <proof
+     prover="6"
     timelimit="5"
     memlimit="1000"
     obsolete="false"
@@ -112,7 +136,7 @@
     <result status="valid" time="0.02"/>
    </proof>
    <proof
-     prover="5"
+     prover="7"
     timelimit="5"
     memlimit="0"
     obsolete="false"
@@ -120,7 +144,7 @@
     <result status="valid" time="0.01"/>
    </proof>
    <proof
-     prover="6"
+     prover="8"
     timelimit="5"
     memlimit="0"
     obsolete="false"
@@ -128,7 +152,7 @@
     <result status="valid" time="0.00"/>
    </proof>
    <proof
-     prover="7"
+     prover="9"
     timelimit="5"
     memlimit="0"
     obsolete="false"
@@ -136,7 +160,7 @@
     <result status="unknown" time="0.01"/>
    </proof>
    <proof
-     prover="8"
+     prover="10"
     timelimit="5"
     memlimit="0"
     obsolete="false"
@@ -144,7 +168,7 @@
     <result status="valid" time="0.01"/>
    </proof>
    <proof
-     prover="9"
+     prover="11"
     timelimit="5"
     memlimit="0"
     obsolete="false"
@@ -152,15 +176,15 @@
     <result status="valid" time="0.01"/>
    </proof>
    <proof
-     prover="10"
+     prover="12"
     timelimit="5"
     memlimit="4000"
     obsolete="false"
     archived="false">
-     <result status="unknown" time="2.12"/>
+     <result status="unknown" time="1.60"/>
    </proof>
    <proof
-     prover="11"
+     prover="13"
     timelimit="5"
     memlimit="4000"
     obsolete="false"
@@ -168,10 +192,9 @@
     <result status="valid" time="0.04"/>
    </proof>
    <proof
-     prover="12"
-     timelimit="5"
-     memlimit="4000"
-     edited="genealogy-Genealogy-Child_is_son_or_daughter_1.smt2"
+     prover="14"
+     timelimit="60"
+     memlimit="1000"
     obsolete="false"
     archived="false">
     <result status="valid" time="0.00"/>
@@ -195,11 +218,11 @@
    </proof>
    <proof
     prover="1"
-     timelimit="5"
-     memlimit="0"
+     timelimit="60"
+     memlimit="1000"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.00"/>
+     <result status="valid" time="0.02"/>
    </proof>
    <proof
     prover="2"
@@ -219,11 +242,11 @@
    </proof>
    <proof
     prover="4"
-     timelimit="5"
+     timelimit="60"
     memlimit="1000"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.12"/>
+     <result status="valid" time="0.00"/>
    </proof>
    <proof
     prover="5"
@@ -236,10 +259,10 @@
    <proof
     prover="6"
     timelimit="5"
-     memlimit="0"
+     memlimit="1000"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.00"/>
+     <result status="valid" time="0.12"/>
    </proof>
    <proof
     prover="7"
@@ -255,7 +278,7 @@
     memlimit="0"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.01"/>
+     <result status="valid" time="0.00"/>
    </proof>
    <proof
     prover="9"
@@ -263,18 +286,34 @@
     memlimit="0"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.01"/>
+     <result status="valid" time="0.00"/>
    </proof>
    <proof
     prover="10"
     timelimit="5"
+     memlimit="0"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.01"/>
+    </proof>
+    <proof
+     prover="11"
+     timelimit="5"
+     memlimit="0"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.01"/>
+    </proof>
+    <proof
+     prover="12"
+     timelimit="5"
     memlimit="4000"
     obsolete="false"
     archived="false">
     <result status="valid" time="0.02"/>
    </proof>
    <proof
-     prover="11"
+     prover="13"
     timelimit="5"
     memlimit="4000"
     obsolete="false"
@@ -282,7 +321,7 @@
     <result status="timeout" time="5.23"/>
    </proof>
    <proof
-     prover="12"
+     prover="14"
     timelimit="5"
     memlimit="4000"
     obsolete="false"
@@ -308,11 +347,11 @@
    </proof>
    <proof
     prover="1"
-     timelimit="5"
-     memlimit="0"
+     timelimit="60"
+     memlimit="1000"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.00"/>
+     <result status="valid" time="0.02"/>
    </proof>
    <proof
     prover="2"
@@ -332,6 +371,22 @@
    </proof>
    <proof
     prover="4"
+     timelimit="60"
+     memlimit="1000"
+     obsolete="false"
+     archived="false">
+     <result status="unknown" time="0.01"/>
+    </proof>
+    <proof
+     prover="5"
+     timelimit="5"
+     memlimit="0"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.00"/>
+    </proof>
+    <proof
+     prover="6"
     timelimit="5"
     memlimit="1000"
     obsolete="false"
@@ -339,7 +394,7 @@
     <result status="valid" time="0.04"/>
    </proof>
    <proof
-     prover="5"
+     prover="7"
     timelimit="5"
     memlimit="0"
     obsolete="false"
@@ -347,7 +402,7 @@
     <result status="valid" time="0.01"/>
    </proof>
    <proof
-     prover="6"
+     prover="8"
     timelimit="5"
     memlimit="0"
     obsolete="false"
@@ -355,7 +410,7 @@
     <result status="valid" time="0.00"/>
    </proof>
    <proof
-     prover="7"
+     prover="9"
     timelimit="5"
     memlimit="0"
     obsolete="false"
@@ -363,7 +418,7 @@
     <result status="unknown" time="0.02"/>
    </proof>
    <proof
-     prover="8"
+     prover="10"
     timelimit="5"
     memlimit="0"
     obsolete="false"
@@ -371,7 +426,7 @@
     <result status="valid" time="0.01"/>
    </proof>
    <proof
-     prover="9"
+     prover="11"
     timelimit="5"
     memlimit="0"
     obsolete="false"
@@ -379,7 +434,7 @@
     <result status="valid" time="0.01"/>
    </proof>
    <proof
-     prover="10"
+     prover="12"
     timelimit="5"
     memlimit="4000"
     obsolete="false"
@@ -387,7 +442,7 @@
     <result status="unknown" time="2.12"/>
    </proof>
    <proof
-     prover="11"
+     prover="13"
     timelimit="5"
     memlimit="4000"
     obsolete="false"
@@ -395,7 +450,7 @@
     <result status="valid" time="0.03"/>
    </proof>
    <proof
-     prover="12"
+     prover="14"
     timelimit="5"
     memlimit="4000"
     obsolete="false"
@@ -421,6 +476,14 @@
    </proof>
    <proof
     prover="1"
+     timelimit="60"
+     memlimit="1000"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.02"/>
+    </proof>
+    <proof
+     prover="2"
     timelimit="5"
     memlimit="0"
     obsolete="false"
@@ -428,7 +491,7 @@
     <result status="valid" time="0.00"/>
    </proof>
    <proof
-     prover="2"
+     prover="3"
     timelimit="5"
     memlimit="0"
     obsolete="false"
@@ -436,7 +499,15 @@
     <result status="valid" time="0.00"/>
    </proof>
    <proof
-     prover="3"
+     prover="4"
+     timelimit="60"
+     memlimit="1000"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.01"/>
+    </proof>
+    <proof
+     prover="5"
     timelimit="5"
     memlimit="0"
     obsolete="false"
@@ -444,7 +515,7 @@
     <result status="valid" time="0.01"/>
    </proof>
    <proof
-     prover="4"
+     prover="6"
     timelimit="5"
     memlimit="1000"
     obsolete="false"
@@ -452,7 +523,7 @@
     <result status="valid" time="0.07"/>
    </proof>
    <proof
-     prover="7"
+     prover="9"
     timelimit="5"
     memlimit="0"
     obsolete="false"
@@ -460,7 +531,7 @@
     <result status="valid" time="0.04"/>
    </proof>
    <proof
-     prover="8"
+     prover="10"
     timelimit="5"
     memlimit="0"
     obsolete="false"
@@ -468,7 +539,7 @@
     <result status="valid" time="0.00"/>
    </proof>
    <proof
-     prover="9"
+     prover="11"
     timelimit="5"
     memlimit="0"
     obsolete="false"
@@ -476,7 +547,7 @@
     <result status="valid" time="0.01"/>
    </proof>
    <proof
-     prover="10"
+     prover="12"
     timelimit="5"
     memlimit="4000"
     obsolete="false"
@@ -484,7 +555,7 @@
     <result status="valid" time="0.03"/>
    </proof>
    <proof
-     prover="11"
+     prover="13"
     timelimit="5"
     memlimit="4000"
     obsolete="false"
@@ -492,7 +563,7 @@
     <result status="timeout" time="5.26"/>
    </proof>
    <proof
-     prover="12"
+     prover="14"
     timelimit="5"
     memlimit="4000"
     obsolete="false"
@@ -518,11 +589,11 @@
    </proof>
    <proof
     prover="1"
-     timelimit="5"
-     memlimit="0"
+     timelimit="60"
+     memlimit="1000"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.00"/>
+     <result status="valid" time="0.01"/>
    </proof>
    <proof
     prover="2"
@@ -542,11 +613,11 @@
    </proof>
    <proof
     prover="4"
-     timelimit="5"
+     timelimit="60"
     memlimit="1000"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.03"/>
+     <result status="valid" time="0.00"/>
    </proof>
    <proof
     prover="5"
@@ -554,12 +625,12 @@
     memlimit="0"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.02"/>
+     <result status="valid" time="0.00"/>
    </proof>
    <proof
     prover="6"
     timelimit="5"
-     memlimit="0"
+     memlimit="1000"
     obsolete="false"
     archived="false">
     <result status="valid" time="0.03"/>
@@ -578,7 +649,7 @@
     memlimit="0"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.01"/>
+     <result status="valid" time="0.03"/>
    </proof>
    <proof
     prover="9"
@@ -586,26 +657,42 @@
     memlimit="0"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.01"/>
+     <result status="valid" time="0.02"/>
    </proof>
    <proof
     prover="10"
     timelimit="5"
+     memlimit="0"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.01"/>
+    </proof>
+    <proof
+     prover="11"
+     timelimit="5"
+     memlimit="0"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.01"/>
+    </proof>
+    <proof
+     prover="12"
+     timelimit="5"
     memlimit="4000"
     obsolete="false"
     archived="false">
     <result status="valid" time="0.03"/>
    </proof>
    <proof
-     prover="11"
+     prover="13"
     timelimit="5"
     memlimit="4000"
     obsolete="false"
     archived="false">
-     <result status="timeout" time="5.10"/>
+     <result status="timeout" time="5.86"/>
    </proof>
    <proof
-     prover="12"
+     prover="14"
     timelimit="5"
     memlimit="4000"
     obsolete="false"
@@ -631,11 +718,11 @@
    </proof>
    <proof
     prover="1"
-     timelimit="5"
-     memlimit="0"
+     timelimit="60"
+     memlimit="1000"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.00"/>
+     <result status="valid" time="0.01"/>
    </proof>
    <proof
     prover="2"
@@ -655,6 +742,22 @@
    </proof>
    <proof
     prover="4"
+     timelimit="60"
+     memlimit="1000"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.01"/>
+    </proof>
+    <proof
+     prover="5"
+     timelimit="5"
+     memlimit="0"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.00"/>
+    </proof>
+    <proof
+     prover="6"
     timelimit="5"
     memlimit="1000"
     obsolete="false"
@@ -662,7 +765,7 @@
     <result status="valid" time="0.03"/>
    </proof>
    <proof
-     prover="5"
+     prover="7"
     timelimit="5"
     memlimit="0"
     obsolete="false"
@@ -670,7 +773,7 @@
     <result status="valid" time="0.02"/>
    </proof>
    <proof
-     prover="6"
+     prover="8"
     timelimit="5"
     memlimit="0"
     obsolete="false"
@@ -678,7 +781,7 @@
     <result status="valid" time="0.01"/>
    </proof>
    <proof
-     prover="7"
+     prover="9"
     timelimit="5"
     memlimit="0"
     obsolete="false"
@@ -686,7 +789,7 @@
     <result status="valid" time="0.03"/>
    </proof>
    <proof
-     prover="8"
+     prover="10"