Attention une mise à jour du serveur va être effectuée le lundi 17 mai entre 13h et 13h30. Cette mise à jour va générer une interruption du service de quelques minutes.

Commit c4fa5942 authored by MARCHE Claude's avatar MARCHE Claude

updated obsolete sessions

parent 62029d77
......@@ -47,7 +47,7 @@
name="Nth_bw_xor_v1true"
locfile="../bitvector.why"
loclnum="46" loccnumb="8" loccnume="25"
sum="53e58804e10b8d4df248321a9d6c4661"
sum="bcc6cb005e612af7c3a2608981d60757"
proved="true"
expanded="false"
shape="ainfix =anthabw_xorV0V1V2anotbanthV1V2Iainfix =anthV0V2aTrueAainfix <V2asizeAainfix <=c0V2F">
......@@ -80,7 +80,7 @@
name="Nth_bw_xor_v1false"
locfile="../bitvector.why"
loclnum="50" loccnumb="8" loccnume="26"
sum="0a603299c90b5c0937109a7c11e79a2c"
sum="48b5a4d291ba174b9d4bb37c998c52c8"
proved="true"
expanded="false"
shape="ainfix =anthabw_xorV0V1V2anthV1V2Iainfix =anthV0V2aFalseAainfix <V2asizeAainfix <=c0V2F">
......@@ -105,7 +105,7 @@
name="Nth_bw_xor_v2true"
locfile="../bitvector.why"
loclnum="54" loccnumb="8" loccnume="25"
sum="a23ee6e27e2057044a06cb62f728c700"
sum="524a661fac22016f966e9de1aac78a4a"
proved="true"
expanded="false"
shape="ainfix =anthabw_xorV0V1V2anotbanthV0V2Iainfix =anthV1V2aTrueAainfix <V2asizeAainfix <=c0V2F">
......@@ -138,7 +138,7 @@
name="Nth_bw_xor_v2false"
locfile="../bitvector.why"
loclnum="58" loccnumb="8" loccnume="26"
sum="758fc5323fad79f44ff6a855f0273c49"
sum="25c45e1dabcd1de49dc5c7dcdce1df9b"
proved="true"
expanded="false"
shape="ainfix =anthabw_xorV0V1V2anthV0V2Iainfix =anthV1V2aFalseAainfix <V2asizeAainfix <=c0V2F">
......@@ -171,7 +171,7 @@
name="to_nat_of_zero2"
locfile="../bitvector.why"
loclnum="194" loccnumb="8" loccnume="23"
sum="8e5c2231702a4338720753b05a2d6b25"
sum="3e57107fd0e18413aed748d70d861ade"
proved="true"
expanded="false"
shape="ainfix =ato_nat_subV0V2c0ato_nat_subV0V1c0Iainfix =anthV0V3aFalseIainfix >V3V1Aainfix >=V2V3FIainfix >=V1c0Aainfix >=V2V1Aainfix >asizeV2F">
......@@ -189,7 +189,7 @@
name="to_nat_of_zero"
locfile="../bitvector.why"
loclnum="200" loccnumb="8" loccnume="22"
sum="429786d935e16d5c4f9d63f38a5b8683"
sum="a28ad2c6a2325fc418f7071f7e61013b"
proved="true"
expanded="false"
shape="ainfix =ato_nat_subV0V2V1c0Iainfix =anthV0V3aFalseIainfix >=V3V1Aainfix >=V2V3FIainfix >=V1c0Aainfix >asizeV2F">
......@@ -207,7 +207,7 @@
name="to_nat_of_one"
locfile="../bitvector.why"
loclnum="205" loccnumb="8" loccnume="21"
sum="1d30421e44d3de741b5b91650ed96f7b"
sum="42cb8da0d0b16ccf5e67a0b0b0e8f3d5"
proved="true"
expanded="false"
shape="ainfix =ato_nat_subV0V2V1ainfix -apow2ainfix +ainfix -V2V1c1c1Iainfix =anthV0V3aTrueIainfix >=V3V1Aainfix >=V2V3FIainfix >=V1c0Aainfix >=V2V1Aainfix >asizeV2F">
......@@ -225,7 +225,7 @@
name="to_nat_sub_footprint"
locfile="../bitvector.why"
loclnum="210" loccnumb="8" loccnume="28"
sum="192aeb48642121964d858da790471115"
sum="7ad2beb531a5fdb347eb7c7f3b82ed89"
proved="true"
expanded="false"
shape="ainfix =ato_nat_subV0V2V3ato_nat_subV1V2V3Iainfix =anthV0V4anthV1V4Iainfix <=V4V2Aainfix <=V3V4FIainfix >=V3c0Aainfix >asizeV2F">
......@@ -243,7 +243,7 @@
name="nth_from_int_low_even"
locfile="../bitvector.why"
loclnum="297" loccnumb="8" loccnume="29"
sum="d85ea6576de917d8becffc1cbca1c054"
sum="e2c5931b5ef2c5436155d4dc517e9426"
proved="true"
expanded="false"
shape="ainfix =anthafrom_intV0c0aFalseIainfix =amodV0c2c0F">
......@@ -276,7 +276,7 @@
name="nth_from_int_low_odd"
locfile="../bitvector.why"
loclnum="300" loccnumb="8" loccnume="28"
sum="1bbd5b442bf57f164e68cd02baff256d"
sum="16b9a9d1f22b3b325635d1e74ad0d3fc"
proved="true"
expanded="false"
shape="ainfix =anthafrom_intV0c0aTrueINainfix =amodV0c2c0F">
......@@ -309,7 +309,7 @@
name="nth_from_int_0"
locfile="../bitvector.why"
loclnum="303" loccnumb="8" loccnume="22"
sum="3ac9bb79fac296fc9104d74fefadc770"
sum="886b69b3b5b4cfec83f1a9d69c229a3e"
proved="true"
expanded="false"
shape="ainfix =anthafrom_intc0V0aFalseIainfix >=V0c0Aainfix >asizeV0F">
......@@ -342,7 +342,7 @@
name="nth_from_int2c_low_even"
locfile="../bitvector.why"
loclnum="339" loccnumb="8" loccnume="31"
sum="298dff62a3bf62b13fa1a02cf622f350"
sum="92582de2a334b6986abbee63cd309308"
proved="true"
expanded="false"
shape="ainfix =anthafrom_int2cV0c0aFalseIainfix =amodV0c2c0F">
......@@ -375,7 +375,7 @@
name="nth_from_int2c_low_odd"
locfile="../bitvector.why"
loclnum="342" loccnumb="8" loccnume="30"
sum="c3a466a2dab42d03c150558fd4ca2915"
sum="c4eed6bf1c9638d4568abf5114040241"
proved="true"
expanded="false"
shape="ainfix =anthafrom_int2cV0c0aTrueINainfix =amodV0c2c0F">
......@@ -408,7 +408,7 @@
name="nth_from_int2c_0"
locfile="../bitvector.why"
loclnum="345" loccnumb="8" loccnume="24"
sum="c19b62647868f221fcc52e10efff519f"
sum="7ed43b95c5759a3e3a0ced2e9302f855"
proved="true"
expanded="false"
shape="ainfix =anthafrom_int2cc0V0aFalseIainfix >=V0c0Aainfix >asizeV0F">
......@@ -441,7 +441,7 @@
name="nth_from_int2c_plus_pow2"
locfile="../bitvector.why"
loclnum="348" loccnumb="8" loccnume="32"
sum="b55d9bee3b363cfa8f60229e84c1c1b8"
sum="b1683fcaf605e25f95106fe3925f5435"
proved="true"
expanded="false"
shape="ainfix =anthafrom_int2cainfix +V0apow2V2V1anthafrom_int2cV0V1Iainfix <V1ainfix -asizec1Aainfix <V1V2Aainfix <=c0V1F">
......@@ -451,7 +451,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.72"/>
<result status="valid" time="0.94"/>
</proof>
<proof
prover="4"
......@@ -495,7 +495,7 @@
name="Test1"
locfile="../bitvector.why"
loclnum="395" loccnumb="7" loccnume="12"
sum="31c20dde9067a30e7163b4a313e63ca9"
sum="6b3e69f67ad7d249a886392c8fb41dab"
proved="true"
expanded="false"
shape="ainfix =anthV0c1aFalseLabw_andabvzeroabvone">
......@@ -552,7 +552,7 @@
name="Test2"
locfile="../bitvector.why"
loclnum="398" loccnumb="7" loccnume="12"
sum="c4f1eb26b9759a7d65ab307ee58051f7"
sum="141d8b005b268120c935e701979a9c4f"
proved="true"
expanded="false"
shape="ainfix =anthV0c15aTrueLalsrabvonec16">
......@@ -609,7 +609,7 @@
name="Test3"
locfile="../bitvector.why"
loclnum="401" loccnumb="7" loccnume="12"
sum="0e324bad8203c203456a76edfae2c6c9"
sum="e6abdd4d1f111b631a41d3c0b6c6e869"
proved="true"
expanded="false"
shape="ainfix =anthV0c16aFalseLalsrabvonec16">
......@@ -674,7 +674,7 @@
name="Test4"
locfile="../bitvector.why"
loclnum="404" loccnumb="7" loccnume="12"
sum="03662c8f5add1179ce0789856ecc4199"
sum="356cf4e8a8d7774f977d99ccc2be4a7e"
proved="true"
expanded="false"
shape="ainfix =anthV0c15aTrueLaasrabvonec16">
......@@ -731,7 +731,7 @@
name="Test5"
locfile="../bitvector.why"
loclnum="407" loccnumb="7" loccnume="12"
sum="89b4cebf9cce0c1696f7ea4c05d7f2ee"
sum="e7328909b22ec74914bd3ea3ac93b73f"
proved="true"
expanded="false"
shape="ainfix =anthV0c16aTrueLaasrabvonec16">
......@@ -788,7 +788,7 @@
name="Test6"
locfile="../bitvector.why"
loclnum="410" loccnumb="7" loccnume="12"
sum="c250e5e7d1fdecbbaaab512633c1aae2"
sum="e4b62ed0658714de218c5bd58955cb9e"
proved="true"
expanded="false"
shape="ainfix =anthV0c16aFalseLaasralsrabvonec1c16">
......@@ -853,7 +853,7 @@
name="to_nat_0x00000000"
locfile="../bitvector.why"
loclnum="413" loccnumb="7" loccnume="24"
sum="ae05e7dfe8dd21fec426519d083ab119"
sum="c2fffbd8f53a35f3b05c7ff9f44aede1"
proved="true"
expanded="false"
shape="ainfix =ato_natabvzeroc0">
......@@ -910,7 +910,7 @@
name="to_nat_0x00000001"
locfile="../bitvector.why"
loclnum="416" loccnumb="7" loccnume="24"
sum="54a6c5cb388d586d728ca95af25d41dd"
sum="90c421949e4c6dc367793c262a158a65"
proved="true"
expanded="false"
shape="ainfix =ato_natalsrabvonec31c1">
......@@ -920,14 +920,14 @@
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="25.54"/>
<result status="valid" time="32.64"/>
</proof>
</goal>
<goal
name="to_nat_0x00000003"
locfile="../bitvector.why"
loclnum="419" loccnumb="7" loccnume="24"
sum="db564c45f521212a48df3135e901f69b"
sum="3e22ed8ce51b7cf915ea406219ebc83f"
proved="true"
expanded="false"
shape="ainfix =ato_natalsrabvonec30c3">
......@@ -937,14 +937,14 @@
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="40.88"/>
<result status="valid" time="55.76"/>
</proof>
</goal>
<goal
name="to_nat_0x00000007"
locfile="../bitvector.why"
loclnum="422" loccnumb="7" loccnume="24"
sum="48cf8cfc863af83f71ff99643cf5d384"
sum="9e8cb3bbea6471664cef7aff8c602fa4"
proved="true"
expanded="false"
shape="ainfix =ato_natalsrabvonec29c7">
......@@ -954,14 +954,14 @@
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="33.53"/>
<result status="valid" time="46.64"/>
</proof>
</goal>
<goal
name="to_nat_0x0000000F"
locfile="../bitvector.why"
loclnum="425" loccnumb="7" loccnume="24"
sum="aa9d24eb080cc56d20d2fba18cf9ece8"
sum="d305534113cfd05a417b0125600c36ce"
proved="true"
expanded="false"
shape="ainfix =ato_natalsrabvonec28c15">
......@@ -971,14 +971,14 @@
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="28.80"/>
<result status="valid" time="36.83"/>
</proof>
</goal>
<goal
name="to_nat_0x0000001F"
locfile="../bitvector.why"
loclnum="428" loccnumb="7" loccnume="24"
sum="b31fde78f7aa5f4b6d14394224353c79"
sum="9842820bfef46a344e5cb8930c270445"
proved="true"
expanded="false"
shape="ainfix =ato_natalsrabvonec27c31">
......@@ -988,14 +988,14 @@
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="27.66"/>
<result status="valid" time="35.49"/>
</proof>
</goal>
<goal
name="to_nat_0x0000003F"
locfile="../bitvector.why"
loclnum="431" loccnumb="7" loccnume="24"
sum="20a5923d0b0e74b6235d0324e72f4aa4"
sum="f3be708ebb98cd741647d2bb835f90e9"
proved="true"
expanded="false"
shape="ainfix =ato_natalsrabvonec26c63">
......@@ -1005,14 +1005,14 @@
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="23.82"/>
<result status="valid" time="30.37"/>
</proof>
</goal>
<goal
name="to_nat_0x0000007F"
locfile="../bitvector.why"
loclnum="434" loccnumb="7" loccnume="24"
sum="a273d532ac01c3b2c85a726ea381f2d6"
sum="2101651d6afe53d5cbaf2765807c5a3f"
proved="true"
expanded="false"
shape="ainfix =ato_natalsrabvonec25c127">
......@@ -1022,14 +1022,14 @@
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="18.56"/>
<result status="valid" time="23.75"/>
</proof>
</goal>
<goal
name="to_nat_0x000000FF"
locfile="../bitvector.why"
loclnum="437" loccnumb="7" loccnume="24"
sum="10d959adc59b512380dbfcf9c670b6b9"
sum="05ca290eb4bcfc88d120afc9ef35e210"
proved="true"
expanded="false"
shape="ainfix =ato_natalsrabvonec24c255">
......@@ -1039,14 +1039,14 @@
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="16.20"/>
<result status="valid" time="20.69"/>
</proof>
</goal>
<goal
name="to_nat_0x000001FF"
locfile="../bitvector.why"
loclnum="440" loccnumb="7" loccnume="24"
sum="505ed57bc65c33ada3d4f795eeb4b846"
sum="0647f5706b34eb6b981dce60044ad599"
proved="true"
expanded="false"
shape="ainfix =ato_natalsrabvonec23c511">
......@@ -1056,14 +1056,14 @@
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="13.53"/>
<result status="valid" time="16.78"/>
</proof>
</goal>
<goal
name="to_nat_0x000003FF"
locfile="../bitvector.why"
loclnum="443" loccnumb="7" loccnume="24"
sum="99f1e514132cea34a20505d0907fb61e"
sum="61e314c16d63d4a3a5b1a211fb456b20"
proved="true"
expanded="false"
shape="ainfix =ato_natalsrabvonec22c1023">
......@@ -1073,14 +1073,14 @@
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="9.56"/>
<result status="valid" time="11.23"/>
</proof>
</goal>
<goal
name="to_nat_0x000007FF"
locfile="../bitvector.why"
loclnum="446" loccnumb="7" loccnume="24"
sum="3b0c1f0a7a6a23c59a22a8bc18652e49"
sum="49ded8ff89ac091559677c7754476796"
proved="true"
expanded="false"
shape="ainfix =ato_natalsrabvonec21c2047">
......@@ -1090,14 +1090,14 @@
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="8.08"/>
<result status="valid" time="9.75"/>
</proof>
</goal>
<goal
name="to_nat_0x00000FFF"
locfile="../bitvector.why"
loclnum="449" loccnumb="7" loccnume="24"
sum="5708d69e99b0f8c0ae5d3d74e2b03d16"
sum="80fa31e1281dcc63f557c2f1fc95c452"
proved="true"
expanded="false"
shape="ainfix =ato_natalsrabvonec20c4095">
......@@ -1107,14 +1107,14 @@
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="7.18"/>
<result status="valid" time="9.01"/>
</proof>
</goal>
<goal
name="to_nat_0x00001FFF"
locfile="../bitvector.why"
loclnum="452" loccnumb="7" loccnume="24"
sum="b553111189fc57579aad5957400ba893"
sum="96a19e6e3ba5b9f2b915615c7e88b49e"
proved="true"
expanded="false"
shape="ainfix =ato_natalsrabvonec19c8191">
......@@ -1124,14 +1124,14 @@
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="5.80"/>
<result status="valid" time="6.99"/>
</proof>
</goal>
<goal
name="to_nat_0x00003FFF"
locfile="../bitvector.why"
loclnum="455" loccnumb="7" loccnume="24"
sum="d3a213e5d10a94f1672c2f81616ef199"
sum="c6dfca8bc247253c90cf0fd544e405c5"
proved="true"
expanded="false"
shape="ainfix =ato_natalsrabvonec18c16383">
......@@ -1141,14 +1141,14 @@
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="4.26"/>
<result status="valid" time="5.71"/>
</proof>
</goal>
<goal
name="to_nat_0x00007FFF"
locfile="../bitvector.why"
loclnum="458" loccnumb="7" loccnume="24"
sum="89780e352ce90762edd80b151dd0fa63"
sum="0c84ed9e9130f49d784474a9d319a2a2"
proved="true"
expanded="false"
shape="ainfix =ato_natalsrabvonec17c32767">
......@@ -1165,7 +1165,7 @@
name="to_nat_0x0000FFFF"
locfile="../bitvector.why"
loclnum="461" loccnumb="7" loccnume="24"
sum="7cf453c2e02082e54109f72a5e101fef"
sum="f3ecf33c4159b8025d690e7d047497c1"
proved="true"
expanded="false"
shape="ainfix =ato_natalsrabvonec16c65535">
......@@ -1175,14 +1175,14 @@
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="2.70"/>
<result status="valid" time="3.38"/>
</proof>
</goal>
<goal
name="to_nat_0x0001FFFF"
locfile="../bitvector.why"
loclnum="469" loccnumb="7" loccnume="24"
sum="81a4492651176e01d54e30bb34905b03"
sum="143d3fa56f0fafac56250bfb8934071a"
proved="true"
expanded="false"
shape="ainfix =ato_natalsrabvonec15c131071">
......@@ -1192,14 +1192,14 @@
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="2.10"/>
<result status="valid" time="2.55"/>
</proof>
</goal>
<goal
name="to_nat_0x0003FFFF"
locfile="../bitvector.why"
loclnum="472" loccnumb="7" loccnume="24"
sum="24edb5c87fb553582f0a0fa7d1d0ba98"
sum="97a22ac3d426508527e064c451b808ad"
proved="true"
expanded="false"
shape="ainfix =ato_natalsrabvonec14c262143">
......@@ -1216,7 +1216,7 @@
name="to_nat_0x0007FFFF"
locfile="../bitvector.why"
loclnum="475" loccnumb="7" loccnume="24"
sum="843cbb41fe2fcc3af6648d1f99201031"
sum="048d1dd9d3b9b6abb4a10907ced048e6"
proved="true"
expanded="false"
shape="ainfix =ato_natalsrabvonec13c524287">
......@@ -1233,7 +1233,7 @@
name="to_nat_0x000FFFFF"
locfile="../bitvector.why"
loclnum="478" loccnumb="7" loccnume="24"
sum="5622cc9887e70441643b97c0c3c29c3d"
sum="2a460dfd46aefadb8bf6be193eb7f2b5"
proved="true"
expanded="false"
shape="ainfix =ato_natalsrabvonec12c1048575">
......@@ -1250,7 +1250,7 @@
name="to_nat_0x00FFFFFF"
locfile="../bitvector.why"
loclnum="481" loccnumb="7" loccnume="24"
sum="f5844696ec84cfe5ad19392c41e4c6dd"
sum="b7ad85ebd477b8f47bc85fdb357d3c6a"
proved="true"
expanded="false"
shape="ainfix =ato_natalsrabvonec8c16777215">
......@@ -1267,7 +1267,7 @@
name="to_nat_0xFFFFFFFF"
locfile="../bitvector.why"
loclnum="484" loccnumb="7" loccnume="24"
sum="36a95261f8d86154ebc74ac1d5036f4c"
sum="dcfcd1f6409fa9ef616335df91645277"
proved="true"
expanded="false"
shape="ainfix =ato_natabvonec4294967295">
......
......@@ -39,7 +39,7 @@
name="Nth_j"
locfile="../neg_as_xor.why"
loclnum="13" loccnumb="8" loccnume="13"
sum="706d233bc684b53d77c1fdf517fed1a4"
sum="cd6486774b11432a83654d5c299cb6ed"
proved="true"
expanded="true"
shape="ainfix =anthajV0aFalseIainfix &lt;=V0c62Aainfix &lt;=c0V0F">
......@@ -56,7 +56,7 @@
name="sign_of_j"
locfile="../neg_as_xor.why"
loclnum="15" loccnumb="8" loccnume="17"
sum="497dc675e45b2db4dad3ac9ac57894ba"
sum="1798f3899f8501c14a2d58e8c99032c2"
proved="true"
expanded="true"
shape="ainfix =asignajaTrue">
......@@ -73,7 +73,7 @@
name="mantissa_of_j"
locfile="../neg_as_xor.why"
loclnum="16" loccnumb="8" loccnume="21"
sum="ba45c67869c2b86e0a2ce419b0bcfa19"
sum="33462fd908bddef0b4d612775fb853fc"
proved="true"
expanded="true"
shape="ainfix =amantissaajc0">
......@@ -107,7 +107,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="3.05"/>
<result status="valid" time="3.52"/>
</proof>
<proof
prover="5"
......@@ -122,7 +122,7 @@
name="exp_of_j"
locfile="../neg_as_xor.why"
loclnum="17" loccnumb="8" loccnume="16"
sum="ca84bfe984f0638331493bb8e52727da"
sum="b3b650d10052127e4ae19c877205f723"
proved="true"
expanded="true"
shape="ainfix =aexpajc0">
......@@ -171,7 +171,7 @@
name="int_of_bv"
locfile="../neg_as_xor.why"
loclnum="18" loccnumb="8" loccnume="17"
sum="3e0d947e2994b4f99cd11906a7700aba"
sum="841e9bd4f7ecc06a59b47e1534ee038a"
proved="true"
expanded="true"
shape="ainfix =adouble_of_bv64ajc0.0">
......@@ -220,7 +220,7 @@
name="MainResultBits"
locfile="../neg_as_xor.why"
loclnum="20" loccnumb="8" loccnume="22"
sum="1a697819ec0cbae299653ca632f5f1f4"
sum="cc4a315b7659f16fbe94460e7753f525"
proved="true"
expanded="true"
shape="ainfix =anthabw_xorV0ajV1anthV0V1Iainfix &lt;V1c63Aainfix &lt;=c0V1FF">
......@@ -245,7 +245,7 @@
name="MainResultSign"
locfile="../neg_as_xor.why"
loclnum="23" loccnumb="8" loccnume="22"
sum="18ddc34735ee8af58fd72b703041d953"
sum="7989d4b134024a98669bec0231eae690"
proved="true"
expanded="true"
shape="ainfix =anthabw_xorV0ajc63anotbanthV0c63F">
......@@ -270,7 +270,7 @@
name="Sign_of_xor_j"
locfile="../neg_as_xor.why"
loclnum="25" loccnumb="8" loccnume="21"
sum="67da7e6f5b583e2adde22650d74059ef"
sum="54961afdd0d7931f55becd944287b323"
proved="true"
expanded="true"
shape="ainfix =asignabw_xorV0ajanotbasignV0F">
......@@ -319,7 +319,7 @@
name="Exp_of_xor_j"
locfile="../neg_as_xor.why"
loclnum="27" loccnumb="8" loccnume="20"
sum="2b0fb2b39ee0b71651449f67ff8412b8"
sum="2c98b346434cb2c1a566009c10d75dd6"
proved="true"
expanded="true"
shape="ainfix =aexpabw_xorV0ajaexpV0F">
......@@ -345,7 +345,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="3.18"/>
<result status="valid" time="3.70"/>
</proof>
<proof
prover="5"
......@@ -360,7 +360,7 @@
name="Mantissa_of_xor_j"
locfile="../neg_as_xor.why"
loclnum="29" loccnumb="8" loccnume="25"
sum="e4819744b3225fae14c6be40ea5ddabd"
sum="1d1cb0537ff7fa9d83c414b9b6a6e0d2"
proved="true"
expanded="true"
shape="ainfix =amantissaabw_xorV0ajamantissaV0F">
......@@ -401,7 +401,7 @@
name="MainResultZero"
locfile="../neg_as_xor.why"
loclnum="31" loccnumb="8" loccnume="22"
sum="350d1e94fdacee12e4a02f4851da9e75"
sum="862dbdfa50a9055a229f41ac799661e3"
proved="true"
expanded="true"
shape="ainfix =adouble_of_bv64abw_xorV0ajaprefix -.adouble_of_bv64V0Iainfix =amantissaV0c0Aainfix =c0aexpV0F">
......@@ -435,7 +435,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="3.33"/>
<result status="valid" time="3.86"/>
</proof>
<proof
prover="5"
......@@ -450,7 +450,7 @@
name="sign_neg"
locfile="../neg_as_xor.why"
loclnum="34" loccnumb="8" loccnume="16"
sum="d86dc14cd3ca2f95f975108838091849"