diff --git a/examples/hashtbl_impl/why3session.xml b/examples/hashtbl_impl/why3session.xml index 6dc7577fba15702ab297be2d19a18f16b2d7d73b..3cff427620ab244162de8f9b8d69549daf152522 100644 --- a/examples/hashtbl_impl/why3session.xml +++ b/examples/hashtbl_impl/why3session.xml @@ -23,13 +23,13 @@ version="4.3.1"/> <file name="../hashtbl_impl.mlw" - verified="false" + verified="true" expanded="true"> <theory name="HashtblImpl" locfile="../hashtbl_impl.mlw" loclnum="1" loccnumb="7" loccnume="18" - verified="false" + verified="true" expanded="true"> <goal name="bucket_bounds" @@ -94,14 +94,14 @@ loclnum="56" loccnumb="6" loccnume="12" expl="VC for resize" sum="5e8dd7b81fdd5d34491f9c9c2a1c85b1" - proved="false" + proved="true" expanded="false" shape="ainfix <=c0V6Aagood_dataV8V9V0amk arrayV6V7FAagood_hashamk arrayV6V7V10Iainfix <V10V6Aainfix <=c0V10FAainfix <c0V6Iainfix =V7V4Aainfix =V6ainfix +ainfix *c2V1c1FIiainfix <abucketV11V1ainfix +ainfix -V1c1c1Aainfix <=c0abucketV11V1agood_dataV11V12V0V5ain_dataV11V12V5NFAagood_hashV5V13Iainfix <V13ainfix +ainfix *c2V1c1Aainfix <=c0V13FAiainfix <abucketV18V1ainfix +V14c1Aainfix <=c0abucketV18V1agood_dataV18V19V0V17ain_dataV18V19V17NFAagood_hashV17V20Iainfix <V20ainfix +ainfix *c2V1c1Aainfix <=c0V20FIiainfix <=abucketV21V1V14Aainfix <=c0abucketV21V1agood_dataV21V22V0V17ain_dataV21V22V17NFAagood_hashV17V23Iainfix <V23ainfix +ainfix *c2V1c1Aainfix <=c0V23FAainfix <=c0ainfix +ainfix *c2V1c1Lamk arrayainfix +ainfix *c2V1c1V16FAiainfix <abucketV24V1V14Aainfix <=c0abucketV24V1agood_dataV24V25V0V5iainfix =abucketV24V1V14ain_dataV24V25V5OamemaTuple2V24V25V15qainfix =agetV0V24aSomeV25ain_dataV24V25V5NFAagood_hashV5V26Iainfix <V26ainfix +ainfix *c2V1c1Aainfix <=c0V26FAainfix =abucketV27V1V14IamemaTuple2V27V28V15FAainfix <=c0ainfix +ainfix *c2V1c1LagetV2V14Aainfix <V14V1Aainfix <=c0V14Iiainfix <abucketV29V1V14Aainfix <=c0abucketV29V1agood_dataV29V30V0V5ain_dataV29V30V5NFAagood_hashV5V31Iainfix <V31ainfix +ainfix *c2V1c1Aainfix <=c0V31FIainfix <=V14ainfix -V1c1Aainfix <=c0V14FLamk arrayainfix +ainfix *c2V1c1V4FAiainfix <abucketV32V1c0Aainfix <=c0abucketV32V1agood_dataV32V33V0V3ain_dataV32V33V3NFAagood_hashV3V34Iainfix <V34ainfix +ainfix *c2V1c1Aainfix <=c0V34FIainfix <=c0ainfix -V1c1Aainfix <=c0V35Aagood_dataV37V38V0amk arrayV35V36FAagood_hashamk arrayV35V36V39Iainfix <V39V35Aainfix <=c0V39FAainfix <c0V35Iainfix =V36aconstaNilAainfix =V35ainfix +ainfix *c2V1c1FIainfix >c0ainfix -V1c1ACV41aNiliainfix <=abucketV47V1V40Aainfix <=c0abucketV47V1agood_dataV47V48V43V46ain_dataV47V48V46NFAagood_hashV46V49Iainfix <V49ainfix +ainfix *c2V1c1Aainfix <=c0V49FaConsaTuple2VVViainfix <=abucketV57V1V40Aainfix <=c0abucketV57V1agood_dataV57V58V43V56ain_dataV57V58V56NFAagood_hashV56V59Iainfix <V59ainfix +ainfix *c2V1c1Aainfix <=c0V59FIiainfix <=abucketV60V1V40Aainfix <=c0abucketV60V1agood_dataV60V61V43V56ain_dataV60V61V56NFAagood_hashV56V62Iainfix <V62ainfix +ainfix *c2V1c1Aainfix <=c0V62FAainfix <=c0ainfix +ainfix *c2V1c1Lamk arrayainfix +ainfix *c2V1c1V55FAiainfix <abucketV63V1V40Aainfix <=c0abucketV63V1agood_dataV63V64V43V54iainfix =abucketV63V1V40ain_dataV63V64V54OamemaTuple2V63V64V52qainfix =agetV43V63aSomeV64ain_dataV63V64V54NFAagood_hashV54V65Iainfix <V65ainfix +ainfix *c2V1c1Aainfix <=c0V65FAainfix =abucketV66V1V40IamemaTuple2V66V67V52FIainfix =V53asetV42abucketV50ainfix +ainfix *c2V1c1aConsaTuple2V50V51agetV42abucketV50ainfix +ainfix *c2V1c1Aainfix <=c0ainfix +ainfix *c2V1c1Lamk arrayainfix +ainfix *c2V1c1V53FAainfix <abucketV50ainfix +ainfix *c2V1c1ainfix +ainfix *c2V1c1Aainfix <=c0abucketV50ainfix +ainfix *c2V1c1Aainfix <abucketV50ainfix +ainfix *c2V1c1ainfix +ainfix *c2V1c1Aainfix <=c0abucketV50ainfix +ainfix *c2V1c1Iiainfix <abucketV68V1V40Aainfix <=c0abucketV68V1agood_dataV68V69V43V46iainfix =abucketV68V1V40ain_dataV68V69V46OamemaTuple2V68V69V41qainfix =agetV43V68aSomeV69ain_dataV68V69V46NFAagood_hashV46V70Iainfix <V70ainfix +ainfix *c2V1c1Aainfix <=c0V70FAainfix =abucketV71V1V40IamemaTuple2V71V72V41FAainfix <=c0ainfix +ainfix *c2V1c1Aainfix <=c0V44Aagood_dataV73V74V43amk arrayV44V45FAagood_hashamk arrayV44V45V75Iainfix <V75V44Aainfix <=c0V75FAainfix <c0V44Lamk arrayainfix +ainfix *c2V1c1V42FFIainfix <=c0ainfix +ainfix *c2V1c1Lamk arrayainfix +ainfix *c2V1c1aconstaNilAainfix >=ainfix +ainfix *c2V1c1c0Iainfix <=c0V1Aagood_dataV76V77V0amk arrayV1V2FAagood_hashamk arrayV1V2V78Iainfix <V78V1Aainfix <=c0V78FAainfix <c0V1F"> <label name="expl:VC for resize"/> <transf name="split_goal_wp" - proved="false" + proved="true" expanded="false"> <goal name="WP_parameter resize.1" @@ -109,7 +109,7 @@ loclnum="56" loccnumb="6" loccnume="12" expl="1. precondition" sum="825cbdcf30bb030f9017480eb1b063e7" - proved="false" + proved="true" expanded="false" shape="ainfix >=ainfix +ainfix *c2V1c1c0Iainfix <=c0V1Aagood_dataV3V4V0amk arrayV1V2FAagood_hashamk arrayV1V2V5Iainfix <V5V1Aainfix <=c0V5FAainfix <c0V1F"> <label @@ -118,7 +118,7 @@ prover="0" timelimit="5" memlimit="1000" - obsolete="true" + obsolete="false" archived="false"> <result status="valid" time="0.02"/> </proof> @@ -129,7 +129,7 @@ loclnum="56" loccnumb="6" loccnume="12" expl="2. postcondition" sum="1f87386b3151c5a29486bc690d87dac6" - proved="false" + proved="true" expanded="false" shape="CV5aNilagood_hashV10V11Iainfix <V11ainfix +ainfix *c2V1c1Aainfix <=c0V11FaConsaTuple2VVVtIiainfix <abucketV15V1V4Aainfix <=c0abucketV15V1agood_dataV15V16V7V10iainfix =abucketV15V1V4ain_dataV15V16V10OamemaTuple2V15V16V5qainfix =agetV7V15aSomeV16ain_dataV15V16V10NFAagood_hashV10V17Iainfix <V17ainfix +ainfix *c2V1c1Aainfix <=c0V17FAainfix =abucketV18V1V4IamemaTuple2V18V19V5FAainfix <=c0ainfix +ainfix *c2V1c1Aainfix <=c0V8Aagood_dataV20V21V7amk arrayV8V9FAagood_hashamk arrayV8V9V22Iainfix <V22V8Aainfix <=c0V22FAainfix <c0V8Lamk arrayainfix +ainfix *c2V1c1V6FFIainfix <=c0ainfix +ainfix *c2V1c1Lamk arrayainfix +ainfix *c2V1c1aconstaNilIainfix >=ainfix +ainfix *c2V1c1c0Iainfix <=c0V1Aagood_dataV23V24V0amk arrayV1V2FAagood_hashamk arrayV1V2V25Iainfix <V25V1Aainfix <=c0V25FAainfix <c0V1F"> <label @@ -138,7 +138,7 @@ prover="0" timelimit="5" memlimit="1000" - obsolete="true" + obsolete="false" archived="false"> <result status="valid" time="0.08"/> </proof> @@ -149,7 +149,7 @@ loclnum="56" loccnumb="6" loccnume="12" expl="3. postcondition" sum="6c9b3ce3c1de55e1964ae8edd0a2192b" - proved="false" + proved="true" expanded="false" shape="CV5aNiliainfix <=abucketV11V1V4Aainfix <=c0abucketV11V1agood_dataV11V12V7V10ain_dataV11V12V10NFaConsaTuple2VVVtIiainfix <abucketV16V1V4Aainfix <=c0abucketV16V1agood_dataV16V17V7V10iainfix =abucketV16V1V4ain_dataV16V17V10OamemaTuple2V16V17V5qainfix =agetV7V16aSomeV17ain_dataV16V17V10NFAagood_hashV10V18Iainfix <V18ainfix +ainfix *c2V1c1Aainfix <=c0V18FAainfix =abucketV19V1V4IamemaTuple2V19V20V5FAainfix <=c0ainfix +ainfix *c2V1c1Aainfix <=c0V8Aagood_dataV21V22V7amk arrayV8V9FAagood_hashamk arrayV8V9V23Iainfix <V23V8Aainfix <=c0V23FAainfix <c0V8Lamk arrayainfix +ainfix *c2V1c1V6FFIainfix <=c0ainfix +ainfix *c2V1c1Lamk arrayainfix +ainfix *c2V1c1aconstaNilIainfix >=ainfix +ainfix *c2V1c1c0Iainfix <=c0V1Aagood_dataV24V25V0amk arrayV1V2FAagood_hashamk arrayV1V2V26Iainfix <V26V1Aainfix <=c0V26FAainfix <c0V1F"> <label @@ -158,7 +158,7 @@ prover="0" timelimit="5" memlimit="1000" - obsolete="true" + obsolete="false" archived="false"> <result status="valid" time="0.07"/> </proof> @@ -169,7 +169,7 @@ loclnum="56" loccnumb="6" loccnume="12" expl="4. precondition" sum="893a6d30fa585f4a9f28148c81535fef" - proved="false" + proved="true" expanded="false" shape="CV5aNiltaConsaTuple2VVVainfix <abucketV11ainfix +ainfix *c2V1c1ainfix +ainfix *c2V1c1Aainfix <=c0abucketV11ainfix +ainfix *c2V1c1Iiainfix <abucketV14V1V4Aainfix <=c0abucketV14V1agood_dataV14V15V7V10iainfix =abucketV14V1V4ain_dataV14V15V10OamemaTuple2V14V15V5qainfix =agetV7V14aSomeV15ain_dataV14V15V10NFAagood_hashV10V16Iainfix <V16ainfix +ainfix *c2V1c1Aainfix <=c0V16FAainfix =abucketV17V1V4IamemaTuple2V17V18V5FAainfix <=c0ainfix +ainfix *c2V1c1Aainfix <=c0V8Aagood_dataV19V20V7amk arrayV8V9FAagood_hashamk arrayV8V9V21Iainfix <V21V8Aainfix <=c0V21FAainfix <c0V8Lamk arrayainfix +ainfix *c2V1c1V6FFIainfix <=c0ainfix +ainfix *c2V1c1Lamk arrayainfix +ainfix *c2V1c1aconstaNilIainfix >=ainfix +ainfix *c2V1c1c0Iainfix <=c0V1Aagood_dataV22V23V0amk arrayV1V2FAagood_hashamk arrayV1V2V24Iainfix <V24V1Aainfix <=c0V24FAainfix <c0V1F"> <label @@ -178,7 +178,7 @@ prover="0" timelimit="5" memlimit="1000" - obsolete="true" + obsolete="false" archived="false"> <result status="valid" time="0.06"/> </proof> @@ -189,7 +189,7 @@ loclnum="56" loccnumb="6" loccnume="12" expl="5. precondition" sum="8d3285924bc21b78bdf43d92cf519f80" - proved="false" + proved="true" expanded="false" shape="CV5aNiltaConsaTuple2VVVainfix <abucketV11ainfix +ainfix *c2V1c1ainfix +ainfix *c2V1c1Aainfix <=c0abucketV11ainfix +ainfix *c2V1c1Iainfix <abucketV11ainfix +ainfix *c2V1c1ainfix +ainfix *c2V1c1Aainfix <=c0abucketV11ainfix +ainfix *c2V1c1Iiainfix <abucketV14V1V4Aainfix <=c0abucketV14V1agood_dataV14V15V7V10iainfix =abucketV14V1V4ain_dataV14V15V10OamemaTuple2V14V15V5qainfix =agetV7V14aSomeV15ain_dataV14V15V10NFAagood_hashV10V16Iainfix <V16ainfix +ainfix *c2V1c1Aainfix <=c0V16FAainfix =abucketV17V1V4IamemaTuple2V17V18V5FAainfix <=c0ainfix +ainfix *c2V1c1Aainfix <=c0V8Aagood_dataV19V20V7amk arrayV8V9FAagood_hashamk arrayV8V9V21Iainfix <V21V8Aainfix <=c0V21FAainfix <c0V8Lamk arrayainfix +ainfix *c2V1c1V6FFIainfix <=c0ainfix +ainfix *c2V1c1Lamk arrayainfix +ainfix *c2V1c1aconstaNilIainfix >=ainfix +ainfix *c2V1c1c0Iainfix <=c0V1Aagood_dataV22V23V0amk arrayV1V2FAagood_hashamk arrayV1V2V24Iainfix <V24V1Aainfix <=c0V24FAainfix <c0V1F"> <label @@ -198,7 +198,7 @@ prover="0" timelimit="5" memlimit="1000" - obsolete="true" + obsolete="false" archived="false"> <result status="valid" time="0.01"/> </proof> @@ -209,7 +209,7 @@ loclnum="56" loccnumb="6" loccnume="12" expl="6. precondition" sum="77554cb0bb7d516b08935777e03f28e5" - proved="false" + proved="true" expanded="false" shape="CV5aNiltaConsaTuple2VVVainfix =abucketV16V1V4IamemaTuple2V16V17V13FIainfix =V14asetV6abucketV11ainfix +ainfix *c2V1c1aConsaTuple2V11V12agetV6abucketV11ainfix +ainfix *c2V1c1Aainfix <=c0ainfix +ainfix *c2V1c1Lamk arrayainfix +ainfix *c2V1c1V14FIainfix <abucketV11ainfix +ainfix *c2V1c1ainfix +ainfix *c2V1c1Aainfix <=c0abucketV11ainfix +ainfix *c2V1c1Iainfix <abucketV11ainfix +ainfix *c2V1c1ainfix +ainfix *c2V1c1Aainfix <=c0abucketV11ainfix +ainfix *c2V1c1Iiainfix <abucketV18V1V4Aainfix <=c0abucketV18V1agood_dataV18V19V7V10iainfix =abucketV18V1V4ain_dataV18V19V10OamemaTuple2V18V19V5qainfix =agetV7V18aSomeV19ain_dataV18V19V10NFAagood_hashV10V20Iainfix <V20ainfix +ainfix *c2V1c1Aainfix <=c0V20FAainfix =abucketV21V1V4IamemaTuple2V21V22V5FAainfix <=c0ainfix +ainfix *c2V1c1Aainfix <=c0V8Aagood_dataV23V24V7amk arrayV8V9FAagood_hashamk arrayV8V9V25Iainfix <V25V8Aainfix <=c0V25FAainfix <c0V8Lamk arrayainfix +ainfix *c2V1c1V6FFIainfix <=c0ainfix +ainfix *c2V1c1Lamk arrayainfix +ainfix *c2V1c1aconstaNilIainfix >=ainfix +ainfix *c2V1c1c0Iainfix <=c0V1Aagood_dataV26V27V0amk arrayV1V2FAagood_hashamk arrayV1V2V28Iainfix <V28V1Aainfix <=c0V28FAainfix <c0V1F"> <label @@ -218,9 +218,9 @@ prover="0" timelimit="5" memlimit="1000" - obsolete="true" + obsolete="false" archived="false"> - <result status="valid" time="0.21"/> + <result status="valid" time="0.08"/> </proof> </goal> <goal @@ -229,14 +229,14 @@ loclnum="56" loccnumb="6" loccnume="12" expl="7. precondition" sum="529071cc18aa746c59dd2a4665fff2da" - proved="false" + proved="true" expanded="false" shape="CV5aNiltaConsaTuple2VVVagood_hashV15V16Iainfix <V16ainfix +ainfix *c2V1c1Aainfix <=c0V16FIainfix =V14asetV6abucketV11ainfix +ainfix *c2V1c1aConsaTuple2V11V12agetV6abucketV11ainfix +ainfix *c2V1c1Aainfix <=c0ainfix +ainfix *c2V1c1Lamk arrayainfix +ainfix *c2V1c1V14FIainfix <abucketV11ainfix +ainfix *c2V1c1ainfix +ainfix *c2V1c1Aainfix <=c0abucketV11ainfix +ainfix *c2V1c1Iainfix <abucketV11ainfix +ainfix *c2V1c1ainfix +ainfix *c2V1c1Aainfix <=c0abucketV11ainfix +ainfix *c2V1c1Iiainfix <abucketV17V1V4Aainfix <=c0abucketV17V1agood_dataV17V18V7V10iainfix =abucketV17V1V4ain_dataV17V18V10OamemaTuple2V17V18V5qainfix =agetV7V17aSomeV18ain_dataV17V18V10NFAagood_hashV10V19Iainfix <V19ainfix +ainfix *c2V1c1Aainfix <=c0V19FAainfix =abucketV20V1V4IamemaTuple2V20V21V5FAainfix <=c0ainfix +ainfix *c2V1c1Aainfix <=c0V8Aagood_dataV22V23V7amk arrayV8V9FAagood_hashamk arrayV8V9V24Iainfix <V24V8Aainfix <=c0V24FAainfix <c0V8Lamk arrayainfix +ainfix *c2V1c1V6FFIainfix <=c0ainfix +ainfix *c2V1c1Lamk arrayainfix +ainfix *c2V1c1aconstaNilIainfix >=ainfix +ainfix *c2V1c1c0Iainfix <=c0V1Aagood_dataV25V26V0amk arrayV1V2FAagood_hashamk arrayV1V2V27Iainfix <V27V1Aainfix <=c0V27FAainfix <c0V1F"> <label name="expl:VC for resize"/> <transf name="inline_all" - proved="false" + proved="true" expanded="false"> <goal name="WP_parameter resize.7.1" @@ -244,7 +244,7 @@ loclnum="56" loccnumb="6" loccnume="12" expl="1. precondition" sum="80d6d821dbaf6d3a9db150b658fb3c90" - proved="false" + proved="true" expanded="false" shape="CV5aNiltaConsaTuple2VVVainfix =amodahashV17alengthV15V16IamemaTuple2V17V18agetaeltsV15V16FIainfix <V16ainfix +ainfix *c2V1c1Aainfix =c0V16Oainfix <c0V16FIainfix =V14asetV6amodahashV11ainfix +ainfix *c2V1c1aConsaTuple2V11V12agetV6amodahashV11ainfix +ainfix *c2V1c1Aainfix =c0ainfix +ainfix *c2V1c1Oainfix <c0ainfix +ainfix *c2V1c1Lamk arrayainfix +ainfix *c2V1c1V14FIainfix <amodahashV11ainfix +ainfix *c2V1c1ainfix +ainfix *c2V1c1Aainfix =c0amodahashV11ainfix +ainfix *c2V1c1Oainfix <c0amodahashV11ainfix +ainfix *c2V1c1Iainfix <amodahashV11ainfix +ainfix *c2V1c1ainfix +ainfix *c2V1c1Aainfix =c0amodahashV11ainfix +ainfix *c2V1c1Oainfix <c0amodahashV11ainfix +ainfix *c2V1c1Iiainfix <amodahashV19V1V4Aainfix =c0amodahashV19V1Oainfix <c0amodahashV19V1amemaTuple2V19V20agetaeltsV10amodahashV19alengthV10qainfix =agetV7V19aSomeV20iainfix =amodahashV19V1V4amemaTuple2V19V20agetaeltsV10amodahashV19alengthV10OamemaTuple2V19V20V5qainfix =agetV7V19aSomeV20amemaTuple2V19V20agetaeltsV10amodahashV19alengthV10NFAainfix =amodahashV22alengthV10V21IamemaTuple2V22V23agetaeltsV10V21FIainfix <V21ainfix +ainfix *c2V1c1Aainfix =c0V21Oainfix <c0V21FAainfix =amodahashV24V1V4IamemaTuple2V24V25V5FAainfix =c0ainfix +ainfix *c2V1c1Oainfix <c0ainfix +ainfix *c2V1c1Aainfix =c0V8Oainfix <c0V8AamemaTuple2V26V27agetaeltsamk arrayV8V9amodahashV26alengthamk arrayV8V9qainfix =agetV7V26aSomeV27FAainfix =amodahashV29alengthamk arrayV8V9V28IamemaTuple2V29V30agetaeltsamk arrayV8V9V28FIainfix <V28V8Aainfix =c0V28Oainfix <c0V28FAainfix <c0V8Lamk arrayainfix +ainfix *c2V1c1V6FFIainfix =c0ainfix +ainfix *c2V1c1Oainfix <c0ainfix +ainfix *c2V1c1Lamk arrayainfix +ainfix *c2V1c1aconstaNilIainfix =c0ainfix +ainfix *c2V1c1Oainfix <c0ainfix +ainfix *c2V1c1Iainfix =c0V1Oainfix <c0V1AamemaTuple2V31V32agetaeltsamk arrayV1V2amodahashV31alengthamk arrayV1V2qainfix =agetV0V31aSomeV32FAainfix =amodahashV34alengthamk arrayV1V2V33IamemaTuple2V34V35agetaeltsamk arrayV1V2V33FIainfix <V33V1Aainfix =c0V33Oainfix <c0V33FAainfix <c0V1F"> <label @@ -253,9 +253,9 @@ prover="1" timelimit="15" memlimit="1000" - obsolete="true" + obsolete="false" archived="false"> - <result status="valid" time="2.70"/> + <result status="valid" time="1.49"/> </proof> </goal> </transf> @@ -266,14 +266,14 @@ loclnum="56" loccnumb="6" loccnume="12" expl="8. precondition" sum="30f6c69f476523b0407a167f307f15ea" - proved="false" + proved="true" expanded="false" shape="CV5aNiltaConsaTuple2VVViainfix <abucketV16V1V4Aainfix <=c0abucketV16V1agood_dataV16V17V7V15iainfix =abucketV16V1V4ain_dataV16V17V15OamemaTuple2V16V17V13qainfix =agetV7V16aSomeV17ain_dataV16V17V15NFIainfix =V14asetV6abucketV11ainfix +ainfix *c2V1c1aConsaTuple2V11V12agetV6abucketV11ainfix +ainfix *c2V1c1Aainfix <=c0ainfix +ainfix *c2V1c1Lamk arrayainfix +ainfix *c2V1c1V14FIainfix <abucketV11ainfix +ainfix *c2V1c1ainfix +ainfix *c2V1c1Aainfix <=c0abucketV11ainfix +ainfix *c2V1c1Iainfix <abucketV11ainfix +ainfix *c2V1c1ainfix +ainfix *c2V1c1Aainfix <=c0abucketV11ainfix +ainfix *c2V1c1Iiainfix <abucketV18V1V4Aainfix <=c0abucketV18V1agood_dataV18V19V7V10iainfix =abucketV18V1V4ain_dataV18V19V10OamemaTuple2V18V19V5qainfix =agetV7V18aSomeV19ain_dataV18V19V10NFAagood_hashV10V20Iainfix <V20ainfix +ainfix *c2V1c1Aainfix <=c0V20FAainfix =abucketV21V1V4IamemaTuple2V21V22V5FAainfix <=c0ainfix +ainfix *c2V1c1Aainfix <=c0V8Aagood_dataV23V24V7amk arrayV8V9FAagood_hashamk arrayV8V9V25Iainfix <V25V8Aainfix <=c0V25FAainfix <c0V8Lamk arrayainfix +ainfix *c2V1c1V6FFIainfix <=c0ainfix +ainfix *c2V1c1Lamk arrayainfix +ainfix *c2V1c1aconstaNilIainfix >=ainfix +ainfix *c2V1c1c0Iainfix <=c0V1Aagood_dataV26V27V0amk arrayV1V2FAagood_hashamk arrayV1V2V28Iainfix <V28V1Aainfix <=c0V28FAainfix <c0V1F"> <label name="expl:VC for resize"/> <transf name="inline_all" - proved="false" + proved="true" expanded="false"> <goal name="WP_parameter resize.8.1" @@ -281,14 +281,14 @@ loclnum="56" loccnumb="6" loccnume="12" expl="1. precondition" sum="c6cbe4ab1dca6de59194165b7f5f8998" - proved="false" + proved="true" expanded="false" shape="CV5aNiltaConsaTuple2VVViainfix <amodahashV16V1V4Aainfix =c0amodahashV16V1Oainfix <c0amodahashV16V1amemaTuple2V16V17agetaeltsV15amodahashV16alengthV15qainfix =agetV7V16aSomeV17iainfix =amodahashV16V1V4amemaTuple2V16V17agetaeltsV15amodahashV16alengthV15OamemaTuple2V16V17V13qainfix =agetV7V16aSomeV17amemaTuple2V16V17agetaeltsV15amodahashV16alengthV15NFIainfix =V14asetV6amodahashV11ainfix +ainfix *c2V1c1aConsaTuple2V11V12agetV6amodahashV11ainfix +ainfix *c2V1c1Aainfix =c0ainfix +ainfix *c2V1c1Oainfix <c0ainfix +ainfix *c2V1c1Lamk arrayainfix +ainfix *c2V1c1V14FIainfix <amodahashV11ainfix +ainfix *c2V1c1ainfix +ainfix *c2V1c1Aainfix =c0amodahashV11ainfix +ainfix *c2V1c1Oainfix <c0amodahashV11ainfix +ainfix *c2V1c1Iainfix <amodahashV11ainfix +ainfix *c2V1c1ainfix +ainfix *c2V1c1Aainfix =c0amodahashV11ainfix +ainfix *c2V1c1Oainfix <c0amodahashV11ainfix +ainfix *c2V1c1Iiainfix <amodahashV18V1V4Aainfix =c0amodahashV18V1Oainfix <c0amodahashV18V1amemaTuple2V18V19agetaeltsV10amodahashV18alengthV10qainfix =agetV7V18aSomeV19iainfix =amodahashV18V1V4amemaTuple2V18V19agetaeltsV10amodahashV18alengthV10OamemaTuple2V18V19V5qainfix =agetV7V18aSomeV19amemaTuple2V18V19agetaeltsV10amodahashV18alengthV10NFAainfix =amodahashV21alengthV10V20IamemaTuple2V21V22agetaeltsV10V20FIainfix <V20ainfix +ainfix *c2V1c1Aainfix =c0V20Oainfix <c0V20FAainfix =amodahashV23V1V4IamemaTuple2V23V24V5FAainfix =c0ainfix +ainfix *c2V1c1Oainfix <c0ainfix +ainfix *c2V1c1Aainfix =c0V8Oainfix <c0V8AamemaTuple2V25V26agetaeltsamk arrayV8V9amodahashV25alengthamk arrayV8V9qainfix =agetV7V25aSomeV26FAainfix =amodahashV28alengthamk arrayV8V9V27IamemaTuple2V28V29agetaeltsamk arrayV8V9V27FIainfix <V27V8Aainfix =c0V27Oainfix <c0V27FAainfix <c0V8Lamk arrayainfix +ainfix *c2V1c1V6FFIainfix =c0ainfix +ainfix *c2V1c1Oainfix <c0ainfix +ainfix *c2V1c1Lamk arrayainfix +ainfix *c2V1c1aconstaNilIainfix =c0ainfix +ainfix *c2V1c1Oainfix <c0ainfix +ainfix *c2V1c1Iainfix =c0V1Oainfix <c0V1AamemaTuple2V30V31agetaeltsamk arrayV1V2amodahashV30alengthamk arrayV1V2qainfix =agetV0V30aSomeV31FAainfix =amodahashV33alengthamk arrayV1V2V32IamemaTuple2V33V34agetaeltsamk arrayV1V2V32FIainfix <V32V1Aainfix =c0V32Oainfix <c0V32FAainfix <c0V1F"> <label name="expl:VC for resize"/> <transf name="split_goal_wp" - proved="false" + proved="true" expanded="false"> <goal name="WP_parameter resize.8.1.1" @@ -296,7 +296,7 @@ loclnum="56" loccnumb="6" loccnume="12" expl="1. precondition" sum="8a43b06de7e0b04831d44b9d6f583fdb" - proved="false" + proved="true" expanded="false" shape="CV5aNiltaConsaTuple2VVVamemaTuple2V16V17agetaeltsV15amodahashV16alengthV15Iainfix =agetV7V16aSomeV17Iainfix <amodahashV16V1V4Aainfix =c0amodahashV16V1Oainfix <c0amodahashV16V1FIainfix =V14asetV6amodahashV11ainfix +ainfix *c2V1c1aConsaTuple2V11V12agetV6amodahashV11ainfix +ainfix *c2V1c1Aainfix =c0ainfix +ainfix *c2V1c1Oainfix <c0ainfix +ainfix *c2V1c1Lamk arrayainfix +ainfix *c2V1c1V14FIainfix <amodahashV11ainfix +ainfix *c2V1c1ainfix +ainfix *c2V1c1Aainfix =c0amodahashV11ainfix +ainfix *c2V1c1Oainfix <c0amodahashV11ainfix +ainfix *c2V1c1Iainfix <amodahashV11ainfix +ainfix *c2V1c1ainfix +ainfix *c2V1c1Aainfix =c0amodahashV11ainfix +ainfix *c2V1c1Oainfix <c0amodahashV11ainfix +ainfix *c2V1c1Iiainfix <amodahashV18V1V4Aainfix =c0amodahashV18V1Oainfix <c0amodahashV18V1amemaTuple2V18V19agetaeltsV10amodahashV18alengthV10qainfix =agetV7V18aSomeV19iainfix =amodahashV18V1V4amemaTuple2V18V19agetaeltsV10amodahashV18alengthV10OamemaTuple2V18V19V5qainfix =agetV7V18aSomeV19amemaTuple2V18V19agetaeltsV10amodahashV18alengthV10NFAainfix =amodahashV21alengthV10V20IamemaTuple2V21V22agetaeltsV10V20FIainfix <V20ainfix +ainfix *c2V1c1Aainfix =c0V20Oainfix <c0V20FAainfix =amodahashV23V1V4IamemaTuple2V23V24V5FAainfix =c0ainfix +ainfix *c2V1c1Oainfix <c0ainfix +ainfix *c2V1c1Aainfix =c0V8Oainfix <c0V8AamemaTuple2V25V26agetaeltsamk arrayV8V9amodahashV25alengthamk arrayV8V9qainfix =agetV7V25aSomeV26FAainfix =amodahashV28alengthamk arrayV8V9V27IamemaTuple2V28V29agetaeltsamk arrayV8V9V27FIainfix <V27V8Aainfix =c0V27Oainfix <c0V27FAainfix <c0V8Lamk arrayainfix +ainfix *c2V1c1V6FFIainfix =c0ainfix +ainfix *c2V1c1Oainfix <c0ainfix +ainfix *c2V1c1Lamk arrayainfix +ainfix *c2V1c1aconstaNilIainfix =c0ainfix +ainfix *c2V1c1Oainfix <c0ainfix +ainfix *c2V1c1Iainfix =c0V1Oainfix <c0V1AamemaTuple2V30V31agetaeltsamk arrayV1V2amodahashV30alengthamk arrayV1V2qainfix =agetV0V30aSomeV31FAainfix =amodahashV33alengthamk arrayV1V2V32IamemaTuple2V33V34agetaeltsamk arrayV1V2V32FIainfix <V32V1Aainfix =c0V32Oainfix <c0V32FAainfix <c0V1F"> <label @@ -305,7 +305,7 @@ prover="2" timelimit="5" memlimit="1000" - obsolete="true" + obsolete="false" archived="false"> <result status="valid" time="0.19"/> </proof> @@ -316,7 +316,7 @@ loclnum="56" loccnumb="6" loccnume="12" expl="2. precondition" sum="b6ad8e172b5991e11c2c978c535ebdd6" - proved="false" + proved="true" expanded="false" shape="CV5aNiltaConsaTuple2VVVainfix =agetV7V16aSomeV17IamemaTuple2V16V17agetaeltsV15amodahashV16alengthV15Iainfix <amodahashV16V1V4Aainfix =c0amodahashV16V1Oainfix <c0amodahashV16V1FIainfix =V14asetV6amodahashV11ainfix +ainfix *c2V1c1aConsaTuple2V11V12agetV6amodahashV11ainfix +ainfix *c2V1c1Aainfix =c0ainfix +ainfix *c2V1c1Oainfix <c0ainfix +ainfix *c2V1c1Lamk arrayainfix +ainfix *c2V1c1V14FIainfix <amodahashV11ainfix +ainfix *c2V1c1ainfix +ainfix *c2V1c1Aainfix =c0amodahashV11ainfix +ainfix *c2V1c1Oainfix <c0amodahashV11ainfix +ainfix *c2V1c1Iainfix <amodahashV11ainfix +ainfix *c2V1c1ainfix +ainfix *c2V1c1Aainfix =c0amodahashV11ainfix +ainfix *c2V1c1Oainfix <c0amodahashV11ainfix +ainfix *c2V1c1Iiainfix <amodahashV18V1V4Aainfix =c0amodahashV18V1Oainfix <c0amodahashV18V1amemaTuple2V18V19agetaeltsV10amodahashV18alengthV10qainfix =agetV7V18aSomeV19iainfix =amodahashV18V1V4amemaTuple2V18V19agetaeltsV10amodahashV18alengthV10OamemaTuple2V18V19V5qainfix =agetV7V18aSomeV19amemaTuple2V18V19agetaeltsV10amodahashV18alengthV10NFAainfix =amodahashV21alengthV10V20IamemaTuple2V21V22agetaeltsV10V20FIainfix <V20ainfix +ainfix *c2V1c1Aainfix =c0V20Oainfix <c0V20FAainfix =amodahashV23V1V4IamemaTuple2V23V24V5FAainfix =c0ainfix +ainfix *c2V1c1Oainfix <c0ainfix +ainfix *c2V1c1Aainfix =c0V8Oainfix <c0V8AamemaTuple2V25V26agetaeltsamk arrayV8V9amodahashV25alengthamk arrayV8V9qainfix =agetV7V25aSomeV26FAainfix =amodahashV28alengthamk arrayV8V9V27IamemaTuple2V28V29agetaeltsamk arrayV8V9V27FIainfix <V27V8Aainfix =c0V27Oainfix <c0V27FAainfix <c0V8Lamk arrayainfix +ainfix *c2V1c1V6FFIainfix =c0ainfix +ainfix *c2V1c1Oainfix <c0ainfix +ainfix *c2V1c1Lamk arrayainfix +ainfix *c2V1c1aconstaNilIainfix =c0ainfix +ainfix *c2V1c1Oainfix <c0ainfix +ainfix *c2V1c1Iainfix =c0V1Oainfix <c0V1AamemaTuple2V30V31agetaeltsamk arrayV1V2amodahashV30alengthamk arrayV1V2qainfix =agetV0V30aSomeV31FAainfix =amodahashV33alengthamk arrayV1V2V32IamemaTuple2V33V34agetaeltsamk arrayV1V2V32FIainfix <V32V1Aainfix =c0V32Oainfix <c0V32FAainfix <c0V1F"> <label @@ -325,7 +325,7 @@ prover="2" timelimit="5" memlimit="1000" - obsolete="true" + obsolete="false" archived="false"> <result status="valid" time="0.16"/> </proof> @@ -336,7 +336,7 @@ loclnum="56" loccnumb="6" loccnume="12" expl="3. precondition" sum="5d00c65189636065dab1432e5ca37012" - proved="false" + proved="true" expanded="false" shape="CV5aNiltaConsaTuple2VVVamemaTuple2V16V17agetaeltsV15amodahashV16alengthV15OamemaTuple2V16V17V13Iainfix =agetV7V16aSomeV17Iainfix =amodahashV16V1V4Iainfix <amodahashV16V1V4Aainfix =c0amodahashV16V1Oainfix <c0amodahashV16V1NFIainfix =V14asetV6amodahashV11ainfix +ainfix *c2V1c1aConsaTuple2V11V12agetV6amodahashV11ainfix +ainfix *c2V1c1Aainfix =c0ainfix +ainfix *c2V1c1Oainfix <c0ainfix +ainfix *c2V1c1Lamk arrayainfix +ainfix *c2V1c1V14FIainfix <amodahashV11ainfix +ainfix *c2V1c1ainfix +ainfix *c2V1c1Aainfix =c0amodahashV11ainfix +ainfix *c2V1c1Oainfix <c0amodahashV11ainfix +ainfix *c2V1c1Iainfix <amodahashV11ainfix +ainfix *c2V1c1ainfix +ainfix *c2V1c1Aainfix =c0amodahashV11ainfix +ainfix *c2V1c1Oainfix <c0amodahashV11ainfix +ainfix *c2V1c1Iiainfix <amodahashV18V1V4Aainfix =c0amodahashV18V1Oainfix <c0amodahashV18V1amemaTuple2V18V19agetaeltsV10amodahashV18alengthV10qainfix =agetV7V18aSomeV19iainfix =amodahashV18V1V4amemaTuple2V18V19agetaeltsV10amodahashV18alengthV10OamemaTuple2V18V19V5qainfix =agetV7V18aSomeV19amemaTuple2V18V19agetaeltsV10amodahashV18alengthV10NFAainfix =amodahashV21alengthV10V20IamemaTuple2V21V22agetaeltsV10V20FIainfix <V20ainfix +ainfix *c2V1c1Aainfix =c0V20Oainfix <c0V20FAainfix =amodahashV23V1V4IamemaTuple2V23V24V5FAainfix =c0ainfix +ainfix *c2V1c1Oainfix <c0ainfix +ainfix *c2V1c1Aainfix =c0V8Oainfix <c0V8AamemaTuple2V25V26agetaeltsamk arrayV8V9amodahashV25alengthamk arrayV8V9qainfix =agetV7V25aSomeV26FAainfix =amodahashV28alengthamk arrayV8V9V27IamemaTuple2V28V29agetaeltsamk arrayV8V9V27FIainfix <V27V8Aainfix =c0V27Oainfix <c0V27FAainfix <c0V8Lamk arrayainfix +ainfix *c2V1c1V6FFIainfix =c0ainfix +ainfix *c2V1c1Oainfix <c0ainfix +ainfix *c2V1c1Lamk arrayainfix +ainfix *c2V1c1aconstaNilIainfix =c0ainfix +ainfix *c2V1c1Oainfix <c0ainfix +ainfix *c2V1c1Iainfix =c0V1Oainfix <c0V1AamemaTuple2V30V31agetaeltsamk arrayV1V2amodahashV30alengthamk arrayV1V2qainfix =agetV0V30aSomeV31FAainfix =amodahashV33alengthamk arrayV1V2V32IamemaTuple2V33V34agetaeltsamk arrayV1V2V32FIainfix <V32V1Aainfix =c0V32Oainfix <c0V32FAainfix <c0V1F"> <label @@ -345,9 +345,9 @@ prover="2" timelimit="15" memlimit="1000" - obsolete="true" + obsolete="false" archived="false"> - <result status="valid" time="14.22"/> + <result status="valid" time="8.10"/> </proof> </goal> <goal @@ -356,7 +356,7 @@ loclnum="56" loccnumb="6" loccnume="12" expl="4. precondition" sum="37c0bdfb28ea5d0895e101cae987787b" - proved="false" + proved="true" expanded="false" shape="CV5aNiltaConsaTuple2VVVainfix =agetV7V16aSomeV17IamemaTuple2V16V17agetaeltsV15amodahashV16alengthV15OamemaTuple2V16V17V13Iainfix =amodahashV16V1V4Iainfix <amodahashV16V1V4Aainfix =c0amodahashV16V1Oainfix <c0amodahashV16V1NFIainfix =V14asetV6amodahashV11ainfix +ainfix *c2V1c1aConsaTuple2V11V12agetV6amodahashV11ainfix +ainfix *c2V1c1Aainfix =c0ainfix +ainfix *c2V1c1Oainfix <c0ainfix +ainfix *c2V1c1Lamk arrayainfix +ainfix *c2V1c1V14FIainfix <amodahashV11ainfix +ainfix *c2V1c1ainfix +ainfix *c2V1c1Aainfix =c0amodahashV11ainfix +ainfix *c2V1c1Oainfix <c0amodahashV11ainfix +ainfix *c2V1c1Iainfix <amodahashV11ainfix +ainfix *c2V1c1ainfix +ainfix *c2V1c1Aainfix =c0amodahashV11ainfix +ainfix *c2V1c1Oainfix <c0amodahashV11ainfix +ainfix *c2V1c1Iiainfix <amodahashV18V1V4Aainfix =c0amodahashV18V1Oainfix <c0amodahashV18V1amemaTuple2V18V19agetaeltsV10amodahashV18alengthV10qainfix =agetV7V18aSomeV19iainfix =amodahashV18V1V4amemaTuple2V18V19agetaeltsV10amodahashV18alengthV10OamemaTuple2V18V19V5qainfix =agetV7V18aSomeV19amemaTuple2V18V19agetaeltsV10amodahashV18alengthV10NFAainfix =amodahashV21alengthV10V20IamemaTuple2V21V22agetaeltsV10V20FIainfix <V20ainfix +ainfix *c2V1c1Aainfix =c0V20Oainfix <c0V20FAainfix =amodahashV23V1V4IamemaTuple2V23V24V5FAainfix =c0ainfix +ainfix *c2V1c1Oainfix <c0ainfix +ainfix *c2V1c1Aainfix =c0V8Oainfix <c0V8AamemaTuple2V25V26agetaeltsamk arrayV8V9amodahashV25alengthamk arrayV8V9qainfix =agetV7V25aSomeV26FAainfix =amodahashV28alengthamk arrayV8V9V27IamemaTuple2V28V29agetaeltsamk arrayV8V9V27FIainfix <V27V8Aainfix =c0V27Oainfix <c0V27FAainfix <c0V8Lamk arrayainfix +ainfix *c2V1c1V6FFIainfix =c0ainfix +ainfix *c2V1c1Oainfix <c0ainfix +ainfix *c2V1c1Lamk arrayainfix +ainfix *c2V1c1aconstaNilIainfix =c0ainfix +ainfix *c2V1c1Oainfix <c0ainfix +ainfix *c2V1c1Iainfix =c0V1Oainfix <c0V1AamemaTuple2V30V31agetaeltsamk arrayV1V2amodahashV30alengthamk arrayV1V2qainfix =agetV0V30aSomeV31FAainfix =amodahashV33alengthamk arrayV1V2V32IamemaTuple2V33V34agetaeltsamk arrayV1V2V32FIainfix <V32V1Aainfix =c0V32Oainfix <c0V32FAainfix <c0V1F"> <label @@ -365,7 +365,7 @@ prover="2" timelimit="5" memlimit="1000" - obsolete="true" + obsolete="false" archived="false"> <result status="valid" time="0.17"/> </proof> @@ -376,7 +376,7 @@ loclnum="56" loccnumb="6" loccnume="12" expl="5. precondition" sum="57fc535a1c7fe3011b64402414439044" - proved="false" + proved="true" expanded="false" shape="CV5aNiltaConsaTuple2VVVamemaTuple2V16V17agetaeltsV15amodahashV16alengthV15NIainfix =amodahashV16V1V4NIainfix <amodahashV16V1V4Aainfix =c0amodahashV16V1Oainfix <c0amodahashV16V1NFIainfix =V14asetV6amodahashV11ainfix +ainfix *c2V1c1aConsaTuple2V11V12agetV6amodahashV11ainfix +ainfix *c2V1c1Aainfix =c0ainfix +ainfix *c2V1c1Oainfix <c0ainfix +ainfix *c2V1c1Lamk arrayainfix +ainfix *c2V1c1V14FIainfix <amodahashV11ainfix +ainfix *c2V1c1ainfix +ainfix *c2V1c1Aainfix =c0amodahashV11ainfix +ainfix *c2V1c1Oainfix <c0amodahashV11ainfix +ainfix *c2V1c1Iainfix <amodahashV11ainfix +ainfix *c2V1c1ainfix +ainfix *c2V1c1Aainfix =c0amodahashV11ainfix +ainfix *c2V1c1Oainfix <c0amodahashV11ainfix +ainfix *c2V1c1Iiainfix <amodahashV18V1V4Aainfix =c0amodahashV18V1Oainfix <c0amodahashV18V1amemaTuple2V18V19agetaeltsV10amodahashV18alengthV10qainfix =agetV7V18aSomeV19iainfix =amodahashV18V1V4amemaTuple2V18V19agetaeltsV10amodahashV18alengthV10OamemaTuple2V18V19V5qainfix =agetV7V18aSomeV19amemaTuple2V18V19agetaeltsV10amodahashV18alengthV10NFAainfix =amodahashV21alengthV10V20IamemaTuple2V21V22agetaeltsV10V20FIainfix <V20ainfix +ainfix *c2V1c1Aainfix =c0V20Oainfix <c0V20FAainfix =amodahashV23V1V4IamemaTuple2V23V24V5FAainfix =c0ainfix +ainfix *c2V1c1Oainfix <c0ainfix +ainfix *c2V1c1Aainfix =c0V8Oainfix <c0V8AamemaTuple2V25V26agetaeltsamk arrayV8V9amodahashV25alengthamk arrayV8V9qainfix =agetV7V25aSomeV26FAainfix =amodahashV28alengthamk arrayV8V9V27IamemaTuple2V28V29agetaeltsamk arrayV8V9V27FIainfix <V27V8Aainfix =c0V27Oainfix <c0V27FAainfix <c0V8Lamk arrayainfix +ainfix *c2V1c1V6FFIainfix =c0ainfix +ainfix *c2V1c1Oainfix <c0ainfix +ainfix *c2V1c1Lamk arrayainfix +ainfix *c2V1c1aconstaNilIainfix =c0ainfix +ainfix *c2V1c1Oainfix <c0ainfix +ainfix *c2V1c1Iainfix =c0V1Oainfix <c0V1AamemaTuple2V30V31agetaeltsamk arrayV1V2amodahashV30alengthamk arrayV1V2qainfix =agetV0V30aSomeV31FAainfix =amodahashV33alengthamk arrayV1V2V32IamemaTuple2V33V34agetaeltsamk arrayV1V2V32FIainfix <V32V1Aainfix =c0V32Oainfix <c0V32FAainfix <c0V1F"> <label @@ -385,7 +385,7 @@ prover="2" timelimit="5" memlimit="1000" - obsolete="true" + obsolete="false" archived="false"> <result status="valid" time="0.15"/> </proof> @@ -400,7 +400,7 @@ loclnum="56" loccnumb="6" loccnume="12" expl="9. postcondition" sum="e86ddedfda00ba24b7ea8df936ad44d9" - proved="false" + proved="true" expanded="false" shape="CV5aNiltaConsaTuple2VVVagood_hashV17V18Iainfix <V18ainfix +ainfix *c2V1c1Aainfix <=c0V18FIiainfix <=abucketV19V1V4Aainfix <=c0abucketV19V1agood_dataV19V20V7V17ain_dataV19V20V17NFAagood_hashV17V21Iainfix <V21ainfix +ainfix *c2V1c1Aainfix <=c0V21FAainfix <=c0ainfix +ainfix *c2V1c1Lamk arrayainfix +ainfix *c2V1c1V16FIiainfix <abucketV22V1V4Aainfix <=c0abucketV22V1agood_dataV22V23V7V15iainfix =abucketV22V1V4ain_dataV22V23V15OamemaTuple2V22V23V13qainfix =agetV7V22aSomeV23ain_dataV22V23V15NFAagood_hashV15V24Iainfix <V24ainfix +ainfix *c2V1c1Aainfix <=c0V24FAainfix =abucketV25V1V4IamemaTuple2V25V26V13FIainfix =V14asetV6abucketV11ainfix +ainfix *c2V1c1aConsaTuple2V11V12agetV6abucketV11ainfix +ainfix *c2V1c1Aainfix <=c0ainfix +ainfix *c2V1c1Lamk arrayainfix +ainfix *c2V1c1V14FIainfix <abucketV11ainfix +ainfix *c2V1c1ainfix +ainfix *c2V1c1Aainfix <=c0abucketV11ainfix +ainfix *c2V1c1Iainfix <abucketV11ainfix +ainfix *c2V1c1ainfix +ainfix *c2V1c1Aainfix <=c0abucketV11ainfix +ainfix *c2V1c1Iiainfix <abucketV27V1V4Aainfix <=c0abucketV27V1agood_dataV27V28V7V10iainfix =abucketV27V1V4ain_dataV27V28V10OamemaTuple2V27V28V5qainfix =agetV7V27aSomeV28ain_dataV27V28V10NFAagood_hashV10V29Iainfix <V29ainfix +ainfix *c2V1c1Aainfix <=c0V29FAainfix =abucketV30V1V4IamemaTuple2V30V31V5FAainfix <=c0ainfix +ainfix *c2V1c1Aainfix <=c0V8Aagood_dataV32V33V7amk arrayV8V9FAagood_hashamk arrayV8V9V34Iainfix <V34V8Aainfix <=c0V34FAainfix <c0V8Lamk arrayainfix +ainfix *c2V1c1V6FFIainfix <=c0ainfix +ainfix *c2V1c1Lamk arrayainfix +ainfix *c2V1c1aconstaNilIainfix >=ainfix +ainfix *c2V1c1c0Iainfix <=c0V1Aagood_dataV35V36V0amk arrayV1V2FAagood_hashamk arrayV1V2V37Iainfix <V37V1Aainfix <=c0V37FAainfix <c0V1F"> <label @@ -409,7 +409,7 @@ prover="1" timelimit="5" memlimit="1000" - obsolete="true" + obsolete="false" archived="false"> <result status="valid" time="0.05"/> </proof> @@ -417,7 +417,7 @@ prover="2" timelimit="5" memlimit="1000" - obsolete="true" + obsolete="false" archived="false"> <result status="valid" time="0.04"/> </proof> @@ -428,7 +428,7 @@ loclnum="56" loccnumb="6" loccnume="12" expl="10. postcondition" sum="4865e83d9f7f74b1dd1cfd6e742d6a41" - proved="false" + proved="true" expanded="false" shape="CV5aNiltaConsaTuple2VVViainfix <=abucketV18V1V4Aainfix <=c0abucketV18V1agood_dataV18V19V7V17ain_dataV18V19V17NFIiainfix <=abucketV20V1V4Aainfix <=c0abucketV20V1agood_dataV20V21V7V17ain_dataV20V21V17NFAagood_hashV17V22Iainfix <V22ainfix +ainfix *c2V1c1Aainfix <=c0V22FAainfix <=c0ainfix +ainfix *c2V1c1Lamk arrayainfix +ainfix *c2V1c1V16FIiainfix <abucketV23V1V4Aainfix <=c0abucketV23V1agood_dataV23V24V7V15iainfix =abucketV23V1V4ain_dataV23V24V15OamemaTuple2V23V24V13qainfix =agetV7V23aSomeV24ain_dataV23V24V15NFAagood_hashV15V25Iainfix <V25ainfix +ainfix *c2V1c1Aainfix <=c0V25FAainfix =abucketV26V1V4IamemaTuple2V26V27V13FIainfix =V14asetV6abucketV11ainfix +ainfix *c2V1c1aConsaTuple2V11V12agetV6abucketV11ainfix +ainfix *c2V1c1Aainfix <=c0ainfix +ainfix *c2V1c1Lamk arrayainfix +ainfix *c2V1c1V14FIainfix <abucketV11ainfix +ainfix *c2V1c1ainfix +ainfix *c2V1c1Aainfix <=c0abucketV11ainfix +ainfix *c2V1c1Iainfix <abucketV11ainfix +ainfix *c2V1c1ainfix +ainfix *c2V1c1Aainfix <=c0abucketV11ainfix +ainfix *c2V1c1Iiainfix <abucketV28V1V4Aainfix <=c0abucketV28V1agood_dataV28V29V7V10iainfix =abucketV28V1V4ain_dataV28V29V10OamemaTuple2V28V29V5qainfix =agetV7V28aSomeV29ain_dataV28V29V10NFAagood_hashV10V30Iainfix <V30ainfix +ainfix *c2V1c1Aainfix <=c0V30FAainfix =abucketV31V1V4IamemaTuple2V31V32V5FAainfix <=c0ainfix +ainfix *c2V1c1Aainfix <=c0V8Aagood_dataV33V34V7amk arrayV8V9FAagood_hashamk arrayV8V9V35Iainfix <V35V8Aainfix <=c0V35FAainfix <c0V8Lamk arrayainfix +ainfix *c2V1c1V6FFIainfix <=c0ainfix +ainfix *c2V1c1Lamk arrayainfix +ainfix *c2V1c1aconstaNilIainfix >=ainfix +ainfix *c2V1c1c0Iainfix <=c0V1Aagood_dataV36V37V0amk arrayV1V2FAagood_hashamk arrayV1V2V38Iainfix <V38V1Aainfix <=c0V38FAainfix <c0V1F"> <label @@ -437,7 +437,7 @@ prover="0" timelimit="5" memlimit="1000" - obsolete="true" + obsolete="false" archived="false"> <result status="valid" time="0.07"/> </proof> @@ -448,7 +448,7 @@ loclnum="56" loccnumb="6" loccnume="12" expl="11. type invariant" sum="26375c8a180a413049c7c6c9230357ab" - proved="false" + proved="true" expanded="false" shape="ainfix <c0V4Iainfix =V5aconstaNilAainfix =V4ainfix +ainfix *c2V1c1FIainfix >c0ainfix -V1c1Iainfix <=c0ainfix +ainfix *c2V1c1Lamk arrayainfix +ainfix *c2V1c1aconstaNilIainfix >=ainfix +ainfix *c2V1c1c0Iainfix <=c0V1Aagood_dataV6V7V0amk arrayV1V2FAagood_hashamk arrayV1V2V8Iainfix <V8V1Aainfix <=c0V8FAainfix <c0V1F"> <label @@ -457,7 +457,7 @@ prover="0" timelimit="5" memlimit="1000" - obsolete="true" + obsolete="false" archived="false"> <result status="valid" time="0.02"/> </proof> @@ -468,7 +468,7 @@ loclnum="56" loccnumb="6" loccnume="12" expl="12. type invariant" sum="390e582d6436bad5ed02531f834eb7fc" - proved="false" + proved="true" expanded="false" shape="agood_hashamk arrayV4V5V6Iainfix <V6V4Aainfix <=c0V6FIainfix =V5aconstaNilAainfix =V4ainfix +ainfix *c2V1c1FIainfix >c0ainfix -V1c1Iainfix <=c0ainfix +ainfix *c2V1c1Lamk arrayainfix +ainfix *c2V1c1aconstaNilIainfix >=ainfix +ainfix *c2V1c1c0Iainfix <=c0V1Aagood_dataV7V8V0amk arrayV1V2FAagood_hashamk arrayV1V2V9Iainfix <V9V1Aainfix <=c0V9FAainfix <c0V1F"> <label @@ -477,7 +477,7 @@ prover="0" timelimit="5" memlimit="1000" - obsolete="true" + obsolete="false" archived="false"> <result status="valid" time="0.05"/> </proof> @@ -488,7 +488,7 @@ loclnum="56" loccnumb="6" loccnume="12" expl="13. type invariant" sum="f8b0224b75b76e6bf8ddf1241fadaf37" - proved="false" + proved="true" expanded="false" shape="agood_dataV6V7V0amk arrayV4V5FIainfix =V5aconstaNilAainfix =V4ainfix +ainfix *c2V1c1FIainfix >c0ainfix -V1c1Iainfix <=c0ainfix +ainfix *c2V1c1Lamk arrayainfix +ainfix *c2V1c1aconstaNilIainfix >=ainfix +ainfix *c2V1c1c0Iainfix <=c0V1Aagood_dataV8V9V0amk arrayV1V2FAagood_hashamk arrayV1V2V10Iainfix <V10V1Aainfix <=c0V10FAainfix <c0V1F"> <label @@ -497,7 +497,7 @@ prover="0" timelimit="5" memlimit="1000" - obsolete="true" + obsolete="false" archived="false"> <result status="valid" time="0.02"/> </proof> @@ -508,7 +508,7 @@ loclnum="56" loccnumb="6" loccnume="12" expl="14. type invariant" sum="82e3b0da9114a04219af882fc34a30ec" - proved="false" + proved="true" expanded="false" shape="ainfix <=c0V4Iainfix =V5aconstaNilAainfix =V4ainfix +ainfix *c2V1c1FIainfix >c0ainfix -V1c1Iainfix <=c0ainfix +ainfix *c2V1c1Lamk arrayainfix +ainfix *c2V1c1aconstaNilIainfix >=ainfix +ainfix *c2V1c1c0Iainfix <=c0V1Aagood_dataV6V7V0amk arrayV1V2FAagood_hashamk arrayV1V2V8Iainfix <V8V1Aainfix <=c0V8FAainfix <c0V1F"> <label @@ -517,7 +517,7 @@ prover="0" timelimit="5" memlimit="1000" - obsolete="true" + obsolete="false" archived="false"> <result status="valid" time="0.02"/> </proof> @@ -528,7 +528,7 @@ loclnum="56" loccnumb="6" loccnume="12" expl="15. loop invariant init" sum="6661c47771a13dda2b1cea0eed8ff4a4" - proved="false" + proved="true" expanded="false" shape="agood_hashV3V4Iainfix <V4ainfix +ainfix *c2V1c1Aainfix <=c0V4FIainfix <=c0ainfix -V1c1Iainfix <=c0ainfix +ainfix *c2V1c1Lamk arrayainfix +ainfix *c2V1c1aconstaNilIainfix >=ainfix +ainfix *c2V1c1c0Iainfix <=c0V1Aagood_dataV5V6V0amk arrayV1V2FAagood_hashamk arrayV1V2V7Iainfix <V7V1Aainfix <=c0V7FAainfix <c0V1F"> <label @@ -537,7 +537,7 @@ prover="0" timelimit="5" memlimit="1000" - obsolete="true" + obsolete="false" archived="false"> <result status="valid" time="0.06"/> </proof> @@ -548,7 +548,7 @@ loclnum="56" loccnumb="6" loccnume="12" expl="16. loop invariant init" sum="42237536111a31f18de665ba58d99529" - proved="false" + proved="true" expanded="false" shape="iainfix <abucketV4V1c0Aainfix <=c0abucketV4V1agood_dataV4V5V0V3ain_dataV4V5V3NFIainfix <=c0ainfix -V1c1Iainfix <=c0ainfix +ainfix *c2V1c1Lamk arrayainfix +ainfix *c2V1c1aconstaNilIainfix >=ainfix +ainfix *c2V1c1c0Iainfix <=c0V1Aagood_dataV6V7V0amk arrayV1V2FAagood_hashamk arrayV1V2V8Iainfix <V8V1Aainfix <=c0V8FAainfix <c0V1F"> <label @@ -557,9 +557,9 @@ prover="0" timelimit="5" memlimit="1000" - obsolete="true" + obsolete="false" archived="false"> - <result status="valid" time="1.27"/> + <result status="valid" time="0.47"/> </proof> </goal> <goal @@ -568,7 +568,7 @@ loclnum="56" loccnumb="6" loccnume="12" expl="17. precondition" sum="829c755c991a444ef572ff369e1e078e" - proved="false" + proved="true" expanded="false" shape="ainfix <V6V1Aainfix <=c0V6Iiainfix <abucketV7V1V6Aainfix <=c0abucketV7V1agood_dataV7V8V0V5ain_dataV7V8V5NFAagood_hashV5V9Iainfix <V9ainfix +ainfix *c2V1c1Aainfix <=c0V9FIainfix <=V6ainfix -V1c1Aainfix <=c0V6FLamk arrayainfix +ainfix *c2V1c1V4FIainfix <=c0ainfix -V1c1Iainfix <=c0ainfix +ainfix *c2V1c1Lamk arrayainfix +ainfix *c2V1c1aconstaNilIainfix >=ainfix +ainfix *c2V1c1c0Iainfix <=c0V1Aagood_dataV10V11V0amk arrayV1V2FAagood_hashamk arrayV1V2V12Iainfix <V12V1Aainfix <=c0V12FAainfix <c0V1F"> <label @@ -577,7 +577,7 @@ prover="0" timelimit="5" memlimit="1000" - obsolete="true" + obsolete="false" archived="false"> <result status="valid" time="0.02"/> </proof> @@ -588,7 +588,7 @@ loclnum="56" loccnumb="6" loccnume="12" expl="18. type invariant" sum="32ad2059ba5233837a05d309d5a2b788" - proved="false" + proved="true" expanded="false" shape="ainfix <=c0ainfix +ainfix *c2V1c1LagetV2V6Iainfix <V6V1Aainfix <=c0V6Iiainfix <abucketV8V1V6Aainfix <=c0abucketV8V1agood_dataV8V9V0V5ain_dataV8V9V5NFAagood_hashV5V10Iainfix <V10ainfix +ainfix *c2V1c1Aainfix <=c0V10FIainfix <=V6ainfix -V1c1Aainfix <=c0V6FLamk arrayainfix +ainfix *c2V1c1V4FIainfix <=c0ainfix -V1c1Iainfix <=c0ainfix +ainfix *c2V1c1Lamk arrayainfix +ainfix *c2V1c1aconstaNilIainfix >=ainfix +ainfix *c2V1c1c0Iainfix <=c0V1Aagood_dataV11V12V0amk arrayV1V2FAagood_hashamk arrayV1V2V13Iainfix <V13V1Aainfix <=c0V13FAainfix <c0V1F"> <label @@ -597,7 +597,7 @@ prover="0" timelimit="5" memlimit="1000" - obsolete="true" + obsolete="false" archived="false"> <result status="valid" time="0.02"/> </proof> @@ -608,14 +608,14 @@ loclnum="56" loccnumb="6" loccnume="12" expl="19. precondition" sum="ad14949252824f7e5f1dee41b1671612" - proved="false" + proved="true" expanded="false" shape="ainfix =abucketV8V1V6IamemaTuple2V8V9V7FIainfix <=c0ainfix +ainfix *c2V1c1LagetV2V6Iainfix <V6V1Aainfix <=c0V6Iiainfix <abucketV10V1V6Aainfix <=c0abucketV10V1agood_dataV10V11V0V5ain_dataV10V11V5NFAagood_hashV5V12Iainfix <V12ainfix +ainfix *c2V1c1Aainfix <=c0V12FIainfix <=V6ainfix -V1c1Aainfix <=c0V6FLamk arrayainfix +ainfix *c2V1c1V4FIainfix <=c0ainfix -V1c1Iainfix <=c0ainfix +ainfix *c2V1c1Lamk arrayainfix +ainfix *c2V1c1aconstaNilIainfix >=ainfix +ainfix *c2V1c1c0Iainfix <=c0V1Aagood_dataV13V14V0amk arrayV1V2FAagood_hashamk arrayV1V2V15Iainfix <V15V1Aainfix <=c0V15FAainfix <c0V1F"> <label name="expl:VC for resize"/> <transf name="inline_all" - proved="false" + proved="true" expanded="false"> <goal name="WP_parameter resize.19.1" @@ -623,7 +623,7 @@ loclnum="56" loccnumb="6" loccnume="12" expl="1. precondition" sum="db9c54dcc70095700a6706e6b9beda68" - proved="false" + proved="true" expanded="false" shape="ainfix =amodahashV8V1V6IamemaTuple2V8V9V7FIainfix =c0ainfix +ainfix *c2V1c1Oainfix <c0ainfix +ainfix *c2V1c1LagetV2V6Iainfix <V6V1Aainfix =c0V6Oainfix <c0V6Iiainfix <amodahashV10V1V6Aainfix =c0amodahashV10V1Oainfix <c0amodahashV10V1amemaTuple2V10V11agetaeltsV5amodahashV10alengthV5qainfix =agetV0V10aSomeV11amemaTuple2V10V11agetaeltsV5amodahashV10alengthV5NFAainfix =amodahashV13alengthV5V12IamemaTuple2V13V14agetaeltsV5V12FIainfix <V12ainfix +ainfix *c2V1c1Aainfix =c0V12Oainfix <c0V12FIainfix =V6ainfix +V1aprefix -c1Oainfix <V6ainfix +V1aprefix -c1Aainfix =c0V6Oainfix <c0V6FLamk arrayainfix +ainfix *c2V1c1V4FIainfix =c0ainfix +V1aprefix -c1Oainfix <c0ainfix +V1aprefix -c1Iainfix =c0ainfix +ainfix *c2V1c1Oainfix <c0ainfix +ainfix *c2V1c1Lamk arrayainfix +ainfix *c2V1c1aconstaNilIainfix =c0ainfix +ainfix *c2V1c1Oainfix <c0ainfix +ainfix *c2V1c1Iainfix =c0V1Oainfix <c0V1AamemaTuple2V15V16agetaeltsamk arrayV1V2amodahashV15alengthamk arrayV1V2qainfix =agetV0V15aSomeV16FAainfix =amodahashV18alengthamk arrayV1V2V17IamemaTuple2V18V19agetaeltsamk arrayV1V2V17FIainfix <V17V1Aainfix =c0V17Oainfix <c0V17FAainfix <c0V1F"> <label @@ -632,7 +632,7 @@ prover="2" timelimit="5" memlimit="1000" - obsolete="true" + obsolete="false" archived="false"> <result status="valid" time="0.15"/> </proof> @@ -645,7 +645,7 @@ loclnum="56" loccnumb="6" loccnume="12" expl="20. precondition" sum="49d78a9a6ccefaa92a4ba7c4848f3db2" - proved="false" + proved="true" expanded="false" shape="agood_hashV5V8Iainfix <V8ainfix +ainfix *c2V1c1Aainfix <=c0V8FIainfix <=c0ainfix +ainfix *c2V1c1LagetV2V6Iainfix <V6V1Aainfix <=c0V6Iiainfix <abucketV9V1V6Aainfix <=c0abucketV9V1agood_dataV9V10V0V5ain_dataV9V10V5NFAagood_hashV5V11Iainfix <V11ainfix +ainfix *c2V1c1Aainfix <=c0V11FIainfix <=V6ainfix -V1c1Aainfix <=c0V6FLamk arrayainfix +ainfix *c2V1c1V4FIainfix <=c0ainfix -V1c1Iainfix <=c0ainfix +ainfix *c2V1c1Lamk arrayainfix +ainfix *c2V1c1aconstaNilIainfix >=ainfix +ainfix *c2V1c1c0Iainfix <=c0V1Aagood_dataV12V13V0amk arrayV1V2FAagood_hashamk arrayV1V2V14Iainfix <V14V1Aainfix <=c0V14FAainfix <c0V1F"> <label @@ -654,7 +654,7 @@ prover="0" timelimit="5" memlimit="1000" - obsolete="true" + obsolete="false" archived="false"> <result status="valid" time="0.04"/> </proof> @@ -665,14 +665,14 @@ loclnum="56" loccnumb="6" loccnume="12" expl="21. precondition" sum="5a30725957b5c08265364046976dc2ce" - proved="false" + proved="true" expanded="false" shape="iainfix <abucketV8V1V6Aainfix <=c0abucketV8V1agood_dataV8V9V0V5iainfix =abucketV8V1V6ain_dataV8V9V5OamemaTuple2V8V9V7qainfix =agetV0V8aSomeV9ain_dataV8V9V5NFIainfix <=c0ainfix +ainfix *c2V1c1LagetV2V6Iainfix <V6V1Aainfix <=c0V6Iiainfix <abucketV10V1V6Aainfix <=c0abucketV10V1agood_dataV10V11V0V5ain_dataV10V11V5NFAagood_hashV5V12Iainfix <V12ainfix +ainfix *c2V1c1Aainfix <=c0V12FIainfix <=V6ainfix -V1c1Aainfix <=c0V6FLamk arrayainfix +ainfix *c2V1c1V4FIainfix <=c0ainfix -V1c1Iainfix <=c0ainfix +ainfix *c2V1c1Lamk arrayainfix +ainfix *c2V1c1aconstaNilIainfix >=ainfix +ainfix *c2V1c1c0Iainfix <=c0V1Aagood_dataV13V14V0amk arrayV1V2FAagood_hashamk arrayV1V2V15Iainfix <V15V1Aainfix <=c0V15FAainfix <c0V1F"> <label name="expl:VC for resize"/> <transf name="inline_all" - proved="false" + proved="true" expanded="false"> <goal name="WP_parameter resize.21.1" @@ -680,7 +680,7 @@ loclnum="56" loccnumb="6" loccnume="12" expl="1. precondition" sum="bf54516eaab767cb027c2f623053c128" - proved="false" + proved="true" expanded="false" shape="iainfix <amodahashV8V1V6Aainfix =c0amodahashV8V1Oainfix <c0amodahashV8V1amemaTuple2V8V9agetaeltsV5amodahashV8alengthV5qainfix =agetV0V8aSomeV9iainfix =amodahashV8V1V6amemaTuple2V8V9agetaeltsV5amodahashV8alengthV5OamemaTuple2V8V9V7qainfix =agetV0V8aSomeV9amemaTuple2V8V9agetaeltsV5amodahashV8alengthV5NFIainfix =c0ainfix +ainfix *c2V1c1Oainfix <c0ainfix +ainfix *c2V1c1LagetV2V6Iainfix <V6V1Aainfix =c0V6Oainfix <c0V6Iiainfix <amodahashV10V1V6Aainfix =c0amodahashV10V1Oainfix <c0amodahashV10V1amemaTuple2V10V11agetaeltsV5amodahashV10alengthV5qainfix =agetV0V10aSomeV11amemaTuple2V10V11agetaeltsV5amodahashV10alengthV5NFAainfix =amodahashV13alengthV5V12IamemaTuple2V13V14agetaeltsV5V12FIainfix <V12ainfix +ainfix *c2V1c1Aainfix =c0V12Oainfix <c0V12FIainfix =V6ainfix +V1aprefix -c1Oainfix <V6ainfix +V1aprefix -c1Aainfix =c0V6Oainfix <c0V6FLamk arrayainfix +ainfix *c2V1c1V4FIainfix =c0ainfix +V1aprefix -c1Oainfix <c0ainfix +V1aprefix -c1Iainfix =c0ainfix +ainfix *c2V1c1Oainfix <c0ainfix +ainfix *c2V1c1Lamk arrayainfix +ainfix *c2V1c1aconstaNilIainfix =c0ainfix +ainfix *c2V1c1Oainfix <c0ainfix +ainfix *c2V1c1Iainfix =c0V1Oainfix <c0V1AamemaTuple2V15V16agetaeltsamk arrayV1V2amodahashV15alengthamk arrayV1V2qainfix =agetV0V15aSomeV16FAainfix =amodahashV18alengthamk arrayV1V2V17IamemaTuple2V18V19agetaeltsamk arrayV1V2V17FIainfix <V17V1Aainfix =c0V17Oainfix <c0V17FAainfix <c0V1F"> <label @@ -689,15 +689,15 @@ prover="0" timelimit="5" memlimit="1000" - obsolete="true" + obsolete="false" archived="false"> - <result status="valid" time="5.27"/> + <result status="valid" time="2.11"/> </proof> <proof prover="2" timelimit="5" memlimit="1000" - obsolete="true" + obsolete="false" archived="false"> <result status="valid" time="0.08"/> </proof> @@ -710,7 +710,7 @@ loclnum="56" loccnumb="6" loccnume="12" expl="22. loop invariant preservation" sum="b8c450ee09c16be05f26799866e2a63d" - proved="false" + proved="true" expanded="false" shape="agood_hashV9V10Iainfix <V10ainfix +ainfix *c2V1c1Aainfix <=c0V10FIiainfix <=abucketV11V1V6Aainfix <=c0abucketV11V1agood_dataV11V12V0V9ain_dataV11V12V9NFAagood_hashV9V13Iainfix <V13ainfix +ainfix *c2V1c1Aainfix <=c0V13FAainfix <=c0ainfix +ainfix *c2V1c1Lamk arrayainfix +ainfix *c2V1c1V8FIiainfix <abucketV14V1V6Aainfix <=c0abucketV14V1agood_dataV14V15V0V5iainfix =abucketV14V1V6ain_dataV14V15V5OamemaTuple2V14V15V7qainfix =agetV0V14aSomeV15ain_dataV14V15V5NFAagood_hashV5V16Iainfix <V16ainfix +ainfix *c2V1c1Aainfix <=c0V16FAainfix =abucketV17V1V6IamemaTuple2V17V18V7FAainfix <=c0ainfix +ainfix *c2V1c1LagetV2V6Iainfix <V6V1Aainfix <=c0V6Iiainfix <abucketV19V1V6Aainfix <=c0abucketV19V1agood_dataV19V20V0V5ain_dataV19V20V5NFAagood_hashV5V21Iainfix <V21ainfix +ainfix *c2V1c1Aainfix <=c0V21FIainfix <=V6ainfix -V1c1Aainfix <=c0V6FLamk arrayainfix +ainfix *c2V1c1V4FIainfix <=c0ainfix -V1c1Iainfix <=c0ainfix +ainfix *c2V1c1Lamk arrayainfix +ainfix *c2V1c1aconstaNilIainfix >=ainfix +ainfix *c2V1c1c0Iainfix <=c0V1Aagood_dataV22V23V0amk arrayV1V2FAagood_hashamk arrayV1V2V24Iainfix <V24V1Aainfix <=c0V24FAainfix <c0V1F"> <label @@ -719,7 +719,7 @@ prover="0" timelimit="5" memlimit="1000" - obsolete="true" + obsolete="false" archived="false"> <result status="valid" time="0.02"/> </proof> @@ -730,7 +730,7 @@ loclnum="56" loccnumb="6" loccnume="12" expl="23. loop invariant preservation" sum="3f2bf1a4e1435a44e8dffbee7df00d79" - proved="false" + proved="true" expanded="false" shape="iainfix <abucketV10V1ainfix +V6c1Aainfix <=c0abucketV10V1agood_dataV10V11V0V9ain_dataV10V11V9NFIiainfix <=abucketV12V1V6Aainfix <=c0abucketV12V1agood_dataV12V13V0V9ain_dataV12V13V9NFAagood_hashV9V14Iainfix <V14ainfix +ainfix *c2V1c1Aainfix <=c0V14FAainfix <=c0ainfix +ainfix *c2V1c1Lamk arrayainfix +ainfix *c2V1c1V8FIiainfix <abucketV15V1V6Aainfix <=c0abucketV15V1agood_dataV15V16V0V5iainfix =abucketV15V1V6ain_dataV15V16V5OamemaTuple2V15V16V7qainfix =agetV0V15aSomeV16ain_dataV15V16V5NFAagood_hashV5V17Iainfix <V17ainfix +ainfix *c2V1c1Aainfix <=c0V17FAainfix =abucketV18V1V6IamemaTuple2V18V19V7FAainfix <=c0ainfix +ainfix *c2V1c1LagetV2V6Iainfix <V6V1Aainfix <=c0V6Iiainfix <abucketV20V1V6Aainfix <=c0abucketV20V1agood_dataV20V21V0V5ain_dataV20V21V5NFAagood_hashV5V22Iainfix <V22ainfix +ainfix *c2V1c1Aainfix <=c0V22FIainfix <=V6ainfix -V1c1Aainfix <=c0V6FLamk arrayainfix +ainfix *c2V1c1V4FIainfix <=c0ainfix -V1c1Iainfix <=c0ainfix +ainfix *c2V1c1Lamk arrayainfix +ainfix *c2V1c1aconstaNilIainfix >=ainfix +ainfix *c2V1c1c0Iainfix <=c0V1Aagood_dataV23V24V0amk arrayV1V2FAagood_hashamk arrayV1V2V25Iainfix <V25V1Aainfix <=c0V25FAainfix <c0V1F"> <label @@ -739,7 +739,7 @@ prover="0" timelimit="5" memlimit="1000" - obsolete="true" + obsolete="false" archived="false"> <result status="valid" time="0.07"/> </proof> @@ -750,7 +750,7 @@ loclnum="56" loccnumb="6" loccnume="12" expl="24. type invariant" sum="d6d37eff6c940b7f4de6d609e65c1a35" - proved="false" + proved="true" expanded="false" shape="ainfix <c0V6Iainfix =V7V4Aainfix =V6ainfix +ainfix *c2V1c1FIiainfix <abucketV8V1ainfix +ainfix -V1c1c1Aainfix <=c0abucketV8V1agood_dataV8V9V0V5ain_dataV8V9V5NFAagood_hashV5V10Iainfix <V10ainfix +ainfix *c2V1c1Aainfix <=c0V10FLamk arrayainfix +ainfix *c2V1c1V4FIainfix <=c0ainfix -V1c1Iainfix <=c0ainfix +ainfix *c2V1c1Lamk arrayainfix +ainfix *c2V1c1aconstaNilIainfix >=ainfix +ainfix *c2V1c1c0Iainfix <=c0V1Aagood_dataV11V12V0amk arrayV1V2FAagood_hashamk arrayV1V2V13Iainfix <V13V1Aainfix <=c0V13FAainfix <c0V1F"> <label @@ -759,7 +759,7 @@ prover="0" timelimit="5" memlimit="1000" - obsolete="true" + obsolete="false" archived="false"> <result status="valid" time="0.01"/> </proof> @@ -770,7 +770,7 @@ loclnum="56" loccnumb="6" loccnume="12" expl="25. type invariant" sum="15a059687741de477aafab3c2e3b00b9" - proved="false" + proved="true" expanded="false" shape="agood_hashamk arrayV6V7V8Iainfix <V8V6Aainfix <=c0V8FIainfix =V7V4Aainfix =V6ainfix +ainfix *c2V1c1FIiainfix <abucketV9V1ainfix +ainfix -V1c1c1Aainfix <=c0abucketV9V1agood_dataV9V10V0V5ain_dataV9V10V5NFAagood_hashV5V11Iainfix <V11ainfix +ainfix *c2V1c1Aainfix <=c0V11FLamk arrayainfix +ainfix *c2V1c1V4FIainfix <=c0ainfix -V1c1Iainfix <=c0ainfix +ainfix *c2V1c1Lamk arrayainfix +ainfix *c2V1c1aconstaNilIainfix >=ainfix +ainfix *c2V1c1c0Iainfix <=c0V1Aagood_dataV12V13V0amk arrayV1V2FAagood_hashamk arrayV1V2V14Iainfix <V14V1Aainfix <=c0V14FAainfix <c0V1F"> <label @@ -779,7 +779,7 @@ prover="0" timelimit="5" memlimit="1000" - obsolete="true" + obsolete="false" archived="false"> <result status="valid" time="0.07"/> </proof> @@ -790,7 +790,7 @@ loclnum="56" loccnumb="6" loccnume="12" expl="26. type invariant" sum="c31d8aa742dfef8b81d3cb5da88bd5d0" - proved="false" + proved="true" expanded="false" shape="agood_dataV8V9V0amk arrayV6V7FIainfix =V7V4Aainfix =V6ainfix +ainfix *c2V1c1FIiainfix <abucketV10V1ainfix +ainfix -V1c1c1Aainfix <=c0abucketV10V1agood_dataV10V11V0V5ain_dataV10V11V5NFAagood_hashV5V12Iainfix <V12ainfix +ainfix *c2V1c1Aainfix <=c0V12FLamk arrayainfix +ainfix *c2V1c1V4FIainfix <=c0ainfix -V1c1Iainfix <=c0ainfix +ainfix *c2V1c1Lamk arrayainfix +ainfix *c2V1c1aconstaNilIainfix >=ainfix +ainfix *c2V1c1c0Iainfix <=c0V1Aagood_dataV13V14V0amk arrayV1V2FAagood_hashamk arrayV1V2V15Iainfix <V15V1Aainfix <=c0V15FAainfix <c0V1F"> <label @@ -799,9 +799,9 @@ prover="0" timelimit="5" memlimit="1000" - obsolete="true" + obsolete="false" archived="false"> - <result status="valid" time="0.32"/> + <result status="valid" time="0.14"/> </proof> </goal> <goal @@ -810,7 +810,7 @@ loclnum="56" loccnumb="6" loccnume="12" expl="27. type invariant" sum="3f8f75a3561506eb0c92c64ffd2bf313" - proved="false" + proved="true" expanded="false" shape="ainfix <=c0V6Iainfix =V7V4Aainfix =V6ainfix +ainfix *c2V1c1FIiainfix <abucketV8V1ainfix +ainfix -V1c1c1Aainfix <=c0abucketV8V1agood_dataV8V9V0V5ain_dataV8V9V5NFAagood_hashV5V10Iainfix <V10ainfix +ainfix *c2V1c1Aainfix <=c0V10FLamk arrayainfix +ainfix *c2V1c1V4FIainfix <=c0ainfix -V1c1Iainfix <=c0ainfix +ainfix *c2V1c1Lamk arrayainfix +ainfix *c2V1c1aconstaNilIainfix >=ainfix +ainfix *c2V1c1c0Iainfix <=c0V1Aagood_dataV11V12V0amk arrayV1V2FAagood_hashamk arrayV1V2V13Iainfix <V13V1Aainfix <=c0V13FAainfix <c0V1F"> <label @@ -819,7 +819,7 @@ prover="0" timelimit="5" memlimit="1000" - obsolete="true" + obsolete="false" archived="false"> <result status="valid" time="0.02"/> </proof> @@ -878,7 +878,7 @@ memlimit="1000" obsolete="false" archived="false"> - <result status="valid" time="0.20"/> + <result status="valid" time="0.02"/> </proof> </goal> <goal @@ -899,7 +899,7 @@ edited="hashtbl_impl_HashtblImpl_WP_parameter_find_1.v" obsolete="false" archived="false"> - <result status="valid" time="1.97"/> + <result status="valid" time="0.68"/> </proof> </goal> </transf> @@ -1090,7 +1090,7 @@ edited="hashtbl_impl_HashtblImpl_WP_parameter_remove_1.v" obsolete="false" archived="false"> - <result status="valid" time="1.90"/> + <result status="valid" time="0.61"/> </proof> </goal> <goal @@ -1254,7 +1254,7 @@ memlimit="1000" obsolete="false" archived="false"> - <result status="valid" time="1.64"/> + <result status="valid" time="0.44"/> </proof> </goal> </transf> @@ -1359,14 +1359,14 @@ loclnum="137" loccnumb="6" loccnume="9" expl="VC for add" sum="5e773205ee8042e7a48ce2cd11636201" - proved="false" + proved="true" expanded="true" shape="ainfix =agetV12V13agetV2V13Iainfix =V13V0NFAainfix =agetV12V0aSomeV1Aainfix <=c0V5Aagood_dataV14V15V12amk arrayV5V10FAagood_hashamk arrayV5V10V16Iainfix <V16V5Aainfix <=c0V16FAainfix <c0V5Iainfix =V12asetV7V0aSomeV1FIainfix =V11ainfix +V9c1FIainfix =V10asetV8abucketV0V5aConsaTuple2V0V1agetV8abucketV0V5Aainfix <=c0V5FAainfix <abucketV0V5V5Aainfix <=c0abucketV0V5Aainfix <abucketV0V5V5Aainfix <=c0abucketV0V5Iainfix =agetV7V17agetV2V17Iainfix =V17V0NFAainfix =agetV7V0aNoneAainfix <=c0V5Aagood_dataV18V19V7amk arrayV5V8FAagood_hashamk arrayV5V8V20Iainfix <V20V5Aainfix <=c0V20FAainfix <c0V5FIainfix <=c0V5Aagood_dataV21V22V2amk arrayV5V6FAagood_hashamk arrayV5V6V23Iainfix <V23V5Aainfix <=c0V23FAainfix <c0V5FIainfix <=c0V3Aagood_dataV24V25V2amk arrayV3V4FAagood_hashamk arrayV3V4V26Iainfix <V26V3Aainfix <=c0V26FAainfix <c0V3FF"> <label name="expl:VC for add"/> <transf name="split_goal_wp" - proved="false" + proved="true" expanded="true"> <goal name="WP_parameter add.1" @@ -1470,7 +1470,7 @@ edited="hashtbl_impl_HashtblImpl_WP_parameter_add_1.v" obsolete="false" archived="false"> - <result status="valid" time="5.68"/> + <result status="valid" time="1.65"/> </proof> </goal> <goal @@ -1479,14 +1479,14 @@ loclnum="137" loccnumb="6" loccnume="9" expl="5. type invariant" sum="f8c0fe7b7f7e09146102c04e89414436" - proved="false" + proved="true" expanded="false" shape="agood_dataV13V14V12amk arrayV5V10FIainfix =V12asetV7V0aSomeV1FIainfix =V11ainfix +V9c1FIainfix =V10asetV8abucketV0V5aConsaTuple2V0V1agetV8abucketV0V5Aainfix <=c0V5FIainfix <abucketV0V5V5Aainfix <=c0abucketV0V5Iainfix <abucketV0V5V5Aainfix <=c0abucketV0V5Iainfix =agetV7V15agetV2V15Iainfix =V15V0NFAainfix =agetV7V0aNoneAainfix <=c0V5Aagood_dataV16V17V7amk arrayV5V8FAagood_hashamk arrayV5V8V18Iainfix <V18V5Aainfix <=c0V18FAainfix <c0V5FIainfix <=c0V5Aagood_dataV19V20V2amk arrayV5V6FAagood_hashamk arrayV5V6V21Iainfix <V21V5Aainfix <=c0V21FAainfix <c0V5FIainfix <=c0V3Aagood_dataV22V23V2amk arrayV3V4FAagood_hashamk arrayV3V4V24Iainfix <V24V3Aainfix <=c0V24FAainfix <c0V3FF"> <label name="expl:VC for add"/> <transf name="inline_all" - proved="false" + proved="true" expanded="false"> <goal name="WP_parameter add.5.1" @@ -1494,14 +1494,14 @@ loclnum="137" loccnumb="6" loccnume="9" expl="1. type invariant" sum="ed72a448e60a0d009d3cc9e938613982" - proved="false" + proved="true" expanded="false" shape="amemaTuple2V13V14agetaeltsamk arrayV5V10amodahashV13alengthamk arrayV5V10qainfix =agetV12V13aSomeV14FIainfix =V12asetV7V0aSomeV1FIainfix =V11ainfix +V9c1FIainfix =V10asetV8amodahashV0V5aConsaTuple2V0V1agetV8amodahashV0V5Aainfix =c0V5Oainfix <c0V5FIainfix <amodahashV0V5V5Aainfix =c0amodahashV0V5Oainfix <c0amodahashV0V5Iainfix <amodahashV0V5V5Aainfix =c0amodahashV0V5Oainfix <c0amodahashV0V5Iainfix =agetV7V15agetV2V15Iainfix =V15V0NFAainfix =agetV7V0aNoneAainfix =c0V5Oainfix <c0V5AamemaTuple2V16V17agetaeltsamk arrayV5V8amodahashV16alengthamk arrayV5V8qainfix =agetV7V16aSomeV17FAainfix =amodahashV19alengthamk arrayV5V8V18IamemaTuple2V19V20agetaeltsamk arrayV5V8V18FIainfix <V18V5Aainfix =c0V18Oainfix <c0V18FAainfix <c0V5FIainfix =c0V5Oainfix <c0V5AamemaTuple2V21V22agetaeltsamk arrayV5V6amodahashV21alengthamk arrayV5V6qainfix =agetV2V21aSomeV22FAainfix =amodahashV24alengthamk arrayV5V6V23IamemaTuple2V24V25agetaeltsamk arrayV5V6V23FIainfix <V23V5Aainfix =c0V23Oainfix <c0V23FAainfix <c0V5FIainfix =c0V3Oainfix <c0V3AamemaTuple2V26V27agetaeltsamk arrayV3V4amodahashV26alengthamk arrayV3V4qainfix =agetV2V26aSomeV27FAainfix =amodahashV29alengthamk arrayV3V4V28IamemaTuple2V29V30agetaeltsamk arrayV3V4V28FIainfix <V28V3Aainfix =c0V28Oainfix <c0V28FAainfix <c0V3FF"> <label name="expl:VC for add"/> <transf name="split_goal_wp" - proved="false" + proved="true" expanded="false"> <goal name="WP_parameter add.5.1.1" @@ -1509,7 +1509,7 @@ loclnum="137" loccnumb="6" loccnume="9" expl="1. type invariant" sum="e02543ad4e7121e2b81a1e14756a4745" - proved="false" + proved="true" expanded="false" shape="amemaTuple2V13V14agetaeltsamk arrayV5V10amodahashV13alengthamk arrayV5V10Iainfix =agetV12V13aSomeV14FIainfix =V12asetV7V0aSomeV1FIainfix =V11ainfix +V9c1FIainfix =V10asetV8amodahashV0V5aConsaTuple2V0V1agetV8amodahashV0V5Aainfix =c0V5Oainfix <c0V5FIainfix <amodahashV0V5V5Aainfix =c0amodahashV0V5Oainfix <c0amodahashV0V5Iainfix <amodahashV0V5V5Aainfix =c0amodahashV0V5Oainfix <c0amodahashV0V5Iainfix =agetV7V15agetV2V15Iainfix =V15V0NFAainfix =agetV7V0aNoneAainfix =c0V5Oainfix <c0V5AamemaTuple2V16V17agetaeltsamk arrayV5V8amodahashV16alengthamk arrayV5V8qainfix =agetV7V16aSomeV17FAainfix =amodahashV19alengthamk arrayV5V8V18IamemaTuple2V19V20agetaeltsamk arrayV5V8V18FIainfix <V18V5Aainfix =c0V18Oainfix <c0V18FAainfix <c0V5FIainfix =c0V5Oainfix <c0V5AamemaTuple2V21V22agetaeltsamk arrayV5V6amodahashV21alengthamk arrayV5V6qainfix =agetV2V21aSomeV22FAainfix =amodahashV24alengthamk arrayV5V6V23IamemaTuple2V24V25agetaeltsamk arrayV5V6V23FIainfix <V23V5Aainfix =c0V23Oainfix <c0V23FAainfix <c0V5FIainfix =c0V3Oainfix <c0V3AamemaTuple2V26V27agetaeltsamk arrayV3V4amodahashV26alengthamk arrayV3V4qainfix =agetV2V26aSomeV27FAainfix =amodahashV29alengthamk arrayV3V4V28IamemaTuple2V29V30agetaeltsamk arrayV3V4V28FIainfix <V28V3Aainfix =c0V28Oainfix <c0V28FAainfix <c0V3FF"> <label @@ -1518,9 +1518,9 @@ prover="1" timelimit="20" memlimit="1000" - obsolete="true" + obsolete="false" archived="false"> - <result status="valid" time="3.24"/> + <result status="valid" time="0.90"/> </proof> </goal> <goal @@ -1529,7 +1529,7 @@ loclnum="137" loccnumb="6" loccnume="9" expl="2. type invariant" sum="93fa4a4153a4999f4be6da8d2a2976c0" - proved="false" + proved="true" expanded="false" shape="ainfix =agetV12V13aSomeV14IamemaTuple2V13V14agetaeltsamk arrayV5V10amodahashV13alengthamk arrayV5V10FIainfix =V12asetV7V0aSomeV1FIainfix =V11ainfix +V9c1FIainfix =V10asetV8amodahashV0V5aConsaTuple2V0V1agetV8amodahashV0V5Aainfix =c0V5Oainfix <c0V5FIainfix <amodahashV0V5V5Aainfix =c0amodahashV0V5Oainfix <c0amodahashV0V5Iainfix <amodahashV0V5V5Aainfix =c0amodahashV0V5Oainfix <c0amodahashV0V5Iainfix =agetV7V15agetV2V15Iainfix =V15V0NFAainfix =agetV7V0aNoneAainfix =c0V5Oainfix <c0V5AamemaTuple2V16V17agetaeltsamk arrayV5V8amodahashV16alengthamk arrayV5V8qainfix =agetV7V16aSomeV17FAainfix =amodahashV19alengthamk arrayV5V8V18IamemaTuple2V19V20agetaeltsamk arrayV5V8V18FIainfix <V18V5Aainfix =c0V18Oainfix <c0V18FAainfix <c0V5FIainfix =c0V5Oainfix <c0V5AamemaTuple2V21V22agetaeltsamk arrayV5V6amodahashV21alengthamk arrayV5V6qainfix =agetV2V21aSomeV22FAainfix =amodahashV24alengthamk arrayV5V6V23IamemaTuple2V24V25agetaeltsamk arrayV5V6V23FIainfix <V23V5Aainfix =c0V23Oainfix <c0V23FAainfix <c0V5FIainfix =c0V3Oainfix <c0V3AamemaTuple2V26V27agetaeltsamk arrayV3V4amodahashV26alengthamk arrayV3V4qainfix =agetV2V26aSomeV27FAainfix =amodahashV29alengthamk arrayV3V4V28IamemaTuple2V29V30agetaeltsamk arrayV3V4V28FIainfix <V28V3Aainfix =c0V28Oainfix <c0V28FAainfix <c0V3FF"> <label @@ -1538,9 +1538,9 @@ prover="1" timelimit="20" memlimit="1000" - obsolete="true" + obsolete="false" archived="false"> - <result status="valid" time="4.02"/> + <result status="valid" time="1.12"/> </proof> </goal> </transf> @@ -1581,14 +1581,14 @@ loclnum="137" loccnumb="6" loccnume="9" expl="7. postcondition" sum="4a8a1ff4cadd693cef1624e070b87343" - proved="false" + proved="true" expanded="false" shape="ainfix =agetV12V0aSomeV1Iainfix <=c0V5Aagood_dataV13V14V12amk arrayV5V10FAagood_hashamk arrayV5V10V15Iainfix <V15V5Aainfix <=c0V15FAainfix <c0V5Iainfix =V12asetV7V0aSomeV1FIainfix =V11ainfix +V9c1FIainfix =V10asetV8abucketV0V5aConsaTuple2V0V1agetV8abucketV0V5Aainfix <=c0V5FIainfix <abucketV0V5V5Aainfix <=c0abucketV0V5Iainfix <abucketV0V5V5Aainfix <=c0abucketV0V5Iainfix =agetV7V16agetV2V16Iainfix =V16V0NFAainfix =agetV7V0aNoneAainfix <=c0V5Aagood_dataV17V18V7amk arrayV5V8FAagood_hashamk arrayV5V8V19Iainfix <V19V5Aainfix <=c0V19FAainfix <c0V5FIainfix <=c0V5Aagood_dataV20V21V2amk arrayV5V6FAagood_hashamk arrayV5V6V22Iainfix <V22V5Aainfix <=c0V22FAainfix <c0V5FIainfix <=c0V3Aagood_dataV23V24V2amk arrayV3V4FAagood_hashamk arrayV3V4V25Iainfix <V25V3Aainfix <=c0V25FAainfix <c0V3FF"> <label name="expl:VC for add"/> <transf name="inline_all" - proved="false" + proved="true" expanded="false"> <goal name="WP_parameter add.7.1" @@ -1596,7 +1596,7 @@ loclnum="137" loccnumb="6" loccnume="9" expl="1. postcondition" sum="858f6ad637571ed4f17f97b80c1c00de" - proved="false" + proved="true" expanded="false" shape="ainfix =agetV12V0aSomeV1Iainfix =c0V5Oainfix <c0V5AamemaTuple2V13V14agetaeltsamk arrayV5V10amodahashV13alengthamk arrayV5V10qainfix =agetV12V13aSomeV14FAainfix =amodahashV16alengthamk arrayV5V10V15IamemaTuple2V16V17agetaeltsamk arrayV5V10V15FIainfix <V15V5Aainfix =c0V15Oainfix <c0V15FAainfix <c0V5Iainfix =V12asetV7V0aSomeV1FIainfix =V11ainfix +V9c1FIainfix =V10asetV8amodahashV0V5aConsaTuple2V0V1agetV8amodahashV0V5Aainfix =c0V5Oainfix <c0V5FIainfix <amodahashV0V5V5Aainfix =c0amodahashV0V5Oainfix <c0amodahashV0V5Iainfix <amodahashV0V5V5Aainfix =c0amodahashV0V5Oainfix <c0amodahashV0V5Iainfix =agetV7V18agetV2V18Iainfix =V18V0NFAainfix =agetV7V0aNoneAainfix =c0V5Oainfix <c0V5AamemaTuple2V19V20agetaeltsamk arrayV5V8amodahashV19alengthamk arrayV5V8qainfix =agetV7V19aSomeV20FAainfix =amodahashV22alengthamk arrayV5V8V21IamemaTuple2V22V23agetaeltsamk arrayV5V8V21FIainfix <V21V5Aainfix =c0V21Oainfix <c0V21FAainfix <c0V5FIainfix =c0V5Oainfix <c0V5AamemaTuple2V24V25agetaeltsamk arrayV5V6amodahashV24alengthamk arrayV5V6qainfix =agetV2V24aSomeV25FAainfix =amodahashV27alengthamk arrayV5V6V26IamemaTuple2V27V28agetaeltsamk arrayV5V6V26FIainfix <V26V5Aainfix =c0V26Oainfix <c0V26FAainfix <c0V5FIainfix =c0V3Oainfix <c0V3AamemaTuple2V29V30agetaeltsamk arrayV3V4amodahashV29alengthamk arrayV3V4qainfix =agetV2V29aSomeV30FAainfix =amodahashV32alengthamk arrayV3V4V31IamemaTuple2V32V33agetaeltsamk arrayV3V4V31FIainfix <V31V3Aainfix =c0V31Oainfix <c0V31FAainfix <c0V3FF"> <label @@ -1605,7 +1605,7 @@ prover="0" timelimit="5" memlimit="1000" - obsolete="true" + obsolete="false" archived="false"> <result status="valid" time="0.04"/> </proof> @@ -1618,14 +1618,14 @@ loclnum="137" loccnumb="6" loccnume="9" expl="8. postcondition" sum="d8123c8d02d5c24fc8cddc76134b337a" - proved="false" + proved="true" expanded="false" shape="ainfix =agetV12V13agetV2V13Iainfix =V13V0NFIainfix <=c0V5Aagood_dataV14V15V12amk arrayV5V10FAagood_hashamk arrayV5V10V16Iainfix <V16V5Aainfix <=c0V16FAainfix <c0V5Iainfix =V12asetV7V0aSomeV1FIainfix =V11ainfix +V9c1FIainfix =V10asetV8abucketV0V5aConsaTuple2V0V1agetV8abucketV0V5Aainfix <=c0V5FIainfix <abucketV0V5V5Aainfix <=c0abucketV0V5Iainfix <abucketV0V5V5Aainfix <=c0abucketV0V5Iainfix =agetV7V17agetV2V17Iainfix =V17V0NFAainfix =agetV7V0aNoneAainfix <=c0V5Aagood_dataV18V19V7amk arrayV5V8FAagood_hashamk arrayV5V8V20Iainfix <V20V5Aainfix <=c0V20FAainfix <c0V5FIainfix <=c0V5Aagood_dataV21V22V2amk arrayV5V6FAagood_hashamk arrayV5V6V23Iainfix <V23V5Aainfix <=c0V23FAainfix <c0V5FIainfix <=c0V3Aagood_dataV24V25V2amk arrayV3V4FAagood_hashamk arrayV3V4V26Iainfix <V26V3Aainfix <=c0V26FAainfix <c0V3FF"> <label name="expl:VC for add"/> <transf name="inline_all" - proved="false" + proved="true" expanded="false"> <goal name="WP_parameter add.8.1" @@ -1633,14 +1633,14 @@ loclnum="137" loccnumb="6" loccnume="9" expl="1. postcondition" sum="2d8840a55677b5d5091921c8b6fc695d" - proved="false" + proved="true" expanded="false" shape="ainfix =agetV12V13agetV2V13Iainfix =V13V0NFIainfix =c0V5Oainfix <c0V5AamemaTuple2V14V15agetaeltsamk arrayV5V10amodahashV14alengthamk arrayV5V10qainfix =agetV12V14aSomeV15FAainfix =amodahashV17alengthamk arrayV5V10V16IamemaTuple2V17V18agetaeltsamk arrayV5V10V16FIainfix <V16V5Aainfix =c0V16Oainfix <c0V16FAainfix <c0V5Iainfix =V12asetV7V0aSomeV1FIainfix =V11ainfix +V9c1FIainfix =V10asetV8amodahashV0V5aConsaTuple2V0V1agetV8amodahashV0V5Aainfix =c0V5Oainfix <c0V5FIainfix <amodahashV0V5V5Aainfix =c0amodahashV0V5Oainfix <c0amodahashV0V5Iainfix <amodahashV0V5V5Aainfix =c0amodahashV0V5Oainfix <c0amodahashV0V5Iainfix =agetV7V19agetV2V19Iainfix =V19V0NFAainfix =agetV7V0aNoneAainfix =c0V5Oainfix <c0V5AamemaTuple2V20V21agetaeltsamk arrayV5V8amodahashV20alengthamk arrayV5V8qainfix =agetV7V20aSomeV21FAainfix =amodahashV23alengthamk arrayV5V8V22IamemaTuple2V23V24agetaeltsamk arrayV5V8V22FIainfix <V22V5Aainfix =c0V22Oainfix <c0V22FAainfix <c0V5FIainfix =c0V5Oainfix <c0V5AamemaTuple2V25V26agetaeltsamk arrayV5V6amodahashV25alengthamk arrayV5V6qainfix =agetV2V25aSomeV26FAainfix =amodahashV28alengthamk arrayV5V6V27IamemaTuple2V28V29agetaeltsamk arrayV5V6V27FIainfix <V27V5Aainfix =c0V27Oainfix <c0V27FAainfix <c0V5FIainfix =c0V3Oainfix <c0V3AamemaTuple2V30V31agetaeltsamk arrayV3V4amodahashV30alengthamk arrayV3V4qainfix =agetV2V30aSomeV31FAainfix =amodahashV33alengthamk arrayV3V4V32IamemaTuple2V33V34agetaeltsamk arrayV3V4V32FIainfix <V32V3Aainfix =c0V32Oainfix <c0V32FAainfix <c0V3FF"> <label name="expl:VC for add"/> <transf name="split_goal_wp" - proved="false" + proved="true" expanded="false"> <goal name="WP_parameter add.8.1.1" @@ -1648,7 +1648,7 @@ loclnum="137" loccnumb="6" loccnume="9" expl="1. postcondition" sum="1911c53aa245c12cbb7de6454bc659b0" - proved="false" + proved="true" expanded="false" shape="ainfix =agetV12V13agetV2V13Iainfix =V13V0NFIainfix =c0V5Oainfix <c0V5AamemaTuple2V14V15agetaeltsamk arrayV5V10amodahashV14alengthamk arrayV5V10qainfix =agetV12V14aSomeV15FAainfix =amodahashV17alengthamk arrayV5V10V16IamemaTuple2V17V18agetaeltsamk arrayV5V10V16FIainfix <V16V5Aainfix =c0V16Oainfix <c0V16FAainfix <c0V5Iainfix =V12asetV7V0aSomeV1FIainfix =V11ainfix +V9c1FIainfix =V10asetV8amodahashV0V5aConsaTuple2V0V1agetV8amodahashV0V5Aainfix =c0V5Oainfix <c0V5FIainfix <amodahashV0V5V5Aainfix =c0amodahashV0V5Oainfix <c0amodahashV0V5Iainfix <amodahashV0V5V5Aainfix =c0amodahashV0V5Oainfix <c0amodahashV0V5Iainfix =agetV7V19agetV2V19Iainfix =V19V0NFAainfix =agetV7V0aNoneAainfix =c0V5Oainfix <c0V5AamemaTuple2V20V21agetaeltsamk arrayV5V8amodahashV20alengthamk arrayV5V8qainfix =agetV7V20aSomeV21FAainfix =amodahashV23alengthamk arrayV5V8V22IamemaTuple2V23V24agetaeltsamk arrayV5V8V22FIainfix <V22V5Aainfix =c0V22Oainfix <c0V22FAainfix <c0V5FIainfix =c0V5Oainfix <c0V5AamemaTuple2V25V26agetaeltsamk arrayV5V6amodahashV25alengthamk arrayV5V6qainfix =agetV2V25aSomeV26FAainfix =amodahashV28alengthamk arrayV5V6V27IamemaTuple2V28V29agetaeltsamk arrayV5V6V27FIainfix <V27V5Aainfix =c0V27Oainfix <c0V27FAainfix <c0V5FIainfix =c0V3Oainfix <c0V3AamemaTuple2V30V31agetaeltsamk arrayV3V4amodahashV30alengthamk arrayV3V4qainfix =agetV2V30aSomeV31FAainfix =amodahashV33alengthamk arrayV3V4V32IamemaTuple2V33V34agetaeltsamk arrayV3V4V32FIainfix <V32V3Aainfix =c0V32Oainfix <c0V32FAainfix <c0V3FF"> <label @@ -1657,7 +1657,7 @@ prover="0" timelimit="5" memlimit="1000" - obsolete="true" + obsolete="false" archived="false"> <result status="valid" time="0.13"/> </proof> @@ -1665,7 +1665,7 @@ prover="1" timelimit="20" memlimit="1000" - obsolete="true" + obsolete="false" archived="false"> <result status="valid" time="0.08"/> </proof>