eval12_bloqqer_pp

Overview

Overall Solving Statistics

SOLVERSATUNSATTOTAL
rareqs-1.16666132
depqbf-lazy-qup6661127
depqbf6659125
hiqqer35959118
ooq5853111
dual_ooq5749106
pre_dual_ooq.py544397
ghost-bq-cegar.sh543892
ghost-cegar.sh543892
squeezebf1.2-qube3.0523991
ghost-plain.sh503585
nenofex393473
Number of Solved Formulas

solverAVERAGESUM
rareqs-1.1495.92136874.36
depqbf-lazy-qup511.51141179.31
depqbf517.55142845.07
hiqqer3550.62151971.55
ooq561.67155021.11
dual_ooq576.78159192.00
pre_dual_ooq.py614.07169483.43
ghost-cegar.sh633.00174710.43
ghost-bq-cegar.sh633.22174768.86
squeezebf1.2-qube3.0635.07175279.90
ghost-plain.sh650.10179428.96
nenofex682.43188351.72
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
C880.blif_0.10_0.20_0_1_inp_exact
ken.flash^14.C-d4
stmt17_74_78
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
connect_6x5_5_R
k_ph_p-16
vis.prodcell^24.E-f3
C880.blif_0.10_1.00_0_0_out_exact
cmu.dme1.B-f4
C5315.blif_0.10_0.20_0_1_out_exact
audio_ddksynth_voice.cpp
AR-fixpoint-2
stmt23_92_96
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
cache-coherence-2-fixpoint-5
C6288.blif_0.10_0.20_0_1_inp_exact
k_branch_n-21
C5315.blif_0.10_0.20_0_0_inp_exact
stmt17_94_98
test3_quant_squaring4
b22_C_2_12
ring_r7_ser--opt-20_
ev-pr-6x6-7-5-0-1-2-s
eijk.S382.S-f4
filesys_smbmrx_smbxchng.c
k6_4_3
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
stmt41_160_235
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
stmt17_70_82
s3330_d14_u
C6288.blif_0.10_1.00_0_0_inp_exact
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
audio_ac97_wavepcistream3.cpprareqs-1.1
biu.mv.xl_ao.bb-b001-p010-MIF05-c07.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
c2_Debug_s5_f1_e1_v3nenofex
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
emptyroom_e4_ser--opt-44_rareqs-1.1
ev-pr-6x6-15-5-0-1-2-lgooq
ev-pr-6x6-5-5-0-1-2-shiqqer3
k_branch_p-21hiqqer3
ring_r6_ser--opt-17_nenofex
ring_r7_ser---19_rareqs-1.1
s510_d26_sdual_ooq
s510_d33_sdual_ooq
stmt17_82_86hiqqer3
stmt31_276_328ooq
stmt41_286_385ooq
Formulas only solved by one solver

sqube bghostc dooqm rareqs ghostc hiqqer ghost depqbfm nenofexm sdooq ooqm ldepqbf
Abduction (6) 5 6 6 6 6 6 6 6 1 6 6 6
Adder (6) 0 0 0 0 0 1 0 0 4 0 0 0
blackbox-01X-QBF (5) 2 0 3 5 0 3 0 4 0 3 3 4
blackbox_design (6) 5 0 4 6 0 5 0 5 0 3 5 5
Blocks (2) 0 2 2 2 2 2 2 2 2 1 2 2
BMC (5) 3 2 4 5 2 5 3 5 5 4 4 5
BooM-NP (11) 3 6 6 5 6 6 6 4 2 6 6 6
BooM-P (12) 3 6 6 5 6 6 6 4 2 6 6 6
C432 (3) 1 3 1 3 3 1 3 3 3 1 1 3
C499 (4) 0 1 2 1 1 2 1 2 1 1 2 2
C5315 (6) 0 2 1 2 2 1 1 1 2 1 1 1
C6288 (6) 0 0 0 2 0 0 0 0 0 0 0 0
C880 (6) 0 0 0 1 0 1 0 0 0 0 0 0
circuits (6) 0 0 0 0 0 0 0 0 0 0 0 0
conformant_planning (16) 2 5 5 11 5 5 5 5 10 5 5 5
Connect4 (4) 1 1 1 0 1 1 1 1 0 1 1 1
Counter (3) 1 1 2 3 1 2 2 2 3 2 2 2
Debug (5) 0 0 0 0 0 0 0 0 4 0 0 0
evader-pursuer-4x4-logarithmic (2) 2 2 1 2 2 2 2 2 0 2 1 2
evader-pursuer-4x4-standard (6) 6 5 0 0 5 3 6 3 0 1 3 3
evader-pursuer-6x6-logarithmic (4) 1 1 2 2 1 3 1 3 1 1 4 3
evader-pursuer-6x6-standard (2) 0 0 0 0 0 1 0 0 0 0 0 0
evader-pursuer-8x8-logarithmic (6) 3 1 3 3 1 5 2 4 1 3 5 4
FPGA_PLB_FIT_FAST (1) 1 1 1 1 1 1 1 1 1 1 1 1
FPGA_PLB_FIT_SLOW (1) 1 1 1 1 1 1 1 1 1 1 1 1
Hardware-Fix-Point (3) 0 0 0 0 0 0 0 0 0 0 0 0
incremental-encoder (5) 3 5 3 5 5 4 3 3 2 3 3 3
irqlkeapclte (6) 0 0 0 0 0 1 0 0 0 0 0 0
jmc_quant (6) 1 1 2 0 1 2 2 2 1 2 2 2
jmc_quant_squaring (6) 0 0 1 0 0 0 0 1 0 1 0 1
k_branch_n (4) 2 0 0 1 0 2 1 1 0 0 0 1
k_branch_p (4) 3 1 0 3 1 4 1 3 0 0 1 2
k_ph_n (6) 6 5 6 6 5 6 5 6 6 6 6 6
k_ph_p (6) 0 0 0 1 0 0 0 0 1 0 0 0
Lights3_021_qdgz (3) 3 3 3 3 3 3 3 3 3 3 3 3
Lights3_035_qdgz (3) 3 3 3 3 3 3 3 3 3 3 3 3
mqm (18) 9 2 2 1 2 12 3 18 0 1 1 18
RankingFunctions (6) 0 0 0 1 0 0 0 0 0 0 0 0
s1196 (6) 1 1 6 6 1 1 1 1 1 4 1 1
s1269 (6) 1 1 3 2 1 1 1 1 1 2 1 1
s298 (6) 3 2 6 6 2 1 1 3 0 5 5 2
s3330 (5) 0 0 1 0 0 0 0 0 0 1 0 0
s386 (1) 0 1 1 1 1 0 0 1 0 1 1 1
s499 (1) 0 1 1 1 1 1 0 1 0 1 1 0
s510 (3) 1 1 3 1 1 1 1 1 1 1 1 1
s641 (3) 3 2 3 3 2 1 1 2 0 3 3 3
s713 (3) 3 3 3 3 3 3 1 3 0 3 3 3
s820 (3) 2 2 3 3 2 0 0 3 0 3 3 3
sauer_reimer (4) 2 3 2 2 3 2 3 2 0 2 2 2
Sorting_networks (6) 0 3 0 4 3 2 1 2 4 0 1 3
terminator (6) 0 0 0 3 0 0 0 0 0 0 5 0
tipdiam (3) 1 2 1 2 2 1 1 1 0 1 2 2
tipfixpoint (8) 0 0 0 0 0 0 0 0 0 0 0 0
Toilet (4) 2 4 2 4 4 4 4 4 4 2 4 4
trafficlight-controller (6) 5 6 6 6 6 6 6 6 5 6 6 6
uclid (3) 0 0 0 0 0 0 0 0 0 0 0 0
total (287) 94 98 112 137 98 124 91 129 75 103 117 133
eval12_bloqqer_pp

sqube bghostc dooqm rareqs ghostc hiqqer ghost depqbfm nenofexm sdooq ooqm ldepqbf
Ansotegui (20) 12 9 6 7 9 14 11 12 2 7 13 12
Ayari (6) 0 0 0 0 0 1 0 0 4 0 0 0
Basler (12) 0 0 0 3 0 1 0 0 0 0 5 0
Biere (14) 2 3 3 5 3 3 3 3 3 3 4 4
gelder (6) 6 6 6 6 6 6 6 6 6 6 6 6
Gent-Rowley (4) 1 1 1 0 1 1 1 1 0 1 1 1
Herbstritt (11) 7 0 7 11 0 8 0 9 0 6 8 9
jiang (12) 3 6 6 5 6 6 6 4 2 6 6 6
Katz (12) 1 1 3 0 1 2 2 3 1 3 2 3
Kontchakov (18) 9 2 2 1 2 12 3 18 0 1 1 18
Lahiri-Seshia (3) 0 0 0 0 0 0 0 0 0 0 0 0
Letombe (6) 5 6 6 6 6 6 6 6 1 6 6 6
Ling (2) 2 2 2 2 2 2 2 2 2 2 2 2
Mangassarian-Veneris (10) 3 2 4 5 2 5 3 5 9 4 4 5
Messinger (6) 0 0 0 0 0 0 0 0 0 0 0 0
Miller-Marin (11) 8 11 9 11 11 10 9 9 7 9 9 9
Mneimneh-Sakallah (37) 14 14 30 26 14 9 6 16 3 24 19 15
Palacios (16) 2 5 5 11 5 5 5 5 10 5 5 5
Pan (20) 11 6 6 11 6 12 7 10 7 6 7 9
Rintanen (12) 2 9 4 10 9 8 7 8 10 3 7 9
sauer_reimer (4) 2 3 2 2 3 2 3 2 0 2 2 2
Scholl-Becker (25) 1 6 4 9 6 5 5 6 6 3 4 6
Wintersteiger (9) 0 0 0 1 0 0 0 0 0 0 0 0
total (276) 91 92 106 132 92 118 85 125 73 97 111 127
eval12_bloqqer_pp

Formulas with Discrepancies

FORMULASATUNSAT
Formulas with Discrepancies