QF_NonLinearIntArith (Single Query Track)

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

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

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

Logics:

• QF_NIA : 11945 benchmarks
• QF_NIRA : 2 benchmarks

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	Abstained	Timeout	Memout
Z3++	0	9990	546309.754	545352.352	9990	6914	3076	1955	2	1899	0
2022-Z3++-fixedn	0	9603	587797.089	586781.745	9603	6676	2927	2342	2	2090	0
yices-ismt	0	9406	626660.095	625732.301	9406	6807	2599	2539	2	917	2
z3-alpha	0	9115	804176.979	803353.908	9115	6084	3031	2830	2	2822	3
cvc5	0	8041	1771469.342	1777160.516	8041	5762	2279	3906	0	3901	5
Yices2	0	7619	123276.48	122889.506	7619	5107	2512	4328	0	4325	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
Z3++	0	9990	546309.754	545352.352	9990	6914	3076	1955	2	1899	0
2022-Z3++-fixedn	0	9603	587797.089	586781.745	9603	6676	2927	2342	2	2090	0
yices-ismt	0	9406	626660.095	625732.301	9406	6807	2599	2539	2	958	2
z3-alpha	0	9115	804176.979	803353.908	9115	6084	3031	2830	2	2822	3
cvc5	0	8041	1771469.342	1777160.516	8041	5762	2279	3906	0	3901	5
Yices2	0	7619	123276.48	122889.506	7619	5107	2512	4328	0	4325	0

SAT Performance

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

UNSAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
Z3++	0	3076	281548.29	281213.989	3076	0	3076	272	8599	1899	0
z3-alpha	0	3031	258264.696	257840.778	3031	0	3031	317	8599	2822	3
2022-Z3++-fixedn	0	2927	43761.014	43460.336	2927	0	2927	421	8599	2090	0
yices-ismt	0	2599	202822.13	202687.226	2599	0	2599	749	8599	958	2
Yices2	0	2512	27202.488	27163.188	2512	0	2512	837	8598	4325	0
cvc5	0	2279	97600.316	97491.267	2279	0	2279	1070	8598	3901	5

24 seconds Performance

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

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.