An efficient approach for SAT-based quantifier elimination and pre-image computation using unrolled designs that significantly improves the performance of pre-image and fix-point computation in SAT-based unbounded symbolic model checking.