AABBCCDD_eval12

Overview

Overall Solving Statistics

SOLVERSATUNSATTOTAL
rareqs-1.1573592
depqbf-lazy-qup523890
depqbf503787
ooq493079
hiqqer3453378
dual_ooq482674
ghost-cegar.sh461864
ghost-bq-cegar.sh461864
ghost-plain.sh431457
pre_dual_ooq.py371754
nenofex321648
squeezebf1.2-qube3.0331346
Number of Solved Formulas

solverAVERAGESUM
rareqs-1.1560.16131079.63
depqbf-lazy-qup587.38137448.88
depqbf601.83140829.59
ooq623.11145808.53
hiqqer3631.10147679.35
dual_ooq639.98149756.79
ghost-cegar.sh687.91160973.10
ghost-bq-cegar.sh688.76161169.88
ghost-plain.sh701.10164058.16
pre_dual_ooq.py716.23167599.82
nenofex727.68170278.29
squeezebf1.2-qube3.0740.40173255.93
Time Statistics (overall runtime, average runtime)

formula
k12_4_2
filesys_fastfat_allocsup.c
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
blocks_enc_2_b4_ser--opt-26_
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
k_ph_p-18
b22_PR_8_20
cmu.periodic.N-f4
b04_C_2_20
s38584_3_238
k_ph_p-12
test1_quant3
s3330_d11_u
test1_quant2
filesys_cdfs_namesup.c
k_ph_p-16
vis.prodcell^24.E-f3
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
stmt47_340_389
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
test3_quant_squaring4
b22_C_2_12
ring_r7_ser--opt-20_
eijk.S382.S-f4
filesys_smbmrx_smbxchng.c
k6_4_3
audio_ac97_wavepcistream3.cpp
b21_C_3_206
b14_C_3_105
k12_2_2
adder-12-sat
s3330_d10_u
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
ethernet-fixpoint-3
k14_3_3
s1269_d13_u
nusmv.tcas^4.B-f3
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
Number of Unsolved Formulas (solved by no solver)

FORMULASOLVER
adder-12-unsatnenofex
adder-14-unsatnenofex
adder-16-unsatnenofex
biu.mv.xl_ao.bb-b001-p010-MIF05-c04.blif-biu.inv1.prop.bb-bmc.with-IOC.unfold-004rareqs-1.1
biu.mv.xl_ao.bb-b003-p020-IPF01-c05.blif-biu.inv.prop.bb-bmc.with-IOC.unfold-009rareqs-1.1
c4_Debug_s3_f1_e1_v3nenofex
c4_Debug_s3_f1_e2_v3nenofex
c4_Debug_s3_f2_e1_v3nenofex
C6288.blif_0.10_1.00_0_1_inp_exactrareqs-1.1
C6288.blif_0.10_1.00_0_1_out_exactrareqs-1.1
C880.blif_0.10_1.00_0_0_out_exactrareqs-1.1
connect_6x5_5_Rsqueezebf1.2-qube3.0
emptyroom_e4_ser--opt-44_rareqs-1.1
ken.flash^14.C-d4rareqs-1.1
ring_r6_ser--opt-17_ooq
ring_r7_ser---19_rareqs-1.1
s1196_d3_udual_ooq
s1196_d5_udual_ooq
s1196_d6_udual_ooq
s1196_d7_udual_ooq
s298_d16_sdual_ooq
s298_d22_udual_ooq
s298_d24_udual_ooq
s3330_d6_sdual_ooq
s510_d33_sdual_ooq
s820_d6_sdual_ooq
s820_d7_sdual_ooq
sortnetsort10.AE.stepl.010depqbf-lazy-qup
stmt17_70_82rareqs-1.1
stmt17_74_78rareqs-1.1
stmt31_276_328ooq
stmt47_290_340ooq
test4_quant_squaring2ooq
Umbrella_tbm_05.tex.module.000011depqbf-lazy-qup
Formulas only solved by one solver

Formulas with Discrepancies

FORMULASATUNSAT
Formulas with Discrepancies