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

Selected timezone: [UTC]
Get HELP: [navigation|page]

Summary View

The job selection includes smtcomp2008, the official SMT-COMP'08 competition run

Solver	Score	Time
QF_UF (100%)
Yices2 (proto c)	196 / 200	7299.0 s
Z3.2	194 / 200	7653.5 s
MathSAT-4.2	181 / 200	18927.1 s
Barcelogic 1.3	118 / 200	15384.2 s
OpenSMT 0.1	85 / 200	25941.8 s
CVC3-1.5	77 / 200	49914.8 s
Z3 0.1, 2007 winner	117 / 200	20936.8 s

Solver	Score	Time
QF_RDL (100%)
Z3.2	169 / 170	5740.3 s
Yices2 (proto c)	169 / 170	8141.5 s
MathSAT-4.2	167 / 170	8324.9 s
sateen-2.1.1	167 / 170	9705.3 s
Barcelogic 1.3	166 / 170	8967.8 s
CVC3-1.5	73 / 170	21045.4 s
Yices 1.0.10, 2007 winner	167 / 170	8760.6 s

Solver	Score	Time
QF_IDL (100%)
Barcelogic 1.3	140 / 203	14895.1 s
Z3.2	139 / 203	15359.4 s
sateen-2.1.1	132 / 203	19487.0 s
Yices2 (proto c)	130 / 203	12854.4 s
MathSAT-4.2	129 / 203	20095.2 s
clsat 0.17f	79 / 203	33050.8 s
CVC3-1.5	49 / 203	8339.2 s
Z3 0.1, 2007 winner	130 / 203	18436.8 s

Solver	Score	Time
QF_BV (100%)
Boolector	192 / 200	3502.5 s
Z3.2	174 / 200	10971.2 s
Beaver-1.0	168 / 200	7186.4 s
MathSAT-4.2	168 / 200	10034.9 s
SWORD v0.2	146 / 200	3630.3 s
Spear	146 / 200	28801.1 s
CVC3-1.5	137 / 200	61943.0 s
Spear v1.9 (fh-1-2), 2007 winner	100 / 200	17289.3 s

Solver	Score	Time
QF_AUFBV (100%)
Boolector	180 / 200	4752.8 s
Z3.2	164 / 200	16650.4 s
CVC3-1.5	77 / 200	7728.9 s
Z3 0.1, 2007 winner	116 / 200	6589.6 s

Solver	Score	Time
QF_UFIDL (100%)
Z3.2	198 / 203	2334.4 s
Barcelogic 1.3	197 / 203	3385.5 s
MathSAT-4.2	194 / 203	8210.2 s
CVC3-1.5	127 / 203	10140.5 s
Yices 1.0.10, 2007 winner	197 / 203	1173.3 s

Solver	Score	Time
QF_AX (100%)
Barcelogic 1.3	200 / 200	13.5 s
Z3.2	200 / 200	17.3 s
CVC3-1.5	195 / 200	2820.2 s

Solver	Score	Time
AUFLIA+p (100%)
Z3.2	194 / 201	20.9 s
CVC3-1.5	185 / 201	157.4 s
Z3 0.1, 2007 winner	191 / 201	95.2 s
Alt-Ergo (revised)	44 / 201	20.8 s
Alt-Ergo	-86	21.0 s

Solver	Score	Time
AUFLIA-p (100%)
Z3.2	193 / 201	19.4 s
CVC3-1.5	161 / 201	1721.0 s
Z3 0.1, 2007 winner	191 / 201	34.4 s
Alt-Ergo (revised)	52 / 201	1858.1 s
Alt-Ergo	-54	1858.1 s

Solver	Score	Time
AUFLIRA (100%)
Z3.2	198 / 200	1018.0 s
CVC3-1.5	147 / 200	5275.6 s
CVC3 1.2, 2007 winner	147 / 200	7619.1 s
Alt-Ergo (revised)	68 / 200	7334.5 s
Alt-Ergo	-317	7461.3 s

Solver	Score	Time
QF_AUFLIA (100%)
Z3.2	206 / 206	195.3 s
Barcelogic 1.3	206 / 206	5572.5 s
CVC3-1.5	157 / 206	9930.7 s
Yices 1.0.10, 2007 winner	206 / 206	585.8 s

Solver	Score	Time
QF_UFLRA (100%)
Z3.2	200 / 200	15.9 s
MathSAT-4.2	200 / 200	106.1 s
Barcelogic 1.3	200 / 200	1630.2 s
CVC3-1.5	184 / 200	4941.7 s

Solver	Score	Time
QF_UFLIA (100%)
Z3.2	202 / 202	201.0 s
MathSAT-4.2	202 / 202	836.6 s
Barcelogic 1.3	202 / 202	3353.5 s
CVC3-1.5	161 / 202	4793.3 s
Yices 1.0.10, 2007 winner	202 / 202	154.7 s

Solver	Score	Time
QF_LRA (100%)
Yices2 (proto c)	184 / 202	4899.1 s
Z3.2	183 / 202	3817.6 s
MathSAT-4.2	182 / 202	6941.6 s
Barcelogic 1.3	182 / 202	11316.7 s
CVC3-1.5	68 / 202	14121.1 s
Yices 1.0.10, 2007 winner	182 / 202	5214.5 s

Solver	Score	Time
QF_LIA (100%)
Z3.2	203 / 205	5104.5 s
MathSAT-4.2	192 / 205	55673.3 s
CVC3-1.5	124 / 205	36294.4 s
Barcelogic 1.3	69 / 205	11636.0 s
Yices 1.0.10, 2007 winner	159 / 205	47754.8 s

Refresh: none|10s|20s|30s|1m|2m|5m

Logged in as: guest (access R/O nosubmit noexec) login

REFRESHING

Refreshing...

July 02 2009 22:40:34 CDT | 0.85s | 619.1K