We present a new and very simple translation of the bounded model checking problem which is linear both in the size of the
formula and the length of the bound. The resulting CNF-formula has a linear number of variables and clauses.
Keywords bounded model checking - LTL - linear translation - NuSMV