SMT-COMP 2014 benchmarks

The SMT Competition will use a subset of the benchmarks available within SMT-LIB, as described in the competition rules. New benchmarks are especially encouraged by the May 15 deadline. The set of benchmarks will be announced as soon as is feasible after that deadline. Please adhere to the following instructions in submitting new benchmarks:

• Benchmarks should be organized into separate directories by logic.
• Within each logic, there should be one or more directories containing the benchmarks - you can choose the names of the directories, but they should be different from any names currently existing in SMT-LIB for that logic. Each benchmark should contain the following metadata:

  (set-logic <logic>)
  (set-info :source |<information about where the benchmark came from
  including author contact, paper citations, etc.>|)
  (set-info :smt-lib-version 2.0)
  (set-info :category <either "industrial", "crafted", or "random">) 
  (set-info :status <either sat, unsat, or unknown>)
  

  In :category, the quotes are needed in the benchmark file.

Thanks to the following for new benchmarks in 2014:

• Clark Barrett
• Philipp Wendler -rec'd
• Aaron Tomb et al. (Galois) -rec'd
• Gergely Kovasznai
• Matthias Heizmann
• Hristina Palikareva
• ...

Last modified: Tue 17 Feb 2015 15:00 UTC