QF_NIA (Single Query Track)

Competition results for the QF_NIA logic in the Single Query Track.

Page generated on 2023-07-06 16:04:54 +0000

Benchmarks: 11945
Time Limit: 1200 seconds
Memory Limit: 60 GB

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24s Performance (parallel)
Z3++	Z3++	Z3++	Z3++	Z3++

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
Z3++	0	9990	546309.754	545352.352	9990	6914	3076	1955	1899	0
2022-Z3++-fixedn	0	9603	587797.089	586781.745	9603	6676	2927	2342	2090	0
yices-ismt	0	9406	626660.095	625732.301	9406	6807	2599	2539	917	2
z3-alpha	0	9115	804176.979	803353.908	9115	6084	3031	2830	2822	3
cvc5	0	8040	1771231.912	1776923.044	8040	5762	2278	3905	3900	5
Yices2	0	7619	123276.48	122889.506	7619	5107	2512	4326	4323	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
Z3++	0	9990	546309.754	545352.352	9990	6914	3076	1955	1899	0
2022-Z3++-fixedn	0	9603	587797.089	586781.745	9603	6676	2927	2342	2090	0
yices-ismt	0	9406	626660.095	625732.301	9406	6807	2599	2539	958	2
z3-alpha	0	9115	804176.979	803353.908	9115	6084	3031	2830	2822	3
cvc5	0	8040	1771231.912	1776923.044	8040	5762	2278	3905	3900	5
Yices2	0	7619	123276.48	122889.506	7619	5107	2512	4326	4323	0

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	N/A	Timeout	Memout
Z3++	0	6914	264761.465	264138.363	6914	6914	0	172	4859	1899	0
yices-ismt	0	6807	423837.965	423045.075	6807	6807	0	279	4859	958	2
2022-Z3++-fixedn	0	6676	544036.075	543321.41	6676	6676	0	410	4859	2090	0
z3-alpha	0	6084	545912.283	545513.13	6084	6084	0	1002	4859	2822	3
cvc5	0	5762	1673869.026	1679669.249	5762	5762	0	1324	4859	3900	5
Yices2	0	5107	96073.992	95726.318	5107	5107	0	1979	4859	4323	0

UNSAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	N/A	Timeout	Memout
Z3++	0	3076	281548.29	281213.989	3076	0	3076	272	8597	1899	0
z3-alpha	0	3031	258264.696	257840.778	3031	0	3031	317	8597	2822	3
2022-Z3++-fixedn	0	2927	43761.014	43460.336	2927	0	2927	421	8597	2090	0
yices-ismt	0	2599	202822.13	202687.226	2599	0	2599	749	8597	958	2
Yices2	0	2512	27202.488	27163.188	2512	0	2512	836	8597	4323	0
cvc5	0	2278	97362.886	97253.795	2278	0	2278	1070	8597	3900	5

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
Z3++	0	7160	26172.537	25826.827	7160	5386	1774	4785	4785	0
Yices2	0	6932	16088.838	15786.042	6932	4597	2335	5013	5013	0
yices-ismt	0	6554	15622.082	15450.742	6554	4342	2212	5391	5389	2
z3-alpha	0	6405	35823.319	35327.663	6405	4398	2007	5540	5537	3
2022-Z3++-fixedn	0	6193	22025.44	21681.192	6193	3715	2478	5752	5751	0
cvc5	0	4230	16889.708	16638.457	4230	2329	1901	7715	7710	5

n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.