Participants

SMT-COMP 2014 Participants

These solvers have expressed intention to participate in SMT-COMP 2014.

Solver	Main Track	Application Track	Preliminary Version Solver ID	Final Version Solver ID	Seed	System Description	Contacts
4Simp	X	-	916	1228 (4-Simp 2014) config 1720 default	20324	?	Trevor Hansen (thansen@csse.unimelb.edu.au)
abziz_portfolio_all_features	X	-	912	1275 abziz_portfolio_all_features config 1803 default	21381	?	Mohammad Abdul Aziz (mohammad.abdulaziz8@gmail.com)
abziz_portfolio_min_features	X	-	950	1273 abziz_portfolio_min_features config 1801 default	21381	?	Mohammad Abdul Aziz (mohammad.abdulaziz8@gmail.com)
AProVE	X	-	865	1229 config 1721 default	2094937	AProVE	Carsten Fuhs (c.fuhs@cs.ucl.ac.uk)
Boolector	X	-	911 : config 1136:	1218 config 1703 boolector	42	Boolector	Mathias Preiner (mathias.preiner@jku.at), Aina Niemetz (aina.niemetz@jku.at), Armin Biere (biere@jku.at)
Boolector (dual propagation)	X	-	911 : config 1134	1218 config 1701 boolectord	42	Boolector	Mathias Preiner (mathias.preiner@jku.at), Aina Niemetz (aina.niemetz@jku.at), Armin Biere (biere@jku.at)
Boolector (justification)	X	-	911 : config 1135	1218 config 1702 boolectorj	42	Boolector	Mathias Preiner (mathias.preiner@jku.at), Aina Niemetz (aina.niemetz@jku.at), Armin Biere (biere@jku.at)
CVC3	X	X	900	1262 config 1785 default	33333	CVC3	Clark Barrett (barrett@cs.nyu.edu), Morgan Deters (mdeters@cs.nyu.edu)
CVC4	X	X	898; application track=899	1257 CVC4 f7118b2: config 1778 app config 1779 application	44444	CVC4	Clark Barrett (barrett@cs.nyu.edu), Morgan Deters (mdeters@cs.nyu.edu)
Kleaver-STP	X	-	893	1196 Kleaver-indie-more-typed config 1738 kleaver_indie_1	12739	Kleaver	Hristina Palikareva (h.palikareva@imperial.ac.uk), Cristian Cadar (c.cadar@imperial.ac.uk)
Kleaver-portfolio	X	-	894	1196 Kleaver-indie-more-typed config 1740 kleaver_portfolio	12739	Kleaver	Hristina Palikareva (h.palikareva@imperial.ac.uk), Cristian Cadar (c.cadar@imperial.ac.uk)
OpenSMT2	X	-	921	1204 OpenSMT2-2014-06-14b config 1789 default	1984	OpenSMT	Antti Hyvärinen (antti.hyvarinen@gmail.com)
raSAT	X	-	922	1199 raSAT-main-track-final config 1654 default.sh	18643	raSAT	Tung Vu Xuan (tungvx@jaist.ac.jp)
SMTInterpol	X	X	1075 smtinterpol-2.1-118-g3dada2f	1075 smtinterpol-2.1-118-g3dada2f config 1375 default	3154861623	SMTInterpol	Jochen Hoenicke (hoenicke@informatik.uni-freiburg.de), Jürgen Christ (christj@informatik.uni-freiburg.de)
sonolar (sonolar_smtcomp-2014)	X	-	938	938 config 1173 default	4	SONOLAR	Florian Lapschies (florian@informatik.uni-bremen.de)
STP-CryptoMiniSat4	X	-	968	1240 stp-cryptominisat4 config 1750 default	1337	STP-CryptoMiniSat4	Mate Soos (florian@informatik.uni-bremen.de)
veriT	X	-	860	1269 veriT-smtcomp2014 config 1797 default	1027	veriT	David Deharbe (david.deharbe@loria.fr), Pascal Fontaine (Pascal.Fontaine@inria.fr)
Yices2	X	X	1095 (config=default); app track config=incremental	1259 Yices-2.2.1-smtcomp2014 config 1781 default app config 1782 incremental	22908	Yices	Bruno Dutertre (bruno@csl.sri.com)
MathSAT 5ⁿ	X	X	174	1079 config 1384 default	-	-	-
Z3ⁿ	X	X	1286 config 1815 default; app ?		-	-	-

n. Non-competitive.

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

Solver	ALIA¹	AUFLIA¹	AUFLIRA¹	AUFNIRA^1,2	BV¹	LIA¹	LRA¹	NIA¹	NRA¹	QF_ABV¹	QF_ALIA¹	QF_AUFBV¹	QF_AUFLIA^1,2	QF_AX¹	QF_BV^1,2	QF_IDL¹	QF_LIA^1,2	QF_LRA^1,2	QF_NIA¹	QF_NRA¹	QF_RDL¹	QF_UF¹	QF_UFBV¹	QF_UFIDL¹	QF_UFLIA^1,2	QF_UFLRA^1,2	QF_UFNIA¹	QF_UFNRA¹	UF¹	UFBV¹	UFIDL¹	UFLIA¹	UFLRA^1,2	UFNIA¹
4Simp¹															X
Abziz¹															X
Abziz2¹															X
AProVE¹																			X
Boolector¹															X
Boolector-d¹										X
Boolector-j¹										X
CVC3^1,2	X	X	X	X	X	X	X	X	X										X	X							X	X	X	X	X	X	X	X
CVC4^1,2	X	X	X	X	X	X	X	X	X	X	X	X	X	X	X	X	X	X	X	X	X	X	X	X	X	X	X	X	X	X	X	X	X	X
Kleaver-STP¹										X
Kleaver-portfolio¹										X
OpenSMT2¹																						X
raSAT¹																				X
SMTInterpol^1,2											X		X	X			X	X				X			X	X
SONOLAR¹										X					X
STP-CryptoMiniSat4¹															X
veriT¹	X	X	X			X	X						X			X	X	X			X	X		X	X	X			X			X	X
Yices2^1,2										X	X	X	X	X	X	X	X	X			X	X	X	X	X	X
MathSAT5^n,1,2										X	X	X	X	X	X		X	X				X	X		X	X
Z3^n,1,2	X	X	X	X	X	X	X	X	X	X	X	X	X	X	X	X	X	X	X	X	X	X	X	X	X	X	X	X	X	X	X	X	X	X

1. Main Track.
2. Application Track.

SL-COMP 2014 Participants

These are the solvers participating in the Separation Logic competition 2014 (SL-COMP 2014). This is a separate competition being conducted with SMT-like solvers that solve encodings of separation logic problems. It is separate from SMT-COMP, though it is using the same infrastructure and being conducted by the same organizing committee. The relationship of the associated logic to SMT-LIB is currently under discussion.

Solver	Preliminary version solver id	Final version solver id	System description	Contacts
Cyclist-SL	1136	1136 config 1487 default pre: 113 SL-CYCLIST3	Cyclist-SL	Nikos Gorogiannis (nikos.gorogiannis@gmail.com)
SLSAT	1137	1137 config 1488 default pre: 117 SL-SAT3	SLSAT	Nikos Gorogiannis (nikos.gorogiannis@gmail.com)
Asterix	986	986 config 1233 default.sh pre: none	Asterix	Juan A. Navarro Perez (juan.navarro@ucl.ac.uk), Andrey Rybalchenko (rybal@microsoft.com)
SLEEK	1084 (default configuration)	1277 sleek-05 config 1806 default pre: 115 SL-SLEEK3; late correction for output format: 1297 sleek-06, config 1834 default	SLEEK	Le Quang Loc (locle@comp.nus.edu.sg), Chin Wei Ngan (chinwn@comp.nus.edu.sg)
SLIDE	920	1255 (SLIDE-final) config 1775 SLD_Input pre: 116 SL-SLIDE3	SLIDE	Adam Rogalewicz (rogalew@fit.vutbr.cz), Radu IOSIF ( Radu.Iosif@imag.fr), Tomas Vojnar (vojnar@fit.vutbr.cz)
SPEN	971	1280 SPEN 1.09 config 1809 spen.sh pre: 118 SL-SPEN3	SPEN	Mihaela Sighireanu (mihaela.sighireanu@gmail.com)

These are the benchmark divisions for SL-COMP 2014 in which each solver is competing.

Solver	UDB_sat	UDB_entl	sll0a_sat	sll0a_entl	FDB_entl
Asterix			X	X
Cyclist-SL		X		X	X
SLSAT	X		X
SLEEK	X	X	X	X	X
SLIDE		X			X
SPEN			X	X	X