Skip to content

GitLab

why3
why3
Commit ae70d9dc authored by MARCHE Claude's avatar MARCHE Claude
Browse files
Options

update sessions after change in Vampire driver

parent ab6283f7
Hide whitespace changes
Inline Side-by-side
Showing with 68 additions and 68 deletions
examples/einstein/why3session.xml
View file @ ae70d9dc
......@@ -108,7 +108,7 @@
timelimit="5"
edited=""
obsolete="false">
<result status="unknown" time="4.98"/>
<result status="timeout" time="2.99"/>
</proof>
<proof
prover="spass"
......@@ -164,7 +164,7 @@
timelimit="5"
edited=""
obsolete="false">
<result status="unknown" time="4.99"/>
<result status="timeout" time="3.08"/>
</proof>
<proof
prover="spass"
......@@ -213,7 +213,7 @@
timelimit="5"
edited=""
obsolete="false">
<result status="unknown" time="4.99"/>
<result status="timeout" time="3.08"/>
</proof>
<proof
prover="spass"
......
examples/genealogy/why3session.xml
View file @ ae70d9dc
......@@ -9,7 +9,7 @@
<prover
id="coq"
name="Coq"
version="8.2pl1"/>
version="8.3pl2"/>
<prover
id="cvc3"
name="CVC3"
......@@ -60,19 +60,12 @@
proved="true"
expanded="true"
shape="adaughterV0V1OasonV0V1qachildV0V1F">
<proof
prover="simplify"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.02"/>
</proof>
<proof
prover="alt-ergo"
timelimit="5"
timelimit="3"
edited=""
obsolete="false">
<result status="unknown" time="0.01"/>
<result status="unknown" time="0.02"/>
</proof>
<proof
prover="cvc3"
......@@ -93,7 +86,7 @@
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="yices"
......@@ -123,13 +116,6 @@
proved="true"
expanded="true"
shape="asiblingV1V0IasiblingV0V1F">
<proof
prover="simplify"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.02"/>
</proof>
<proof
prover="cvc3"
timelimit="5"
......@@ -142,7 +128,7 @@
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="eprover"
......@@ -186,16 +172,9 @@
proved="true"
expanded="true"
shape="asisterV0V1OabrotherV0V1qasiblingV0V1F">
<proof
prover="simplify"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.12"/>
</proof>
<proof
prover="alt-ergo"
timelimit="5"
timelimit="3"
edited=""
obsolete="false">
<result status="unknown" time="0.01"/>
......@@ -240,7 +219,7 @@
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
......@@ -249,13 +228,6 @@
proved="true"
expanded="true"
shape="agrandmotherV0V1OagrandfatherV0V1qagrandparentV0V1F">
<proof
prover="simplify"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.12"/>
</proof>
<proof
prover="cvc3"
timelimit="5"
......@@ -275,7 +247,7 @@
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="z3"
......@@ -286,10 +258,10 @@
</proof>
<proof
prover="vampire"
timelimit="5"
timelimit="3"
edited=""
obsolete="false">
<result status="unknown" time="5.01"/>
<result status="timeout" time="3.08"/>
</proof>
<proof
prover="yices"
......@@ -300,10 +272,10 @@
</proof>
<proof
prover="spass"
timelimit="5"
timelimit="3"
edited=""
obsolete="false">
<result status="timeout" time="5.23"/>
<result status="timeout" time="3.45"/>
</proof>
</goal>
<goal
......@@ -312,13 +284,6 @@
proved="true"
expanded="true"
shape="ainfix =agenderV0aMaleIagrandfatherV0V1F">
<proof
prover="simplify"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.03"/>
</proof>
<proof
prover="cvc3"
timelimit="5"
......@@ -331,7 +296,7 @@
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="eprover"
......@@ -352,14 +317,14 @@
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="vampire"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.03"/>
</proof>
<proof
prover="spass"
......@@ -375,13 +340,6 @@
proved="true"
expanded="true"
shape="ainfix =agenderV0aFemaleIagrandmotherV0V1F">
<proof
prover="simplify"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.03"/>
</proof>
<proof
prover="cvc3"
timelimit="5"
......@@ -438,13 +396,6 @@
proved="true"
expanded="true"
shape="ainfix =V0V2Oainfix =V1V2Oainfix =V0V1IagrandfatherV2V3IagrandfatherV1V3IagrandfatherV0V3F">
<proof
prover="simplify"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.12"/>
</proof>
<proof
prover="cvc3"
timelimit="5"
......@@ -473,6 +424,13 @@
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="vampire"
timelimit="3"
edited=""
obsolete="false">
<result status="timeout" time="3.09"/>
</proof>
<proof
prover="yices"
timelimit="5"
......@@ -485,7 +443,7 @@
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
</theory>
......
examples/programs/fibonacci/why3session.xml
View file @ ae70d9dc
......@@ -233,6 +233,13 @@
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="vampire"
timelimit="3"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="WP_parameter logfib.2"
......@@ -255,6 +262,13 @@
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="vampire"
timelimit="3"
edited=""
obsolete="false">
<result status="timeout" time="2.98"/>
</proof>
</goal>
<goal
name="WP_parameter logfib.3"
......@@ -284,6 +298,13 @@
obsolete="false">
<result status="timeout" time="5.03"/>
</proof>
<proof
prover="vampire"
timelimit="3"
edited=""
obsolete="false">
<result status="timeout" time="2.99"/>
</proof>
</goal>
</transf>
</goal>
......@@ -359,6 +380,13 @@
obsolete="false">
<result status="timeout" time="5.03"/>
</proof>
<proof
prover="vampire"
timelimit="3"
edited=""
obsolete="false">
<result status="timeout" time="2.99"/>
</proof>
</goal>
<goal
name="fib_m.2"
......@@ -387,6 +415,13 @@
obsolete="false">
<result status="timeout" time="5.03"/>
</proof>
<proof
prover="vampire"
timelimit="3"
edited=""
obsolete="false">
<result status="timeout" time="2.99"/>
</proof>
</goal>
</transf>
</goal>
......@@ -411,6 +446,13 @@
obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="vampire"
timelimit="3"
edited=""
obsolete="false">
<result status="timeout" time="3.02"/>
</proof>
</goal>
</theory>
</file>
......
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