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	`644448b9207cc0dc085ef0b7843796c7 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	`d83b010be3fc41dd2a2508cfa518e404 bclt.tar.gz`
Beaver-1.0	Susmit Jha	EECS UC Berkeley	94720	QF_BV	beaver.pdf	`84fadb81b50604ad2c64595a018536bd submit-beaver.tar.gz`
Boolector	Robert Brummayer	JKU, Austria	8128	QF_BV, QF_AUFBV	boolector-smtcomp08.pdf	`0183b75e8d341ae6ad321d3ad413950a boolector-0.4.tar`
clsat 0.17f	CLSat Shared Account	Washington University	1551	QF_IDL	description.pdf	`6ab205fed30784efbdf85251d7fb8eab 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	`058c9d87347f6a5639d3ec1b21a6be31 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	`9f4b404a9fcc9ae65f0a99a78c1f19e9 mathsat-smtcomp08.tar.gz`
OpenSMT 0.1	Roberto Bruttomesso	University of Lugano, CH	19112000	QF_UF	sys_desc.pdf	`d70cac78e591bdaee4c16ba3723115cb opensmt.tgz`
sateen-2.1.1	Hyondeuk Kim	University of Colorado at Boulder	2147483647	QF_RDL, QF_IDL	sateen.pdf	`408e43eb37e5ba0044108b8601ee910b Sateen-2.1.1.tgz`
Spear	Domagoj Babic	Cadence Research Laboratories	80085	QF_BV	paper.pdf	`d7290d030d502743faa0d52e8266c103 spear.tar.gz`
SWORD v0.2	Robert Wille	University of Bremen	823	QF_BV	sword.pdf	`9ac92bad90baf3d21361c495e27ca8b6 sword.tgz`
Yices2 (proto c)	Bruno Dutertre	SRI International	665309	QF_UF, QF_RDL, QF_IDL, QF_LRA	yices2proto.pdf	`859475bdcb96243327fdddac0cbff446 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	`250a55cdb8ccd8af7c6aa57074198a9e z3-2008.tar.gz`
Competition seed will be:	97883759 + 8481.60 (rounded) = 97892241 (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