eval12

Overview

Overall Solving Statistics

SOLVERSATUNSATTOTAL
ghost-bq-cegar.sh11199210
ghost-cegar.sh10391194
hiqqer39389182
ghost-plain.sh8785172
pre_dual_ooq.py8089169
dual_ooq6677143
squeezebf1.2-qube3.06067127
depqbf-lazy-qup4364107
depqbf4263105
ooq346498
rareqs-1.1346397
nenofex344377
Number of Solved Formulas

solverAVERAGESUM
ghost-bq-cegar.sh382.63132008.34
ghost-cegar.sh424.93146601.03
hiqqer3452.31156048.76
ghost-plain.sh476.01164225.79
pre_dual_ooq.py490.20169122.06
dual_ooq550.99190092.10
squeezebf1.2-qube3.0602.81207970.77
depqbf-lazy-qup640.29220901.81
depqbf648.33223676.21
rareqs-1.1661.07228069.71
ooq662.31228499.66
nenofex710.84245243.01
Time Statistics (overall runtime, average runtime)

formula
k12_4_2
filesys_fastfat_allocsup.c
test4_quant_squaring4
test4_quant4
s1269_d15_u
k12_3_3
connect_7x6_4_R
test1_quant_squaring3
k_branch_n-20
blocks_enc_2_b4_ser--opt-26_
connect_9x8_3_R
s3330_d13_u
k_ph_p-17
c4_Debug_s3_f2_e1_v3
c2_Debug_s5_f1_e1_v3
k_ph_p-18
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
ev-pr-6x6-5-5-0-1-2-s
C5315.blif_0.10_0.20_0_1_out_exact
audio_ddksynth_voice.cpp
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
C6288.blif_0.10_0.20_0_1_inp_exact
k_branch_n-21
C5315.blif_0.10_0.20_0_0_inp_exact
test3_quant_squaring4
sortnetsort10.AE.stepl.010
b22_C_2_12
ring_r7_ser--opt-20_
ev-pr-6x6-7-5-0-1-2-s
filesys_smbmrx_smbxchng.c
k6_4_3
audio_ac97_wavepcistream3.cpp
b21_C_3_206
b14_C_3_105
k12_2_2
s3330_d10_u
k12_2_3
k_branch_n-14
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
s3330_d14_u
sortnetsort10.AE.stepl.008
C6288.blif_0.10_1.00_0_0_inp_exact
C6288.blif_0.10_0.20_0_0_out_exact
b20_C_3_2
Number of Unsolved Formulas (solved by no solver)

FORMULASOLVER
adder-10-satnenofex
adder-12-satnenofex
adder-12-unsatnenofex
adder-14-unsatnenofex
adder-16-unsatnenofex
AR-fixpoint-2squeezebf1.2-qube3.0
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
C880.blif_0.10_0.20_0_0_inp_exactghost-plain.sh
C880.blif_0.10_0.20_0_1_inp_exactghost-plain.sh
cache-coherence-2-fixpoint-5squeezebf1.2-qube3.0
counter_32hiqqer3
counter_e_8nenofex
cube_c11_ser--opt-42_rareqs-1.1
cube_c7_ser---23_rareqs-1.1
emptyroom_e4_ser--opt-44_rareqs-1.1
ethernet-fixpoint-3squeezebf1.2-qube3.0
k_branch_n-10hiqqer3
k_branch_p-10hiqqer3
k_branch_p-13hiqqer3
k_branch_p-15hiqqer3
k_branch_p-21hiqqer3
ring_r6_ser--opt-17_rareqs-1.1
ring_r7_ser---19_rareqs-1.1
stmt31_276_328pre_dual_ooq.py
stmt41_286_385pre_dual_ooq.py
stmt47_290_340pre_dual_ooq.py
stmt47_340_389pre_dual_ooq.py
test4_quant_squaring2pre_dual_ooq.py
Formulas only solved by one solver

sqube bghostc dooqm rareqs ghostc hiqqer ghost depqbfm nenofexm sdooq ooqm ldepqbf
Abduction (6) 6 6 6 6 6 6 6 6 2 6 6 6
Adder (6) 0 0 0 0 0 1 0 0 6 0 0 0
blackbox-01X-QBF (6) 4 3 4 6 3 4 4 5 1 4 5 5
blackbox_design (6) 6 6 6 1 6 5 6 1 0 6 1 1
Blocks (2) 0 2 2 2 2 2 1 1 2 2 2 1
BMC (6) 2 4 4 6 4 6 3 5 5 4 4 6
BooM-NP (11) 2 5 6 1 5 6 5 5 1 6 6 4
BooM-P (12) 2 5 6 1 5 6 5 5 1 6 6 4
C432 (3) 0 3 1 3 3 1 3 1 1 1 1 1
C499 (4) 0 1 0 1 1 1 1 0 1 0 0 0
C5315 (6) 1 3 1 2 3 1 3 1 2 1 1 1
C6288 (6) 1 2 1 0 2 0 2 0 0 2 0 0
C880 (6) 0 4 0 2 4 0 6 0 0 0 0 0
circuits (6) 0 0 0 0 0 0 0 0 0 0 0 0
conformant_planning (16) 2 9 5 14 9 5 4 5 9 5 5 4
Connect4 (4) 1 1 1 0 1 1 1 1 0 1 1 1
Counter (4) 1 2 2 0 2 3 2 2 3 2 2 2
Debug (5) 0 0 0 0 0 0 0 0 2 0 0 0
evader-pursuer-4x4-logarithmic (2) 1 2 1 1 2 2 2 1 0 1 2 1
evader-pursuer-4x4-standard (6) 6 0 0 0 0 2 0 0 0 6 0 0
evader-pursuer-6x6-logarithmic (4) 1 1 2 2 1 2 2 4 0 1 3 4
evader-pursuer-6x6-standard (2) 0 0 0 0 0 0 0 0 0 0 0 0
evader-pursuer-8x8-logarithmic (6) 3 2 3 3 2 4 3 5 0 3 5 5
FPGA_PLB_FIT_FAST (1) 0 1 1 1 1 1 1 1 1 1 1 1
FPGA_PLB_FIT_SLOW (1) 0 1 1 1 1 1 0 1 1 1 1 1
fpu (6) 6 6 6 6 6 6 6 6 6 6 6 6
Hardware-Fix-Point (6) 5 3 0 0 0 3 0 0 1 2 0 0
incremental-encoder (6) 4 6 4 6 6 5 4 4 2 4 4 4
irqlkeapclte (6) 0 6 0 0 6 0 0 0 0 0 0 0
jmc_quant (6) 2 0 0 0 0 2 0 0 1 2 0 0
jmc_quant_squaring (6) 0 0 0 0 0 0 0 0 0 1 0 0
k_branch_n (6) 0 2 0 0 0 3 1 0 0 0 0 0
k_branch_p (6) 0 2 1 0 1 6 2 0 0 1 0 0
k_d4_n (6) 0 6 0 0 6 6 6 0 0 0 0 0
k_d4_p (6) 0 6 6 0 6 6 6 0 1 6 6 0
k_dum_n (6) 0 6 0 0 6 6 6 0 6 3 0 0
k_dum_p (6) 3 6 6 0 6 6 6 2 6 6 6 2
k_ph_n (6) 6 3 6 6 3 6 1 6 0 6 6 6
k_ph_p (6) 1 2 0 0 2 0 2 0 2 0 0 0
Lights3_021_qdgz (6) 5 6 6 3 6 6 6 6 1 6 5 6
Lights3_035_qdgz (6) 4 6 5 3 6 6 6 5 2 5 5 5
mqm (18) 12 8 16 0 8 18 0 18 0 17 1 18
RankingFunctions (12) 6 6 0 0 1 6 1 0 0 6 0 0
s1196 (6) 1 6 1 0 6 1 6 0 0 1 0 0
s1269 (6) 1 3 1 0 3 1 3 0 0 1 0 0
s298 (6) 1 6 3 0 6 1 6 0 0 2 0 0
s3330 (6) 1 2 1 0 2 1 2 0 0 1 0 0
s386 (1) 1 1 1 0 1 0 1 0 0 1 0 0
s499 (1) 1 1 1 0 1 0 1 0 0 0 0 0
s510 (3) 1 3 1 0 3 1 3 0 0 1 0 0
s641 (3) 2 3 3 0 3 1 3 0 0 3 0 0
s713 (3) 3 3 3 0 3 3 3 0 0 3 0 0
s820 (3) 3 3 3 0 3 0 3 0 0 3 0 0
sauer_reimer (6) 2 6 2 2 6 4 5 1 0 2 2 1
Sorting_networks (6) 0 2 1 4 2 1 3 3 4 0 1 4
SzymanskiP (6) 6 5 6 5 0 6 0 0 0 6 4 0
terminator (6) 0 1 1 0 1 0 2 0 0 6 0 0
tipdiam (3) 2 3 2 0 3 1 3 0 0 2 0 0
tipfixpoint (9) 2 9 5 1 9 1 9 1 0 2 1 1
Toilet (4) 2 4 3 4 4 3 4 3 4 3 3 4
trafficlight-controller (6) 4 3 2 5 3 6 3 5 4 6 2 6
uclid (3) 0 2 0 0 2 0 2 0 0 0 0 0
wmiforward (6) 3 6 0 0 6 6 2 0 0 2 0 0
total (356) 129 215 149 98 199 188 177 110 78 175 104 111
eval12

sqube bghostc dooqm rareqs ghostc hiqqer ghost depqbfm nenofexm sdooq ooqm ldepqbf
Ansotegui (20) 11 5 6 6 5 10 7 10 0 11 10 10
Ayari (12) 6 5 6 5 0 7 0 0 6 6 4 0
Basler (18) 3 13 1 0 13 6 4 0 0 8 0 0
Biere (16) 5 14 9 1 14 5 14 3 3 6 3 3
gelder (12) 9 12 11 6 12 12 12 11 3 11 10 11
Gent-Rowley (4) 1 1 1 0 1 1 1 1 0 1 1 1
Herbstritt (12) 10 9 10 7 9 9 10 6 1 10 6 6
jiang (12) 2 5 6 1 5 6 5 5 1 6 6 4
Katz (12) 2 0 0 0 0 2 0 0 1 3 0 0
Kontchakov (18) 12 8 16 0 8 18 0 18 0 17 1 18
Lahiri-Seshia (3) 0 2 0 0 2 0 2 0 0 0 0 0
Letombe (6) 6 6 6 6 6 6 6 6 2 6 6 6
Ling (2) 0 2 2 2 2 2 1 2 2 2 2 2
Mangassarian-Veneris (11) 2 4 4 6 4 6 3 5 7 4 4 6
Messinger (6) 0 0 0 0 0 0 0 0 0 0 0 0
Miller-Marin (18) 14 15 12 17 15 17 13 15 12 16 12 16
Mneimneh-Sakallah (38) 15 31 18 0 31 9 31 0 0 16 0 0
Palacios (16) 2 9 5 14 9 5 4 5 9 5 5 4
Pan (48) 10 33 19 6 30 39 30 8 15 22 18 8
Rintanen (12) 2 8 6 10 8 6 8 7 10 5 6 9
sauer_reimer (6) 2 6 2 2 6 4 5 1 0 2 2 1
Scholl-Becker (25) 2 13 3 8 13 3 15 2 4 4 2 2
Wintersteiger (18) 11 9 0 0 1 9 1 0 1 8 0 0
total (345) 127 210 143 97 194 182 172 105 77 169 98 107
eval12

Formulas with Discrepancies

FORMULASATUNSAT
Formulas with Discrepancies