AADDBBCC_eval12

Overview

• number of participating solvers: 12
• number of participating formulas: 241

Overall Solving Statistics

Number of Solved Formulas

SOLVER	SAT	UNSAT	TOTAL
rareqs-1.1	59	45	104
depqbf-lazy-qup	59	45	104
depqbf	59	43	102
hiqqer3	52	38	90
ooq	56	34	90
dual_ooq	54	26	80
pre_dual_ooq.py	43	21	64
ghost-plain.sh	43	18	61
ghost-cegar.sh	40	19	59
ghost-bq-cegar.sh	40	19	59
squeezebf1.2-qube3.0	37	21	58
nenofex	34	18	52

Time Statistics (overall runtime, average runtime)

solver	AVERAGE	SUM
rareqs-1.1	535.06	128951.37
depqbf-lazy-qup	548.77	132254.75
depqbf	555.96	133988.60
ooq	587.02	141473.61
hiqqer3	600.93	144824.19
dual_ooq	628.16	151387.39
pre_dual_ooq.py	688.03	165816.93
ghost-plain.sh	695.53	167624.15
squeezebf1.2-qube3.0	697.03	167986.26
ghost-bq-cegar.sh	698.69	168384.48
ghost-cegar.sh	698.78	168406.20
nenofex	717.39	172892.45

Number of Unsolved Formulas (solved by no solver)

formula
k12_4_2
uclid-pipe3a
test4_quant_squaring4
test4_quant4
C880.blif_0.10_0.20_0_0_out_exact
s1269_d15_u
k12_3_3
connect_7x6_4_R
test1_quant_squaring3
stmt19_83_91
C880.blif_0.10_0.20_0_0_inp_exact
k_branch_n-20
cube_c11_ser--opt-42_
nusmv.tcas^2.B-f2
connect_9x8_3_R
s3330_d13_u
nusmv.tcas-t^6.B-f3
k_ph_p-17
c2_Debug_s5_f1_e1_v3
C880.blif_0.10_0.20_0_1_inp_exact
stmt17_74_78
k_ph_p-18
b22_PR_8_20
b04_C_2_20
s38584_3_238
s1196_d5_u
k_ph_p-12
test1_quant3
s1269_d9_s
s3330_d11_u
test1_quant2
filesys_cdfs_namesup.c
k_ph_p-16
vis.prodcell^24.E-f3
s1196_d6_u
cmu.dme1.B-f4
C5315.blif_0.10_0.20_0_1_out_exact
W5-Umbrella_tbm_25.tex.moduleQ3.7S.000003
audio_ddksynth_voice.cpp
W5-Umbrella_tbm_05.tex.moduleQ3.8S.000001
AR-fixpoint-2
stmt23_92_96
s1196_d3_u
cube_c7_ser---23_
test2_quant2
C6288.blif_0.10_0.20_0_1_out_exact
test2_quant_squaring2
C5315.blif_0.10_0.20_0_0_out_exact
s1269_d10_s
C880.blif_0.10_0.20_0_1_out_exact
vis.prodcell^23.E-f4
C6288.blif_0.10_0.20_0_1_inp_exact
k_branch_n-21
C5315.blif_0.10_0.20_0_0_inp_exact
s1269_d8_s
stmt17_94_98
test3_quant_squaring4
b20_PR_5_10
b22_C_2_12
ring_r7_ser--opt-20_
filesys_smbmrx_smbxchng.c
k6_4_3
b21_C_3_206
b14_C_3_105
k12_2_2
s1196_d7_u
adder-12-sat
s3330_d10_u
stmt17_82_86
k12_2_3
c3_Debug_s3_f2_e2_v2
ev-pr-8x8-19-7-0-1-2-lg
test1_quant_squaring2
C499.blif_0.10_0.20_0_0_out_exact
uclid-pipe2
filesys_fastfat_easup.c
C499.blif_0.10_0.20_0_1_out_exact
k14_3_3
s1269_d13_u
nusmv.tcas^4.B-f3
stmt17_70_82
s3330_d14_u
C6288.blif_0.10_1.00_0_0_inp_exact
s1196_d4_u
C6288.blif_0.10_0.20_0_0_out_exact
uclid-pipe3b
adder-10-sat
b20_C_3_2
k_ph_p-11
C5315.blif_0.10_0.20_0_1_inp_exact

Formulas only solved by one solver

FORMULA	SOLVER
adder-12-unsat	nenofex
adder-14-unsat	nenofex
adder-16-unsat	nenofex
audio_ac97_wavepcistream3.cpp	rareqs-1.1
biu.mv.xl_ao.bb-b003-p020-IPF01-c05.blif-biu.inv.prop.bb-bmc.with-IOC.unfold-009	rareqs-1.1
blocks_enc_2_b4_ser--opt-26_	rareqs-1.1
c4_Debug_s3_f1_e1_v3	nenofex
c4_Debug_s3_f1_e2_v3	nenofex
c4_Debug_s3_f2_e1_v3	nenofex
C880.blif_0.10_1.00_0_0_out_exact	rareqs-1.1
connect_6x5_5_R	ooq
emptyroom_e4_par--opt-22_	rareqs-1.1
emptyroom_e4_ser--opt-44_	rareqs-1.1
filesys_fastfat_allocsup.c	rareqs-1.1
ring_r6_ser--opt-17_	ooq
ring_r7_ser---19_	rareqs-1.1
s298_d13_s	dual_ooq
s298_d16_s	dual_ooq
s298_d22_u	dual_ooq
s298_d24_u	dual_ooq
s3330_d6_s	dual_ooq
s499_d15_s	dual_ooq
s510_d26_s	dual_ooq
s510_d33_s	dual_ooq
s641_d7_u	dual_ooq
s713_d5_s	dual_ooq
s820_d6_s	dual_ooq
s820_d8_s	dual_ooq

Formulas with Discrepancies

Formulas with Discrepancies

FORMULA

SAT

UNSAT