Type and interval aware array constraint solving for symbolic execution