Program verification using constraint handling rules and array constraint generalizations