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
CUED1919_NNL
QBFEVAL'17 - Prenex CNF Track
Instance
Result
Time
halfadder_match2.unsat
FAIL
0
C432.blif_0.10_0.20_0_0_out_exact
FAIL
0.01
mvs16y.unsat
FAIL
0.01
s00400_PR_9_90
FAIL
0.01
C432.blif_0.10_0.20_0_1_out_exact
FAIL
0.02
test4_quant_squaring2
FAIL
0.02
equalization32
SAT
0.03
halfadder_match2.sat
SAT
0.03
C880.blif_0.10_0.20_0_0_inp_exact
FAIL
0.03
C880.blif_0.10_0.20_0_1_inp_exact
FAIL
0.03
C880.blif_0.10_1.00_0_0_inp_exact
FAIL
0.03
C880.blif_0.10_0.20_0_0_out_exact
FAIL
0.04
C499.blif_0.10_0.20_0_1_out_exact
FAIL
0.04
lights3_021_1_022
FAIL
0.04
C880.blif_0.10_0.20_0_1_out_exact
FAIL
0.04
C499.blif_0.10_0.20_0_0_inp_exact
FAIL
0.04
C499.blif_0.10_0.20_0_0_out_exact
FAIL
0.04
C880.blif_0.10_1.00_0_0_out_exact
FAIL
0.04
test3_quant_squaring4
FAIL
0.04
test5_quant_squaring5
FAIL
0.05
test4_quant_squaring4
FAIL
0.06
Core1108_tbm_21.tex.module.000030
FAIL
0.07
add4_REDUCED
FAIL
0.08
Core1108_tbm_21.tex.module.000008
FAIL
0.09
add4_COMPLETE
FAIL
0.09
unit11_3_b
FAIL
0.1
test1_quant_squaring2
FAIL
0.1
driver_d9y.unsat
FAIL
0.12
add5_REDUCED
FAIL
0.13
uclid-pipe2
FAIL
0.14
add5_COMPLETE
FAIL
0.14
uclid-pipe3a
FAIL
0.14
cmu.dme1.B-f3
FAIL
0.17
add6_REDUCED
FAIL
0.17
tlc05-nonuniform-depth-6
FAIL
0.17
add6_COMPLETE
FAIL
0.18
add7_REDUCED
FAIL
0.23
test1_quant_squaring3
FAIL
0.24
sortnetsort8.v.stepl.007
FAIL
0.24
add7_COMPLETE
FAIL
0.25
sortnetsort9.v.stepl.005
FAIL
0.25
eijk.S713.S-f2
FAIL
0.27
gttt_1_1_001020_3x3_torus_b
FAIL
0.28
cmu.dme2.B-f3
FAIL
0.29
tlc04-nonuniform-depth-8
FAIL
0.29
Umbrella_tbm_05.tex.module.000039
FAIL
0.35
incrementer-enc03-nonuniform-depth-5
FAIL
0.39
sortnetsort10.v.stepl.005
FAIL
0.42
sortnetsort9.v.stepl.007
FAIL
0.42
eijk.bs3330.S-d3
FAIL
0.45
kmdf_pcidrv_sys_hw_physet.c
FAIL
0.54
C6288.blif_0.10_1.00_0_0_inp_exact
FAIL
0.55
C6288.blif_0.10_1.00_0_1_inp_exact
FAIL
0.55
cnt08e
FAIL
0.57
C6288.blif_0.10_0.20_0_1_inp_exact
FAIL
0.57
ltl2dba_C2-6_comp3_REAL.unsat
FAIL
0.58
C6288.blif_0.10_0.20_0_0_inp_exact
FAIL
0.58
Adder2-8-c
FAIL
0.59
s05378_PR_9_75
FAIL
0.6
C6288.blif_0.10_0.20_0_0_out_exact
FAIL
0.63
C6288.blif_0.10_0.20_0_1_out_exact
FAIL
0.63
C6288.blif_0.10_1.00_0_0_out_exact
FAIL
0.63
s09234_PR_9_5
FAIL
0.73
Adder2-8-s
FAIL
0.74
C5315.blif_0.10_0.20_0_1_inp_exact
FAIL
0.85
C5315.blif_0.10_0.20_0_0_inp_exact
FAIL
0.86
amba2f9n.unsat
FAIL
0.87
C5315.blif_0.10_1.00_0_0_out_exact
FAIL
0.92
adder-12-unsat
FAIL
1.01
C5315.blif_0.10_0.20_0_0_out_exact
FAIL
1.07
C5315.blif_0.10_0.20_0_1_out_exact
FAIL
1.08
tlc03-nonuniform-depth-19
FAIL
1.33
dungeon_i20-m100-u4-v0.pddl_planlen=6
FAIL
1.58
ii8d1-90
FAIL
1.75
Adder2-10-s
FAIL
1.84
b14_PR_1_50
FAIL
1.96
cmu.gigamax.B-d4
FAIL
2
k5_2_3
FAIL
2.19
query03_query25_1344
FAIL
2.24
f600-50
FAIL
2.33
ii8d1-00
FAIL
2.36
adder-10-sat
FAIL
2.51
ken.oop^2.C-d3
FAIL
2.53
s641_d6_s
FAIL
2.53
small-bug1-fixpoint-7
SAT
2.58
tlc04-nonuniform-depth-27
FAIL
2.62
k5_3_2
FAIL
2.63
b20_PR_7_20
FAIL
2.66
f600-00
FAIL
2.76
unit6_3_b
FAIL
2.85
biu.mv.xl_ao.bb-b003-p020-IPF02-c05.blif-biu.inv.prop.bb-bmc.conf04.01X-QBF.BB1-01X.BB2-01X.BB3-Zi.with-IOC.unfold-005
FAIL
3.08
ltl2dpa_C26_comp2_REAL.unsat
FAIL
3.3
arbiter-05-comp-error01-qbf-hardness-depth-8
FAIL
3.33
uclid-pipe3b
FAIL
3.35
incrementer-enc04-nonuniform-depth-17
FAIL
3.4
incrementer-enc06-nonuniform-depth-10
FAIL
3.42
eijk.S1196.S-f2
FAIL
3.48
s641_d7_u
FAIL
3.61
nusmv.tcas-t^1.B-d2
FAIL
3.65
test2_quant_squaring2
FAIL
4.1
k6_2_3
FAIL
4.37
ssa7552-158-00
FAIL
4.41
s713_d7_u
FAIL
4.44
ken.oop^2.C-d4
FAIL
4.95
driver_a9n.unsat
FAIL
5
adder-12-sat
FAIL
5.39
genbuf9b4n.unsat
FAIL
5.6
s1196_1_5
FAIL
5.68
filesys_smbmrx_midatlas.c
FAIL
5.96
stay24n.unsat
FAIL
6.18
network_ndis_rtlnwifi_hw_hw_ccmp.c
FAIL
6.2
texas.PI_main^08.E-f3
FAIL
6.39
s298_d17_s
FAIL
6.52
test2_quant3
FAIL
6.69
s1196_d5_u
FAIL
7.09
Adder2-14-s
FAIL
7.22
test2_quant_squaring3
FAIL
7.29
genbuf10b4n.unsat
FAIL
7.6
texas.PI_main^05.E-f3
FAIL
7.91
incrementer-enc08-nonuniform-depth-24
FAIL
8.29
s1269_d5_s
FAIL
8.37
b22_PR_8_20
FAIL
8.83
audio_ddksynth_csynth2.cpp
FAIL
9
nusmv.reactor^3.C-d4
FAIL
9.37
ken.flash^08.C-d4
FAIL
9.47
nusmv.tcas^2.B-f2
FAIL
9.75
adder-14-sat
FAIL
10.05
cf_5_5x6_r_
FAIL
10.46
nusmv.tcas^3.B-f2
FAIL
10.55
tlc02-nonuniform-depth-73
FAIL
10.7
eijk.bs1512.S-f4
FAIL
11.1
s15850_PR_0_50
FAIL
11.15
Adder2-16-c
FAIL
11.6
gttt_1_1_000111_4x4_torus_b
FAIL
11.76
cycle_sched_6_7_1.unsat
FAIL
11.99
gttt_1_1_00101121_4x4_torus_w
FAIL
12.4
gttt_1_1_000111_4x4_torus_w
FAIL
12.79
incrementer-enc07-uniform-depth-25
FAIL
13.02
k_branch_n-10
FAIL
13.27
cnt16
FAIL
13.31
k_branch_p-10
FAIL
13.66
cf_4_7x4_d_
FAIL
13.98
Adder2-16-s
FAIL
14.26
k7_2_2
FAIL
14.35
cnt16r
FAIL
14.57
dungeon_i30-m30-u5-v0.pddl_planlen=4
FAIL
15.16
incrementer-enc08-uniform-depth-33
FAIL
16.39
s713_d11_u
FAIL
16.52
b15_PR_4_2
FAIL
17.65
arbiter-08-comp-error02-qbf-hardness-depth-9
FAIL
18.09
s298_d25_u
FAIL
18.8
neclaftp4001
UNSAT
20.84
s1196_d7_u
FAIL
21.42
mult_bool_matrix_10_9_11.unsat
FAIL
21.84
s499_d19_s
FAIL
22.91
k_branch_p-11
FAIL
22.94
k_branch_n-11
FAIL
23.6
incrementer-enc05-nonuniform-depth-22
FAIL
24.14
amba4b9y.unsat
FAIL
26.18
arbiter-06-comp-error01-qbf-hardness-depth-11
FAIL
27.12
tlc01-nonuniform-depth-63
FAIL
27.4
emptyroom_e3_ser---19_
FAIL
27.76
tlc04-nonuniform-depth-64
FAIL
27.89
s38584_3_238
FAIL
28.56
cf_6_6x6_w_
FAIL
29.21
b17_PR_0_90
FAIL
29.54
incrementer-enc06-uniform-depth-24
FAIL
31.76
tlc03-nonuniform-depth-67
FAIL
32.03
tlc05-nonuniform-depth-73
FAIL
36.72
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-007
FAIL
38.88
add4_CHOOSE
FAIL
38.88
ev-pr-4x4-17-3-0-0-1-lg
FAIL
44.73
k_branch_n-12
FAIL
47.44
k_branch_p-12
FAIL
48.32
s820_d10_s
FAIL
50.27
tlc02-uniform-depth-151
FAIL
50.91
nusmv.tcas^4.B-f3
FAIL
58.95
dungeon_i10-m10-u10-v0.pddl_planlen=166
FAIL
61.59
s499_d25_u
FAIL
61.83
query10_query36_1344
FAIL
63.14
b22_C_2_12
FAIL
64.45
dungeon_i15-m7-u4-v0.pddl_planlen=81
FAIL
70.11
incrementer-enc02-uniform-depth-58
FAIL
71.22
eijk.bs4863.S-d4
FAIL
71.91
incrementer-enc02-uniform-depth-63
FAIL
85.89
s3330_d4_s
FAIL
86.28
s1269_d10_s
FAIL
90.65
incrementer-enc02-nonuniform-depth-58
FAIL
91.19
incrementer-enc02-nonuniform-depth-59
FAIL
94.18
dungeon_i30-m30-u5-v0.pddl_planlen=8
FAIL
97.08
query31_reachqu_1344n
SAT
97.86
incrementer-enc02-nonuniform-depth-60
FAIL
99.17
sortnetsort9.AE.stepl.012
UNSAT
108.53
b18_PR_4_2
FAIL
108.67
depots09_13
FAIL
117.83
AR-fixpoint-9
FAIL
118.47
AR-fixpoint-7
FAIL
119.64
pipesnotankage17_5
FAIL
120.72
load_3c_comp_comp7_REAL.unsat
FAIL
120.94
pipesnotankage19_7
FAIL
122.03
depots09_12
FAIL
123.73
pipesnotankage17_7
FAIL
123.91
freecell03_5
FAIL
124.35
depots09_11
FAIL
125.15
freecell02_6
FAIL
125.39
ken.flash^05.C-d3
FAIL
125.7
pipesnotankage19_9
FAIL
126.04
freecell02_4
FAIL
126.99
c1_Debug_s3_f2_e1_v2
FAIL
127.32
ev-pr-4x4-5-3-0-0-1-s
FAIL
128.13
dungeon_i30-m30-u5-v0.pddl_planlen=9
FAIL
128.25
k8_2_3
FAIL
132.27
depots13_9
FAIL
132.7
pipesnotankage17_6
FAIL
144.03
k8_3_2
FAIL
144.43
biu.mv.xl_ao.bb-b003-p020-IPF02-c05.blif-biu.inv.prop.bb-bmc.with-IOC.unfold-007
FAIL
144.55
connect_7x6_4_R
FAIL
148.58
c3_Debug_s3_f2_e2_v3
FAIL
156.08
k7_4_4
FAIL
157.2
nusmv.tcas^6.B-f4
FAIL
161.7
c3_Debug_s3_f2_e2_v2
FAIL
169.72
k_branch_p-14
FAIL
171.31
ken.flash^11.C-f3
FAIL
174.5
biu.mv.xl_ao.bb-b003-p020-IPF02-c05.blif-biu.inv.prop.bb-bmc.conf05.01X-QBF.BB1-Zi.BB2-01X.BB3-Zi.with-IOC.unfold-007
FAIL
176.12
add7_CHOOSE
FAIL
186.07
c1_Debug_s3_f1_e1_v1
FAIL
189.21
c1_Debug_s3_f2_e1_v1
FAIL
194.8
s820_d15_u
FAIL
200.67
eijk.bs3384.S-f4
FAIL
207.96
ken.flash^09.C-d4
FAIL
208.26
biu.mv.xl_ao.bb-b003-p020-IPF01-c05.blif-biu.inv.prop.bb-bmc.conf05.01X-QBF.BB1-Zi.BB2-01X.BB3-Zi.with-IOC.unfold-007
FAIL
212.35
gttt_2_1_001020_4x4_torus_w
FAIL
224.71
s510_d36_s
FAIL
226.42
k_ph_p-11
FAIL
245.69
pipesnotankage04_5
FAIL
247.71
gttt_2_1_00102030_4x4_torus_b
FAIL
259.9
input_mouser_detect.c
FAIL
293.25
filesys_smbmrx_cvsndrcv.c
FAIL
293.4
s510_d41_s
FAIL
298.57
input_mouser_cseries.c
FAIL
298.61
biu.mv.xl_ao.bb-b003-p020-IPF01-c05.blif-biu.inv.prop.bb-bmc.conf01.01X-QBF.BB1-Zi.BB2-01X.BB3-01X.with-IOC.unfold-010
FAIL
303.39
biu.mv.xl_ao.bb-b003-p020-IPF03-c03.blif-biu.inv.prop.bb-bmc.conf02.01X-QBF.BB1-01X.BB2-Zi.BB3-01X.with-IOC.unfold-009
FAIL
308.72
cf_7_8x7_r_
FAIL
313.16
query21_query58_1344n
UNSAT
318.11
kernel_agplib_intrface.c
FAIL
323.95
network_trans_sys_notify.c
FAIL
330.48
hid_hclient_ecdisp.c
FAIL
331.18
network_ndis_coisdn_TpiParam.c
FAIL
332.33
input_pnpi8042_moudep.c
FAIL
332.85
network_irda_miniport_nscirda_settings.c
FAIL
335.45
filesys_fastfat_easup.c
FAIL
336.32
k8_3_4
FAIL
338.83
dungeon_i15-m7-u4-v0.pddl_planlen=168
FAIL
345.58
arbiter-06-comp-error01-qbf-hardness-depth-15
FAIL
345.69
load_full_4_comp3_REAL.unsat
FAIL
348.63
c4_Debug_s3_f1_e1_v2
FAIL
367.29
gttt_2_1_00011020_4x4_b
FAIL
385.78
biu.mv.xl_ao.bb-b003-p020-MIF04-c05.blif-biu.inv.prop.bb-bmc.with-IOC.unfold-008
FAIL
396.69
connect_8x7_6_R
FAIL
402.66
network_irda_miniport_nscirda_comm.c
FAIL
406.67
counter_re_32
FAIL
418.22
c2_Debug_s3_f1_e1_v2
FAIL
430.43
ev-pr-4x4-7-3-0-0-1-s
FAIL
437.36
fpu-10Xh-correct02-nonuniform-depth-2
FAIL
439.3
cf_8_8x8_d_
FAIL
457.63
add6_CHOOSE
FAIL
466.86
c4_Debug_s3_f1_e2_v3
FAIL
467.25
biu.mv.xl_ao.bb-b003-p020-IPF01-c05.blif-biu.inv.prop.bb-bmc.conf05.01X-QBF.BB1-Zi.BB2-01X.BB3-Zi.with-IOC.unfold-008
FAIL
471.11
c4_Debug_s3_f1_e2_v2
FAIL
471.16
k_branch_p-16
FAIL
480.77
c2_Debug_s3_f2_e1_v3
FAIL
483.07
k8_4_3
FAIL
484.32
mult_bool_matrix_17_17_17.unsat
FAIL
494.53
freecell03_7
FAIL
495.44
pipesnotankage16_10
FAIL
496.8
pipesnotankage14_10
FAIL
498.37
connect_8x7_5_R
FAIL
502.4
pipesnotankage13_5
FAIL
512.55
ev-pr-6x6-11-5-0-1-2-lg
FAIL
523.95
pipesnotankage18_8
FAIL
526.02
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-010
FAIL
527.79
AR-fixpoint-5
FAIL
528.78
c4_Debug_s3_f2_e2_v3
FAIL
536.25
depots16_5
FAIL
537.41
freecell03_6
FAIL
546.5
fpu-10Xh-correct04-uniform-depth-3
FAIL
554.66
fpu-10Xh-correct03-uniform-depth-3
FAIL
554.78
mult_bool_matrix_17_17_17.sat
FAIL
560.86
beemldelec4b1_c0to127.unsat
FAIL
562.83
connect_8x7_4_R
FAIL
579.36
c4_Debug_s3_f2_e2_v2
FAIL
582.47
cf_3_9x6_r_
FAIL
592.47
cf_2_9x6_r_
FAIL
598.73
cf_7_8x8_r_
FAIL
604.42
pipesnotankage11_8
FAIL
635.32
k_branch_n-17
FAIL
675.11
pipesnotankage15_10
FAIL
676.37
pipesnotankage18_7
FAIL
692.73
biu.mv.xl_ao.bb-b003-p020-MIF02-c01.blif-biu.inv.prop.bb-bmc.with-IOC.unfold-009
FAIL
736.01
ev-pr-6x6-13-5-0-1-2-lg
FAIL
759.18
cf_6_9x7_r_
FAIL
765.04
add5_CHOOSE
FAIL
779.5
s3330_d10_u
FAIL
788.67
fpu-01Xh-error02-nonuniform-depth-3
FAIL
793.72
ev-pr-4x4-9-3-0-0-1-s
FAIL
809.74
arbiter-09-comp-error01-qbf-hardness-depth-15
FAIL
847.03
oski3ub5i_c0to255.unsat
FAIL
879.72
biu.mv.xl_ao.bb-b003-p020-IPF03-c03.blif-biu.inv.prop.bb-bmc.with-IOC.unfold-009
FAIL
885.41
b20_C_3_2
FAIL
885.75
dungeon_i25-m12-u5-v0.pddl_planlen=143
FAIL
900
mvs16y.sat
FAIL
900
ev-pr-8x8-13-7-0-1-2-lg
FAIL
900
ev-pr-4x4-17-3-0-0-1-s
FAIL
900
ev-pr-6x6-19-5-0-1-2-lg
FAIL
900
stay24n.sat
FAIL
900
driverlog13_6
FAIL
900
dungeon_i25-m12-u5-v0.pddl_planlen=59
FAIL
900
dungeon_i25-m12-u5-v0.pddl_planlen=200
FAIL
900
dungeon_i25-m12-u5-v0.pddl_planlen=199
FAIL
900
dungeon_i25-m12-u5-v0.pddl_planlen=198
FAIL
900
dungeon_i25-m12-u5-v0.pddl_planlen=197
FAIL
900
dungeon_i25-m12-u5-v0.pddl_planlen=128
FAIL
900
ev-pr-8x8-17-7-0-1-2-lg
FAIL
900
dungeon_i25-m12-u3-v0.pddl_planlen=146
FAIL
900
dungeon_i25-m12-u5-v0.pddl_planlen=81
FAIL
900
dungeon_i25-m12-u5-v0.pddl_planlen=86
FAIL
900
dungeon_i25-m12-u5-v0.pddl_planlen=92
FAIL
900
driverlog12_7
FAIL
900
dungeon_i25-m12-u5-v0.pddl_planlen=98
FAIL
900
ev-pr-6x6-17-5-0-1-2-s
FAIL
900
ev-pr-6x6-13-5-0-1-2-s
FAIL
900
ev-pr-6x6-11-5-0-1-2-s
FAIL
900
ev-pr-4x4-15-3-0-0-1-s
FAIL
900
depots08_6
FAIL
900
depots07_8
FAIL
900
dungeon_i25-m12-u3-v0.pddl_planlen=125
FAIL
900
kenflashp12
FAIL
900
ActivityService2
FAIL
900
ev-pr-4x4-11-3-0-0-1-s
FAIL
900
counter_64
FAIL
900
ev-pr-6x6-5-5-0-1-2-s
FAIL
900
LoginService2
FAIL
900
ev-pr-6x6-19-5-0-1-2-s
FAIL
900
k_branch_n-21
FAIL
900
szymanski-24-s
FAIL
900
ev-pr-8x8-15-7-0-1-2-lg
FAIL
900
ProcessBean
FAIL
900
connect_9x8_6_R
FAIL
900
pdtpmsmiim
FAIL
900
szymanski-20-s
FAIL
900
k_branch_p-21
FAIL
900
eijkbs4863
FAIL
900
bobsmfpu
FAIL
900
intermediate128
FAIL
900
floor256
FAIL
900
decomposition256
FAIL
900
ceiling128
FAIL
900
unit9_2_b
FAIL
900
unit8_2_b
FAIL
900
k_ph_p-20
FAIL
900
unit12_2_b
FAIL
900
k_ph_p-12
FAIL
900
connect_9x8_3_R
FAIL
900
ProjectService3
FAIL
900
UserServiceImpl
FAIL
900
genbuf9b4n.sat
FAIL
900
beemldelec4b1_c0to127.sat
FAIL
900
oski3ub5i_c0to255.sat
FAIL
900
load_3c_comp_comp7_REAL.sat
FAIL
900
load_full_4_comp3_REAL.sat
FAIL
900
arbiter-09-comp-error01-qbf-hardness-depth-21
FAIL
900
ev-pr-8x8-11-7-0-1-2-lg
FAIL
900
ltl2dba_C2-6_comp3_REAL.sat
FAIL
900
ev-pr-6x6-15-5-0-1-2-s
FAIL
900
ltl2dpa_C26_comp2_REAL.sat
FAIL
900
mult_bool_matrix_10_9_11.sat
FAIL
900
ev-pr-8x8-19-7-0-1-2-lg
FAIL
900
genbuf10b4n.sat
FAIL
900
driver_d9y.sat
FAIL
900
amba2f9n.sat
FAIL
900
ev-pr-6x6-15-5-0-1-2-lg
FAIL
900
amba4b9y.sat
FAIL
900
k_branch_n-20
FAIL
900
cycle_sched_4_7_1.sat
FAIL
900
cycle_sched_4_7_1.unsat
FAIL
900
cycle_sched_6_7_1.sat
FAIL
900
driver_a9n.sat
FAIL
900
ev-pr-4x4-13-3-0-0-1-s
FAIL
900
arbiter-10-comp-error01-qbf-hardness-depth-24
FAIL
900
arbiter-10-comp-error01-qbf-hardness-depth-23
FAIL
900
ev-pr-6x6-9-5-0-1-2-s
FAIL
900
cache-coherence-3-fixpoint-3
FAIL
900
k12_3_2
FAIL
900
k12_4_2
FAIL
900
stmt32_329_378
FAIL
900
stmt19_83_412
FAIL
900
stmt21_181_369
FAIL
900
stmt21_310_360
FAIL
900
stmt41_160_235
FAIL
900
stmt19_313_412
FAIL
900
stmt21_319_418
FAIL
900
stmt39_285_335
FAIL
900
stmt29_226_376
FAIL
900
stmt17_86_98
FAIL
900
stmt17_63_82
FAIL
900
stmt17_70_90
FAIL
900
k10_4_3
FAIL
900
biu.mv.xl_ao.bb-b003-p020-IPF02-c05.blif-biu.inv.prop.bb-bmc.with-IOC.unfold-010
FAIL
900
k14_4_4
FAIL
900
small-seq-fixpoint-3
FAIL
900
small-pipeline-fixpoint-6
FAIL
900
small-seq-fixpoint-7
FAIL
900
small-equiv-fixpoint-6
FAIL
900
small-seq-fixpoint-8
FAIL
900
itc-b13-fixpoint-5
FAIL
900
usb-phy-fixpoint-3
FAIL
900
small-seq-fixpoint-9
FAIL
900
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-010
FAIL
900
rankfunc35_signed_32
FAIL
900
rankfunc60_signed_32
FAIL
900
biu.mv.xl_ao.bb-b003-p020-IPF02-c05.blif-biu.inv.prop.bb-bmc.conf06.01X-QBF.BB1-01X.BB2-Zi.BB3-Zi.with-IOC.unfold-009
FAIL
900
biu.mv.xl_ao.bb-b003-p020-IPF02-c05.blif-biu.inv.prop.bb-bmc.conf07.01X-QBF.BB1-Zi.BB2-Zi.BB3-Zi.with-IOC.unfold-008
FAIL
900
k14_2_3
FAIL
900
stmt23_66_96
FAIL
900
stmt17_82_98
FAIL
900
c2_BMC_p1_k2048
FAIL
900
c1_BMC_p2_k2048
FAIL
900
c1_BMC_p2_k1024
FAIL
900
c1_BMC_p1_k2048
FAIL
900
ring_r7_ser--opt-20_
FAIL
900
ring_r7_ser---19_
FAIL
900
ring_r6_ser--opt-17_
FAIL
900
emptyroom_e4_ser--opt-44_
FAIL
900
emptyroom_e4_par---21_
FAIL
900
biu.mv.xl_ao.bb-b003-p020-MIF02-c01.blif-biu.inv.prop.bb-bmc.conf07.01X-QBF.BB1-Zi.BB2-Zi.BB3-Zi.with-IOC.unfold-009
FAIL
900
cube_c7_ser---23_
FAIL
900
cube_c11_ser--opt-42_
FAIL
900
blocks_enc_2_b4_ser--opt-26_
FAIL
900
c4_Debug_s5_f2_e2_v1
FAIL
900
c3_BMC_p1_k256
FAIL
900
c5_BMC_p1_k128
FAIL
900
c5_BMC_p1_k32
FAIL
900
stmt28_68_81
FAIL
900
stmt23_72_76
FAIL
900
stmt17_70_98
FAIL
900
stmt17_62_98
FAIL
900
stmt19_64_99
FAIL
900
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-008
FAIL
900
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-009
FAIL
900
biu.mv.xl_ao.bb-b003-p020-MIF02-c01.blif-biu.inv.prop.bb-bmc.conf06.01X-QBF.BB1-01X.BB2-Zi.BB3-Zi.with-IOC.unfold-010
FAIL
900
c5_BMC_p2_k64
FAIL
900
c5_BMC_p2_k512
FAIL
900
c5_BMC_p2_k256
FAIL
900
c5_BMC_p2_k128
FAIL
900
c5_BMC_p2_k1024
FAIL
900
c5_BMC_p1_k64
FAIL
900
c1_Debug_s5_f1_e1_v2
FAIL
900
k_ph_p-21
FAIL
900
arbiter-07-comp-error01-qbf-hardness-depth-20
FAIL
900
k_ph_p-19
FAIL
900
k_ph_p-13
FAIL
900
k_ph_p-14
FAIL
900
k_ph_p-15
FAIL
900
cf_4_9x9_r_
FAIL
900
cf_5_9x9_d_
FAIL
900
fpu-10Xh-correct04-uniform-depth-24
FAIL
900
fpu-10Xh-correct04-nonuniform-depth-13
FAIL
900
fpu-10Xh-correct03-uniform-depth-14
FAIL
900
fpu-10Xh-correct03-uniform-depth-10
FAIL
900
fpu-10Xh-correct03-nonuniform-depth-26
FAIL
900
fpu-10Xh-correct03-nonuniform-depth-22
FAIL
900
fpu-10Xh-correct02-uniform-depth-13
FAIL
900
k_ph_p-18
FAIL
900
arbiter-10-comp-error01-qbf-hardness-depth-22
FAIL
900
k_ph_p-17
FAIL
900
ev-pr-6x6-7-5-0-1-2-s
FAIL
900
query44_query26_1344n
FAIL
900
query42_query06_1344n
FAIL
900
k_branch_p-18
FAIL
900
dungeon_i25-m12-u5-v0.pddl_planlen=65
FAIL
900
dungeon_i25-m12-u5-v0.pddl_planlen=170
FAIL
900
dungeon_i25-m12-u3-v0.pddl_planlen=72
FAIL
900
dungeon_i25-m12-u3-v0.pddl_planlen=190
FAIL
900
dungeon_i25-m12-u3-v0.pddl_planlen=165
FAIL
900
dungeon_i25-m12-u3-v0.pddl_planlen=130
FAIL
900
driverlog10_6
FAIL
900
depots03_9
FAIL
900
k_branch_p-19
FAIL
900
b21_C_3_206
FAIL
900
fpu-10Xh-correct02-nonuniform-depth-8
FAIL
900
fpu-10Xe-correct02-uniform-depth-20
FAIL
900
audio_ac97_wavepcistream.cpp
FAIL
900
small-seq-fixpoint-5
FAIL
900
small-synabs-fixpoint-3
FAIL
900
sortnetsort9.AE.stepl.009
FAIL
900
small-dyn-partition-fixpoint-8
FAIL
900
small-pipeline-fixpoint-7
FAIL
900
small-equiv-fixpoint-10
FAIL
900
AR-fixpoint-1
FAIL
900
cache-coherence-2-fixpoint-4
FAIL
900
pi-bus-fixpoint-1
FAIL
900
sdlx-fixpoint-3
FAIL
900
small-equiv-fixpoint-9
FAIL
900
AR-fixpoint-3
FAIL
900
pi-bus-fixpoint-3
FAIL
900
hid_firefly_app_firefly.cpp
FAIL
900
AVStream_hwsim.cpp
FAIL
900
filesys_cdfs_namesup.c
FAIL
900
fpu-10Xe-correct02-nonuniform-depth-6
FAIL
900
fpu-10Xe-correct02-nonuniform-depth-16
FAIL
900
fpu-01Xh-error02-uniform-depth-8
FAIL
900
fpu-01Xh-error02-uniform-depth-18
FAIL
900
fpu-01Xh-error02-nonuniform-depth-7
FAIL
900
fpu-01Xh-error02-nonuniform-depth-22
FAIL
900
fpu-01Xh-error02-nonuniform-depth-13
FAIL
900
cube_c11_par---13_
FAIL
900
cf_8_9x8_d_
FAIL
900
ev-pr-6x6-17-5-0-1-2-lg
FAIL
900
kmdf_AMCC5933_sys_S5933DK1.c
FAIL
900
network_ndis_rtlnwifi_extsta_st_misc.c
FAIL
900
network_usbnwifi_mp_util.c
FAIL
900
filesys_cdfs_allocsup.c
FAIL
900
cache-coherence-2-fixpoint-6
FAIL
900
Contact
|
Organization
|
Links
|
Citing QBFLIB