SAFARI: SMT-Based Abstraction for Arrays with Interpolants