EUF-based Solving Dyck-Reachability with Applications to Static Analysis