Commit d660eb09 authored by MARCHE Claude's avatar MARCHE Claude

fixed sessions

parent 553236ab
......@@ -1466,14 +1466,14 @@
expl="VC for zeckendorf_fast"
sum="0213974dd5e75f842e093303cb5b7080"
proved="true"
expanded="true"
expanded="false"
shape="iiiainfix =V0asumV5Aawfc2V5iainfix <V9V6Aainfix <=c0V6ACtaNilainfix <V4afibainfix -V12c1aConsVwV5Aainfix =ainfix +V4asumV5V0Aawfc2V5Aainfix <=V4V0Aainfix <=c0V4Aainfix <=c1V10Aainfix <=c1V11Aainfix =V10afibainfix +V9c1Aainfix <V4V10Aainfix <=afibV9V0Aainfix =V11afibV9Aainfix <=c1V9Iainfix =V11ainfix -V7V8FIainfix =V10V8FIainfix =V9ainfix -V6c1Fainfix <V15V6Aainfix <=c0V6ACtaNilainfix <V13afibainfix -V18c1aConsVwV14Aainfix =ainfix +V13asumV14V0Aawfc2V14Aainfix <=V13V0Aainfix <=c0V13Aainfix <=c1V16Aainfix <=c1V17Aainfix =V16afibainfix +V15c1Aainfix <V13V16Aainfix <=afibV15V0Aainfix =V17afibV15Aainfix <=c1V15Iainfix =V17ainfix -V7V8FIainfix =V16V8FIainfix =V15ainfix -V6c1FIainfix =V14aConsV6V5FIainfix =V13ainfix -V4V8Fainfix <=V8V4ainfix >V4c0ICtaNilainfix <V4afibainfix -V19c1aConsVwV5Aainfix =ainfix +V4asumV5V0Aawfc2V5Aainfix <=V4V0Aainfix <=c0V4Aainfix <=c1V7Aainfix <=c1V8Aainfix =V7afibainfix +V6c1Aainfix <V4V7Aainfix <=afibV6V0Aainfix =V8afibV6Aainfix <=c1V6FAainfix <ainfix -V0V3afibainfix -V1c1Aainfix =ainfix +ainfix -V0V3asumaConsV1aNilV0Aawfc2aConsV1aNilAainfix <=ainfix -V0V3V0Aainfix <=c0ainfix -V0V3Aainfix <=c1V2Aainfix <=c1V3Aainfix =V2afibainfix +V1c1Aainfix <ainfix -V0V3V2Aainfix <=afibV1V0Aainfix =V3afibV1Aainfix <=c1V1Aainfix =afibainfix +V1c1V2Aainfix <V0afibainfix +V1c1Aainfix <=afibV1V0Aainfix =V3afibV1Aainfix <=c1V3Aainfix <=c2V1ainfix <ainfix -ainfix *c2V0ainfix +V20V21ainfix -ainfix *c2V0ainfix +V3V2Aainfix <=c0ainfix -ainfix *c2V0ainfix +V3V2Aainfix <=c1V21Aainfix <=c1V20Aainfix =V21afibainfix +V22c1Aainfix <=afibV22V0Aainfix =V20afibV22Aainfix <=c1V22Iainfix =V22ainfix +V1c1FIainfix =V21ainfix +V3V2FIainfix =V20V2Fainfix <=V2V0Iainfix <=c1V2Aainfix <=c1V3Aainfix =V2afibainfix +V1c1Aainfix <=afibV1V0Aainfix =V3afibV1Aainfix <=c1V1FAainfix <=c1c1Aainfix =c1afibainfix +c1c1Aainfix <=afibc1V0Aainfix =c1afibc1Aainfix <=c1c1ainfix =V0asumV23Aawfc2V23LaNilainfix =V0c0Iainfix <=c0V0F">
<label
name="expl:VC for zeckendorf_fast"/>
<transf
name="split_goal_wp"
proved="true"
expanded="true">
expanded="false">
<goal
name="WP_parameter zeckendorf_fast.1"
locfile="../fibonacci.mlw"
......@@ -1924,11 +1924,11 @@
</proof>
<proof
prover="9"
timelimit="6"
timelimit="3"
memlimit="1000"
obsolete="true"
obsolete="false"
archived="false">
<result status="timeout" time="5.97"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
......@@ -1958,7 +1958,7 @@
expl="18. loop invariant preservation"
sum="73ae64d9e78da3167aa7f49a6b6457f6"
proved="true"
expanded="true"
expanded="false"
shape="loop invariant preservationawfc2V10Iainfix =V13ainfix -V7V8FIainfix =V12V8FIainfix =V11ainfix -V6c1FIainfix =V10aConsV6V5FIainfix =V9ainfix -V4V8FIainfix &lt;=V8V4Iainfix &gt;V4c0ICtaNilainfix &lt;V4afibainfix -V14c1aConsVwV5Aainfix =ainfix +V4asumV5V0Aawfc2V5Aainfix &lt;=V4V0Aainfix &lt;=c0V4Aainfix &lt;=c1V7Aainfix &lt;=c1V8Aainfix =V7afibainfix +V6c1Aainfix &lt;V4V7Aainfix &lt;=afibV6V0Aainfix =V8afibV6Aainfix &lt;=c1V6FIainfix =afibainfix +V1c1V2Aainfix &lt;V0afibainfix +V1c1Aainfix &lt;=afibV1V0Aainfix =V3afibV1Aainfix &lt;=c1V3Aainfix &lt;=c2V1INainfix &lt;=V2V0Iainfix &lt;=c1V2Aainfix &lt;=c1V3Aainfix =V2afibainfix +V1c1Aainfix &lt;=afibV1V0Aainfix =V3afibV1Aainfix &lt;=c1V1FINainfix =V0c0Iainfix &lt;=c0V0F">
<label
name="expl:VC for zeckendorf_fast"/>
......
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