QF_Equality+NonLinearArith (QF_UFNRA, QF_UFNIA, QF_ANIA, QF_AUFNIA) - Single Query Track

Competition results for the QF_Equality+NonLinearArith (QF_UFNRA, QF_UFNIA, QF_ANIA, QF_AUFNIA) division in the Single Query Track.

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

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

Winners

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

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
CVC4	0	390	30758.296	30765.445	390	295	95	40	23	0
MathSAT5n	0	371	62156.761	62166.121	371	275	96	59	51	0
2019-CVC4n	0	365	14332.272	14337.216	365	281	84	29	11	0
z3n	0	344	74158.273	74149.262	344	251	93	86	54	0
Yices2	0	303	37411.201	37381.179	303	229	74	24	24	0
Yices2-fixedn	0	303	37541.615	37547.904	303	229	74	24	24	0
Alt-Ergo	0	51	84149.632	76628.651	51	0	51	379	34	0
2019-Par4n	0	26	5742.812	2873.927	26	24	2	1	1	0
2019-MathSAT-defaultn	0	9	3.653	3.653	9	2	7	0	0	0
veriT+raSAT+Redlog	0	1	31193.657	31200.89	1	1	0	26	26	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
CVC4	0	390	30758.296	30765.445	390	295	95	40	23	0
MathSAT5n	0	371	62156.761	62166.121	371	275	96	59	51	0
2019-CVC4n	0	365	14332.272	14337.216	365	281	84	29	11	0
z3n	0	344	74158.273	74149.262	344	251	93	86	54	0
Yices2	0	303	37411.201	37381.179	303	229	74	24	24	0
Yices2-fixedn	0	303	37541.615	37547.904	303	229	74	24	24	0
Alt-Ergo	0	51	150363.192	43030.131	51	0	51	379	34	0
2019-Par4n	0	26	5742.812	2873.927	26	24	2	1	1	0
2019-MathSAT-defaultn	0	9	3.653	3.653	9	2	7	0	0	0
veriT+raSAT+Redlog	0	1	31193.657	31200.89	1	1	0	26	26	0

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
CVC4	0	295	26656.589	26663.02	295	295	0	135	23	0
2019-CVC4n	0	281	10078.511	10082.28	281	281	0	113	11	0
MathSAT5n	0	275	45897.127	45903.264	275	275	0	155	51	0
z3n	0	251	64549.904	64539.312	251	251	0	179	54	0
Yices2	0	229	12212.905	12177.814	229	229	0	98	24	0
Yices2-fixedn	0	229	12342.551	12344.233	229	229	0	98	24	0
2019-Par4n	0	24	5742.799	2873.675	24	24	0	3	1	0
2019-MathSAT-defaultn	0	2	0.54	0.54	2	2	0	7	0	0
veriT+raSAT+Redlog	0	1	28794.267	28800.86	1	1	0	26	26	0
Alt-Ergo	0	0	126861.46	37109.44	0	0	0	430	34	0

UNSAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
MathSAT5n	0	96	10260.534	10262.626	96	0	96	334	51	0
CVC4	0	95	2805.826	2806.367	95	0	95	335	23	0
z3n	0	93	5776.927	5777.91	93	0	93	337	54	0
2019-CVC4n	0	84	4108.554	4109.737	84	0	84	310	11	0
Yices2	0	74	19198.936	19203.205	74	0	74	253	24	0
Yices2-fixedn	0	74	19199.364	19203.281	74	0	74	253	24	0
Alt-Ergo	0	51	23500.136	5920.176	51	0	51	379	34	0
2019-MathSAT-defaultn	0	7	3.113	3.113	7	0	7	2	0	0
2019-Par4n	0	2	0.012	0.252	2	0	2	25	1	0
veriT+raSAT+Redlog	0	0	2399.39	2400.03	0	0	0	27	26	0

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
CVC4	0	372	1267.109	1267.12	372	281	91	58	44	0
MathSAT5n	0	362	1664.829	1663.908	362	271	91	68	60	0
2019-CVC4n	0	356	706.434	706.504	356	276	80	38	22	0
z3n	0	321	2542.366	2521.78	321	229	92	109	87	0
Yices2	0	276	1254.603	1254.839	276	202	74	51	51	0
Yices2-fixedn	0	276	1254.86	1255.591	276	202	74	51	51	0
Alt-Ergo	0	43	2130.041	1420.121	43	0	43	387	47	0
2019-Par4n	0	19	348.712	271.892	19	17	2	8	8	0
2019-MathSAT-defaultn	0	9	3.653	3.653	9	2	7	0	0	0
veriT+raSAT+Redlog	0	1	624.007	624.01	1	1	0	26	26	0

n Non-competing.