Commit 8d900930 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

update session

parent 64120027
......@@ -2433,14 +2433,14 @@
expl="VC for downsweep"
sum="71358bf69f5a71ef175fb71cac5ebc21"
proved="true"
expanded="false"
expanded="true"
shape="iainfix >V1ainfix +V0c1ainfix =agetV13V15agetV4V15Iainfix >V15V1FAainfix =agetV13V16agetV4V16Iainfix <=V16ainfix -V0ainfix -V1V0FAapartial_sumV0V1V7V14Aapartial_sumainfix -V1adivainfix -V1V0c2V1V7V14Aapartial_sumainfix -V0adivainfix -V1V0c2V0V7V14Iainfix =agetV13V17agetV11V17Iainfix >V17V1FAainfix =agetV13V18agetV11V18Iainfix <=V18ainfix -ainfix -V1adivainfix -V1V0c2ainfix -V1ainfix -V1adivainfix -V1V0c2FAapartial_sumainfix -V1adivainfix -V1V0c2V1V7V14Aainfix <=c0V3Lamk arrayV3V13FAaphase1ainfix -V1adivainfix -V1V0c2V1V7V12Aainfix =agetV11V1asumV5c0ainfix +ainfix -ainfix -V1adivainfix -V1V0c2ainfix -V1ainfix -V1adivainfix -V1V0c2c1Aais_power_of_2ainfix -V1ainfix -V1adivainfix -V1V0c2Aainfix <=aprefix -c1ainfix -ainfix -V1adivainfix -V1V0c2ainfix -V1ainfix -V1adivainfix -V1V0c2Aainfix <V1V3Aainfix <ainfix -V1adivainfix -V1V0c2V1Aainfix <=c0ainfix -V1adivainfix -V1V0c2Iainfix =agetV11V19agetV9V19Iainfix >V19V0FAainfix =agetV11V20agetV9V20Iainfix <=V20ainfix -ainfix -V0adivainfix -V1V0c2ainfix -V0ainfix -V0adivainfix -V1V0c2FAapartial_sumainfix -V0adivainfix -V1V0c2V0V7V12Aainfix <=c0V3Lamk arrayV3V11FAaphase1ainfix -V0adivainfix -V1V0c2V0V7V10Aainfix =agetV9V0asumV5c0ainfix +ainfix -ainfix -V0adivainfix -V1V0c2ainfix -V0ainfix -V0adivainfix -V1V0c2c1Aais_power_of_2ainfix -V0ainfix -V0adivainfix -V1V0c2Aainfix <=aprefix -c1ainfix -ainfix -V0adivainfix -V1V0c2ainfix -V0ainfix -V0adivainfix -V1V0c2Aainfix <V0V3Aainfix <ainfix -V0adivainfix -V1V0c2V0Aainfix <=c0ainfix -V0adivainfix -V1V0c2Aaphase1ago_rightV0V1V1V7V10Aaphase1ago_rightV0V1V1V7V6Aaphase1ago_leftV0V1V0V7V6ainfix =agetV9V21agetV4V21Iainfix >V21V1FAainfix =agetV9V22agetV4V22Iainfix <=V22ainfix -V0ainfix -V1V0FAapartial_sumV0V1V7V10Aainfix =agetV9V1asumV5c0ainfix +V0c1Iainfix =V9asetV8V0agetV4V1Aainfix <=c0V3Lamk arrayV3V9FAainfix <V0V3Aainfix <=c0V0Iainfix =V8asetV4V1ainfix +agetV4V1agetV4V0Aainfix <=c0V3FAainfix <V1V3Aainfix <=c0V1Aainfix <V1V3Aainfix <=c0V1Aainfix <V0V3Aainfix <=c0V0Aainfix =agetV4V0asumV5ainfix +ainfix -V0ainfix -V1V0c1ainfix +V0c1Aainfix =agetV4V1asumV5c0ainfix +ainfix -V0ainfix -V1V0c1Aainfix <V1V3Aainfix <=c0V1Iaphase1V0V1V7V6Aainfix =agetV4V1asumV5c0ainfix +ainfix -V0ainfix -V1V0c1Aais_power_of_2ainfix -V1V0Aainfix <=aprefix -c1ainfix -V0ainfix -V1V0Aainfix <V1V3Aainfix <V0V1Aainfix <=c0V0Aainfix <=c0V3Aainfix <=c0V2Lamk arrayV2V5Lamk arrayV3V4FF">
<label
name="expl:VC for downsweep"/>
<transf
name="split_goal_wp"
proved="true"
expanded="false">
expanded="true">
<goal
name="WP_parameter downsweep.1"
locfile="../verifythis_PrefixSumRec.mlw"
......@@ -4632,7 +4632,7 @@
expl="27. postcondition"
sum="95bb4075e904f1c2570c1df322e70256"
proved="true"
expanded="false"
expanded="true"
shape="apartial_sumV0V1V7V10Iainfix &gt;V1ainfix +V0c1NIainfix =agetV9V1asumV5c0ainfix +V0c1Iainfix =V9asetV8V0agetV4V1Aainfix &lt;=c0V3Lamk arrayV3V9FIainfix &lt;V0V3Aainfix &lt;=c0V0Iainfix =V8asetV4V1ainfix +agetV4V1agetV4V0Aainfix &lt;=c0V3FIainfix &lt;V1V3Aainfix &lt;=c0V1Iainfix &lt;V1V3Aainfix &lt;=c0V1Iainfix &lt;V0V3Aainfix &lt;=c0V0Iainfix =agetV4V0asumV5ainfix +ainfix -V0ainfix -V1V0c1ainfix +V0c1Iainfix =agetV4V1asumV5c0ainfix +ainfix -V0ainfix -V1V0c1Iainfix &lt;V1V3Aainfix &lt;=c0V1Iaphase1V0V1V7V6Aainfix =agetV4V1asumV5c0ainfix +ainfix -V0ainfix -V1V0c1Aais_power_of_2ainfix -V1V0Aainfix &lt;=aprefix -c1ainfix -V0ainfix -V1V0Aainfix &lt;V1V3Aainfix &lt;V0V1Aainfix &lt;=c0V0Aainfix &lt;=c0V3Aainfix &lt;=c0V2Lamk arrayV2V5Lamk arrayV3V4FF">
<label
name="expl:VC for downsweep"/>
......@@ -4694,11 +4694,11 @@
</proof>
<proof
prover="8"
timelimit="10"
memlimit="1000"
timelimit="15"
memlimit="4000"
obsolete="false"
archived="false">
<result status="timeout" time="10.10"/>
<result status="valid" time="8.87"/>
</proof>
<proof
prover="9"
......
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