Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005)

Clark Barrett, Leonardo De Moura, Aaron Stump

Research output: Contribution to journalArticle


The Satisfiability Modulo Theories Competition (SMT-COMP) is intended to spark further advances in the decision procedures field, especially for applications in hardware and software verification. Public competitions are a well-known means of stimulating advancement in automated reasoning. Evaluation of SMT solvers entered in SMT-COMP took place while CAV 2005 was meeting. Twelve solvers were entered; 1,352 benchmarks were collected in seven different divisions.

Original languageEnglish (US)
Pages (from-to)373-390
Number of pages18
JournalJournal of Automated Reasoning
Issue number4
StatePublished - Nov 1 2005



  • Competition
  • Decision procedures
  • Satisfiability modulo theories

ASJC Scopus subject areas

  • Software
  • Computational Theory and Mathematics
  • Artificial Intelligence

Cite this