[SAL-HELP] Array elimination

[David Friggens]

Hi. I've been trying to explore what I can do with sal-inf-bmc and 
induction, and I'm confused by the need for --enable-ate. I have a 
system with two properties that fail with an error (can't expand 
quantifier) with ate; without ate one is proved at depth 5 and the 
other fails with a segmentation violation exception for depths greater 
than 3.

What exactly does it (--enable-ate) do, and what limitations does it 
impose?

Does it mean that sal-inf-bmc can't handle systems with arrays, or just 
certain types of arrays?

If it's required due to a limitation of ICS is there another solver I 
can use instead?

Thanks
David