Counterexample-guided abstraction refinement for linear programs with arrays