updated proof session

parent cb031468
...@@ -21,6 +21,10 @@ ...@@ -21,6 +21,10 @@
id="4" id="4"
name="Z3" name="Z3"
version="2.19"/> version="2.19"/>
<prover
id="5"
name="Z3"
version="4.3.1"/>
<file <file
name="../gcd.mlw" name="../gcd.mlw"
verified="true" verified="true"
...@@ -214,7 +218,7 @@ ...@@ -214,7 +218,7 @@
expl="1. loop invariant init" expl="1. loop invariant init"
sum="5a2214a241ef5919406e1dce9fab47c1" sum="5a2214a241ef5919406e1dce9fab47c1"
proved="true" proved="true"
expanded="false" expanded="true"
shape="loop invariant initainfix &gt;=V1c0Aainfix &gt;=V0c0Iainfix &gt;=V1c0Aainfix &gt;=V0c0F"> shape="loop invariant initainfix &gt;=V1c0Aainfix &gt;=V0c0Iainfix &gt;=V1c0Aainfix &gt;=V0c0F">
<label <label
name="expl:VC for gcd"/> name="expl:VC for gcd"/>
...@@ -234,7 +238,7 @@ ...@@ -234,7 +238,7 @@
expl="2. loop invariant init" expl="2. loop invariant init"
sum="8d426254805264123885c5a7e67d38d2" sum="8d426254805264123885c5a7e67d38d2"
proved="true" proved="true"
expanded="false" expanded="true"
shape="loop invariant initainfix =agcdV0V1agcdV0V1Iainfix &gt;=V1c0Aainfix &gt;=V0c0F"> shape="loop invariant initainfix =agcdV0V1agcdV0V1Iainfix &gt;=V1c0Aainfix &gt;=V0c0F">
<label <label
name="expl:VC for gcd"/> name="expl:VC for gcd"/>
...@@ -254,7 +258,7 @@ ...@@ -254,7 +258,7 @@
expl="3. loop invariant preservation" expl="3. loop invariant preservation"
sum="fc2460530d56c590dbcaa039058e38eb" sum="fc2460530d56c590dbcaa039058e38eb"
proved="true" proved="true"
expanded="false" expanded="true"
shape="loop invariant preservationainfix &gt;=V4c0Aainfix &gt;=V5c0Iainfix =V5V2FIainfix =V4amodV3V2FINainfix =V2c0Iainfix =agcdV3V2agcdV0V1Aainfix &gt;=V2c0Aainfix &gt;=V3c0FIainfix &gt;=V1c0Aainfix &gt;=V0c0F"> shape="loop invariant preservationainfix &gt;=V4c0Aainfix &gt;=V5c0Iainfix =V5V2FIainfix =V4amodV3V2FINainfix =V2c0Iainfix =agcdV3V2agcdV0V1Aainfix &gt;=V2c0Aainfix &gt;=V3c0FIainfix &gt;=V1c0Aainfix &gt;=V0c0F">
<label <label
name="expl:VC for gcd"/> name="expl:VC for gcd"/>
...@@ -274,7 +278,7 @@ ...@@ -274,7 +278,7 @@
expl="4. loop invariant preservation" expl="4. loop invariant preservation"
sum="cf776c8d21eccdc90f18c62bc0dcdf9c" sum="cf776c8d21eccdc90f18c62bc0dcdf9c"
proved="true" proved="true"
expanded="false" expanded="true"
shape="loop invariant preservationainfix =agcdV5V4agcdV0V1Iainfix =V5V2FIainfix =V4amodV3V2FINainfix =V2c0Iainfix =agcdV3V2agcdV0V1Aainfix &gt;=V2c0Aainfix &gt;=V3c0FIainfix &gt;=V1c0Aainfix &gt;=V0c0F"> shape="loop invariant preservationainfix =agcdV5V4agcdV0V1Iainfix =V5V2FIainfix =V4amodV3V2FINainfix =V2c0Iainfix =agcdV3V2agcdV0V1Aainfix &gt;=V2c0Aainfix &gt;=V3c0FIainfix &gt;=V1c0Aainfix &gt;=V0c0F">
<label <label
name="expl:VC for gcd"/> name="expl:VC for gcd"/>
...@@ -294,25 +298,25 @@ ...@@ -294,25 +298,25 @@
expl="5. loop variant decrease" expl="5. loop variant decrease"
sum="caab89302ad24174467c877c6498e3be" sum="caab89302ad24174467c877c6498e3be"
proved="true" proved="true"
expanded="false" expanded="true"
shape="loop variant decreaseainfix &lt;V4V2Aainfix &lt;=c0V2Iainfix =V5V2FIainfix =V4amodV3V2FINainfix =V2c0Iainfix =agcdV3V2agcdV0V1Aainfix &gt;=V2c0Aainfix &gt;=V3c0FIainfix &gt;=V1c0Aainfix &gt;=V0c0F"> shape="loop variant decreaseainfix &lt;V4V2Aainfix &lt;=c0V2Iainfix =V5V2FIainfix =V4amodV3V2FINainfix =V2c0Iainfix =agcdV3V2agcdV0V1Aainfix &gt;=V2c0Aainfix &gt;=V3c0FIainfix &gt;=V1c0Aainfix &gt;=V0c0F">
<label <label
name="expl:VC for gcd"/> name="expl:VC for gcd"/>
<proof <proof
prover="0" prover="2"
timelimit="10" timelimit="10"
memlimit="1000" memlimit="1000"
obsolete="false" obsolete="false"
archived="false"> archived="false">
<undone/> <result status="valid" time="0.02"/>
</proof> </proof>
<proof <proof
prover="2" prover="5"
timelimit="10" timelimit="30"
memlimit="1000" memlimit="1000"
obsolete="false" obsolete="false"
archived="false"> archived="false">
<result status="valid" time="0.02"/> <result status="valid" time="0.01"/>
</proof> </proof>
</goal> </goal>
<goal <goal
...@@ -322,7 +326,7 @@ ...@@ -322,7 +326,7 @@
expl="6. postcondition" expl="6. postcondition"
sum="1644ab1125c43173f855bc860eb6e22e" sum="1644ab1125c43173f855bc860eb6e22e"
proved="true" proved="true"
expanded="false" expanded="true"
shape="postconditionainfix =V3agcdV0V1INNainfix =V2c0Iainfix =agcdV3V2agcdV0V1Aainfix &gt;=V2c0Aainfix &gt;=V3c0FIainfix &gt;=V1c0Aainfix &gt;=V0c0F"> shape="postconditionainfix =V3agcdV0V1INNainfix =V2c0Iainfix =agcdV3V2agcdV0V1Aainfix &gt;=V2c0Aainfix &gt;=V3c0FIainfix &gt;=V1c0Aainfix &gt;=V0c0F">
<label <label
name="expl:VC for gcd"/> name="expl:VC for gcd"/>
......
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