Instances solved by ghostq-cegar
QBFEVAL'16 - Prenex non-CNF Track.

InstanceResultTime
toilet_g_04_01.2SAT0.06
z4ml.blif_0.10_1.00_0_1_out_exactSAT0.06
tree-exa2-20UNSAT0.06
tree-exa2-25UNSAT0.06
tree-exa10-10SAT0.06
rewriting_k_10UNSAT0.06
flipflop-3-cUNSAT0.06
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-001UNSAT0.06
incrementer-enc05-uniform-depth-2UNSAT0.06
rewriting_k_21UNSAT0.07
tree-exa2-35UNSAT0.07
z4ml.blif_0.10_0.20_0_1_out_exactSAT0.07
rewriting_k_17UNSAT0.07
counter6_2SAT0.07
stmt44_107_108SAT0.07
s27_d4_uUNSAT0.07
impl08SAT0.07
z4ml.blif_0.10_1.00_0_0_inp_exactUNSAT0.07
toilet_a_04_01.4UNSAT0.07
toilet_g_08_01.2SAT0.07
counter4_3SAT0.07
z4ml.blif_0.10_0.20_0_1_inp_exactSAT0.07
counter4_2SAT0.07
tree-exa2-45UNSAT0.07
k_ph_p-3UNSAT0.07
ring4_2SAT0.07
impl10SAT0.07
rewriting_k_19UNSAT0.07
toilet_c_06_01.4UNSAT0.08
counter4_4SAT0.08
counter5_2SAT0.08
k_d4_n-1SAT0.08
qshifter_3SAT0.08
counter7_2SAT0.08
ring5_2SAT0.08
ring4_3SAT0.08
ring6_2SAT0.08
s27_d5_uUNSAT0.08
impl12SAT0.08
impl16SAT0.08
k_path_p-2UNSAT0.08
k_lin_p-2UNSAT0.08
toilet_a_04_01.6UNSAT0.09
k_dum_n-1SAT0.09
counter5_4SAT0.09
stmt17_18_19SAT0.09
impl20SAT0.09
counter4_6SAT0.09
counter8_2SAT0.09
toilet_g_15_01.2SAT0.09
counter4_5SAT0.09
ring5_4SAT0.1
counter6_4SAT0.1
irst.dme6.B-d2SAT0.1
ring4_4SAT0.1
k_dum_p-3UNSAT0.1
k_poly_n-2SAT0.1
k3_1_1SAT0.1
semaphore_2SAT0.1
eijk.S382.S-d4SAT0.1
counter4_7SAT0.1
k_dum_p-2UNSAT0.1
C5315.blif_0.10_1.00_0_0_out_exactUNSAT0.11
counter4_9SAT0.11
ring4_5SAT0.11
C432.blif_0.10_1.00_0_1_out_exactSAT0.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-003UNSAT0.11
term1.blif_0.10_1.00_0_1_out_exactSAT0.11
counter4_8SAT0.11
C5315.blif_0.10_1.00_0_0_inp_exactUNSAT0.12
query01_ntrivil_1344UNSAT0.12
semaphore3_2SAT0.12
counter4_11SAT0.12
counter4_10SAT0.12
k_grz_n-2SAT0.12
ring6_4SAT0.12
ring4_6SAT0.12
counter7_4SAT0.12
semaphore_3SAT0.13
mutex-2-sSAT0.13
toilet_g_20_01.2SAT0.13
lut4_XOR_fORUNSAT0.13
counter5_8SAT0.13
par8-1-c-50UNSAT0.13
counter8_4SAT0.13
ring4_7SAT0.14
counter4_13SAT0.14
k_dum_n-5SAT0.14
term1.blif_0.10_1.00_0_0_out_exactUNSAT0.14
semaphore4_2SAT0.14
k_dum_p-6UNSAT0.15
ring5_8SAT0.15
ring4_8SAT0.15
k_poly_p-4UNSAT0.15
counter4_15SAT0.15
k_d4_n-2SAT0.15
counter4_16SAT0.16
semaphore5_2SAT0.16
semaphore_4SAT0.16
stmt27_296_297SAT0.16
s641_d2_sSAT0.16
k_branch_n-2SAT0.16
counter6_8SAT0.16
counter4_14SAT0.16
toilet_a_06_01.6UNSAT0.16
term1.blif_0.10_0.20_0_1_inp_exactSAT0.17
k_ph_p-5UNSAT0.17
k_grz_n-5SAT0.17
semaphore3_3SAT0.17
s713_d2_sSAT0.17
stmt27_16_97UNSAT0.18
C499.blif_0.10_1.00_0_1_inp_exactSAT0.18
biu.mv.xl_ao.bb-b001-p010-IPF05-c07.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-003SAT0.18
k_ph_n-6SAT0.18
k_poly_n-7SAT0.19
semaphore_5SAT0.19
ring6_8SAT0.19
dmeSmall_2SAT0.19
k_t4p_n-2SAT0.19
Core1108_tbm_21.tex.module.000091UNSAT0.19
counter7_8SAT0.2
toilet_c_08_05.4SAT0.2
semaphore6_2SAT0.2
k_path_n-5SAT0.2
s510_d3_sSAT0.2
counter5_16SAT0.21
s01238_PR_8_2SAT0.21
k_poly_p-7UNSAT0.21
Umbrella_tbm_24.tex.module.000103UNSAT0.21
semaphore4_3SAT0.21
counter4_12SAT0.22
Core1108_tbm_21.tex.module.000027UNSAT0.22
Core1108_tbm_03.tex.module.000092UNSAT0.22
rewriting_k_100UNSAT0.22
Core1108_tbm_03.tex.module.000064UNSAT0.22
Core1108_tbm_03.tex.module.000058UNSAT0.22
Core1108_tbm_03.tex.module.000056UNSAT0.22
Core1108_tbm_03.tex.module.000057UNSAT0.22
Umbrella_tbm_24.tex.module.000066UNSAT0.22
Core1108_tbm_03.tex.module.000021UNSAT0.22
semaphore3_4SAT0.22
Core1108_tbm_03.tex.module.000065UNSAT0.22
Core1108_tbm_03.tex.module.000090UNSAT0.23
s386_d3_sSAT0.23
Core1108_tbm_21.tex.module.000014UNSAT0.23
counter8_8SAT0.23
arbiter-07-comp-error01-qbf-hardness-depth-4UNSAT0.23
Core1108_tbm_21.tex.module.000030UNSAT0.23
Core1108_tbm_03.tex.module.000048UNSAT0.23
Core1108_tbm_03.tex.module.000038UNSAT0.24
Core1108_tbm_03.tex.module.000031UNSAT0.24
Umbrella_tbm_29.tex.module.000078UNSAT0.24
Core1108_tbm_21.tex.module.000009UNSAT0.24
k_dum_n-12SAT0.24
Core1108_tbm_21.tex.module.000010UNSAT0.24
lights3_035_0_027UNSAT0.24
lights3_035_0_051UNSAT0.24
Core1108_tbm_21.tex.module.000026UNSAT0.24
biu.mv.xl_ao.bb-b001-p010-IPF02-c08.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-003SAT0.24
C432.blif_0.10_1.00_0_0_out_exactUNSAT0.24
Core1108_tbm_03.tex.module.000003UNSAT0.24
Core1108_tbm_21.tex.module.000008UNSAT0.24
k_poly_p-8UNSAT0.24
semaphore5_3SAT0.25
biu.mv.xl_ao.bb-b001-p010-OPF02-c08.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-003SAT0.25
Core1108_tbm_03.tex.module.000039UNSAT0.25
vis.4-arbit^2.E-f2SAT0.25
Core1108_tbm_03.tex.module.000037UNSAT0.25
Core1108_tbm_03.tex.module.000023UNSAT0.25
k_dum_p-12UNSAT0.26
k_grz_p-10UNSAT0.26
ring5_16SAT0.26
Core1108_tbm_03.tex.module.000034UNSAT0.26
stmt16_950_951SAT0.26
s1196_d2_sSAT0.26
k_t4p_p-4UNSAT0.27
b12_PR_9_2SAT0.27
Core1108_tbm_03.tex.module.000019UNSAT0.28
Core1108_tbm_21.tex.module.000017UNSAT0.28
counter6_16SAT0.28
semaphore4_4SAT0.28
Umbrella_tbm_29.tex.module.000010UNSAT0.28
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.29
arbiter-06-comp-error02-qbf-hardness-depth-5UNSAT0.29
Adder2-2-cUNSAT0.29
Umbrella_tbm_29.tex.module.000009UNSAT0.29
semaphore6_3SAT0.3
k_dum_p-16UNSAT0.3
s386_d4_sSAT0.3
Umbrella_tbm_05.tex.module.000088UNSAT0.31
dme1_2SAT0.31
k_d4_p-8UNSAT0.31
Umbrella_tbm_21.tex.module.000139UNSAT0.32
Umbrella_tbm_21.tex.module.000129UNSAT0.32
Umbrella_tbm_26.tex.module.000061UNSAT0.32
Umbrella_tbm_21.tex.module.000134UNSAT0.32
ring6_16SAT0.32
k_grz_p-13UNSAT0.32
Umbrella_tbm_21.tex.module.000056UNSAT0.33
Umbrella_tbm_26.tex.module.000004UNSAT0.33
Umbrella_tbm_26.tex.module.000041UNSAT0.33
counter7_16SAT0.33
Umbrella_tbm_21.tex.module.000149UNSAT0.33
Umbrella_tbm_21.tex.module.000044UNSAT0.34
semaphore5_4SAT0.34
Core1108_tbm_09.tex.module.000033UNSAT0.34
k_grz_p-11UNSAT0.34
Umbrella_tbm_21.tex.module.000049UNSAT0.34
k_dum_n-17SAT0.34
Umbrella_tbm_21.tex.module.000079UNSAT0.34
Umbrella_tbm_21.tex.module.000069UNSAT0.35
Core1108_tbm_09.tex.module.000028UNSAT0.35
par8-4-50UNSAT0.36
k_grz_n-10SAT0.36
Umbrella_tbm_26.tex.module.000021UNSAT0.36
k_path_n-9SAT0.36
Umbrella_tbm_05.tex.module.000064UNSAT0.37
Core1108_tbm_09.tex.module.000010UNSAT0.37
Core1108_tbm_09.tex.module.000008UNSAT0.37
Core1108_tbm_09.tex.module.000009UNSAT0.37
Umbrella_tbm_21.tex.module.000024UNSAT0.38
counter5_32SAT0.38
Umbrella_tbm_05.tex.module.000079UNSAT0.38
Umbrella_tbm_21.tex.module.000029UNSAT0.38
k_path_p-5UNSAT0.38
dme1_3SAT0.38
Umbrella_tbm_25.tex.module.000106UNSAT0.39
s820_d3_sSAT0.4
Umbrella_tbm_25.tex.module.000084UNSAT0.4
Umbrella_tbm_05.tex.module.000053UNSAT0.4
Umbrella_tbm_05.tex.module.000065UNSAT0.4
Umbrella_tbm_25.tex.module.000087UNSAT0.4
Umbrella_tbm_25.tex.module.000121UNSAT0.4
k_dum_n-18SAT0.41
semaphore6_4SAT0.41
C880.blif_0.10_1.00_0_0_out_exactUNSAT0.41
Core1108_tbm_21.tex.module.000023UNSAT0.41
BLOCKS3ii.4.3UNSAT0.41
counter8_16SAT0.41
dmeSmall_4SAT0.42
Umbrella_tbm_05.tex.module.000043UNSAT0.42
s641_d4_sSAT0.42
counter5_33SAT0.43
s713_d4_sSAT0.44
stmt41_738_749SAT0.44
k_grz_n-20SAT0.44
Umbrella_tbm_25.tex.module.000099UNSAT0.44
k_poly_n-17SAT0.45
Umbrella_tbm_05.tex.module.000025UNSAT0.45
W3-Umbrella_tbm_21.tex.moduleQ3.6S.000001UNSAT0.45
tlc03-nonuniform-depth-17UNSAT0.45
k_poly_n-18SAT0.46
Umbrella_tbm_05.tex.module.000030UNSAT0.46
ring_r3_ser--opt-8_SAT0.46
k_path_n-12SAT0.47
k_poly_p-16UNSAT0.47
Umbrella_tbm_25.tex.module.000041UNSAT0.48
Umbrella_tbm_25.tex.module.000031UNSAT0.48
ring5_33SAT0.48
k_d4_p-11UNSAT0.48
Umbrella_tbm_05.tex.module.000015UNSAT0.48
Umbrella_tbm_25.tex.module.000003UNSAT0.48
W4-Umbrella_tbm_26.tex.moduleQ3.7S.000003UNSAT0.48
ring5_32SAT0.49
counter6_32SAT0.49
k_path_p-14UNSAT0.49
Umbrella_tbm_05.tex.module.000011UNSAT0.49
stmt19_90_266UNSAT0.5
flipflop-5-cUNSAT0.5
s499_d7_sSAT0.51
W5-Umbrella_tbm_26.tex.moduleQ3.7S.000003UNSAT0.52
W4-Umbrella_tbm_21.tex.moduleQ3.6S.000001UNSAT0.52
k_path_p-16UNSAT0.54
Core1108_tbm_21.tex.moduleQ3.2S.000002UNSAT0.54
Core1108_tbm_21.tex.moduleQ3.2S.000011UNSAT0.54
Core1108_tbm_21.tex.moduleQ3.2S.000027UNSAT0.54
ii32b1-00SAT0.54
k_grz_p-17UNSAT0.54
biu.mv.xl_ao.bb-b001-p005-OPF05-c02.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-004SAT0.54
k_d4_p-13UNSAT0.55
C499.blif_0.10_1.00_0_0_out_exactUNSAT0.55
Core1108_tbm_21.tex.moduleQ3.2S.000014UNSAT0.56
dme1_4SAT0.56
Core1108_tbm_21.tex.moduleQ3.2S.000024UNSAT0.57
Core1108_tbm_21.tex.moduleQ3.2S.000015UNSAT0.58
Core1108_tbm_28.tex.moduleQ2.2S.000003UNSAT0.58
Core1108_tbm_03.tex.moduleQ3.2S.000003UNSAT0.58
s3330_d2_sSAT0.59
Core1108_tbm_21.tex.moduleQ3.2S.000019UNSAT0.59
k_poly_n-21SAT0.59
tlc03-uniform-depth-21UNSAT0.59
ring6_32SAT0.6
Core1108_tbm_03.tex.moduleQ3.2S.000048UNSAT0.6
k_poly_p-19UNSAT0.61
Core1108_tbm_03.tex.moduleQ3.2S.000002UNSAT0.61
Core1108_tbm_21.tex.moduleQ3.2S.000007UNSAT0.61
k_t4p_n-5SAT0.61
toilet_a_08_05.2UNSAT0.62
Core1108_tbm_03.tex.moduleQ3.2S.000009UNSAT0.62
dme1_5SAT0.63
s1269_d3_sSAT0.64
Core1108_tbm_03.tex.moduleQ3.2S.000011UNSAT0.65
Core1108_tbm_02.tex.moduleQ3.2S.000026UNSAT0.66
Core1108_tbm_02.tex.moduleQ3.2S.000007UNSAT0.66
k_grz_n-21SAT0.66
query48_query15_1344UNSAT0.66
Core1108_tbm_02.tex.moduleQ3.2S.000095UNSAT0.66
Core1108_tbm_02.tex.moduleQ3.2S.000056UNSAT0.67
BLOCKS3iii.5SAT0.68
dmeSmall_8SAT0.68
Core1108_tbm_02.tex.moduleQ3.2S.000108UNSAT0.69
Core1108_tbm_02.tex.moduleQ3.2S.000077UNSAT0.69
Core1108_tbm_02.tex.moduleQ3.2S.000098UNSAT0.69
Core1108_tbm_03.tex.moduleQ3.2S.000018UNSAT0.7
W4-Umbrella_tbm_25.tex.moduleQ3.7S.000003UNSAT0.72
Core1108_tbm_02.tex.moduleQ3.2S.000099UNSAT0.74
k_grz_p-18UNSAT0.75
dmeSmall_9SAT0.76
dme1_6SAT0.77
possibility3_0_2FAIL0.77
assertion3_0_2FAIL0.77
possibility1_0_2FAIL0.78
assertion6_0_2FAIL0.78
possibility5_0_2FAIL0.78
assertion5_0_2FAIL0.78
possibility10_0_2FAIL0.78
assertion10_0_2FAIL0.78
assertion4_0_2FAIL0.78
possibility11_0_2FAIL0.78
assertion11_0_2FAIL0.78
consistency_0_2FAIL0.78
assertion9_0_2FAIL0.78
assertion1_0_2FAIL0.78
assertion2_0_2FAIL0.78
assertion7_0_2FAIL0.78
possibility8_0_2FAIL0.78
possibility2_0_2FAIL0.78
possibility6_0_2FAIL0.78
possibility9_0_2FAIL0.78
assertion12_0_2FAIL0.78
possibility7_0_2FAIL0.78
possibility12_0_2FAIL0.79
counter7_32SAT0.83
k_d4_p-17UNSAT0.83
W5-Umbrella_tbm_05.tex.moduleQ3.8S.000001UNSAT0.85
Umbrella_tbm_29.tex.moduleQ2.2S.000001UNSAT0.86
W5-Umbrella_tbm_25.tex.moduleQ3.7S.000003UNSAT0.87
possibility4_0_2FAIL0.88
counter8_32SAT0.88
dme1_7SAT0.92
counter_e_2SAT0.92
term1.blif_0.10_0.20_0_0_out_exactUNSAT0.93
k_path_p-10UNSAT0.96
possibility6_0_1UNSAT0.97
assertion11_0_1UNSAT0.97
assertion12_0_1UNSAT0.97
biu.mv.xl_ao.bb-b001-p010-MIF01-c01.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-004SAT0.98
c4_BMC_p1_k32SAT0.98
k_t4p_p-12UNSAT0.98
assertion5_0_1UNSAT1.01
Umbrella_tbm_24.tex.moduleQ2.1S.000136UNSAT1.01
Umbrella_tbm_26.tex.moduleQ3.2S.000009UNSAT1.02
BLOCKS3i.5.3UNSAT1.03
W4-Umbrella_tbm_05.tex.moduleQ3.8S.000001UNSAT1.04
assertion7_0_1UNSAT1.04
Umbrella_tbm_26.tex.moduleQ3.2S.000037UNSAT1.04
k_d4_p-20UNSAT1.05
Umbrella_tbm_23.tex.moduleQ1.2S.000001UNSAT1.05
dme1_8SAT1.05
counter6_64SAT1.05
Umbrella_tbm_26.tex.moduleQ3.2S.000014UNSAT1.05
counter6_65SAT1.06
Umbrella_tbm_26.tex.moduleQ3.2S.000041UNSAT1.06
assertion8_0_2FAIL1.06
assertion6_0_3FAIL1.11
s386_d8_uUNSAT1.11
k_branch_n-3SAT1.11
assertion6_0_1UNSAT1.11
possibility6_0_3FAIL1.12
possibility9_0_3FAIL1.12
assertion12_0_3FAIL1.12
assertion3_0_3FAIL1.12
possibility10_0_3FAIL1.12
assertion11_0_3FAIL1.12
BLOCKS3ii.5.3SAT1.12
possibility2_0_3FAIL1.12
possibility1_0_3FAIL1.12
consistency_0_3FAIL1.12
possibility7_0_3FAIL1.13
assertion9_0_3FAIL1.13
assertion1_0_3FAIL1.13
possibility3_0_3FAIL1.13
possibility11_0_3FAIL1.13
assertion8_0_3FAIL1.13
assertion2_0_3FAIL1.13
assertion5_0_3FAIL1.13
possibility12_0_3FAIL1.13
toilet_c_08_01.11UNSAT1.14
assertion4_0_3FAIL1.14
assertion7_0_3FAIL1.14
possibility5_0_3FAIL1.14
k_path_n-16SAT1.15
possibility8_0_3FAIL1.15
k_path_n-13SAT1.16
Umbrella_tbm_24.tex.moduleQ2.1S.000188UNSAT1.17
s298_d12_sSAT1.19
Umbrella_tbm_24.tex.moduleQ2.1S.000022UNSAT1.26
ring6_65SAT1.27
ring_r4_ser--opt-11_UNSAT1.29
gttt_1_1_000111_3x3_torus_wUNSAT1.29
k_lin_p-4UNSAT1.3
lut4_2_fXORSAT1.31
flipflop-6-cUNSAT1.33
Umbrella_tbm_26.tex.moduleQ3.2S.000020UNSAT1.36
ring6_64SAT1.37
Core1108_tbm_09.tex.moduleQ3.2S.000003UNSAT1.38
assertion10_0_3FAIL1.45
s713_d6_sSAT1.46
possibility4_0_3FAIL1.48
k_t4p_p-15UNSAT1.5
consistency_0_4FAIL1.5
possibility2_0_4FAIL1.51
possibility3_0_4FAIL1.51
assertion1_0_4FAIL1.51
assertion12_0_4FAIL1.52
possibility11_0_4FAIL1.52
assertion8_0_4FAIL1.52
assertion4_0_4FAIL1.52
assertion2_0_4FAIL1.52
possibility9_0_4FAIL1.52
assertion9_0_4FAIL1.52
assertion7_0_4FAIL1.52
possibility7_0_4FAIL1.52
possibility6_0_4FAIL1.52
possibility5_0_4FAIL1.52
assertion10_0_4FAIL1.53
possibility12_0_4FAIL1.53
possibility1_0_4FAIL1.53
assertion11_0_4FAIL1.53
counter7_64SAT1.53
assertion6_0_4FAIL1.54
possibility8_0_4FAIL1.55
s510_d11_sSAT1.56
Umbrella_tbm_14.tex.moduleQ2.1S.000787UNSAT1.56
Umbrella_tbm_14.tex.moduleQ2.1S.000792UNSAT1.57
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.57
Umbrella_tbm_14.tex.moduleQ2.1S.000812UNSAT1.57
Umbrella_tbm_14.tex.moduleQ2.2S.000001UNSAT1.57
Umbrella_tbm_14.tex.moduleQ2.2S.000003UNSAT1.58
Umbrella_tbm_14.tex.moduleQ2.1S.000720UNSAT1.58
Umbrella_tbm_14.tex.moduleQ2.1S.000773UNSAT1.6
nusmv.tcas^3.B-f2SAT1.6
gttt_2_1_000111_3x3_torus_bSAT1.64
Core1108_tbm_09.tex.moduleQ3.10S.000001UNSAT1.66
Core1108_tbm_09.tex.moduleQ3.9S.000001UNSAT1.66
Core1108_tbm_09.tex.moduleQ3.2S.000010UNSAT1.66
Core1108_tbm_09.tex.moduleQ3.2S.000011UNSAT1.67
tlc03-uniform-depth-52UNSAT1.7
k_d4_n-14SAT1.7
BLOCKS4iii.6UNSAT1.71
c4_BMC_p2_k128UNSAT1.73
k_ph_n-9SAT1.73
s386_d10_uUNSAT1.74
incrementer-enc03-nonuniform-depth-24UNSAT1.75
s499_d15_sSAT1.78
Umbrella_tbm_14.tex.moduleQ2.1S.000757UNSAT1.8
Umbrella_tbm_14.tex.moduleQ2.1S.000749UNSAT1.8
possibility4_0_4FAIL1.81
possibility10_0_4FAIL1.82
Umbrella_tbm_14.tex.moduleQ2.1S.000808UNSAT1.82
k_t4p_p-16UNSAT1.87
s298_d14_sSAT1.88
assertion5_0_4FAIL1.9
Core1108_tbm_09.tex.moduleQ3.2S.000005UNSAT1.9
Umbrella_tbm_14.tex.moduleQ2.2S.000002UNSAT1.92
Umbrella_tbm_25.tex.moduleQ3.2S.000120UNSAT1.94
possibility2_0_5FAIL1.95
k_t4p_p-18UNSAT1.96
Umbrella_tbm_25.tex.moduleQ3.2S.000063UNSAT1.96
possibility10_0_5FAIL1.96
assertion1_0_5FAIL1.96
assertion6_0_5FAIL1.96
possibility5_0_5FAIL1.96
assertion2_0_5FAIL1.97
possibility6_0_5FAIL1.97
assertion7_0_5FAIL1.97
assertion4_0_5FAIL1.97
assertion10_0_5FAIL1.97
assertion12_0_5FAIL1.97
possibility4_0_5FAIL1.98
assertion11_0_5FAIL1.98
assertion8_0_5FAIL1.98
possibility1_0_5FAIL1.98
possibility11_0_5FAIL1.98
possibility3_0_5FAIL1.98
assertion5_0_5FAIL1.98
assertion3_0_5FAIL1.98
possibility9_0_5FAIL1.99
possibility8_0_5FAIL2.01
k_d4_n-15SAT2.05
Core1108_tbm_09.tex.moduleQ3.2S.000007UNSAT2.07
counter8_64SAT2.1
Umbrella_tbm_25.tex.moduleQ3.2S.000052UNSAT2.18
possibility7_0_5FAIL2.38
C5315.blif_0.10_0.20_0_1_inp_exactSAT2.38
possibility12_0_5FAIL2.39
s386_d12_uUNSAT2.47
consistency_0_5FAIL2.47
possibility4_0_6FAIL2.49
consistency_0_6FAIL2.49
possibility11_0_6FAIL2.5
possibility1_0_6FAIL2.5
possibility3_0_6FAIL2.51
assertion6_0_6FAIL2.51
s3330_d3_sSAT2.51
assertion5_0_6FAIL2.51
possibility9_0_6FAIL2.52
assertion1_0_6FAIL2.52
assertion9_0_6FAIL2.52
possibility2_0_6FAIL2.53
assertion11_0_6FAIL2.53
assertion12_0_6FAIL2.53
possibility5_0_6FAIL2.53
possibility6_0_6FAIL2.53
assertion4_0_6FAIL2.54
assertion3_0_6FAIL2.54
assertion8_0_6FAIL2.54
s499_d17_sSAT2.56
query51_query50_1344UNSAT2.56
possibility8_0_6FAIL2.62
k_t4p_n-13SAT2.63
assertion3_0_4FAIL2.7
connect_6x5_5_DUNSAT2.72
assertion2_0_6FAIL2.77
possibility7_0_6FAIL2.8
assertion10_0_6FAIL2.8
s820_d8_sSAT2.81
k_d4_n-20SAT2.82
stmt21_79_304UNSAT2.89
possibility10_0_6FAIL2.94
assertion9_0_5FAIL2.95
k_lin_p-10UNSAT3.06
possibility2_0_7FAIL3.11
possibility1_0_7FAIL3.11
assertion6_0_7FAIL3.12
possibility10_0_7FAIL3.12
assertion1_0_7FAIL3.12
assertion10_0_7FAIL3.12
consistency_0_7FAIL3.12
assertion9_0_7FAIL3.13
assertion11_0_7FAIL3.13
possibility4_0_7FAIL3.13
possibility5_0_7FAIL3.13
possibility7_0_7FAIL3.13
assertion4_0_7FAIL3.14
assertion2_0_7FAIL3.14
assertion7_0_7FAIL3.14
assertion3_0_7FAIL3.15
assertion5_0_7FAIL3.15
possibility9_0_7FAIL3.15
assertion12_0_7FAIL3.15
possibility11_0_7FAIL3.17
assertion8_0_7FAIL3.2
possibility8_0_7FAIL3.22
assertion7_0_6FAIL3.28
k_t4p_n-15SAT3.32
counter7_129SAT3.34
ken.flash^10.C-f3UNSAT3.42
incrementer-enc08-uniform-depth-33SAT3.5
possibility12_0_7FAIL3.59
possibility6_0_7FAIL3.62
possibility12_0_6FAIL3.63
possibility11_0_8FAIL3.79
possibility4_0_8FAIL3.81
assertion11_0_8FAIL3.81
possibility1_0_8FAIL3.81
possibility10_0_8FAIL3.82
possibility6_0_8FAIL3.82
k_t4p_n-14SAT3.82
assertion3_0_8FAIL3.82
assertion12_0_8FAIL3.83
assertion9_0_8FAIL3.83
possibility3_0_8FAIL3.83
possibility2_0_8FAIL3.83
consistency_0_8FAIL3.83
possibility5_0_8FAIL3.84
assertion7_0_8FAIL3.85
assertion5_0_8FAIL3.86
assertion2_0_8FAIL3.86
possibility9_0_8FAIL3.87
toilet_a_10_05.3UNSAT3.87
assertion8_0_8FAIL3.88
possibility12_0_8FAIL3.88
assertion6_0_8FAIL3.88
possibility3_0_7FAIL3.9
possibility8_0_8FAIL3.92
possibility7_0_8FAIL4.03
tlc04-nonuniform-depth-56UNSAT4.03
toilet_c_10_01.12UNSAT4.14
assertion1_0_8FAIL4.16
assertion4_0_8FAIL4.16
k_lin_p-9UNSAT4.19
stmt52_244_394UNSAT4.35
counter8_128SAT4.51
possibility1_0_9FAIL4.61
assertion11_0_9FAIL4.62
assertion6_0_9FAIL4.63
possibility2_0_9FAIL4.64
assertion9_0_9FAIL4.64
assertion8_0_9FAIL4.65
assertion4_0_9FAIL4.65
assertion10_0_9FAIL4.66
consistency_0_9FAIL4.66
possibility7_0_9FAIL4.67
possibility6_0_9FAIL4.67
assertion12_0_9FAIL4.67
possibility3_0_9FAIL4.67
C432.blif_0.10_0.20_0_0_out_exactUNSAT4.67
assertion3_0_9FAIL4.68
assertion5_0_9FAIL4.68
possibility10_0_9FAIL4.69
possibility5_0_9FAIL4.69
assertion2_0_9FAIL4.69
possibility11_0_9FAIL4.72
possibility12_0_9FAIL4.74
lut4_AND_fXORUNSAT4.75
assertion1_0_9FAIL4.76
assertion10_0_8FAIL4.77
assertion7_0_9FAIL4.78
possibility8_0_9FAIL4.82
possibility4_0_9FAIL5.07
possibility9_0_9FAIL5.17
possibility10_0_10FAIL5.58
possibility1_0_10FAIL5.6
possibility11_0_10FAIL5.6
consistency_0_10FAIL5.6
assertion5_0_10FAIL5.62
assertion3_0_10FAIL5.63
possibility3_0_10FAIL5.63
assertion11_0_10FAIL5.63
assertion9_0_10FAIL5.63
possibility4_0_10FAIL5.63
possibility6_0_10FAIL5.64
assertion1_0_10FAIL5.64
possibility9_0_10FAIL5.65
assertion7_0_10FAIL5.65
assertion10_0_10FAIL5.65
assertion2_0_10FAIL5.66
assertion4_0_10FAIL5.66
assertion6_0_10FAIL5.67
possibility11_0_1UNSAT5.69
possibility5_0_10FAIL5.7
possibility7_0_10FAIL5.71
assertion8_0_10FAIL5.74
possibility12_0_10FAIL5.75
CHAIN14v.15SAT5.75
s3330_d4_sSAT5.76
possibility8_0_10FAIL5.81
k_lin_n-3SAT5.87
connect_7x6_4_WUNSAT5.88
texas.PI_main^05.E-f3SAT5.92
possibility2_0_10FAIL5.94
assertion12_0_10FAIL6
assertion2_0_1UNSAT6.12
counter7_128SAT6.16
lognBWLARGEA1UNSAT6.24
k_ph_n-11SAT6.46
s641_d6_sSAT6.47
fpu-10Xh-error01-uniform-depth-5UNSAT7.14
s820_d11_uUNSAT7.24
tlc01-uniform-depth-73UNSAT7.56
lut4_2_f2UNSAT7.7
vonNeumann-ripple-carry-5-cUNSAT7.88
s820_d12_uUNSAT8.8
fpu-10Xe-correct01-nonuniform-depth-6UNSAT8.87
incrementer-enc07-uniform-depth-25UNSAT9.16
nusmv.tcas-t^1.B-d2SAT9.31
s09234_PR_8_2SAT9.59
s499_d22_uUNSAT9.63
texas.PI_main^08.E-f3SAT10.61
s298_d19_uUNSAT11.34
s1269_d8_sSAT11.78
p10-10.pddl_planlen=10SAT11.78
connect_8x7_7_WUNSAT12.24
cnt05SAT12.4
vonNeumann-ripple-carry-6-cUNSAT12.44
s499_d24_uUNSAT13.9
s510_d24_sSAT15.14
emptyroom_e3_ser--opt-20_SAT15.19
s820_d15_uUNSAT15.57
possibility3_0_1UNSAT16.66
vonNeumann-ripple-carry-7-cUNSAT17.42
par16-1-50UNSAT19.26
s298_d22_uUNSAT19.65
ev-pr-4x4-7-3-0-0-1-lgSAT19.78
flipflop-10-cUNSAT20.27
k_lin_n-5SAT21.33
s298_d25_uUNSAT21.45
p10-10.pddl_planlen=6UNSAT22.26
flipflop-11-cUNSAT25.95
s641_d7_uUNSAT26.89
counter8_257SAT28.6
C432.blif_0.10_0.20_0_1_inp_exactSAT29.05
k_lin_p-19UNSAT29.81
lognBWLARGEB1UNSAT30.99
possibility5_0_1UNSAT32.36
gttt_1_1_001020_3x3_wUNSAT32.65
s510_d31_sSAT33.25
k_lin_n-6SAT33.94
possibility10_0_1UNSAT37.64
s641_d8_uUNSAT38.83
k_branch_p-5UNSAT42.18
Umbrella_tbm_24.tex.module.000131SAT43.44
fpu-10Xe-correct01-nonuniform-depth-24UNSAT46.41
fpu-10Xe-correct01-uniform-depth-22UNSAT47.7
s713_d7_uUNSAT49.59
fpu-10Xh-correct04-nonuniform-depth-27UNSAT54.18
k_lin_n-8SAT57.5
b22_PR_8_20SAT60.52
b20_PR_7_20SAT62.95
counter8_256SAT63.26
s510_d36_sSAT66.92
s1196_d3_uUNSAT67.86
vonNeumann-ripple-carry-11-cUNSAT74.24
s713_d8_uUNSAT77.65
dungeon_i25-m12-u3-v0.pddl_planlen=165FAIL88.12
c4_Debug_s5_f2_e2_v1FAIL90.42
vonNeumann-ripple-carry-12-cFAIL100.13
dungeon_i25-m12-u3-v0.pddl_planlen=190FAIL101.03
c2_BMC_p1_k2048FAIL101.42
ev-pr-6x6-17-5-0-1-2-sFAIL102.32
CHAIN16v.17SAT107.53
pipesnotankage14_10FAIL116.22
ev-pr-4x4-9-3-0-0-1-lgSAT121.66
ev-pr-6x6-13-5-0-1-2-sFAIL124.13
s1196_d5_uUNSAT126.03
arbiter-10-comp-error01-qbf-hardness-depth-10UNSAT157.09
ev-pr-6x6-11-5-0-1-2-sFAIL160.72
k_ph_p-10UNSAT168.88
ev-pr-6x6-9-5-0-1-2-sFAIL170.52
k_branch_p-6UNSAT170.71
p20-20.pddl_planlen=23FAIL175.32
dungeon_i10-m5-u10-v0.pddl_planlen=23UNSAT178.57
lut4_3_fANDSAT181.25
stmt28_68_81SAT204.88
Umbrella_tbm_25.tex.moduleQ3.2S.000075UNSAT207.4
ev-pr-4x4-13-3-0-0-1-sFAIL224.62
incrementer-enc02-uniform-depth-58UNSAT229.63
b20_C_3_2FAIL235.23
sortnetsort8.v.stepl.009SAT254.44
ev-pr-8x8-19-7-0-1-2-lgFAIL254.72
k_ph_n-16SAT256.88
pipesnotankage18_8FAIL258.62
toilet_c_10_01.17UNSAT261.94
ev-pr-4x4-15-3-0-0-1-sFAIL276.32
c3_Debug_s3_f2_e2_v2FAIL288.62
ev-pr-8x8-13-7-0-1-2-lgFAIL293.72
cube_c7_ser--opt-24_SAT298.95
ev-pr-4x4-17-3-0-0-1-sFAIL299.42
ev-pr-4x4-7-3-0-0-1-sFAIL305.22
b21_C_3_206FAIL318.52
connect_9x8_6_RFAIL323.23
connect_8x7_6_RFAIL328.12
ev-pr-4x4-11-3-0-0-1-lgSAT337.61
CHAIN23v.24FAIL340.72
dungeon_i10-m10-u10-v0.pddl_planlen=187UNSAT345.21
stmt17_86_98SAT382.04
cnt10SAT417.6
qshifter_8FAIL419.62
ev-pr-8x8-15-7-0-1-2-lgFAIL429.83
stmt17_70_90SAT448.64
driverlog03_7SAT452.17
qshifter_7FAIL476.52
C880.blif_0.10_0.20_0_1_out_exactUNSAT567.63
stmt17_63_82SAT568.69
ev-pr-6x6-9-5-0-1-2-lgFAIL576.52
ev-pr-6x6-17-5-0-1-2-lgFAIL582.44
ring_r6_ser--opt-17_FAIL583.02
k_lin_n-17SAT593.13
c2_Debug_s3_f1_e1_v2FAIL597.11
c1_Debug_s5_f1_e1_v2FAIL597.51
c4_Debug_s3_f2_e2_v2FAIL597.81
c5_BMC_p2_k128FAIL599.11
szymanski-14-sFAIL599.31
szymanski-16-sFAIL599.31
c5_BMC_p2_k64FAIL599.43
network_irda_miniport_nscirda_comm.cFAIL599.52
k14_2_3FAIL599.53
filesys_smbmrx_cvsndrcv.cFAIL599.53
s3330_d12_uFAIL599.53
input_pnpi8042_moudep.cFAIL599.53
query42_query06_1344nFAIL599.53
Adder2-16-sFAIL599.61
s1269_d15_uFAIL599.61
s3330_d9_sFAIL599.61
ev-pr-6x6-19-5-0-1-2-lgFAIL599.61
arbiter-10-comp-error01-qbf-hardness-depth-22FAIL599.61
szymanski-8-sFAIL599.61
ev-pr-6x6-11-5-0-1-2-lgFAIL599.71
uclid-pipe3aFAIL599.71
C6288.blif_0.10_0.20_0_1_out_exactFAIL599.71
adder-14-satFAIL599.71
possibility4_0_1FAIL599.71
C880.blif_0.10_0.20_0_1_inp_exactFAIL599.71
Core1108_tbm_02.tex.moduleQ3.2S.000015FAIL599.71
test2_quant_squaring3FAIL599.71
mutex-32-sFAIL599.71
stmt19_64_99FAIL599.71
mutex-64-sFAIL599.71
audio_ddksynth_csynth2.cppFAIL599.71
cache-coherence-2-fixpoint-6FAIL599.71
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-005FAIL599.71
possibility7_0_1FAIL599.71
sdlx-fixpoint-3FAIL599.71
sortnetsort9.AE.stepl.012FAIL599.71
possibility8_0_1FAIL599.71
C6288.blif_0.10_0.20_0_0_inp_exactFAIL599.71
adder-10-satFAIL599.71
network_ndis_rtlnwifi_hw_hw_ccmp.cFAIL599.71
k_branch_p-16FAIL599.71
k12_4_2FAIL599.71
adder-12-unsatFAIL599.71
possibility12_0_1FAIL599.71
k_branch_n-8FAIL599.71
szymanski-6-sFAIL599.71
rankfunc13_unsigned_64FAIL599.71
gttt_2_2_001020_4x4_wFAIL599.71
dungeon_i15-m7-u4-v0.pddl_planlen=81FAIL599.71
s1269_d13_uFAIL599.71
gttt_2_1_00102030_4x4_torus_bFAIL599.71
assertion1_0_1FAIL599.71
s15850_PR_8_50FAIL599.71
rankfunc33_signed_32FAIL599.71
cnt16rFAIL599.71
possibility1_0_1FAIL599.71
s1269_d12_uFAIL599.71
query44_query26_1344nFAIL599.71
ev-pr-8x8-7-7-0-1-2-lgFAIL599.71
assertion8_0_1FAIL599.71
consistency_0_1FAIL599.71
stmt41_160_235FAIL599.71
k_branch_n-10FAIL599.71
k_branch_p-10FAIL599.71
p20-1.pddl_planlen=24FAIL599.71
assertion9_0_1FAIL599.71
possibility2_0_1FAIL599.71
rankfunc14_signed_64FAIL599.71
ken.flash^08.C-d4FAIL599.71
k_branch_p-11FAIL599.71
rankfunc17_unsigned_16FAIL599.81
assertion3_0_1FAIL599.81
f600-50FAIL599.81
possibility9_0_1FAIL599.81
C6288.blif_0.10_0.20_0_0_out_exactFAIL599.81
emptyroom_e4_ser--opt-44_FAIL599.81
k_ph_p-12FAIL599.81
k_ph_p-19FAIL599.81
mutex-4-sFAIL599.81
sortnetsort9.v.stepl.007FAIL599.81
Umbrella_tbm_05.tex.module.000039FAIL599.81
sortnetsort9.v.stepl.005FAIL599.81
C5315.blif_0.10_0.20_0_0_out_exactFAIL599.81
C6288.blif_0.10_1.00_0_0_out_exactFAIL599.81
ken.oop^2.C-d4FAIL599.81
k_ph_n-21FAIL599.81
C499.blif_0.10_0.20_0_1_out_exactFAIL599.81
szymanski-5-sFAIL599.81
test2_quant_squaring2FAIL599.81
assertion4_0_1FAIL599.81
arbiter-08-comp-error02-qbf-hardness-depth-9FAIL599.81
uclid-pipe2FAIL599.81
k_branch_n-12FAIL599.81
rankfunc5_unsigned_64FAIL599.81
ev-pr-4x4-13-3-0-0-1-lgFAIL599.81
CHAIN22v.23FAIL599.81
C880.blif_0.10_1.00_0_0_inp_exactFAIL599.81
cnt14FAIL599.82
CHAIN20v.21FAIL599.91
sortnetsort10.v.stepl.005FAIL599.91
small-swap2-fixpoint-4FAIL599.91
test3_quant_squaring2FAIL599.91
C499.blif_0.10_0.20_0_0_out_exactFAIL599.91
small-synabs-fixpoint-9FAIL599.91
k8_2_3FAIL599.91
small-swap1-fixpoint-3FAIL599.91
p20-5.pddl_planlen=32FAIL600
test3_quant_squaring4FAIL600.01
k5_2_3FAIL600.02
test1_quant_squaring3FAIL600.02
assertion10_0_1FAIL606.07