summaryrefslogtreecommitdiff
path: root/Test/linear/async-bug.bpl.expect
blob: 73a5eaee71ec4a0fd6c2bec9eec531ee20a55c4b (plain)
1
2
3
async-bug.bpl(21,30): Error: unavailable source for a linear read
async-bug.bpl(28,0): Error: Input variable tid must be available at a return
2 type checking errors detected in async-bug.bpl