Commit 2e43db62 authored by MARCHE Claude's avatar MARCHE Claude

update obsolete sessions after patch on checksum

parent e4267f5c
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/check-builtin/ac/why3session.xml">
<prover id="alt-ergo" name="Alt-Ergo" version="0.93"/>
<prover id="coq" name="Coq" version="8.3pl2"/>
<prover id="cvc3" name="CVC3" version="2.2"/>
<prover id="gappa" name="Gappa" version="0.15.0"/>
<prover id="simplify" name="Simplify" version="1.5.4"/>
<prover id="spass" name="Spass" version="3.7"/>
<prover id="vampire" name="Vampire" version="0.6"/>
<prover id="yices" name="Yices" version="1.0.25"/>
<prover id="z3" name="Z3" version="2.19"/>
<file name="../ac.why" verified="true" expanded="true">
<theory name="Test" verified="true" expanded="true">
<goal name="G1" sum="fa87ff4f5d7bfd19a59c9e156ce503b1" proved="true" expanded="true" shape="ainfix =afV0V1afV1V0F">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<why3session
name="check-builtin/ac/why3session.xml">
<prover
id="alt-ergo"
name="Alt-Ergo"
version="0.93"/>
<prover
id="coq"
name="Coq"
version="8.3pl2"/>
<prover
id="cvc3"
name="CVC3"
version="2.2"/>
<prover
id="gappa"
name="Gappa"
version="0.15.0"/>
<prover
id="simplify"
name="Simplify"
version="1.5.4"/>
<prover
id="spass"
name="Spass"
version="3.7"/>
<prover
id="vampire"
name="Vampire"
version="0.6"/>
<prover
id="yices"
name="Yices"
version="1.0.25"/>
<prover
id="z3"
name="Z3"
version="2.19"/>
<file
name="../ac.why"
verified="true"
expanded="true">
<theory
name="Test"
verified="true"
expanded="true">
<goal
name="G1"
sum="45e02e66d9739a55c44525af4d6e4458"
proved="true"
expanded="true"
shape="ainfix =afV0V1afV1V0F">
<proof
prover="cvc3"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<proof
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<proof
prover="z3"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
<proof
prover="spass"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="G2" sum="596822f280e706913494c5aafa0c406d" proved="true" expanded="true" shape="ainfix =afafV0V1V2afV0afV1V2F">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<goal
name="G2"
sum="e397e36857589fae6d7f9b1f39ca555c"
proved="true"
expanded="true"
shape="ainfix =afafV0V1V2afV0afV1V2F">
<proof
prover="cvc3"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<proof
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<proof
prover="z3"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
<proof
prover="spass"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
</theory>
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="check-builtin/array/why3session.xml">
<prover id="alt-ergo" name="Alt-Ergo" version="0.93"/>
<prover id="coq" name="Coq" version="8.3pl2"/>
<prover id="cvc3" name="CVC3" version="2.2"/>
<prover id="gappa" name="Gappa" version="0.15.0"/>
<prover id="simplify" name="Simplify" version="1.5.4"/>
<prover id="spass" name="Spass" version="3.7"/>
<prover id="vampire" name="Vampire" version="0.6"/>
<prover id="yices" name="Yices" version="1.0.25"/>
<prover id="z3" name="Z3" version="2.19"/>
<file name="../array.why" verified="true" expanded="true">
<theory name="Test_simplify_array" verified="true" expanded="true">
<goal name="G1" sum="236061dc63571fd08d3960c30b3a3ef2" proved="true" expanded="true" shape="ainfix =agetasetV2V1V0V1V0FF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<why3session
name="check-builtin/array/why3session.xml">
<prover
id="alt-ergo"
name="Alt-Ergo"
version="0.93"/>
<prover
id="coq"
name="Coq"
version="8.3pl2"/>
<prover
id="cvc3"
name="CVC3"
version="2.2"/>
<prover
id="gappa"
name="Gappa"
version="0.15.0"/>
<prover
id="simplify"
name="Simplify"
version="1.5.4"/>
<prover
id="spass"
name="Spass"
version="3.7"/>
<prover
id="vampire"
name="Vampire"
version="0.6"/>
<prover
id="yices"
name="Yices"
version="1.0.25"/>
<prover
id="z3"
name="Z3"
version="2.19"/>
<file
name="../array.why"
verified="true"
expanded="true">
<theory
name="Test_simplify_array"
verified="true"
expanded="true">
<goal
name="G1"
sum="29ec6c5848eb3ed18713d686702aef5e"
proved="true"
expanded="true"
shape="ainfix =agetasetV2V1V0V1V0FF">
<proof
prover="cvc3"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<proof
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<proof
prover="z3"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<proof
prover="spass"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="G2" sum="513c66a055e3640e12c0ee979bfe922a" proved="true" expanded="true" shape="ainfix =agetasetV5V0V4V3V1Iainfix =agetV5V3V1Iainfix =V3V0NFF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<goal
name="G2"
sum="9ca083c595c2b42b28299af777f91406"
proved="true"
expanded="true"
shape="ainfix =agetasetV5V0V4V3V1Iainfix =agetV5V3V1Iainfix =V3V0NFF">
<proof
prover="cvc3"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<proof
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<proof
prover="z3"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<proof
prover="spass"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="G3" sum="24f733b6ec5fd3c898c797c4f8d4e82e" proved="true" expanded="true" shape="ainfix =agetasetV2c1V1c0V0Iainfix =agetV2c0V0FF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<goal
name="G3"
sum="bc20452878718e3a9221c68f6c073ca0"
proved="true"
expanded="true"
shape="ainfix =agetasetV2c1V1c0V0Iainfix =agetV2c0V0FF">
<proof
prover="cvc3"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<proof
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<proof
prover="z3"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.15"/>
<proof
prover="spass"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.14"/>
</proof>
</goal>
<goal name="G4" sum="c193125d14526422133026f1ae07551e" proved="true" expanded="true" shape="ainfix =agetasetasetV2c1V1c0V0c1V1FF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<goal
name="G4"
sum="866acb8953cccc8b3f703b9ef8b1b70c"
proved="true"
expanded="true"
shape="ainfix =agetasetasetV2c1V1c0V0c1V1FF">
<proof
prover="cvc3"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<proof
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<proof
prover="z3"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<proof
prover="spass"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.19"/>
</proof>
</goal>
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="check-builtin/bool/why3session.xml">
<prover id="alt-ergo" name="Alt-Ergo" version="0.93"/>
<prover id="coq" name="Coq" version="8.3pl2"/>
<prover id="cvc3" name="CVC3" version="2.2"/>
<prover id="gappa" name="Gappa" version="0.15.0"/>
<prover id="simplify" name="Simplify" version="1.5.4"/>
<prover id="spass" name="Spass" version="3.7"/>
<prover id="vampire" name="Vampire" version="0.6"/>
<prover id="yices" name="Yices" version="1.0.25"/>
<prover id="z3" name="Z3" version="2.19"/>
<file name="../bool.why" verified="true" expanded="true">
<theory name="Test" verified="true" expanded="true">
<goal name="G1" sum="5e6719215b28357019f9093ba80a13ae" proved="true" expanded="true" shape="ainfix =aTrueaFalseN">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<why3session
name="check-builtin/bool/why3session.xml">
<prover
id="alt-ergo"
name="Alt-Ergo"
version="0.93"/>
<prover
id="coq"
name="Coq"
version="8.3pl2"/>
<prover
id="cvc3"
name="CVC3"
version="2.2"/>
<prover
id="gappa"
name="Gappa"
version="0.15.0"/>
<prover
id="simplify"
name="Simplify"
version="1.5.4"/>
<prover
id="spass"
name="Spass"
version="3.7"/>
<prover
id="vampire"
name="Vampire"
version="0.6"/>
<prover
id="yices"
name="Yices"
version="1.0.25"/>
<prover
id="z3"
name="Z3"
version="2.19"/>
<file
name="../bool.why"
verified="true"
expanded="true">
<theory
name="Test"
verified="true"
expanded="true">
<goal
name="G1"
sum="8448ab8d0500172c3ab2c0b3831f2a80"
proved="true"
expanded="true"
shape="ainfix =aTrueaFalseN">
<proof
prover="cvc3"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<proof
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<proof
prover="z3"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<proof
prover="spass"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="G2" sum="c7425a171e64e10c6cdebdcf3addcadc" proved="true" expanded="true" shape="ainfix =V0aFalseOainfix =V0aTrueF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<goal
name="G2"
sum="9e2baed029f6b942f211d65adab0c03b"
proved="true"
expanded="true"
shape="ainfix =V0aFalseOainfix =V0aTrueF">
<proof
prover="cvc3"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<proof
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<proof
prover="z3"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<proof
prover="spass"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="G3" sum="601dae5d276391434bfebe04388a4f59" proved="true" expanded="true" shape="fIainfix =V2V0NAainfix =V1V2NAainfix =V0V1NF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<goal
name="G3"
sum="56e344acd505f1c2135ed5a2d2500321"
proved="true"
expanded="true"
shape="fIainfix =V2V0NAainfix =V1V2NAainfix =V0V1NF">
<proof
prover="cvc3"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="unknown" time="0.01"/>
<proof
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
<result status="unknown" time="0.00"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<proof
prover="z3"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
<proof
prover="spass"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
</theory>
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="check-builtin/euclideandivision/why3session.xml">
<prover id="alt-ergo" name="Alt-Ergo" version="0.93"/>
<prover id="coq" name="Coq" version="8.3pl2"/>
<prover id="cvc3" name="CVC3" version="2.2"/>
<prover id="gappa" name="Gappa" version="0.15.0"/>
<prover id="simplify" name="Simplify" version="1.5.4"/>
<prover id="spass" name="Spass" version="3.7"/>
<prover id="vampire" name="Vampire" version="0.6"/>
<prover id="yices" name="Yices" version="1.0.25"/>
<prover id="z3" name="Z3" version="2.19"/>
<file name="../euclideandivision.why" verified="true" expanded="true">
<theory name="Test" verified="true" expanded="true">
<goal name="G1" sum="90824745f1a68d5b5da57840125d3fdf" proved="true" expanded="true" shape="ainfix =amodc10c3c1">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<why3session
name="check-builtin/euclideandivision/why3session.xml">
<prover
id="alt-ergo"
name="Alt-Ergo"
version="0.93"/>
<prover
id="coq"
name="Coq"
version="8.3pl2"/>
<prover
id="cvc3"
name="CVC3"
version="2.2"/>
<prover
id="gappa"
name="Gappa"
version="0.15.0"/>
<prover
id="simplify"
name="Simplify"
version="1.5.4"/>
<prover
id="spass"
name="Spass"
version="3.7"/>
<prover
id="vampire"
name="Vampire"
version="0.6"/>
<prover
id="yices"
name="Yices"
version="1.0.25"/>
<prover
id="z3"
name="Z3"
version="2.19"/>
<file
name="../euclideandivision.why"
verified="true"
expanded="true">
<theory
name="Test"
verified="true"
expanded="true">
<goal
name="G1"
sum="4dc9ae7d5b1a4ba9a7b8e25ccadca2ab"
proved="true"
expanded="true"
shape="ainfix =amodc10c3c1">
<proof
prover="cvc3"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<proof
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<proof
prover="z3"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.64"/>
<proof
prover="spass"
timelimit="10"
edited=""
obsolete="false">
<result status="timeout" time="10.66"/>
</proof>
</goal>
<goal name="G2" sum="9b4f0670f5abfa09eb5977e0253d4fd7" proved="true" expanded="true" shape="ainfix =adivc10c3c3">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<goal
name="G2"
sum="72097fc8849d86d1b24de44d3735fd4d"
proved="true"
expanded="true"
shape="ainfix =adivc10c3c3">
<proof
prover="cvc3"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<proof
prover="alt-ergo"
timelimit="10"