Regression verification is an approach complementing regression
testing with formal verification. The goal is to formally prove that
two versions of a program behave either equally or differently in a
precisely specified way. In this paper, we present a novel automatic
approach for regression verification that reduces the equivalence of
two related imperative integer programs to Horn constraints over
uninterpreted predicates.  Subsequently, state-of-the-art SMT solvers
are used to solve the constraints. We have implemented the approach,
and our experiments show non-trivial integer programs that can now be
proved equivalent without further user input.