Model Checking Linear Programs with Arrays