CNF Benchmark Suite: DLX-IQ-UNSAT.2.0
========================================

Description:    formulas from formal verification of DLX processors with 
                multicycle functional units, exceptions, branch prediction,
                and instruction queues

# of instances: 32

Author:         Miroslav N. Velev (mvelev@ece.cmu.edu)
                http://www.ece.cmu.edu/~mvelev

Date:           August 2, 2003



The formula sizes range in:

CNF Formula              Size [Bytes]    Variables    Clauses    Literals    Avg. Literals/Clause
----------------------------------------------------------------------------------------------------
1dlx_c_mc_ex_bp_f_iq33_a     86160764       207885    3889667    11334393                2.913975

...

1dlx_c_mc_ex_bp_f_iq64_a    334340704       836658   14201404    41383808                2.914065