Skip to content

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

update sessions after changes in stdlib

parent 462af650
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 2592 additions and 2620 deletions
examples/bitvectors/double/why3session.xml
View file @ 19294149
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/usr/local/share/why3/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<why3session
name="bitvectors/double/why3session.xml">
<prover
......@@ -47,7 +47,7 @@
name="nth_one1"
locfile="bitvectors/double/../double.why"
loclnum="73" loccnumb="8" loccnume="16"
sum="34a279baa129aac0fcc2d447f8de36b3"
sum="d18ab08209f31f731dfd704613a2e30b"
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.08"/>
<result status="valid" time="0.07"/>
</proof>
</goal>
<goal
name="nth_one2"
locfile="bitvectors/double/../double.why"
loclnum="74" loccnumb="8" loccnume="16"
sum="d4fd2ebb7543ddc1efbfc29bc763b12d"
sum="dbdf93155a985325f8f4fedd2cc1ce23"
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.06"/>
<result status="valid" time="0.05"/>
</proof>
</goal>
<goal
name="nth_one3"
locfile="bitvectors/double/../double.why"
loclnum="75" loccnumb="8" loccnume="16"
sum="53b2680762e76045630fdd36ac83e432"
sum="78dcef156ce4f14b8c06646563922753"
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="897a15945706f7211dfec1e426df12ec"
sum="ff5eb7f2e82fa0653ea1884adaa61d9f"
proved="true"
expanded="false"
shape="ainfix =asignaoneaFalse">
......@@ -147,7 +147,7 @@
name="exp_one"
locfile="bitvectors/double/../double.why"
loclnum="78" loccnumb="8" loccnume="15"
sum="91a77d47edf1564a3294b7ac8bf6cd19"
sum="08f27bcd545f7664746d5232bff96501"
proved="true"
expanded="false"
shape="ainfix =aexpaonec1023">
......@@ -157,7 +157,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="4.85"/>
<result status="valid" time="4.87"/>
</proof>
<proof
prover="3"
......@@ -166,14 +166,14 @@
edited="double_TestDouble_exp_one_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.61"/>
<result status="valid" time="0.60"/>
</proof>
</goal>
<goal
name="mantissa_one"
locfile="bitvectors/double/../double.why"
loclnum="79" loccnumb="8" loccnume="20"
sum="db1502f2576a2745cf7a8ce06bb58128"
sum="3916c94461ebce50b2aa55917a3011b8"
proved="true"
expanded="false"
shape="ainfix =amantissaaonec0">
......@@ -183,7 +183,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.68"/>
<result status="valid" time="0.67"/>
</proof>
<proof
prover="0"
......@@ -191,7 +191,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.25"/>
<result status="valid" time="0.26"/>
</proof>
<proof
prover="5"
......@@ -199,14 +199,14 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="3.05"/>
<result status="valid" time="2.98"/>
</proof>
</goal>
<goal
name="double_value_of_1"
locfile="bitvectors/double/../double.why"
loclnum="81" loccnumb="8" loccnume="25"
sum="3d1cdf4304de33fa460a20135b841e4a"
sum="d5d64f7ab2d369243a42739379eb07a9"
proved="true"
expanded="false"
shape="ainfix =adouble_of_bv64aonec1.0">
......@@ -232,7 +232,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.03"/>
</proof>
</goal>
</theory>
......
examples/bitvectors/neg_as_xor/why3session.xml
View file @ 19294149
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/usr/local/share/why3/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<why3session
name="bitvectors/neg_as_xor/why3session.xml">
<prover
......@@ -32,7 +32,7 @@
name="Nth_j"
locfile="bitvectors/neg_as_xor/../neg_as_xor.why"
loclnum="13" loccnumb="8" loccnume="13"
sum="7ec4d7915c10debbadd32a08b1bba541"
sum="abc7eaee768e35d633c1052837f84c8c"
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.07"/>
<result status="valid" time="0.08"/>
</proof>
</goal>
<goal
name="sign_of_j"
locfile="bitvectors/neg_as_xor/../neg_as_xor.why"
loclnum="15" loccnumb="8" loccnume="17"
sum="fa860d7163dfa79ef6d19648db1e3bf3"
sum="34eec7200ed8e48eaf94d3cc7620a3dc"
proved="true"
expanded="false"
shape="ainfix =asignajaTrue">
......@@ -59,14 +59,14 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal
name="mantissa_of_j"
locfile="bitvectors/neg_as_xor/../neg_as_xor.why"
loclnum="16" loccnumb="8" loccnume="21"
sum="593bd2ae8ac1580cd936f7465278b56a"
sum="6970305c1ef7a17012115ef268945552"
proved="true"
expanded="false"
shape="ainfix =amantissaajc0">
......@@ -76,7 +76,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.65"/>
<result status="valid" time="0.66"/>
</proof>
<proof
prover="0"
......@@ -92,14 +92,14 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="3.10"/>
<result status="valid" time="3.40"/>
</proof>
</goal>
<goal
name="exp_of_j"
locfile="bitvectors/neg_as_xor/../neg_as_xor.why"
loclnum="17" loccnumb="8" loccnume="16"
sum="92d1d38910f3800cff767a0156f01ca4"
sum="8faf4117201f47f3d9a2bbedaae3c556"
proved="true"
expanded="false"
shape="ainfix =aexpajc0">
......@@ -109,7 +109,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.67"/>
<result status="valid" time="0.66"/>
</proof>
<proof
prover="0"
......@@ -125,14 +125,14 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="3.09"/>
<result status="valid" time="3.21"/>
</proof>
</goal>
<goal
name="int_of_bv"
locfile="bitvectors/neg_as_xor/../neg_as_xor.why"
loclnum="18" loccnumb="8" loccnume="17"
sum="5720bbc6be0a2fd678d97babf499bd80"
sum="aa658bdd2ce269f4bcf82983ea27b498"
proved="true"
expanded="false"
shape="ainfix =adouble_of_bv64ajc0.0">
......@@ -150,7 +150,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.04"/>
</proof>
<proof
prover="3"
......@@ -165,7 +165,7 @@
name="MainResultBits"
locfile="bitvectors/neg_as_xor/../neg_as_xor.why"
loclnum="20" loccnumb="8" loccnume="22"
sum="63b7e5215c95e3ef6b230f9d389e494a"
sum="03bfc9513d319c9b73254a74d633013c"
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.07"/>
<result status="valid" time="0.08"/>
</proof>
</goal>
<goal
name="MainResultSign"
locfile="bitvectors/neg_as_xor/../neg_as_xor.why"
loclnum="23" loccnumb="8" loccnume="22"
sum="30826f815867c84380c4207b9e3ab0b6"
sum="4f563eb91bd49148fab0954a7ac4b7a8"
proved="true"
expanded="false"
shape="ainfix =anthabw_xorV0ajc63anotbanthV0c63F">
......@@ -192,14 +192,14 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="Sign_of_xor_j"
locfile="bitvectors/neg_as_xor/../neg_as_xor.why"
loclnum="25" loccnumb="8" loccnume="21"
sum="c3ffa2aae59ab871686c14e211d573d2"
sum="b19c46ce4058940cea14d79fc9d3d0c0"
proved="true"
expanded="false"
shape="ainfix =asignabw_xorV0ajanotbasignV0F">
......@@ -217,7 +217,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.03"/>
</proof>
<proof
prover="3"
......@@ -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="bdd1a3dd5cf05477f7cc8de0d890c8c1"
sum="bf6f51fa79aaec331c331c4b0ebda5dd"
proved="true"
expanded="false"
shape="ainfix =aexpabw_xorV0ajaexpV0F">
......@@ -242,7 +242,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.68"/>
<result status="valid" time="0.69"/>
</proof>
<proof
prover="0"
......@@ -250,7 +250,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.90"/>
<result status="valid" time="0.91"/>
</proof>
<proof
prover="3"
......@@ -258,14 +258,14 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="2.92"/>
<result status="valid" time="3.16"/>
</proof>
</goal>
<goal
name="Mantissa_of_xor_j"
locfile="bitvectors/neg_as_xor/../neg_as_xor.why"
loclnum="29" loccnumb="8" loccnume="25"
sum="b997d22b0c326c06f927e5cdc38d194e"
sum="5742f66ed818a0906e1a42f5abc3f359"
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.69"/>
</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.56"/>
</proof>
<proof
prover="3"
......@@ -291,14 +291,14 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="3.25"/>
<result status="valid" time="3.32"/>
</proof>
</goal>
<goal
name="MainResultZero"
locfile="bitvectors/neg_as_xor/../neg_as_xor.why"
loclnum="31" loccnumb="8" loccnume="22"
sum="563c0cf0e2af6a9fc62ef235940036ba"
sum="921818a19cb7e0dd4adaa3784b678292"
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.70"/>
<result status="valid" time="0.67"/>
</proof>
<proof
prover="0"
......@@ -316,7 +316,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="1.76"/>
<result status="valid" time="1.72"/>
</proof>
<proof
prover="3"
......@@ -324,14 +324,14 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="2.82"/>
<result status="valid" time="3.10"/>
</proof>
</goal>
<goal
name="sign_neg"
locfile="bitvectors/neg_as_xor/../neg_as_xor.why"
loclnum="34" loccnumb="8" loccnume="16"
sum="abdf4c8e2fa5fd4e490a8315fd4c9548"
sum="b54402c83b94259ef155185ddfdf1260"
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.86"/>
<result status="valid" time="2.80"/>
</proof>
</goal>
<goal
name="MainResult"
locfile="bitvectors/neg_as_xor/../neg_as_xor.why"
loclnum="36" loccnumb="8" loccnume="18"
sum="7885f90ac0dd14f66c73365f153f63a2"
sum="fa6f38fbf181f139fbf31b549f4e91ba"
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="0.91"/>
</proof>
</goal>
</theory>
......
examples/bitvectors/power2/why3session.xml
View file @ 19294149
This diff is collapsed.
examples/bts/12475/why3session.xml
View file @ 19294149
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/usr/local/share/why3/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<why3session
name="bts/12475/why3session.xml">
<prover
......@@ -34,7 +34,7 @@
name="toto"
locfile="bts/12475/../12475.why"
loclnum="6" loccnumb="7" loccnume="11"
sum="bef94593fc244d7e427d59e3543a820b"
sum="5dfb61fb4e47918e08b6c1345d16fd44"
proved="true"
expanded="true"
shape="ainfix &lt;V0ainfix +aroundaUpV0c1.F">
......
examples/bts/12934/why3session.xml
View file @ 19294149
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/usr/local/share/why3/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<why3session
name="bts/12934/why3session.xml">
<prover
......@@ -30,7 +30,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.43"/>
<result status="valid" time="0.50"/>
</proof>
</goal>
</theory>
......
examples/bts/13849/why3session.xml
View file @ 19294149
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/usr/local/share/why3/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<why3session
name="bts/13849/why3session.xml">
<prover
......@@ -31,7 +31,7 @@
edited="13849_T_x_2.v"
obsolete="false"
archived="false">
<result status="valid" time="0.42"/>
<result status="valid" time="0.51"/>
</proof>
</goal>
</theory>
......
examples/bts/13853/why3session.xml
View file @ 19294149
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/usr/local/share/why3/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<why3session
name="bts/13853/why3session.xml">
<prover
......@@ -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
......@@ -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>
......
examples/bts/13854/why3session.xml
View file @ 19294149
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/usr/local/share/why3/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<why3session
name="bts/13854/why3session.xml">
<prover
......@@ -31,7 +31,7 @@
edited="13854_T_g_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.43"/>
<result status="valid" time="0.50"/>
</proof>
</goal>
<goal
......@@ -49,7 +49,7 @@
edited="13854_T_x_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.44"/>
<result status="valid" time="0.50"/>
</proof>
</goal>
</theory>
......
examples/check-builtin/ac/why3session.xml
View file @ 19294149
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/usr/local/share/why3/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<why3session
name="check-builtin/ac/why3session.xml">
<prover
......
examples/check-builtin/array/why3session.xml
View file @ 19294149
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/usr/local/share/why3/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<why3session
name="check-builtin/array/why3session.xml">
<prover
......@@ -119,7 +119,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="4"
......@@ -127,7 +127,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="1"
......@@ -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"
......@@ -192,7 +192,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.14"/>
<result status="valid" time="0.15"/>
</proof>
<proof
prover="1"
......@@ -257,7 +257,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.22"/>
<result status="valid" time="0.24"/>
</proof>
<proof
prover="1"
......
examples/check-builtin/bool/why3session.xml
View file @ 19294149
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/usr/local/share/why3/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<why3session
name="check-builtin/bool/why3session.xml">
<prover
......@@ -91,7 +91,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="1"
......@@ -132,7 +132,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="1"
......
examples/check-builtin/euclideandivision/why3session.xml
View file @ 19294149
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/usr/local/share/why3/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<why3session
name="check-builtin/euclideandivision/why3session.xml">
<prover
......@@ -50,7 +50,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="10.31"/>
<result status="timeout" time="9.45"/>
</proof>
<proof
prover="1"
......@@ -66,7 +66,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
......@@ -91,7 +91,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="10.36"/>
<result status="timeout" time="9.26"/>
</proof>
<proof
prover="1"
......@@ -107,7 +107,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
</theory>
......
examples/check-builtin/floats/why3session.xml
View file @ 19294149
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/usr/local/share/why3/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<why3session
name="check-builtin/floats/why3session.xml">
<prover
......@@ -32,7 +32,7 @@
name="Round_single_01"
locfile="check-builtin/floats/../floats.why"
loclnum="11" loccnumb="7" loccnume="22"
sum="573c0411296e0cd6234d1297e8b577c1"
sum="88a4c1b2a6f1f03b9b71187a7948ae7e"
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="5a42446f594a536207f1c027b72d61b8"
sum="0a6c684833c7b3a0d8f1d2a061ac45f2"
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="44e3f9d032bf5fc4ad04532da6e3bb0f"
sum="e10e2f63ebfa7211f99fd93fb8668224"
proved="true"
expanded="true"
shape="ainfix &lt;=aprefix -c3.0V0Iainfix &lt;=aabsV0c2.0F">
......@@ -76,7 +76,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="1"
......@@ -92,7 +92,7 @@