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

InstanceResultTime
Q_2-3_v-80-100_r-13.9UNSAT0
floor256SAT0
Q_2-3_v-80-100_r-13.5UNSAT0
Q_2-3_v-80-100_r-13.7UNSAT0
kenflashp12SAT0
Q_2-3_v-80-100_r-13.8UNSAT0
axquery_query42_1344nUNSAT0
stmt21_178_258UNSAT0
Q_2-3_v-80-100_r-13.6UNSAT0
nxquery_query42_1344nUNSAT0
small-pipeline-fixpoint-1UNSAT0
query02_query42_1344nUNSAT0
Q_2-3_v-80-100_r-13.4UNSAT0
bobtuint31negSAT0
stmt27_16_224UNSAT0
Q_2-3_v-80-100_r-13.0UNSAT0
floor128SAT0
Q_2-3_v-80-100_r-13.1UNSAT0
Q_2-3_v-80-100_r-13.2UNSAT0
rankfunc60_unsigned_32SAT0
rankfunc48_unsigned_16SAT0
itc-b13-fixpoint-1UNSAT0
kenflashp04SAT0
Q_2-3_v-80-100_r-13.3UNSAT0
decomposition128SAT0
ntrivil_query42_1344nUNSAT0.01
trivial_query42_1344nUNSAT0.01
stmt21_71_354UNSAT0.01
decomposition256SAT0.01
stmt21_70_369UNSAT0.01
stmt21_84_364UNSAT0.01
stmt29_226_376UNSAT0.01
stmt21_181_369UNSAT0.01
query07_query42_1344nUNSAT0.01
stmt22_311_370UNSAT0.02
stmt19_352_359UNSAT0.02
stmt31_22_328UNSAT0.6
exquery_query42_1344nUNSAT0.91
Q_2-3_v-80-100_r-11.3UNSAT1.01
query21_query42_1344nUNSAT1.42
stmt44_40_387UNSAT3.22
Q_2-3_v-80-100_r-11.2UNSAT3.49
Q_2-3_v-80-100_r-11.6UNSAT9.14
query26_query42_1344nUNSAT12.78
stmt21_310_360UNSAT26.51
stmt19_66_214UNSAT30.56
Q_2-3_v-80-100_r-11.0UNSAT42.89
Q_2-3_v-80-100_r-11.4UNSAT50.89
sortnetsort8.AE.stepl.008UNSAT61.99
stmt46_111_238UNSAT68.7
query02_query44_1344nUNSAT83.75
query27_query42_1344nUNSAT124.1
nxquery_query50_1344nSAT128.72
stmt21_71_413UNSAT171.96
stmt19_90_408UNSAT173.67
stmt27_149_224UNSAT175.35
mult9.satSAT176.99
stmt19_133_217UNSAT191.25
query06_query42_1344nUNSAT197.57
query04_query42_1344nUNSAT216.31
stmt21_143_403UNSAT238.07
stmt19_313_412UNSAT264.49
stmt41_160_235UNSAT294.19
stmt22_6_414UNSAT340.24
stmt19_83_412UNSAT374.54
query31_query50_1344nSAT378.56
stmt19_3_401UNSAT380.83
sortnetsort7.AE.stepl.005SAT389.44
stmt19_137_408UNSAT405.22
Q_2-3_v-80-100_r-11.8UNSAT562.33
stmt21_181_218UNSAT567.14
stmt53_208_245UNSAT657.36
sortnetsort8.AE.stepl.004SAT750.03
cache-coherence-2-fixpoint-4FAIL900
add20y.satFAIL900
ethernet-fixpoint-2FAIL900
stay24n.satFAIL900
sortnetsort10.AE.stepl.009FAIL900
small-seq-fixpoint-7FAIL900
query31_eequery_1344nFAIL900
rankfunc52_unsigned_64FAIL900
NotificationServiceImpl2FAIL900
stmt31_276_328FAIL900
neclaftp2002FAIL900
stmt41_286_385FAIL900
cycle_sched_4_7_1.satFAIL900
query09_query42_1344nFAIL900
query11_query42_1344nFAIL900
stmt17_82_98FAIL900
ci.e#1.a#3.E#40.A#60.c#408.w#2.s#2.aspFAIL900
stmt46_289_388FAIL900
query60_query44_1344nFAIL900
itc-b13-fixpoint-4FAIL900
query55_query42_1344nFAIL900
query33_query57_1344nFAIL900
stmt28_68_73FAIL900
stmt23_66_76FAIL900
pdtpmsmiimFAIL900
rankfunc61_signed_64FAIL900.01
small-seq-fixpoint-3FAIL900.01
AR-fixpoint-2FAIL900.01
rankfunc51_unsigned_64FAIL900.01
stmt17_74_90FAIL900.01
rankfunc49_signed_64FAIL900.01
sdlx-fixpoint-10FAIL900.01
query48_query42_1344nFAIL900.01
reachqu_query42_1344nFAIL900.01
intermediate128FAIL900.01
neclaftp4001FAIL900.01
amba2f9n.satFAIL900.01
driver_d9y.satFAIL900.01
beemldelec4b1_c0to127.satFAIL900.01
GuidanceServiceFAIL900.01
driver_a10y.satFAIL900.01
driver_b8n.satFAIL900.01
driver_c9y.satFAIL900.01
query25_query42_1344nFAIL900.01
query05_query42_1344nFAIL900.01
eequery_query42_1344nFAIL900.01
cache-coherence-3-fixpoint-1FAIL900.01
itc-b13-fixpoint-10FAIL900.01
sdlx-fixpoint-9FAIL900.01
small-swap1-fixpoint-5FAIL900.01
small-synabs-fixpoint-3FAIL900.01
query42_query06_1344nFAIL900.01
query36_query25_1344nFAIL900.01
query49_ntrivil_1344nFAIL900.01
query64_query11_1344nFAIL900.01
ci.e#1.a#3.E#40.A#60.c#384.w#6.s#8.aspFAIL900.01
ci.e#1.a#3.E#40.A#60.c#408.w#2.s#1.aspFAIL900.01
mult_bool_matrix_12_13_11.satFAIL900.01
sortnetsort9.AE.stepl.011FAIL900.01
stmt29_275_376FAIL900.01
stmt25_52_53FAIL900.01
stmt23_88_92FAIL900.01
stmt41_262_275FAIL900.01
stmt124_966_965FAIL900.01
stmt39_285_335FAIL900.01
sortnetsort10.AE.stepl.011FAIL900.01
stmt19_64_99FAIL900.01
stmt41_336_385FAIL900.01
sortnetsort10.AE.stepl.010FAIL900.01
sortnetsort9.AE.stepl.010FAIL900.01
stmt9_445_446FAIL900.01
stmt17_74_78FAIL900.01
stmt23_66_67FAIL900.01
stmt17_70_78FAIL900.01
stmt17_63_82FAIL900.01
stmt28_73_97FAIL900.01
stmt17_70_82FAIL900.01
stmt19_71_95FAIL900.01
stmt19_75_83FAIL900.01
stmt19_64_87FAIL900.01
itc-b13-fixpoint-9FAIL900.02
stmt28_89_97FAIL900.02
small-seq-fixpoint-1FAIL900.02
cache-coherence-3-fixpoint-2FAIL900.02
pi-bus-fixpoint-1FAIL900.02
stmt19_75_95FAIL900.02
small-equiv-fixpoint-1FAIL900.02
stmt17_70_86FAIL900.02
sdlx-fixpoint-8FAIL900.02
stmt17_70_90FAIL900.02
AR-fixpoint-6FAIL900.02
usb-phy-fixpoint-5FAIL900.02
AR-fixpoint-1FAIL900.02
ci.e#1.a#3.E#40.A#60.c#288.w#6.s#2.aspFAIL900.02
ActivityServiceFAIL900.02
ctrl.e#1.a#3.E#116.A#48.c#.w#7.s#56.aspFAIL900.02
stmt17_63_78FAIL900.02
query42_query45_1344nFAIL900.02
query33_query45_1344nFAIL900.02
query33_query42_1344nFAIL900.02
stmt27_93_98FAIL900.02
query36_query42_1344nFAIL900.02
query31_reachqu_1344nFAIL900.02
ctrl.e#1.a#3.E#128.A#48.c#.w#9.s#1.aspFAIL900.02
small-swap1-fixpoint-10FAIL900.02
small-swap1-fixpoint-4FAIL900.02
ctrl.e#1.a#3.E#134.A#48.c#.w#9.s#40.aspFAIL900.02
query58_query42_1344nFAIL900.02
stmt22_320_370FAIL900.02
sortnetsort9.AE.stepl.008FAIL900.02
rankfunc54_unsigned_64FAIL900.02
rankfunc58_unsigned_64FAIL900.02
stmt53_296_346FAIL900.02
stmt19_368_417FAIL900.02
ceiling256FAIL900.02
query01_query42_1344nFAIL900.02
itc-b13-fixpoint-3FAIL900.02
usb-phy-fixpoint-2FAIL900.02
ActivityService2FAIL900.02
UserServiceImplFAIL900.02
rankfunc58_signed_64FAIL900.02
rankfunc55_unsigned_64FAIL900.03
stmt25_597_598FAIL900.03
query10_query45_1344nFAIL900.03
ctrl.e#1.a#3.E#128.A#48.c#.w#7.s#60.aspFAIL900.03
stmt19_79_87FAIL900.03
small-equiv-fixpoint-5FAIL900.03
driver_a9n.satFAIL900.03
stmt17_86_98FAIL900.03
query45_query42_1344nFAIL900.03
6s289rb05233_c0to63.satFAIL900.03
rankfunc35_signed_64FAIL900.03
query51_query42_1344nFAIL900.03
sortnetsort8.AE.stepl.005FAIL900.03
query52_query25_1344nFAIL900.03
query54_query58_1344nFAIL900.03
stmt28_68_69FAIL900.03
stmt17_62_78FAIL900.03
bs128n.satFAIL900.03
rankfunc56_signed_64FAIL900.03
Q_2-3_v-80-100_r-11.9FAIL900.03
sortnetsort9.AE.stepl.004FAIL900.03
stmt17_63_70FAIL900.03
stmt23_92_96FAIL900.03
Q_2-3_v-80-100_r-11.1FAIL900.03
stmt23_67_92FAIL900.03
query71_query36_1344nFAIL900.03
ltl2dba_C2-6_comp3_REAL.satFAIL900.03
query64_query01_1344nFAIL900.03
stmt17_62_98FAIL900.03
stmt17_82_94FAIL900.03
AR-fixpoint-8FAIL900.03
usb-phy-fixpoint-3FAIL900.03
stmt5_731_730FAIL900.03
small-seq-fixpoint-10FAIL900.03
small-equiv-fixpoint-4FAIL900.03
ceiling128FAIL900.03
small-swap1-fixpoint-8FAIL900.03
query10_query42_1344nFAIL900.03
sdlx-fixpoint-4FAIL900.03
pi-bus-fixpoint-2FAIL900.03
usb-phy-fixpoint-1FAIL900.03
driver_c9n.satFAIL900.03
reachqu_query64_1344nFAIL900.03
small-equiv-fixpoint-8FAIL900.03
stmt47_340_389FAIL900.03
itc-b13-fixpoint-6FAIL900.03
small-seq-fixpoint-8FAIL900.03
query52_query42_1344nFAIL900.03
stmt28_73_85FAIL900.03
small-seq-fixpoint-4FAIL900.03
cycle_sched_12_2_1.satFAIL900.03
small-seq-fixpoint-6FAIL900.03
rankfunc61_unsigned_64FAIL900.04
load_2c_comp_comp7_REAL.satFAIL900.04
rankfunc54_signed_64FAIL900.04
rankfunc49_unsigned_64FAIL900.04
reachqu_query71_1344nFAIL900.04
stmt19_65_87FAIL900.04
stmt19_79_83FAIL900.04
stmt23_66_96FAIL900.04
bs128y.satFAIL900.04
stmt17_82_86FAIL900.04
rankfunc48_unsigned_64FAIL900.04
eijkbs4863FAIL900.04
AR-fixpoint-4FAIL900.04
rankfunc59_unsigned_64FAIL900.04
stmt17_78_98FAIL900.04
mult_bool_matrix_17_17_17.satFAIL900.04
query34_query11_1344nFAIL900.04
intermediate256FAIL900.04
query31_query42_1344nFAIL900.04
small-equiv-fixpoint-2FAIL900.04
oski3ub5i_c0to63.satFAIL900.04
small-synabs-fixpoint-10FAIL900.04
pdtpmsrotate32FAIL900.04
query54_query42_1344nFAIL900.04
amba3b5y.satFAIL900.04
small-seq-fixpoint-2FAIL900.04
cycle_sched_2_10_1.satFAIL900.04
stmt44_554_604FAIL900.04
sortnetsort9.AE.stepl.005FAIL900.04
query71_query31_1344nFAIL900.04
sdlx-fixpoint-7FAIL900.04
query21_query58_1344nFAIL900.04
amba2c7n.satFAIL900.04
beemskbn1f1_c0to7.satFAIL900.04
cycle_sched_4_4_2.satFAIL900.04
ctrl.e#1.a#3.E#120.A#48.c#.w#3.s#3.aspFAIL900.04
ctrl.e#1.a#3.E#124.A#48.c#.w#7.s#50.aspFAIL900.04
rankfunc56_unsigned_64FAIL900.05
query50_query42_1344nFAIL900.05
PhaseServiceFAIL900.05
query64_query42_1344nFAIL900.05
sortnetsort7.AE.stepl.008FAIL900.05
stmt17_70_98FAIL900.05
eijkbs3330FAIL900.05
sortnetsort9.AE.stepl.007FAIL900.05
query34_query42_1344nFAIL900.05
stmt17_78_94FAIL900.05
sortnetsort7.AE.stepl.006FAIL900.05
rankfunc31_signed_64FAIL900.05
small-seq-fixpoint-9FAIL900.05
nreachq_query54_1344nFAIL900.05
eequery_query64_1344nFAIL900.05
query44_query26_1344nFAIL900.05
ctrl.e#1.a#3.E#128.A#48.c#.w#9.s#60.aspFAIL900.05
cache-coherence-2-fixpoint-6FAIL900.05
AR-fixpoint-10FAIL900.05
ethernet-fixpoint-4FAIL900.05
ethernet-fixpoint-1FAIL900.05
sdlx-fixpoint-5FAIL900.05
sdlx-fixpoint-6FAIL900.05
stmt21_354_403FAIL900.05
rankfunc52_signed_64FAIL900.05
query50_query06_1344nFAIL900.05
pi-bus-fixpoint-3FAIL900.05
rankfunc48_signed_64FAIL900.05
rankfunc51_signed_64FAIL900.05
sortnetsort10.AE.stepl.005FAIL900.05
ci.e#1.a#3.E#40.A#60.c#416.w#2.s#3.aspFAIL900.05
stmt19_64_91FAIL900.05
query51_query57_1344nFAIL900.05
rankfunc41_signed_64FAIL900.05
cache-coherence-2-fixpoint-5FAIL900.05
rankfunc53_signed_64FAIL900.06
stmt47_290_340FAIL900.06
ltl2dpa_C26_comp2_REAL.satFAIL900.06
stmt17_78_90FAIL900.06
sortnetsort9.AE.stepl.012FAIL900.06
cache-coherence-3-fixpoint-3FAIL900.06
itc-b13-fixpoint-2FAIL900.06
mult_bool_matrix_10_9_11.satFAIL900.06
rankfunc57_unsigned_64FAIL900.06
itc-b13-fixpoint-5FAIL900.06
stmt85_300_399FAIL900.06
rankfunc2_unsigned_64FAIL900.06
stmt16_818_819FAIL900.06
query60_query45_1344nFAIL900.06
ci.e#1.a#3.E#40.A#60.c#400.w#2.s#1.aspFAIL900.06
ConcreteActivityServiceFAIL900.06
IssueServiceImplFAIL900.06
stmt17_94_98FAIL900.06
GuidanceService2FAIL900.06
ctrl.e#1.a#3.E#110.A#48.c#.w#9.s#13.aspFAIL900.06
ctrl.e#1.a#3.E#128.A#48.c#.w#7.s#1.aspFAIL900.06
sortnetsort10.AE.stepl.012FAIL900.06
query04_query25_1344nFAIL900.06
stmt1_79_80FAIL900.06
small-pipeline-fixpoint-2FAIL900.06
small-equiv-fixpoint-3FAIL900.06
small-swap1-fixpoint-7FAIL900.06
sortnetsort8.AE.stepl.006FAIL900.06
stmt19_302_352FAIL900.06
sortnetsort9.AE.stepl.009FAIL900.07
oski3ub5i_c0to511.satFAIL900.07
ltl2dba_C2-8_comp4_REAL.satFAIL900.07
sortnetsort7.AE.stepl.007FAIL900.07
sortnetsort8.AE.stepl.009FAIL900.07
sdlx-fixpoint-3FAIL900.07
stmt21_319_418FAIL900.07
stmt19_83_91FAIL900.07
Q_2-3_v-80-100_r-11.5FAIL900.07
usb-phy-fixpoint-4FAIL900.07
itc-b13-fixpoint-8FAIL900.07
query33_query51_1344nFAIL900.07
small-swap1-fixpoint-9FAIL900.07
sortnetsort10.AE.stepl.004FAIL900.07
stmt19_87_95FAIL900.07
rankfunc31_unsigned_64FAIL900.07
rankfunc35_unsigned_64FAIL900.07
query08_query42_1344nFAIL900.07
query05_query31_1344nFAIL900.07
cycle_sched_6_7_1.satFAIL900.07
rankfunc53_unsigned_64FAIL900.08
stmt31_190_227FAIL900.08
query48_exquery_1344nFAIL900.08
small-swap1-fixpoint-6FAIL900.08
cycle_sched_6_6_2.satFAIL900.08
mult_bool_matrix_dyn_9_5.satFAIL900.08
sortnetsort10.AE.stepl.008FAIL900.08
stmt32_329_378FAIL900.08
stmt50_343_392FAIL900.08
cache-coherence-2-fixpoint-2FAIL900.08
ethernet-fixpoint-3FAIL900.08
stmt23_72_76FAIL900.08
nreachq_query11_1344nFAIL900.08
oski3ub5i_c0to255.satFAIL900.08
ctrl.e#1.a#3.E#128.A#48.c#.w#3.s#26.aspFAIL900.08
stmt2_976_999FAIL900.08
genbuf9b4n.satFAIL900.08
stmt19_65_95FAIL900.09
IterationServiceFAIL900.09
rankfunc59_signed_64FAIL900.09
query42_query42_1344nFAIL900.09
mult_bool_matrix_18_18_18.satFAIL900.09
sortnetsort7.AE.stepl.009FAIL900.09
rankfunc41_unsigned_64FAIL900.09
small-pipeline-fixpoint-3FAIL900.09
query03_query42_1344nFAIL900.09
small-seq-fixpoint-5FAIL900.09
ctrl.e#1.a#3.E#128.A#48.c#.w#7.s#7.aspFAIL900.09
ctrl.e#1.a#3.E#112.A#48.c#.w#5.s#27.aspFAIL900.09
itc-b13-fixpoint-7FAIL900.09
Q_2-3_v-80-100_r-11.7FAIL900.09
ctrl.e#1.a#3.E#118.A#48.c#.w#5.s#7.aspFAIL900.09
stmt52_295_394FAIL900.1
ctrl.e#1.a#3.E#128.A#48.c#.w#5.s#60.aspFAIL900.1
stmt28_68_81FAIL900.1