SMT-Exec: Competitors: 2008

SMT-Exec

General help: Rows in tables are clickable to navigate between different views of the results; hover the cursor over the row to get a description of the view you'll be taken to. Most column headings are clickable to change sort order. Informational notices and links to other result views are available toward the top of many pages.

Jobs: This system is job-driven; the competition run is merely one job. Multiple jobs can be selected for focus at the top right of results pages; doing so merges the results of the selected jobs.

Legend for this page:

job complete

job incomplete

results

no results yet

refreshed with new results

currently running

running hors concours

REFRESHING

Competitors: SMT-COMP 2008

Solver	Submitter	Affiliation	Random Seed	Divisions	System Description	Tarball
Alt-Ergo	Evelyne Contejean	CNRS Universite Paris-Sud	645	AUFLIA+p, AUFLIA-p, AUFLIRA	description.pdf	`ergo.tgz`
Barcelogic 1.3	Albert Oliveras	Technical University of Catalonia	23412432	QF_UF, QF_RDL, QF_IDL, QF_UFIDL, QF_AX, QF_AUFLIA, QF_UFLRA, QF_UFLIA, QF_LRA, QF_LIA	bclt-descript.pdf	`bclt.tar.gz`
Beaver-1.0	Susmit Jha	EECS UC Berkeley	94720	QF_BV	beaver.pdf	`submit-beaver.tar.gz`
Boolector	Robert Brummayer	JKU, Austria	8128	QF_BV, QF_AUFBV	boolector-smtcomp08.pdf	`boolector-0.4.tar`
clsat 0.17f	CLSat Shared Account	Washington University	1551	QF_IDL	description.pdf	`clsat0.17f.tar`
CVC3-1.5	Clark Barrett	New York University	3	QF_UF, QF_RDL, QF_IDL, QF_BV, QF_AUFBV, QF_UFIDL, QF_AX, AUFLIA+p, AUFLIA-p, AUFLIRA, QF_AUFLIA, QF_UFLRA, QF_UFLIA, QF_LRA, QF_LIA	cvc3.pdf	`cvc3-smtcomp2008.tar.gz`
MathSAT-4.2	Alberto Griggio	DISI - University of Trento	54507995	QF_UF, QF_RDL, QF_IDL, QF_BV, QF_UFIDL, QF_UFLRA, QF_UFLIA, QF_LRA, QF_LIA	mathsat_smtcomp08_system_description.pdf	`mathsat-smtcomp08.tar.gz`
OpenSMT 0.1	Roberto Bruttomesso	University of Lugano, CH	19112000	QF_UF	sys_desc.pdf	`opensmt.tgz`
sateen-2.1.1	Hyondeuk Kim	University of Colorado at Boulder	2147483647	QF_RDL, QF_IDL	sateen.pdf	`Sateen-2.1.1.tgz`
Spear	Domagoj Babic	Cadence Research Laboratories	80085	QF_BV	paper.pdf	`spear.tar.gz`
SWORD v0.2	Robert Wille	University of Bremen	823	QF_BV	sword.pdf	`sword.tgz`
Yices2 (proto c)	Bruno Dutertre	SRI International	665309	QF_UF, QF_RDL, QF_IDL, QF_LRA	yices2proto.pdf	`yices2proto-fixed2-smtcomp.tar.gz`
Z3.2	Leonardo de Moura	Microsoft Research	69	QF_UF, QF_RDL, QF_IDL, QF_BV, QF_AUFBV, QF_UFIDL, QF_AX, AUFLIA+p, AUFLIA-p, AUFLIRA, QF_AUFLIA, QF_UFLRA, QF_UFLIA, QF_LRA, QF_LIA	z3.pdf	`z3-2008.tar.gz`
Competition seed will be:	-975858065 + 8481.60 (rounded) = -975849583 (8481.60 was the opening value of the NYSE Composite Index on July 7 2008)

Alt-Ergo

Evelyne Contejean

CNRS Universite Paris-Sud

645

AUFLIA+p, AUFLIA-p, AUFLIRA