QF_ALIA (Single Query Track)

Competition results for the QF_ALIA division in the Single Query Track.

Page generated on 2019-07-23 17:56:09 +0000

Benchmarks: 139
Time Limit: 2400 seconds
Memory Limit: 60 GB

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24s Performance (parallel)
Yices 2.6.2	Yices 2.6.2	Yices 2.6.2	Yices 2.6.2	Yices 2.6.2

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
Yices 2.6.2	0	139	57.784	57.948	139	59	80	0		0	0
2018-Yicesn	0	139	61.481	61.647	139	59	80	0		0	0
SMTInterpol	0	139	849.261	413.676	139	59	80	0		0	0
CVC4	0	138	5920.914	5922.027	138	59	79	1		1	0
Z3n	0	134	13291.91	13290.119	134	54	80	5		5	0
Alt-Ergo	0	70	142021.048	133943.646	70	0	70	69		54	0
veriT	0	16	7.645	7.606	16	0	16	123		0	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
Yices 2.6.2	0	139	57.784	57.948	139	59	80	0		0	0
2018-Yicesn	0	139	61.481	61.647	139	59	80	0		0	0
SMTInterpol	0	139	849.261	413.676	139	59	80	0		0	0
CVC4	0	138	5921.154	5922.007	138	59	79	1		1	0
Z3n	0	134	13293.57	13289.869	134	54	80	5		5	0
Alt-Ergo	0	71	154452.518	129673.616	71	0	71	68		49	0
veriT	0	16	7.645	7.606	16	0	16	123		0	0

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
Yices 2.6.2	0	59	51.416	51.42	59	59	0	80	0	0
2018-Yicesn	0	59	54.831	54.843	59	59	0	80	0	0
SMTInterpol	0	59	450.646	179.278	59	59	0	80	0	0
CVC4	0	59	1940.408	1941.108	59	59	0	80	1	0
Z3n	0	54	13203.67	13199.968	54	54	0	85	5	0
veriT	0	0	3.753	3.737	0	0	0	139	0	0
Alt-Ergo	0	0	121389.831	105180.367	0	0	0	139	49	0

UNSAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
Yices 2.6.2	0	80	6.367	6.528	80	0	80	59	0	0
2018-Yicesn	0	80	6.65	6.805	80	0	80	59	0	0
Z3n	0	80	89.9	89.901	80	0	80	59	5	0
SMTInterpol	0	80	398.615	234.399	80	0	80	59	0	0
CVC4	0	79	3980.746	3980.899	79	0	79	60	1	0
Alt-Ergo	0	71	33062.687	24493.249	71	0	71	68	49	0
veriT	0	16	3.892	3.87	16	0	16	123	0	0

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
Yices 2.6.2	0	139	57.784	57.948	139	59	80	0		0	0
2018-Yicesn	0	139	61.481	61.647	139	59	80	0		0	0
SMTInterpol	0	136	767.209	367.851	136	59	77	3		3	0
Z3n	0	118	666.767	663.007	118	39	79	21		21	0
CVC4	0	116	634.852	634.819	116	45	71	23		23	0
Alt-Ergo	0	66	2784.92	1960.728	66	0	66	73		69	0
veriT	0	16	7.645	7.606	16	0	16	123		0	0

n Non-competing.
Abstained: Total of benchmarks in logics in this division that solver chose to abstain from. For SAT/UNSAT scores, this column also includes benchmarks not known to be SAT/UNSAT.