QF_Equality+LinearArith (QF_ALIA, QF_AUFLIA, QF_UFLIA, QF_UFLRA, QF_UFIDL) - Single Query Track

Competition results for the QF_Equality+LinearArith (QF_ALIA, QF_AUFLIA, QF_UFLIA, QF_UFLRA, QF_UFIDL) division in the Single Query Track.

Page generated on 2020-01-29 22:04:58 +0000

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

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24s Performance (parallel)
Yices2	Yices2	Yices2	Yices2	Yices2

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
Yices2-fixedn	0	1611	5707.44	5703.847	1611	822	789	4	4	0
Yices2	0	1611	5718.591	5704.206	1611	822	789	4	4	0
SMTInterpol	0	1597	40153.773	35001.571	1597	822	775	18	18	0
SMTInterpol-fixedn	0	1597	40190.85	35163.505	1597	822	775	18	18	0
MathSAT5n	0	1594	34619.964	34605.542	1594	821	773	21	21	0
z3n	0	1593	29258.973	29257.705	1593	804	789	22	22	0
CVC4	0	1582	58898.62	58871.024	1582	822	760	33	33	0
veriT	0	1035	60793.003	60779.411	1035	528	507	580	30	0
2019-Yices 2.6.2n	0	881	3176.44	3177.656	881	342	539	2	2	0
Alt-Ergo	0	519	574038.713	442087.236	519	0	519	796	160	8
2019-SMTInterpoln	0	431	4130.707	2865.884	431	250	181	1	1	0
2018-Yicesn	0	300	52.376	53.545	300	231	69	0	0	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
Yices2-fixedn	0	1611	5707.44	5703.847	1611	822	789	4	4	0
Yices2	0	1611	5718.591	5704.206	1611	822	789	4	4	0
SMTInterpol	0	1597	40153.773	35001.571	1597	822	775	18	18	0
SMTInterpol-fixedn	0	1597	40190.85	35163.505	1597	822	775	18	18	0
MathSAT5n	0	1594	34619.964	34605.542	1594	821	773	21	21	0
z3n	0	1593	29258.973	29257.705	1593	804	789	22	22	0
CVC4	0	1582	58898.62	58871.024	1582	822	760	33	33	0
veriT	0	1035	60793.003	60779.411	1035	528	507	580	30	0
2019-Yices 2.6.2n	0	881	3176.44	3177.656	881	342	539	2	2	0
Alt-Ergo	0	526	872716.683	273893.773	526	0	526	789	148	8
2019-SMTInterpoln	0	431	4130.707	2865.884	431	250	181	1	1	0
2018-Yicesn	0	300	52.376	53.545	300	231	69	0	0	0

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
Yices2	0	822	1305.095	1306.668	822	822	0	793	4	0
Yices2-fixedn	0	822	1303.908	1308.229	822	822	0	793	4	0
SMTInterpol	0	822	5215.323	3486.338	822	822	0	793	18	0
SMTInterpol-fixedn	0	822	5268.815	3521.883	822	822	0	793	18	0
CVC4	0	822	4847.955	4845.554	822	822	0	793	33	0
MathSAT5n	0	821	3130.303	3130.936	821	821	0	794	21	0
z3n	0	804	23773.557	23771.643	804	804	0	811	22	0
veriT	0	528	22575.829	22578.577	528	528	0	1087	30	0
2019-Yices 2.6.2n	0	342	57.599	58.155	342	342	0	541	2	0
2019-SMTInterpoln	0	250	2064.865	1399.948	250	250	0	182	1	0
2018-Yicesn	0	231	5.008	5.892	231	231	0	69	0	0
Alt-Ergo	0	0	607649.87	194527.119	0	0	0	1315	148	8

UNSAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
Yices2-fixedn	0	789	3203.632	3195.598	789	0	789	826	4	0
Yices2	0	789	3213.606	3197.508	789	0	789	826	4	0
z3n	0	789	4285.456	4285.962	789	0	789	826	22	0
SMTInterpol	0	775	33578.291	30315.212	775	0	775	840	18	0
SMTInterpol-fixedn	0	775	33562.594	30441.592	775	0	775	840	18	0
MathSAT5n	0	773	30289.981	30274.586	773	0	773	842	21	0
CVC4	0	760	52850.995	52825.37	760	0	760	855	33	0
2019-Yices 2.6.2n	0	539	3118.841	3119.501	539	0	539	344	2	0
Alt-Ergo	0	526	260299.323	78166.594	526	0	526	789	148	8
veriT	0	507	37017.204	37000.794	507	0	507	1108	30	0
2019-SMTInterpoln	0	181	714.992	265.835	181	0	181	251	1	0
2018-Yicesn	0	69	47.368	47.654	69	0	69	231	0	0

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
Yices2	0	1606	584.611	569.654	1606	822	784	9	9	0
Yices2-fixedn	0	1606	576.06	571.935	1606	822	784	9	9	0
z3n	0	1572	1791.675	1787.619	1572	792	780	43	43	0
MathSAT5n	0	1556	2498.835	2477.535	1556	813	743	59	59	0
SMTInterpol-fixedn	0	1556	7352.399	3822.03	1556	815	741	59	59	0
SMTInterpol	0	1556	7454.361	3839.882	1556	815	741	59	59	0
CVC4	0	1488	4114.896	4110.107	1488	804	684	127	127	0
veriT	0	945	4597.702	4576.262	945	467	478	670	134	0
2019-Yices 2.6.2n	0	876	405.43	406.412	876	342	534	7	7	0
2019-SMTInterpoln	0	427	1532.293	656.306	427	246	181	5	5	0
Alt-Ergo	0	364	27516.125	18323.951	364	0	364	951	607	8
2018-Yicesn	0	300	52.376	53.545	300	231	69	0	0	0

n Non-competing.