Traditional Bounded Model Checking (BMC) is based on translating the model
checking problem into SAT, the Boolean satisfiability problem. This paper
introduces an encoding of Linear Temporal Logic with Past operators (PLTL) into
the Quantifier-Free Difference Logic with Uninterpreted Functions (QF-UFIDL).
The resulting encoding is a simpler and more concise version of existing
SATbased encodings, currently used in BMC.