Commit 399609b7 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

flag: updated proof session (no Z3 4.0 on moloch)

parent 07573b55
......@@ -17,10 +17,6 @@
id="3"
name="Z3"
version="2.19"/>
<prover
id="4"
name="Z3"
version="4.0"/>
<file
name="../flag.mlw"
verified="true"
......@@ -38,7 +34,7 @@
expl="VC for swap"
sum="fb5f53b55cef698d07b619225a4fa173"
proved="true"
expanded="false"
expanded="true"
shape="aexchangeV3V5V1V2Iainfix =V5asetV4V2agetV3V1FAainfix &lt;V2V0Aainfix &lt;=c0V2Iainfix =V4asetV3V1agetV3V2FAainfix &lt;V1V0Aainfix &lt;=c0V1Aainfix &lt;V2V0Aainfix &lt;=c0V2Aainfix &lt;V1V0Aainfix &lt;=c0V1Iainfix &lt;V2V0Aainfix &lt;=c0V2Aainfix &lt;V1V0Aainfix &lt;=c0V1FF">
<label
name="expl:VC for swap"/>
......@@ -81,7 +77,7 @@
expl="1. loop invariant init"
sum="03b07c1e7cbebdb41c9953a23bfa4605"
proved="true"
expanded="false"
expanded="true"
shape="ainfix &lt;=V0V0Aainfix &lt;=c0V0Aainfix &lt;=c0c0Aainfix &lt;=c0c0Iainfix &lt;=c0V0Lamk arrayV0V1FF">
<label
name="expl:VC for dutch_flag"/>
......@@ -101,7 +97,7 @@
expl="2. loop invariant init"
sum="94eb695be8a750e37b97b4788299de8f"
proved="true"
expanded="false"
expanded="true"
shape="amonochromeV2c0c0aBlueIainfix &lt;=c0V0Lamk arrayV0V1FF">
<label
name="expl:VC for dutch_flag"/>
......@@ -121,7 +117,7 @@
expl="3. loop invariant init"
sum="0e500e39f4b7b10d789318c02d190785"
proved="true"
expanded="false"
expanded="true"
shape="amonochromeV2c0c0aWhiteIainfix &lt;=c0V0Lamk arrayV0V1FF">
<label
name="expl:VC for dutch_flag"/>
......@@ -141,7 +137,7 @@
expl="4. loop invariant init"
sum="5ba0dc59c0fd910eff2768e31edf9a80"
proved="true"
expanded="false"
expanded="true"
shape="amonochromeV2V0V0aRedIainfix &lt;=c0V0Lamk arrayV0V1FF">
<label
name="expl:VC for dutch_flag"/>
......@@ -161,7 +157,7 @@
expl="5. loop invariant init"
sum="dbebb96b18bc6b57481a7ce078a6ad27"
proved="true"
expanded="false"
expanded="true"
shape="apermutV2V2Iainfix &lt;=c0V0Lamk arrayV0V1FF">
<label
name="expl:VC for dutch_flag"/>
......@@ -181,7 +177,7 @@
expl="6. precondition"
sum="e1a2c6c96c29aec7752f58093de9d699"
proved="true"
expanded="false"
expanded="true"
shape="ainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix &lt;V4V3IapermutV2V7AamonochromeV7V3V0aRedAamonochromeV7V5V4aWhiteAamonochromeV7c0V5aBlueAainfix &lt;=V3V0Aainfix &lt;=V4V3Aainfix &lt;=V5V4Aainfix &lt;=c0V5Lamk arrayV0V6FIainfix &lt;=c0V0Lamk arrayV0V1FF">
<label
name="expl:VC for dutch_flag"/>
......@@ -201,7 +197,7 @@
expl="7. precondition"
sum="1babbbbe7269ed54fd2f5e583a6b0f6a"
proved="true"
expanded="false"
expanded="true"
shape="CagetV6V4aBlueainfix &lt;V4V0Aainfix &lt;=c0V4Aainfix &lt;V5V0Aainfix &lt;=c0V5aWhitetaRedtIainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix &lt;V4V3IapermutV2V7AamonochromeV7V3V0aRedAamonochromeV7V5V4aWhiteAamonochromeV7c0V5aBlueAainfix &lt;=V3V0Aainfix &lt;=V4V3Aainfix &lt;=V5V4Aainfix &lt;=c0V5Lamk arrayV0V6FIainfix &lt;=c0V0Lamk arrayV0V1FF">
<label
name="expl:VC for dutch_flag"/>
......@@ -221,7 +217,7 @@
expl="8. loop invariant preservation"
sum="726fd717eed00a6f64013147484b36e4"
proved="true"
expanded="false"
expanded="true"
shape="CagetV6V4aBlueainfix &lt;=V3V0Aainfix &lt;=V11V3Aainfix &lt;=V10V11Aainfix &lt;=c0V10Iainfix =V11ainfix +V4c1FIainfix =V10ainfix +V5c1FIaexchangeV6V8V5V4Lamk arrayV0V8FIainfix &lt;V4V0Aainfix &lt;=c0V4Aainfix &lt;V5V0Aainfix &lt;=c0V5aWhitetaRedtIainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix &lt;V4V3IapermutV2V7AamonochromeV7V3V0aRedAamonochromeV7V5V4aWhiteAamonochromeV7c0V5aBlueAainfix &lt;=V3V0Aainfix &lt;=V4V3Aainfix &lt;=V5V4Aainfix &lt;=c0V5Lamk arrayV0V6FIainfix &lt;=c0V0Lamk arrayV0V1FF">
<label
name="expl:VC for dutch_flag"/>
......@@ -241,7 +237,7 @@
expl="9. loop invariant preservation"
sum="9c29ad43fb41b87122805e30ad12fec5"
proved="true"
expanded="false"
expanded="true"
shape="CagetV6V4aBlueamonochromeV9c0V10aBlueIainfix =V11ainfix +V4c1FIainfix =V10ainfix +V5c1FIaexchangeV6V8V5V4Lamk arrayV0V8FIainfix &lt;V4V0Aainfix &lt;=c0V4Aainfix &lt;V5V0Aainfix &lt;=c0V5aWhitetaRedtIainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix &lt;V4V3IapermutV2V7AamonochromeV7V3V0aRedAamonochromeV7V5V4aWhiteAamonochromeV7c0V5aBlueAainfix &lt;=V3V0Aainfix &lt;=V4V3Aainfix &lt;=V5V4Aainfix &lt;=c0V5Lamk arrayV0V6FIainfix &lt;=c0V0Lamk arrayV0V1FF">
<label
name="expl:VC for dutch_flag"/>
......@@ -261,7 +257,7 @@
expl="10. loop invariant preservation"
sum="b82262a9c5aac43f6e8e891a89450326"
proved="true"
expanded="false"
expanded="true"
shape="CagetV6V4aBlueamonochromeV9V10V11aWhiteIainfix =V11ainfix +V4c1FIainfix =V10ainfix +V5c1FIaexchangeV6V8V5V4Lamk arrayV0V8FIainfix &lt;V4V0Aainfix &lt;=c0V4Aainfix &lt;V5V0Aainfix &lt;=c0V5aWhitetaRedtIainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix &lt;V4V3IapermutV2V7AamonochromeV7V3V0aRedAamonochromeV7V5V4aWhiteAamonochromeV7c0V5aBlueAainfix &lt;=V3V0Aainfix &lt;=V4V3Aainfix &lt;=V5V4Aainfix &lt;=c0V5Lamk arrayV0V6FIainfix &lt;=c0V0Lamk arrayV0V1FF">
<label
name="expl:VC for dutch_flag"/>
......@@ -281,7 +277,7 @@
expl="11. loop invariant preservation"
sum="4022ea57fb8a0c5e2fe46da8fbae6b38"
proved="true"
expanded="false"
expanded="true"
shape="CagetV6V4aBlueamonochromeV9V3V0aRedIainfix =V11ainfix +V4c1FIainfix =V10ainfix +V5c1FIaexchangeV6V8V5V4Lamk arrayV0V8FIainfix &lt;V4V0Aainfix &lt;=c0V4Aainfix &lt;V5V0Aainfix &lt;=c0V5aWhitetaRedtIainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix &lt;V4V3IapermutV2V7AamonochromeV7V3V0aRedAamonochromeV7V5V4aWhiteAamonochromeV7c0V5aBlueAainfix &lt;=V3V0Aainfix &lt;=V4V3Aainfix &lt;=V5V4Aainfix &lt;=c0V5Lamk arrayV0V6FIainfix &lt;=c0V0Lamk arrayV0V1FF">
<label
name="expl:VC for dutch_flag"/>
......@@ -301,7 +297,7 @@
expl="12. loop invariant preservation"
sum="0a22cacd07920327300a1444e98f6309"
proved="true"
expanded="false"
expanded="true"
shape="CagetV6V4aBlueapermutV2V9Iainfix =V11ainfix +V4c1FIainfix =V10ainfix +V5c1FIaexchangeV6V8V5V4Lamk arrayV0V8FIainfix &lt;V4V0Aainfix &lt;=c0V4Aainfix &lt;V5V0Aainfix &lt;=c0V5aWhitetaRedtIainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix &lt;V4V3IapermutV2V7AamonochromeV7V3V0aRedAamonochromeV7V5V4aWhiteAamonochromeV7c0V5aBlueAainfix &lt;=V3V0Aainfix &lt;=V4V3Aainfix &lt;=V5V4Aainfix &lt;=c0V5Lamk arrayV0V6FIainfix &lt;=c0V0Lamk arrayV0V1FF">
<label
name="expl:VC for dutch_flag"/>
......@@ -321,7 +317,7 @@
expl="13. loop variant decrease"
sum="0aaed10f096b2cd99c1760b6a570a7a6"
proved="true"
expanded="false"
expanded="true"
shape="CagetV6V4aBlueainfix &lt;ainfix -V3V11ainfix -V3V4Aainfix &lt;=c0ainfix -V3V4Iainfix =V11ainfix +V4c1FIainfix =V10ainfix +V5c1FIaexchangeV6V8V5V4Lamk arrayV0V8FIainfix &lt;V4V0Aainfix &lt;=c0V4Aainfix &lt;V5V0Aainfix &lt;=c0V5aWhitetaRedtIainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix &lt;V4V3IapermutV2V7AamonochromeV7V3V0aRedAamonochromeV7V5V4aWhiteAamonochromeV7c0V5aBlueAainfix &lt;=V3V0Aainfix &lt;=V4V3Aainfix &lt;=V5V4Aainfix &lt;=c0V5Lamk arrayV0V6FIainfix &lt;=c0V0Lamk arrayV0V1FF">
<label
name="expl:VC for dutch_flag"/>
......@@ -341,7 +337,7 @@
expl="14. loop invariant preservation"
sum="2c931423105ae373ad5eff9b110af135"
proved="true"
expanded="false"
expanded="true"
shape="CagetV6V4aBluetaWhiteainfix &lt;=V3V0Aainfix &lt;=V8V3Aainfix &lt;=V5V8Aainfix &lt;=c0V5Iainfix =V8ainfix +V4c1FaRedtIainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix &lt;V4V3IapermutV2V7AamonochromeV7V3V0aRedAamonochromeV7V5V4aWhiteAamonochromeV7c0V5aBlueAainfix &lt;=V3V0Aainfix &lt;=V4V3Aainfix &lt;=V5V4Aainfix &lt;=c0V5Lamk arrayV0V6FIainfix &lt;=c0V0Lamk arrayV0V1FF">
<label
name="expl:VC for dutch_flag"/>
......@@ -361,7 +357,7 @@
expl="15. loop invariant preservation"
sum="75f619e13ac86d9480f2fc0e5f87049d"
proved="true"
expanded="false"
expanded="true"
shape="CagetV6V4aBluetaWhiteamonochromeV7c0V5aBlueIainfix =V8ainfix +V4c1FaRedtIainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix &lt;V4V3IapermutV2V7AamonochromeV7V3V0aRedAamonochromeV7V5V4aWhiteAamonochromeV7c0V5aBlueAainfix &lt;=V3V0Aainfix &lt;=V4V3Aainfix &lt;=V5V4Aainfix &lt;=c0V5Lamk arrayV0V6FIainfix &lt;=c0V0Lamk arrayV0V1FF">
<label
name="expl:VC for dutch_flag"/>
......@@ -381,7 +377,7 @@
expl="16. loop invariant preservation"
sum="0d92f8c0d40ba5d9913ff2b8a3c9eff0"
proved="true"
expanded="false"
expanded="true"
shape="CagetV6V4aBluetaWhiteamonochromeV7V5V8aWhiteIainfix =V8ainfix +V4c1FaRedtIainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix &lt;V4V3IapermutV2V7AamonochromeV7V3V0aRedAamonochromeV7V5V4aWhiteAamonochromeV7c0V5aBlueAainfix &lt;=V3V0Aainfix &lt;=V4V3Aainfix &lt;=V5V4Aainfix &lt;=c0V5Lamk arrayV0V6FIainfix &lt;=c0V0Lamk arrayV0V1FF">
<label
name="expl:VC for dutch_flag"/>
......@@ -401,7 +397,7 @@
expl="17. loop invariant preservation"
sum="b70f33af7d000eb42e528e5db53b7414"
proved="true"
expanded="false"
expanded="true"
shape="CagetV6V4aBluetaWhiteamonochromeV7V3V0aRedIainfix =V8ainfix +V4c1FaRedtIainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix &lt;V4V3IapermutV2V7AamonochromeV7V3V0aRedAamonochromeV7V5V4aWhiteAamonochromeV7c0V5aBlueAainfix &lt;=V3V0Aainfix &lt;=V4V3Aainfix &lt;=V5V4Aainfix &lt;=c0V5Lamk arrayV0V6FIainfix &lt;=c0V0Lamk arrayV0V1FF">
<label
name="expl:VC for dutch_flag"/>
......@@ -421,7 +417,7 @@
expl="18. loop invariant preservation"
sum="fd9e1055397c32b01654affde8df3729"
proved="true"
expanded="false"
expanded="true"
shape="CagetV6V4aBluetaWhiteapermutV2V7Iainfix =V8ainfix +V4c1FaRedtIainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix &lt;V4V3IapermutV2V7AamonochromeV7V3V0aRedAamonochromeV7V5V4aWhiteAamonochromeV7c0V5aBlueAainfix &lt;=V3V0Aainfix &lt;=V4V3Aainfix &lt;=V5V4Aainfix &lt;=c0V5Lamk arrayV0V6FIainfix &lt;=c0V0Lamk arrayV0V1FF">
<label
name="expl:VC for dutch_flag"/>
......@@ -441,7 +437,7 @@
expl="19. loop variant decrease"
sum="aabcccf58fb18a27316bf9ac2639ccc5"
proved="true"
expanded="false"
expanded="true"
shape="CagetV6V4aBluetaWhiteainfix &lt;ainfix -V3V8ainfix -V3V4Aainfix &lt;=c0ainfix -V3V4Iainfix =V8ainfix +V4c1FaRedtIainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix &lt;V4V3IapermutV2V7AamonochromeV7V3V0aRedAamonochromeV7V5V4aWhiteAamonochromeV7c0V5aBlueAainfix &lt;=V3V0Aainfix &lt;=V4V3Aainfix &lt;=V5V4Aainfix &lt;=c0V5Lamk arrayV0V6FIainfix &lt;=c0V0Lamk arrayV0V1FF">
<label
name="expl:VC for dutch_flag"/>
......@@ -461,7 +457,7 @@
expl="20. precondition"
sum="ea9da2e1387e190fead802db1f2d653d"
proved="true"
expanded="false"
expanded="true"
shape="CagetV6V4aBluetaWhitetaRedainfix &lt;V4V0Aainfix &lt;=c0V4Aainfix &lt;V8V0Aainfix &lt;=c0V8Iainfix =V8ainfix -V3c1FIainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix &lt;V4V3IapermutV2V7AamonochromeV7V3V0aRedAamonochromeV7V5V4aWhiteAamonochromeV7c0V5aBlueAainfix &lt;=V3V0Aainfix &lt;=V4V3Aainfix &lt;=V5V4Aainfix &lt;=c0V5Lamk arrayV0V6FIainfix &lt;=c0V0Lamk arrayV0V1FF">
<label
name="expl:VC for dutch_flag"/>
......@@ -481,7 +477,7 @@
expl="21. loop invariant preservation"
sum="af687a64ae4479fc3e00df1550550828"
proved="true"
expanded="false"
expanded="true"
shape="CagetV6V4aBluetaWhitetaRedainfix &lt;=V8V0Aainfix &lt;=V4V8Aainfix &lt;=V5V4Aainfix &lt;=c0V5IaexchangeV6V9V8V4Lamk arrayV0V9FIainfix &lt;V4V0Aainfix &lt;=c0V4Aainfix &lt;V8V0Aainfix &lt;=c0V8Iainfix =V8ainfix -V3c1FIainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix &lt;V4V3IapermutV2V7AamonochromeV7V3V0aRedAamonochromeV7V5V4aWhiteAamonochromeV7c0V5aBlueAainfix &lt;=V3V0Aainfix &lt;=V4V3Aainfix &lt;=V5V4Aainfix &lt;=c0V5Lamk arrayV0V6FIainfix &lt;=c0V0Lamk arrayV0V1FF">
<label
name="expl:VC for dutch_flag"/>
......@@ -501,7 +497,7 @@
expl="22. loop invariant preservation"
sum="f109b4e973a4417b5fdeb75d417e6ed4"
proved="true"
expanded="false"
expanded="true"
shape="CagetV6V4aBluetaWhitetaRedamonochromeV10c0V5aBlueIaexchangeV6V9V8V4Lamk arrayV0V9FIainfix &lt;V4V0Aainfix &lt;=c0V4Aainfix &lt;V8V0Aainfix &lt;=c0V8Iainfix =V8ainfix -V3c1FIainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix &lt;V4V3IapermutV2V7AamonochromeV7V3V0aRedAamonochromeV7V5V4aWhiteAamonochromeV7c0V5aBlueAainfix &lt;=V3V0Aainfix &lt;=V4V3Aainfix &lt;=V5V4Aainfix &lt;=c0V5Lamk arrayV0V6FIainfix &lt;=c0V0Lamk arrayV0V1FF">
<label
name="expl:VC for dutch_flag"/>
......@@ -521,17 +517,17 @@
expl="23. loop invariant preservation"
sum="c0f46d3621f179c846154e6c2d682c2c"
proved="true"
expanded="false"
expanded="true"
shape="CagetV6V4aBluetaWhitetaRedamonochromeV10V5V4aWhiteIaexchangeV6V9V8V4Lamk arrayV0V9FIainfix &lt;V4V0Aainfix &lt;=c0V4Aainfix &lt;V8V0Aainfix &lt;=c0V8Iainfix =V8ainfix -V3c1FIainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix &lt;V4V3IapermutV2V7AamonochromeV7V3V0aRedAamonochromeV7V5V4aWhiteAamonochromeV7c0V5aBlueAainfix &lt;=V3V0Aainfix &lt;=V4V3Aainfix &lt;=V5V4Aainfix &lt;=c0V5Lamk arrayV0V6FIainfix &lt;=c0V0Lamk arrayV0V1FF">
<label
name="expl:VC for dutch_flag"/>
<proof
prover="4"
prover="3"
timelimit="8"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.24"/>
<result status="valid" time="0.20"/>
</proof>
</goal>
<goal
......@@ -541,7 +537,7 @@
expl="24. loop invariant preservation"
sum="4f2d21ad7a8aba06e1bdd9b8a1764bac"
proved="true"
expanded="false"
expanded="true"
shape="CagetV6V4aBluetaWhitetaRedamonochromeV10V8V0aRedIaexchangeV6V9V8V4Lamk arrayV0V9FIainfix &lt;V4V0Aainfix &lt;=c0V4Aainfix &lt;V8V0Aainfix &lt;=c0V8Iainfix =V8ainfix -V3c1FIainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix &lt;V4V3IapermutV2V7AamonochromeV7V3V0aRedAamonochromeV7V5V4aWhiteAamonochromeV7c0V5aBlueAainfix &lt;=V3V0Aainfix &lt;=V4V3Aainfix &lt;=V5V4Aainfix &lt;=c0V5Lamk arrayV0V6FIainfix &lt;=c0V0Lamk arrayV0V1FF">
<label
name="expl:VC for dutch_flag"/>
......@@ -561,7 +557,7 @@
expl="25. loop invariant preservation"
sum="2926a1dbe5a2c727dcb484ebbf810f01"
proved="true"
expanded="false"
expanded="true"
shape="CagetV6V4aBluetaWhitetaRedapermutV2V10IaexchangeV6V9V8V4Lamk arrayV0V9FIainfix &lt;V4V0Aainfix &lt;=c0V4Aainfix &lt;V8V0Aainfix &lt;=c0V8Iainfix =V8ainfix -V3c1FIainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix &lt;V4V3IapermutV2V7AamonochromeV7V3V0aRedAamonochromeV7V5V4aWhiteAamonochromeV7c0V5aBlueAainfix &lt;=V3V0Aainfix &lt;=V4V3Aainfix &lt;=V5V4Aainfix &lt;=c0V5Lamk arrayV0V6FIainfix &lt;=c0V0Lamk arrayV0V1FF">
<label
name="expl:VC for dutch_flag"/>
......@@ -581,7 +577,7 @@
expl="26. loop variant decrease"
sum="c0d2118d54467659da6070dc9044e2eb"
proved="true"
expanded="false"
expanded="true"
shape="CagetV6V4aBluetaWhitetaRedainfix &lt;ainfix -V8V4ainfix -V3V4Aainfix &lt;=c0ainfix -V3V4IaexchangeV6V9V8V4Lamk arrayV0V9FIainfix &lt;V4V0Aainfix &lt;=c0V4Aainfix &lt;V8V0Aainfix &lt;=c0V8Iainfix =V8ainfix -V3c1FIainfix &lt;V4V0Aainfix &lt;=c0V4Iainfix &lt;V4V3IapermutV2V7AamonochromeV7V3V0aRedAamonochromeV7V5V4aWhiteAamonochromeV7c0V5aBlueAainfix &lt;=V3V0Aainfix &lt;=V4V3Aainfix &lt;=V5V4Aainfix &lt;=c0V5Lamk arrayV0V6FIainfix &lt;=c0V0Lamk arrayV0V1FF">
<label
name="expl:VC for dutch_flag"/>
......@@ -621,7 +617,7 @@
expl="28. postcondition"
sum="2334bcb0601bbbb3239712b1ff73bf96"
proved="true"
expanded="false"
expanded="true"
shape="apermutV2V7Iainfix &lt;V4V3NIapermutV2V7AamonochromeV7V3V0aRedAamonochromeV7V5V4aWhiteAamonochromeV7c0V5aBlueAainfix &lt;=V3V0Aainfix &lt;=V4V3Aainfix &lt;=V5V4Aainfix &lt;=c0V5Lamk arrayV0V6FIainfix &lt;=c0V0Lamk arrayV0V1FF">
<label
name="expl:VC for dutch_flag"/>
......
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