Commit 75871d67 authored by Asma Tafat-Bouzid's avatar Asma Tafat-Bouzid
Browse files

update proofs

parent 9127530d
......@@ -26,10 +26,6 @@
id="5"
name="Z3"
version="3.2"/>
<prover
id="6"
name="veriT"
version="dev"/>
<file
name="../blocking_semantics2.mlw"
verified="false"
......@@ -39,14 +35,14 @@
locfile="blocking_semantics2/../blocking_semantics2.mlw"
loclnum="6" loccnumb="7" loccnume="14"
verified="false"
expanded="false">
expanded="true">
<goal
name="get_stack_eq"
locfile="blocking_semantics2/../blocking_semantics2.mlw"
loclnum="197" loccnumb="6" loccnume="18"
sum="316bb13c7b39a24b4575df7480151f7b"
proved="true"
expanded="false"
expanded="true"
shape="ainfix =aget_stackV0aConsaTuple2V0V1V2V1F">
<proof
prover="0"
......@@ -63,7 +59,7 @@
loclnum="201" loccnumb="6" loccnume="19"
sum="30ec5f4e42a1df986a85720287b6da5b"
proved="true"
expanded="false"
expanded="true"
shape="ainfix =aget_stackV1aConsaTuple2V0V2V3aget_stackV1V3Iainfix =V0V1NF">
<proof
prover="0"
......@@ -80,7 +76,7 @@
loclnum="269" loccnumb="6" loccnume="22"
sum="5414c32f6343d5437b3ee28b23b0ff2c"
proved="false"
expanded="false"
expanded="true"
shape="ainfix =aeval_termV0V1amsubst_termV2V3V4aeval_termasetV0V3aget_stackV4V1V1V2Iafresh_in_termV4V2F">
<proof
prover="4"
......@@ -106,14 +102,6 @@
archived="false">
<result status="unknown" time="0.18"/>
</proof>
<proof
prover="6"
timelimit="3"
memlimit="0"
obsolete="false"
archived="false">
<result status="failure" time="0.00"/>
</proof>
<proof
prover="2"
timelimit="3"
......@@ -137,7 +125,7 @@
loclnum="275" loccnumb="6" loccnume="21"
sum="059dc8e4613b9c79d7c5b0e19d707211"
proved="false"
expanded="false"
expanded="true"
shape="ainfix =aeval_termV0V1asubst_termV2V3V4aeval_termV0aConsaTuple2V3aget_stackV4V1V1V2Iafresh_in_termV4V2F">
<proof
prover="4"
......@@ -163,14 +151,6 @@
archived="false">
<result status="unknown" time="1.90"/>
</proof>
<proof
prover="6"
timelimit="3"
memlimit="0"
obsolete="false"
archived="false">
<result status="failure" time="0.00"/>
</proof>
<proof
prover="2"
timelimit="3"
......@@ -194,7 +174,7 @@
loclnum="281" loccnumb="6" loccnume="27"
sum="2c690fdc6b891ab883aa79fe49ded02b"
proved="false"
expanded="false"
expanded="true"
shape="ainfix =aeval_termV1aConsaTuple2V3V4V2V0aeval_termV1V2V0Iafresh_in_termV3V0F">
<proof
prover="4"
......@@ -220,14 +200,6 @@
archived="false">
<result status="unknown" time="1.63"/>
</proof>
<proof
prover="6"
timelimit="3"
memlimit="0"
obsolete="false"
archived="false">
<result status="failure" time="0.00"/>
</proof>
<proof
prover="2"
timelimit="3"
......@@ -251,7 +223,7 @@
loclnum="316" loccnumb="6" loccnume="17"
sum="de2ee05fc1df247bfe6c620e293e6c28"
proved="false"
expanded="false"
expanded="true"
shape="ainfix =asubstV0V1V2V0Iafresh_in_fmlaV1V0F">
<proof
prover="4"
......@@ -277,14 +249,6 @@
archived="false">
<result status="unknown" time="0.04"/>
</proof>
<proof
prover="6"
timelimit="3"
memlimit="0"
obsolete="false"
archived="false">
<result status="failure" time="0.00"/>
</proof>
<proof
prover="2"
timelimit="3"
......@@ -308,7 +272,7 @@
loclnum="320" loccnumb="6" loccnume="15"
sum="e4d4949f6f877465f3b8a21941bd7426"
proved="true"
expanded="false"
expanded="true"
shape="ainfix =amsubstaFletV2V0V1V4V3aFletV2amsubst_termV0V4V3amsubstV1V4V3F">
<proof
prover="0"
......@@ -334,7 +298,7 @@
loclnum="330" loccnumb="6" loccnume="16"
sum="496d1bae09ed0f0c318d40578ed3daf8"
proved="false"
expanded="false"
expanded="true"
shape="aeval_fmlaV1aConsaTuple2V3aget_stackV4V2V2V0qaeval_fmlaV1V2asubstV0V3V4Iafresh_in_fmlaV4V0F">
<proof
prover="4"
......@@ -360,14 +324,6 @@
archived="false">
<result status="unknown" time="0.09"/>
</proof>
<proof
prover="6"
timelimit="3"
memlimit="0"
obsolete="true"
archived="false">
<result status="failure" time="0.00"/>
</proof>
<proof
prover="2"
timelimit="3"
......@@ -391,7 +347,7 @@
loclnum="336" loccnumb="6" loccnume="15"
sum="9bb7a5da2751671b824a1cb3722be0be"
proved="false"
expanded="false"
expanded="true"
shape="aeval_fmlaV1aConsaTuple2V4V6aConsaTuple2V3V5V2V0qaeval_fmlaV1aConsaTuple2V3V5aConsaTuple2V4V6V2V0Iainfix =V3V4NF">
<proof
prover="4"
......@@ -417,14 +373,6 @@
archived="false">
<result status="timeout" time="3.04"/>
</proof>
<proof
prover="6"
timelimit="3"
memlimit="0"
obsolete="true"
archived="false">
<result status="failure" time="0.00"/>
</proof>
<proof
prover="2"
timelimit="3"
......@@ -457,7 +405,7 @@
loclnum="347" loccnumb="6" loccnume="22"
sum="905040776f511369692f1102a8eb9890"
proved="false"
expanded="false"
expanded="true"
shape="aeval_fmlaV1V2V0qaeval_fmlaV1aConsaTuple2V3V4V2V0Iafresh_in_fmlaV3V0F">
<proof
prover="4"
......@@ -483,14 +431,6 @@
archived="false">
<result status="unknown" time="1.40"/>
</proof>
<proof
prover="6"
timelimit="3"
memlimit="0"
obsolete="true"
archived="false">
<result status="failure" time="0.00"/>
</proof>
<proof
prover="2"
timelimit="3"
......@@ -514,7 +454,7 @@
loclnum="357" loccnumb="6" loccnume="15"
sum="4f8b0e3409ab567861133ea77a79bd7d"
proved="false"
expanded="false"
expanded="true"
shape="aeval_fmlaV4V5aFletV0V2V3Iaeval_fmlaV4V5aFletV1V2asubstV3V0V1Iafresh_in_fmlaV1V3FF">
<proof
prover="4"
......@@ -540,14 +480,6 @@
archived="false">
<result status="timeout" time="3.08"/>
</proof>
<proof
prover="6"
timelimit="3"
memlimit="0"
obsolete="true"
archived="false">
<result status="failure" time="0.00"/>
</proof>
<proof
prover="2"
timelimit="3"
......@@ -589,7 +521,7 @@
loclnum="486" loccnumb="8" loccnume="21"
sum="f98b4dac31bc6d16ca70619c65a99f12"
proved="false"
expanded="false"
expanded="true"
shape="ainfix &gt;=V6c0Iamany_stepsV0V2V4V1V3V5V6F">
<proof
prover="4"
......@@ -615,14 +547,6 @@
archived="false">
<result status="timeout" time="3.03"/>
</proof>
<proof
prover="6"
timelimit="3"
memlimit="0"
obsolete="true"
archived="false">
<result status="failure" time="0.00"/>
</proof>
<proof
prover="2"
timelimit="3"
......@@ -646,7 +570,7 @@
loclnum="490" loccnumb="8" loccnume="22"
sum="3c1eaad9e29116e132c7dbdee9e26152"
proved="false"
expanded="false"
expanded="true"
shape="ainfix =V6ainfix +ainfix +c1V9V10Aamany_stepsV7V8V5V1V3avoidV10Aamany_stepsV0V2V4V7V8avoidV9EIamany_stepsV0V2aEseqV4V5V1V3avoidV6F">
<proof
prover="4"
......@@ -672,14 +596,6 @@
archived="false">
<result status="timeout" time="3.06"/>
</proof>
<proof
prover="6"
timelimit="3"
memlimit="0"
obsolete="true"
archived="false">
<result status="failure" time="0.00"/>
</proof>
<proof
prover="2"
timelimit="3"
......@@ -703,7 +619,7 @@
loclnum="498" loccnumb="8" loccnume="22"
sum="72f382b8d8227d911b0522449b88f3f2"
proved="false"
expanded="false"
expanded="true"
shape="ainfix =V8ainfix +ainfix +c1V12V13Aamany_stepsV9aConsaTuple2V4V11V10V6V1V3aEvalueV7V13Aamany_stepsV0V2V5V9V10aEvalueV11V12EIamany_stepsV0V2aEletV4V5V6V1V3aEvalueV7V8F">
<proof
prover="4"
......@@ -729,14 +645,6 @@
archived="false">
<result status="timeout" time="3.01"/>
</proof>
<proof
prover="6"
timelimit="3"
memlimit="0"
obsolete="true"
archived="false">
<result status="failure" time="0.00"/>
</proof>
<proof
prover="2"
timelimit="3"
......@@ -760,7 +668,7 @@
loclnum="506" loccnumb="7" loccnume="27"
sum="723c088314f59a3676c5d9540ecc8b24"
proved="false"
expanded="false"
expanded="true"
shape="aone_stepV2V4V0V3V5V1Iaone_stepV2aConsaTuple2V6V7V4V0V3V5V1Iafresh_in_exprV6V0F">
<proof
prover="4"
......@@ -786,14 +694,6 @@
archived="false">
<result status="unknown" time="2.24"/>
</proof>
<proof
prover="6"
timelimit="3"
memlimit="0"
obsolete="true"
archived="false">
<result status="failure" time="0.00"/>
</proof>
<proof
prover="2"
timelimit="3"
......@@ -817,14 +717,14 @@
locfile="blocking_semantics2/../blocking_semantics2.mlw"
loclnum="533" loccnumb="7" loccnume="20"
verified="false"
expanded="false">
expanded="true">
<goal
name="Test13"
locfile="blocking_semantics2/../blocking_semantics2.mlw"
loclnum="543" loccnumb="5" loccnume="11"
sum="c05090723c2cdddc3b46c2b7090e09b8"
proved="true"
expanded="false"
expanded="true"
shape="ainfix =aeval_termamy_sigmaamy_piaTvalueaVintc13aVintc13">
<proof
prover="0"
......@@ -841,7 +741,7 @@
loclnum="546" loccnumb="5" loccnume="15"
sum="bd23f1bb2dc17b73ed25e172288d1ff3"
proved="true"
expanded="false"
expanded="true"
shape="amany_stepsamy_sigmaamy_piaEvalueaVintc13amy_sigmaamy_piaEvalueaVintc13c0">
<proof
prover="0"
......@@ -858,7 +758,7 @@
loclnum="549" loccnumb="5" loccnume="11"
sum="8c224a217b52482dede7f7637eef716d"
proved="true"
expanded="false"
expanded="true"
shape="ainfix =aeval_termamy_sigmaamy_piaTvaraxaVintc42">
<proof
prover="0"
......@@ -875,7 +775,7 @@
loclnum="552" loccnumb="5" loccnume="15"
sum="170acecd7b1dfbd712689c42b3a6ee0d"
proved="false"
expanded="false"
expanded="true"
shape="amany_stepsamy_sigmaamy_piaEvaraxamy_sigmaamy_piaEvalueaVintc42c1">
<proof
prover="0"
......@@ -892,7 +792,7 @@
loclnum="555" loccnumb="5" loccnume="10"
sum="8cdc3ff1aeafd6a06fc44eca79be7f17"
proved="true"
expanded="false"
expanded="true"
shape="ainfix =aeval_termamy_sigmaamy_piaTderefayaVintc0">
<proof
prover="0"
......@@ -909,7 +809,7 @@
loclnum="558" loccnumb="5" loccnume="14"
sum="092b55df3f218c3f4e5d7ec5eb7f4ce8"
proved="false"
expanded="false"
expanded="true"
shape="amany_stepsamy_sigmaamy_piaEderefayamy_sigmaamy_piaEvalueaVintc0c1">
<proof
prover="0"
......@@ -926,7 +826,7 @@
loclnum="561" loccnumb="5" loccnume="11"
sum="5b1b8b973239ae804cc006005a487e83"
proved="false"
expanded="false"
expanded="true"
shape="ainfix =aeval_termamy_sigmaamy_piaTbinaTvaraxaOplusaTvalueaVintc13aVintc55">
<proof
prover="0"
......@@ -943,7 +843,7 @@
loclnum="564" loccnumb="5" loccnume="15"
sum="d8ef82747afd38232a293752769e5f8c"
proved="false"
expanded="false"
expanded="true"
shape="amany_stepsamy_sigmaamy_piaEbinaEvaraxaOplusaEvalueaVintc13amy_sigmaamy_piaEvalueaVintc55c2">
<proof
prover="0"
......@@ -960,7 +860,7 @@
loclnum="567" loccnumb="5" loccnume="10"
sum="832e1ddbf46383da65ff91f45474990d"
proved="true"
expanded="false"
expanded="true"
shape="ainfix =agetV0ayaVintc42Iaone_stepamy_sigmaamy_piaEassignayaEvalueaVintc42V0V1avoidF">
<proof
prover="0"
......@@ -977,7 +877,7 @@
loclnum="572" loccnumb="5" loccnume="9"
sum="dca0c1b3441c53cbd3e815f53b8ff040"
proved="false"
expanded="false"
expanded="true"
shape="ainfix =agetV1ayaVintc13Iaone_stepV0V2V4V1V3avoidIaone_stepamy_sigmaamy_piaEifaEbinaEderefayaOleaEvalueaVintc10aEassignayaEvalueaVintc13aEassignayaEvalueaVintc42V0V2V4F">
<proof
prover="0"
......@@ -994,14 +894,14 @@
locfile="blocking_semantics2/../blocking_semantics2.mlw"
loclnum="586" loccnumb="7" loccnume="17"
verified="false"
expanded="false">
expanded="true">
<goal
name="consequence_rule"
locfile="blocking_semantics2/../blocking_semantics2.mlw"
loclnum="593" loccnumb="6" loccnume="22"
sum="484768bc758918deb32617126cc7b287"
proved="false"
expanded="false"
expanded="true"
shape="avalid_tripleV1V4V3Iavalid_fmlaaFimpliesV2V3Iavalid_tripleV0V4V2Iavalid_fmlaaFimpliesV1V0F">
<proof
prover="0"
......@@ -1018,7 +918,7 @@
loclnum="600" loccnumb="6" loccnume="16"
sum="c8882ad8152643850a22c5110ae47352"
proved="false"
expanded="false"
expanded="true"
shape="avalid_tripleV0aEvalueV1V0Iafresh_in_fmlaaresultV0F">
<proof
prover="0"
......@@ -1035,7 +935,7 @@
loclnum="604" loccnumb="6" loccnume="17"
sum="ff610019c40923cca3ad9e3f2340e5a8"
proved="false"
expanded="false"
expanded="true"
shape="avalid_tripleV0aEassignV2V3V1Iavalid_tripleV0V3amsubstV1V2aresultF">
<proof
prover="0"
......@@ -1052,7 +952,7 @@
loclnum="609" loccnumb="6" loccnume="14"
sum="8662fdc8b3bd896db38f9b0905a2d85a"
proved="false"
expanded="false"
expanded="true"
shape="avalid_tripleV0aEseqV3V4V1Iavalid_tripleV2V4V1Aavalid_tripleV0V3V2F">
<proof
prover="0"
......@@ -1069,7 +969,7 @@
loclnum="614" loccnumb="6" loccnume="14"
sum="04118ff15decf9ea6dda00ce568499e5"
proved="false"
expanded="false"
expanded="true"
shape="avalid_tripleV0aEletV3V4V5V1Iavalid_tripleaFletaresultaTvarV3V2V5V1Aavalid_tripleV0V4V2Iafresh_in_fmlaV3V2Iainfix =V3aresultNF">
<proof
prover="0"
......@@ -1086,7 +986,7 @@
loclnum="628" loccnumb="6" loccnume="17"
sum="935028019b27c3f255df3d6bdd5be4a3"
proved="false"
expanded="false"
expanded="true"
shape="avalid_tripleV1aEassertV0V1Iavalid_fmlaaFimpliesV1V0F">
<proof
prover="0"
......@@ -1103,7 +1003,7 @@
loclnum="632" loccnumb="6" loccnume="21"
sum="aff92d287559312bc82f1a5261d2bfc9"
proved="false"
expanded="false"
expanded="true"
shape="avalid_tripleaFimpliesV0V1aEassertV0V1F">
<proof
prover="0"
......@@ -1120,14 +1020,14 @@
locfile="blocking_semantics2/../blocking_semantics2.mlw"
loclnum="653" loccnumb="7" loccnume="22"
verified="true"
expanded="false">
expanded="true">
<goal
name="simpl_tautology"
locfile="blocking_semantics2/../blocking_semantics2.mlw"
loclnum="658" loccnumb="8" loccnume="23"
sum="4e337593f2731debe350aaa609d33d2d"
proved="true"
expanded="false"
expanded="true"
shape="apqaqAapqaqIap">
<proof
prover="0"
......@@ -1151,7 +1051,7 @@
loclnum="679" loccnumb="6" loccnume="18"
sum="cb3b9ee43d4813229a150613db5c2eb6"
proved="true"
expanded="false"
expanded="true"
shape="aassignsV0V1V0F">
<proof
prover="0"
......@@ -1168,7 +1068,7 @@
loclnum="682" loccnumb="6" loccnume="19"
sum="93311d663dd417149055125ce6dff7f0"
proved="true"
expanded="false"
expanded="true"
shape="aassignsV0V3V2IaassignsV1V3V2AaassignsV0V3V1F">
<proof
prover="0"
......@@ -1185,7 +1085,7 @@
loclnum="687" loccnumb="6" loccnume="24"
sum="fca1a52de8d38c567078c7ff3b1a4092"
proved="true"
expanded="false"
expanded="true"
shape="aassignsV0aunionV2V3V1IaassignsV0V2V1F">
<proof
prover="0"
......@@ -1202,7 +1102,7 @@
loclnum="691" loccnumb="6" loccnume="25"
sum="ca302b6e3b90010c5c67f51beae295a8"
proved="true"
expanded="false"
expanded="true"
shape="aassignsV0aunionV2V3V1IaassignsV0V3V1F">
<proof
prover="0"
......@@ -1272,7 +1172,7 @@
loclnum="787" loccnumb="8" loccnume="20"
sum="2d0b6f44baaa00612a42f9f3542a7008"
proved="true"
expanded="false"
expanded="true"
shape="ainfix =V0aEvalueV1EOais_valueV0NF">
<proof
prover="1"
......@@ -1297,7 +1197,7 @@
loclnum="790" loccnumb="8" loccnume="18"
sum="231765b0df9f9cabcd6ff9691475f6eb"
proved="true"
expanded="false"
expanded="true"
shape="ainfix =V0aVboolaTrueOainfix =V0aVboolaFalseIatype_exprV1V2aEvalueV0aTYboolF">
<proof
prover="3"
......@@ -1315,7 +1215,7 @@
loclnum="795" loccnumb="8" loccnume="18"
sum="f005480f6439168a078df4a297dce627"
proved="true"
expanded="false"
expanded="true"
shape="ainfix =V0aVvoidIatype_exprV1V2aEvalueV0aTYunitF">
<proof
prover="1"
......
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