Commit 7a8f4458 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Update obsolete sessions.

parent 906a84ea
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/usr/local/share/why3/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/users/demons/melquion/src/why3/share/why3session.dtd">
<why3session
name="bitvectors/double/why3session.xml" shape_version="2">
<prover
......@@ -47,7 +47,7 @@
name="nth_one1"
locfile="bitvectors/double/../double.why"
loclnum="73" loccnumb="8" loccnume="16"
sum="06f37921b8d6e1de5911cfa60ee3f495"
sum="68b26f6bd21633cb2cb9250019b673f2"
proved="true"
expanded="false"
shape="ainfix =anthaoneV0aFalseIainfix &lt;=V0c51Aainfix &lt;=c0V0F">
......@@ -64,7 +64,7 @@
name="nth_one2"
locfile="bitvectors/double/../double.why"
loclnum="74" loccnumb="8" loccnume="16"
sum="07d361ed2fa63880733bc14101b15f6e"
sum="f08cb866a3ab9529aea096452c0c2aba"
proved="true"
expanded="false"
shape="ainfix =anthaoneV0aTrueIainfix &lt;=V0c61Aainfix &lt;=c52V0F">
......@@ -74,14 +74,14 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.22"/>
<result status="valid" time="0.23"/>
</proof>
</goal>
<goal
name="nth_one3"
locfile="bitvectors/double/../double.why"
loclnum="75" loccnumb="8" loccnume="16"
sum="b76bf4048e9811e187d0ef7e4dacce4e"
sum="45f916af66fcd9ac376a27c68412cbea"
proved="true"
expanded="false"
shape="ainfix =anthaoneV0aFalseIainfix &lt;=V0c63Aainfix &lt;=c62V0F">
......@@ -98,7 +98,7 @@
name="sign_one"
locfile="bitvectors/double/../double.why"
loclnum="77" loccnumb="8" loccnume="16"
sum="9e7ae345c718068eb332ff5be1cc0617"
sum="ae26ebd49d4971fd05324b0e13322dd7"
proved="true"
expanded="false"
shape="ainfix =asignaoneaFalse">
......@@ -108,7 +108,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.12"/>
<result status="valid" time="0.11"/>
</proof>
<proof
prover="1"
......@@ -132,7 +132,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.03"/>
</proof>
<proof
prover="5"
......@@ -140,14 +140,14 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.10"/>
<result status="valid" time="0.11"/>
</proof>
</goal>
<goal
name="exp_one"
locfile="bitvectors/double/../double.why"
loclnum="78" loccnumb="8" loccnume="15"
sum="817bbb0bf9d16ebf84d1209148a2d86b"
sum="df76b3cb3a441260a89d05f9f45d59fb"
proved="true"
expanded="false"
shape="ainfix =aexpaonec1023">
......@@ -157,7 +157,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="2.08"/>
<result status="valid" time="2.09"/>
</proof>
<proof
prover="3"
......@@ -166,14 +166,14 @@
edited="double_TestDouble_exp_one_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.58"/>
<result status="valid" time="0.67"/>
</proof>
</goal>
<goal
name="mantissa_one"
locfile="bitvectors/double/../double.why"
loclnum="79" loccnumb="8" loccnume="20"
sum="4e7bcdfa56cb11635fc70f768867ab60"
sum="fea308f93f031eb47ac1cca53b50bafd"
proved="true"
expanded="false"
shape="ainfix =amantissaaonec0">
......@@ -183,7 +183,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.70"/>
<result status="valid" time="0.69"/>
</proof>
<proof
prover="0"
......@@ -191,7 +191,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.10"/>
<result status="valid" time="0.09"/>
</proof>
<proof
prover="5"
......@@ -199,14 +199,14 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="2.86"/>
<result status="valid" time="2.91"/>
</proof>
</goal>
<goal
name="double_value_of_1"
locfile="bitvectors/double/../double.why"
loclnum="81" loccnumb="8" loccnume="25"
sum="362e56694a4e63a3214575ce1d7ffbc7"
sum="5c567bd886a7249af1b84ee36fa83a02"
proved="true"
expanded="false"
shape="ainfix =adouble_of_bv64aonec1.0">
......@@ -224,7 +224,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.04"/>
</proof>
<proof
prover="2"
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/usr/local/share/why3/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/users/demons/melquion/src/why3/share/why3session.dtd">
<why3session
name="bitvectors/neg_as_xor/why3session.xml" shape_version="2">
<prover
......@@ -32,7 +32,7 @@
name="Nth_j"
locfile="bitvectors/neg_as_xor/../neg_as_xor.why"
loclnum="13" loccnumb="8" loccnume="13"
sum="f0956e2cb757960a17f81a3067b715a6"
sum="ffa7aadc98c7c81aa8afa142b455755d"
proved="true"
expanded="false"
shape="ainfix =anthajV0aFalseIainfix &lt;=V0c62Aainfix &lt;=c0V0F">
......@@ -42,14 +42,14 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.27"/>
<result status="valid" time="0.28"/>
</proof>
</goal>
<goal
name="sign_of_j"
locfile="bitvectors/neg_as_xor/../neg_as_xor.why"
loclnum="15" loccnumb="8" loccnume="17"
sum="682b25f524efe50b9b47b2d9cd3c5ebc"
sum="eff4aeb7674767da11cced006af36114"
proved="true"
expanded="false"
shape="ainfix =asignajaTrue">
......@@ -66,7 +66,7 @@
name="mantissa_of_j"
locfile="bitvectors/neg_as_xor/../neg_as_xor.why"
loclnum="16" loccnumb="8" loccnume="21"
sum="13cc5b0010039968be9ba46aa4ccd86c"
sum="2efb10e521eba776b7ece640f4473a5f"
proved="true"
expanded="false"
shape="ainfix =amantissaajc0">
......@@ -76,7 +76,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.67"/>
<result status="valid" time="0.69"/>
</proof>
<proof
prover="0"
......@@ -92,14 +92,14 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="3.05"/>
<result status="valid" time="3.10"/>
</proof>
</goal>
<goal
name="exp_of_j"
locfile="bitvectors/neg_as_xor/../neg_as_xor.why"
loclnum="17" loccnumb="8" loccnume="16"
sum="e05572302f7143feff19510e43ab8d5e"
sum="fc87a20dea9a71534d543df10bf7ab7f"
proved="true"
expanded="false"
shape="ainfix =aexpajc0">
......@@ -109,7 +109,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.69"/>
<result status="valid" time="0.71"/>
</proof>
<proof
prover="0"
......@@ -125,14 +125,14 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="3.37"/>
<result status="valid" time="3.44"/>
</proof>
</goal>
<goal
name="int_of_bv"
locfile="bitvectors/neg_as_xor/../neg_as_xor.why"
loclnum="18" loccnumb="8" loccnume="17"
sum="61e2aff1d7bd95ae2a08d5fa89369fae"
sum="23ea5b39ea99f819456d1b2e7e0344f2"
proved="true"
expanded="false"
shape="ainfix =adouble_of_bv64ajc0.0">
......@@ -142,7 +142,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.12"/>
<result status="valid" time="0.11"/>
</proof>
<proof
prover="0"
......@@ -158,14 +158,14 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.11"/>
<result status="valid" time="0.10"/>
</proof>
</goal>
<goal
name="MainResultBits"
locfile="bitvectors/neg_as_xor/../neg_as_xor.why"
loclnum="20" loccnumb="8" loccnume="22"
sum="19ca0ae277e12bb1ec831954401ceac3"
sum="4707f538b9d68b3fa116ca0ad59aa071"
proved="true"
expanded="false"
shape="ainfix =anthabw_xorV0ajV1anthV0V1Iainfix &lt;V1c63Aainfix &lt;=c0V1FF">
......@@ -182,7 +182,7 @@
name="MainResultSign"
locfile="bitvectors/neg_as_xor/../neg_as_xor.why"
loclnum="23" loccnumb="8" loccnume="22"
sum="ef1b5e1c8fd4d961aa2ec3e400594311"
sum="6352e7cd945029c87d1ea3a6482d4683"
proved="true"
expanded="false"
shape="ainfix =anthabw_xorV0ajc63anotbanthV0c63F">
......@@ -199,7 +199,7 @@
name="Sign_of_xor_j"
locfile="bitvectors/neg_as_xor/../neg_as_xor.why"
loclnum="25" loccnumb="8" loccnume="21"
sum="09c25162719fe2d5f04b4a958353d6c7"
sum="44f96c656d009bca0b5dabe0f3343dd7"
proved="true"
expanded="false"
shape="ainfix =asignabw_xorV0ajanotbasignV0F">
......@@ -232,7 +232,7 @@
name="Exp_of_xor_j"
locfile="bitvectors/neg_as_xor/../neg_as_xor.why"
loclnum="27" loccnumb="8" loccnume="20"
sum="32330f454a4e9cdd0863a6fead5e0491"
sum="4836861f99a9dc39ab00265e89154d00"
proved="true"
expanded="false"
shape="ainfix =aexpabw_xorV0ajaexpV0F">
......@@ -242,7 +242,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.70"/>
<result status="valid" time="0.71"/>
</proof>
<proof
prover="0"
......@@ -258,14 +258,14 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="3.06"/>
<result status="valid" time="3.18"/>
</proof>
</goal>
<goal
name="Mantissa_of_xor_j"
locfile="bitvectors/neg_as_xor/../neg_as_xor.why"
loclnum="29" loccnumb="8" loccnume="25"
sum="ff7efb49476971e2ae56be09001b5037"
sum="5662f7f7ef7b6f8e2d958c949cdb6b93"
proved="true"
expanded="false"
shape="ainfix =amantissaabw_xorV0ajamantissaV0F">
......@@ -275,7 +275,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.71"/>
<result status="valid" time="0.72"/>
</proof>
<proof
prover="0"
......@@ -283,7 +283,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.57"/>
<result status="valid" time="0.58"/>
</proof>
<proof
prover="3"
......@@ -291,14 +291,14 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="2.90"/>
<result status="valid" time="3.00"/>
</proof>
</goal>
<goal
name="MainResultZero"
locfile="bitvectors/neg_as_xor/../neg_as_xor.why"
loclnum="31" loccnumb="8" loccnume="22"
sum="856675b97e95759d373dbfd29851a233"
sum="3218b62d0748383b9d38e4f71ffd6cb1"
proved="true"
expanded="false"
shape="ainfix =adouble_of_bv64abw_xorV0ajaprefix -.adouble_of_bv64V0Iainfix =amantissaV0c0Aainfix =c0aexpV0F">
......@@ -308,7 +308,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.96"/>
<result status="valid" time="0.97"/>
</proof>
<proof
prover="0"
......@@ -316,7 +316,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="1.73"/>
<result status="valid" time="1.77"/>
</proof>
<proof
prover="3"
......@@ -324,14 +324,14 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="3.32"/>
<result status="valid" time="3.33"/>
</proof>
</goal>
<goal
name="sign_neg"
locfile="bitvectors/neg_as_xor/../neg_as_xor.why"
loclnum="34" loccnumb="8" loccnume="16"
sum="512a9c88e57a3fdb1b019741fa36287d"
sum="eb021a51368e1a70d9d38dcc3ade5616"
proved="true"
expanded="false"
shape="ainfix =asign_valueanotbasignV0aprefix -.asign_valueasignV0F">
......@@ -341,14 +341,14 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="2.78"/>
<result status="valid" time="2.86"/>
</proof>
</goal>
<goal
name="MainResult"
locfile="bitvectors/neg_as_xor/../neg_as_xor.why"
loclnum="36" loccnumb="8" loccnume="18"
sum="4849d551d35fd59faec06345b4bdfeb8"
sum="3c4e973663d5b160e10c91d79275f1a9"
proved="true"
expanded="true"
shape="ainfix =adouble_of_bv64abw_xorV0ajaprefix -.adouble_of_bv64V0Iainfix &lt;aexpV0c2047Aainfix &lt;c0aexpV0F">
......@@ -359,7 +359,7 @@
edited="neg_as_xor_TestNegAsXOR_MainResult_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.94"/>
<result status="valid" time="1.04"/>
</proof>
</goal>
</theory>
......
This diff is collapsed.
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/usr/local/share/why3/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/users/demons/melquion/src/why3/share/why3session.dtd">
<why3session
name="bts/12475/why3session.xml" shape_version="2">
<prover
......@@ -34,7 +34,7 @@
name="toto"
locfile="bts/12475/../12475.why"
loclnum="6" loccnumb="7" loccnume="11"
sum="b2db1ecda9fbba750ff04a700c301dfe"
sum="124ff5e00ef7f3e7e752aa5c976dfeed"
proved="true"
expanded="true"
shape="ainfix &lt;V0ainfix +aroundaUpV0c1.F">
......@@ -44,7 +44,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="1"
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/andrei/prj/why-git/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/users/demons/melquion/src/why3/share/why3session.dtd">
<why3session
name="bts/13853/why3session.xml" shape_version="2">
<prover
......@@ -21,7 +21,7 @@
locfile="bts/13853/../13853.mlw"
loclnum="16" loccnumb="8" loccnume="9"
expl="exceptional postcondition"
sum="d865701dbb7f87358e2cdfcba8f2bd06"
sum="893cd69e3c7345f5514a1b4ddab4cd80"
proved="true"
expanded="false"
shape="t">
......@@ -33,7 +33,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
......@@ -41,7 +41,7 @@
locfile="bts/13853/../13853.mlw"
loclnum="18" loccnumb="7" loccnume="8"
expl="exceptional postcondition"
sum="6ba20de7876f29cbedefdbabd855b605"
sum="bddadcafb90c4cc9043521e5c27e2f6f"
proved="true"
expanded="false"
shape="t">
......@@ -53,7 +53,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
</theory>
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/users/demons/melquion/src/why3/share/why3session.dtd">
<why3session
name="bts/fsetint/why3session.xml" shape_version="2">
<prover
......@@ -40,7 +40,7 @@
name="l_false"
locfile="bts/fsetint/../fsetint.why"
loclnum="5" loccnumb="9" loccnume="16"
sum="dccc55c14590d1b87dbed47d9b0b7ca4"
sum="0b906d19fc47dc5b0bc0f52ad3c7e2a6"
proved="false"
expanded="true"
shape="f">
......@@ -104,7 +104,7 @@
name="mem_integer"
locfile="bts/fsetint/../fsetint.why"
loclnum="13" loccnumb="8" loccnume="19"
sum="83012d44889c35b4b77dfddaf6119875"
sum="0e867f2d3083e428ad1c9c1a524b8ded"
proved="false"
expanded="true"
shape="amemV0aintegerF">
......@@ -154,14 +154,14 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
<result status="unknown" time="0.01"/>
</proof>
</goal>
<goal
name="foo"
locfile="bts/fsetint/../fsetint.why"
loclnum="15" loccnumb="7" loccnume="10"
sum="1ac5f7ac42f0e2a8b0d1a1f11f9f0d71"
sum="f6b9b46665fbeed71dcc8e03749b097f"
proved="false"
expanded="true"
shape="f">
......@@ -225,7 +225,7 @@
name="foo"
locfile="bts/fsetint/../fsetint.why"
loclnum="30" loccnumb="7" loccnume="10"
sum="298aff6b85501a01c5fd7cab28f641d0"
sum="ee9eb17e39034c473cffb6f065106935"
proved="false"
expanded="true"
shape="f">
......@@ -235,7 +235,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
<result status="unknown" time="0.01"/>
</proof>
<proof
prover="2"
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/users/demons/melquion/src/why3/share/why3session.dtd">
<why3session
name="check-builtin/array/why3session.xml" shape_version="2">
<prover
......@@ -44,7 +44,7 @@
name="G1"
locfile="check-builtin/array/../array.why"
loclnum="4" loccnumb="7" loccnume="9"
sum="4b45d6270f4a53daefb6fce54b8ebff7"
sum="b1b23c8283e46198921be8711654af8c"
proved="true"
expanded="true"
shape="ainfix =agetasetV2V1V0V1V0FF">
......@@ -62,7 +62,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="1"
......@@ -78,7 +78,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="2"
......@@ -109,7 +109,7 @@
name="G2"
locfile="check-builtin/array/../array.why"
loclnum="6" loccnumb="7" loccnume="9"
sum="6ccca0aeacb41ec5118c79435eb055a1"
sum="7e66ed444e94f55df480003cd20a589c"
proved="true"
expanded="true"
shape="ainfix =agetasetV5V0V4V3V1Iainfix =agetV5V3V1Iainfix =V3V0NFF">
......@@ -143,7 +143,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="2"
......@@ -159,7 +159,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="3"
......@@ -174,7 +174,7 @@
name="G3"
locfile="check-builtin/array/../array.why"
loclnum="10" loccnumb="7" loccnume="9"
sum="6108a9e01a2539ed185406b5ade7ca86"
sum="400615409a3f600f2025269e1c4492c2"
proved="true"
expanded="true"
shape="ainfix =agetasetV2c1V1c0V0Iainfix =agetV2c0V0FF">
......@@ -192,7 +192,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.14"/>
<result status="valid" time="0.17"/>
</proof>
<proof
prover="1"
......@@ -239,7 +239,7 @@
name="G4"
locfile="check-builtin/array/../array.why"
loclnum="13" loccnumb="7" loccnume="9"
sum="34fa3208c06f03a03e0897d791b6fa13"
sum="b0f82094e35dbd134112abc5ff16bcc8"
proved="true"