  We present a new approach to proving non-termination of non-deterministic
integer programs. Our technique is rather simple but efficient. It relies on a
purely syntactic reversal of the program's transition system followed by a
constraint-based invariant synthesis with constraints coming from both the
original and the reversed transition system. The latter task is performed by a
simple call to an off-the-shelf SMT-solver, which allows us to leverage the
latest advances in SMT-solving. Moreover, our method offers a combination of
features not present (as a whole) in previous approaches: it handles programs
with non-determinism, provides relative completeness guarantees and supports
programs with polynomial arithmetic. The experiments performed with our
prototype tool RevTerm show that our approach, despite its simplicity and
stronger theoretical guarantees, is at least on par with the state-of-the-art
tools, often achieving a non-trivial improvement under a proper configuration
of its parameters.
