Benchmarks

For the 2009 competition, QF_UF eq_diamond benchmarks are ineligible for competition, as are (of course) any unknown-status benchmarks, as are bitvector benchmarks that depend on the semantics of divide-by-zero (a list of such bitvector benchmarks is here, the satisifiability of all other bitvector benchmarks in SMT-LIB with division operators at the time of writing does not depend on the interpretation of divide-by-zero). This list was determined by CVC3's type correctness conditions, which were then checked by several independent SMT solvers.

You can download just the set of benchmarks used for SMT-COMP 2009, in scrambled form.

Last modified: Tue 17 Feb 2015 15:03 UTC