Commit 221c0e2c authored by MARCHE Claude's avatar MARCHE Claude

Update sessions after small changes in theories/set.why

parent 4eb4518f
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/users/demons/melquion/src/why3/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/home/marche/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="0b906d19fc47dc5b0bc0f52ad3c7e2a6"
sum="e5228e61b1bf3ae1b0b7f5c3c5fc4a87"
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="0e867f2d3083e428ad1c9c1a524b8ded"
sum="ad9722cec30603b93adbe5ee3c3947d6"
proved="false"
expanded="true"
shape="amemV0aintegerF">
......@@ -154,14 +154,14 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.01"/>
<result status="unknown" time="0.00"/>
</proof>
</goal>
<goal
name="foo"
locfile="bts/fsetint/../fsetint.why"
loclnum="15" loccnumb="7" loccnume="10"
sum="f6b9b46665fbeed71dcc8e03749b097f"
sum="7c99b63c028149b0160d1fc1b66ea6ba"
proved="false"
expanded="true"
shape="f">
......@@ -251,7 +251,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
<result status="unknown" time="0.01"/>
</proof>
<proof
prover="3"
......@@ -267,7 +267,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.01"/>
<result status="unknown" time="0.02"/>
</proof>
<proof
prover="1"
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/users/demons/melquion/src/why3/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<why3session
name="hoare_logic/blocking_semantics/why3session.xml" shape_version="2">
<prover
......@@ -84,7 +84,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.17"/>
<result status="unknown" time="0.16"/>
</proof>
</goal>
<goal
......@@ -127,7 +127,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
......@@ -144,7 +144,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.08"/>
<result status="unknown" time="0.09"/>
</proof>
</goal>
<goal
......@@ -157,11 +157,11 @@
shape="aeval_fmlaV1aConsaTuple2V4V6aConsaTuple2V3V5V2V0qaeval_fmlaV1aConsaTuple2V3V5aConsaTuple2V4V6V2V0Iainfix =V3V4NF">
<proof
prover="0"
timelimit="9"
timelimit="10"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="4.59"/>
<result status="unknown" time="4.50"/>
</proof>
</goal>
<goal
......@@ -178,7 +178,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="1.42"/>
<result status="unknown" time="1.41"/>
</proof>
</goal>
<goal
......@@ -195,7 +195,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.08"/>
<result status="timeout" time="5.01"/>
</proof>
</goal>
<goal
......@@ -212,7 +212,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.08"/>
<result status="timeout" time="5.01"/>
</proof>
</goal>
<goal
......@@ -229,7 +229,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.08"/>
<result status="timeout" time="5.02"/>
</proof>
</goal>
<goal
......@@ -246,7 +246,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.38"/>
<result status="timeout" time="5.02"/>
</proof>
</goal>
<goal
......@@ -313,7 +313,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
......@@ -330,7 +330,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.09"/>
<result status="timeout" time="5.02"/>
</proof>
<proof
prover="1"
......@@ -338,7 +338,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.09"/>
<result status="timeout" time="5.01"/>
</proof>
<proof
prover="0"
......@@ -354,7 +354,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.09"/>
<result status="timeout" time="5.02"/>
</proof>
<proof
prover="5"
......@@ -362,7 +362,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.19"/>
<result status="timeout" time="5.02"/>
</proof>
</goal>
<goal
......@@ -379,7 +379,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.05"/>
<result status="valid" time="0.04"/>
</proof>
</goal>
<goal
......@@ -396,7 +396,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.08"/>
<result status="timeout" time="5.12"/>
</proof>
<proof
prover="1"
......@@ -404,7 +404,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.08"/>
<result status="timeout" time="5.02"/>
</proof>
<proof
prover="0"
......@@ -412,7 +412,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="4.78"/>
<result status="unknown" time="4.74"/>
</proof>
<proof
prover="2"
......@@ -420,7 +420,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.08"/>
<result status="timeout" time="5.01"/>
</proof>
<proof
prover="5"
......@@ -428,7 +428,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.38"/>
<result status="timeout" time="5.01"/>
</proof>
</goal>
<goal
......@@ -445,7 +445,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.02"/>
<result status="timeout" time="5.01"/>
</proof>
<proof
prover="1"
......@@ -453,7 +453,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.02"/>
<result status="timeout" time="5.01"/>
</proof>
<proof
prover="0"
......@@ -461,7 +461,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.02"/>
<result status="timeout" time="5.01"/>
</proof>
<proof
prover="2"
......@@ -469,7 +469,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.02"/>
<result status="timeout" time="5.01"/>
</proof>
<proof
prover="5"
......@@ -494,7 +494,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.12"/>
<result status="timeout" time="5.11"/>
</proof>
<proof
prover="1"
......@@ -502,7 +502,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.02"/>
<result status="timeout" time="5.01"/>
</proof>
<proof
prover="0"
......@@ -510,7 +510,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.02"/>
<result status="timeout" time="5.01"/>
</proof>
<proof
prover="2"
......@@ -518,7 +518,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.33"/>
<result status="timeout" time="5.02"/>
</proof>
<proof
prover="5"
......@@ -526,7 +526,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.13"/>
<result status="timeout" time="5.02"/>
</proof>
</goal>
<goal
......@@ -543,7 +543,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.51"/>
<result status="valid" time="0.50"/>
</proof>
</goal>
<goal
......@@ -560,7 +560,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.02"/>
<result status="timeout" time="5.01"/>
</proof>
</goal>
</theory>
......@@ -584,7 +584,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.02"/>
<result status="timeout" time="5.01"/>
</proof>
</goal>
<goal
......@@ -601,7 +601,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="9.98"/>
<result status="valid" time="9.94"/>
</proof>
</goal>
<goal
......@@ -618,7 +618,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.03"/>
<result status="timeout" time="5.01"/>
</proof>
</goal>
<goal
......@@ -635,7 +635,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.04"/>
<result status="timeout" time="5.01"/>
</proof>
</goal>
<goal
......@@ -652,7 +652,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.04"/>
<result status="timeout" time="5.01"/>
</proof>
</goal>
<goal
......@@ -669,7 +669,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.04"/>
<result status="timeout" time="5.02"/>
</proof>
</goal>
<goal
......@@ -686,7 +686,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.03"/>
<result status="timeout" time="5.02"/>
</proof>
</goal>
</theory>
......@@ -700,7 +700,7 @@
name="assigns_refl"
locfile="hoare_logic/blocking_semantics/../blocking_semantics.mlw"
loclnum="487" loccnumb="6" loccnume="18"
sum="d12a0280d996d2455332b1a4e227bf69"
sum="207b728f8e24b65cfdf8155d73ac7f24"
proved="true"
expanded="false"
shape="aassignsV0V1V0F">
......@@ -710,14 +710,14 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="assigns_trans"
locfile="hoare_logic/blocking_semantics/../blocking_semantics.mlw"
loclnum="490" loccnumb="6" loccnume="19"
sum="cf0c5634ce5bb0161e74e4ee588fae69"
sum="1b5d0a35d5321935c26f7b6d6da5bcef"
proved="true"
expanded="false"
shape="aassignsV0V3V2IaassignsV1V3V2AaassignsV0V3V1F">
......@@ -734,7 +734,7 @@
name="assigns_union_left"
locfile="hoare_logic/blocking_semantics/../blocking_semantics.mlw"
loclnum="495" loccnumb="6" loccnume="24"
sum="d3b2b8077e0afc39dd71decfb43a5c03"
sum="ab97a79a4547f31f351fc9572a7ade02"
proved="true"
expanded="false"
shape="aassignsV0aunionV2V3V1IaassignsV0V2V1F">
......@@ -744,14 +744,14 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal
name="assigns_union_right"
locfile="hoare_logic/blocking_semantics/../blocking_semantics.mlw"
loclnum="499" loccnumb="6" loccnume="25"
sum="43721be948a583b90a1afef14abcf2d2"
sum="ef1c986fe8a7ffd355888623cef2a3d0"
proved="true"
expanded="false"
shape="aassignsV0aunionV2V3V1IaassignsV0V3V1F">
......@@ -768,7 +768,7 @@
name="wp_subst"
locfile="hoare_logic/blocking_semantics/../blocking_semantics.mlw"
loclnum="563" loccnumb="8" loccnume="16"
sum="56912b63c12cc1865fb31eaeff0eed32"
sum="265a766a7cb0365bb47d47e77f5c319c"
proved="false"
expanded="false"
shape="ainfix =asubstawpV0V1V2V3awpV0asubstV1V2V3Iafresh_in_exprV2V0F">
......@@ -777,7 +777,7 @@
name="wp_implies"
locfile="hoare_logic/blocking_semantics/../blocking_semantics.mlw"
loclnum="568" loccnumb="8" loccnume="18"
sum="7188d2758a4fe602092b7f8c16590f5a"
sum="092a912cf70664d783c8c0837fa769a3"
proved="false"
expanded="false"
shape="aeval_fmlaV2V3awpV4V1Iaeval_fmlaV2V3awpV4V0FIaeval_fmlaV5V6V1Iaeval_fmlaV5V6V0FF">
......@@ -786,25 +786,25 @@
name="wp_conj"
locfile="hoare_logic/blocking_semantics/../blocking_semantics.mlw"
loclnum="577" loccnumb="8" loccnume="15"
sum="785e1eb0909a53b839cb21e5da5e04d0"
sum="943dfa37ab963fe3c947bb1e22881337"
proved="false"
expanded="false"
shape="aeval_fmlaV0V1awpV2V4Aaeval_fmlaV0V1awpV2V3qaeval_fmlaV0V1awpV2aFandV3V4F">
<proof
prover="3"
timelimit="24"
timelimit="25"
memlimit="1000"
edited="blocking_semantics_WP_wp_conj_1.v"
obsolete="false"
archived="false">
<result status="unknown" time="12.00"/>
<result status="unknown" time="11.85"/>
</proof>
</goal>
<goal
name="wp_reduction"
locfile="hoare_logic/blocking_semantics/../blocking_semantics.mlw"
loclnum="584" loccnumb="8" loccnume="20"
sum="ffb351c824824bd1728bedc04fca0f84"
sum="ad4fe21da86e1900cd2dc0d5f3954060"
proved="true"
expanded="false"
shape="aeval_fmlaV1V3awpV5V6Iaeval_fmlaV0V2awpV4V6FIaone_stepV0V2V4V1V3V5F">
......@@ -815,14 +815,14 @@
edited="blocking_semantics_WP_wp_reduction_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.78"/>
<result status="valid" time="0.76"/>
</proof>
</goal>
<goal
name="decide_value"
locfile="hoare_logic/blocking_semantics/../blocking_semantics.mlw"
loclnum="597" loccnumb="8" loccnume="20"
sum="7f5a49a6b163b0d9f798420e7c386035"
sum="a2a1d1223a4e12a635ddf027163acde4"
proved="true"
expanded="false"
shape="ainfix =V0aEvalueV1EOanot_a_valueV0F">
......@@ -839,7 +839,7 @@
name="progress"
locfile="hoare_logic/blocking_semantics/../blocking_semantics.mlw"
loclnum="600" loccnumb="8" loccnume="16"
sum="0f93de1f14867094c73fb45594779111"
sum="9841f706af20265bae5147921eece1ba"
proved="true"
expanded="true"
shape="aone_stepV1V2V0V4V5V6EIanot_a_valueV0Aaeval_fmlaV1V2awpV0V3F">
......@@ -850,7 +850,7 @@
edited="blocking_semantics_WP_progress_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.86"/>
<result status="valid" time="0.85"/>
</proof>
</goal>
</theory>
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/users/demons/melquion/src/why3/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<why3session
name="hoare_logic/blocking_semantics2/why3session.xml" shape_version="2">
<prover
......@@ -88,7 +88,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="3.05"/>
<result status="timeout" time="3.07"/>
</proof>
<proof
prover="2"
......@@ -96,7 +96,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="3.08"/>
<result status="timeout" time="3.10"/>
</proof>
<proof
prover="0"
......@@ -112,7 +112,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="3.07"/>
<result status="timeout" time="3.05"/>
</proof>
<proof
prover="6"
......@@ -120,7 +120,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="3.11"/>
<result status="timeout" time="3.05"/>
</proof>
</goal>
<goal
......@@ -145,7 +145,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="3.06"/>
<result status="timeout" time="3.01"/>
</proof>
<proof
prover="0"
......@@ -153,7 +153,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="unknown" time="2.04"/>
<result status="unknown" time="2.00"/>
</proof>
<proof
prover="3"
......@@ -161,7 +161,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="3.02"/>
<result status="timeout" time="3.01"/>
</proof>
<proof
prover="6"
......@@ -169,7 +169,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="3.02"/>
<result status="timeout" time="3.01"/>
</proof>
</goal>
<goal
......@@ -186,7 +186,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="3.02"/>
<result status="timeout" time="3.11"/>
</proof>
<proof
prover="2"
......@@ -194,7 +194,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="3.02"/>
<result status="timeout" time="3.01"/>
</proof>
<proof
prover="0"
......@@ -202,7 +202,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="unknown" time="1.73"/>
<result status="unknown" time="1.68"/>
</proof>
<proof
prover="3"
......@@ -210,7 +210,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="3.02"/>
<result status="timeout" time="3.01"/>
</proof>
<proof
prover="6"
......@@ -218,7 +218,7 @@