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
AIGSolve
QBFEVAL'17 - Prenex CNF Track
Instance
Result
Time
halfadder_match2.unsat
UNSAT
0
s00400_PR_9_90
UNSAT
0
halfadder_match2.sat
SAT
0.01
mvs16y.unsat
UNSAT
0.01
small-bug1-fixpoint-7
SAT
0.02
tlc05-nonuniform-depth-6
UNSAT
0.02
tlc04-nonuniform-depth-8
UNSAT
0.04
cf_4_7x4_d_
UNSAT
0.05
mvs16y.sat
SAT
0.05
test4_quant_squaring2
UNSAT
0.06
cf_6_6x6_w_
UNSAT
0.06
incrementer-enc03-nonuniform-depth-5
UNSAT
0.08
lights3_021_1_022
SAT
0.08
ltl2dba_C2-6_comp3_REAL.unsat
UNSAT
0.12
driver_d9y.unsat
UNSAT
0.13
small-dyn-partition-fixpoint-8
UNSAT
0.13
cf_8_8x8_d_
UNSAT
0.15
C432.blif_0.10_0.20_0_1_out_exact
UNSAT
0.21
C432.blif_0.10_0.20_0_0_out_exact
UNSAT
0.21
cf_8_9x8_d_
UNSAT
0.21
fpu-10Xh-correct02-nonuniform-depth-2
UNSAT
0.22
kenflashp12
SAT
0.23
small-synabs-fixpoint-3
UNSAT
0.23
fpu-10Xh-correct03-uniform-depth-3
UNSAT
0.33
fpu-10Xh-correct04-uniform-depth-3
UNSAT
0.34
fpu-01Xh-error02-nonuniform-depth-3
UNSAT
0.34
pipesnotankage04_5
UNSAT
0.36
equalization32
SAT
0.38
tlc03-nonuniform-depth-19
UNSAT
0.39
dungeon_i30-m30-u5-v0.pddl_planlen=4
UNSAT
0.45
dungeon_i20-m100-u4-v0.pddl_planlen=6
SAT
0.56
unit9_2_b
SAT
0.56
cf_5_9x9_d_
UNSAT
0.59
ltl2dpa_C26_comp2_REAL.unsat
UNSAT
0.65
rankfunc60_signed_32
SAT
0.67
fpu-10Xe-correct02-nonuniform-depth-6
UNSAT
0.85
tlc01-nonuniform-depth-63
UNSAT
0.85
tlc04-nonuniform-depth-27
UNSAT
0.93
stay24n.unsat
UNSAT
0.96
incrementer-enc06-nonuniform-depth-10
UNSAT
1.09
fpu-01Xh-error02-nonuniform-depth-7
UNSAT
1.16
fpu-01Xh-error02-uniform-depth-8
UNSAT
1.3
test3_quant_squaring4
UNSAT
1.31
fpu-10Xh-correct02-nonuniform-depth-8
UNSAT
1.31
test1_quant_squaring2
SAT
1.34
C5315.blif_0.10_1.00_0_0_out_exact
UNSAT
1.51
ceiling128
SAT
1.53
C880.blif_0.10_1.00_0_0_out_exact
UNSAT
1.57
fpu-10Xh-correct03-uniform-depth-10
UNSAT
1.66
eijk.S1196.S-f2
UNSAT
1.8
dungeon_i30-m30-u5-v0.pddl_planlen=8
UNSAT
2.09
C880.blif_0.10_0.20_0_1_out_exact
UNSAT
2.09
C880.blif_0.10_0.20_0_0_out_exact
UNSAT
2.11
fpu-01Xh-error02-nonuniform-depth-13
UNSAT
2.13
fpu-10Xh-correct02-uniform-depth-13
UNSAT
2.14
fpu-10Xh-correct04-nonuniform-depth-13
UNSAT
2.14
nusmv.reactor^3.C-d4
SAT
2.23
fpu-10Xh-correct03-uniform-depth-14
UNSAT
2.28
driverlog10_6
UNSAT
2.31
unit8_2_b
SAT
2.49
rankfunc35_signed_32
SAT
2.7
dungeon_i30-m30-u5-v0.pddl_planlen=9
UNSAT
2.76
fpu-01Xh-error02-uniform-depth-18
UNSAT
2.82
driver_a9n.unsat
UNSAT
2.93
incrementer-enc04-nonuniform-depth-17
SAT
3.01
driver_d9y.sat
SAT
3.09
fpu-01Xh-error02-nonuniform-depth-22
UNSAT
3.45
fpu-10Xh-correct03-nonuniform-depth-22
UNSAT
3.47
test5_quant_squaring5
SAT
3.72
fpu-10Xh-correct04-uniform-depth-24
UNSAT
3.78
test4_quant_squaring4
UNSAT
3.99
fpu-10Xh-correct03-nonuniform-depth-26
UNSAT
4.17
C499.blif_0.10_0.20_0_1_out_exact
UNSAT
4.22
cnt08e
SAT
4.23
unit11_3_b
UNSAT
4.5
fpu-10Xe-correct02-nonuniform-depth-16
UNSAT
4.54
stmt21_181_369
UNSAT
4.9
s09234_PR_9_5
SAT
5.13
b15_PR_4_2
SAT
5.21
tlc02-nonuniform-depth-73
UNSAT
5.53
fpu-10Xe-correct02-uniform-depth-20
UNSAT
5.62
stmt19_83_412
UNSAT
5.8
mult_bool_matrix_10_9_11.sat
SAT
5.86
incrementer-enc08-nonuniform-depth-24
UNSAT
5.92
s05378_PR_9_75
UNSAT
6.1
test1_quant_squaring3
SAT
6.31
pdtpmsmiim
SAT
6.49
Adder2-8-s
SAT
6.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-007
UNSAT
6.73
tlc04-nonuniform-depth-64
UNSAT
6.91
stmt41_160_235
UNSAT
7.2
floor256
SAT
8.26
load_3c_comp_comp7_REAL.unsat
UNSAT
8.3
tlc05-nonuniform-depth-73
UNSAT
8.43
Adder2-8-c
UNSAT
8.44
cycle_sched_6_7_1.unsat
UNSAT
8.5
depots03_9
UNSAT
8.56
tlc03-nonuniform-depth-67
UNSAT
8.64
depots07_8
UNSAT
8.68
c1_BMC_p2_k1024
UNSAT
8.73
decomposition256
SAT
8.88
unit12_2_b
SAT
9.56
C499.blif_0.10_0.20_0_0_out_exact
UNSAT
9.67
adder-10-sat
SAT
9.99
c5_BMC_p1_k32
SAT
10.07
ken.oop^2.C-d3
UNSAT
10.24
incrementer-enc07-uniform-depth-25
UNSAT
10.6
dungeon_i10-m10-u10-v0.pddl_planlen=166
UNSAT
11.14
stay24n.sat
SAT
11.39
amba2f9n.unsat
UNSAT
11.5
texas.PI_main^08.E-f3
SAT
11.59
mult_bool_matrix_17_17_17.sat
SAT
11.67
texas.PI_main^05.E-f3
SAT
11.89
incrementer-enc08-uniform-depth-33
SAT
12
pipesnotankage11_8
UNSAT
12.34
stmt17_63_82
SAT
12.51
szymanski-24-s
UNSAT
12.59
stmt29_226_376
UNSAT
13.06
stmt23_72_76
SAT
13.28
beemldelec4b1_c0to127.unsat
UNSAT
13.63
stmt28_68_81
SAT
13.92
driverlog12_7
UNSAT
14.14
stmt23_66_96
SAT
15.4
incrementer-enc06-uniform-depth-24
UNSAT
15.79
incrementer-enc05-nonuniform-depth-22
UNSAT
16.02
stmt19_64_99
SAT
16.63
ken.flash^09.C-d4
UNSAT
17.41
dungeon_i25-m12-u5-v0.pddl_planlen=81
UNSAT
17.68
adder-12-sat
SAT
17.88
dungeon_i25-m12-u5-v0.pddl_planlen=86
UNSAT
18.16
mult_bool_matrix_10_9_11.unsat
UNSAT
18.3
oski3ub5i_c0to255.unsat
UNSAT
18.34
driverlog13_6
UNSAT
18.44
stmt17_70_98
SAT
18.48
dungeon_i25-m12-u5-v0.pddl_planlen=92
UNSAT
18.71
stmt21_319_418
SAT
18.74
c1_BMC_p2_k2048
UNSAT
19.23
c3_BMC_p1_k256
SAT
19.3
dungeon_i25-m12-u5-v0.pddl_planlen=98
UNSAT
19.33
C499.blif_0.10_0.20_0_0_inp_exact
UNSAT
19.38
load_full_4_comp3_REAL.unsat
UNSAT
19.76
pipesnotankage13_5
UNSAT
19.85
amba2f9n.sat
SAT
20.06
ken.flash^05.C-d3
UNSAT
20.43
mult_bool_matrix_17_17_17.unsat
UNSAT
20.5
uclid-pipe2
SAT
20.73
cycle_sched_4_7_1.unsat
UNSAT
21.16
dungeon_i25-m12-u3-v0.pddl_planlen=130
UNSAT
22.73
stmt17_82_98
SAT
22.74
ken.flash^08.C-d4
UNSAT
23.04
dungeon_i25-m12-u3-v0.pddl_planlen=125
UNSAT
23.13
dungeon_i15-m7-u4-v0.pddl_planlen=81
UNSAT
23.16
uclid-pipe3a
SAT
23.43
dungeon_i25-m12-u3-v0.pddl_planlen=146
UNSAT
24.73
tlc02-uniform-depth-151
UNSAT
25
stmt17_86_98
SAT
25.64
adder-14-sat
SAT
26.04
dungeon_i25-m12-u5-v0.pddl_planlen=128
UNSAT
26.63
stmt17_70_90
SAT
27.29
dungeon_i25-m12-u3-v0.pddl_planlen=165
UNSAT
27.58
emptyroom_e3_ser---19_
UNSAT
27.82
driver_a9n.sat
SAT
28.03
dungeon_i25-m12-u5-v0.pddl_planlen=143
UNSAT
28.1
stmt17_62_98
SAT
28.28
eijk.S713.S-f2
UNSAT
28.55
freecell02_4
UNSAT
29.14
adder-12-unsat
UNSAT
29.69
szymanski-20-s
UNSAT
29.79
dungeon_i25-m12-u3-v0.pddl_planlen=190
UNSAT
30.58
dungeon_i25-m12-u5-v0.pddl_planlen=59
UNSAT
31.01
ev-pr-4x4-5-3-0-0-1-s
SAT
31.26
stmt21_310_360
UNSAT
31.63
dungeon_i25-m12-u5-v0.pddl_planlen=170
UNSAT
32.49
dungeon_i15-m7-u4-v0.pddl_planlen=168
UNSAT
32.65
dungeon_i25-m12-u5-v0.pddl_planlen=65
UNSAT
33.76
dungeon_i25-m12-u3-v0.pddl_planlen=72
UNSAT
33.92
depots08_6
UNSAT
35.55
freecell02_6
UNSAT
36.1
dungeon_i25-m12-u5-v0.pddl_planlen=197
UNSAT
36.38
dungeon_i25-m12-u5-v0.pddl_planlen=199
UNSAT
36.76
dungeon_i25-m12-u5-v0.pddl_planlen=198
UNSAT
36.78
cnt16
SAT
36.96
sdlx-fixpoint-3
UNSAT
37.68
dungeon_i25-m12-u5-v0.pddl_planlen=200
UNSAT
38.66
pipesnotankage14_10
UNSAT
40.49
Adder2-10-s
SAT
40.95
eijk.bs3330.S-d3
SAT
41.1
itc-b13-fixpoint-5
SAT
41.66
k5_2_3
SAT
41.78
ltl2dba_C2-6_comp3_REAL.sat
SAT
42.86
cache-coherence-3-fixpoint-3
UNSAT
46.03
intermediate128
SAT
47.33
small-seq-fixpoint-3
UNSAT
51.77
cnt16r
SAT
53.87
k_branch_n-10
SAT
60.54
freecell03_6
UNSAT
62.01
freecell03_5
UNSAT
63.05
k_branch_p-10
UNSAT
66.08
cache-coherence-2-fixpoint-6
UNSAT
70.2
freecell03_7
SAT
75.32
genbuf9b4n.unsat
UNSAT
89.77
depots13_9
SAT
91.4
Adder2-14-s
SAT
97.64
pipesnotankage16_10
UNSAT
98.43
pipesnotankage15_10
UNSAT
99.76
k_branch_p-11
UNSAT
101.37
k_branch_p-12
UNSAT
108.95
neclaftp4001
UNSAT
110.17
cache-coherence-2-fixpoint-4
UNSAT
110.93
k_branch_n-11
SAT
117.57
ken.flash^11.C-f3
UNSAT
120.08
depots16_5
UNSAT
124.98
ken.oop^2.C-d4
UNSAT
127.34
k_branch_n-12
SAT
129.31
beemldelec4b1_c0to127.sat
SAT
137.18
small-seq-fixpoint-5
UNSAT
145.65
Adder2-16-s
SAT
157.17
AR-fixpoint-3
FAIL
167.18
gttt_1_1_001020_3x3_torus_b
UNSAT
203.41
AR-fixpoint-1
FAIL
209.91
k5_3_2
SAT
216.02
cmu.gigamax.B-d4
SAT
222.2
AR-fixpoint-5
FAIL
239.25
k_ph_p-11
UNSAT
245.6
b17_PR_0_90
UNSAT
250.28
k_branch_p-14
UNSAT
265
pipesnotankage19_7
UNSAT
283.43
stmt32_329_378
UNSAT
301.68
small-seq-fixpoint-7
UNSAT
311.43
s15850_PR_0_50
SAT
318.03
pi-bus-fixpoint-1
UNSAT
318.29
c4_Debug_s3_f2_e2_v3
FAIL
319.1
c4_Debug_s3_f1_e2_v3
FAIL
337.97
pipesnotankage18_7
UNSAT
356.22
cmu.dme2.B-f3
SAT
361.27
genbuf9b4n.sat
SAT
362.6
pipesnotankage18_8
UNSAT
364.81
s641_d6_s
SAT
370.99
AR-fixpoint-7
FAIL
384.5
c4_Debug_s3_f1_e2_v2
FAIL
419.1
c4_Debug_s3_f1_e1_v2
FAIL
420.82
c4_Debug_s3_f2_e2_v2
FAIL
427.62
small-seq-fixpoint-8
UNSAT
434.82
genbuf10b4n.unsat
UNSAT
440.67
stmt19_313_412
UNSAT
513.38
c2_Debug_s3_f1_e1_v2
FAIL
535.07
s298_d17_s
SAT
548.41
s641_d7_u
UNSAT
569.74
pipesnotankage19_9
UNSAT
569.75
AR-fixpoint-9
FAIL
577.91
incrementer-enc02-uniform-depth-58
FAIL
579.09
incrementer-enc02-uniform-depth-63
FAIL
611.66
small-seq-fixpoint-9
UNSAT
626.1
input_mouser_detect.c
FAIL
650.28
c1_Debug_s5_f1_e1_v2
FAIL
656.13
network_irda_miniport_nscirda_settings.c
FAIL
690.24
c2_Debug_s3_f2_e1_v3
FAIL
696.04
s713_d7_u
UNSAT
704.14
input_pnpi8042_moudep.c
FAIL
704.38
c2_BMC_p1_k2048
SAT
708.22
hid_hclient_ecdisp.c
FAIL
708.57
network_trans_sys_notify.c
FAIL
727.15
add4_COMPLETE
FAIL
736.12
add7_COMPLETE
FAIL
749.72
network_ndis_coisdn_TpiParam.c
FAIL
756.31
filesys_smbmrx_midatlas.c
FAIL
756.78
network_ndis_rtlnwifi_hw_hw_ccmp.c
FAIL
762.72
C5315.blif_0.10_0.20_0_1_inp_exact
FAIL
770.35
network_irda_miniport_nscirda_comm.c
FAIL
788.72
hid_firefly_app_firefly.cpp
FAIL
796.07
c1_BMC_p1_k2048
SAT
797.23
input_mouser_cseries.c
FAIL
807.5
cf_7_8x8_r_
FAIL
813.41
depots09_13
UNSAT
816.15
filesys_fastfat_easup.c
FAIL
822.06
cube_c11_par---13_
UNSAT
828.75
filesys_smbmrx_cvsndrcv.c
FAIL
831.98
kmdf_AMCC5933_sys_S5933DK1.c
FAIL
853.68
C6288.blif_0.10_1.00_0_0_inp_exact
FAIL
861.43
connect_7x6_4_R
FAIL
867.21
sortnetsort9.v.stepl.005
FAIL
869.21
ev-pr-6x6-5-5-0-1-2-s
UNSAT
879.69
k_branch_n-20
FAIL
880.42
audio_ddksynth_csynth2.cpp
FAIL
894.73
gttt_1_1_000111_4x4_torus_b
FAIL
900
k_ph_p-13
FAIL
900
k_ph_p-19
FAIL
900
ev-pr-4x4-11-3-0-0-1-s
FAIL
900
b14_PR_1_50
FAIL
900
C880.blif_0.10_0.20_0_0_inp_exact
FAIL
900
ev-pr-4x4-17-3-0-0-1-lg
FAIL
900
counter_64
FAIL
900
k_ph_p-18
FAIL
900
k_ph_p-17
FAIL
900
query21_query58_1344n
FAIL
900
C880.blif_0.10_1.00_0_0_inp_exact
FAIL
900
b18_PR_4_2
FAIL
900
unit6_3_b
FAIL
900
k_ph_p-12
FAIL
900
cf_2_9x6_r_
FAIL
900
k_ph_p-15
FAIL
900
C5315.blif_0.10_0.20_0_0_out_exact
FAIL
900
s38584_3_238
FAIL
900
k_ph_p-14
FAIL
900
gttt_2_1_001020_4x4_torus_w
FAIL
900
k_branch_p-21
FAIL
900
gttt_1_1_000111_4x4_torus_w
FAIL
900
arbiter-09-comp-error01-qbf-hardness-depth-21
FAIL
900
query10_query36_1344
FAIL
900
k_branch_p-19
FAIL
900
arbiter-10-comp-error01-qbf-hardness-depth-23
FAIL
900
connect_9x8_3_R
FAIL
900
ev-pr-8x8-15-7-0-1-2-lg
FAIL
900
C5315.blif_0.10_0.20_0_1_out_exact
FAIL
900
k_branch_n-21
FAIL
900
arbiter-09-comp-error01-qbf-hardness-depth-15
FAIL
900
arbiter-06-comp-error01-qbf-hardness-depth-11
FAIL
900
arbiter-05-comp-error01-qbf-hardness-depth-8
FAIL
900
pipesnotankage17_5
FAIL
900
ev-pr-6x6-19-5-0-1-2-s
FAIL
900
pipesnotankage17_7
FAIL
900
ev-pr-8x8-11-7-0-1-2-lg
FAIL
900
ev-pr-6x6-15-5-0-1-2-s
FAIL
900
C5315.blif_0.10_0.20_0_0_inp_exact
FAIL
900
k_branch_p-18
FAIL
900
k_branch_n-17
FAIL
900
ev-pr-6x6-7-5-0-1-2-s
FAIL
900
depots09_11
FAIL
900
depots09_12
FAIL
900
ev-pr-4x4-9-3-0-0-1-s
FAIL
900
k_ph_p-21
FAIL
900
arbiter-10-comp-error01-qbf-hardness-depth-24
FAIL
900
uclid-pipe3b
FAIL
900
ev-pr-8x8-17-7-0-1-2-lg
FAIL
900
ev-pr-6x6-13-5-0-1-2-lg
FAIL
900
pipesnotankage17_6
FAIL
900
C6288.blif_0.10_0.20_0_1_inp_exact
FAIL
900
add6_REDUCED
FAIL
900
s820_d10_s
FAIL
900
k_branch_p-16
FAIL
900
ev-pr-6x6-13-5-0-1-2-s
FAIL
900
ltl2dpa_C26_comp2_REAL.sat
FAIL
900
ev-pr-6x6-17-5-0-1-2-s
FAIL
900
Adder2-16-c
FAIL
900
ev-pr-8x8-13-7-0-1-2-lg
FAIL
900
load_full_4_comp3_REAL.sat
FAIL
900
C6288.blif_0.10_1.00_0_0_out_exact
FAIL
900
load_3c_comp_comp7_REAL.sat
FAIL
900
ev-pr-6x6-19-5-0-1-2-lg
FAIL
900
test2_quant_squaring2
FAIL
900
ev-pr-6x6-9-5-0-1-2-s
FAIL
900
C6288.blif_0.10_0.20_0_0_out_exact
FAIL
900
ev-pr-6x6-11-5-0-1-2-s
FAIL
900
add5_COMPLETE
FAIL
900
add7_CHOOSE
FAIL
900
add5_REDUCED
FAIL
900
add7_REDUCED
FAIL
900
add5_CHOOSE
FAIL
900
add6_COMPLETE
FAIL
900
add4_CHOOSE
FAIL
900
add4_REDUCED
FAIL
900
add6_CHOOSE
FAIL
900
counter_re_32
FAIL
900
ev-pr-6x6-11-5-0-1-2-lg
FAIL
900
connect_8x7_6_R
FAIL
900
ev-pr-4x4-15-3-0-0-1-s
FAIL
900
oski3ub5i_c0to255.sat
FAIL
900
connect_8x7_4_R
FAIL
900
UserServiceImpl
FAIL
900
ProjectService3
FAIL
900
ProcessBean
FAIL
900
LoginService2
FAIL
900
ActivityService2
FAIL
900
connect_8x7_5_R
FAIL
900
ev-pr-6x6-15-5-0-1-2-lg
FAIL
900
eijkbs4863
FAIL
900
bobsmfpu
FAIL
900
connect_9x8_6_R
FAIL
900
s3330_d10_u
FAIL
900
C6288.blif_0.10_1.00_0_1_inp_exact
FAIL
900
test2_quant3
FAIL
900
ev-pr-4x4-13-3-0-0-1-s
FAIL
900
ev-pr-4x4-17-3-0-0-1-s
FAIL
900
ev-pr-4x4-7-3-0-0-1-s
FAIL
900
s3330_d4_s
FAIL
900
C6288.blif_0.10_0.20_0_0_inp_exact
FAIL
900
test2_quant_squaring3
FAIL
900
genbuf10b4n.sat
FAIL
900
s1269_d10_s
FAIL
900
C880.blif_0.10_0.20_0_1_inp_exact
FAIL
900
ev-pr-8x8-19-7-0-1-2-lg
FAIL
900
cycle_sched_6_7_1.sat
FAIL
900
C6288.blif_0.10_0.20_0_1_out_exact
FAIL
900
cycle_sched_4_7_1.sat
FAIL
900
amba4b9y.unsat
FAIL
900
amba4b9y.sat
FAIL
900
k_ph_p-20
FAIL
900
cf_3_9x6_r_
FAIL
900
c3_Debug_s3_f2_e2_v3
FAIL
900
filesys_cdfs_allocsup.c
FAIL
900
filesys_cdfs_namesup.c
FAIL
900
AVStream_hwsim.cpp
FAIL
900
audio_ac97_wavepcistream.cpp
FAIL
900
ring_r7_ser---19_
FAIL
900
ring_r7_ser--opt-20_
FAIL
900
small-pipeline-fixpoint-7
FAIL
900
small-equiv-fixpoint-10
FAIL
900
c5_BMC_p1_k128
FAIL
900
c5_BMC_p1_k64
FAIL
900
c5_BMC_p2_k1024
FAIL
900
c5_BMC_p2_k128
FAIL
900
c5_BMC_p2_k256
FAIL
900
network_usbnwifi_mp_util.c
FAIL
900
network_ndis_rtlnwifi_extsta_st_misc.c
FAIL
900
kernel_agplib_intrface.c
FAIL
900
c4_Debug_s5_f2_e2_v1
FAIL
900
blocks_enc_2_b4_ser--opt-26_
FAIL
900
s499_d25_u
FAIL
900
cube_c11_ser--opt-42_
FAIL
900
cube_c7_ser---23_
FAIL
900
emptyroom_e4_par---21_
FAIL
900
emptyroom_e4_ser--opt-44_
FAIL
900
ring_r6_ser--opt-17_
FAIL
900
incrementer-enc02-nonuniform-depth-60
FAIL
900
incrementer-enc02-nonuniform-depth-59
FAIL
900
incrementer-enc02-nonuniform-depth-58
FAIL
900
k8_2_3
FAIL
900
kmdf_pcidrv_sys_hw_physet.c
FAIL
900
c5_BMC_p2_k512
FAIL
900
small-equiv-fixpoint-9
FAIL
900
k12_3_2
FAIL
900
s510_d41_s
FAIL
900
s713_d11_u
FAIL
900
s298_d25_u
FAIL
900
s820_d15_u
FAIL
900
s510_d36_s
FAIL
900
k10_4_3
FAIL
900
k6_2_3
FAIL
900
k8_4_3
FAIL
900
k14_2_3
FAIL
900
k14_4_4
FAIL
900
k8_3_2
FAIL
900
k7_2_2
FAIL
900
k8_3_4
FAIL
900
k12_4_2
FAIL
900
Core1108_tbm_21.tex.module.000008
FAIL
900
c5_BMC_p2_k64
FAIL
900
pi-bus-fixpoint-3
FAIL
900
f600-00
FAIL
900
f600-50
FAIL
900
ii8d1-00
FAIL
900
small-pipeline-fixpoint-6
FAIL
900
ii8d1-90
FAIL
900
small-equiv-fixpoint-6
FAIL
900
ssa7552-158-00
FAIL
900
stmt39_285_335
FAIL
900
usb-phy-fixpoint-3
FAIL
900
Umbrella_tbm_05.tex.module.000039
FAIL
900
Core1108_tbm_21.tex.module.000030
FAIL
900
k7_4_4
FAIL
900
c3_Debug_s3_f2_e2_v2
FAIL
900
cf_4_9x9_r_
FAIL
900
gttt_2_1_00011020_4x4_b
FAIL
900
gttt_1_1_00101121_4x4_torus_w
FAIL
900
cmu.dme1.B-f3
FAIL
900
eijk.bs1512.S-f4
FAIL
900
eijk.bs3384.S-f4
FAIL
900
nusmv.tcas^2.B-f2
FAIL
900
nusmv.tcas^3.B-f2
FAIL
900
nusmv.tcas^4.B-f3
FAIL
900
nusmv.tcas^6.B-f4
FAIL
900
sortnetsort10.v.stepl.005
FAIL
900
sortnetsort8.v.stepl.007
FAIL
900
b22_PR_8_20
FAIL
900
b22_C_2_12
FAIL
900
gttt_2_1_00102030_4x4_torus_b
FAIL
900
nusmv.tcas-t^1.B-d2
FAIL
900
eijk.bs4863.S-d4
FAIL
900
cf_5_5x6_r_
FAIL
900
cf_6_9x7_r_
FAIL
900
cf_7_8x7_r_
FAIL
900
s1196_d5_u
FAIL
900
s1196_d7_u
FAIL
900
s1269_d5_s
FAIL
900
ev-pr-6x6-17-5-0-1-2-lg
FAIL
900
s1196_1_5
FAIL
900
query44_query26_1344n
FAIL
900
query42_query06_1344n
FAIL
900
query31_reachqu_1344n
FAIL
900
query03_query25_1344
FAIL
900
s499_d19_s
FAIL
900
b21_C_3_206
FAIL
900
b20_PR_7_20
FAIL
900
biu.mv.xl_ao.bb-b003-p020-IPF02-c05.blif-biu.inv.prop.bb-bmc.with-IOC.unfold-007
FAIL
900
biu.mv.xl_ao.bb-b003-p020-IPF02-c05.blif-biu.inv.prop.bb-bmc.with-IOC.unfold-010
FAIL
900
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
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-IPF03-c03.blif-biu.inv.prop.bb-bmc.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
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
biu.mv.xl_ao.bb-b003-p020-MIF02-c01.blif-biu.inv.prop.bb-bmc.with-IOC.unfold-009
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
biu.mv.xl_ao.bb-b003-p020-MIF04-c05.blif-biu.inv.prop.bb-bmc.with-IOC.unfold-008
FAIL
900
c1_Debug_s3_f1_e1_v1
FAIL
900
c1_Debug_s3_f2_e1_v1
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
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.conf05.01X-QBF.BB1-Zi.BB2-01X.BB3-Zi.with-IOC.unfold-007
FAIL
900
b20_C_3_2
FAIL
900
arbiter-10-comp-error01-qbf-hardness-depth-22
FAIL
900
arbiter-08-comp-error02-qbf-hardness-depth-9
FAIL
900
arbiter-07-comp-error01-qbf-hardness-depth-20
FAIL
900
arbiter-06-comp-error01-qbf-hardness-depth-15
FAIL
900
sortnetsort9.AE.stepl.009
FAIL
900
sortnetsort9.AE.stepl.012
FAIL
900
sortnetsort9.v.stepl.007
FAIL
900
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
900
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
900
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
900
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
900
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
900
c1_Debug_s3_f2_e1_v2
FAIL
900
Contact
|
Organization
|
Links
|
Citing QBFLIB