Commit a46349ca authored by MARCHE Claude's avatar MARCHE Claude
Browse files

session updates after prover upgrade

parent 316f02ad
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session
name="bts/12475/why3session.xml">
name="examples/bts/12475/why3session.xml">
<prover
id="alt-ergo"
id="0"
name="Alt-Ergo"
version="0.94"/>
<prover
id="coq"
name="Coq"
version="8.3pl3"/>
<prover
id="cvc3-2.2"
id="1"
name="CVC3"
version="2.2"/>
<prover
id="cvc3-2.4"
name="CVC3"
version="2.4.1"/>
<prover
id="eprover"
name="Eprover"
version="1.4"/>
<prover
id="gappa"
id="2"
name="Gappa"
version="0.15.1"/>
<prover
id="simplify"
name="Simplify"
version="1.5.4"/>
<prover
id="spass"
name="Spass"
version="3.7"/>
version="0.16.0"/>
<prover
id="vampire"
name="Vampire"
version="0.6"/>
<prover
id="verit"
name="veriT"
version="dev"/>
<prover
id="yices"
name="Yices"
version="1.0.25"/>
<prover
id="z3-2"
id="3"
name="Z3"
version="2.19"/>
<prover
id="z3-3"
name="Z3"
version="3.2"/>
<file
name="../12475.why"
verified="true"
expanded="true">
<theory
name="Stmt"
locfile="examples/bts/12475/../12475.why"
loclnum="1" loccnumb="7" loccnume="11"
verified="true"
expanded="true">
<label
name="some_statement">
</label>
<goal
name="toto"
locfile="examples/bts/12475/../12475.why"
loclnum="6" loccnumb="7" loccnume="11"
sum="2ba9689c5337113bcea3af15657e9144"
proved="true"
expanded="true"
shape="ainfix <V0ainfix +aroundaUpV0c1.F">
<proof
prover="z3-2"
prover="3"
timelimit="2"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="cvc3-2.2"
prover="1"
timelimit="2"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="alt-ergo"
prover="0"
timelimit="2"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="gappa"
timelimit="2"
edited=""
obsolete="false">
prover="2"
timelimit="5"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
</proof>
</goal>
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session
name="check-builtin/floats/why3session.xml">
name="examples/check-builtin/floats/why3session.xml">
<prover
id="alt-ergo"
id="0"
name="Alt-Ergo"
version="0.94"/>
<prover
id="coq"
name="Coq"
version="8.3pl3"/>
<prover
id="cvc3-2.2"
id="1"
name="CVC3"
version="2.2"/>
<prover
id="cvc3-2.4"
name="CVC3"
version="2.4.1"/>
<prover
id="eprover"
name="Eprover"
version="1.4"/>
<prover
id="gappa"
id="2"
name="Gappa"
version="0.15.1"/>
<prover
id="simplify"
name="Simplify"
version="1.5.4"/>
<prover
id="spass"
name="Spass"
version="3.7"/>
version="0.16.0"/>
<prover
id="vampire"
name="Vampire"
version="0.6"/>
<prover
id="verit"
name="veriT"
version="dev"/>
<prover
id="yices"
name="Yices"
version="1.0.25"/>
<prover
id="z3-2"
id="3"
name="Z3"
version="2.19"/>
<prover
id="z3-3"
name="Z3"
version="3.2"/>
<file
name="../floats.why"
verified="true"
expanded="true">
<theory
name="TestGappa"
locfile="examples/check-builtin/floats/../floats.why"
loclnum="2" loccnumb="7" loccnume="16"
verified="true"
expanded="true">
<goal
name="Round_single_01"
locfile="examples/check-builtin/floats/../floats.why"
loclnum="11" loccnumb="7" loccnume="22"
sum="4e928e1b5febc9bcd148dfb85835ab49"
proved="true"
expanded="true"
shape="ainfix =aroundaNearestTiesToEvenc0.1c0x1.99999ap-4">
<proof
prover="gappa"
prover="2"
timelimit="5"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="Round_double_01"
locfile="examples/check-builtin/floats/../floats.why"
loclnum="14" loccnumb="7" loccnume="22"
sum="8cc089135a59e2ab087a08a13d587d28"
proved="true"
expanded="true"
shape="ainfix =aroundaNearestTiesToEvenc0.1c0x1.999999999999ap-4">
<proof
prover="gappa"
prover="2"
timelimit="5"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="Test00"
locfile="examples/check-builtin/floats/../floats.why"
loclnum="17" loccnumb="8" loccnume="14"
sum="82fbc864e6e6a33d8a3e7850715af655"
proved="true"
expanded="true"
shape="ainfix <=aprefix -c3.0V0Iainfix <=aabsV0c2.0F">
<proof
prover="z3-2"
prover="3"
timelimit="5"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="cvc3-2.2"
prover="1"
timelimit="5"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="alt-ergo"
prover="0"
timelimit="5"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="gappa"
prover="2"
timelimit="5"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="Test01"
locfile="examples/check-builtin/floats/../floats.why"
loclnum="19" loccnumb="8" loccnume="14"
sum="b36ee8c5c24e4f96eb2a1dad86986324"
proved="true"
expanded="true"
shape="ainfix <=aabsainfix -ainfix *avalueV0avalueV0aroundaNearestTiesToEvenainfix *avalueV0avalueV0c0x1.p-52Iainfix <=avalueV0c2.0Aainfix <=aprefix -c2.0avalueV0F">
<proof
prover="gappa"
prover="2"
timelimit="5"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="Test02"
locfile="examples/check-builtin/floats/../floats.why"
loclnum="25" loccnumb="8" loccnume="14"
sum="645db8205ab2ae42952c3ac8d735dff8"
proved="true"
expanded="true"
shape="ainfix <=aabsainfix -ainfix *avalueV1avalueV1aroundaNearestTiesToEvenainfix *avalueV0avalueV0c0x1.p-52Iainfix =V1V0Iainfix <=aabsavalueV0c2.0F">
<proof
prover="gappa"
prover="2"
timelimit="5"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="Test03"
locfile="examples/check-builtin/floats/../floats.why"
loclnum="32" loccnumb="8" loccnume="14"
sum="95d9ef3dec936610365ed81d8e720aae"
proved="true"
expanded="true"
shape="ainfix <=asqrtainfix *ainfix -avalueV2ainfix *avalueV0avalueV0ainfix -avalueV1ainfix *avalueV0avalueV0c0x1.p-52Iainfix =V2V1Iainfix =avalueV1aroundaNearestTiesToEvenainfix *avalueV0avalueV0Iainfix <=aabsavalueV0c2.0F">
<proof
prover="gappa"
prover="2"
timelimit="5"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session
name="my_cosine/why3session.xml">
name="examples/my_cosine/why3session.xml">
<prover
id="0"
name="Alt-Ergo"
......@@ -13,20 +13,20 @@
<prover
id="2"
name="Gappa"
version="0.15.1"/>
version="0.16.0"/>
<file
name="../my_cosine.why"
verified="true"
expanded="true">
<theory
name="CosineSingle"
locfile="my_cosine/../my_cosine.why"
locfile="examples/my_cosine/../my_cosine.why"
loclnum="1" loccnumb="7" loccnume="19"
verified="true"
expanded="true">
<goal
name="MethodError"
locfile="my_cosine/../my_cosine.why"
locfile="examples/my_cosine/../my_cosine.why"
loclnum="13" loccnumb="6" loccnume="17"
sum="5952f9383dbffe78b1fa14037bc54de0"
proved="true"
......@@ -38,12 +38,12 @@
edited="my_cosine_CosineSingle_MethodError_1.v"
obsolete="false"
archived="false">
<result status="valid" time="3.73"/>
<result status="valid" time="4.00"/>
</proof>
</goal>
<goal
name="TotalErrorFullyExpanded"
locfile="my_cosine/../my_cosine.why"
locfile="examples/my_cosine/../my_cosine.why"
loclnum="20" loccnumb="6" loccnume="29"
sum="25f5a9c908fe4d1265b4f0f95504caa8"
proved="true"
......@@ -54,12 +54,12 @@
timelimit="2"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="TotalErrorExpanded"
locfile="my_cosine/../my_cosine.why"
locfile="examples/my_cosine/../my_cosine.why"
loclnum="31" loccnumb="6" loccnume="24"
sum="847de2c0fab20f50a5c8c20a22a7efcf"
proved="true"
......@@ -70,12 +70,12 @@
timelimit="2"
obsolete="false"
archived="false">
<result status="valid" time="0.86"/>
<result status="valid" time="0.83"/>
</proof>
</goal>
<goal
name="TotalError"
locfile="my_cosine/../my_cosine.why"
locfile="examples/my_cosine/../my_cosine.why"
loclnum="51" loccnumb="6" loccnume="16"
sum="5af50be8fb318e8a3b66da558f5685c7"
proved="true"
......@@ -86,7 +86,7 @@
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="3.04"/>
<result status="valid" time="3.05"/>
</proof>
</goal>
</theory>
......
<
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session
name="./ns_clone/why3session.xml">
name="examples/ns_clone/why3session.xml">
<prover
id="alt-ergo"
id="0"
name="Alt-Ergo"
version="0.94"/>
<prover
id="coq"
name="Coq"
version="8.3pl3"/>
<prover
id="cvc3-2.2"
id="1"
name="CVC3"
version="2.2"/>
<prover
id="eprover"
name="Eprover"
version="1.4"/>
<prover
id="gappa"
id="2"
name="Gappa"
version="0.15.1"/>
version="0.16.0"/>
<prover
id="simplify"
id="3"
name="Simplify"
version="1.5.4"/>
<prover
id="spass"
id="4"
name="Spass"
version="3.7"/>
<prover
id="vampire"
id="5"
name="Vampire"
version="0.6"/>
<prover
id="verit"
name="veriT"
version="dev"/>
<prover
id="yices"
id="6"
name="Yices"
version="1.0.25"/>
<prover
id="z3-2"
id="7"
name="Z3"
version="2.19"/>
<file
......@@ -52,152 +40,166 @@
expanded="true">
<theory
name="Sig"
locfile="examples/ns_clone/../ns_clone.why"
loclnum="1" loccnumb="7" loccnume="10"
verified="true"
expanded="true">
</theory>
<theory
name="Struct"
locfile="examples/ns_clone/../ns_clone.why"
loclnum="11" loccnumb="7" loccnume="13"
verified="true"
expanded="true">
<goal
name="AddMem"
locfile="examples/ns_clone/../ns_clone.why"
loclnum="8" loccnumb="8" loccnume="14"
sum="b6ef15114d241c69f0f9cd3d506d3d32"
proved="true"
expanded="true"
shape="amemV0aaddV0V1F">
<proof
prover="simplify"
prover="7"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="cvc3-2.2"
prover="4"
timelimit="5"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="alt-ergo"
prover="1"
timelimit="5"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="gappa"
prover="0"
timelimit="5"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="z3-2"
prover="2"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="yices"
prover="3"
timelimit="5"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="vampire"
prover="5"
timelimit="5"
edited=""
obsolete="false">
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="spass"
prover="6"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
</theory>
<theory
name="Shared"
locfile="examples/ns_clone/../ns_clone.why"
loclnum="26" loccnumb="7" loccnume="13"
verified="true"
expanded="true">
</theory>
<theory
name="AbstractUser"
locfile="examples/ns_clone/../ns_clone.why"
loclnum="30" loccnumb="7" loccnume="19"
verified="true"
expanded="true">
</theory>
<theory
name="ConcreteUser"
locfile="examples/ns_clone/../ns_clone.why"
loclnum="37" loccnumb="7" loccnume="19"
verified="true"
expanded="true">
<goal
name="AddMem"
locfile="examples/ns_clone/../ns_clone.why"
loclnum="8" loccnumb="8" loccnume="14"
sum="bba87d4c5622caffbd75ed8c97dc5383"
proved="true"
expanded="true"
shape="amemV0aaddV0V1F">
<proof
prover="simplify"