Benchmarks

SMT-COMP 2016 will use a subset of the benchmarks available within the 2016-05-23 release of SMT-LIB, as described in the competition rules. Specifically, benchmarks with unknown status, bit-vector benchmarks that contain partial operations (i.e., bvudiv, bvurem, bvsdiv, bvsrem or bvsmod), and floating-point benchmarks that contain underspecified operations (i.e., fp.min, fp.max, fp.to_ubv, fp.to_sbv or fp.to_real) will not be used.

The SMT-LIB benchmarks are available in space root/SMT/SMT-LIB benchmarks/2016-05-23 on StarExec.

Main Track

1. Excluded because they contain partial or underspecified operations (e.g., bit-vector division, fp.min).

Application Track

2. For the application track, a benchmark is ineligible if its first check-sat command has unknown status. Otherwise, (some non-empty prefix of) the benchmark is eligible.
3. As there are no eligible benchmarks in SMT-LIB, AUFNIRA is not actually an application track division in SMT-COMP 2016.
4. Benchmark incremental/QF_LIA/UltimateBuchiAutomizer/AliasDarteFeautrierGonnord-SAS2010-loops_true-termination.c.smt2 was excluded because it contained incorrect :status information.

Unsat-Core Track

All unsatisfiable main track benchmarks are eligible for the unsat-core track (with minor modifications, e.g., named assertions). The unsat-core track is experimental in 2016.

Last modified: Tue 23 Oct 2018 09:42 UTC