Skip to content

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

update proof sessions

parent 0497d13d
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 3851 additions and 3851 deletions
examples/bitvectors/double/why3session.xml
View file @ a8a44982
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/usr/local/share/why3/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="1de7d115c0c2e47b0f7c904ae25676bb"
sum="06f37921b8d6e1de5911cfa60ee3f495"
proved="true"
expanded="false"
shape="ainfix =anthaoneV0aFalseIainfix &lt;=V0c51Aainfix &lt;=c0V0F">
......@@ -57,14 +57,14 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.25"/>
<result status="valid" time="0.26"/>
</proof>
</goal>
<goal
name="nth_one2"
locfile="bitvectors/double/../double.why"
loclnum="74" loccnumb="8" loccnume="16"
sum="4239a716540729c82b5bc2cb996d81d4"
sum="07d361ed2fa63880733bc14101b15f6e"
proved="true"
expanded="false"
shape="ainfix =anthaoneV0aTrueIainfix &lt;=V0c61Aainfix &lt;=c52V0F">
......@@ -81,7 +81,7 @@
name="nth_one3"
locfile="bitvectors/double/../double.why"
loclnum="75" loccnumb="8" loccnume="16"
sum="928a77dfb46ea44de4515a93357273e6"
sum="b76bf4048e9811e187d0ef7e4dacce4e"
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="788a6aa6d6f8e7ef9798104faf310e0b"
sum="9e7ae345c718068eb332ff5be1cc0617"
proved="true"
expanded="false"
shape="ainfix =asignaoneaFalse">
......@@ -108,7 +108,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.11"/>
<result status="valid" time="0.12"/>
</proof>
<proof
prover="1"
......@@ -132,7 +132,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="5"
......@@ -147,7 +147,7 @@
name="exp_one"
locfile="bitvectors/double/../double.why"
loclnum="78" loccnumb="8" loccnume="15"
sum="39c4e12e174fe68af3511bdb137ff4c0"
sum="817bbb0bf9d16ebf84d1209148a2d86b"
proved="true"
expanded="false"
shape="ainfix =aexpaonec1023">
......@@ -157,7 +157,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="2.12"/>
<result status="valid" time="2.08"/>
</proof>
<proof
prover="3"
......@@ -166,14 +166,14 @@
edited="double_TestDouble_exp_one_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.60"/>
<result status="valid" time="0.58"/>
</proof>
</goal>
<goal
name="mantissa_one"
locfile="bitvectors/double/../double.why"
loclnum="79" loccnumb="8" loccnume="20"
sum="4a54620e16f0d6a5918a273d53fcdbeb"
sum="4e7bcdfa56cb11635fc70f768867ab60"
proved="true"
expanded="false"
shape="ainfix =amantissaaonec0">
......@@ -183,7 +183,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.71"/>
<result status="valid" time="0.70"/>
</proof>
<proof
prover="0"
......@@ -191,7 +191,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.08"/>
<result status="valid" time="0.10"/>
</proof>
<proof
prover="5"
......@@ -199,14 +199,14 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="2.91"/>
<result status="valid" time="2.86"/>
</proof>
</goal>
<goal
name="double_value_of_1"
locfile="bitvectors/double/../double.why"
loclnum="81" loccnumb="8" loccnume="25"
sum="eca3f0dc4bf6860b6c1b6bb8e52e8b86"
sum="362e56694a4e63a3214575ce1d7ffbc7"
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.04"/>
<result status="valid" time="0.03"/>
</proof>
<proof
prover="2"
......
examples/bitvectors/neg_as_xor/why3session.xml
View file @ a8a44982
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/usr/local/share/why3/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="d3063104903bdd668679f74cb5f68a13"
sum="f0956e2cb757960a17f81a3067b715a6"
proved="true"
expanded="false"
shape="ainfix =anthajV0aFalseIainfix &lt;=V0c62Aainfix &lt;=c0V0F">
......@@ -49,7 +49,7 @@
name="sign_of_j"
locfile="bitvectors/neg_as_xor/../neg_as_xor.why"
loclnum="15" loccnumb="8" loccnume="17"
sum="b08967f54f1e1489f089ec817a18e2f7"
sum="682b25f524efe50b9b47b2d9cd3c5ebc"
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="55572bb59d8addee4c9cfe6fd7ee4ef9"
sum="13cc5b0010039968be9ba46aa4ccd86c"
proved="true"
expanded="false"
shape="ainfix =amantissaajc0">
......@@ -92,14 +92,14 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="3.02"/>
<result status="valid" time="3.05"/>
</proof>
</goal>
<goal
name="exp_of_j"
locfile="bitvectors/neg_as_xor/../neg_as_xor.why"
loclnum="17" loccnumb="8" loccnume="16"
sum="f8f50f4305a26cc7f52c1387cafe90aa"
sum="e05572302f7143feff19510e43ab8d5e"
proved="true"
expanded="false"
shape="ainfix =aexpajc0">
......@@ -117,7 +117,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.06"/>
<result status="valid" time="0.07"/>
</proof>
<proof
prover="3"
......@@ -125,14 +125,14 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="3.35"/>
<result status="valid" time="3.37"/>
</proof>
</goal>
<goal
name="int_of_bv"
locfile="bitvectors/neg_as_xor/../neg_as_xor.why"
loclnum="18" loccnumb="8" loccnume="17"
sum="159f78875f137f073a9314efffe2ca7a"
sum="61e2aff1d7bd95ae2a08d5fa89369fae"
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.11"/>
<result status="valid" time="0.12"/>
</proof>
<proof
prover="0"
......@@ -165,7 +165,7 @@
name="MainResultBits"
locfile="bitvectors/neg_as_xor/../neg_as_xor.why"
loclnum="20" loccnumb="8" loccnume="22"
sum="c6fe8a6f64727e31d01f461b664b4a81"
sum="19ca0ae277e12bb1ec831954401ceac3"
proved="true"
expanded="false"
shape="ainfix =anthabw_xorV0ajV1anthV0V1Iainfix &lt;V1c63Aainfix &lt;=c0V1FF">
......@@ -175,14 +175,14 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.04"/>
</proof>
</goal>
<goal
name="MainResultSign"
locfile="bitvectors/neg_as_xor/../neg_as_xor.why"
loclnum="23" loccnumb="8" loccnume="22"
sum="e0b3867568f72ea27b09baae32e7f679"
sum="ef1b5e1c8fd4d961aa2ec3e400594311"
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="9174061a363d9c2b808fff999dd1c00d"
sum="09c25162719fe2d5f04b4a958353d6c7"
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="f86ab36765de5476dc2c4e7364803681"
sum="32330f454a4e9cdd0863a6fead5e0491"
proved="true"
expanded="false"
shape="ainfix =aexpabw_xorV0ajaexpV0F">
......@@ -242,7 +242,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.71"/>
<result status="valid" time="0.70"/>
</proof>
<proof
prover="0"
......@@ -258,14 +258,14 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="3.53"/>
<result status="valid" time="3.06"/>
</proof>
</goal>
<goal
name="Mantissa_of_xor_j"
locfile="bitvectors/neg_as_xor/../neg_as_xor.why"
loclnum="29" loccnumb="8" loccnume="25"
sum="6adbf301ff82007071dbc52506e1365f"
sum="ff7efb49476971e2ae56be09001b5037"
proved="true"
expanded="false"
shape="ainfix =amantissaabw_xorV0ajamantissaV0F">
......@@ -275,7 +275,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.70"/>
<result status="valid" time="0.71"/>
</proof>
<proof
prover="0"
......@@ -283,7 +283,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.58"/>
<result status="valid" time="0.57"/>
</proof>
<proof
prover="3"
......@@ -291,14 +291,14 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="3.36"/>
<result status="valid" time="2.90"/>
</proof>
</goal>
<goal
name="MainResultZero"
locfile="bitvectors/neg_as_xor/../neg_as_xor.why"
loclnum="31" loccnumb="8" loccnume="22"
sum="621950aa9bf7f4a583419ff60844561c"
sum="856675b97e95759d373dbfd29851a233"
proved="true"
expanded="false"
shape="ainfix =adouble_of_bv64abw_xorV0ajaprefix -.adouble_of_bv64V0Iainfix =amantissaV0c0Aainfix =c0aexpV0F">
......@@ -316,7 +316,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="1.72"/>
<result status="valid" time="1.73"/>
</proof>
<proof
prover="3"
......@@ -324,14 +324,14 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="3.17"/>
<result status="valid" time="3.32"/>
</proof>
</goal>
<goal
name="sign_neg"
locfile="bitvectors/neg_as_xor/../neg_as_xor.why"
loclnum="34" loccnumb="8" loccnume="16"
sum="b229184f963e55e6442db8ef235d1c89"
sum="512a9c88e57a3fdb1b019741fa36287d"
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.79"/>
<result status="valid" time="2.78"/>
</proof>
</goal>
<goal
name="MainResult"
locfile="bitvectors/neg_as_xor/../neg_as_xor.why"
loclnum="36" loccnumb="8" loccnume="18"
sum="7d1ac00d3cad260c4aba86035625d542"
sum="4849d551d35fd59faec06345b4bdfeb8"
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.95"/>
<result status="valid" time="0.94"/>
</proof>
</goal>
</theory>
......
examples/bts/12475/why3session.xml
View file @ a8a44982
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/usr/local/share/why3/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="07763c823feaf262c263cca6378f25f1"
sum="b2db1ecda9fbba750ff04a700c301dfe"
proved="true"
expanded="true"
shape="ainfix &lt;V0ainfix +aroundaUpV0c1.F">
......@@ -60,7 +60,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="2"
......
examples/bts/13853/why3session.xml
View file @ a8a44982
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/usr/local/share/why3/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="b94bdf7e8e0d350ccc769aa2abfed2a5"
sum="abda3939af653d7d9704361e09e71ef8"
proved="true"
expanded="false"
shape="t">
......@@ -41,7 +41,7 @@
locfile="bts/13853/../13853.mlw"
loclnum="18" loccnumb="7" loccnume="8"
expl="exceptional postcondition"
sum="290f50192a8d9eb5fed96206ef53b3b4"
sum="a99bac9a5a8c3cd01f574ec5280fe162"
proved="true"
expanded="false"
shape="t">
......
examples/check-builtin/bool/why3session.xml
View file @ a8a44982
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/usr/local/share/why3/why3session.dtd">
<why3session
name="check-builtin/bool/why3session.xml" shape_version="2">
<prover
......@@ -32,7 +32,7 @@
name="G1"
locfile="check-builtin/bool/../bool.why"
loclnum="4" loccnumb="11" loccnume="13"
sum="ca83f9c0bba83999ea519362a0f979d3"
sum="af4d670afdfdd1e631e80d30d19ede7b"
proved="true"
expanded="true"
shape="ainfix =aTrueaFalseN">
......@@ -50,7 +50,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="1"
......@@ -73,7 +73,7 @@
name="G2"
locfile="check-builtin/bool/../bool.why"
loclnum="5" loccnumb="11" loccnume="13"
sum="5f38ad601b7696e2fe3ba2f557f615e0"
sum="7a72a9f2346a915442af5b3c5630e0f3"
proved="true"
expanded="true"
shape="ainfix =V0aFalseOainfix =V0aTrueF">
......@@ -114,7 +114,7 @@
name="G3"
locfile="check-builtin/bool/../bool.why"
loclnum="6" loccnumb="11" loccnume="13"
sum="0787a194d06b1338870206245188cc68"
sum="a79670357144984023e697f917d5885f"
proved="true"
expanded="true"
shape="fIainfix =V2V0NAainfix =V1V2NAainfix =V0V1NF">
......@@ -132,7 +132,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="1"
......
examples/check-builtin/floats/why3session.xml
View file @ a8a44982
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/usr/local/share/why3/why3session.dtd">
<why3session
name="check-builtin/floats/why3session.xml" shape_version="2">
<prover
......@@ -32,7 +32,7 @@
name="Round_single_01"
locfile="check-builtin/floats/../floats.why"
loclnum="11" loccnumb="7" loccnume="22"
sum="397906d94bbb0b5341288dfce84f89dc"
sum="bfd5a60d467e1aaa8054ae8842947c8c"
proved="true"
expanded="true"
shape="ainfix =aroundaNearestTiesToEvenc0.1c0x1.99999ap-4">
......@@ -49,7 +49,7 @@
name="Round_double_01"
locfile="check-builtin/floats/../floats.why"
loclnum="14" loccnumb="7" loccnume="22"
sum="35b08355e175d22b4d9ab4c1c827526f"
sum="6186c79d4d7c8f61aace83164e841e28"
proved="true"
expanded="true"
shape="ainfix =aroundaNearestTiesToEvenc0.1c0x1.999999999999ap-4">
......@@ -66,7 +66,7 @@
name="Test00"
locfile="check-builtin/floats/../floats.why"
loclnum="17" loccnumb="8" loccnume="14"
sum="e45b8dc86a2bf34e6b3beb8b8a8a720e"
sum="805ff5506a81fd6cd32faf5d79e52e9d"
proved="true"
expanded="true"
shape="ainfix &lt;=aprefix -c3.0V0Iainfix &lt;=aabsV0c2.0F">
......@@ -107,7 +107,7 @@
name="Test01"
locfile="check-builtin/floats/../floats.why"
loclnum="19" loccnumb="8" loccnume="14"
sum="ebff461c0eb487a4284b1d316905f8a2"
sum="9c775c9baae104ab97f7c6a0c6220f45"
proved="true"
expanded="true"
shape="ainfix &lt;=aabsainfix -ainfix *avalueV0avalueV0aroundaNearestTiesToEvenainfix *avalueV0avalueV0c0x1.p-52Iainfix &lt;=avalueV0c2.0Aainfix &lt;=aprefix -c2.0avalueV0F">
......@@ -124,7 +124,7 @@
name="Test02"
locfile="check-builtin/floats/../floats.why"
loclnum="25" loccnumb="8" loccnume="14"
sum="10d968c72c3f3e64f89fa7904576ed89"
sum="02a5543d6b9c1095fceac08e502df51d"
proved="true"
expanded="true"
shape="ainfix &lt;=aabsainfix -ainfix *avalueV1avalueV1aroundaNearestTiesToEvenainfix *avalueV0avalueV0c0x1.p-52Iainfix =V1V0Iainfix &lt;=aabsavalueV0c2.0F">
......@@ -141,7 +141,7 @@
name="Test03"
locfile="check-builtin/floats/../floats.why"
loclnum="32" loccnumb="8" loccnume="14"
sum="07cb638f137dc0341ef32cb3e91c11fc"
sum="0e72d2ab0c53e3663a3af01f31880922"
proved="true"
expanded="true"
shape="ainfix &lt;=asqrtainfix *ainfix -avalueV2ainfix *avalueV0avalueV0ainfix -avalueV1ainfix *avalueV0avalueV0c0x1.p-52Iainfix =V2V1Iainfix =avalueV1aroundaNearestTiesToEvenainfix *avalueV0avalueV0Iainfix &lt;=aabsavalueV0c2.0F">
......
examples/foveoos2011/array_max/why3session.xml
View file @ a8a44982
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/usr/local/share/why3/why3session.dtd">
<why3session
name="foveoos2011/array_max/why3session.xml" shape_version="2">
<prover
......@@ -29,7 +29,7 @@
locfile="foveoos2011/array_max/../array_max.mlw"
loclnum="21" loccnumb="6" loccnume="9"
expl="parameter max"
sum="d352c899d3258c870d470a9bbd204e5a"
sum="9dab516c509ac11688e82e472c1c925d"
proved="true"
expanded="true"
shape="iainfix =V3V2Niainfix &lt;=agetV1V3agetV1V2ainfix &lt;ainfix -V2V4ainfix -V2V3Aainfix &lt;=c0ainfix -V2V3Aainfix &lt;=agetV1V5amaxagetV1V4agetV1V2Iainfix &lt;V5V0Aainfix &lt;V2V5Oainfix &lt;V5V4Aainfix &lt;=c0V5FAainfix &lt;V2V0Aainfix &lt;=V4V2Aainfix &lt;=c0V4Iainfix =V4ainfix +V3c1Fainfix &lt;ainfix -V6V3ainfix -V2V3Aainfix &lt;=c0ainfix -V2V3Aainfix &lt;=agetV1V7amaxagetV1V3agetV1V6Iainfix &lt;V7V0Aainfix &lt;V6V7Oainfix &lt;V7V3Aainfix &lt;=c0V7FAainfix &lt;V6V0Aainfix &lt;=V3V6Aainfix &lt;=c0V3Iainfix =V6ainfix -V2c1FAainfix &lt;V2V0Aainfix &lt;=c0V2Aainfix &lt;V3V0Aainfix &lt;=c0V3ainfix &lt;=agetV1V8agetV1V3Iainfix &lt;V8V0Aainfix &lt;=c0V8FAainfix &lt;V3V0Aainfix &lt;=c0V3Iainfix &lt;=agetV1V9amaxagetV1V3agetV1V2Iainfix &lt;V9V0Aainfix &lt;V2V9Oainfix &lt;V9V3Aainfix &lt;=c0V9FAainfix &lt;V2V0Aainfix &lt;=V3V2Aainfix &lt;=c0V3FFAainfix &lt;=agetV1V10amaxagetV1c0agetV1ainfix -V0c1Iainfix &lt;V10V0Aainfix &lt;ainfix -V0c1V10Oainfix &lt;V10c0Aainfix &lt;=c0V10FAainfix &lt;ainfix -V0c1V0Aainfix &lt;=c0ainfix -V0c1Aainfix &lt;=c0c0Iainfix &lt;c0V0FF">
......
examples/foveoos2011/duplets/why3session.xml
View file @ a8a44982
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/usr/local/share/why3/why3session.dtd">
<why3session
name="foveoos2011/duplets/why3session.xml" shape_version="2">
<prover
......@@ -36,7 +36,7 @@
locfile="foveoos2011/duplets/../duplets.mlw"
loclnum="43" loccnumb="6" loccnume="12"
expl="parameter duplet"
sum="aaef24bf6872f9c4745d6a701f54da37"
sum="282ac37920f177cf046d50aec95d7d04"
proved="true"
expanded="true"
shape="ais_dupletV3V4V5NICV1aNonefaSomeVainfix =V6agetV2V4NIainfix &lt;V5V0Aainfix &lt;V4V5Aainfix &lt;V4ainfix +ainfix -V0c2c1Aainfix &lt;=c0V4FNAiCV1aNonefaSomeVainfix =V9V8ais_dupletV3V10V11NICV1aNonefaSomeVainfix =V12agetV2V10NIainfix &lt;V11V0Aainfix &lt;V10V11Aainfix &lt;V10ainfix +V7c1Aainfix &lt;=c0V10Fais_dupletV3V13V14NICV1aNonefaSomeVainfix =V15agetV2V13NIainfix &lt;V14V0Aainfix &lt;V13V14Aainfix &lt;V13ainfix +V7c1Aainfix &lt;=c0V13FIais_dupletV3V7V16NIainfix &lt;V16ainfix +ainfix -V0c1c1Aainfix &lt;V7V16FAiainfix =agetV2V17V8CV1aNonefaSomeVainfix =V20agetV2V18NAais_dupletV3V18V19Iainfix =V19V17Aainfix =V18V7Fais_dupletV3V7V21NIainfix &lt;V21ainfix +V17c1Aainfix &lt;V7V21FAainfix &lt;V17V0Aainfix &lt;=c0V17Iais_dupletV3V7V22NIainfix &lt;V22V17Aainfix &lt;V7V22FIainfix &lt;=V17ainfix -V0c1Aainfix &lt;=ainfix +V7c1V17FAais_dupletV3V7V23NIainfix &lt;V23ainfix +V7c1Aainfix &lt;V7V23FIainfix &lt;=ainfix +V7c1ainfix -V0c1Aais_dupletV3V24V25NICV1aNonefaSomeVainfix =V26agetV2V24NIainfix &lt;V25V0Aainfix &lt;V24V25Aainfix &lt;V24ainfix +V7c1Aainfix &lt;=c0V24FIainfix &gt;ainfix +V7c1ainfix -V0c1LagetV2V7Aainfix &lt;V7V0Aainfix &lt;=c0V7Iais_dupletV3V27V28NICV1aNonefaSomeVainfix =V29agetV2V27NIainfix &lt;V28V0Aainfix &lt;V27V28Aainfix &lt;V27V7Aainfix &lt;=c0V27FIainfix &lt;=V7ainfix -V0c2Aainfix &lt;=c0V7FAais_dupletV3V30V31NICV1aNonefaSomeVainfix =V32agetV2V30NIainfix &lt;V31V0Aainfix &lt;V30V31Aainfix &lt;V30c0Aainfix &lt;=c0V30FIainfix &lt;=c0ainfix -V0c2Aainfix &gt;c0ainfix -V0c2NICV1aNonefaSomeVainfix =V35agetV2V33NAais_dupletV3V33V34EAainfix &lt;=c2V0Lamk arrayV0V2FFF">
......@@ -64,7 +64,7 @@
locfile="foveoos2011/duplets/../duplets.mlw"
loclnum="75" loccnumb="6" loccnume="13"
expl="parameter duplets"
sum="3b7d11776c6b8563220ab05f94c52ec5"
sum="5dd8ad997d77137f499f9396569cad38"
proved="true"
expanded="true"
shape="ainfix =agetV1V3agetV1V6NAais_dupletV2V6V7Aais_dupletV2V3V4Iainfix =V5agetV1V6NAais_dupletV2V6V7FAainfix =V5agetV1V8NAais_dupletV2V8V9EAainfix &lt;=c2V0LagetV1V4Aainfix &lt;V4V0Aainfix &lt;=c0V4Iais_dupletV2V3V4FAais_dupletV2V10V11EAainfix &lt;=c2V0Iainfix =agetV1V12agetV1V14NAais_dupletV2V14V15Aais_dupletV2V12V13EAainfix &lt;=c4V0Lamk arrayV0V1FF">
......@@ -84,7 +84,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="0"
......
examples/foveoos2011/tree_max/why3session.xml
View file @ a8a44982
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/usr/local/share/why3/why3session.dtd">
<why3session
name="foveoos2011/tree_max/why3session.xml" shape_version="2">
<prover
......@@ -50,7 +50,7 @@
locfile="foveoos2011/tree_max/../tree_max.mlw"
loclnum="58" loccnumb="10" loccnume="17"
expl="parameter max_aux"
sum="fd19a0d15660fc84baa28f170db90b43"
sum="891fffcd5f344e46c98ef7ae8747969d"
proved="true"
expanded="true"
shape="CV0aNullainfix &gt;=V1V1Aage_treeV1V0aTreeVVVamemV6V0Oainfix =V6V1Aainfix &gt;=V6V1Aage_treeV6V0IamemV6V3Oainfix =V6V5Aainfix &gt;=V6V5Aage_treeV6V3FIamemV5V4Oainfix =V5amaxV2V1Aainfix &gt;=V5amaxV2V1Aage_treeV5V4FFF">
......@@ -70,7 +70,7 @@
locfile="foveoos2011/tree_max/../tree_max.mlw"
loclnum="68" loccnumb="6" loccnume="9"
expl="parameter max"
sum="2b396ce2e0ce29212289ff83a143c14c"
sum="ee2fc36b6012dbe44bd1d38988ffc725"
proved="true"
expanded="true"
shape="CV0aNullfaTreeVVVamemV5V0Aage_treeV5V0IamemV5V2Oainfix =V5V4Aainfix &gt;=V5V4Aage_treeV5V2FIamemV4V3Oainfix =V4V1Aainfix &gt;=V4V1Aage_treeV4V3FIainfix =V0aNullNF">
......@@ -82,7 +82,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
</theory>
......
examples/hoare_logic/formula/why3session.xml
View file @ a8a44982
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/usr/local/share/why3/why3session.dtd">
<why3session
name="hoare_logic/formula/why3session.xml" shape_version="2">
<prover
......@@ -35,7 +35,7 @@
name="Test1"
locfile="hoare_logic/formula/../formula.why"
loclnum="47" loccnumb="7" loccnume="12"
sum="976cf2a1c08759beae42d6227ad23ce8"
sum="ecd0baa86456fee2a4f497d193389d75"
proved="true"
expanded="true"
shape="ainfix =aevalaForaFnotaFatomV0aFfalseV1aFalseLasetaconstaFalseV0aTrueLamk_identc0">
......@@ -53,7 +53,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
<result status="valid" time="0.05"/>
</proof>
<proof
prover="2"
......
examples/hoare_logic/wp2/why3session.xml
View file @ a8a44982
This diff is collapsed.
examples/hoare_logic/wp3/why3session.xml
View file @ a8a44982
This diff is collapsed.
examples/hoare_logic/wp4/why3session.xml
View file @ a8a44982
This diff is collapsed.
examples/my_cosine/why3session.xml
View file @ a8a44982
This diff is collapsed.
examples/programs/add_list/why3session.xml
View file @ a8a44982
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/usr/local/share/why3/why3session.dtd">
<why3session
name="programs/add_list/why3session.xml" shape_version="2">
<prover
......@@ -36,7 +36,7 @@
locfile="programs/add_list/../add_list.mlw"
loclnum="33" loccnumb="8" loccnume="11"
expl="parameter sum"
sum="e8f428f8ff2f8c4c809829b72ccf847b"
sum="f7d306de59b39cf45eadf71089850050"
proved="true"
expanded="true"
shape="CV0aNilainfix =c0.0aadd_realV0Aainfix =c0aadd_intV0aConsVVCV1aIntegerVainfix =V4aadd_realV0Aainfix =ainfix +V5V3aadd_intV0aRealVainfix =ainfix +.V6V4aadd_realV0Aainfix =V3aadd_intV0Iainfix =V4aadd_realV2Aainfix =V3aadd_intV2FF">
......@@ -48,7 +48,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="1"
......@@ -72,7 +72,7 @@
locfile="programs/add_list/../add_list.mlw"
loclnum="46" loccnumb="4" loccnume="8"
expl="parameter main"
sum="840b6a07c4fa0fa9cbf47eb732cef621"
sum="cee447c37a40e9395e9dc1efbf26f7d3"
proved="true"
expanded="true"
shape="ainfix =V1c4.7Aainfix =V0c22Iainfix =V1aadd_realaConsaIntegerc5aConsaRealc3.3aConsaIntegerc8aConsaRealc1.4aConsaIntegerc9aNilAainfix =V0aadd_intaConsaIntegerc5aConsaRealc3.3aConsaIntegerc8aConsaRealc1.4aConsaIntegerc9aNilF">
......@@ -107,7 +107,7 @@
locfile="programs/add_list/../add_list.mlw"
loclnum="65" loccnumb="4" loccnume="7"
expl="parameter sum"
sum="a1e9fc3e91b972d21b1df21784b15a5f"
sum="69c23e7543a318c07b301d459f137a57"
proved="true"
expanded="true"
shape="CV1aNilainfix =V2aadd_realV0Aainfix =V3aadd_intV0aConsaIntegerVVainfix =ainfix +.V2aadd_realV7aadd_realV0Aainfix =ainfix +V6aadd_intV7aadd_intV0Iainfix =V7V5FIainfix =V6ainfix +V3V4FaConsaRealVVainfix =ainfix +.V10aadd_realV11aadd_realV0Aainfix =ainfix +V3aadd_intV11aadd_intV0Iainfix =V11V9FIainfix =V10ainfix +.V2V8FIainfix =ainfix +.V2aadd_realV1aadd_realV0Aainfix =ainfix +V3aadd_intV1aadd_intV0FFFAainfix =ainfix +.c0.0aadd_realV0aadd_realV0Aainfix =ainfix +c0aadd_intV0aadd_intV0F">
......@@ -135,7 +135,7 @@
locfile="programs/add_list/../add_list.mlw"
loclnum="89" loccnumb="4" loccnume="8"