Mentions légales du service
Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
why3
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Deploy
Releases
Container registry
Monitor
Service Desk
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
Why3
why3
Commits
a4a8c17d
Commit
a4a8c17d
authored
12 years ago
by
Jean-Christophe Filliâtre
Browse files
Options
Downloads
Patches
Plain Diff
fix hashtbl_impl session, really
parent
616056f7
No related branches found
No related tags found
No related merge requests found
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
examples/hashtbl_impl/why3session.xml
+112
-112
112 additions, 112 deletions
examples/hashtbl_impl/why3session.xml
with
112 additions
and
112 deletions
examples/hashtbl_impl/why3session.xml
+
112
−
112
View file @
a4a8c17d
...
...
@@ -23,13 +23,13 @@
version=
"4.3.1"
/>
<file
name=
"../hashtbl_impl.mlw"
verified=
"
fals
e"
verified=
"
tru
e"
expanded=
"true"
>
<theory
name=
"HashtblImpl"
locfile=
"../hashtbl_impl.mlw"
loclnum=
"1"
loccnumb=
"7"
loccnume=
"18"
verified=
"
fals
e"
verified=
"
tru
e"
expanded=
"true"
>
<goal
name=
"bucket_bounds"
...
...
@@ -94,14 +94,14 @@
loclnum=
"56"
loccnumb=
"6"
loccnume=
"12"
expl=
"VC for resize"
sum=
"5e8dd7b81fdd5d34491f9c9c2a1c85b1"
proved=
"
fals
e"
proved=
"
tru
e"
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=
"
fals
e"
proved=
"
tru
e"
expanded=
"false"
>
<goal
name=
"WP_parameter resize.1"
...
...
@@ -109,7 +109,7 @@
loclnum=
"56"
loccnumb=
"6"
loccnume=
"12"
expl=
"1. precondition"
sum=
"825cbdcf30bb030f9017480eb1b063e7"
proved=
"
fals
e"
proved=
"
tru
e"
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=
"
tru
e"
obsolete=
"
fals
e"
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=
"
fals
e"
proved=
"
tru
e"
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=
"
tru
e"
obsolete=
"
fals
e"
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=
"
fals
e"
proved=
"
tru
e"
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=
"
tru
e"
obsolete=
"
fals
e"
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=
"
fals
e"
proved=
"
tru
e"
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=
"
tru
e"
obsolete=
"
fals
e"
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=
"
fals
e"
proved=
"
tru
e"
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=
"
tru
e"
obsolete=
"
fals
e"
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=
"
fals
e"
proved=
"
tru
e"
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=
"
tru
e"
obsolete=
"
fals
e"
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=
"
fals
e"
proved=
"
tru
e"
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=
"
fals
e"
proved=
"
tru
e"
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=
"
fals
e"
proved=
"
tru
e"
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=
"
tru
e"
obsolete=
"
fals
e"
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=
"
fals
e"
proved=
"
tru
e"
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=
"
fals
e"
proved=
"
tru
e"
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=
"
fals
e"
proved=
"
tru
e"
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=
"
fals
e"
proved=
"
tru
e"
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=
"
fals
e"
proved=
"
tru
e"
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=
"
tru
e"
obsolete=
"
fals
e"
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=
"
fals
e"
proved=
"
tru
e"
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=
"
tru
e"
obsolete=
"
fals
e"
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=
"
fals
e"
proved=
"
tru
e"
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=
"
tru
e"
obsolete=
"
fals
e"
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=
"
fals
e"
proved=
"
tru
e"
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=
"
tru
e"
obsolete=
"
fals
e"
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=
"
fals
e"
proved=
"
tru
e"
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=
"
tru
e"
obsolete=
"
fals
e"
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=
"
fals
e"
proved=
"
tru
e"
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=
"
tru
e"
obsolete=
"
fals
e"
archived=
"false"
>
<result
status=
"valid"
time=
"0.05"
/>
</proof>
...
...
@@ -417,7 +417,7 @@
prover=
"2"
timelimit=
"5"
memlimit=
"1000"
obsolete=
"
tru
e"
obsolete=
"
fals
e"
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=
"
fals
e"
proved=
"
tru
e"
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=
"
tru
e"
obsolete=
"
fals
e"
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=
"
fals
e"
proved=
"
tru
e"
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=
"
tru
e"
obsolete=
"
fals
e"
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=
"
fals
e"
proved=
"
tru
e"
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=
"
tru
e"
obsolete=
"
fals
e"
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=
"
fals
e"
proved=
"
tru
e"
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=
"
tru
e"
obsolete=
"
fals
e"
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=
"
fals
e"
proved=
"
tru
e"
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=
"
tru
e"
obsolete=
"
fals
e"
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=
"
fals
e"
proved=
"
tru
e"
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=
"
tru
e"
obsolete=
"
fals
e"
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=
"
fals
e"
proved=
"
tru
e"
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=
"
tru
e"
obsolete=
"
fals
e"
archived=
"false"
>
<result
status=
"valid"
time=
"
1.2
7"
/>
<result
status=
"valid"
time=
"
0.4
7"
/>
</proof>
</goal>
<goal
...
...
@@ -568,7 +568,7 @@
loclnum=
"56"
loccnumb=
"6"
loccnume=
"12"
expl=
"17. precondition"
sum=
"829c755c991a444ef572ff369e1e078e"
proved=
"
fals
e"
proved=
"
tru
e"
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=
"
tru
e"
obsolete=
"
fals
e"
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=
"
fals
e"
proved=
"
tru
e"
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=
"
tru
e"
obsolete=
"
fals
e"
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=
"
fals
e"
proved=
"
tru
e"
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=
"
fals
e"
proved=
"
tru
e"
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=
"
fals
e"
proved=
"
tru
e"
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=
"
tru
e"
obsolete=
"
fals
e"
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=
"
fals
e"
proved=
"
tru
e"
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=
"
tru
e"
obsolete=
"
fals
e"
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=
"
fals
e"
proved=
"
tru
e"
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=
"
fals
e"
proved=
"
tru
e"
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=
"
fals
e"
proved=
"
tru
e"
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=
"
tru
e"
obsolete=
"
fals
e"
archived=
"false"
>
<result
status=
"valid"
time=
"
5.27
"
/>
<result
status=
"valid"
time=
"
2.11
"
/>
</proof>
<proof
prover=
"2"
timelimit=
"5"
memlimit=
"1000"
obsolete=
"
tru
e"
obsolete=
"
fals
e"
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=
"
fals
e"
proved=
"
tru
e"
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=
"
tru
e"
obsolete=
"
fals
e"
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=
"
fals
e"
proved=
"
tru
e"
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=
"
tru
e"
obsolete=
"
fals
e"
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=
"
fals
e"
proved=
"
tru
e"
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=
"
tru
e"
obsolete=
"
fals
e"
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=
"
fals
e"
proved=
"
tru
e"
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=
"
tru
e"
obsolete=
"
fals
e"
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=
"
fals
e"
proved=
"
tru
e"
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=
"
tru
e"
obsolete=
"
fals
e"
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=
"
fals
e"
proved=
"
tru
e"
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=
"
tru
e"
obsolete=
"
fals
e"
archived=
"false"
>
<result
status=
"valid"
time=
"0.02"
/>
</proof>
...
...
@@ -878,7 +878,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.
2
0"
/>
<result
status=
"valid"
time=
"0.0
2
"
/>
</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.6
4"
/>
<result
status=
"valid"
time=
"
0.4
4"
/>
</proof>
</goal>
</transf>
...
...
@@ -1359,14 +1359,14 @@
loclnum=
"137"
loccnumb=
"6"
loccnume=
"9"
expl=
"VC for add"
sum=
"5e773205ee8042e7a48ce2cd11636201"
proved=
"
fals
e"
proved=
"
tru
e"
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=
"
fals
e"
proved=
"
tru
e"
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
.6
8
"
/>
<result
status=
"valid"
time=
"
1
.6
5
"
/>
</proof>
</goal>
<goal
...
...
@@ -1479,14 +1479,14 @@
loclnum=
"137"
loccnumb=
"6"
loccnume=
"9"
expl=
"5. type invariant"
sum=
"f8c0fe7b7f7e09146102c04e89414436"
proved=
"
fals
e"
proved=
"
tru
e"
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=
"
fals
e"
proved=
"
tru
e"
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=
"
fals
e"
proved=
"
tru
e"
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=
"
fals
e"
proved=
"
tru
e"
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=
"
fals
e"
proved=
"
tru
e"
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=
"
tru
e"
obsolete=
"
fals
e"
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=
"
fals
e"
proved=
"
tru
e"
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=
"
tru
e"
obsolete=
"
fals
e"
archived=
"false"
>
<result
status=
"valid"
time=
"
4.0
2"
/>
<result
status=
"valid"
time=
"
1.1
2"
/>
</proof>
</goal>
</transf>
...
...
@@ -1581,14 +1581,14 @@
loclnum=
"137"
loccnumb=
"6"
loccnume=
"9"
expl=
"7. postcondition"
sum=
"4a8a1ff4cadd693cef1624e070b87343"
proved=
"
fals
e"
proved=
"
tru
e"
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=
"
fals
e"
proved=
"
tru
e"
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=
"
fals
e"
proved=
"
tru
e"
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=
"
tru
e"
obsolete=
"
fals
e"
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=
"
fals
e"
proved=
"
tru
e"
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=
"
fals
e"
proved=
"
tru
e"
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=
"
fals
e"
proved=
"
tru
e"
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=
"
fals
e"
proved=
"
tru
e"
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=
"
fals
e"
proved=
"
tru
e"
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=
"
tru
e"
obsolete=
"
fals
e"
archived=
"false"
>
<result
status=
"valid"
time=
"0.13"
/>
</proof>
...
...
@@ -1665,7 +1665,7 @@
prover=
"1"
timelimit=
"20"
memlimit=
"1000"
obsolete=
"
tru
e"
obsolete=
"
fals
e"
archived=
"false"
>
<result
status=
"valid"
time=
"0.08"
/>
</proof>
...
...
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Save comment
Cancel
Please
register
or
sign in
to comment
