diff --git a/examples/logic/genealogy/why3session.xml b/examples/logic/genealogy/why3session.xml index 56e6f2423af134c3dda33b743b3cb84e748c7ddd..4c5221fb4034c5f98533e7388af8777bf44164d5 100644 --- a/examples/logic/genealogy/why3session.xml +++ b/examples/logic/genealogy/why3session.xml @@ -16,7 +16,7 @@ <prover id="11" name="Simplify" version="1.5.4" timelimit="3" steplimit="1" memlimit="1000"/> <prover id="12" name="Yices" version="1.0.38" timelimit="5" steplimit="1" memlimit="0"/> <prover id="13" name="Zenon" version="0.7.1" timelimit="5" steplimit="1" memlimit="4000"/> -<prover id="14" name="Alt-Ergo" version="1.01" timelimit="5" memlimit="4000"/> +<prover id="14" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="1" memlimit="4000"/> <prover id="15" name="Metis" version="2.3" timelimit="5" steplimit="1" memlimit="1000"/> <prover id="16" name="Z3" version="3.2" timelimit="5" steplimit="1" memlimit="0"/> <prover id="17" name="Alt-Ergo" version="0.95.2" timelimit="60" steplimit="1" memlimit="1000"/> @@ -30,7 +30,8 @@ <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="Coq" version="8.4pl6" timelimit="5" steplimit="1" memlimit="4000"/> -<prover id="28" name="Z3" version="4.4.1" timelimit="5" memlimit="4000"/> +<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" memlimit="1000"/> <file name="../genealogy.why" expanded="true"> <theory name="Genealogy" sum="35e1439432a79e05534b2c5cf39ad9dc" expanded="true"> <goal name="Child_is_son_or_daughter" expanded="true"> @@ -59,6 +60,7 @@ <proof prover="26"><result status="valid" time="0.02"/></proof> <proof prover="27" edited="genealogy_Genealogy_Child_is_son_or_daughter_1.v"><result status="valid" time="0.80"/></proof> <proof prover="28"><result status="valid" time="0.01"/></proof> + <proof prover="29"><result status="valid" time="0.00" steps="10"/></proof> </goal> <goal name="Sibling_sym" expanded="true"> <proof prover="0" edited="genealogy_Genealogy_Sibling_sym_1.xml"><result status="valid" time="6.09"/></proof> @@ -86,6 +88,7 @@ <proof prover="25"><result status="valid" time="0.00" steps="2"/></proof> <proof prover="26"><result status="valid" time="0.02"/></proof> <proof prover="28"><result status="valid" time="0.00"/></proof> + <proof prover="29"><result status="valid" time="0.00" steps="3"/></proof> </goal> <goal name="Sibling_is_brother_or_sister" expanded="true"> <proof prover="0" edited="genealogy_Genealogy_Sibling_is_brother_or_sister_1.xml"><result status="valid" time="6.19"/></proof> @@ -111,6 +114,7 @@ <proof prover="25"><result status="valid" time="0.00" steps="8"/></proof> <proof prover="26"><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> </goal> <goal name="Grandparent_is_grandfather_or_grandmother" expanded="true"> <proof prover="0" edited="genealogy_Genealogy_Grandparent_is_grandfather_or_grandmother_1.xml"><result status="valid" time="6.50"/></proof> @@ -137,6 +141,7 @@ <proof prover="25"><result status="valid" time="0.00" steps="38"/></proof> <proof prover="26"><result status="valid" time="0.02"/></proof> <proof prover="28"><result status="valid" time="0.01"/></proof> + <proof prover="29"><result status="valid" time="0.00" steps="36"/></proof> </goal> <goal name="Grandfather_male" expanded="true"> <proof prover="1"><result status="valid" time="0.00"/></proof> @@ -163,6 +168,7 @@ <proof prover="25"><result status="valid" time="0.00" steps="5"/></proof> <proof prover="26"><result status="valid" time="0.02"/></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" expanded="true"> <proof prover="1"><result status="valid" time="0.01"/></proof> @@ -189,6 +195,7 @@ <proof prover="25"><result status="valid" time="0.00" steps="5"/></proof> <proof prover="26"><result status="valid" time="0.02"/></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" expanded="true"> <proof prover="1"><result status="valid" time="0.01"/></proof> @@ -215,6 +222,7 @@ <proof prover="25"><result status="valid" time="0.00" steps="8"/></proof> <proof prover="26"><result status="valid" time="0.02"/></proof> <proof prover="28"><result status="valid" time="0.01"/></proof> + <proof prover="29"><result status="valid" time="0.00" steps="9"/></proof> </goal> </theory> </file> diff --git a/share/provers-detection-data.conf b/share/provers-detection-data.conf index 54ebc460b2dd07ebb15443c2919a955c2f24efee..6e4dc77e20d27db2e2ece6eecdc18062739d3418 100644 --- a/share/provers-detection-data.conf +++ b/share/provers-detection-data.conf @@ -1,12 +1,14 @@ [ATP alt-ergo] name = "Alt-Ergo" exec = "alt-ergo" +exec = "alt-ergo-1.30" exec = "alt-ergo-1.20.prv" exec = "alt-ergo-1.10.prv" exec = "alt-ergo-1.01" exec = "alt-ergo-1.00.prv" version_switch = "-version" version_regexp = "^\\([0-9.]+\\(-dev\\|prv\\)?\\)$" +version_ok = "1.30" version_ok = "1.20.prv" version_ok = "1.10.prv" version_ok = "1.01"