High-performance deduction for verification: a case study in the theory of arrays