Automatic analysis of integer-manipulating programs is a main problem in program analysis. Such programs are a basic building block of more complex imperative programs (e.g. with linked lists or strings) since analysis of the latter can often be reduced to analysis of the former (e.g. by some variants of counter abstractions). Since they are already Turing-complete, the challenge is to devise approximation techniques that give useful answers in many cases. Following a standard automata-theoretic approach, we will consider Minsky’s counter systems as an abstraction of integer-manipulating programs, i.e., finite-state automata with integer counters whose values can be incremented/decremented by and compared against integer constants. In order to analyze such systems, we will consider reversal-bounded acceleration, which is an underapproximation technique that covers runs of a fixed number of reversals between non-incrementing/non-decrementing modes of the counters. We will show that reversal-bounded analysis of counter systems is efficiently reducible to satisfiability of quantifier-free Presburger formulas (in fact, NP-complete) and so can be solved using highly-optimized SMT solvers like Z3. We have implemented a prototype of the reduction and shows the efficacies of the technique on a few interesting examples (e.g. derived from Linux device drivers) which other techniques (e.g. predicate abstractions and bounded-model checking) cannot deal with. This is a joint work with Matthew Hague, which has appeared in CAV'11 and CAV'12.