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
rev_qfun0.1
QBFEVAL'17 - Prenex CNF Track
Instance
Result
Time
small-bug1-fixpoint-7
SAT
0
equalization32
SAT
0
halfadder_match2.unsat
UNSAT
0
halfadder_match2.sat
SAT
0
s00400_PR_9_90
UNSAT
0
lights3_021_1_022
SAT
0.01
floor256
SAT
0.01
mvs16y.sat
SAT
0.01
kenflashp12
SAT
0.01
decomposition256
SAT
0.01
pdtpmsmiim
SAT
0.02
ceiling128
SAT
0.02
rankfunc60_signed_32
SAT
0.03
tlc05-nonuniform-depth-6
UNSAT
0.03
driver_d9y.unsat
UNSAT
0.04
driver_d9y.sat
SAT
0.04
small-dyn-partition-fixpoint-8
UNSAT
0.05
small-synabs-fixpoint-3
UNSAT
0.05
tlc04-nonuniform-depth-8
UNSAT
0.05
cf_4_7x4_d_
UNSAT
0.05
cf_6_6x6_w_
UNSAT
0.06
stay24n.unsat
UNSAT
0.08
rankfunc35_signed_32
SAT
0.09
incrementer-enc03-nonuniform-depth-5
UNSAT
0.1
driver_a9n.unsat
UNSAT
0.11
cnt16
SAT
0.12
eijkbs4863
SAT
0.14
driver_a9n.sat
SAT
0.18
ltl2dba_C2-6_comp3_REAL.sat
SAT
0.2
cf_8_8x8_d_
UNSAT
0.21
fpu-10Xh-correct02-nonuniform-depth-2
UNSAT
0.21
mult_bool_matrix_10_9_11.sat
SAT
0.25
C432.blif_0.10_0.20_0_1_out_exact
UNSAT
0.25
mvs16y.unsat
UNSAT
0.25
C432.blif_0.10_0.20_0_0_out_exact
UNSAT
0.28
fpu-10Xh-correct03-uniform-depth-3
UNSAT
0.29
fpu-10Xh-correct04-uniform-depth-3
UNSAT
0.29
cf_8_9x8_d_
UNSAT
0.29
fpu-01Xh-error02-nonuniform-depth-3
UNSAT
0.29
C880.blif_0.10_1.00_0_0_out_exact
UNSAT
0.35
unit9_2_b
SAT
0.45
itc-b13-fixpoint-5
SAT
0.47
fpu-10Xe-correct02-nonuniform-depth-6
UNSAT
0.56
cf_5_9x9_d_
UNSAT
0.63
C880.blif_0.10_0.20_0_1_out_exact
UNSAT
0.64
C880.blif_0.10_0.20_0_0_out_exact
UNSAT
0.64
k_branch_p-16
UNSAT
0.64
fpu-01Xh-error02-nonuniform-depth-7
UNSAT
0.68
fpu-01Xh-error02-uniform-depth-8
UNSAT
0.76
fpu-10Xh-correct02-nonuniform-depth-8
UNSAT
0.76
cmu.dme1.B-f3
SAT
0.78
ltl2dba_C2-6_comp3_REAL.unsat
UNSAT
0.81
fpu-10Xh-correct03-uniform-depth-10
UNSAT
0.95
eijk.bs3330.S-d3
SAT
1
unit11_3_b
UNSAT
1.1
C499.blif_0.10_0.20_0_1_out_exact
UNSAT
1.12
ltl2dpa_C26_comp2_REAL.sat
SAT
1.19
fpu-10Xh-correct02-uniform-depth-13
UNSAT
1.21
fpu-01Xh-error02-nonuniform-depth-13
UNSAT
1.21
fpu-10Xh-correct04-nonuniform-depth-13
UNSAT
1.21
C499.blif_0.10_0.20_0_0_out_exact
UNSAT
1.24
dungeon_i10-m10-u10-v0.pddl_planlen=166
UNSAT
1.28
fpu-10Xh-correct03-uniform-depth-14
UNSAT
1.29
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
UNSAT
1.36
cmu.dme2.B-f3
SAT
1.49
fpu-01Xh-error02-uniform-depth-18
UNSAT
1.64
fpu-10Xe-correct02-nonuniform-depth-16
UNSAT
1.67
Adder2-8-c
UNSAT
1.67
stmt21_181_369
UNSAT
1.7
cmu.gigamax.B-d4
SAT
1.71
C5315.blif_0.10_1.00_0_0_out_exact
UNSAT
1.84
C880.blif_0.10_1.00_0_0_inp_exact
UNSAT
1.85
nusmv.tcas-t^1.B-d2
SAT
1.89
fpu-01Xh-error02-nonuniform-depth-22
UNSAT
1.93
fpu-10Xh-correct03-nonuniform-depth-22
UNSAT
1.94
fpu-10Xe-correct02-uniform-depth-20
UNSAT
2.1
fpu-10Xh-correct04-uniform-depth-24
UNSAT
2.1
fpu-10Xh-correct03-nonuniform-depth-26
UNSAT
2.29
ltl2dpa_C26_comp2_REAL.unsat
UNSAT
2.3
C6288.blif_0.10_1.00_0_1_inp_exact
SAT
2.3
sortnetsort8.v.stepl.007
SAT
2.39
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
2.9
tlc03-nonuniform-depth-19
UNSAT
3.01
nusmv.tcas^2.B-f2
SAT
3.1
incrementer-enc06-nonuniform-depth-10
UNSAT
3.15
nusmv.tcas^3.B-f2
SAT
3.17
nusmv.reactor^3.C-d4
SAT
3.2
s05378_PR_9_75
UNSAT
3.45
tlc02-nonuniform-depth-73
FAIL
3.65
dungeon_i20-m100-u4-v0.pddl_planlen=6
SAT
3.71
arbiter-05-comp-error01-qbf-hardness-depth-8
UNSAT
3.75
query03_query25_1344
UNSAT
3.8
texas.PI_main^05.E-f3
SAT
3.85
s09234_PR_9_5
SAT
4.1
oski3ub5i_c0to255.unsat
UNSAT
4.19
biu.mv.xl_ao.bb-b003-p020-IPF02-c05.blif-biu.inv.prop.bb-bmc.with-IOC.unfold-007
UNSAT
4.2
tlc04-nonuniform-depth-27
UNSAT
4.2
unit8_2_b
SAT
4.91
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
UNSAT
5.16
texas.PI_main^08.E-f3
SAT
5.16
add4_REDUCED
SAT
5.22
pipesnotankage04_5
UNSAT
5.23
s1196_1_5
SAT
5.24
nusmv.tcas^4.B-f3
SAT
5.25
tlc05-nonuniform-depth-73
FAIL
5.4
biu.mv.xl_ao.bb-b003-p020-MIF04-c05.blif-biu.inv.prop.bb-bmc.with-IOC.unfold-008
UNSAT
5.87
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
UNSAT
5.87
incrementer-enc08-nonuniform-depth-24
UNSAT
5.88
s641_d6_s
SAT
5.91
unit12_2_b
SAT
6.23
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
UNSAT
6.31
incrementer-enc07-uniform-depth-25
UNSAT
6.68
stmt29_226_376
UNSAT
6.84
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
UNSAT
6.88
biu.mv.xl_ao.bb-b003-p020-MIF02-c01.blif-biu.inv.prop.bb-bmc.with-IOC.unfold-009
UNSAT
7.03
add4_COMPLETE
SAT
7.09
driverlog10_6
UNSAT
7.21
incrementer-enc02-nonuniform-depth-58
FAIL
7.56
incrementer-enc08-uniform-depth-33
SAT
7.59
incrementer-enc02-nonuniform-depth-59
FAIL
7.67
incrementer-enc02-uniform-depth-58
FAIL
7.67
incrementer-enc05-nonuniform-depth-22
UNSAT
7.69
incrementer-enc02-nonuniform-depth-60
FAIL
7.74
Adder2-16-c
UNSAT
7.85
incrementer-enc06-uniform-depth-24
UNSAT
7.87
beemldelec4b1_c0to127.unsat
UNSAT
7.88
nusmv.tcas^6.B-f4
SAT
7.96
tlc02-uniform-depth-151
FAIL
8.1
incrementer-enc02-uniform-depth-63
FAIL
8.29
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
UNSAT
8.59
biu.mv.xl_ao.bb-b003-p020-IPF03-c03.blif-biu.inv.prop.bb-bmc.with-IOC.unfold-009
UNSAT
8.71
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
UNSAT
8.72
s38584_3_238
SAT
8.78
tlc01-nonuniform-depth-63
UNSAT
8.96
biu.mv.xl_ao.bb-b003-p020-IPF02-c05.blif-biu.inv.prop.bb-bmc.with-IOC.unfold-010
UNSAT
9.4
dungeon_i30-m30-u5-v0.pddl_planlen=4
UNSAT
9.47
eijk.bs4863.S-d4
SAT
9.59
eijk.bs1512.S-f4
SAT
10.34
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
UNSAT
10.75
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
UNSAT
10.8
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
UNSAT
11.34
C5315.blif_0.10_0.20_0_1_inp_exact
SAT
11.34
k_ph_p-11
UNSAT
11.4
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
UNSAT
12.07
s298_d17_s
SAT
12.28
tlc03-nonuniform-depth-67
UNSAT
12.72
emptyroom_e3_ser---19_
UNSAT
12.78
emptyroom_e4_par---21_
UNSAT
12.79
load_3c_comp_comp7_REAL.unsat
UNSAT
12.87
tlc04-nonuniform-depth-64
UNSAT
13.38
c1_BMC_p2_k1024
UNSAT
13.68
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
UNSAT
13.84
cube_c11_par---13_
UNSAT
14.44
ken.flash^09.C-d4
UNSAT
15.12
b14_PR_1_50
SAT
16.13
b20_PR_7_20
SAT
16.36
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
UNSAT
16.55
add4_CHOOSE
SAT
16.68
amba2f9n.unsat
UNSAT
17.21
b15_PR_4_2
SAT
18.11
b17_PR_0_90
UNSAT
18.32
dungeon_i30-m30-u5-v0.pddl_planlen=8
UNSAT
18.84
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
UNSAT
19.18
add5_REDUCED
SAT
19.85
network_trans_sys_notify.c
UNSAT
20.05
dungeon_i30-m30-u5-v0.pddl_planlen=9
UNSAT
21.32
c5_BMC_p1_k32
SAT
21.49
szymanski-20-s
UNSAT
22.45
sortnetsort9.AE.stepl.012
UNSAT
22.46
s499_d19_s
SAT
23.16
s641_d7_u
UNSAT
24.83
c1_BMC_p2_k2048
UNSAT
25.48
C6288.blif_0.10_0.20_0_1_out_exact
SAT
25.49
filesys_smbmrx_cvsndrcv.c
UNSAT
25.7
s820_d10_s
SAT
27.73
c3_BMC_p1_k256
SAT
29.78
stay24n.sat
SAT
29.9
b21_C_3_206
SAT
35.54
uclid-pipe3a
SAT
36.95
stmt17_63_82
SAT
38.02
driverlog12_7
UNSAT
38.16
stmt28_68_81
SAT
42.24
s298_d25_u
UNSAT
42.74
stmt23_72_76
SAT
47.09
stmt23_66_96
SAT
47.2
s3330_d4_s
SAT
47.93
stmt17_70_90
SAT
50.19
stmt19_64_99
SAT
52.92
stmt17_62_98
SAT
53.98
sortnetsort9.AE.stepl.009
UNSAT
54.37
driverlog13_6
UNSAT
54.55
oski3ub5i_c0to255.sat
FAIL
55.39
depots07_8
UNSAT
57.27
stmt17_70_98
SAT
58.27
b22_PR_8_20
SAT
60.18
AR-fixpoint-1
FAIL
61.37
szymanski-24-s
UNSAT
64.05
depots03_9
UNSAT
65.8
s499_d25_u
UNSAT
69.16
s1269_d5_s
SAT
69.26
stmt17_82_98
SAT
74.51
stmt17_86_98
SAT
82.93
add5_CHOOSE
SAT
84.93
unit6_3_b
UNSAT
97.55
ken.flash^05.C-d3
UNSAT
98.61
query10_query36_1344
SAT
100.26
s820_d15_u
UNSAT
101.38
sortnetsort9.v.stepl.007
SAT
109.13
s713_d7_u
UNSAT
127.14
s1196_d5_u
UNSAT
131.24
s713_d11_u
UNSAT
142.56
load_full_4_comp3_REAL.unsat
UNSAT
148.03
uclid-pipe3b
UNSAT
150.13
ring_r7_ser---19_
UNSAT
162.54
add5_COMPLETE
SAT
167.29
genbuf9b4n.unsat
UNSAT
171.51
s510_d36_s
SAT
184.97
emptyroom_e4_ser--opt-44_
SAT
195.52
depots08_6
UNSAT
196.15
AR-fixpoint-3
FAIL
196.51
dungeon_i15-m7-u4-v0.pddl_planlen=81
UNSAT
200.61
s510_d41_s
SAT
212.51
b18_PR_4_2
SAT
215
pipesnotankage11_8
UNSAT
234.99
pipesnotankage13_5
UNSAT
241.96
AR-fixpoint-5
FAIL
243.23
c2_BMC_p1_k2048
SAT
244.85
ii8d1-00
SAT
245.66
genbuf10b4n.unsat
UNSAT
250.16
AR-fixpoint-7
FAIL
278.65
dungeon_i15-m7-u4-v0.pddl_planlen=168
UNSAT
293
s1196_d7_u
UNSAT
317.24
depots16_5
UNSAT
327.46
AR-fixpoint-9
FAIL
333.76
ken.flash^08.C-d4
UNSAT
466.66
freecell02_4
UNSAT
466.93
depots13_9
SAT
578.86
b20_C_3_2
SAT
668.06
add6_CHOOSE
SAT
677.38
gttt_1_1_001020_3x3_torus_b
UNSAT
715.67
freecell02_6
UNSAT
724.09
cycle_sched_4_7_1.unsat
UNSAT
777.39
c1_BMC_p1_k2048
FAIL
806.03
pipesnotankage17_5
UNSAT
842.11
pipesnotankage17_6
UNSAT
845.28
k5_2_3
SAT
848.56
pipesnotankage16_10
UNSAT
851.87
pipesnotankage15_10
UNSAT
857.99
pipesnotankage17_7
UNSAT
859.51
pipesnotankage14_10
UNSAT
860.81
k_ph_p-12
UNSAT
883.77
c3_Debug_s3_f2_e2_v2
FAIL
887.92
c3_Debug_s3_f2_e2_v3
FAIL
889.02
c1_Debug_s3_f2_e1_v1
FAIL
893.13
add7_CHOOSE
FAIL
894.93
c4_Debug_s3_f1_e2_v2
FAIL
895.32
c4_Debug_s3_f1_e1_v2
FAIL
895.38
c4_Debug_s3_f1_e2_v3
FAIL
895.91
dungeon_i25-m12-u5-v0.pddl_planlen=198
FAIL
895.97
dungeon_i25-m12-u5-v0.pddl_planlen=200
FAIL
896.02
dungeon_i25-m12-u5-v0.pddl_planlen=199
FAIL
896.11
dungeon_i25-m12-u5-v0.pddl_planlen=197
FAIL
896.11
dungeon_i25-m12-u3-v0.pddl_planlen=190
FAIL
896.23
dungeon_i25-m12-u5-v0.pddl_planlen=170
FAIL
896.52
c1_Debug_s3_f2_e1_v2
FAIL
896.54
c4_Debug_s5_f2_e2_v1
FAIL
896.63
dungeon_i25-m12-u3-v0.pddl_planlen=165
FAIL
896.81
mult_bool_matrix_17_17_17.unsat
FAIL
900
mult_bool_matrix_10_9_11.unsat
FAIL
900
mult_bool_matrix_17_17_17.sat
FAIL
900
arbiter-06-comp-error01-qbf-hardness-depth-15
FAIL
900
add7_REDUCED
FAIL
900
beemldelec4b1_c0to127.sat
FAIL
900
add6_COMPLETE
FAIL
900
amba4b9y.sat
FAIL
900
amba4b9y.unsat
FAIL
900
cycle_sched_6_7_1.sat
FAIL
900
genbuf10b4n.sat
FAIL
900
add6_REDUCED
FAIL
900
genbuf9b4n.sat
FAIL
900
load_3c_comp_comp7_REAL.sat
FAIL
900
arbiter-07-comp-error01-qbf-hardness-depth-20
FAIL
900
load_full_4_comp3_REAL.sat
FAIL
900
cycle_sched_4_7_1.sat
FAIL
900
pipesnotankage18_8
FAIL
900
add7_COMPLETE
FAIL
900
cycle_sched_6_7_1.unsat
FAIL
900
pipesnotankage19_7
FAIL
900
freecell03_6
FAIL
900
freecell03_5
FAIL
900
depots09_13
FAIL
900
depots09_12
FAIL
900
depots09_11
FAIL
900
dungeon_i25-m12-u5-v0.pddl_planlen=98
FAIL
900
dungeon_i25-m12-u5-v0.pddl_planlen=92
FAIL
900
dungeon_i25-m12-u5-v0.pddl_planlen=86
FAIL
900
dungeon_i25-m12-u5-v0.pddl_planlen=81
FAIL
900
dungeon_i25-m12-u5-v0.pddl_planlen=59
FAIL
900
freecell03_7
FAIL
900
gttt_2_1_001020_4x4_torus_w
FAIL
900
pipesnotankage19_9
FAIL
900
arbiter-06-comp-error01-qbf-hardness-depth-11
FAIL
900
arbiter-09-comp-error01-qbf-hardness-depth-15
FAIL
900
arbiter-09-comp-error01-qbf-hardness-depth-21
FAIL
900
arbiter-10-comp-error01-qbf-hardness-depth-23
FAIL
900
arbiter-10-comp-error01-qbf-hardness-depth-24
FAIL
900
query21_query58_1344n
FAIL
900
s15850_PR_0_50
FAIL
900
gttt_1_1_000111_4x4_torus_b
FAIL
900
gttt_1_1_000111_4x4_torus_w
FAIL
900
dungeon_i25-m12-u5-v0.pddl_planlen=143
FAIL
900
dungeon_i25-m12-u3-v0.pddl_planlen=146
FAIL
900
dungeon_i25-m12-u5-v0.pddl_planlen=128
FAIL
900
ProcessBean
FAIL
900
ProjectService3
FAIL
900
gttt_1_1_00101121_4x4_torus_w
FAIL
900
dungeon_i25-m12-u5-v0.pddl_planlen=65
FAIL
900
dungeon_i25-m12-u3-v0.pddl_planlen=72
FAIL
900
UserServiceImpl
FAIL
900
dungeon_i25-m12-u3-v0.pddl_planlen=130
FAIL
900
amba2f9n.sat
FAIL
900
b22_C_2_12
FAIL
900
arbiter-10-comp-error01-qbf-hardness-depth-22
FAIL
900
gttt_2_1_00011020_4x4_b
FAIL
900
gttt_2_1_00102030_4x4_torus_b
FAIL
900
intermediate128
FAIL
900
dungeon_i25-m12-u3-v0.pddl_planlen=125
FAIL
900
bobsmfpu
FAIL
900
neclaftp4001
FAIL
900
ActivityService2
FAIL
900
query44_query26_1344n
FAIL
900
query42_query06_1344n
FAIL
900
query31_reachqu_1344n
FAIL
900
LoginService2
FAIL
900
pipesnotankage18_7
FAIL
900
arbiter-08-comp-error02-qbf-hardness-depth-9
FAIL
900
ev-pr-4x4-9-3-0-0-1-s
FAIL
900
Adder2-10-s
FAIL
900
ev-pr-6x6-15-5-0-1-2-s
FAIL
900
test1_quant_squaring2
FAIL
900
C5315.blif_0.10_0.20_0_0_inp_exact
FAIL
900
ev-pr-6x6-13-5-0-1-2-lg
FAIL
900
Adder2-8-s
FAIL
900
ev-pr-8x8-17-7-0-1-2-lg
FAIL
900
k_ph_p-21
FAIL
900
C499.blif_0.10_0.20_0_0_inp_exact
FAIL
900
adder-12-unsat
FAIL
900
ev-pr-8x8-11-7-0-1-2-lg
FAIL
900
test4_quant_squaring2
FAIL
900
k_branch_n-21
FAIL
900
C6288.blif_0.10_1.00_0_0_inp_exact
FAIL
900
C5315.blif_0.10_0.20_0_1_out_exact
FAIL
900
test5_quant_squaring5
FAIL
900
adder-12-sat
FAIL
900
ev-pr-8x8-15-7-0-1-2-lg
FAIL
900
connect_9x8_3_R
FAIL
900
test4_quant_squaring4
FAIL
900
ev-pr-4x4-5-3-0-0-1-s
FAIL
900
ev-pr-6x6-7-5-0-1-2-s
FAIL
900
k_branch_n-10
FAIL
900
k_ph_p-15
FAIL
900
cnt08e
FAIL
900
cnt16r
FAIL
900
cf_2_9x6_r_
FAIL
900
cf_3_9x6_r_
FAIL
900
cf_4_9x9_r_
FAIL
900
cf_5_5x6_r_
FAIL
900
cf_6_9x7_r_
FAIL
900
cf_7_8x7_r_
FAIL
900
k_ph_p-14
FAIL
900
k_ph_p-13
FAIL
900
k_ph_p-19
FAIL
900
k_branch_n-11
FAIL
900
k_branch_n-17
FAIL
900
k_branch_p-10
FAIL
900
k_branch_p-11
FAIL
900
k_branch_p-14
FAIL
900
k_branch_p-18
FAIL
900
k_branch_p-19
FAIL
900
k_ph_p-17
FAIL
900
k_ph_p-18
FAIL
900
cf_7_8x8_r_
FAIL
900
ev-pr-6x6-19-5-0-1-2-s
FAIL
900
counter_re_32
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
connect_8x7_4_R
FAIL
900
ev-pr-4x4-7-3-0-0-1-s
FAIL
900
C6288.blif_0.10_0.20_0_0_inp_exact
FAIL
900
test2_quant_squaring3
FAIL
900
s1269_d10_s
FAIL
900
C880.blif_0.10_0.20_0_1_inp_exact
FAIL
900
C6288.blif_0.10_1.00_0_0_out_exact
FAIL
900
ev-pr-8x8-13-7-0-1-2-lg
FAIL
900
ev-pr-6x6-17-5-0-1-2-s
FAIL
900
adder-14-sat
FAIL
900
ev-pr-6x6-11-5-0-1-2-lg
FAIL
900
connect_8x7_6_R
FAIL
900
adder-10-sat
FAIL
900
ev-pr-4x4-15-3-0-0-1-s
FAIL
900
ev-pr-6x6-11-5-0-1-2-s
FAIL
900
C6288.blif_0.10_0.20_0_0_out_exact
FAIL
900
k_branch_n-12
FAIL
900
ev-pr-6x6-13-5-0-1-2-s
FAIL
900
connect_7x6_4_R
FAIL
900
ev-pr-8x8-19-7-0-1-2-lg
FAIL
900
k_branch_p-12
FAIL
900
C5315.blif_0.10_0.20_0_0_out_exact
FAIL
900
test1_quant_squaring3
FAIL
900
k_branch_p-21
FAIL
900
Adder2-16-s
FAIL
900
ev-pr-4x4-11-3-0-0-1-s
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
Adder2-14-s
FAIL
900
C6288.blif_0.10_0.20_0_1_inp_exact
FAIL
900
k_ph_p-20
FAIL
900
uclid-pipe2
FAIL
900
ev-pr-4x4-17-3-0-0-1-s
FAIL
900
ev-pr-4x4-13-3-0-0-1-s
FAIL
900
connect_8x7_5_R
FAIL
900
k_branch_n-20
FAIL
900
ev-pr-6x6-15-5-0-1-2-lg
FAIL
900
connect_9x8_6_R
FAIL
900
s3330_d10_u
FAIL
900
test2_quant3
FAIL
900
ev-pr-6x6-5-5-0-1-2-s
FAIL
900
ev-pr-6x6-17-5-0-1-2-lg
FAIL
900
k14_2_3
FAIL
900
small-seq-fixpoint-3
FAIL
900
cache-coherence-3-fixpoint-3
FAIL
900
cache-coherence-2-fixpoint-6
FAIL
900
pi-bus-fixpoint-3
FAIL
900
small-equiv-fixpoint-9
FAIL
900
sdlx-fixpoint-3
FAIL
900
pi-bus-fixpoint-1
FAIL
900
cache-coherence-2-fixpoint-4
FAIL
900
small-equiv-fixpoint-10
FAIL
900
small-pipeline-fixpoint-6
FAIL
900
small-seq-fixpoint-7
FAIL
900
small-equiv-fixpoint-6
FAIL
900
k8_4_3
FAIL
900
k6_2_3
FAIL
900
test3_quant_squaring4
FAIL
900
Core1108_tbm_21.tex.module.000008
FAIL
900
Core1108_tbm_21.tex.module.000030
FAIL
900
Umbrella_tbm_05.tex.module.000039
FAIL
900
small-seq-fixpoint-9
FAIL
900
usb-phy-fixpoint-3
FAIL
900
small-seq-fixpoint-8
FAIL
900
small-pipeline-fixpoint-7
FAIL
900
small-seq-fixpoint-5
FAIL
900
network_ndis_coisdn_TpiParam.c
FAIL
900
input_mouser_detect.c
FAIL
900
network_usbnwifi_mp_util.c
FAIL
900
network_ndis_rtlnwifi_extsta_st_misc.c
FAIL
900
kmdf_AMCC5933_sys_S5933DK1.c
FAIL
900
audio_ddksynth_csynth2.cpp
FAIL
900
kernel_agplib_intrface.c
FAIL
900
kmdf_pcidrv_sys_hw_physet.c
FAIL
900
input_mouser_cseries.c
FAIL
900
network_irda_miniport_nscirda_comm.c
FAIL
900
hid_hclient_ecdisp.c
FAIL
900
filesys_smbmrx_midatlas.c
FAIL
900
audio_ac97_wavepcistream.cpp
FAIL
900
hid_firefly_app_firefly.cpp
FAIL
900
network_irda_miniport_nscirda_settings.c
FAIL
900
filesys_fastfat_easup.c
FAIL
900
AVStream_hwsim.cpp
FAIL
900
network_ndis_rtlnwifi_hw_hw_ccmp.c
FAIL
900
filesys_cdfs_namesup.c
FAIL
900
filesys_cdfs_allocsup.c
FAIL
900
input_pnpi8042_moudep.c
FAIL
900
incrementer-enc04-nonuniform-depth-17
FAIL
900
k14_4_4
FAIL
900
ken.oop^2.C-d3
FAIL
900
c4_Debug_s3_f2_e2_v3
FAIL
900
blocks_enc_2_b4_ser--opt-26_
FAIL
900
cube_c11_ser--opt-42_
FAIL
900
cube_c7_ser---23_
FAIL
900
ring_r6_ser--opt-17_
FAIL
900
ring_r7_ser--opt-20_
FAIL
900
c5_BMC_p1_k128
FAIL
900
c5_BMC_p1_k64
FAIL
900
c5_BMC_p2_k1024
FAIL
900
c4_Debug_s3_f2_e2_v2
FAIL
900
c2_Debug_s3_f2_e1_v3
FAIL
900
c2_Debug_s3_f1_e1_v2
FAIL
900
ken.oop^2.C-d4
FAIL
900
eijk.bs3384.S-f4
FAIL
900
eijk.S1196.S-f2
FAIL
900
eijk.S713.S-f2
FAIL
900
ken.flash^11.C-f3
FAIL
900
sortnetsort10.v.stepl.005
FAIL
900
sortnetsort9.v.stepl.005
FAIL
900
c1_Debug_s3_f1_e1_v1
FAIL
900
c1_Debug_s5_f1_e1_v2
FAIL
900
c5_BMC_p2_k128
FAIL
900
c5_BMC_p2_k256
FAIL
900
stmt32_329_378
FAIL
900
k12_4_2
FAIL
900
k8_3_4
FAIL
900
k12_3_2
FAIL
900
k10_4_3
FAIL
900
k5_3_2
FAIL
900
k8_2_3
FAIL
900
k7_4_4
FAIL
900
k7_2_2
FAIL
900
stmt19_83_412
FAIL
900
stmt21_310_360
FAIL
900
stmt41_160_235
FAIL
900
c5_BMC_p2_k512
FAIL
900
c5_BMC_p2_k64
FAIL
900
f600-00
FAIL
900
f600-50
FAIL
900
ii8d1-90
FAIL
900
ssa7552-158-00
FAIL
900
stmt39_285_335
FAIL
900
stmt21_319_418
FAIL
900
stmt19_313_412
FAIL
900
k8_3_2
FAIL
900
Contact
|
Organization
|
Links
|
Citing QBFLIB