Instances solved by ASPQ_2018
QBFEVAL'18 - Prenex 2QBF Track

InstanceResultTime
driver_d9y.satSAT0
decomposition256SAT0
itc-b13-fixpoint-1UNSAT0
floor256SAT0
rankfunc56_unsigned_64SAT0
kenflashp12SAT0
stmt124_966_965SAT0
rankfunc53_signed_64SAT0
pdtpmsmiimSAT0
stmt5_731_730SAT0
rankfunc61_unsigned_64SAT0
stmt41_262_275SAT0
pdtpmsrotate32SAT0
kenflashp04SAT0
ceiling256SAT0
floor128SAT0
ceiling128SAT0
rankfunc60_unsigned_32SAT0
small-synabs-fixpoint-3UNSAT0
small-swap1-fixpoint-5SAT0
add20y.satSAT0
rankfunc56_signed_64SAT0
small-swap1-fixpoint-6SAT0
driver_c9y.satSAT0
bobtuint31negSAT0
stmt9_445_446SAT0
rankfunc48_unsigned_16SAT0
stmt16_818_819SAT0
stmt25_597_598SAT0
stmt44_554_604SAT0
rankfunc53_unsigned_64SAT0
decomposition128SAT0
Q_2-3_v-80-100_r-13.3UNSAT0.05
Q_2-3_v-80-100_r-13.9UNSAT0.05
Q_2-3_v-80-100_r-13.0UNSAT0.05
Q_2-3_v-80-100_r-13.4UNSAT0.06
stmt25_52_53SAT0.51
itc-b13-fixpoint-2UNSAT0.52
stmt1_79_80SAT0.53
usb-phy-fixpoint-1UNSAT0.54
rankfunc51_unsigned_64SAT0.6
rankfunc51_signed_64SAT0.6
driver_c9n.satSAT0.61
small-seq-fixpoint-1UNSAT0.61
stmt27_93_98SAT0.61
small-swap1-fixpoint-4SAT0.62
eijkbs4863SAT0.63
rankfunc54_unsigned_64SAT0.66
Q_2-3_v-80-100_r-13.2UNSAT0.66
rankfunc54_signed_64SAT0.66
nxquery_query42_1344nUNSAT0.73
cycle_sched_12_2_1.satSAT0.73
small-pipeline-fixpoint-1UNSAT0.77
exquery_query42_1344nUNSAT0.82
rankfunc52_unsigned_64SAT0.83
small-swap1-fixpoint-7SAT0.84
axquery_query42_1344nUNSAT0.84
rankfunc61_signed_64SAT0.85
rankfunc52_signed_64SAT0.86
rankfunc58_unsigned_64SAT0.86
rankfunc58_signed_64SAT0.89
small-synabs-fixpoint-10UNSAT0.9
small-swap1-fixpoint-8SAT0.98
rankfunc31_unsigned_64SAT1.07
itc-b13-fixpoint-3SAT1.07
rankfunc55_unsigned_64SAT1.08
rankfunc59_signed_64SAT1.08
rankfunc31_signed_64SAT1.08
query02_query42_1344nUNSAT1.11
rankfunc59_unsigned_64SAT1.12
rankfunc41_signed_64SAT1.12
rankfunc41_unsigned_64SAT1.14
ethernet-fixpoint-1UNSAT1.14
query04_query25_1344nSAT1.19
ltl2dba_C2-6_comp3_REAL.satSAT1.2
rankfunc49_signed_64SAT1.24
rankfunc35_unsigned_64SAT1.26
rankfunc49_unsigned_64SAT1.28
Q_2-3_v-80-100_r-13.5UNSAT1.44
query26_query42_1344nUNSAT1.44
query27_query42_1344nUNSAT1.44
trivial_query42_1344nUNSAT1.45
small-swap1-fixpoint-9SAT1.47
ntrivil_query42_1344nUNSAT1.5
small-swap1-fixpoint-10SAT1.52
query52_query25_1344nSAT1.66
driver_a10y.satSAT1.67
itc-b13-fixpoint-4SAT1.68
rankfunc57_unsigned_64SAT1.71
rankfunc2_unsigned_64SAT1.75
driver_b8n.satSAT1.79
query36_query25_1344nSAT1.93
query31_eequery_1344nSAT1.96
mult_bool_matrix_dyn_9_5.satSAT1.98
stmt21_181_218UNSAT2.28
bs128n.satSAT2.39
bs128y.satSAT2.39
driver_a9n.satSAT2.4
itc-b13-fixpoint-5SAT2.41
stmt53_208_245UNSAT2.41
cache-coherence-3-fixpoint-1UNSAT2.46
usb-phy-fixpoint-2UNSAT2.5
rankfunc48_unsigned_64SAT2.61
ltl2dba_C2-8_comp4_REAL.satSAT2.69
query07_query42_1344nUNSAT2.75
rankfunc35_signed_64SAT2.78
query02_query44_1344nUNSAT2.9
Q_2-3_v-80-100_r-13.7UNSAT2.94
cache-coherence-2-fixpoint-2UNSAT3.02
stmt19_66_214UNSAT3.33
Q_2-3_v-80-100_r-13.1UNSAT3.35
sortnetsort7.AE.stepl.007UNSAT3.44
itc-b13-fixpoint-6SAT3.48
sortnetsort8.AE.stepl.004SAT3.6
sortnetsort7.AE.stepl.006UNSAT3.86
ctrl.e#1.a#3.E#112.A#48.c#.w#5.s#27.aspSAT3.86
ltl2dpa_C26_comp2_REAL.satSAT3.92
cycle_sched_4_4_2.satSAT3.92
query21_query42_1344nUNSAT3.94
stmt23_66_67SAT4.1
usb-phy-fixpoint-3UNSAT4.13
stmt22_320_370SAT4.18
ethernet-fixpoint-2UNSAT4.37
stmt17_63_70SAT4.47
itc-b13-fixpoint-7SAT4.68
sortnetsort7.AE.stepl.008UNSAT4.72
sortnetsort7.AE.stepl.009UNSAT4.84
stay24n.satSAT5.01
stmt21_354_403SAT5.07
ci.e#1.a#3.E#40.A#60.c#288.w#6.s#2.aspSAT5.14
nxquery_query50_1344nSAT5.59
itc-b13-fixpoint-8SAT5.89
cache-coherence-3-fixpoint-2UNSAT6.01
ctrl.e#1.a#3.E#110.A#48.c#.w#9.s#13.aspSAT6.26
stmt19_64_87SAT6.29
ctrl.e#1.a#3.E#128.A#48.c#.w#7.s#1.aspSAT6.38
ctrl.e#1.a#3.E#116.A#48.c#.w#7.s#56.aspSAT6.85
cache-coherence-2-fixpoint-4UNSAT6.95
stmt27_16_224UNSAT6.97
ci.e#1.a#3.E#40.A#60.c#416.w#2.s#3.aspUNSAT7.02
itc-b13-fixpoint-9SAT7.06
stmt22_6_414UNSAT7.18
query03_query42_1344nUNSAT7.3
query21_query58_1344nUNSAT7.37
mult_bool_matrix_10_9_11.satSAT7.4
ctrl.e#1.a#3.E#120.A#48.c#.w#3.s#3.aspSAT7.86
sortnetsort8.AE.stepl.006UNSAT7.89
sortnetsort9.AE.stepl.004SAT8.49
query49_ntrivil_1344nSAT8.6
stmt19_352_359UNSAT8.89
stmt19_137_408UNSAT9.13
itc-b13-fixpoint-10SAT9.14
GuidanceServiceUNSAT9.26
GuidanceService2UNSAT9.4
cache-coherence-3-fixpoint-3UNSAT9.66
cycle_sched_2_10_1.satSAT9.66
ctrl.e#1.a#3.E#128.A#48.c#.w#3.s#26.aspSAT10.58
cache-coherence-2-fixpoint-5UNSAT10.82
query04_query42_1344nUNSAT11.34
stmt19_90_408UNSAT11.67
load_2c_comp_comp7_REAL.satSAT12.24
query08_query42_1344nUNSAT12.25
stmt21_84_364UNSAT12.3
ctrl.e#1.a#3.E#128.A#48.c#.w#9.s#60.aspSAT12.91
query09_query42_1344nUNSAT13.25
cache-coherence-2-fixpoint-6UNSAT14.11
sortnetsort10.AE.stepl.004SAT14.47
stmt22_311_370UNSAT14.66
stmt39_285_335UNSAT15.29
sortnetsort8.AE.stepl.008UNSAT15.85
query48_exquery_1344nSAT16.05
ctrl.e#1.a#3.E#118.A#48.c#.w#5.s#7.aspSAT17.25
stmt19_133_217UNSAT17.66
query33_query45_1344nSAT17.85
query31_query50_1344nSAT18.16
ctrl.e#1.a#3.E#128.A#48.c#.w#7.s#60.aspSAT18.28
query50_query42_1344nSAT18.37
pi-bus-fixpoint-1UNSAT18.79
Q_2-3_v-80-100_r-13.8UNSAT19.08
stmt2_976_999SAT20.49
sortnetsort8.AE.stepl.005SAT21.89
mult_bool_matrix_12_13_11.satSAT22.5
stmt21_178_258UNSAT23.11
eequery_query64_1344nSAT23.29
query06_query42_1344nUNSAT24.2
amba2c7n.satSAT24.42
Q_2-3_v-80-100_r-13.6UNSAT26.05
stmt29_226_376UNSAT28
query05_query31_1344nSAT28.58
sortnetsort8.AE.stepl.009UNSAT28.64
query25_query42_1344nSAT29.98
stmt21_143_403UNSAT34.81
stmt41_286_385UNSAT34.84
stmt41_160_235UNSAT35.66
sortnetsort9.AE.stepl.005SAT36.81
ci.e#1.a#3.E#40.A#60.c#400.w#2.s#1.aspUNSAT37.27
cycle_sched_4_7_1.satSAT40.46
cycle_sched_6_6_2.satSAT42.45
stmt31_22_328UNSAT45.18
stmt19_313_412UNSAT45.37
stmt47_340_389UNSAT46.51
sortnetsort9.AE.stepl.007UNSAT48.67
query55_query42_1344nSAT54.97
sortnetsort9.AE.stepl.008UNSAT61.95
stmt21_310_360UNSAT75.83
sortnetsort9.AE.stepl.009UNSAT78.6
query60_query45_1344nSAT81.76
ctrl.e#1.a#3.E#128.A#48.c#.w#7.s#7.aspSAT88.69
query50_query06_1344nSAT96.57
stmt46_111_238UNSAT101.23
amba2f9n.satSAT102.65
eequery_query42_1344nSAT122.48
sortnetsort9.AE.stepl.011UNSAT124.25
query54_query42_1344nSAT128.26
sortnetsort9.AE.stepl.012UNSAT131.3
query51_query42_1344nSAT136.21
stmt47_290_340UNSAT142.26
stmt53_296_346UNSAT146.8
query45_query42_1344nSAT161.66
usb-phy-fixpoint-4UNSAT165.17
query33_query51_1344nSAT166.5
sortnetsort9.AE.stepl.010UNSAT166.57
query33_query57_1344nSAT172.62
sortnetsort10.AE.stepl.010UNSAT174.24
query51_query57_1344nSAT182.37
ctrl.e#1.a#3.E#128.A#48.c#.w#9.s#1.aspSAT187.57
query54_query58_1344nSAT215.82
stmt19_3_401UNSAT219.87
mult9.satSAT257.96
query34_query11_1344nSAT265.53
sortnetsort10.AE.stepl.011UNSAT271.75
query31_query42_1344nSAT278.15
sortnetsort10.AE.stepl.009UNSAT301.1
ci.e#1.a#3.E#40.A#60.c#408.w#2.s#2.aspUNSAT301.45
ctrl.e#1.a#3.E#128.A#48.c#.w#5.s#60.aspSAT308.04
query52_query42_1344nSAT311.67
query05_query42_1344nSAT320.39
query31_reachqu_1344nSAT330.98
sortnetsort7.AE.stepl.005SAT331.86
query33_query42_1344nSAT398.39
ctrl.e#1.a#3.E#134.A#48.c#.w#9.s#40.aspSAT404.14
sortnetsort10.AE.stepl.008UNSAT423.06
query42_query42_1344nUNSAT427.26
sortnetsort10.AE.stepl.012UNSAT442.75
query11_query42_1344nSAT496.18
Q_2-3_v-80-100_r-11.8UNSAT498.22
stmt31_276_328UNSAT503.79
stmt21_71_354UNSAT547.67
stmt27_149_224UNSAT548.78
query64_query01_1344nSAT560.43
ci.e#1.a#3.E#40.A#60.c#408.w#2.s#1.aspUNSAT639.37
stmt41_336_385UNSAT641.69
stmt21_181_369UNSAT646.93
query10_query45_1344nSAT657.88
query64_query11_1344nSAT702.07
stmt46_289_388UNSAT717.86
query36_query42_1344nSAT791.56
stmt21_70_369UNSAT846.31
query01_query42_1344nFAIL900
sdlx-fixpoint-4FAIL900
rankfunc48_signed_64FAIL900
small-equiv-fixpoint-4FAIL900
stmt19_65_95FAIL900
query42_query45_1344nFAIL900
stmt50_343_392FAIL900
stmt17_63_82FAIL900
query10_query42_1344nFAIL900.01
sdlx-fixpoint-9FAIL900.01
stmt28_68_73FAIL900.01
query34_query42_1344nFAIL900.01
AR-fixpoint-10FAIL900.01
stmt17_82_86FAIL900.01
stmt17_70_90FAIL900.01
stmt29_275_376FAIL900.01
reachqu_query42_1344nFAIL900.01
reachqu_query64_1344nFAIL900.01
NotificationServiceImpl2FAIL900.01
mult_bool_matrix_17_17_17.satFAIL900.01
stmt19_79_83FAIL900.01
beemldelec4b1_c0to127.satFAIL900.01
cycle_sched_6_7_1.satFAIL900.01
UserServiceImplFAIL900.01
neclaftp4001FAIL900.01
stmt17_78_90FAIL900.01
sdlx-fixpoint-8FAIL900.01
IterationServiceFAIL900.01
sortnetsort10.AE.stepl.005FAIL900.01
Q_2-3_v-80-100_r-11.7FAIL900.01
small-seq-fixpoint-2FAIL900.01
Q_2-3_v-80-100_r-11.4FAIL900.01
Q_2-3_v-80-100_r-11.3FAIL900.01
stmt21_319_418FAIL900.01
stmt17_94_98FAIL900.02
sdlx-fixpoint-10FAIL900.02
Q_2-3_v-80-100_r-11.1FAIL900.02
query44_query26_1344nFAIL900.02
stmt23_72_76FAIL900.02
pi-bus-fixpoint-3FAIL900.02
stmt28_73_97FAIL900.02
stmt19_64_91FAIL900.02
stmt17_70_86FAIL900.02
stmt28_89_97FAIL900.02
stmt17_74_90FAIL900.02
AR-fixpoint-2FAIL900.02
sdlx-fixpoint-7FAIL900.02
small-pipeline-fixpoint-3FAIL900.02
reachqu_query71_1344nFAIL900.02
stmt19_368_417FAIL900.03
query60_query44_1344nFAIL900.03
stmt28_68_81FAIL900.03
stmt19_79_87FAIL900.03
stmt21_71_413FAIL900.03
mult_bool_matrix_18_18_18.satFAIL900.03
nreachq_query11_1344nFAIL900.03
Q_2-3_v-80-100_r-11.5FAIL900.03
stmt19_83_91FAIL900.03
stmt17_70_82FAIL900.03
PhaseServiceFAIL900.04
stmt23_67_92FAIL900.04
amba3b5y.satFAIL900.04
genbuf9b4n.satFAIL900.04
sdlx-fixpoint-3FAIL900.04
stmt19_75_83FAIL900.04
stmt28_73_85FAIL900.04
ActivityService2FAIL900.04
stmt23_92_96FAIL900.04
stmt17_78_98FAIL900.04
oski3ub5i_c0to63.satFAIL900.04
intermediate128FAIL900.04
stmt17_82_94FAIL900.04
Q_2-3_v-80-100_r-11.9FAIL900.04
stmt19_302_352FAIL900.04
usb-phy-fixpoint-5FAIL900.04
oski3ub5i_c0to511.satFAIL900.04
AR-fixpoint-1FAIL900.04
neclaftp2002FAIL900.04
small-seq-fixpoint-10FAIL900.04
sdlx-fixpoint-5FAIL900.04
query58_query42_1344nFAIL900.05
stmt17_63_78FAIL900.05
small-equiv-fixpoint-8FAIL900.05
ConcreteActivityServiceFAIL900.05
IssueServiceImplFAIL900.05
AR-fixpoint-4FAIL900.05
stmt17_86_98FAIL900.05
eijkbs3330FAIL900.05
stmt23_88_92FAIL900.05
stmt19_65_87FAIL900.05
sdlx-fixpoint-6FAIL900.05
stmt23_66_96FAIL900.05
AR-fixpoint-8FAIL900.05
pi-bus-fixpoint-2FAIL900.05
query64_query42_1344nFAIL900.05
small-seq-fixpoint-4FAIL900.05
query42_query06_1344nFAIL900.05
small-equiv-fixpoint-1FAIL900.06
small-seq-fixpoint-9FAIL900.06
stmt32_329_378FAIL900.06
AR-fixpoint-6FAIL900.06
small-equiv-fixpoint-5FAIL900.06
intermediate256FAIL900.06
small-seq-fixpoint-8FAIL900.06
stmt85_300_399FAIL900.06
Q_2-3_v-80-100_r-11.6FAIL900.06
Q_2-3_v-80-100_r-11.2FAIL900.06
stmt19_71_95FAIL900.06
stmt17_74_78FAIL900.06
small-pipeline-fixpoint-2FAIL900.06
stmt31_190_227FAIL900.06
ci.e#1.a#3.E#40.A#60.c#384.w#6.s#8.aspFAIL900.06
oski3ub5i_c0to255.satFAIL900.06
query71_query31_1344nFAIL900.06
small-seq-fixpoint-6FAIL900.06
stmt44_40_387FAIL900.06
stmt17_62_98FAIL900.06
stmt17_70_98FAIL900.06
small-seq-fixpoint-5FAIL900.07
stmt52_295_394FAIL900.07
small-equiv-fixpoint-2FAIL900.07
ethernet-fixpoint-3FAIL900.07
stmt19_75_95FAIL900.07
small-equiv-fixpoint-3FAIL900.07
query48_query42_1344nFAIL900.07
6s289rb05233_c0to63.satFAIL900.07
Q_2-3_v-80-100_r-11.0FAIL900.07
stmt19_83_412FAIL900.08
stmt17_78_94FAIL900.08
small-seq-fixpoint-3FAIL900.08
ctrl.e#1.a#3.E#124.A#48.c#.w#7.s#50.aspFAIL900.08
stmt19_64_99FAIL900.09
stmt23_66_76FAIL900.09
stmt17_70_78FAIL900.09
stmt17_62_78FAIL900.09
stmt17_82_98FAIL900.09
ethernet-fixpoint-4FAIL900.09
ActivityServiceFAIL900.1
query71_query36_1344nFAIL900.1
stmt28_68_69FAIL900.1
stmt19_87_95FAIL900.11
small-seq-fixpoint-7FAIL900.11
nreachq_query54_1344nFAIL900.11
beemskbn1f1_c0to7.satFAIL900.23