Commit 833b28df authored by Guillaume Melquiond's avatar Guillaume Melquiond

Use Gappa 1.1.1 for tests. Mark versions 0.1x as obsolete.

parent fe493761
......@@ -24,7 +24,7 @@
<prover
id="5"
name="Gappa"
version="1.0.0"/>
version="1.1.1"/>
<prover
id="6"
name="Z3"
......
......@@ -24,7 +24,7 @@
<prover
id="5"
name="Gappa"
version="1.0.0"/>
version="1.1.1"/>
<prover
id="6"
name="Z3"
......
......@@ -12,7 +12,7 @@
<prover
id="2"
name="Gappa"
version="1.0.0"/>
version="1.1.1"/>
<prover
id="3"
name="Z3"
......
......@@ -12,7 +12,7 @@
<prover
id="2"
name="Gappa"
version="1.0.0"/>
version="1.1.1"/>
<prover
id="3"
name="Z3"
......
......@@ -16,7 +16,7 @@
<prover
id="3"
name="Gappa"
version="1.0.0"/>
version="1.1.1"/>
<prover
id="4"
name="Spass"
......
......@@ -28,7 +28,7 @@
<prover
id="6"
name="Gappa"
version="1.0.0"/>
version="1.1.1"/>
<prover
id="7"
name="MetiTarski"
......
......@@ -12,7 +12,7 @@
<prover
id="2"
name="Gappa"
version="1.0.0"/>
version="1.1.1"/>
<prover
id="3"
name="MetiTarski"
......
......@@ -12,7 +12,7 @@
<prover
id="2"
name="Gappa"
version="1.0.0"/>
version="1.1.1"/>
<prover
id="3"
name="Spass"
......
......@@ -8,7 +8,7 @@
<prover
id="1"
name="Gappa"
version="1.0.0"/>
version="1.1.1"/>
<file
name="../my_cosine.mlw"
verified="true"
......
......@@ -19,14 +19,18 @@
version="2.4.1"/>
<prover
id="4"
name="Gappa"
version="1.1.1"/>
<prover
id="5"
name="Z3"
version="2.19"/>
<prover
id="5"
id="6"
name="Z3"
version="3.2"/>
<prover
id="6"
id="7"
name="Z3"
version="4.3.1"/>
<file
......@@ -69,7 +73,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="5"
......@@ -85,6 +89,14 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="7"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
......@@ -129,7 +141,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="4"
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
......@@ -137,7 +149,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="5"
prover="6"
timelimit="5"
memlimit="1000"
obsolete="false"
......@@ -145,7 +157,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="6"
prover="7"
timelimit="5"
memlimit="1000"
obsolete="false"
......@@ -194,7 +206,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="4"
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
......@@ -202,7 +214,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="5"
prover="6"
timelimit="5"
memlimit="1000"
obsolete="false"
......@@ -210,7 +222,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="6"
prover="7"
timelimit="5"
memlimit="1000"
obsolete="false"
......@@ -224,7 +236,7 @@
loclnum="14" loccnumb="8" loccnume="16"
sum="caa9c135ebad086ab4a3fadd7ad92344"
proved="true"
expanded="true"
expanded="false"
shape="ainfix =ainfix /.ainfix *.V0V1V1ainfix *.V0ainfix /.V1V1Iainfix &gt;V1c0.0Aainfix &gt;V0c0.0F">
<proof
prover="0"
......@@ -251,7 +263,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="4"
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
......@@ -259,7 +271,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="5"
prover="6"
timelimit="5"
memlimit="1000"
obsolete="false"
......@@ -267,7 +279,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="6"
prover="7"
timelimit="5"
memlimit="1000"
obsolete="false"
......@@ -281,10 +293,10 @@
loclnum="17" loccnumb="8" loccnume="17"
sum="083074e2fccefc1e9ca1ecf2b6ad7eae"
proved="true"
expanded="true"
expanded="false"
shape="ainfix =ainfix /.ainfix *.V0V1V1ainfix *.ainfix /.V0V1V1Iainfix &gt;V1c0.0Aainfix &gt;V0c0.0F">
<proof
prover="4"
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
......@@ -292,7 +304,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="5"
prover="6"
timelimit="5"
memlimit="1000"
obsolete="false"
......@@ -300,7 +312,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="6"
prover="7"
timelimit="5"
memlimit="1000"
obsolete="false"
......@@ -333,7 +345,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="4"
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
......@@ -341,7 +353,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="5"
prover="6"
timelimit="5"
memlimit="1000"
obsolete="false"
......@@ -349,7 +361,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="6"
prover="7"
timelimit="5"
memlimit="1000"
obsolete="false"
......@@ -382,7 +394,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="4"
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
......@@ -390,7 +402,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="5"
prover="6"
timelimit="5"
memlimit="1000"
obsolete="false"
......@@ -398,7 +410,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="6"
prover="7"
timelimit="5"
memlimit="1000"
obsolete="false"
......@@ -431,7 +443,7 @@
<result status="valid" time="0.02"/>
</proof>
<proof
prover="4"
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
......@@ -439,7 +451,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="5"
prover="6"
timelimit="5"
memlimit="1000"
obsolete="false"
......@@ -447,7 +459,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="6"
prover="7"
timelimit="5"
memlimit="1000"
obsolete="false"
......@@ -480,7 +492,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="4"
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
......@@ -488,7 +500,7 @@
<result status="valid" time="0.02"/>
</proof>
<proof
prover="5"
prover="6"
timelimit="5"
memlimit="1000"
obsolete="false"
......@@ -496,7 +508,7 @@
<result status="valid" time="0.02"/>
</proof>
<proof
prover="6"
prover="7"
timelimit="5"
memlimit="1000"
obsolete="false"
......@@ -529,7 +541,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="4"
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
......@@ -537,7 +549,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="5"
prover="6"
timelimit="5"
memlimit="1000"
obsolete="false"
......@@ -586,7 +598,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="4"
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
......@@ -594,7 +606,7 @@
<result status="valid" time="0.02"/>
</proof>
<proof
prover="5"
prover="6"
timelimit="5"
memlimit="1000"
obsolete="false"
......@@ -602,7 +614,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="6"
prover="7"
timelimit="5"
memlimit="1000"
obsolete="false"
......@@ -635,7 +647,7 @@
<result status="valid" time="0.10"/>
</proof>
<proof
prover="4"
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
......@@ -643,7 +655,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="5"
prover="6"
timelimit="5"
memlimit="1000"
obsolete="false"
......@@ -651,7 +663,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="6"
prover="7"
timelimit="5"
memlimit="1000"
obsolete="false"
......
......@@ -48,7 +48,7 @@
<prover
id="11"
name="Gappa"
version="1.0.0"/>
version="1.1.1"/>
<prover
id="12"
name="MetiTarski"
......
......@@ -4,7 +4,7 @@
<prover
id="0"
name="Gappa"
version="1.0.0"/>
version="1.1.1"/>
<file
name="../gappa.why"
verified="true"
......
......@@ -28,7 +28,7 @@
<prover
id="6"
name="Gappa"
version="1.0.0"/>
version="1.1.1"/>
<prover
id="7"
name="Spass"
......
......@@ -175,19 +175,12 @@ driver = "drivers/eprover.drv"
[ATP gappa]
name = "Gappa"
exec = "gappa"
exec = "gappa-1.1.0"
exec = "gappa-1.1.1"
exec = "gappa-1.0.0"
exec = "gappa-0.16.1"
exec = "gappa-0.16.0"
exec = "gappa-0.15.1"
exec = "gappa-0.14.1"
exec = "gappa-0.13.0"
exec = "gappa-0.12.3"
version_switch = "--version"
version_regexp = "Gappa \\([^ \n]*\\)"
version_ok = "^1\.[0-1]\..+$"
version_ok = "^0\.1[4-8]\..+$"
version_old = "^0\.1[1-3]\..+$"
version_old = "^0\.1[1-8]\..+$"
command = "%l/why3-cpulimit %t %m -s %e -Eprecision=70"
driver = "drivers/gappa.drv"
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment