Commit a7d9e86f authored by MARCHE Claude's avatar MARCHE Claude

Fix sessions after removal of unused quantified variables

parent 412f3e5c
<?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="check-builtin/real/why3session.xml" shape_version="2">
<prover
......@@ -74,7 +74,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="3"
......@@ -106,7 +106,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
......@@ -139,7 +139,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="3"
......@@ -196,7 +196,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="3"
......@@ -366,7 +366,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="3"
......@@ -480,7 +480,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="3"
......@@ -537,7 +537,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="3"
......@@ -617,7 +617,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
......@@ -634,7 +634,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="2"
......@@ -650,7 +650,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="3"
......@@ -674,7 +674,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
......@@ -691,7 +691,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="1.28"/>
<result status="valid" time="1.27"/>
</proof>
<proof
prover="2"
......@@ -731,7 +731,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="32.82"/>
<result status="valid" time="33.10"/>
</proof>
</goal>
</theory>
......@@ -801,7 +801,7 @@
name="Pow_2_2"
locfile="check-builtin/real/../real.why"
loclnum="42" loccnumb="8" loccnume="15"
sum="51dc68a8f6198d61d48bccdb10ab7308"
sum="b4f39dbe2ac4dd89e455abedb473c966"
proved="true"
expanded="false"
shape="ainfix =apowerc2.0c2c4.0">
......@@ -811,7 +811,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="3.02"/>
<result status="timeout" time="3.01"/>
</proof>
<proof
prover="2"
......@@ -835,7 +835,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="unknown" time="0.15"/>
<result status="unknown" time="0.16"/>
</proof>
<proof
prover="4"
......@@ -851,7 +851,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="3.02"/>
<result status="timeout" time="3.01"/>
</proof>
<proof
prover="1"
......@@ -873,7 +873,7 @@
name="Pow_2_2"
locfile="check-builtin/real/../real.why"
loclnum="51" loccnumb="8" loccnume="15"
sum="f5b5f77a5e8663c6bca7a8bcc2abe2e8"
sum="38a4f95c27069a2dc6dcd4d7442ce8f7"
proved="true"
expanded="false"
shape="ainfix =apowc2.0c2.0c4.0">
......@@ -955,7 +955,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.09"/>
<result status="valid" time="0.08"/>
</proof>
</goal>
<goal
......@@ -972,7 +972,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.16"/>
<result status="valid" time="0.15"/>
</proof>
<proof
prover="0"
......@@ -980,7 +980,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="4.00"/>
<result status="valid" time="3.94"/>
</proof>
<proof
prover="2"
......@@ -1004,7 +1004,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.12"/>
<result status="valid" time="0.11"/>
</proof>
<proof
prover="1"
......@@ -1012,7 +1012,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="3.44"/>
<result status="valid" time="3.34"/>
</proof>
</goal>
<goal
......
This diff is collapsed.
This diff is collapsed.
<?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="programs/list_rev/why3session.xml" shape_version="2">
<prover
......@@ -36,7 +36,7 @@
name="acyclic_list"
locfile="programs/list_rev/../list_rev.mlw"
loclnum="109" loccnumb="8" loccnume="20"
sum="6fe7363650b0ba023b5484233086a6e6"
sum="c582d66421efa4c8c1fa0751a607276b"
proved="false"
expanded="true"
shape="asep_node_listV0V1amixfix []V0V1Iais_listV0V1Iainfix =V1anullNF">
......@@ -54,7 +54,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="unknown" time="2.26"/>
<result status="unknown" time="2.18"/>
</proof>
<proof
prover="0"
......@@ -69,7 +69,7 @@
name="consistent"
locfile="programs/list_rev/../list_rev.mlw"
loclnum="112" loccnumb="7" loccnume="17"
sum="2e573958f566bbde02242d6304a50c70"
sum="4b207f3e6c8ab31e80e9ab412daebe80"
proved="false"
expanded="true"
shape="fIais_listV0V2Iais_listV0V1F">
......@@ -79,7 +79,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="unknown" time="0.02"/>
<result status="unknown" time="0.03"/>
</proof>
<proof
prover="1"
......@@ -87,7 +87,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="unknown" time="0.16"/>
<result status="unknown" time="0.15"/>
</proof>
<proof
prover="0"
......@@ -103,7 +103,7 @@
locfile="programs/list_rev/../list_rev.mlw"
loclnum="115" loccnumb="6" loccnume="14"
expl="parameter list_rev"
sum="6bd088ac04edb428f5d364d134b317b3"
sum="13592b1c84c778d77586cbf3aa5f42aa"
proved="true"
expanded="true"
shape="iainfix =V3anullNasep_list_listV5V7V6Aais_listV5V6Aais_listV5V7Iainfix =V7amixfix []V4V3FIainfix =V6V3FIainfix =V5amixfix [&lt;-]V4V3V2Fais_listV4V2Iasep_list_listV4V3V2Aais_listV4V2Aais_listV4V3FAasep_list_listV1V0anullAais_listV1anullAais_listV1V0Iais_listV1V0F">
......@@ -122,7 +122,7 @@
name="reverse_append"
locfile="programs/list_rev/../list_rev.mlw"
loclnum="145" loccnumb="8" loccnume="22"
sum="2269ed50b6b4c839c1299b498b3ca7dd"
sum="a347b9e0b4ffb3f5d04fd1e338e8a6f4"
proved="true"
expanded="true"
shape="ainfix =ainfix ++areverseaConsV2V0V1ainfix ++areverseV0aConsV2V1Fainfix ++areverseV0aConsV2V1ainfix ++areverseaConsV2V0V1">
......@@ -132,7 +132,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
......@@ -140,7 +140,7 @@
locfile="programs/list_rev/../list_rev.mlw"
loclnum="156" loccnumb="6" loccnume="19"
expl="parameter list_rev_behv"
sum="e87c9518dce19070cbb7d3e3f8f90a36"
sum="1a1b135eb95701a3f1f5f6eaf618482a"
proved="false"
expanded="true"
shape="iainfix =V3anullNainfix =areverseamodelV1V0ainfix ++areverseamodelV5V7amodelV5V6Aasep_list_listV5V7V6Aais_listV5V6Aais_listV5V7Iainfix =V7amixfix []V4V3FIainfix =V6V3FAainfix =ainfix ++areverseaConsV3amodelV5amixfix []V4V3amodelV5V2ainfix ++areverseamodelV5amixfix []V4V3aConsV3amodelV5V2Iainfix =V5amixfix [&lt;-]V4V3V2Fainfix =areverseamodelV1V0amodelV4V2Aais_listV4V2Iainfix =areverseamodelV1V0ainfix ++areverseamodelV4V3amodelV4V2Aasep_list_listV4V3V2Aais_listV4V2Aais_listV4V3FAainfix =areverseamodelV1V0ainfix ++areverseamodelV1V0amodelV1anullAasep_list_listV1V0anullAais_listV1anullAais_listV1V0Iais_listV1V0F">
......@@ -168,7 +168,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="10.03"/>
<result status="timeout" time="10.04"/>
</proof>
</goal>
</theory>
......@@ -210,7 +210,7 @@
edited="list_rev_M2_frame_list_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.54"/>
<result status="valid" time="0.48"/>
</proof>
</goal>
<goal
......@@ -228,7 +228,7 @@
edited="list_rev_M2_frame_list_ft_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.53"/>
<result status="valid" time="0.49"/>
</proof>
</goal>
<goal
......@@ -253,7 +253,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="unknown" time="2.08"/>
<result status="unknown" time="2.03"/>
</proof>
<proof
prover="0"
......@@ -286,7 +286,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="10.61"/>
<result status="timeout" time="10.43"/>
</proof>
<proof
prover="0"
......@@ -294,7 +294,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="unknown" time="0.10"/>
<result status="unknown" time="0.09"/>
</proof>
</goal>
<goal
......@@ -321,10 +321,10 @@
name="frame_model"
locfile="programs/list_rev/../list_rev.mlw"
loclnum="318" loccnumb="8" loccnume="19"
sum="6a3d5c2cccf252827803b4aa8acaf712"
sum="3c9551a133d05343b883d6508da7e135"
proved="true"
expanded="true"
shape="ainfix =amodelV1V2amodelamixfix [&lt;-]V1V3V4V2Iain_ftV3alist_ftV1V2NIais_listV1V2Famodelamixfix [&lt;-]V1V3V4V2">
shape="ainfix =amodelV0V1amodelamixfix [&lt;-]V0V2V3V1Iain_ftV2alist_ftV0V1NIais_listV0V1Famodelamixfix [&lt;-]V0V2V3V1">
<proof
prover="2"
timelimit="10"
......@@ -332,14 +332,14 @@
edited="list_rev_M2_frame_model_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.55"/>
<result status="valid" time="0.52"/>
</proof>
</goal>
<goal
name="consistent_behv"
locfile="programs/list_rev/../list_rev.mlw"
loclnum="325" loccnumb="7" loccnume="22"
sum="0ee1a5bef7562af167f68d3b756f3a33"
sum="d0f358e183245bc07dcb0767cd75ff04"
proved="false"
expanded="true"
shape="fIais_listV0V2Iais_listV0V1F">
......@@ -357,7 +357,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="timeout" time="10.66"/>
<result status="timeout" time="10.78"/>
</proof>
<proof
prover="0"
......@@ -373,7 +373,7 @@
locfile="programs/list_rev/../list_rev.mlw"
loclnum="328" loccnumb="6" loccnume="19"
expl="parameter list_rev_behv"
sum="929100a38875e7bf21b1cbb9994820a5"
sum="fd17422e7e18ac48cf85d4e677d301a5"
proved="true"
expanded="true"
shape="iainfix =V3anullNainfix =areverseamodelV1V0ainfix ++areverseamodelV5V7amodelV5V6Aasep_list_listV5V7V6Aais_listV5V6Aais_listV5V7Iainfix =V7amixfix []V4V3FIainfix =V6V3FIainfix =V5amixfix [&lt;-]V4V3V2Fainfix =areverseamodelV1V0amodelV4V2Aais_listV4V2Iainfix =areverseamodelV1V0ainfix ++areverseamodelV4V3amodelV4V2Aasep_list_listV4V3V2Aais_listV4V2Aais_listV4V3FAainfix =areverseamodelV1V0ainfix ++areverseamodelV1V0amodelV1anullAasep_list_listV1V0anullAais_listV1anullAais_listV1V0Iais_listV1V0F">
......@@ -385,7 +385,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="2.16"/>
<result status="valid" time="2.26"/>
</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="tests-provers/coq-interval/why3session.xml" shape_version="2">
<prover
......@@ -20,7 +20,7 @@
name="pow_eps2_max_int"
locfile="tests-provers/coq-interval/../coq-interval.why"
loclnum="6" loccnumb="7" loccnume="23"
sum="4e16499348739c5249b66daa996cb549"
sum="af4e3aae419b8421e306b6c39490401a"
proved="true"
expanded="true"
shape="ainfix &lt;=apowerainfix +c1.0ainfix +c0x7.p-50c0x3.p-53c2147483647c2.0">
......@@ -31,7 +31,7 @@
edited="coqmninterval_P_pow_eps2_max_int_1.v"
obsolete="false"
archived="false">
<result status="valid" time="2.45"/>
<result status="valid" time="2.35"/>
</proof>
</goal>
</theory>
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment