Towards SMT Model Checking of Array-Based Systems