CNF formulas generated with BMC
The following file
contains propositional formulas in conjunctive normal form (CNF),
i.e. in DIMACS format, that have been generated by the bounded model
checker BMC for
three examples used in  and .
A. Biere, A. Cimatti, E. M. Clarke, and Y. Zhu. Symbolic Model Checking
without BDDs. In Tools and Algorithms for the Analysis and Construction of
Systems (TACAS'99), number 1579 in LNCS. Springer-Verlag, 1999.
A. Biere, A. Cimatti, E. M. Clarke, M. Fujita, and Y. Zhu. Symbolic Model
Checking using SAT procedures instead of BDDs. In Design Automation
Conference (DAC'99), 1999.