Pushdown systems (PDSs) consist of a stack and a finite state machine and are frequently used to model abstractions of software. They correspond to sequential recursive programs with finite-domain variables. This paper presents a novel algorithm for deciding reachability of particular locations of PDSs. We exploit the fact that most PDSs used in practice are
, and propose to use SAT-based Bounded Model Checking to search for counterexamples. Completeness is achieved by computing
of the procedures in the program.