This paper introduces Semi-Linear Integer Vector Addition Systems with Resets (SVASR). A SVASR is a labeled transition system in which the states are finite rational-valued vectors and the transitions go from one state to another by applying an orthogonal projection followed by a translation drawn from a semi-linear set. We give a polynomial-time algorithm for computing a linear integer arithmetic formula defining the reachability relation of an SVASR with states and a stack.

We then consider the use of SVASRs for over-approximating the reachability relation of transition systems in which the transition relation is a semi-linear set. We show that any semi-linear transition system has a ``best'' SVASR that simulates its behavior, called its SVASR-reflection. The dimension of the SVASR-reflection of a semi-linear transition system $T$ with states is exponential in the number of states; however, we show that the over-approximate reachability induced by $T$'s SVASR-reflection can be computed in polynomial time.