Instances solved by squeezebf+aqme
QBFEVAL'16 - Solver Portfolio Track.

InstanceResultTime
biu.mv.xl_ao.bb-b003-p020-MIF04-c05.blif-biu.inv.prop.bb-bmc.conf01.01X-QBF.BB1-Zi.BB2-01X.BB3-01X.with-IOC.unfold-001FAIL0.1
lognBWLARGEB0FAIL0.1
k_ph_n-1FAIL0.11
biu.mv.xl_ao.bb-b003-p020-IPF03-c03.blif-biu.inv.prop.bb-bmc.conf00.01X-QBF.BB1-01X.BB2-01X.BB3-01X.with-IOC.unfold-003FAIL0.11
flipflop-3-cFAIL0.11
incrementer-enc05-uniform-depth-2FAIL0.12
vonNeumann-ripple-carry-5-cFAIL0.18
ken.flash^10.C-f2FAIL0.21
connect_5x4_3_DFAIL0.22
lognBWLARGEA0FAIL0.24
vonNeumann-ripple-carry-6-cFAIL0.28
ken.flash^10.C-f3FAIL0.29
connect_6x5_5_DFAIL0.33
vonNeumann-ripple-carry-7-cFAIL0.45
impl04SAT0.49
tree-exa10-10SAT0.49
rewriting_k_10UNSAT0.5
rewriting_k_17UNSAT0.5
cnt01SAT0.5
tree-exa2-45UNSAT0.5
impl02SAT0.5
z4ml.blif_0.10_0.20_0_1_inp_exactSAT0.5
counter_e_2SAT0.5
impl16SAT0.5
stmt44_107_113SAT0.5
impl20SAT0.5
tree-exa2-10UNSAT0.5
k_ph_p-1UNSAT0.5
toilet_g_06_01.2SAT0.51
impl14SAT0.51
impl06SAT0.51
toilet_g_10_01.2SAT0.51
impl12SAT0.51
tree-exa2-35UNSAT0.51
toilet_g_08_01.2SAT0.51
tree-exa2-40UNSAT0.51
z4ml.blif_0.10_0.20_0_1_out_exactSAT0.51
stmt1_30_31SAT0.51
stmt44_107_108SAT0.51
tree-exa2-30UNSAT0.51
lut4_XOR_fORUNSAT0.51
rewriting_k_19UNSAT0.51
k_ph_n-3SAT0.51
tree-exa10-30SAT0.51
k_d4_n-1SAT0.51
toilet_g_02_01.2SAT0.52
z4ml.blif_0.10_1.00_0_0_out_exactUNSAT0.52
toilet_g_04_01.2SAT0.52
toilet_c_08_01.2UNSAT0.52
mutex-2-sSAT0.52
k_lin_p-2UNSAT0.52
k3_1_1SAT0.52
z4ml.blif_0.10_1.00_0_0_inp_exactUNSAT0.52
s27_d2_sSAT0.52
z4ml.blif_0.10_0.20_0_0_out_exactUNSAT0.52
cnt02eSAT0.52
tree-exa2-20UNSAT0.52
impl18SAT0.52
k_path_p-2UNSAT0.53
s27_d3_uUNSAT0.53
toilet_c_04_01.4UNSAT0.53
k_dum_n-2SAT0.53
toilet_c_06_01.4UNSAT0.53
k_dum_n-3SAT0.53
toilet_a_04_01.6UNSAT0.53
adder-2-unsatUNSAT0.53
k_poly_p-2UNSAT0.53
impl08SAT0.53
impl10SAT0.53
toilet_a_04_05.2SAT0.54
k_poly_n-2SAT0.54
CHAIN12v.13SAT0.54
k_dum_n-1SAT0.54
lut4_XOR_f1SAT0.54
k_path_n-5SAT0.54
tree-exa2-50UNSAT0.54
toilet_c_06_01.8UNSAT0.54
toilet_c_08_01.6UNSAT0.55
k_path_n-3SAT0.55
k_lin_p-3UNSAT0.55
qshifter_4SAT0.55
flipflop-4-cUNSAT0.55
k_ph_n-4SAT0.55
k_d4_p-4UNSAT0.55
k_poly_n-6SAT0.55
k_poly_n-7SAT0.55
toilet_a_04_01.4UNSAT0.55
CHAIN17v.18SAT0.55
k_dum_p-2UNSAT0.56
k_grz_p-4UNSAT0.56
k_path_p-5UNSAT0.56
z4ml.blif_0.10_1.00_0_1_inp_exactSAT0.56
k_grz_n-5SAT0.56
toilet_a_02_10.2SAT0.56
CHAIN16v.17SAT0.56
k_poly_p-4UNSAT0.56
CHAIN14v.15SAT0.56
k_dum_n-5SAT0.56
toilet_a_06_01.6UNSAT0.56
cnt05SAT0.56
mutex-4-sSAT0.56
C432.blif_0.10_1.00_0_1_out_exactSAT0.57
k_dum_p-12UNSAT0.57
k_poly_p-7UNSAT0.57
k_t4p_n-2SAT0.57
texas.parsesys^1.E-d4SAT0.57
k_poly_p-8UNSAT0.57
k_grz_n-8SAT0.57
sortnetsort5.v.stepl.004UNSAT0.57
k_t4p_p-4UNSAT0.57
k_poly_n-5SAT0.57
k_path_n-4SAT0.57
k_grz_n-2SAT0.57
toilet_a_06_01.10UNSAT0.57
lut4_2_fXORSAT0.57
k_d4_n-2SAT0.57
k_dum_n-11SAT0.57
k_lin_n-3SAT0.58
k_dum_p-4UNSAT0.58
k_grz_p-5UNSAT0.58
k_grz_n-6SAT0.58
k_path_p-13UNSAT0.58
k_dum_p-6UNSAT0.58
k_ph_p-5UNSAT0.58
k_path_n-6SAT0.58
k_poly_p-11UNSAT0.58
toilet_c_08_01.7UNSAT0.58
toilet_g_15_01.2SAT0.58
C432.blif_0.10_1.00_0_1_inp_exactSAT0.58
k_ph_n-6SAT0.59
toilet_c_08_05.4SAT0.59
BLOCKS3ii.4.3UNSAT0.59
k_dum_n-17SAT0.59
C432.blif_0.10_1.00_0_0_out_exactUNSAT0.59
k_poly_n-16SAT0.59
k_path_n-9SAT0.59
k_dum_n-12SAT0.59
BLOCKS3ii.5.2UNSAT0.6
k_dum_p-21UNSAT0.6
k_poly_p-9UNSAT0.6
k_dum_p-17UNSAT0.6
k_t4p_p-6UNSAT0.6
k_path_p-10UNSAT0.6
k_dum_p-16UNSAT0.6
k_grz_n-7SAT0.6
k_dum_p-14UNSAT0.6
k_dum_n-18SAT0.61
k_poly_p-15UNSAT0.61
k_path_n-13SAT0.61
k_t4p_n-5SAT0.61
p5-5.pddl_planlen=6SAT0.61
k_dum_p-20UNSAT0.61
k_dum_n-21SAT0.61
k_path_n-12SAT0.61
k_poly_n-14SAT0.61
k_path_p-19UNSAT0.61
k_t4p_n-4SAT0.61
k_lin_p-4UNSAT0.62
query48_query15_1344UNSAT0.62
k_poly_n-20SAT0.62
C499.blif_0.10_1.00_0_1_out_exactSAT0.62
k_poly_p-14UNSAT0.62
k_path_n-19SAT0.62
k_path_p-15UNSAT0.62
p5-5.pddl_planlen=5SAT0.62
k_poly_p-19UNSAT0.62
k_path_n-16SAT0.62
k_path_n-14SAT0.62
k_path_p-14UNSAT0.62
C499.blif_0.10_1.00_0_1_inp_exactSAT0.63
k_poly_n-17SAT0.63
k_path_p-16UNSAT0.63
aim-100-6_0-yes1-3-50SAT0.63
cube_c3_ser--opt-6_SAT0.63
toilet_c_08_01.11UNSAT0.63
k_poly_n-18SAT0.63
k_path_p-21UNSAT0.64
aim-200-1_6-yes1-4-90SAT0.64
term1.blif_0.10_1.00_0_1_out_exactSAT0.64
driverlog01_7SAT0.64
k_poly_p-16UNSAT0.64
qshifter_5SAT0.64
term1.blif_0.10_1.00_0_1_inp_exactSAT0.64
s27_d4_uUNSAT0.64
k_branch_n-2SAT0.64
k_path_p-18UNSAT0.64
BLOCKS3i.5.4SAT0.65
toilet_g_20_01.2SAT0.65
lut4_2_f1SAT0.65
k_poly_n-21SAT0.66
gttt_2_2_0010_3x3_torus_wUNSAT0.66
flipflop-5-cUNSAT0.66
szymanski-6-sUNSAT0.66
driverlog03_7SAT0.66
eijk.S382.S-d4SAT0.67
c4_BMC_p1_k32SAT0.67
lights3_021_0_009SAT0.67
term1.blif_0.10_1.00_0_0_inp_exactUNSAT0.67
k_dum_n-9SAT0.68
tlc03-uniform-depth-9UNSAT0.69
lights3_021_0_027UNSAT0.71
flipflop-6-cUNSAT0.72
lut4_AND_f1SAT0.72
k_branch_p-6UNSAT0.72
s298_d2_sSAT0.73
toilet_a_08_05.2UNSAT0.73
lights3_035_0_002UNSAT0.74
biu.mv.xl_ao.bb-b003-p020-MIF04-c05.blif-biu.inv.prop.bb-bmc.conf05.01X-QBF.BB1-Zi.BB2-01X.BB3-Zi.with-IOC.unfold-003UNSAT0.75
toilet_a_08_05.9SAT0.76
vonNeumann-ripple-carry-8-cFAIL0.78
c4_BMC_p2_k128UNSAT0.78
term1.blif_0.10_1.00_0_0_out_exactUNSAT0.8
gttt_2_1_000111_3x3_torus_bSAT0.81
rewriting_k_21UNSAT0.82
lights3_035_0_051UNSAT0.82
rewriting_k_30UNSAT0.83
rewriting_k_23UNSAT0.83
Adder2-2-cUNSAT0.83
lights3_035_0_027UNSAT0.83
tree-exa2-25UNSAT0.84
tlc03-nonuniform-depth-17UNSAT0.84
query26_query34_1344SAT0.84
z4ml.blif_0.10_1.00_0_1_out_exactSAT0.84
rewriting_k_25UNSAT0.85
qshifter_3SAT0.86
k_d4_p-1UNSAT0.86
z4ml.blif_0.10_0.20_0_0_inp_exactUNSAT0.86
k_ph_p-3UNSAT0.86
mutex-8-sSAT0.86
rewriting_k_50UNSAT0.87
b12_PR_9_2SAT0.87
BLOCKS3iii.4UNSAT0.87
s01238_PR_8_2SAT0.88
par8-4-50UNSAT0.88
k_grz_n-4SAT0.88
jnh212-50UNSAT0.88
mutex-16-sSAT0.88
ev-pr-4x4-5-3-0-0-1-lgSAT0.89
rewriting_k_75UNSAT0.89
irst.dme6.B-d2SAT0.9
szymanski-8-sUNSAT0.91
toilet_c_10_01.12UNSAT0.91
k_dum_p-3UNSAT0.91
lut4_AND_fXORUNSAT0.92
BLOCKS3iii.5SAT0.93
C880.blif_0.10_1.00_0_1_inp_exactSAT0.93
sortnetsort7.v.stepl.007SAT0.93
k_ph_n-8SAT0.93
tlc03-uniform-depth-21UNSAT0.93
C5315.blif_0.10_1.00_0_1_out_exactSAT0.94
mutex-32-sSAT0.95
ring_r4_ser--opt-11_UNSAT0.96
C432.blif_0.10_0.20_0_1_inp_exactSAT0.97
k_branch_p-8UNSAT0.97
BLOCKS3i.5.3UNSAT0.98
flipflop-7-cUNSAT0.99
rewriting_k_100UNSAT1
vis.prodcell^01.E-d2SAT1
BLOCKS3ii.5.3SAT1.01
arbiter-07-comp-error01-qbf-hardness-depth-4UNSAT1.01
aim-100-1_6-yes1-2-00SAT1.01
mutex-64-sSAT1.03
k_lin_p-8UNSAT1.03
toilet_a_08_01.13UNSAT1.05
b20_PR_7_90UNSAT1.08
gttt_1_1_001020_3x3_wUNSAT1.1
aim-50-6_0-yes1-3-50UNSAT1.11
biu.mv.xl_ao.bb-b003-p020-MIF04-c05.blif-biu.inv.prop.bb-bmc.conf03.01X-QBF.BB1-Zi.BB2-Zi.BB3-01X.with-IOC.unfold-005UNSAT1.11
s05378_PR_9_2SAT1.11
s09234_PR_8_2SAT1.12
k_lin_n-5SAT1.12
connect_7x6_4_WFAIL1.12
sortnetsort8.AE.stepl.003SAT1.13
incrementer-enc03-nonuniform-depth-13UNSAT1.17
gttt_1_1_000111_3x3_torus_wUNSAT1.21
k_lin_p-9UNSAT1.21
mutex-128-sSAT1.22
biu.mv.xl_ao.bb-b003-p020-IPF02-c05.blif-biu.inv.prop.bb-bmc.conf01.01X-QBF.BB1-Zi.BB2-01X.BB3-01X.with-IOC.unfold-005UNSAT1.25
par8-1-c-50UNSAT1.27
szymanski-5-sUNSAT1.28
flipflop-8-cUNSAT1.29
emptyroom_e3_ser--opt-20_SAT1.31
s09234_PR_8_5SAT1.32
connect_8x7_7_WFAIL1.34
C432.blif_0.10_1.00_0_0_inp_exactUNSAT1.34
vonNeumann-ripple-carry-9-cFAIL1.38
C5315.blif_0.10_1.00_0_1_inp_exactSAT1.41
k_lin_p-10UNSAT1.42
szymanski-10-sUNSAT1.44
lut4_3_fANDSAT1.46
k_branch_p-10UNSAT1.46
driverlog10_6UNSAT1.49
p10-10.pddl_planlen=10SAT1.56
k_grz_n-10SAT1.56
qshifter_6SAT1.58
stmt17_18_19SAT1.62
ring_r3_ser--opt-8_SAT1.65
gttt_2_2_00101121_3x3_bUNSAT1.67
k_lin_p-11UNSAT1.67
sortnetsort8.v.stepl.007SAT1.68
k_grz_p-11UNSAT1.74
C499.blif_0.10_1.00_0_0_out_exactUNSAT1.78
k_t4p_n-14SAT1.81
connect_5x4_4_RUNSAT1.82
k_ph_n-9SAT1.83
ev-pr-6x6-5-5-0-1-2-lgUNSAT1.88
s27_d5_uUNSAT1.92
flipflop-9-cUNSAT1.93
tlc03-uniform-depth-52UNSAT1.94
k_t4p_n-15SAT1.98
lognBWLARGEA1UNSAT1.99
k_d4_p-7UNSAT2
lut4_2_f2UNSAT2.07
sortnetsort8.v.stepl.009SAT2.08
k_lin_p-12UNSAT2.08
C6288.blif_0.10_1.00_0_1_out_exactSAT2.09
cnt10SAT2.13
fpu-10Xh-error01-uniform-depth-5FAIL2.17
tlc01-uniform-depth-73UNSAT2.18
k_grz_p-10UNSAT2.2
ii32b1-00SAT2.2
k_d4_p-8UNSAT2.21
ev-pr-4x4-7-3-0-0-1-lgSAT2.28
k_branch_p-11UNSAT2.3
cnt07eSAT2.36
szymanski-12-sUNSAT2.38
vonNeumann-ripple-carry-10-cFAIL2.42
incrementer-enc07-nonuniform-depth-17UNSAT2.43
k_branch_p-12UNSAT2.51
arbiter-06-comp-error02-qbf-hardness-depth-5UNSAT2.59
fpu-10Xe-correct01-nonuniform-depth-6FAIL2.66
incrementer-enc03-nonuniform-depth-24UNSAT2.73
query01_ntrivil_1344UNSAT2.81
s386_d2_sSAT2.86
toilet_a_10_05.3UNSAT2.91
gttt_2_1_0010_4x4_torus_bUNSAT3.04
flipflop-10-cUNSAT3.06
stmt19_90_266UNSAT3.18
k_d4_p-10UNSAT3.19
k_lin_n-6SAT3.28
k_lin_p-14UNSAT3.37
ev-pr-8x8-5-7-0-1-2-lgUNSAT3.44
stmt27_296_297SAT3.59
incrementer-enc02-nonuniform-depth-31UNSAT3.72
ken.flash^03.C-f3UNSAT3.9
k_d4_p-11UNSAT3.91
fpu-10Xh-correct04-uniform-depth-8FAIL4
lognBWLARGEB1UNSAT4.11
cnt11SAT4.19
incrementer-enc07-nonuniform-depth-21UNSAT4.19
tlc04-nonuniform-depth-56UNSAT4.27
ev-pr-4x4-5-3-0-0-1-sSAT4.31
vonNeumann-ripple-carry-11-cFAIL4.36
C5315.blif_0.10_1.00_0_0_inp_exactUNSAT4.48
szymanski-14-sUNSAT4.58
k_lin_n-7SAT4.63
BLOCKS4iii.6UNSAT4.69
C5315.blif_0.10_1.00_0_0_out_exactUNSAT4.75
k_grz_p-13UNSAT4.76
k_grz_p-12UNSAT4.83
c1_BMC_p1_k4SAT4.86
k_branch_n-4SAT5
ev-pr-8x8-7-7-0-1-2-lgUNSAT5.08
k_d4_p-13UNSAT5.14
tlc02-uniform-depth-114UNSAT5.39
flipflop-11-cUNSAT5.47
connect_5x4_3_RUNSAT5.53
stmt21_79_304UNSAT5.61
tlc04-uniform-depth-36UNSAT5.71
ev-pr-6x6-7-5-0-1-2-lgUNSAT5.98
k_grz_p-16UNSAT6.04
stmt19_217_309UNSAT6.08
par16-1-50UNSAT6.08
k_grz_p-18UNSAT6.25
Umbrella_tbm_24.tex.module.000131SAT6.34
k_grz_p-17UNSAT6.35
BLOCKS4i.6.4UNSAT6.42
nusmv.reactor^3.C-d4SAT6.42
C6288.blif_0.10_1.00_0_1_inp_exactSAT6.48
C499.blif_0.10_0.20_0_1_inp_exactSAT6.5
k_lin_n-8SAT6.54
k_grz_n-18SAT6.63
ev-pr-8x8-9-7-0-1-2-lgUNSAT6.76
k_branch_n-3SAT6.84
cnt08eSAT7.07
BLOCKS4ii.7.2UNSAT7.08
k_grz_p-19UNSAT7.45
vonNeumann-ripple-carry-12-cFAIL7.48
k_d4_p-16UNSAT7.56
query21_ntrivil_1344UNSAT8.21
depots03_9UNSAT8.24
k_d4_p-17UNSAT8.35
szymanski-16-sUNSAT8.39
k_lin_p-19UNSAT8.55
k_lin_n-9SAT8.92
b20_PR_7_20SAT8.93
k_grz_n-21SAT8.99
Core1108_tbm_21.tex.module.000030SAT9.39
dungeon_i25-m12-u3-v0.pddl_planlen=72UNSAT9.4
Core1108_tbm_21.tex.module.000026UNSAT9.55
fpu-10Xh-correct04-uniform-depth-14FAIL9.66
Umbrella_tbm_24.tex.module.000066SAT9.67
flipflop-12-cUNSAT10
stmt29_226_376UNSAT10.06
biu.mv.xl_ao.bb-b003-p020-MIF04-c05.blif-biu.inv.prop.bb-bmc.conf07.01X-QBF.BB1-Zi.BB2-Zi.BB3-Zi.with-IOC.unfold-007UNSAT10.16
k_grz_n-20SAT10.28
fpu-10Xh-correct04-uniform-depth-15FAIL10.47
stmt52_244_394UNSAT10.95
dungeon_i25-m12-u5-v0.pddl_planlen=65UNSAT11.08
k_d4_p-20UNSAT11.42
tlc04-nonuniform-depth-98UNSAT11.83
fpu-10Xh-correct04-uniform-depth-16FAIL11.92
sortnetsort9.v.stepl.005UNSAT12.9
vonNeumann-ripple-carry-13-cFAIL13.24
c5_BMC_p1_k32SAT13.29
arbiter-10-comp-error01-qbf-hardness-depth-10UNSAT13.93
qshifter_7SAT14.67
fpu-10Xh-correct04-nonuniform-depth-18FAIL15.1
s15850_PR_8_50SAT15.1
szymanski-18-sUNSAT15.4
k_branch_p-14UNSAT15.69
stmt19_83_412UNSAT15.84
C499.blif_0.10_1.00_0_0_inp_exactUNSAT16.22
dungeon_i25-m12-u3-v0.pddl_planlen=130UNSAT17.89
Core1108_tbm_02.tex.moduleQ3.2S.000015UNSAT18.07
k_d4_n-3SAT18.47
s15850_PR_2_2SAT18.92
k_t4p_p-9UNSAT19.37
k_lin_n-11SAT19.49
Core1108_tbm_21.tex.module.000027UNSAT19.55
fpu-10Xe-correct01-uniform-depth-22FAIL19.8
Core1108_tbm_21.tex.module.000008SAT20.59
tlc02-uniform-depth-241UNSAT23.2
gttt_2_2_001020_4x4_wUNSAT23.5
k_t4p_n-6SAT23.9
k_t4p_p-10UNSAT23.91
dungeon_i25-m12-u3-v0.pddl_planlen=165UNSAT24.64
fpu-10Xe-correct01-nonuniform-depth-24FAIL24.92
Core1108_tbm_03.tex.moduleQ3.2S.000002UNSAT26.4
szymanski-20-sUNSAT26.66
s641_d2_sSAT28.18
dungeon_i25-m12-u3-v0.pddl_planlen=190UNSAT29.15
fpu-10Xh-correct04-nonuniform-depth-27FAIL30.97
vonNeumann-ripple-carry-15-cFAIL32.7
dungeon_i25-m12-u5-v0.pddl_planlen=170UNSAT32.94
sortnetsort10.v.stepl.005UNSAT33.58
k_t4p_p-12UNSAT33.99
cnt14SAT34.83
s298_d4_sSAT36.87
arbiter-07-comp-error02-qbf-hardness-depth-6UNSAT39.49
k_lin_n-14SAT41.74
k_t4p_n-8SAT44.57
emptyroom_e4_par---21_UNSAT46.13
vis.4-arbit^2.E-f2SAT46.94
ev-pr-4x4-9-3-0-0-1-lgSAT47.62
k_d4_n-7SAT51.21
k_lin_n-15SAT51.79
k_t4p_p-15UNSAT52.5
k_t4p_n-9SAT56.54
toilet_c_10_01.17UNSAT57.01
k_t4p_p-16UNSAT59.78
emptyroom_e3_ser---19_UNSAT62.42
k5_2_3SAT62.45
szymanski-24-sUNSAT67.28
k_t4p_p-17UNSAT68.16
rankfunc33_signed_32SAT70.16
rankfunc5_unsigned_64SAT71.82
rankfunc3_signed_64SAT72.67
k_d4_n-8SAT75.12
k_t4p_p-18UNSAT75.19
k_branch_p-16UNSAT75.43
cube_c9_par--opt-11_SAT75.92
k_lin_n-17SAT77.08
biu.mv.xl_ao.bb-b003-p020-IPF01-c05.blif-biu.inv.prop.bb-bmc.conf04.01X-QBF.BB1-01X.BB2-01X.BB3-Zi.with-IOC.unfold-008UNSAT78.66
rankfunc5_signed_32SAT79.38
ev-pr-6x6-5-5-0-1-2-sUNSAT79.65
cube_c11_par---13_UNSAT81.63
s713_d2_sSAT81.67
rankfunc14_signed_64SAT82.63
k_t4p_p-20UNSAT93.67
C432.blif_0.10_0.20_0_0_out_exactUNSAT95.07
arbiter-06-comp-error01-qbf-hardness-depth-12UNSAT96.44
rankfunc51_signed_32SAT100.73
k_t4p_n-12SAT107.13
c1_BMC_p2_k512UNSAT109.58
C432.blif_0.10_0.20_0_0_inp_exactUNSAT114.17
k_t4p_n-13SAT121.66
ev-pr-6x6-7-5-0-1-2-sUNSAT131.37
arbiter-07-comp-error01-qbf-hardness-depth-11UNSAT133.33
k_d4_n-10SAT133.5
C432.blif_0.10_0.20_0_1_out_exactUNSAT140.59
s820_d2_sSAT146.55
ev-pr-4x4-11-3-0-0-1-lgSAT149.26
c1_BMC_p2_k1024UNSAT153.49
qshifter_8SAT241.2
adder-10-satSAT274.23
query51_query50_1344UNSAT293.83
k_d4_n-14SAT294.73
gttt_2_1_00011020_4x4_bUNSAT328.83
ev-pr-4x4-13-3-0-0-1-lgSAT329.11
pipesnotankage14_10UNSAT342.55
CHAIN18v.19SAT361.38
k_branch_p-18UNSAT448.74
ev-pr-4x4-7-3-0-0-1-sSAT490.83
ev-pr-6x6-9-5-0-1-2-lgUNSAT500.11
Umbrella_tbm_05.tex.module.000039SAT514.61
c2_Debug_s3_f1_e1_v2FAIL599.71
c4_Debug_s5_f2_e2_v1FAIL599.71
c4_Debug_s3_f1_e2_v3FAIL599.72
c4_Debug_s3_f1_e1_v2FAIL599.72
c4_Debug_s3_f1_e2_v2FAIL599.72
c1_Debug_s5_f1_e1_v2FAIL599.72
c1_Debug_s3_f1_e1_v1FAIL599.72
s510_d32_sFAIL600
rankfunc13_unsigned_64FAIL600
query11_query21_1344FAIL600
rankfunc17_unsigned_16FAIL600
query31_reachqu_1344nFAIL600
query42_query06_1344nFAIL600
query44_query26_1344nFAIL600
C880.blif_0.10_0.20_0_1_out_exactFAIL600
s820_d10_sFAIL600
rankfunc13_signed_32FAIL600
s499_d17_sFAIL600
s510_d6_sFAIL600
rankfunc22_signed_64FAIL600
query03_query25_1344FAIL600
pipesnotankage18_8FAIL600
ev-pr-6x6-13-5-0-1-2-sFAIL600
k_branch_n-12FAIL600
Umbrella_tbm_25.tex.moduleQ3.2S.000075FAIL600
p10-10.pddl_planlen=6FAIL600
p20-1.pddl_planlen=24FAIL600
p20-1.pddl_planlen=26FAIL600
p20-1.pddl_planlen=32FAIL600
pipesnotankage18_7FAIL600
p20-20.pddl_planlen=23FAIL600
p20-5.pddl_planlen=17FAIL600
p20-5.pddl_planlen=32FAIL600
ev-pr-6x6-17-5-0-1-2-sFAIL600
C6288.blif_0.10_0.20_0_0_out_exactFAIL600
s510_d23_sFAIL600
s499_d25_uFAIL600
ev-pr-6x6-11-5-0-1-2-lgFAIL600
s298_d22_uFAIL600
s499_d12_sFAIL600
s05378_PR_1_75FAIL600
s298_d12_sFAIL600
adder-14-satFAIL600
s1196_1_5FAIL600
s499_d24_uFAIL600
s1269_d13_uFAIL600
s510_d36_sFAIL600
s499_d9_sFAIL600
s510_d11_sFAIL600
s510_d24_sFAIL600
s510_d3_sFAIL600
s713_d5_sFAIL600
connect_8x7_6_RFAIL600
s820_d15_uFAIL600
s510_d28_sFAIL600
s510_d35_sFAIL600
s713_d11_uFAIL600
s386_d6_sFAIL600
ev-pr-6x6-11-5-0-1-2-sFAIL600
s820_d7_sFAIL600
s3330_d7_sFAIL600
s386_d11_uFAIL600
s1269_d14_uFAIL600
s3330_d14_uFAIL600
s499_d15_sFAIL600
s298_d25_uFAIL600
ev-pr-4x4-15-3-0-0-1-sFAIL600
s1269_d12_uFAIL600
s3330_d5_sFAIL600
CHAIN20v.21FAIL600
C6288.blif_0.10_0.20_0_1_out_exactFAIL600
uclid-pipe2FAIL600
uclid-pipe3aFAIL600
C6288.blif_0.10_0.20_0_0_inp_exactFAIL600
b20_C_3_2FAIL600
incrementer-enc02-uniform-depth-58FAIL600
s3330_d4_sFAIL600
input_mouser_cseries.cFAIL600
b21_C_3_206FAIL600
kernel_agplib_intrface.cFAIL600
audio_ddksynth_csynth2.cppFAIL600
network_irda_miniport_nscirda_comm.cFAIL600
b22_C_2_12FAIL600
incrementer-enc06-uniform-depth-24FAIL600
C5315.blif_0.10_0.20_0_1_inp_exactFAIL600
ev-pr-8x8-19-7-0-1-2-lgFAIL600
C880.blif_0.10_0.20_0_1_inp_exactFAIL600
s1269_d4_sFAIL600
s386_d4_sFAIL600
s1269_d10_sFAIL600
k_d4_n-16FAIL600
s713_d4_sFAIL600
arbiter-06-comp-error01-qbf-hardness-depth-15FAIL600
incrementer-enc08-uniform-depth-33FAIL600
arbiter-07-comp-error01-qbf-hardness-depth-20FAIL600
test2_quant_squaring3FAIL600
arbiter-08-comp-error02-qbf-hardness-depth-9FAIL600
arbiter-10-comp-error01-qbf-hardness-depth-22FAIL600
incrementer-enc07-uniform-depth-25FAIL600
network_trans_sys_notify.cFAIL600
hid_hclient_ecdisp.cFAIL600
dungeon_i10-m10-u10-v0.pddl_planlen=187FAIL600
dungeon_i10-m5-u10-v0.pddl_planlen=134FAIL600
small-seq-fixpoint-3FAIL600
dungeon_i10-m5-u10-v0.pddl_planlen=23FAIL600
dungeon_i15-m7-u4-v0.pddl_planlen=81FAIL600
k_branch_n-16FAIL600
connect_8x7_4_RFAIL600
gttt_1_1_00101121_4x4_torus_wFAIL600
ev-pr-6x6-9-5-0-1-2-sFAIL600
test2_quant_squaring2FAIL600
ev-pr-6x6-19-5-0-1-2-lgFAIL600
gttt_2_1_00102030_4x4_torus_bFAIL600
C6288.blif_0.10_1.00_0_0_out_exactFAIL600
C880.blif_0.10_1.00_0_0_out_exactFAIL600
cache-coherence-3-fixpoint-3FAIL600
cache-coherence-2-fixpoint-6FAIL600
input_pnpi8042_moudep.cFAIL600
network_ndis_rtlnwifi_hw_hw_ccmp.cFAIL600
filesys_smbmrx_cvsndrcv.cFAIL600
network_irda_miniport_nscirda_settings.cFAIL600
small-seq-fixpoint-5FAIL600
cache-coherence-2-fixpoint-1FAIL600
small-swap2-fixpoint-4FAIL600
small-synabs-fixpoint-9FAIL600
AR-fixpoint-5FAIL600
b22_PR_8_20FAIL600
small-swap1-fixpoint-3FAIL600
s386_d7_sFAIL600
sdlx-fixpoint-3FAIL600
ev-pr-8x8-13-7-0-1-2-lgFAIL600
k6_2_3FAIL600
C5315.blif_0.10_0.20_0_1_out_exactFAIL600
C880.blif_0.10_0.20_0_0_inp_exactFAIL600
k_ph_n-21FAIL600
ev-pr-4x4-11-3-0-0-1-sFAIL600
s1196_d3_uFAIL600
CHAIN22v.23FAIL600
s641_d6_sFAIL600
cnt16rFAIL600
C880.blif_0.10_1.00_0_0_inp_exactFAIL600
CHAIN19v.20FAIL600
ev-pr-4x4-17-3-0-0-1-lgFAIL600
k_ph_n-16FAIL600
k_d4_n-20FAIL600
C6288.blif_0.10_1.00_0_0_inp_exactFAIL600
term1.blif_0.10_0.20_0_1_inp_exactFAIL600
s713_d6_sFAIL600
ev-pr-6x6-17-5-0-1-2-lgFAIL600
Adder2-8-cFAIL600
ev-pr-4x4-9-3-0-0-1-sFAIL600
ev-pr-6x6-19-5-0-1-2-sFAIL600
test3_quant_squaring2FAIL600
test3_quant_squaring4FAIL600
s1196_d5_uFAIL600
s1196_d6_uFAIL600
s386_d12_uFAIL600
s386_d10_uFAIL600
s386_d3_sFAIL600
s499_d7_sFAIL600
s499_d19_sFAIL600
s499_d18_sFAIL600
s510_d31_sFAIL600
s641_d8_uFAIL600
s641_d10_uFAIL600
s386_d9_uFAIL600
s3330_d3_sFAIL600
s3330_d12_uFAIL600
s1196_d7_uFAIL600
s1196_d4_uFAIL600
s1269_d5_sFAIL600
s1269_d9_sFAIL600
s1269_d15_uFAIL600
s1269_d3_sFAIL600
s298_d14_sFAIL600
s298_d17_sFAIL600
s298_d10_sFAIL600
s641_d11_uFAIL600
k_ph_p-15FAIL600
k_d4_n-15FAIL600
Adder2-8-sFAIL600
s1269_d8_sFAIL600
ev-pr-6x6-13-5-0-1-2-lgFAIL600
C5315.blif_0.10_0.20_0_0_inp_exactFAIL600
test1_quant_squaring2FAIL600
s298_d19_uFAIL600
ev-pr-6x6-15-5-0-1-2-sFAIL600
Adder2-10-sFAIL600
s298_d18_sFAIL600
s820_d11_uFAIL600
ev-pr-8x8-17-7-0-1-2-lgFAIL600
s3330_d8_sFAIL600
k_branch_p-5FAIL600
k_branch_n-11FAIL600
k_branch_n-10FAIL600
k_branch_n-9FAIL600
C499.blif_0.10_0.20_0_0_inp_exactFAIL600
uclid-pipe3bFAIL600
ev-pr-4x4-15-3-0-0-1-lgFAIL600
s641_d7_uFAIL600
s3330_d2_sFAIL600
C499.blif_0.10_0.20_0_0_out_exactFAIL600
adder-12-unsatFAIL600
test5_quant_squaring4FAIL600
k_ph_n-14FAIL600
adder-12-satFAIL600
k_ph_n-11FAIL600
k_ph_p-18FAIL600
test5_quant_squaring5FAIL600
k_ph_p-10FAIL600
CHAIN21v.22FAIL600
k_ph_p-19FAIL600
term1.blif_0.10_0.20_0_1_out_exactFAIL600
s499_d22_uFAIL600
C880.blif_0.10_1.00_0_1_out_exactFAIL600
k_branch_n-8FAIL600
ev-pr-8x8-11-7-0-1-2-lgFAIL600
s820_d8_sFAIL600
test4_quant_squaring2FAIL600
test4_quant_squaring4FAIL600
C880.blif_0.10_0.20_0_0_out_exactFAIL600
term1.blif_0.10_0.20_0_0_inp_exactFAIL600
ev-pr-8x8-15-7-0-1-2-lgFAIL600
s1196_d2_sFAIL600
k_ph_p-13FAIL600
s641_d3_sFAIL600
cube_c7_ser--opt-24_FAIL600
s3330_d10_uFAIL600
connect_9x8_6_RFAIL600
stmt19_64_99FAIL600
stmt17_62_98FAIL600
stmt17_70_98FAIL600
stmt23_72_76FAIL600
stmt28_68_81FAIL600
stmt17_82_98FAIL600
stmt23_66_96FAIL600
f600-50FAIL600
test1_quant_squaring3FAIL600
s641_d4_sFAIL600
C6288.blif_0.10_0.20_0_1_inp_exactFAIL600
emptyroom_e4_ser--opt-44_FAIL600
k_ph_p-20FAIL600
c2_BMC_p1_k2048FAIL600
c3_BMC_p1_k256FAIL600
s386_d8_uFAIL600
c5_BMC_p2_k128FAIL600
c5_BMC_p2_k64FAIL600
C499.blif_0.10_0.20_0_1_out_exactFAIL600
stmt17_70_90FAIL600
stmt17_63_82FAIL600
stmt41_160_235FAIL600
stmt27_16_97FAIL600
k12_4_2FAIL600
k8_3_4FAIL600
k5_3_2FAIL600
k8_2_3FAIL600
ev-pr-4x4-17-3-0-0-1-sFAIL600
k8_3_2FAIL600
k14_2_3FAIL600
stmt19_3_214FAIL600
stmt21_319_418FAIL600
ev-pr-4x4-13-3-0-0-1-sFAIL600
stmt17_86_98FAIL600
stmt25_52_53FAIL600
stmt16_950_951FAIL600
stmt44_916_917FAIL600
ev-pr-6x6-15-5-0-1-2-lgFAIL600
stmt24_765_766FAIL600
stmt41_738_749FAIL600
k_branch_n-20FAIL600
connect_8x7_5_RFAIL600
k8_4_3FAIL600
CHAIN23v.24FAIL600
s641_d5_sFAIL600
nusmv.tcas-t^1.B-d2FAIL600
Adder2-16-sFAIL600
nusmv.tcas^3.B-f2FAIL600
nusmv.tcas^6.B-f4FAIL600
texas.PI_main^05.E-f3FAIL600
texas.PI_main^08.E-f3FAIL600
texas.PI_main^16.E-f2FAIL600
texas.two_proc^4.E-f2FAIL600
k_branch_p-21FAIL600
ken.oop^2.C-d4FAIL600
ken.oop^2.C-d3FAIL600
ken.flash^08.C-d4FAIL600
s713_d8_uFAIL600
s713_d9_uFAIL600
s713_d10_uFAIL600
s713_d3_sFAIL600
s820_d9_sFAIL600
s820_d12_uFAIL600
s820_d14_uFAIL600
s820_d3_sFAIL600
eijk.bs4863.S-d4FAIL600
s713_d7_uFAIL600
s3330_d9_sFAIL600
biu.mv.xl_ao.bb-b001-p010-MIF05-c07.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-004FAIL600
biu.mv.xl_ao.bb-b001-p010-OPF02-c08.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-003FAIL600
term1.blif_0.10_0.20_0_0_out_exactFAIL600
biu.mv.xl_ao.bb-b003-p020-IPF03-c03.blif-biu.inv.prop.bb-bmc.conf07.01X-QBF.BB1-Zi.BB2-Zi.BB3-Zi.with-IOC.unfold-008FAIL600
biu.mv.xl_ao.bb-b003-p020-IPF03-c03.blif-biu.inv.prop.bb-bmc.with-IOC.unfold-009FAIL600
k_ph_p-12FAIL600
biu.mv.xl_ao.bb-b003-p020-MIF04-c05.blif-biu.inv.prop.bb-bmc.conf07.01X-QBF.BB1-Zi.BB2-Zi.BB3-Zi.with-IOC.unfold-010FAIL600
c2_Debug_s3_f2_e1_v3FAIL600
c3_Debug_s3_f2_e2_v2FAIL600
biu.mv.xl_ao.bb-b001-p010-MIF04-c06.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-005FAIL600
biu.mv.xl_ao.bb-b001-p010-MIF01-c01.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-004FAIL600
biu.mv.xl_ao.bb-b001-p010-IPF05-c07.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-003FAIL600
C5315.blif_0.10_0.20_0_0_out_exactFAIL600
sortnetsort9.AE.stepl.009FAIL600
sortnetsort9.AE.stepl.012FAIL600
sortnetsort9.v.stepl.007FAIL600
biu.mv.xl_ao.bb-b001-p005-OPF03-c09.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-003FAIL600
biu.mv.xl_ao.bb-b001-p005-OPF05-c02.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-004FAIL600
biu.mv.xl_ao.bb-b001-p005-OPF05-c03.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-004FAIL600
biu.mv.xl_ao.bb-b001-p010-IPF02-c07.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-003FAIL600
biu.mv.xl_ao.bb-b001-p010-IPF02-c08.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-003FAIL600
c4_Debug_s3_f2_e2_v2FAIL600