Support for E prover 1.9 and 2.0

CHANGES

 
 * marks an incompatible change
 
+
+Provers
+  o support for E 2.0 (released Jul 4, 2017)
+  o support for E 1.9.1 (release Aug 31, 2016)
+
 Tools
 
   o why3 config now generates default proof strategies using the

examples/logic/genealogy/why3session.xml

@@ -29,12 +29,13 @@
 <prover id="24" name="veriT" version="201410" timelimit="5" steplimit="1" memlimit="1000"/>
 <prover id="25" name="Alt-Ergo" version="1.00.prv" timelimit="5" steplimit="1" memlimit="1000"/>
 <prover id="26" name="Zenon Modulo" version="0.4.1" timelimit="5" steplimit="1" memlimit="1000"/>
+<prover id="27" name="Eprover" version="2.0" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="28" name="Z3" version="4.4.1" timelimit="5" steplimit="1" memlimit="4000"/>
 <prover id="29" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="30" name="Isabelle" version="2016-1" timelimit="100" steplimit="1" memlimit="1000"/>
 <file name="../genealogy.why" expanded="true">
 <theory name="Genealogy" sum="35e1439432a79e05534b2c5cf39ad9dc" expanded="true">
- <goal name="Child_is_son_or_daughter">
+ <goal name="Child_is_son_or_daughter" expl="" expanded="true">
  <proof prover="0" edited="genealogy_Genealogy_Child_is_son_or_daughter_1.v"><result status="valid" time="0.31"/></proof>
  <proof prover="2"><result status="valid" time="0.02"/></proof>
  <proof prover="3"><result status="valid" time="0.00"/></proof>
@@ -58,11 +59,12 @@
  <proof prover="24"><result status="valid" time="0.00"/></proof>
  <proof prover="25"><result status="valid" time="0.00" steps="7"/></proof>
  <proof prover="26"><result status="valid" time="0.02"/></proof>
+ <proof prover="27"><result status="valid" time="0.01"/></proof>
  <proof prover="28"><result status="valid" time="0.01"/></proof>
  <proof prover="29"><result status="valid" time="0.00" steps="10"/></proof>
  <proof prover="30" edited="genealogy_Genealogy_Child_is_son_or_daughter_1.xml"><result status="valid" time="21.67"/></proof>
  </goal>
- <goal name="Sibling_sym">
+ <goal name="Sibling_sym" expl="" expanded="true">
  <proof prover="1"><result status="valid" time="0.00"/></proof>
  <proof prover="3"><result status="valid" time="0.00"/></proof>
  <proof prover="4"><result status="valid" time="0.00"/></proof>
@@ -86,11 +88,12 @@
  <proof prover="24"><result status="valid" time="0.00"/></proof>
  <proof prover="25"><result status="valid" time="0.00" steps="2"/></proof>
  <proof prover="26"><result status="valid" time="0.02"/></proof>
+ <proof prover="27"><result status="valid" time="0.00"/></proof>
  <proof prover="28"><result status="valid" time="0.00"/></proof>
  <proof prover="29"><result status="valid" time="0.00" steps="3"/></proof>
  <proof prover="30" edited="genealogy_Genealogy_Sibling_sym_1.xml"><result status="valid" time="21.58"/></proof>
  </goal>
- <goal name="Sibling_is_brother_or_sister">
+ <goal name="Sibling_is_brother_or_sister" expl="" expanded="true">
  <proof prover="2"><result status="valid" time="0.03"/></proof>
  <proof prover="3"><result status="valid" time="0.00"/></proof>
  <proof prover="4"><result status="valid" time="0.00"/></proof>
@@ -112,11 +115,12 @@
  <proof prover="24"><result status="valid" time="0.00"/></proof>
  <proof prover="25"><result status="valid" time="0.00" steps="8"/></proof>
  <proof prover="26"><result status="valid" time="0.01"/></proof>
+ <proof prover="27"><result status="valid" time="0.01"/></proof>
  <proof prover="28"><result status="valid" time="0.01"/></proof>
  <proof prover="29"><result status="valid" time="0.00" steps="10"/></proof>
  <proof prover="30" edited="genealogy_Genealogy_Sibling_is_brother_or_sister_1.xml"><result status="valid" time="20.20"/></proof>
  </goal>
- <goal name="Grandparent_is_grandfather_or_grandmother">
+ <goal name="Grandparent_is_grandfather_or_grandmother" expl="" expanded="true">
  <proof prover="1"><result status="valid" time="0.01"/></proof>
  <proof prover="3"><result status="valid" time="0.00"/></proof>
  <proof prover="4"><result status="valid" time="0.01"/></proof>
@@ -139,11 +143,12 @@
  <proof prover="24"><result status="valid" time="0.00"/></proof>
  <proof prover="25"><result status="valid" time="0.00" steps="38"/></proof>
  <proof prover="26"><result status="valid" time="0.02"/></proof>
+ <proof prover="27"><result status="valid" time="0.01"/></proof>
  <proof prover="28"><result status="valid" time="0.01"/></proof>
  <proof prover="29"><result status="valid" time="0.00" steps="36"/></proof>
  <proof prover="30" edited="genealogy_Genealogy_Grandparent_is_grandfather_or_grandmother_1.xml"><result status="valid" time="20.18"/></proof>
  </goal>
- <goal name="Grandfather_male">
+ <goal name="Grandfather_male" expl="" expanded="true">
  <proof prover="1"><result status="valid" time="0.00"/></proof>
  <proof prover="3"><result status="valid" time="0.00"/></proof>
  <proof prover="4"><result status="valid" time="0.00"/></proof>
@@ -167,10 +172,11 @@
  <proof prover="24"><result status="valid" time="0.00"/></proof>
  <proof prover="25"><result status="valid" time="0.00" steps="5"/></proof>
  <proof prover="26"><result status="valid" time="0.02"/></proof>
+ <proof prover="27"><result status="valid" time="0.01"/></proof>
  <proof prover="28"><result status="valid" time="0.00"/></proof>
  <proof prover="29"><result status="valid" time="0.00" steps="8"/></proof>
  </goal>
- <goal name="Grandmother_female">
+ <goal name="Grandmother_female" expl="" expanded="true">
  <proof prover="1"><result status="valid" time="0.01"/></proof>
  <proof prover="3"><result status="valid" time="0.00"/></proof>
  <proof prover="4"><result status="valid" time="0.00"/></proof>
@@ -194,10 +200,11 @@
  <proof prover="24"><result status="valid" time="0.00"/></proof>
  <proof prover="25"><result status="valid" time="0.00" steps="5"/></proof>
  <proof prover="26"><result status="valid" time="0.02"/></proof>
+ <proof prover="27"><result status="valid" time="0.00"/></proof>
  <proof prover="28"><result status="valid" time="0.00"/></proof>
  <proof prover="29"><result status="valid" time="0.00" steps="8"/></proof>
  </goal>
- <goal name="Only_two_grandfathers">
+ <goal name="Only_two_grandfathers" expl="" expanded="true">
  <proof prover="1"><result status="valid" time="0.01"/></proof>
  <proof prover="3"><result status="valid" time="0.00"/></proof>
  <proof prover="4"><result status="valid" time="0.01"/></proof>
@@ -221,6 +228,7 @@
  <proof prover="24"><result status="valid" time="0.00"/></proof>
  <proof prover="25"><result status="valid" time="0.00" steps="8"/></proof>
  <proof prover="26"><result status="valid" time="0.02"/></proof>
+ <proof prover="27"><result status="valid" time="0.01"/></proof>
  <proof prover="28"><result status="valid" time="0.01"/></proof>
  <proof prover="29"><result status="valid" time="0.00" steps="9"/></proof>
  </goal>

share/provers-detection-data.conf

@@ -174,6 +174,9 @@ driver = "yices-smt2"
 [ATP eprover]
 name = "Eprover"
 exec = "eprover"
+exec = "eprover-2.0"
+exec = "eprover-1.9.1"
+exec = "eprover-1.9"
 exec = "eprover-1.8"
 exec = "eprover-1.7"
 exec = "eprover-1.6"
@@ -181,7 +184,10 @@ exec = "eprover-1.5"
 exec = "eprover-1.4"
 version_switch = "--version"
 version_regexp = "E \\([-0-9.]+\\) [^\n]+"
-version_ok  = "1.8-001"
+version_ok  = "2.0"
+version_old = "1.9.1-001"
+version_old = "1.9"
+version_old = "1.8-001"
 version_old = "1.7"
 version_old = "1.6"
 version_old = "1.5"