FMCAD'14: Turbo-Charging Lemmas on Demand with Don't Care Reasoning
==============================================================================

fmcad14-dpjust-bin.tar.gz contains two Boolector binaries:

  - boolector - the base version of Boolector
      Note: use option -ju to enable justification-based optimization
            use option -dp to enable dual propagation-based optimization

  - boolector_smtcomp12 - the SMTCOMP'12 version of Boolector

------------------------------------------------------------------------------

fmcad14-dpjust-logs.7z contains all logs of our experimental evaluation.

------------------------------------------------------------------------------

Benchmark set SMT'12 contains the following benchmarks:

QF_AUFBV/bench_ab/a21test0002.smt2
QF_AUFBV/bench_ab/a295test0001.smt2
QF_AUFBV/bench_ab/a73test0004.smt2
QF_AUFBV/bench_ab/b163test0005.smt2
QF_AUFBV/bench_ab/b172test0014.smt2
QF_AUFBV/bench_ab/b186test0002.smt2
QF_AUFBV/bench_ab/b33test0001.smt2
QF_AUFBV/bench_ab/b6test0005.smt2
QF_AUFBV/bench_ab/ft-out-2006-03-04test0016.smt2
QF_AUFBV/brummayerbiere/binarysearch32s128.smt2
QF_AUFBV/brummayerbiere/bubsort016un.smt2
QF_AUFBV/brummayerbiere/fifo32bc06k07.smt2
QF_AUFBV/brummayerbiere/fifo32in10k06.smt2
QF_AUFBV/brummayerbiere/fifo32in10k08.smt2
QF_AUFBV/brummayerbiere/memcpy07.smt2
QF_AUFBV/brummayerbiere/memcpy08.smt2
QF_AUFBV/brummayerbiere2/countbitstable064.smt2
QF_AUFBV/brummayerbiere2/countbitstableoffbyone0064.smt2
QF_AUFBV/brummayerbiere2/countbitstableoffbyone0256.smt2
QF_AUFBV/brummayerbiere2/countbitstableoffbyone0512.smt2
QF_AUFBV/brummayerbiere2/countbitstableuninit0032.smt2
QF_AUFBV/btfnt/btfnt_atlas_out.smt2
QF_AUFBV/calc2/calc2_sec2_adder_bmc15.atlas.smt2
QF_AUFBV/calc2/calc2_sec2_adder_bmc20.atlas.smt2
QF_AUFBV/calc2/calc2_sec2_adder_bmc25.atlas.smt2
QF_AUFBV/calc2/calc2_sec2_adder_bmc30.atlas.smt2
QF_AUFBV/calc2/calc2_sec2_adder_bmc5.atlas.smt2
QF_AUFBV/calc2/calc2_sec2_adder_shifter_bmc15.atlas.smt2
QF_AUFBV/calc2/calc2_sec2_adder_shifter_bmc20.atlas.smt2
QF_AUFBV/calc2/calc2_sec2_adder_shifter_bmc25.atlas.smt2
QF_AUFBV/calc2/calc2_sec2_adder_shifter_bmc30.atlas.smt2
QF_AUFBV/calc2/calc2_sec2_adder_shifter_bmc5.atlas.smt2
QF_AUFBV/calc2/calc2_sec2_bmc15.atlas.smt2
QF_AUFBV/calc2/calc2_sec2_bmc20.atlas.smt2
QF_AUFBV/calc2/calc2_sec2_bmc25.atlas.smt2
QF_AUFBV/calc2/calc2_sec2_bmc30.atlas.smt2
QF_AUFBV/calc2/calc2_sec2_mult_bmc10.atlas.smt2
QF_AUFBV/calc2/calc2_sec2_mult_bmc15.atlas.smt2
QF_AUFBV/calc2/calc2_sec2_mult_bmc20.atlas.smt2
QF_AUFBV/calc2/calc2_sec2_mult_bmc25.atlas.smt2
QF_AUFBV/calc2/calc2_sec2_mult_bmc30.atlas.smt2
QF_AUFBV/calc2/calc2_sec2_shifter_bmc10.atlas.smt2
QF_AUFBV/calc2/calc2_sec2_shifter_bmc15.atlas.smt2
QF_AUFBV/calc2/calc2_sec2_shifter_bmc20.atlas.smt2
QF_AUFBV/calc2/calc2_sec2_shifter_bmc25.atlas.smt2
QF_AUFBV/calc2/calc2_sec2_shifter_bmc30.atlas.smt2
QF_AUFBV/calc2/calc2_sec2_shifter_mult_bmc15.atlas.smt2
QF_AUFBV/calc2/calc2_sec2_shifter_mult_bmc20.atlas.smt2
QF_AUFBV/calc2/calc2_sec2_shifter_mult_bmc25.atlas.smt2
QF_AUFBV/calc2/calc2_sec2_shifter_mult_bmc30.atlas.smt2
QF_AUFBV/dwp_formulas/try5_small_difret_functions_wp_chgrp.bkm_scale.il.wp.smt2
QF_AUFBV/dwp_formulas/try5_small_difret_functions_wp_csplit.bkm_scale.il.wp.smt2
QF_AUFBV/dwp_formulas/try5_small_difret_functions_wp_fmt.bkm_scale.il.wp.smt2
QF_AUFBV/dwp_formulas/try5_small_difret_functions_wp_fold.bkm_scale.il.wp.smt2
QF_AUFBV/dwp_formulas/try5_small_difret_functions_wp_join.bkm_scale.il.wp.smt2
QF_AUFBV/dwp_formulas/try5_small_difret_functions_wp_logname.get_quoting_style.il.wp.smt2
QF_AUFBV/dwp_formulas/try5_small_difret_functions_wp_mkfifo.mode_adjust.il.wp.smt2
QF_AUFBV/dwp_formulas/try5_small_difret_functions_wp_mknod.mode_adjust.il.wp.smt2
QF_AUFBV/dwp_formulas/try5_small_difret_functions_wp_paste.get_quoting_style.il.wp.smt2
QF_AUFBV/dwp_formulas/try5_small_difret_functions_wp_ptx.bkm_scale.il.wp.smt2
QF_AUFBV/dwp_formulas/try5_small_difret_functions_wp_shuf.bkm_scale.il.wp.smt2
QF_AUFBV/dwp_formulas/try5_small_difret_functions_wp_split.bkm_scale.il.wp.smt2
QF_AUFBV/dwp_formulas/try5_small_difret_functions_wp_tail.bkm_scale.il.wp.smt2
QF_AUFBV/dwp_formulas/try5_small_difret_functions_wp_uniq.bkm_scale.il.wp.smt2
QF_AUFBV/dwp_formulas/try5_small_difret_functions_wp_vdir.bkm_scale.il.wp.smt2
QF_AUFBV/dwp_formulas/try5_small_difret_functions_wp_vdir.free_entry.il.wp.smt2
QF_AUFBV/dwp_formulas/try5_small_noof_functions_wp_csplit.rpl_re_set_registers.il.wp.smt2
QF_AUFBV/dwp_formulas/try5_small_noof_functions_wp_dd.quoting_options_from_style.il.wp.smt2
QF_AUFBV/dwp_formulas/try5_small_noof_functions_wp_nl.mark_opt_subexp.il.wp.smt2
QF_AUFBV/dwp_formulas/try5_small_noof_functions_wp_nl.re_string_translate_buffer.il.wp.smt2
QF_AUFBV/dwp_formulas/try5_small_noof_functions_wp_sha1sum.quoting_options_from_style.il.wp.smt2
QF_AUFBV/dwp_formulas/try5_small_noof_functions_wp_sha224sum.set_quoting_style.il.wp.smt2
QF_AUFBV/dwp_formulas/try5_small_noof_functions_wp_stat.quoting_options_from_style.il.wp.smt2
QF_AUFBV/dwp_formulas/try5_small_noof_functions_wp_users.close_stdout_set_file_name.il.wp.smt2
QF_AUFBV/egt/egt-1020.smt2
QF_AUFBV/egt/egt-3363.smt2
QF_AUFBV/egt/egt-3756.smt2
QF_AUFBV/egt/egt-5221.smt2
QF_AUFBV/egt/egt-5224.smt2
QF_AUFBV/egt/egt-6377.smt2
QF_AUFBV/egt/egt-6877.smt2
QF_AUFBV/egt/egt-7784.smt2
QF_AUFBV/platania/copy_array/copy_array71.c.smt2
QF_AUFBV/platania/copy_array/copy_array91.c.smt2
QF_AUFBV/platania/no_init_bubble_sort/no_init_bubble_sort_safe17.c.smt2
QF_AUFBV/platania/no_init_bubble_sort/no_init_bubble_sort_safe22.c.smt2
QF_AUFBV/platania/no_init_bubble_sort/no_init_bubble_sort_safe27.c.smt2
QF_AUFBV/platania/no_init_bubble_sort/no_init_bubble_sort_safe7.c.smt2
QF_AUFBV/platania/no_init_bubble_sort/no_init_bubble_sort_unsafe22.c.smt2
QF_AUFBV/platania/no_init_bubble_sort/no_init_bubble_sort_unsafe27.c.smt2
QF_AUFBV/platania/no_init_bubble_sort/no_init_bubble_sort_unsafe7.c.smt2
QF_AUFBV/platania/no_init_extract_sublist/no_init_extract_sublist105.smt2
QF_AUFBV/platania/no_init_multi_delete/no_init_multi_delete15.smt2
QF_AUFBV/platania/no_init_multi_delete/no_init_multi_delete25.smt2
QF_AUFBV/platania/no_init_multi_delete/no_init_multi_delete5.smt2
QF_AUFBV/platania/no_init_multi_delete/no_init_multi_delete6.smt2
QF_AUFBV/platania/no_init_multi_member/no_init_multi_member17.smt2
QF_AUFBV/platania/no_init_multi_member/no_init_multi_member19.smt2
QF_AUFBV/platania/no_init_multi_member/no_init_multi_member20.smt2
QF_AUFBV/platania/no_init_multi_member/no_init_multi_member21.smt2
QF_AUFBV/platania/no_init_multi_member/no_init_multi_member22.smt2
QF_AUFBV/platania/no_init_multi_member/no_init_multi_member23.smt2
QF_AUFBV/platania/no_init_multi_member/no_init_multi_member24.smt2
QF_AUFBV/platania/no_init_multi_member/no_init_multi_member25.smt2
QF_AUFBV/platania/no_init_selection_sort/no_init_selection_sort_safe12.c.smt2
QF_AUFBV/platania/no_init_selection_sort/no_init_selection_sort_safe17.c.smt2
QF_AUFBV/platania/no_init_selection_sort/no_init_selection_sort_safe27.c.smt2
QF_AUFBV/platania/no_init_selection_sort/no_init_selection_sort_safe7.c.smt2
QF_AUFBV/platania/no_init_selection_sort/no_init_selection_sort_unsafe12.c.smt2
QF_AUFBV/platania/no_init_selection_sort/no_init_selection_sort_unsafe17.c.smt2
QF_AUFBV/platania/no_init_selection_sort/no_init_selection_sort_unsafe22.c.smt2
QF_AUFBV/platania/no_init_selection_sort/no_init_selection_sort_unsafe27.c.smt2
QF_AUFBV/platania/no_init_simple_member/no_init_simple_member237.smt2
QF_AUFBV/platania/selection_sort/selection_sort2.c.smt2
QF_AUFBV/platania/strcmp/strcmp57.c.smt2
QF_AUFBV/platania/strcmp/strcmp62.c.smt2
QF_AUFBV/platania/strcmp/strcmp67.c.smt2
QF_AUFBV/platania/strcmp/strcmp72.c.smt2
QF_AUFBV/platania/strcmp/strcmp77.c.smt2
QF_AUFBV/platania/strcmp/strcmp82.c.smt2
QF_AUFBV/platania/strcmp/strcmp87.c.smt2
QF_AUFBV/platania/strcmp/strcmp92.c.smt2
QF_AUFBV/platania/strcmp/strcmp97.c.smt2
QF_AUFBV/stp/blaster-concrete.stp.smt2
QF_AUFBV/stp/blaster-small.stp.smt2
QF_AUFBV/stp/blaster-wp.ir.3.simplified13.stp.smt2
QF_AUFBV/stp/blaster-wp.ir.3.simplified4.stp.smt2
QF_AUFBV/stp/blaster-wp.ir.3.simplified8.stp.smt2
QF_AUFBV/stp/blaster.stp.smt2
QF_AUFBV/stp/cmu-model15.smt2
QF_AUFBV/stp/grep0065.stp.smt2
QF_AUFBV/stp/grep0084.stp.smt2
QF_AUFBV/stp/grep0095.stp.smt2
QF_AUFBV/stp/grep0106.stp.smt2
QF_AUFBV/stp/testcase1.stp.smt2
QF_AUFBV/stp/testcase11.stp.smt2
QF_AUFBV/stp/testcase12.stp.smt2
QF_AUFBV/stp/testcase13.stp.smt2
QF_AUFBV/stp/testcase14.stp.smt2
QF_AUFBV/stp/testcase16.stp.smt2
QF_AUFBV/stp/testcase18.stp.smt2
QF_AUFBV/stp/testcase19.stp.smt2
QF_AUFBV/stp/testcase2.stp.smt2
QF_AUFBV/stp/testcase20.stp.smt2
QF_AUFBV/stp/testcase4.stp.smt2
QF_AUFBV/stp/testcase5.stp.smt2
QF_AUFBV/stp/testcase6.stp.smt2
QF_AUFBV/stp/testcase8.stp.smt2
QF_AUFBV/stp/testcase9.stp.smt2

------------------------------------------------------------------------------

Benchmark set Selected contains the following benchmarks:

QF_AUFBV/btfnt/btfnt_atlas_out.smt2
QF_AUFBV/stp/testcase18.stp.smt2
QF_AUFBV/stp/grep0084.stp.smt2
QF_AUFBV/stp/testcase12.stp.smt2
QF_AUFBV/stp/grep0106.stp.smt2
QF_AUFBV/stp/testcase5.stp.smt2
QF_AUFBV/stp/testcase3.stp.smt2
QF_AUFBV/stp/grep0117.stp.smt2
QF_AUFBV/stp/testcase21.stp.smt2
QF_AUFBV/stp/grep0095.stp.smt2
QF_AUFBV/stp/testcase4.stp.smt2
QF_AUFBV/stp/grep0777.stp.smt2
QF_AUFBV/stp/testcase11.stp.smt2
QF_AUFBV/stp/noregions-fullmemite.stp.smt2
QF_AUFBV/stp/noregions-stpmem.stp.smt2
QF_AUFBV/stp/ff.stp.smt2
QF_AUFBV/stp/testcase20.stp.smt2
QF_AUFBV/stp/testcase9.stp.smt2
QF_AUFBV/egt/egt-5228.smt2
QF_AUFBV/egt/egt-0127.smt2
QF_AUFBV/egt/egt-5224.smt2
QF_AUFBV/egt/egt-5221.smt2
QF_AUFBV/egt/egt-5212.smt2
QF_AUFBV/brummayerbiere/fifo32in10k08.smt2
QF_AUFBV/brummayerbiere/fifo32in08k06.smt2
QF_AUFBV/brummayerbiere/selsort012un.smt2
QF_AUFBV/brummayerbiere/bubsort012un.smt2
QF_AUFBV/brummayerbiere/binarysearch32s032.smt2
QF_AUFBV/brummayerbiere/bubsort040un.smt2
QF_AUFBV/brummayerbiere/bubsort014un.smt2
QF_AUFBV/brummayerbiere/fifo32in10k09.smt2
QF_AUFBV/brummayerbiere/fifo32in10k06.smt2
QF_AUFBV/brummayerbiere/selsort040un.smt2
QF_AUFBV/brummayerbiere/selsort007un.smt2
QF_AUFBV/brummayerbiere/binarysearch32s128.smt2
QF_AUFBV/brummayerbiere/selsort030un.smt2
QF_AUFBV/brummayerbiere/selsort009un.smt2
QF_AUFBV/brummayerbiere/fifo32bc08k10.smt2
QF_AUFBV/brummayerbiere/bubsort030un.smt2
QF_AUFBV/brummayerbiere/fifo32in08k10.smt2
QF_AUFBV/brummayerbiere/bubsort018un.smt2
QF_AUFBV/brummayerbiere/fifo32in08k07.smt2
QF_AUFBV/brummayerbiere/selsort014un.smt2
QF_AUFBV/brummayerbiere/fifo32in10k10.smt2
QF_AUFBV/brummayerbiere/bubsort025un.smt2
QF_AUFBV/brummayerbiere/bubsort045un.smt2
QF_AUFBV/brummayerbiere/selsort018un.smt2
QF_AUFBV/brummayerbiere/fifo32in08k08.smt2
QF_AUFBV/brummayerbiere/fifo32bc06k09.smt2
QF_AUFBV/brummayerbiere/binarysearch32s256.smt2
QF_AUFBV/brummayerbiere/bubsort009un.smt2
QF_AUFBV/brummayerbiere/bubsort050un.smt2
QF_AUFBV/brummayerbiere/fifo32bc04k10.smt2
QF_AUFBV/brummayerbiere/bubsort010un.smt2
QF_AUFBV/brummayerbiere/bubsort016un.smt2
QF_AUFBV/brummayerbiere/selsort025un.smt2
QF_AUFBV/brummayerbiere/selsort016un.smt2
QF_AUFBV/brummayerbiere/binarysearch32s064.smt2
QF_AUFBV/brummayerbiere/fifo32in10k05.smt2
QF_AUFBV/brummayerbiere/fifo32bc08k09.smt2
QF_AUFBV/brummayerbiere/fifo32bc08k08.smt2
QF_AUFBV/brummayerbiere/fifo32in08k09.smt2
QF_AUFBV/brummayerbiere/selsort020un.smt2
QF_AUFBV/brummayerbiere/fifo32bc08k06.smt2
QF_AUFBV/brummayerbiere/selsort008un.smt2
QF_AUFBV/brummayerbiere/bubsort020un.smt2
QF_AUFBV/brummayerbiere/bubsort035un.smt2
QF_AUFBV/brummayerbiere/memcpy12.smt2
QF_AUFBV/brummayerbiere/selsort035un.smt2
QF_AUFBV/brummayerbiere/fifo32in08k05.smt2
QF_AUFBV/brummayerbiere/fifo32bc08k07.smt2
QF_AUFBV/brummayerbiere/fifo32in10k07.smt2
QF_AUFBV/brummayerbiere/memcpy11.smt2
QF_AUFBV/brummayerbiere/selsort045un.smt2
QF_AUFBV/brummayerbiere/selsort050un.smt2
QF_AUFBV/brummayerbiere/selsort010un.smt2
QF_AUFBV/brummayerbiere/fifo32bc06k10.smt2
QF_AUFBV/check/jagertest.smt2
QF_AUFBV/check/jagertest2.smt2
QF_AUFBV/brummayerbiere3/unconstrained05.smt2
QF_AUFBV/brummayerbiere3/unconstrained02.smt2
QF_AUFBV/brummayerbiere3/unconstrained04.smt2
QF_AUFBV/brummayerbiere3/unconstrained03.smt2
QF_AUFBV/brummayerbiere3/unconstrained01.smt2
QF_AUFBV/brummayerbiere3/unconstrained09.smt2
QF_AUFBV/platania/no_init_bubble_sort/no_init_bubble_sort_safe17.c.smt2
QF_AUFBV/platania/no_init_bubble_sort/no_init_bubble_sort_unsafe27.c.smt2
QF_AUFBV/platania/no_init_bubble_sort/no_init_bubble_sort_unsafe22.c.smt2
QF_AUFBV/platania/no_init_bubble_sort/no_init_bubble_sort_safe12.c.smt2
QF_AUFBV/platania/no_init_bubble_sort/no_init_bubble_sort_safe27.c.smt2
QF_AUFBV/platania/no_init_bubble_sort/no_init_bubble_sort_safe7.c.smt2
QF_AUFBV/platania/no_init_bubble_sort/no_init_bubble_sort_safe22.c.smt2
QF_AUFBV/platania/no_init_selection_sort/no_init_selection_sort_safe27.c.smt2
QF_AUFBV/platania/no_init_selection_sort/no_init_selection_sort_unsafe12.c.smt2
QF_AUFBV/platania/no_init_selection_sort/no_init_selection_sort_unsafe27.c.smt2
QF_AUFBV/platania/no_init_selection_sort/no_init_selection_sort_safe12.c.smt2
QF_AUFBV/platania/no_init_selection_sort/no_init_selection_sort_unsafe17.c.smt2
QF_AUFBV/platania/no_init_selection_sort/no_init_selection_sort_unsafe22.c.smt2
QF_AUFBV/platania/no_init_selection_sort/no_init_selection_sort_safe17.c.smt2
QF_AUFBV/platania/no_init_selection_sort/no_init_selection_sort_safe7.c.smt2
QF_AUFBV/platania/no_init_selection_sort/no_init_selection_sort_safe22.c.smt2
QF_AUFBV/platania/no_init_multi_delete/no_init_multi_delete47.smt2
QF_AUFBV/platania/no_init_multi_delete/no_init_multi_delete155.smt2
QF_AUFBV/platania/no_init_multi_delete/no_init_multi_delete195.smt2
QF_AUFBV/platania/no_init_multi_delete/no_init_multi_delete15.smt2
QF_AUFBV/platania/no_init_multi_delete/no_init_multi_delete65.smt2
QF_AUFBV/platania/no_init_multi_delete/no_init_multi_delete35.smt2
QF_AUFBV/platania/no_init_multi_delete/no_init_multi_delete53.smt2
QF_AUFBV/platania/no_init_multi_delete/no_init_multi_delete115.smt2
QF_AUFBV/platania/no_init_multi_delete/no_init_multi_delete105.smt2
QF_AUFBV/platania/no_init_multi_delete/no_init_multi_delete175.smt2
QF_AUFBV/platania/no_init_multi_delete/no_init_multi_delete25.smt2
QF_AUFBV/platania/no_init_multi_delete/no_init_multi_delete125.smt2
QF_AUFBV/platania/no_init_multi_delete/no_init_multi_delete185.smt2
QF_AUFBV/platania/no_init_multi_delete/no_init_multi_delete12.smt2
QF_AUFBV/platania/no_init_multi_delete/no_init_multi_delete95.smt2
QF_AUFBV/platania/no_init_multi_delete/no_init_multi_delete145.smt2
QF_AUFBV/platania/no_init_multi_delete/no_init_multi_delete55.smt2
QF_AUFBV/platania/no_init_multi_delete/no_init_multi_delete85.smt2
QF_AUFBV/platania/no_init_multi_delete/no_init_multi_delete135.smt2
QF_AUFBV/platania/no_init_multi_delete/no_init_multi_delete51.smt2
QF_AUFBV/platania/no_init_multi_delete/no_init_multi_delete49.smt2
QF_AUFBV/platania/no_init_multi_delete/no_init_multi_delete45.smt2
QF_AUFBV/platania/no_init_multi_delete/no_init_multi_delete75.smt2
QF_AUFBV/platania/no_init_multi_delete/no_init_multi_delete165.smt2
QF_AUFBV/platania/no_init_multi_member/no_init_multi_member18.smt2
QF_AUFBV/platania/no_init_multi_member/no_init_multi_member15.smt2
QF_AUFBV/platania/no_init_multi_member/no_init_multi_member12.smt2
QF_AUFBV/platania/no_init_multi_member/no_init_multi_member17.smt2
QF_AUFBV/platania/no_init_multi_member/no_init_multi_member25.smt2
QF_AUFBV/platania/no_init_multi_member/no_init_multi_member14.smt2
QF_AUFBV/platania/no_init_multi_member/no_init_multi_member20.smt2
QF_AUFBV/platania/no_init_multi_member/no_init_multi_member22.smt2
QF_AUFBV/platania/no_init_multi_member/no_init_multi_member19.smt2
QF_AUFBV/platania/no_init_multi_member/no_init_multi_member21.smt2
QF_AUFBV/platania/no_init_multi_member/no_init_multi_member16.smt2
QF_AUFBV/platania/no_init_multi_member/no_init_multi_member23.smt2
QF_AUFBV/platania/no_init_multi_member/no_init_multi_member24.smt2
QF_AUFBV/platania/no_init_simple_delete/no_init_simple_delete185.smt2
QF_AUFBV/platania/no_init_simple_delete/no_init_simple_delete175.smt2
QF_AUFBV/platania/no_init_simple_delete/no_init_simple_delete165.smt2
QF_AUFBV/platania/no_init_simple_delete/no_init_simple_delete195.smt2
QF_AUFBV/dwp_formulas/try5_small_difret_functions_wp_mkfifo.mode_adjust.il.wp.smt2
QF_AUFBV/dwp_formulas/try5_small_difret_functions_wp_shred.isaac_mix.il.wp.smt2
QF_AUFBV/dwp_formulas/try5_small_true_functions_wp_md5sum.md5_process_block.il.wp.smt2
QF_AUFBV/dwp_formulas/try5_small_difret_functions_wp_fmt.fmt_paragraph.il.wp.smt2
QF_AUFBV/dwp_formulas/try5_small_difret_functions_wp_mkdir.mode_adjust.il.wp.smt2
QF_AUFBV/dwp_formulas/try5_small_difret_functions_wp_mknod.mode_adjust.il.wp.smt2
QF_AUFBV/dwp_formulas/try5_small_difret_functions_wp_md5sum.md5_process_block.il.wp.smt2
QF_AUFBV/dwp_formulas/try5_small_noof_functions_wp_md5sum.md5_process_block.il.wp.smt2
QF_AUFBV/dwp_formulas/try5_small_difret_functions_wp_shuf.isaac_mix.il.wp.smt2
QF_AUFBV/pipe/pipe-abs.atlas.smt2
QF_AUFBV/calc2/calc2_sec2_mult_bmc20.atlas.smt2
QF_AUFBV/calc2/calc2_sec2_mult_bmc30.atlas.smt2
QF_AUFBV/calc2/calc2_sec2_bmc25.atlas.smt2
QF_AUFBV/calc2/calc2_sec2_mult_bmc25.atlas.smt2
QF_AUFBV/calc2/calc2_sec2_shifter_mult_bmc30.atlas.smt2
QF_AUFBV/calc2/calc2_sec2_shifter_mult_bmc25.atlas.smt2
QF_AUFBV/calc2/calc2_sec2_adder_bmc25.atlas.smt2
QF_AUFBV/calc2/calc2_sec2_adder_bmc30.atlas.smt2
QF_AUFBV/calc2/calc2_sec2_shifter_bmc25.atlas.smt2
QF_AUFBV/calc2/calc2_sec2_adder_shifter_bmc30.atlas.smt2
QF_AUFBV/calc2/calc2_sec2_bmc30.atlas.smt2
QF_AUFBV/calc2/calc2_sec2_shifter_bmc30.atlas.smt2
QF_AUFBV/brummayerbiere2/countbitstable128.smt2
QF_AUFBV/brummayerbiere2/countbitstableoffbyone0512.smt2
QF_AUFBV/brummayerbiere2/countbitstableoffbyone1024.smt2
QF_AUFBV/brummayerbiere2/countbitstable064.smt2
QF_AUFBV/brummayerbiere2/countbitstableuninit0512.smt2
QF_AUFBV/brummayerbiere2/countbitstableuninit0256.smt2
QF_AUFBV/brummayerbiere2/countbitstable256.smt2
QF_AUFBV/brummayerbiere2/countbitstableoffbyone0256.smt2
QF_AUFBV/brummayerbiere2/countbitstableuninit1024.smt2

------------------------------------------------------------------------------

All benchmarks in sets SMT'12 and Selected can be found at 
http://www.smtlib.org.