QF_UFLIA (Single Query Track)

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

Page generated on 2020-07-04 11:46:59 +0000

Benchmarks: 300
Time Limit: 1200 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	Abstained	Timeout	Memout
2018-Yicesn	0	300	52.376	53.545	300	231	69	0		0	0
Yices2-fixedn	0	300	66.073	56.288	300	231	69	0		0	0
Yices2	0	300	73.354	55.636	300	231	69	0		0	0
z3n	0	300	147.535	147.592	300	231	69	0		0	0
CVC4	0	300	565.883	565.866	300	231	69	0		0	0
SMTInterpol	0	300	2423.497	1764.278	300	231	69	0		0	0
SMTInterpol-fixedn	0	300	2434.247	1811.616	300	231	69	0		0	0
MathSAT5n	0	298	4640.648	4641.692	298	230	68	2		2	0
veriT	0	273	25859.468	25839.299	273	206	67	27		7	0
Alt-Ergo	0	64	92381.571	87739.173	64	0	64	236		60	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
2018-Yicesn	0	300	52.376	53.545	300	231	69	0		0	0
Yices2	0	300	73.354	55.636	300	231	69	0		0	0
Yices2-fixedn	0	300	66.073	56.288	300	231	69	0		0	0
z3n	0	300	147.535	147.592	300	231	69	0		0	0
CVC4	0	300	565.883	565.866	300	231	69	0		0	0
SMTInterpol	0	300	2423.497	1764.278	300	231	69	0		0	0
SMTInterpol-fixedn	0	300	2434.247	1811.616	300	231	69	0		0	0
MathSAT5n	0	298	4640.978	4641.612	298	230	68	2		2	0
veriT	0	273	25860.048	25839.029	273	206	67	27		7	0
Alt-Ergo	0	65	102569.951	86021.328	65	0	65	235		57	0

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
Yices2	0	231	4.595	5.25	231	231	0	69	0	0
Yices2-fixedn	0	231	4.567	5.84	231	231	0	69	0	0
2018-Yicesn	0	231	5.008	5.892	231	231	0	69	0	0
z3n	0	231	30.12	30.149	231	231	0	69	0	0
CVC4	0	231	135.741	135.705	231	231	0	69	0	0
SMTInterpol	0	231	1776.429	1303.939	231	231	0	69	0	0
SMTInterpol-fixedn	0	231	1786.932	1337.729	231	231	0	69	0	0
MathSAT5n	0	230	1694.944	1695.009	230	230	0	70	2	0
veriT	0	206	21291.699	21292.956	206	206	0	94	7	0
Alt-Ergo	0	0	95344.067	80602.214	0	0	0	300	57	0

UNSAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
2018-Yicesn	0	69	47.368	47.654	69	0	69	231	0	0
Yices2	0	69	68.758	50.386	69	0	69	231	0	0
Yices2-fixedn	0	69	61.506	50.448	69	0	69	231	0	0
z3n	0	69	117.414	117.443	69	0	69	231	0	0
CVC4	0	69	430.142	430.161	69	0	69	231	0	0
SMTInterpol	0	69	647.068	460.339	69	0	69	231	0	0
SMTInterpol-fixedn	0	69	647.315	473.888	69	0	69	231	0	0
MathSAT5n	0	68	2946.034	2946.602	68	0	68	232	2	0
veriT	0	67	4568.349	4546.073	67	0	67	233	7	0
Alt-Ergo	0	65	7225.883	5419.115	65	0	65	235	57	0

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
2018-Yicesn	0	300	52.376	53.545	300	231	69	0		0	0
Yices2	0	300	73.354	55.636	300	231	69	0		0	0
Yices2-fixedn	0	300	66.073	56.288	300	231	69	0		0	0
z3n	0	299	94.222	94.269	299	231	68	1		1	0
CVC4	0	295	345.45	345.404	295	231	64	5		5	0
SMTInterpol-fixedn	0	294	1032.573	506.967	294	228	66	6		6	0
SMTInterpol	0	294	1086.366	527.095	294	228	66	6		6	0
MathSAT5n	0	289	402.741	402.785	289	224	65	11		11	0
veriT	0	202	3079.26	3056.821	202	145	57	98		88	0
Alt-Ergo	0	62	5280.269	3526.118	62	0	62	238		117	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.