Abstraction and Acceleration in SMT-based Model-Checking for Array Programs