Home Intro Rules Participants Results Tools Bench Org SMT-LIB

Answers

This page contains the answer for all benchmarks used in the competition.

BenchmarkAnswer
QF_AUFLIA/array_benchmarks/pipeline-invalid.smtsat
QF_AUFLIA/array_benchmarks/pointer-invalid-10.smtsat
QF_AUFLIA/array_benchmarks/pointer-invalid-15.smtsat
QF_AUFLIA/array_benchmarks/pointer-invalid-20.smtsat
QF_AUFLIA/array_benchmarks/pointer-invalid-5.smtsat
QF_AUFLIA/array_benchmarks/pointer-safe-10.smtunsat
QF_AUFLIA/array_benchmarks/pointer-safe-15.smtunsat
QF_AUFLIA/array_benchmarks/pointer-safe-20.smtunsat
QF_AUFLIA/array_benchmarks/pointer-safe-5.smtunsat
QF_AUFLIA/array_benchmarks/qlock-bug-10.smtsat
QF_AUFLIA/array_benchmarks/qlock-bug-15.smtsat
QF_AUFLIA/array_benchmarks/qlock-bug-20.smtsat
QF_AUFLIA/array_benchmarks/qlock-bug-5.smtsat
QF_AUFLIA/array_benchmarks/qlock-bug2-10.smtsat
QF_AUFLIA/array_benchmarks/qlock-bug2-15.smtsat
QF_AUFLIA/array_benchmarks/qlock-bug2-20.smtsat
QF_AUFLIA/array_benchmarks/qlock-mutex-10.smtunsat
QF_AUFLIA/array_benchmarks/qlock-mutex-15.smtunsat
QF_AUFLIA/array_benchmarks/qlock-mutex-20.smtunsat
QF_AUFLIA/array_benchmarks/qlock-mutex-5.smtunsat
QF_AUFLIA/array_benchmarks/queue-th1-6.smtunsat
QF_AUFLIA/array_benchmarks/queue-th2-6.smtunsat
QF_AUFLIA/array_benchmarks/stack-invalid-6.smtsat
QF_AUFLIA/array_benchmarks/stack-th1-6.smtunsat
QF_AUFLIA/array_benchmarks/stack-th2-6.smtunsat
QF_AUFLIA/check/array_incompleteness1.smtunsat
QF_AUFLIA/check/int_incompleteness1.smtunsat
QF_AUFLIA/cvc/add4.smtunsat
QF_AUFLIA/cvc/add5.smtunsat
QF_AUFLIA/cvc/add6.smtunsat
QF_AUFLIA/cvc/dlx-dmem.smtunsat
QF_AUFLIA/cvc/dlx-pc.smtunsat
QF_AUFLIA/cvc/dlx-regfile.smtunsat
QF_AUFLIA/cvc/fb_var_12_11.smtunsat
QF_AUFLIA/cvc/fb_var_27_8.smtsat
QF_AUFLIA/cvc/fb_var_33_6.smtunsat
QF_AUFLIA/cvc/fb_var_5_12.smtunsat
QF_AUFLIA/cvc/fb_var_6_12.smtunsat
QF_AUFLIA/cvc/pp-TakenBranch-s2e.smtunsat
QF_AUFLIA/cvc/pp-bloaddata-a.smtunsat
QF_AUFLIA/cvc/pp-bloaddata.smtunsat
QF_AUFLIA/cvc/pp-dmem-a.smtunsat
QF_AUFLIA/cvc/pp-dmem.smtunsat
QF_AUFLIA/cvc/pp-dmem2.smtunsat
QF_AUFLIA/cvc/pp-invariant.smtunsat
QF_AUFLIA/cvc/pp-pc-s2i.smtunsat
QF_AUFLIA/cvc/pp-regfile.smtunsat
QF_AUFLIA/cvc/read2.smtunsat
QF_AUFLIA/cvc/read5.smtunsat
QF_AUFLIA/cvc/read6.smtunsat
QF_AUFLIA/cvc/read7.smtunsat
QF_AUFLIA/cvc/read8.smtunsat
QF_IDL/DTP/DTP_k2_n35_c175_s9.smtsat
QF_IDL/DTP/DTP_k2_n35_c210_s10.smtunsat
QF_IDL/DTP/DTP_k2_n35_c210_s16.smtunsat
QF_IDL/DTP/DTP_k2_n35_c210_s2.smtunsat
QF_IDL/DTP/DTP_k2_n35_c210_s4.smtunsat
QF_IDL/DTP/DTP_k2_n35_c210_s9.smtsat
QF_IDL/DTP/DTP_k2_n35_c245_s10.smtunsat
QF_IDL/DTP/DTP_k2_n35_c245_s15.smtunsat
QF_IDL/DTP/DTP_k2_n35_c245_s2.smtsat
QF_IDL/DTP/DTP_k2_n35_c245_s20.smtunsat
QF_IDL/DTP/DTP_k2_n35_c245_s5.smtunsat
QF_IDL/DTP/DTP_k2_n35_c245_s9.smtunsat
QF_IDL/check/int_incompleteness1.smtunsat
QF_IDL/diamonds/diamonds.10.2.i.a.u.smtunsat
QF_IDL/diamonds/diamonds.10.3.i.a.u.smtunsat
QF_IDL/diamonds/diamonds.14.5.i.a.u.smtunsat
QF_IDL/diamonds/diamonds.18.10.i.a.u.smtunsat
QF_IDL/diamonds/diamonds.18.5.i.a.u.smtunsat
QF_IDL/mathsat/FISCHER10-10-ninc.smtunsat
QF_IDL/mathsat/FISCHER10-11-ninc.smtsat
QF_IDL/mathsat/FISCHER10-5-ninc.smtunsat
QF_IDL/mathsat/FISCHER13-10-ninc.smtunsat
QF_IDL/mathsat/FISCHER13-13-ninc.smtunsat
QF_IDL/mathsat/FISCHER13-14-ninc.smtsat
QF_IDL/mathsat/FISCHER13-5-ninc.smtunsat
QF_IDL/mathsat/FISCHER14-10-ninc.smtunsat
QF_IDL/mathsat/FISCHER14-14-ninc.smtunsat
QF_IDL/mathsat/FISCHER14-15-ninc.smtsat
QF_IDL/mathsat/FISCHER5-5-ninc.smtunsat
QF_IDL/mathsat/FISCHER9-10-ninc.smtsat
QF_IDL/mathsat/FISCHER9-9-ninc.smtunsat
QF_IDL/mathsat/PO3-10-PO3.smtsat
QF_IDL/mathsat/PO3-5-PO3.smtunsat
QF_IDL/mathsat/PO3-7-PO3.smtunsat
QF_IDL/mathsat/PO4-10-PO4.smtunsat
QF_IDL/mathsat/PO4-11-PO4.smtunsat
QF_IDL/mathsat/PO4-4-PO4.smtunsat
QF_IDL/mathsat/PO4-6-PO4.smtunsat
QF_IDL/mathsat/PO4-8-PO4.smtunsat
QF_IDL/sal/inf-bakery-invalid-10.smtsat
QF_IDL/sal/inf-bakery-mutex-10.smtunsat
QF_IDL/sal/inf-bakery-mutex-15.smtunsat
QF_IDL/sal/inf-bakery-mutex-20.smtunsat
QF_IDL/sal/lpsat-goal-10.smtunsat
QF_IDL/sal/lpsat-goal-15.smtunsat
QF_IDL/sal/lpsat-goal-19.smtsat
QF_IDL/sal/lpsat-goal-20.smtsat
QF_IDL/sal/lpsat-goal-5.smtunsat
QF_IDL/sep/LD_ST_neg.2step.smtunsat
QF_IDL/sep/LD_ST_neg.3step.smtunsat
QF_IDL/sep/cache_neg.2step.smtunsat
QF_LIA/CIRC/MULTIPLIER_10.msat.smtunsat
QF_LIA/CIRC/MULTIPLIER_14.msat.smtunsat
QF_LIA/CIRC/MULTIPLIER_16.msat.smtunsat
QF_LIA/CIRC/MULTIPLIER_5.msat.smtunsat
QF_LIA/CIRC/MULTIPLIER_8.msat.smtunsat
QF_LIA/CIRC/MULTIPLIER_PRIME_10.msat.smtsat
QF_LIA/CIRC/MULTIPLIER_PRIME_15.msat.smtsat
QF_LIA/CIRC/MULTIPLIER_PRIME_3.msat.smtsat
QF_LIA/CIRC/MULTIPLIER_PRIME_5.msat.smtsat
QF_LIA/CIRC/MULTIPLIER_PRIME_8.msat.smtsat
QF_LIA/CIRC/SIMPLEBITADDER_COMPOSE_10.msat.smtunsat
QF_LIA/CIRC/SIMPLEBITADDER_COMPOSE_15.msat.smtunsat
QF_LIA/CIRC/SIMPLEBITADDER_COMPOSE_3.msat.smtunsat
QF_LIA/CIRC/SIMPLEBITADDER_COMPOSE_32.msat.smtunsat
QF_LIA/CIRC/SIMPLEBITADDER_COMPOSE_5.msat.smtunsat
QF_LIA/CIRC/SIMPLEBITADDER_COMPOSE_8.msat.smtunsat
QF_LIA/RTCL/b04_tf_15/ckt_PROP0_tf_15.smtsat
QF_LIA/RTCL/b04_tf_20/ckt_PROP0_tf_20.smtsat
QF_LIA/RTCL/b13_tf_100/b13_tf_100.smtunsat
QF_LIA/check/int_incompleteness2.smtunsat
QF_LIA/check/int_incompleteness3.smtunsat
QF_LIA/mathsat/FISCHER10-10-fair.smtunsat
QF_LIA/mathsat/FISCHER10-12-fair.smtunsat
QF_LIA/mathsat/FISCHER10-15-fair.smtsat
QF_LIA/mathsat/FISCHER10-4-fair.smtunsat
QF_LIA/mathsat/FISCHER10-5-fair.smtunsat
QF_LIA/mathsat/FISCHER10-8-fair.smtunsat
QF_LIA/mathsat/FISCHER10-9-fair.smtunsat
QF_LIA/mathsat/FISCHER11-10-fair.smtunsat
QF_LIA/mathsat/FISCHER11-12-fair.smtunsat
QF_LIA/mathsat/FISCHER11-13-fair.smtunsat
QF_LIA/mathsat/FISCHER11-14-fair.smtunsat
QF_LIA/mathsat/FISCHER11-15-fair.smtunsat
QF_LIA/mathsat/FISCHER11-16-fair.smtsat
QF_LIA/mathsat/FISCHER11-5-fair.smtunsat
QF_LIA/mathsat/FISCHER2-2-fair.smtunsat
QF_LIA/mathsat/FISCHER2-5-fair.smtunsat
QF_LIA/mathsat/FISCHER6-10-fair.smtunsat
QF_LIA/mathsat/FISCHER6-11-fair.smtsat
QF_LIA/mathsat/FISCHER6-5-fair.smtunsat
QF_LIA/mathsat/FISCHER7-10-fair.smtunsat
QF_LIA/mathsat/FISCHER7-12-fair.smtsat
QF_LIA/mathsat/FISCHER7-5-fair.smtunsat
QF_LIA/mathsat/FISCHER8-10-fair.smtunsat
QF_LIA/mathsat/FISCHER8-13-fair.smtsat
QF_LIA/mathsat/FISCHER8-5-fair.smtunsat
QF_LIA/mathsat/FISCHER9-10-fair.smtunsat
QF_LIA/mathsat/FISCHER9-14-fair.smtsat
QF_LIA/mathsat/FISCHER9-5-fair.smtunsat
QF_LIA/wisa/wisa1.smtsat
QF_LIA/wisa/wisa2.smtunsat
QF_LIA/wisa/wisa3.smtsat
QF_LIA/wisa/wisa4.smtsat
QF_LIA/wisa/wisa5.smtunsat
QF_LRA/TM/p-0-bucket_s13.smtsat
QF_LRA/TM/p-1-bucket_s9.smtsat
QF_LRA/TM/p-2-bucket_s11.smtsat
QF_LRA/TM/p-3-bucket_s10.smtsat
QF_LRA/TM/p3-driverlogNumeric_s8.smtsat
QF_LRA/TM/p4-driverlogNumeric_s8.smtsat
QF_LRA/TM/p5-driverlogNumeric_s8.smtsat
QF_LRA/TM/p5-driverlogNumeric_s9.smtunsat
QF_LRA/sal/Carpark2-ausgabe-5.smtunsat
QF_LRA/sal/gasburner-prop3-10.smtunsat
QF_LRA/sal/gasburner-prop3-15.smtunsat
QF_LRA/sal/gasburner-prop3-20.smtunsat
QF_LRA/sal/gasburner-prop3-5.smtunsat
QF_LRA/sal/pursuit-safety-10.smtunsat
QF_LRA/sal/pursuit-safety-15.smtunsat
QF_LRA/sal/pursuit-safety-20.smtunsat
QF_LRA/sal/pursuit-safety-5.smtunsat
QF_LRA/sal/tgc_io-nosafe-5.smtunsat
QF_LRA/sal/tgc_io-safe-10.smtunsat
QF_LRA/sal/tgc_io-safe-15.smtunsat
QF_LRA/sal/tgc_io-safe-20.smtsat
QF_LRA/sal/tgc_io-safe-5.smtunsat
QF_LRA/sal/windowreal-no_t_deadlock-10.smtunsat
QF_LRA/sal/windowreal-no_t_deadlock-15.smtunsat
QF_LRA/sal/windowreal-no_t_deadlock-20.smtunsat
QF_LRA/sal/windowreal-no_t_deadlock-5.smtunsat
QF_LRA/spider_benchmarks/frame_prop.induction.smtunsat
QF_LRA/spider_benchmarks/fs_frame_gap.base.smtunsat
QF_LRA/spider_benchmarks/fs_frame_gap.induction.smtunsat
QF_LRA/spider_benchmarks/fs_init_no_op_accs.base.smtunsat
QF_LRA/spider_benchmarks/fs_init_no_op_accs.induction.smtunsat
QF_LRA/spider_benchmarks/fs_no_op_accs.base.smtunsat
QF_LRA/spider_benchmarks/fs_no_op_accs.induction.smtunsat
QF_LRA/spider_benchmarks/fs_not_sc_seen.base.smtunsat
QF_LRA/spider_benchmarks/fs_not_sc_seen.induction.smtunsat
QF_LRA/spider_benchmarks/fs_window.base.smtunsat
QF_LRA/spider_benchmarks/fs_window.induction.smtunsat
QF_LRA/spider_benchmarks/good_frame_update.base.smtunsat
QF_LRA/spider_benchmarks/good_frame_update.induction.smtunsat
QF_LRA/spider_benchmarks/op_seen_less2.base.smtunsat
QF_LRA/spider_benchmarks/op_seen_less2.induction.smtunsat
QF_LRA/spider_benchmarks/op_seen_more1.base.smtunsat
QF_LRA/spider_benchmarks/op_seen_more1.induction.smtunsat
QF_LRA/spider_benchmarks/pd_no_op_accs.base.smtunsat
QF_LRA/spider_benchmarks/pd_no_op_accs.induction.smtunsat
QF_LRA/spider_benchmarks/reint_to_least.induction.smtunsat
QF_LRA/spider_benchmarks/sc_init_frame_gap.base.smtunsat
QF_LRA/spider_benchmarks/sc_init_frame_gap.induction.smtunsat
QF_LRA/spider_benchmarks/synched.base.smtunsat
QF_LRA/spider_benchmarks/synched.induction.smtunsat
QF_RDL/sal/fischer3-mutex-10.smtunsat
QF_RDL/sal/fischer3-mutex-11.smtunsat
QF_RDL/sal/fischer3-mutex-12.smtunsat
QF_RDL/sal/fischer3-mutex-15.smtunsat
QF_RDL/sal/fischer3-mutex-20.smtunsat
QF_RDL/sal/fischer3-mutex-3.smtunsat
QF_RDL/sal/fischer3-mutex-5.smtunsat
QF_RDL/sal/fischer3-mutex-8.smtunsat
QF_RDL/sal/fischer6-mutex-10.smtunsat
QF_RDL/sal/fischer6-mutex-11.smtunsat
QF_RDL/sal/fischer6-mutex-12.smtunsat
QF_RDL/sal/fischer6-mutex-15.smtunsat
QF_RDL/sal/fischer6-mutex-20.smtunsat
QF_RDL/sal/fischer6-mutex-3.smtunsat
QF_RDL/sal/fischer6-mutex-5.smtunsat
QF_RDL/sal/fischer6-mutex-8.smtunsat
QF_RDL/sal/fischer9-mutex-10.smtunsat
QF_RDL/sal/fischer9-mutex-11.smtunsat
QF_RDL/sal/fischer9-mutex-12.smtunsat
QF_RDL/sal/fischer9-mutex-15.smtunsat
QF_RDL/sal/fischer9-mutex-20.smtunsat
QF_RDL/sal/fischer9-mutex-3.smtunsat
QF_RDL/sal/fischer9-mutex-5.smtunsat
QF_RDL/sal/fischer9-mutex-8.smtunsat
QF_RDL/scheduling/abz5_1000.smtunsat
QF_RDL/scheduling/abz5_1200.smtunsat
QF_RDL/scheduling/abz5_1234.smtsat
QF_RDL/scheduling/abz6_800.smtunsat
QF_RDL/scheduling/abz6_900.smtunsat
QF_RDL/scheduling/orb01_900.smtunsat
QF_RDL/scheduling/orb02_888.smtsat
QF_RDL/scheduling/orb03_1005.smtsat
QF_RDL/scheduling/orb03_950.smtunsat
QF_RDL/scheduling/orb07_250.smtunsat
QF_RDL/scheduling/orb07_330.smtunsat
QF_RDL/scheduling/orb07_397.smtsat
QF_RDL/scheduling/orb09_800.smtunsat
QF_RDL/scheduling/orb09_900.smtunsat
QF_RDL/scheduling/orb09_934.smtsat
QF_RDL/scheduling/orb10_1000.smtsat
QF_RDL/scheduling/orb10_800.smtunsat
QF_RDL/scheduling/yn1_750.smtunsat
QF_RDL/scheduling/yn2_750.smtunsat
QF_RDL/scheduling/yn2_950.smtsat
QF_RDL/scheduling/yn3_750.smtunsat
QF_RDL/scheduling/yn3_950.smtsat
QF_RDL/skdmxa/skdmxa-3x3-10.smtunsat
QF_RDL/skdmxa/skdmxa-3x3-15.smtunsat
QF_RDL/skdmxa/skdmxa-3x3-20.smtunsat
QF_RDL/skdmxa/skdmxa-3x3-5.smtunsat
QF_UF/NEQ/NEQ004_size4.smtunsat
QF_UF/NEQ/NEQ004_size7.smtunsat
QF_UF/NEQ/NEQ006_size5.smtunsat
QF_UF/NEQ/NEQ015_size3.smtunsat
QF_UF/NEQ/NEQ016_size5.smtunsat
QF_UF/NEQ/NEQ016_size8.smtunsat
QF_UF/NEQ/NEQ031_size10.smtunsat
QF_UF/NEQ/NEQ032_size3.smtunsat
QF_UF/NEQ/NEQ041_size6.smtunsat
QF_UF/NEQ/NEQ046_size3.smtunsat
QF_UF/NEQ/NEQ048_size6.smtunsat
QF_UF/NEQ/NEQ048_size9.smtunsat
QF_UF/PEQ/PEQ002_size6.smtunsat
QF_UF/PEQ/PEQ002_size8.smtunsat
QF_UF/PEQ/PEQ003_size7.smtunsat
QF_UF/PEQ/PEQ003_size9.smtunsat
QF_UF/PEQ/PEQ004_size7.smtunsat
QF_UF/PEQ/PEQ011_size5.smtunsat
QF_UF/PEQ/PEQ011_size7.smtunsat
QF_UF/PEQ/PEQ012_size3.smtunsat
QF_UF/PEQ/PEQ012_size5.smtunsat
QF_UF/PEQ/PEQ013_size8.smtunsat
QF_UF/PEQ/PEQ016_size4.smtunsat
QF_UF/PEQ/PEQ016_size6.smtunsat
QF_UF/PEQ/PEQ016_size7.smtunsat
QF_UF/PEQ/PEQ018_size4.smtunsat
QF_UF/PEQ/PEQ018_size7.smtunsat
QF_UF/PEQ/PEQ019_size5.smtunsat
QF_UF/PEQ/PEQ020_size4.smtunsat
QF_UF/PEQ/PEQ020_size6.smtunsat
QF_UF/SEQ/SEQ004_size5.smtunsat
QF_UF/SEQ/SEQ004_size6.smtunsat
QF_UF/SEQ/SEQ004_size7.smtsat
QF_UF/SEQ/SEQ005_size9.smtunsat
QF_UF/SEQ/SEQ009_size7.smtunsat
QF_UF/SEQ/SEQ009_size8.smtunsat
QF_UF/SEQ/SEQ009_size9.smtunsat
QF_UF/SEQ/SEQ010_size9.smtunsat
QF_UF/SEQ/SEQ011_size4.smtsat
QF_UF/SEQ/SEQ013_size6.smtsat
QF_UF/SEQ/SEQ015_size4.smtsat
QF_UF/SEQ/SEQ017_size6.smtsat
QF_UF/SEQ/SEQ018_size8.smtsat
QF_UF/SEQ/SEQ020_size4.smtsat
QF_UF/SEQ/SEQ026_size4.smtunsat
QF_UF/SEQ/SEQ032_size2.smtunsat
QF_UF/SEQ/SEQ035_size6.smtsat
QF_UF/SEQ/SEQ038_size9.smtunsat
QF_UF/SEQ/SEQ042_size3.smtunsat
QF_UF/SEQ/SEQ050_size3.smtunsat
QF_UFIDL/check/int_incompleteness1.smtunsat
QF_UFIDL/pete/6stage-flush.smtunsat
QF_UFIDL/pete/9stage-flush.smtunsat
QF_UFIDL/pete/cxs-bp-ex-inp.smtunsat
QF_UFIDL/pete/cxs-bp.smtunsat
QF_UFIDL/pete/cxs-safety.smtunsat
QF_UFIDL/pete/cxs.smtunsat
QF_UFIDL/pete/fxs-bp-ex-inp-safety.smtunsat
QF_UFIDL/pete/fxs-bp-ex.smtunsat
QF_UFIDL/pete/fxs-safety.smtunsat
QF_UFIDL/pete/fxs.smtunsat
QF_UFIDL/pete2/c10ni.smtunsat
QF_UFIDL/pete2/c6_s.smtunsat
QF_UFIDL/pete2/c6b_s.smtunsat
QF_UFIDL/pete2/c6bidw_s.smtunsat
QF_UFIDL/pete2/c8b_i.smtunsat
QF_UFIDL/pete2/c8idw_i.smtunsat
QF_UFIDL/pete2/f10nidw.smtunsat
QF_UFIDL/pete2/f8b.smtunsat
QF_UFIDL/pete2/f8bidw.smtunsat
QF_UFIDL/pete2/f9.smtunsat
QF_UFIDL/pete2/f9idw.smtunsat
QF_UFIDL/pete2/g10bidw.smtunsat
QF_UFIDL/pete2/g10i.smtunsat
QF_UFIDL/pete2/g6bidw.smtunsat
QF_UFIDL/pete2/g7.smtunsat
QF_UFIDL/pete2/g8nidw.smtunsat
QF_UFIDL/pete2/g9idw.smtunsat
QF_UFIDL/pete2/g9n.smtunsat
QF_UFIDL/uclid/22s.smtunsat
QF_UFIDL/uclid/43s.smtunsat
QF_UFIDL/uclid/cache.inv12.smtunsat
QF_UFIDL/uclid/cache.inv8.smtunsat
QF_UFIDL/uclid/dlx1c.rwmem.smtunsat
QF_UFIDL/uclid/dlx1c.smtunsat
QF_UFIDL/uclid/elf.rf10.smtunsat
QF_UFIDL/uclid/elf.rf8.smtunsat
QF_UFIDL/uclid/ooo.rf10.smtunsat
QF_UFIDL/uclid/ooo.rf6.smtunsat
QF_UFIDL/uclid/ooo.tag10.smtunsat
QF_UFIDL/uclid/q2.10.smtunsat
QF_UFIDL/uclid/q2.14.smtunsat
QF_UFIDL/uclid2/bug1.smtsat
QF_UFIDL/uclid2/bug2.smtsat
QF_UFIDL/uclid2/cache.inv15.smtunsat
QF_UFIDL/uclid2/elf.rf12.smtunsat
QF_UFIDL/uclid2/ooo.rf13.smtunsat
QF_UFIDL/uclid2/ooo.tag15.smtunsat
QF_UFIDL/uclid2/ooo.tag19.smtunsat
Home Intro Rules Participants Results Tools Bench Org SMT-LIB

Last modified: Tue 17 Feb 2015 14:59 UTC