Home Intro Tools Specs Thanks SMT-LIB Previous


These benchmarks and tools are subject to change until their respective freeze dates, as documented in the SMT-COMP rules.

Application track Benchmarks

Unsat core benchmarks

The unsat core benchmarks are the subset of the benchmarks from the indicated logics that are unsatisfiable; the benchmarks themselves have been modified to include names for the assertions. Per the SMTLIB standard, the benchmarks are allowed to contain a mix of named and unmaned formulae, though ordinarily, all top-level formulae will have names. The names may be scrambled by the benchmark scrambler.

Format for results files

Each tarball contains one or two status files for each benchmark:

These files contain one status per line, corresponding to the series of (check-sat) commands in the benchmarks.

Each status line (where different from "unknown") has been determined by running at least 3 different SMT solvers on the set of instances resulted from "unfolding" each incremental benchmark using the scrambler. For *.results.txt, all the results different from "unknown" have been reported by at least 2 different solvers, whereas all the status lines generated by a single solver only (because e.g. the others timed out) have been replaced with "unknown". For *.results_untrusted.txt, the single-solver answer is also included. However, they are marked with an "# untrusted" comment.

Home Intro Tools Specs Thanks SMT-LIB Previous

Last modified: Tue 17 Feb 2015 14:57 UTC
Valid XHTML 1.0 Valid CSS!