Game semantics provides fully abstract (sound and complete) models for open program fragments containing calls to undefined identifiers (e.g., library functions). The standard regular-language representation for algorithmic game semantics of open programs with unbounded integers yields infinite-state automata. By employing symbolic instead of concrete values for integers, we obtain symbolic finite automata (SFA) representation that is amenable to automatic reasoning if the predicates labelling transitions of the given SFA are from a decidable first-order theory, like the linear integer arithmetic. Otherwise, no automatic analysis can be performed. In this paper, we employ abstract interpretation techniques to define over-approximations of the SFAs representing game models by applying abstractions on symbolic (predicate) level. As a result, we obtain abstract symbolic finite automata (ASFA) that can be automatically analyzed, and so they can be applied to prove safety (assertion validity) of open programs. That is, provided that the abstraction preserves the safety property, the analysis of smaller ASFA suffices to decide the safety of the input open programs. This way, we enable efficient automatic verification of open programs containing various constraint formulae, like polynomial and exponential constraints from the non-linear integer arithmetic.