It's a static analysis tool, so it has many TimeOut limitations :-) In practise, many abstract interpretation based tools generalize too much, lose too much information, then get lost and TO instead. The test suite released there gives a good empirical idea of what SLAyer can do. You'll see lots of while-loops over single- and doubly-linked lists as SLAyer can generalize Separation Logic points-to predicates to 'sll' list predicates.

I'm specifically interested here in what the tool cannot do, more than what it can do. For now all I can tell is it "works for some empirical cases, and maybe works in rest of cases, but not strictly defined, don't expect anything concrete".