Benchmarks

The 2010 SMT competition is the first to use benchmarks conforming to the SMT-LIB 2.0 specification.

SMT-LIB 2.0 benchmarks are available here.

For the 2010 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.

Last modified: Tue 17 Feb 2015 15:01 UTC