QBF Solver Evaluation Portal
Home
QBFLIB
QBFGALLERY'23
QBFEVALs
2022
2020
2019
2018
2017
2016
2010
2008
2007
2006
2005
2004
QBF GALLERIES
QBF Gallery 2014
QBF Gallery 2013
DOWNLOADS
Download the QBFEVAL'22 dataset
Download the QBFEVAL'20 dataset
Download the QBFEVAL'19 dataset and raw results
Download the QBFEVAL'18 dataset and raw results
Download the QBFEVAL'17 dataset and raw results
Download the QBFEVAL'16 dataset
Download the QBFEVAL'10 dataset
Download the QBFEVAL'08 dataset
Download the non-prenex non-cnf track dataset
Download the QBFEVAL'07 dataset
Download the QBFEVAL'06 dataset
Download the QDIMACS to QPRO converter
Download the QDIMACS to QBF1.0 converter
qbflib.org
Instances solved by
ghostq-cegar
QBFEVAL'16 - Prenex non-CNF Track.
Instance
Result
Time
toilet_g_04_01.2
SAT
0.06
z4ml.blif_0.10_1.00_0_1_out_exact
SAT
0.06
tree-exa2-20
UNSAT
0.06
tree-exa2-25
UNSAT
0.06
tree-exa10-10
SAT
0.06
rewriting_k_10
UNSAT
0.06
flipflop-3-c
UNSAT
0.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-001
UNSAT
0.06
incrementer-enc05-uniform-depth-2
UNSAT
0.06
rewriting_k_21
UNSAT
0.07
tree-exa2-35
UNSAT
0.07
z4ml.blif_0.10_0.20_0_1_out_exact
SAT
0.07
rewriting_k_17
UNSAT
0.07
counter6_2
SAT
0.07
stmt44_107_108
SAT
0.07
s27_d4_u
UNSAT
0.07
impl08
SAT
0.07
z4ml.blif_0.10_1.00_0_0_inp_exact
UNSAT
0.07
toilet_a_04_01.4
UNSAT
0.07
toilet_g_08_01.2
SAT
0.07
counter4_3
SAT
0.07
z4ml.blif_0.10_0.20_0_1_inp_exact
SAT
0.07
counter4_2
SAT
0.07
tree-exa2-45
UNSAT
0.07
k_ph_p-3
UNSAT
0.07
ring4_2
SAT
0.07
impl10
SAT
0.07
rewriting_k_19
UNSAT
0.07
toilet_c_06_01.4
UNSAT
0.08
counter4_4
SAT
0.08
counter5_2
SAT
0.08
k_d4_n-1
SAT
0.08
qshifter_3
SAT
0.08
counter7_2
SAT
0.08
ring5_2
SAT
0.08
ring4_3
SAT
0.08
ring6_2
SAT
0.08
s27_d5_u
UNSAT
0.08
impl12
SAT
0.08
impl16
SAT
0.08
k_path_p-2
UNSAT
0.08
k_lin_p-2
UNSAT
0.08
toilet_a_04_01.6
UNSAT
0.09
k_dum_n-1
SAT
0.09
counter5_4
SAT
0.09
stmt17_18_19
SAT
0.09
impl20
SAT
0.09
counter4_6
SAT
0.09
counter8_2
SAT
0.09
toilet_g_15_01.2
SAT
0.09
counter4_5
SAT
0.09
ring5_4
SAT
0.1
counter6_4
SAT
0.1
irst.dme6.B-d2
SAT
0.1
ring4_4
SAT
0.1
k_dum_p-3
UNSAT
0.1
k_poly_n-2
SAT
0.1
k3_1_1
SAT
0.1
semaphore_2
SAT
0.1
eijk.S382.S-d4
SAT
0.1
counter4_7
SAT
0.1
k_dum_p-2
UNSAT
0.1
C5315.blif_0.10_1.00_0_0_out_exact
UNSAT
0.11
counter4_9
SAT
0.11
ring4_5
SAT
0.11
C432.blif_0.10_1.00_0_1_out_exact
SAT
0.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-003
UNSAT
0.11
term1.blif_0.10_1.00_0_1_out_exact
SAT
0.11
counter4_8
SAT
0.11
C5315.blif_0.10_1.00_0_0_inp_exact
UNSAT
0.12
query01_ntrivil_1344
UNSAT
0.12
semaphore3_2
SAT
0.12
counter4_11
SAT
0.12
counter4_10
SAT
0.12
k_grz_n-2
SAT
0.12
ring6_4
SAT
0.12
ring4_6
SAT
0.12
counter7_4
SAT
0.12
semaphore_3
SAT
0.13
mutex-2-s
SAT
0.13
toilet_g_20_01.2
SAT
0.13
lut4_XOR_fOR
UNSAT
0.13
counter5_8
SAT
0.13
par8-1-c-50
UNSAT
0.13
counter8_4
SAT
0.13
ring4_7
SAT
0.14
counter4_13
SAT
0.14
k_dum_n-5
SAT
0.14
term1.blif_0.10_1.00_0_0_out_exact
UNSAT
0.14
semaphore4_2
SAT
0.14
k_dum_p-6
UNSAT
0.15
ring5_8
SAT
0.15
ring4_8
SAT
0.15
k_poly_p-4
UNSAT
0.15
counter4_15
SAT
0.15
k_d4_n-2
SAT
0.15
counter4_16
SAT
0.16
semaphore5_2
SAT
0.16
semaphore_4
SAT
0.16
stmt27_296_297
SAT
0.16
s641_d2_s
SAT
0.16
k_branch_n-2
SAT
0.16
counter6_8
SAT
0.16
counter4_14
SAT
0.16
toilet_a_06_01.6
UNSAT
0.16
term1.blif_0.10_0.20_0_1_inp_exact
SAT
0.17
k_ph_p-5
UNSAT
0.17
k_grz_n-5
SAT
0.17
semaphore3_3
SAT
0.17
s713_d2_s
SAT
0.17
stmt27_16_97
UNSAT
0.18
C499.blif_0.10_1.00_0_1_inp_exact
SAT
0.18
biu.mv.xl_ao.bb-b001-p010-IPF05-c07.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-003
SAT
0.18
k_ph_n-6
SAT
0.18
k_poly_n-7
SAT
0.19
semaphore_5
SAT
0.19
ring6_8
SAT
0.19
dmeSmall_2
SAT
0.19
k_t4p_n-2
SAT
0.19
Core1108_tbm_21.tex.module.000091
UNSAT
0.19
counter7_8
SAT
0.2
toilet_c_08_05.4
SAT
0.2
semaphore6_2
SAT
0.2
k_path_n-5
SAT
0.2
s510_d3_s
SAT
0.2
counter5_16
SAT
0.21
s01238_PR_8_2
SAT
0.21
k_poly_p-7
UNSAT
0.21
Umbrella_tbm_24.tex.module.000103
UNSAT
0.21
semaphore4_3
SAT
0.21
counter4_12
SAT
0.22
Core1108_tbm_21.tex.module.000027
UNSAT
0.22
Core1108_tbm_03.tex.module.000092
UNSAT
0.22
rewriting_k_100
UNSAT
0.22
Core1108_tbm_03.tex.module.000064
UNSAT
0.22
Core1108_tbm_03.tex.module.000058
UNSAT
0.22
Core1108_tbm_03.tex.module.000056
UNSAT
0.22
Core1108_tbm_03.tex.module.000057
UNSAT
0.22
Umbrella_tbm_24.tex.module.000066
UNSAT
0.22
Core1108_tbm_03.tex.module.000021
UNSAT
0.22
semaphore3_4
SAT
0.22
Core1108_tbm_03.tex.module.000065
UNSAT
0.22
Core1108_tbm_03.tex.module.000090
UNSAT
0.23
s386_d3_s
SAT
0.23
Core1108_tbm_21.tex.module.000014
UNSAT
0.23
counter8_8
SAT
0.23
arbiter-07-comp-error01-qbf-hardness-depth-4
UNSAT
0.23
Core1108_tbm_21.tex.module.000030
UNSAT
0.23
Core1108_tbm_03.tex.module.000048
UNSAT
0.23
Core1108_tbm_03.tex.module.000038
UNSAT
0.24
Core1108_tbm_03.tex.module.000031
UNSAT
0.24
Umbrella_tbm_29.tex.module.000078
UNSAT
0.24
Core1108_tbm_21.tex.module.000009
UNSAT
0.24
k_dum_n-12
SAT
0.24
Core1108_tbm_21.tex.module.000010
UNSAT
0.24
lights3_035_0_027
UNSAT
0.24
lights3_035_0_051
UNSAT
0.24
Core1108_tbm_21.tex.module.000026
UNSAT
0.24
biu.mv.xl_ao.bb-b001-p010-IPF02-c08.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-003
SAT
0.24
C432.blif_0.10_1.00_0_0_out_exact
UNSAT
0.24
Core1108_tbm_03.tex.module.000003
UNSAT
0.24
Core1108_tbm_21.tex.module.000008
UNSAT
0.24
k_poly_p-8
UNSAT
0.24
semaphore5_3
SAT
0.25
biu.mv.xl_ao.bb-b001-p010-OPF02-c08.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-003
SAT
0.25
Core1108_tbm_03.tex.module.000039
UNSAT
0.25
vis.4-arbit^2.E-f2
SAT
0.25
Core1108_tbm_03.tex.module.000037
UNSAT
0.25
Core1108_tbm_03.tex.module.000023
UNSAT
0.25
k_dum_p-12
UNSAT
0.26
k_grz_p-10
UNSAT
0.26
ring5_16
SAT
0.26
Core1108_tbm_03.tex.module.000034
UNSAT
0.26
stmt16_950_951
SAT
0.26
s1196_d2_s
SAT
0.26
k_t4p_p-4
UNSAT
0.27
b12_PR_9_2
SAT
0.27
Core1108_tbm_03.tex.module.000019
UNSAT
0.28
Core1108_tbm_21.tex.module.000017
UNSAT
0.28
counter6_16
SAT
0.28
semaphore4_4
SAT
0.28
Umbrella_tbm_29.tex.module.000010
UNSAT
0.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-003
UNSAT
0.29
arbiter-06-comp-error02-qbf-hardness-depth-5
UNSAT
0.29
Adder2-2-c
UNSAT
0.29
Umbrella_tbm_29.tex.module.000009
UNSAT
0.29
semaphore6_3
SAT
0.3
k_dum_p-16
UNSAT
0.3
s386_d4_s
SAT
0.3
Umbrella_tbm_05.tex.module.000088
UNSAT
0.31
dme1_2
SAT
0.31
k_d4_p-8
UNSAT
0.31
Umbrella_tbm_21.tex.module.000139
UNSAT
0.32
Umbrella_tbm_21.tex.module.000129
UNSAT
0.32
Umbrella_tbm_26.tex.module.000061
UNSAT
0.32
Umbrella_tbm_21.tex.module.000134
UNSAT
0.32
ring6_16
SAT
0.32
k_grz_p-13
UNSAT
0.32
Umbrella_tbm_21.tex.module.000056
UNSAT
0.33
Umbrella_tbm_26.tex.module.000004
UNSAT
0.33
Umbrella_tbm_26.tex.module.000041
UNSAT
0.33
counter7_16
SAT
0.33
Umbrella_tbm_21.tex.module.000149
UNSAT
0.33
Umbrella_tbm_21.tex.module.000044
UNSAT
0.34
semaphore5_4
SAT
0.34
Core1108_tbm_09.tex.module.000033
UNSAT
0.34
k_grz_p-11
UNSAT
0.34
Umbrella_tbm_21.tex.module.000049
UNSAT
0.34
k_dum_n-17
SAT
0.34
Umbrella_tbm_21.tex.module.000079
UNSAT
0.34
Umbrella_tbm_21.tex.module.000069
UNSAT
0.35
Core1108_tbm_09.tex.module.000028
UNSAT
0.35
par8-4-50
UNSAT
0.36
k_grz_n-10
SAT
0.36
Umbrella_tbm_26.tex.module.000021
UNSAT
0.36
k_path_n-9
SAT
0.36
Umbrella_tbm_05.tex.module.000064
UNSAT
0.37
Core1108_tbm_09.tex.module.000010
UNSAT
0.37
Core1108_tbm_09.tex.module.000008
UNSAT
0.37
Core1108_tbm_09.tex.module.000009
UNSAT
0.37
Umbrella_tbm_21.tex.module.000024
UNSAT
0.38
counter5_32
SAT
0.38
Umbrella_tbm_05.tex.module.000079
UNSAT
0.38
Umbrella_tbm_21.tex.module.000029
UNSAT
0.38
k_path_p-5
UNSAT
0.38
dme1_3
SAT
0.38
Umbrella_tbm_25.tex.module.000106
UNSAT
0.39
s820_d3_s
SAT
0.4
Umbrella_tbm_25.tex.module.000084
UNSAT
0.4
Umbrella_tbm_05.tex.module.000053
UNSAT
0.4
Umbrella_tbm_05.tex.module.000065
UNSAT
0.4
Umbrella_tbm_25.tex.module.000087
UNSAT
0.4
Umbrella_tbm_25.tex.module.000121
UNSAT
0.4
k_dum_n-18
SAT
0.41
semaphore6_4
SAT
0.41
C880.blif_0.10_1.00_0_0_out_exact
UNSAT
0.41
Core1108_tbm_21.tex.module.000023
UNSAT
0.41
BLOCKS3ii.4.3
UNSAT
0.41
counter8_16
SAT
0.41
dmeSmall_4
SAT
0.42
Umbrella_tbm_05.tex.module.000043
UNSAT
0.42
s641_d4_s
SAT
0.42
counter5_33
SAT
0.43
s713_d4_s
SAT
0.44
stmt41_738_749
SAT
0.44
k_grz_n-20
SAT
0.44
Umbrella_tbm_25.tex.module.000099
UNSAT
0.44
k_poly_n-17
SAT
0.45
Umbrella_tbm_05.tex.module.000025
UNSAT
0.45
W3-Umbrella_tbm_21.tex.moduleQ3.6S.000001
UNSAT
0.45
tlc03-nonuniform-depth-17
UNSAT
0.45
k_poly_n-18
SAT
0.46
Umbrella_tbm_05.tex.module.000030
UNSAT
0.46
ring_r3_ser--opt-8_
SAT
0.46
k_path_n-12
SAT
0.47
k_poly_p-16
UNSAT
0.47
Umbrella_tbm_25.tex.module.000041
UNSAT
0.48
Umbrella_tbm_25.tex.module.000031
UNSAT
0.48
ring5_33
SAT
0.48
k_d4_p-11
UNSAT
0.48
Umbrella_tbm_05.tex.module.000015
UNSAT
0.48
Umbrella_tbm_25.tex.module.000003
UNSAT
0.48
W4-Umbrella_tbm_26.tex.moduleQ3.7S.000003
UNSAT
0.48
ring5_32
SAT
0.49
counter6_32
SAT
0.49
k_path_p-14
UNSAT
0.49
Umbrella_tbm_05.tex.module.000011
UNSAT
0.49
stmt19_90_266
UNSAT
0.5
flipflop-5-c
UNSAT
0.5
s499_d7_s
SAT
0.51
W5-Umbrella_tbm_26.tex.moduleQ3.7S.000003
UNSAT
0.52
W4-Umbrella_tbm_21.tex.moduleQ3.6S.000001
UNSAT
0.52
k_path_p-16
UNSAT
0.54
Core1108_tbm_21.tex.moduleQ3.2S.000002
UNSAT
0.54
Core1108_tbm_21.tex.moduleQ3.2S.000011
UNSAT
0.54
Core1108_tbm_21.tex.moduleQ3.2S.000027
UNSAT
0.54
ii32b1-00
SAT
0.54
k_grz_p-17
UNSAT
0.54
biu.mv.xl_ao.bb-b001-p005-OPF05-c02.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-004
SAT
0.54
k_d4_p-13
UNSAT
0.55
C499.blif_0.10_1.00_0_0_out_exact
UNSAT
0.55
Core1108_tbm_21.tex.moduleQ3.2S.000014
UNSAT
0.56
dme1_4
SAT
0.56
Core1108_tbm_21.tex.moduleQ3.2S.000024
UNSAT
0.57
Core1108_tbm_21.tex.moduleQ3.2S.000015
UNSAT
0.58
Core1108_tbm_28.tex.moduleQ2.2S.000003
UNSAT
0.58
Core1108_tbm_03.tex.moduleQ3.2S.000003
UNSAT
0.58
s3330_d2_s
SAT
0.59
Core1108_tbm_21.tex.moduleQ3.2S.000019
UNSAT
0.59
k_poly_n-21
SAT
0.59
tlc03-uniform-depth-21
UNSAT
0.59
ring6_32
SAT
0.6
Core1108_tbm_03.tex.moduleQ3.2S.000048
UNSAT
0.6
k_poly_p-19
UNSAT
0.61
Core1108_tbm_03.tex.moduleQ3.2S.000002
UNSAT
0.61
Core1108_tbm_21.tex.moduleQ3.2S.000007
UNSAT
0.61
k_t4p_n-5
SAT
0.61
toilet_a_08_05.2
UNSAT
0.62
Core1108_tbm_03.tex.moduleQ3.2S.000009
UNSAT
0.62
dme1_5
SAT
0.63
s1269_d3_s
SAT
0.64
Core1108_tbm_03.tex.moduleQ3.2S.000011
UNSAT
0.65
Core1108_tbm_02.tex.moduleQ3.2S.000026
UNSAT
0.66
Core1108_tbm_02.tex.moduleQ3.2S.000007
UNSAT
0.66
k_grz_n-21
SAT
0.66
query48_query15_1344
UNSAT
0.66
Core1108_tbm_02.tex.moduleQ3.2S.000095
UNSAT
0.66
Core1108_tbm_02.tex.moduleQ3.2S.000056
UNSAT
0.67
BLOCKS3iii.5
SAT
0.68
dmeSmall_8
SAT
0.68
Core1108_tbm_02.tex.moduleQ3.2S.000108
UNSAT
0.69
Core1108_tbm_02.tex.moduleQ3.2S.000077
UNSAT
0.69
Core1108_tbm_02.tex.moduleQ3.2S.000098
UNSAT
0.69
Core1108_tbm_03.tex.moduleQ3.2S.000018
UNSAT
0.7
W4-Umbrella_tbm_25.tex.moduleQ3.7S.000003
UNSAT
0.72
Core1108_tbm_02.tex.moduleQ3.2S.000099
UNSAT
0.74
k_grz_p-18
UNSAT
0.75
dmeSmall_9
SAT
0.76
dme1_6
SAT
0.77
possibility3_0_2
FAIL
0.77
assertion3_0_2
FAIL
0.77
possibility1_0_2
FAIL
0.78
assertion6_0_2
FAIL
0.78
possibility5_0_2
FAIL
0.78
assertion5_0_2
FAIL
0.78
possibility10_0_2
FAIL
0.78
assertion10_0_2
FAIL
0.78
assertion4_0_2
FAIL
0.78
possibility11_0_2
FAIL
0.78
assertion11_0_2
FAIL
0.78
consistency_0_2
FAIL
0.78
assertion9_0_2
FAIL
0.78
assertion1_0_2
FAIL
0.78
assertion2_0_2
FAIL
0.78
assertion7_0_2
FAIL
0.78
possibility8_0_2
FAIL
0.78
possibility2_0_2
FAIL
0.78
possibility6_0_2
FAIL
0.78
possibility9_0_2
FAIL
0.78
assertion12_0_2
FAIL
0.78
possibility7_0_2
FAIL
0.78
possibility12_0_2
FAIL
0.79
counter7_32
SAT
0.83
k_d4_p-17
UNSAT
0.83
W5-Umbrella_tbm_05.tex.moduleQ3.8S.000001
UNSAT
0.85
Umbrella_tbm_29.tex.moduleQ2.2S.000001
UNSAT
0.86
W5-Umbrella_tbm_25.tex.moduleQ3.7S.000003
UNSAT
0.87
possibility4_0_2
FAIL
0.88
counter8_32
SAT
0.88
dme1_7
SAT
0.92
counter_e_2
SAT
0.92
term1.blif_0.10_0.20_0_0_out_exact
UNSAT
0.93
k_path_p-10
UNSAT
0.96
possibility6_0_1
UNSAT
0.97
assertion11_0_1
UNSAT
0.97
assertion12_0_1
UNSAT
0.97
biu.mv.xl_ao.bb-b001-p010-MIF01-c01.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-004
SAT
0.98
c4_BMC_p1_k32
SAT
0.98
k_t4p_p-12
UNSAT
0.98
assertion5_0_1
UNSAT
1.01
Umbrella_tbm_24.tex.moduleQ2.1S.000136
UNSAT
1.01
Umbrella_tbm_26.tex.moduleQ3.2S.000009
UNSAT
1.02
BLOCKS3i.5.3
UNSAT
1.03
W4-Umbrella_tbm_05.tex.moduleQ3.8S.000001
UNSAT
1.04
assertion7_0_1
UNSAT
1.04
Umbrella_tbm_26.tex.moduleQ3.2S.000037
UNSAT
1.04
k_d4_p-20
UNSAT
1.05
Umbrella_tbm_23.tex.moduleQ1.2S.000001
UNSAT
1.05
dme1_8
SAT
1.05
counter6_64
SAT
1.05
Umbrella_tbm_26.tex.moduleQ3.2S.000014
UNSAT
1.05
counter6_65
SAT
1.06
Umbrella_tbm_26.tex.moduleQ3.2S.000041
UNSAT
1.06
assertion8_0_2
FAIL
1.06
assertion6_0_3
FAIL
1.11
s386_d8_u
UNSAT
1.11
k_branch_n-3
SAT
1.11
assertion6_0_1
UNSAT
1.11
possibility6_0_3
FAIL
1.12
possibility9_0_3
FAIL
1.12
assertion12_0_3
FAIL
1.12
assertion3_0_3
FAIL
1.12
possibility10_0_3
FAIL
1.12
assertion11_0_3
FAIL
1.12
BLOCKS3ii.5.3
SAT
1.12
possibility2_0_3
FAIL
1.12
possibility1_0_3
FAIL
1.12
consistency_0_3
FAIL
1.12
possibility7_0_3
FAIL
1.13
assertion9_0_3
FAIL
1.13
assertion1_0_3
FAIL
1.13
possibility3_0_3
FAIL
1.13
possibility11_0_3
FAIL
1.13
assertion8_0_3
FAIL
1.13
assertion2_0_3
FAIL
1.13
assertion5_0_3
FAIL
1.13
possibility12_0_3
FAIL
1.13
toilet_c_08_01.11
UNSAT
1.14
assertion4_0_3
FAIL
1.14
assertion7_0_3
FAIL
1.14
possibility5_0_3
FAIL
1.14
k_path_n-16
SAT
1.15
possibility8_0_3
FAIL
1.15
k_path_n-13
SAT
1.16
Umbrella_tbm_24.tex.moduleQ2.1S.000188
UNSAT
1.17
s298_d12_s
SAT
1.19
Umbrella_tbm_24.tex.moduleQ2.1S.000022
UNSAT
1.26
ring6_65
SAT
1.27
ring_r4_ser--opt-11_
UNSAT
1.29
gttt_1_1_000111_3x3_torus_w
UNSAT
1.29
k_lin_p-4
UNSAT
1.3
lut4_2_fXOR
SAT
1.31
flipflop-6-c
UNSAT
1.33
Umbrella_tbm_26.tex.moduleQ3.2S.000020
UNSAT
1.36
ring6_64
SAT
1.37
Core1108_tbm_09.tex.moduleQ3.2S.000003
UNSAT
1.38
assertion10_0_3
FAIL
1.45
s713_d6_s
SAT
1.46
possibility4_0_3
FAIL
1.48
k_t4p_p-15
UNSAT
1.5
consistency_0_4
FAIL
1.5
possibility2_0_4
FAIL
1.51
possibility3_0_4
FAIL
1.51
assertion1_0_4
FAIL
1.51
assertion12_0_4
FAIL
1.52
possibility11_0_4
FAIL
1.52
assertion8_0_4
FAIL
1.52
assertion4_0_4
FAIL
1.52
assertion2_0_4
FAIL
1.52
possibility9_0_4
FAIL
1.52
assertion9_0_4
FAIL
1.52
assertion7_0_4
FAIL
1.52
possibility7_0_4
FAIL
1.52
possibility6_0_4
FAIL
1.52
possibility5_0_4
FAIL
1.52
assertion10_0_4
FAIL
1.53
possibility12_0_4
FAIL
1.53
possibility1_0_4
FAIL
1.53
assertion11_0_4
FAIL
1.53
counter7_64
SAT
1.53
assertion6_0_4
FAIL
1.54
possibility8_0_4
FAIL
1.55
s510_d11_s
SAT
1.56
Umbrella_tbm_14.tex.moduleQ2.1S.000787
UNSAT
1.56
Umbrella_tbm_14.tex.moduleQ2.1S.000792
UNSAT
1.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-005
UNSAT
1.57
Umbrella_tbm_14.tex.moduleQ2.1S.000812
UNSAT
1.57
Umbrella_tbm_14.tex.moduleQ2.2S.000001
UNSAT
1.57
Umbrella_tbm_14.tex.moduleQ2.2S.000003
UNSAT
1.58
Umbrella_tbm_14.tex.moduleQ2.1S.000720
UNSAT
1.58
Umbrella_tbm_14.tex.moduleQ2.1S.000773
UNSAT
1.6
nusmv.tcas^3.B-f2
SAT
1.6
gttt_2_1_000111_3x3_torus_b
SAT
1.64
Core1108_tbm_09.tex.moduleQ3.10S.000001
UNSAT
1.66
Core1108_tbm_09.tex.moduleQ3.9S.000001
UNSAT
1.66
Core1108_tbm_09.tex.moduleQ3.2S.000010
UNSAT
1.66
Core1108_tbm_09.tex.moduleQ3.2S.000011
UNSAT
1.67
tlc03-uniform-depth-52
UNSAT
1.7
k_d4_n-14
SAT
1.7
BLOCKS4iii.6
UNSAT
1.71
c4_BMC_p2_k128
UNSAT
1.73
k_ph_n-9
SAT
1.73
s386_d10_u
UNSAT
1.74
incrementer-enc03-nonuniform-depth-24
UNSAT
1.75
s499_d15_s
SAT
1.78
Umbrella_tbm_14.tex.moduleQ2.1S.000757
UNSAT
1.8
Umbrella_tbm_14.tex.moduleQ2.1S.000749
UNSAT
1.8
possibility4_0_4
FAIL
1.81
possibility10_0_4
FAIL
1.82
Umbrella_tbm_14.tex.moduleQ2.1S.000808
UNSAT
1.82
k_t4p_p-16
UNSAT
1.87
s298_d14_s
SAT
1.88
assertion5_0_4
FAIL
1.9
Core1108_tbm_09.tex.moduleQ3.2S.000005
UNSAT
1.9
Umbrella_tbm_14.tex.moduleQ2.2S.000002
UNSAT
1.92
Umbrella_tbm_25.tex.moduleQ3.2S.000120
UNSAT
1.94
possibility2_0_5
FAIL
1.95
k_t4p_p-18
UNSAT
1.96
Umbrella_tbm_25.tex.moduleQ3.2S.000063
UNSAT
1.96
possibility10_0_5
FAIL
1.96
assertion1_0_5
FAIL
1.96
assertion6_0_5
FAIL
1.96
possibility5_0_5
FAIL
1.96
assertion2_0_5
FAIL
1.97
possibility6_0_5
FAIL
1.97
assertion7_0_5
FAIL
1.97
assertion4_0_5
FAIL
1.97
assertion10_0_5
FAIL
1.97
assertion12_0_5
FAIL
1.97
possibility4_0_5
FAIL
1.98
assertion11_0_5
FAIL
1.98
assertion8_0_5
FAIL
1.98
possibility1_0_5
FAIL
1.98
possibility11_0_5
FAIL
1.98
possibility3_0_5
FAIL
1.98
assertion5_0_5
FAIL
1.98
assertion3_0_5
FAIL
1.98
possibility9_0_5
FAIL
1.99
possibility8_0_5
FAIL
2.01
k_d4_n-15
SAT
2.05
Core1108_tbm_09.tex.moduleQ3.2S.000007
UNSAT
2.07
counter8_64
SAT
2.1
Umbrella_tbm_25.tex.moduleQ3.2S.000052
UNSAT
2.18
possibility7_0_5
FAIL
2.38
C5315.blif_0.10_0.20_0_1_inp_exact
SAT
2.38
possibility12_0_5
FAIL
2.39
s386_d12_u
UNSAT
2.47
consistency_0_5
FAIL
2.47
possibility4_0_6
FAIL
2.49
consistency_0_6
FAIL
2.49
possibility11_0_6
FAIL
2.5
possibility1_0_6
FAIL
2.5
possibility3_0_6
FAIL
2.51
assertion6_0_6
FAIL
2.51
s3330_d3_s
SAT
2.51
assertion5_0_6
FAIL
2.51
possibility9_0_6
FAIL
2.52
assertion1_0_6
FAIL
2.52
assertion9_0_6
FAIL
2.52
possibility2_0_6
FAIL
2.53
assertion11_0_6
FAIL
2.53
assertion12_0_6
FAIL
2.53
possibility5_0_6
FAIL
2.53
possibility6_0_6
FAIL
2.53
assertion4_0_6
FAIL
2.54
assertion3_0_6
FAIL
2.54
assertion8_0_6
FAIL
2.54
s499_d17_s
SAT
2.56
query51_query50_1344
UNSAT
2.56
possibility8_0_6
FAIL
2.62
k_t4p_n-13
SAT
2.63
assertion3_0_4
FAIL
2.7
connect_6x5_5_D
UNSAT
2.72
assertion2_0_6
FAIL
2.77
possibility7_0_6
FAIL
2.8
assertion10_0_6
FAIL
2.8
s820_d8_s
SAT
2.81
k_d4_n-20
SAT
2.82
stmt21_79_304
UNSAT
2.89
possibility10_0_6
FAIL
2.94
assertion9_0_5
FAIL
2.95
k_lin_p-10
UNSAT
3.06
possibility2_0_7
FAIL
3.11
possibility1_0_7
FAIL
3.11
assertion6_0_7
FAIL
3.12
possibility10_0_7
FAIL
3.12
assertion1_0_7
FAIL
3.12
assertion10_0_7
FAIL
3.12
consistency_0_7
FAIL
3.12
assertion9_0_7
FAIL
3.13
assertion11_0_7
FAIL
3.13
possibility4_0_7
FAIL
3.13
possibility5_0_7
FAIL
3.13
possibility7_0_7
FAIL
3.13
assertion4_0_7
FAIL
3.14
assertion2_0_7
FAIL
3.14
assertion7_0_7
FAIL
3.14
assertion3_0_7
FAIL
3.15
assertion5_0_7
FAIL
3.15
possibility9_0_7
FAIL
3.15
assertion12_0_7
FAIL
3.15
possibility11_0_7
FAIL
3.17
assertion8_0_7
FAIL
3.2
possibility8_0_7
FAIL
3.22
assertion7_0_6
FAIL
3.28
k_t4p_n-15
SAT
3.32
counter7_129
SAT
3.34
ken.flash^10.C-f3
UNSAT
3.42
incrementer-enc08-uniform-depth-33
SAT
3.5
possibility12_0_7
FAIL
3.59
possibility6_0_7
FAIL
3.62
possibility12_0_6
FAIL
3.63
possibility11_0_8
FAIL
3.79
possibility4_0_8
FAIL
3.81
assertion11_0_8
FAIL
3.81
possibility1_0_8
FAIL
3.81
possibility10_0_8
FAIL
3.82
possibility6_0_8
FAIL
3.82
k_t4p_n-14
SAT
3.82
assertion3_0_8
FAIL
3.82
assertion12_0_8
FAIL
3.83
assertion9_0_8
FAIL
3.83
possibility3_0_8
FAIL
3.83
possibility2_0_8
FAIL
3.83
consistency_0_8
FAIL
3.83
possibility5_0_8
FAIL
3.84
assertion7_0_8
FAIL
3.85
assertion5_0_8
FAIL
3.86
assertion2_0_8
FAIL
3.86
possibility9_0_8
FAIL
3.87
toilet_a_10_05.3
UNSAT
3.87
assertion8_0_8
FAIL
3.88
possibility12_0_8
FAIL
3.88
assertion6_0_8
FAIL
3.88
possibility3_0_7
FAIL
3.9
possibility8_0_8
FAIL
3.92
possibility7_0_8
FAIL
4.03
tlc04-nonuniform-depth-56
UNSAT
4.03
toilet_c_10_01.12
UNSAT
4.14
assertion1_0_8
FAIL
4.16
assertion4_0_8
FAIL
4.16
k_lin_p-9
UNSAT
4.19
stmt52_244_394
UNSAT
4.35
counter8_128
SAT
4.51
possibility1_0_9
FAIL
4.61
assertion11_0_9
FAIL
4.62
assertion6_0_9
FAIL
4.63
possibility2_0_9
FAIL
4.64
assertion9_0_9
FAIL
4.64
assertion8_0_9
FAIL
4.65
assertion4_0_9
FAIL
4.65
assertion10_0_9
FAIL
4.66
consistency_0_9
FAIL
4.66
possibility7_0_9
FAIL
4.67
possibility6_0_9
FAIL
4.67
assertion12_0_9
FAIL
4.67
possibility3_0_9
FAIL
4.67
C432.blif_0.10_0.20_0_0_out_exact
UNSAT
4.67
assertion3_0_9
FAIL
4.68
assertion5_0_9
FAIL
4.68
possibility10_0_9
FAIL
4.69
possibility5_0_9
FAIL
4.69
assertion2_0_9
FAIL
4.69
possibility11_0_9
FAIL
4.72
possibility12_0_9
FAIL
4.74
lut4_AND_fXOR
UNSAT
4.75
assertion1_0_9
FAIL
4.76
assertion10_0_8
FAIL
4.77
assertion7_0_9
FAIL
4.78
possibility8_0_9
FAIL
4.82
possibility4_0_9
FAIL
5.07
possibility9_0_9
FAIL
5.17
possibility10_0_10
FAIL
5.58
possibility1_0_10
FAIL
5.6
possibility11_0_10
FAIL
5.6
consistency_0_10
FAIL
5.6
assertion5_0_10
FAIL
5.62
assertion3_0_10
FAIL
5.63
possibility3_0_10
FAIL
5.63
assertion11_0_10
FAIL
5.63
assertion9_0_10
FAIL
5.63
possibility4_0_10
FAIL
5.63
possibility6_0_10
FAIL
5.64
assertion1_0_10
FAIL
5.64
possibility9_0_10
FAIL
5.65
assertion7_0_10
FAIL
5.65
assertion10_0_10
FAIL
5.65
assertion2_0_10
FAIL
5.66
assertion4_0_10
FAIL
5.66
assertion6_0_10
FAIL
5.67
possibility11_0_1
UNSAT
5.69
possibility5_0_10
FAIL
5.7
possibility7_0_10
FAIL
5.71
assertion8_0_10
FAIL
5.74
possibility12_0_10
FAIL
5.75
CHAIN14v.15
SAT
5.75
s3330_d4_s
SAT
5.76
possibility8_0_10
FAIL
5.81
k_lin_n-3
SAT
5.87
connect_7x6_4_W
UNSAT
5.88
texas.PI_main^05.E-f3
SAT
5.92
possibility2_0_10
FAIL
5.94
assertion12_0_10
FAIL
6
assertion2_0_1
UNSAT
6.12
counter7_128
SAT
6.16
lognBWLARGEA1
UNSAT
6.24
k_ph_n-11
SAT
6.46
s641_d6_s
SAT
6.47
fpu-10Xh-error01-uniform-depth-5
UNSAT
7.14
s820_d11_u
UNSAT
7.24
tlc01-uniform-depth-73
UNSAT
7.56
lut4_2_f2
UNSAT
7.7
vonNeumann-ripple-carry-5-c
UNSAT
7.88
s820_d12_u
UNSAT
8.8
fpu-10Xe-correct01-nonuniform-depth-6
UNSAT
8.87
incrementer-enc07-uniform-depth-25
UNSAT
9.16
nusmv.tcas-t^1.B-d2
SAT
9.31
s09234_PR_8_2
SAT
9.59
s499_d22_u
UNSAT
9.63
texas.PI_main^08.E-f3
SAT
10.61
s298_d19_u
UNSAT
11.34
s1269_d8_s
SAT
11.78
p10-10.pddl_planlen=10
SAT
11.78
connect_8x7_7_W
UNSAT
12.24
cnt05
SAT
12.4
vonNeumann-ripple-carry-6-c
UNSAT
12.44
s499_d24_u
UNSAT
13.9
s510_d24_s
SAT
15.14
emptyroom_e3_ser--opt-20_
SAT
15.19
s820_d15_u
UNSAT
15.57
possibility3_0_1
UNSAT
16.66
vonNeumann-ripple-carry-7-c
UNSAT
17.42
par16-1-50
UNSAT
19.26
s298_d22_u
UNSAT
19.65
ev-pr-4x4-7-3-0-0-1-lg
SAT
19.78
flipflop-10-c
UNSAT
20.27
k_lin_n-5
SAT
21.33
s298_d25_u
UNSAT
21.45
p10-10.pddl_planlen=6
UNSAT
22.26
flipflop-11-c
UNSAT
25.95
s641_d7_u
UNSAT
26.89
counter8_257
SAT
28.6
C432.blif_0.10_0.20_0_1_inp_exact
SAT
29.05
k_lin_p-19
UNSAT
29.81
lognBWLARGEB1
UNSAT
30.99
possibility5_0_1
UNSAT
32.36
gttt_1_1_001020_3x3_w
UNSAT
32.65
s510_d31_s
SAT
33.25
k_lin_n-6
SAT
33.94
possibility10_0_1
UNSAT
37.64
s641_d8_u
UNSAT
38.83
k_branch_p-5
UNSAT
42.18
Umbrella_tbm_24.tex.module.000131
SAT
43.44
fpu-10Xe-correct01-nonuniform-depth-24
UNSAT
46.41
fpu-10Xe-correct01-uniform-depth-22
UNSAT
47.7
s713_d7_u
UNSAT
49.59
fpu-10Xh-correct04-nonuniform-depth-27
UNSAT
54.18
k_lin_n-8
SAT
57.5
b22_PR_8_20
SAT
60.52
b20_PR_7_20
SAT
62.95
counter8_256
SAT
63.26
s510_d36_s
SAT
66.92
s1196_d3_u
UNSAT
67.86
vonNeumann-ripple-carry-11-c
UNSAT
74.24
s713_d8_u
UNSAT
77.65
dungeon_i25-m12-u3-v0.pddl_planlen=165
FAIL
88.12
c4_Debug_s5_f2_e2_v1
FAIL
90.42
vonNeumann-ripple-carry-12-c
FAIL
100.13
dungeon_i25-m12-u3-v0.pddl_planlen=190
FAIL
101.03
c2_BMC_p1_k2048
FAIL
101.42
ev-pr-6x6-17-5-0-1-2-s
FAIL
102.32
CHAIN16v.17
SAT
107.53
pipesnotankage14_10
FAIL
116.22
ev-pr-4x4-9-3-0-0-1-lg
SAT
121.66
ev-pr-6x6-13-5-0-1-2-s
FAIL
124.13
s1196_d5_u
UNSAT
126.03
arbiter-10-comp-error01-qbf-hardness-depth-10
UNSAT
157.09
ev-pr-6x6-11-5-0-1-2-s
FAIL
160.72
k_ph_p-10
UNSAT
168.88
ev-pr-6x6-9-5-0-1-2-s
FAIL
170.52
k_branch_p-6
UNSAT
170.71
p20-20.pddl_planlen=23
FAIL
175.32
dungeon_i10-m5-u10-v0.pddl_planlen=23
UNSAT
178.57
lut4_3_fAND
SAT
181.25
stmt28_68_81
SAT
204.88
Umbrella_tbm_25.tex.moduleQ3.2S.000075
UNSAT
207.4
ev-pr-4x4-13-3-0-0-1-s
FAIL
224.62
incrementer-enc02-uniform-depth-58
UNSAT
229.63
b20_C_3_2
FAIL
235.23
sortnetsort8.v.stepl.009
SAT
254.44
ev-pr-8x8-19-7-0-1-2-lg
FAIL
254.72
k_ph_n-16
SAT
256.88
pipesnotankage18_8
FAIL
258.62
toilet_c_10_01.17
UNSAT
261.94
ev-pr-4x4-15-3-0-0-1-s
FAIL
276.32
c3_Debug_s3_f2_e2_v2
FAIL
288.62
ev-pr-8x8-13-7-0-1-2-lg
FAIL
293.72
cube_c7_ser--opt-24_
SAT
298.95
ev-pr-4x4-17-3-0-0-1-s
FAIL
299.42
ev-pr-4x4-7-3-0-0-1-s
FAIL
305.22
b21_C_3_206
FAIL
318.52
connect_9x8_6_R
FAIL
323.23
connect_8x7_6_R
FAIL
328.12
ev-pr-4x4-11-3-0-0-1-lg
SAT
337.61
CHAIN23v.24
FAIL
340.72
dungeon_i10-m10-u10-v0.pddl_planlen=187
UNSAT
345.21
stmt17_86_98
SAT
382.04
cnt10
SAT
417.6
qshifter_8
FAIL
419.62
ev-pr-8x8-15-7-0-1-2-lg
FAIL
429.83
stmt17_70_90
SAT
448.64
driverlog03_7
SAT
452.17
qshifter_7
FAIL
476.52
C880.blif_0.10_0.20_0_1_out_exact
UNSAT
567.63
stmt17_63_82
SAT
568.69
ev-pr-6x6-9-5-0-1-2-lg
FAIL
576.52
ev-pr-6x6-17-5-0-1-2-lg
FAIL
582.44
ring_r6_ser--opt-17_
FAIL
583.02
k_lin_n-17
SAT
593.13
c2_Debug_s3_f1_e1_v2
FAIL
597.11
c1_Debug_s5_f1_e1_v2
FAIL
597.51
c4_Debug_s3_f2_e2_v2
FAIL
597.81
c5_BMC_p2_k128
FAIL
599.11
szymanski-14-s
FAIL
599.31
szymanski-16-s
FAIL
599.31
c5_BMC_p2_k64
FAIL
599.43
network_irda_miniport_nscirda_comm.c
FAIL
599.52
k14_2_3
FAIL
599.53
filesys_smbmrx_cvsndrcv.c
FAIL
599.53
s3330_d12_u
FAIL
599.53
input_pnpi8042_moudep.c
FAIL
599.53
query42_query06_1344n
FAIL
599.53
Adder2-16-s
FAIL
599.61
s1269_d15_u
FAIL
599.61
s3330_d9_s
FAIL
599.61
ev-pr-6x6-19-5-0-1-2-lg
FAIL
599.61
arbiter-10-comp-error01-qbf-hardness-depth-22
FAIL
599.61
szymanski-8-s
FAIL
599.61
ev-pr-6x6-11-5-0-1-2-lg
FAIL
599.71
uclid-pipe3a
FAIL
599.71
C6288.blif_0.10_0.20_0_1_out_exact
FAIL
599.71
adder-14-sat
FAIL
599.71
possibility4_0_1
FAIL
599.71
C880.blif_0.10_0.20_0_1_inp_exact
FAIL
599.71
Core1108_tbm_02.tex.moduleQ3.2S.000015
FAIL
599.71
test2_quant_squaring3
FAIL
599.71
mutex-32-s
FAIL
599.71
stmt19_64_99
FAIL
599.71
mutex-64-s
FAIL
599.71
audio_ddksynth_csynth2.cpp
FAIL
599.71
cache-coherence-2-fixpoint-6
FAIL
599.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-005
FAIL
599.71
possibility7_0_1
FAIL
599.71
sdlx-fixpoint-3
FAIL
599.71
sortnetsort9.AE.stepl.012
FAIL
599.71
possibility8_0_1
FAIL
599.71
C6288.blif_0.10_0.20_0_0_inp_exact
FAIL
599.71
adder-10-sat
FAIL
599.71
network_ndis_rtlnwifi_hw_hw_ccmp.c
FAIL
599.71
k_branch_p-16
FAIL
599.71
k12_4_2
FAIL
599.71
adder-12-unsat
FAIL
599.71
possibility12_0_1
FAIL
599.71
k_branch_n-8
FAIL
599.71
szymanski-6-s
FAIL
599.71
rankfunc13_unsigned_64
FAIL
599.71
gttt_2_2_001020_4x4_w
FAIL
599.71
dungeon_i15-m7-u4-v0.pddl_planlen=81
FAIL
599.71
s1269_d13_u
FAIL
599.71
gttt_2_1_00102030_4x4_torus_b
FAIL
599.71
assertion1_0_1
FAIL
599.71
s15850_PR_8_50
FAIL
599.71
rankfunc33_signed_32
FAIL
599.71
cnt16r
FAIL
599.71
possibility1_0_1
FAIL
599.71
s1269_d12_u
FAIL
599.71
query44_query26_1344n
FAIL
599.71
ev-pr-8x8-7-7-0-1-2-lg
FAIL
599.71
assertion8_0_1
FAIL
599.71
consistency_0_1
FAIL
599.71
stmt41_160_235
FAIL
599.71
k_branch_n-10
FAIL
599.71
k_branch_p-10
FAIL
599.71
p20-1.pddl_planlen=24
FAIL
599.71
assertion9_0_1
FAIL
599.71
possibility2_0_1
FAIL
599.71
rankfunc14_signed_64
FAIL
599.71
ken.flash^08.C-d4
FAIL
599.71
k_branch_p-11
FAIL
599.71
rankfunc17_unsigned_16
FAIL
599.81
assertion3_0_1
FAIL
599.81
f600-50
FAIL
599.81
possibility9_0_1
FAIL
599.81
C6288.blif_0.10_0.20_0_0_out_exact
FAIL
599.81
emptyroom_e4_ser--opt-44_
FAIL
599.81
k_ph_p-12
FAIL
599.81
k_ph_p-19
FAIL
599.81
mutex-4-s
FAIL
599.81
sortnetsort9.v.stepl.007
FAIL
599.81
Umbrella_tbm_05.tex.module.000039
FAIL
599.81
sortnetsort9.v.stepl.005
FAIL
599.81
C5315.blif_0.10_0.20_0_0_out_exact
FAIL
599.81
C6288.blif_0.10_1.00_0_0_out_exact
FAIL
599.81
ken.oop^2.C-d4
FAIL
599.81
k_ph_n-21
FAIL
599.81
C499.blif_0.10_0.20_0_1_out_exact
FAIL
599.81
szymanski-5-s
FAIL
599.81
test2_quant_squaring2
FAIL
599.81
assertion4_0_1
FAIL
599.81
arbiter-08-comp-error02-qbf-hardness-depth-9
FAIL
599.81
uclid-pipe2
FAIL
599.81
k_branch_n-12
FAIL
599.81
rankfunc5_unsigned_64
FAIL
599.81
ev-pr-4x4-13-3-0-0-1-lg
FAIL
599.81
CHAIN22v.23
FAIL
599.81
C880.blif_0.10_1.00_0_0_inp_exact
FAIL
599.81
cnt14
FAIL
599.82
CHAIN20v.21
FAIL
599.91
sortnetsort10.v.stepl.005
FAIL
599.91
small-swap2-fixpoint-4
FAIL
599.91
test3_quant_squaring2
FAIL
599.91
C499.blif_0.10_0.20_0_0_out_exact
FAIL
599.91
small-synabs-fixpoint-9
FAIL
599.91
k8_2_3
FAIL
599.91
small-swap1-fixpoint-3
FAIL
599.91
p20-5.pddl_planlen=32
FAIL
600
test3_quant_squaring4
FAIL
600.01
k5_2_3
FAIL
600.02
test1_quant_squaring3
FAIL
600.02
assertion10_0_1
FAIL
606.07
Contact
|
Organization
|
Links
|
Citing QBFLIB