CNF Benchmark Suite: VLIW-SAT-4.0
========================================

Description:    satisfiable formulas from formal verification of buggy VLIW processors with instruction queues
                and 9-stage pipelines; the processors implement advanced loads, predicated execution,
                branch prediction, and exceptions

# of instances: 10

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

Date:           October 24, 2003





CNF Formula                      Size [Bytes]    Variables    Clauses    Literals    Avg. Literals/Clause
---------------------------------------------------------------------------------------------------------
9vliw_m_9stages_iq3_C1_bug1.cnf     314723803       521188   13378641    39204979                2.930416
9vliw_m_9stages_iq3_C1_bug2.cnf     314721111       521158   13378532    39204686                2.930418
9vliw_m_9stages_iq3_C1_bug3.cnf     314662761       521046   13376161    39197797                2.930422
9vliw_m_9stages_iq3_C1_bug4.cnf     314000013       520721   13348117    39114325                2.930325
9vliw_m_9stages_iq3_C1_bug5.cnf     314757003       520770   13380350    39210884                2.930483
9vliw_m_9stages_iq3_C1_bug6.cnf     314726828       521192   13378781    39205391                2.930416
9vliw_m_9stages_iq3_C1_bug7.cnf     314707245       521147   13378010    39203144                2.930417
9vliw_m_9stages_iq3_C1_bug8.cnf     314722831       521179   13378617    39204907                2.930416
9vliw_m_9stages_iq3_C1_bug9.cnf     314722868       521187   13378624    39204898                2.930413
9vliw_m_9stages_iq3_C1_bug10.cnf    314723037       521182   13378625    39204931                2.930416





output of md5sum:
-------------------------------------------------------------------------------------------------
1911de49ec477d3e34b9a95eb8bf0845  9vliw_m_9stages_iq3_C1_bug1.cnf
de190892801b59cd9842bfb52b694299  9vliw_m_9stages_iq3_C1_bug2.cnf
dc050785d671b86f856b07b158553686  9vliw_m_9stages_iq3_C1_bug3.cnf
c9a9723a58c9cb8a0b55a82eb452ac90  9vliw_m_9stages_iq3_C1_bug4.cnf
c77a56af24208a6401c763e11a38de01  9vliw_m_9stages_iq3_C1_bug5.cnf
abc624ca713aad9563ab3886d918a526  9vliw_m_9stages_iq3_C1_bug6.cnf
6dcc1a7a687db45349fbaf9870c73e4b  9vliw_m_9stages_iq3_C1_bug7.cnf
5fe5b52b05e512edbe82e7d139ac7362  9vliw_m_9stages_iq3_C1_bug8.cnf
838f83d2fc04e408a3e66700f0dc0173  9vliw_m_9stages_iq3_C1_bug9.cnf
b96b75461795057ef2d559ebb6ae2ba1  9vliw_m_9stages_iq3_C1_bug10.cnf