Due to the development of high speed circuits beyond the 2-GHz mark, the significance of automatic test pattern generation for Path Delay Faults (PDFs) drastically increased in the last years. This paper describes an algorithm for generating robust and non-robust tests for PDFs based on Boolean Satisfiability (SAT). A new formulation for the robust path delay fault model as a SAT instance is introduced. Unlike previous SAT-based approaches our approach can cope with latches and is therefore applicable for sequential circuits. The formulation provides the possibility to apply the SAT technique Incremental SAT to accelerate the process. Experimental results show the efficiency of the approach.