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