SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2012

Rules
Benchmarks
Tools
Specs
Participants
Results
Report

Participants

These solvers have been submitted to SMT-COMP 2012 or were entered as non-competing solvers by the organizers for comparison.

Solver Main Track Application Track Unsat-core Track (Demonstration) Exhibition Track (Demonstration) System description Contact(s)
4Simp X AbzizPortfolio Trevor Hansen (University of Melbourne)
AbzizPortfolio X AbzizPortfolio Mohammed Abdul Aziz (University of Cairo)
Boolector X Boolector Armin Biere (Johannes Kepler University, Linz)
CVC3 v2.4.2 X X Morgan Deters (NYU)
CVC4 1.0rc.3931 X X CVC4 ACSys Group (NYU)
MathSAT-HeavyBV X MathSAT-HeavyBV Bas Schaffsma (University of Trento and FBK)
MathSAT5-smtcomp12 X X X X MathSAT5 Alberto Griggio (University of Trento and FBK)
SMTInterpol X X X X SMTInterpol Jochen Hoenicke (University of Freiburg)
SONOLAR X SONOLAR Florian Lapschies (University of Bremen)
STP2 X STP2 Trevor Hansen (University of Melbourne) and Vijay Ganesh (MIT)
Tiffany de Wintermonte & Sonolar X TDW Trevor Hansen (University of Melbourne)
Boolector 1.5.23-833, 2011 winnern X
CVC3 v2.4, 2011 winnern X
CVC4 1.0.rc.3970, patched resubmissionn X
MathSAT5, 2010 winner, tied Z3 in QF_UFLRA in 2011n X
Z3, 2011 winnern X X X
Total 16 3 2 5

n. Non-competing.

Divisions

These are the logic divisions in which each solver is participating.

Solver AUFLIA-p AUFLIA+p AUFNIRA QF_AUFBV QF_BV QF_IDL QF_UFLIA QF_UFLRA
4Simp X
AbzizPortfolio X
Boolector X X
CVC3 v2.4.2 X X X X X X X X
CVC4 1.0rc.3931 X X X X X X X
MathSAT-HeavyBV X
MathSAT5-smtcomp12 X X X X
SMTInterpol X X
SONOLAR X X
STP2 X
Tiffany de Wintermonte X
Boolector 1.5.23-833, 2011 winner X
CVC3 v2.4, 2011 winner X
CVC4 1.0.rc.3970, patched resubmission X X
MathSAT5, 2010 winner, tied Z3 in QF_UFLRA in 2011 X
Z3, 2011 winner X X X X X X

Application Track

Solver QF_UFLIA QF_LIA QF_LRA
MathSAT5-smtcomp12 X X X
SMTInterpol X X X
Z3, 2011 winner X X X

Unsat Core Track (Demonstration)

Solver QF_BV QF_LIA QF_LRA
MathSAT5-smtcomp12 X X X
SMTInterpol X X
Z3, 2011 winner X X

Exhibition Track (Demonstration)

Solver QF_AUFLIA QF_LIA QF_LRA QF_UF
CVC3 v2.4.2 X X X X
CVC4 1.0rc.3931 X X X X
MathSAT5-smtcomp12 X X X X
SMTInterpol X X X
Z3, 2011 winner X X X X