QF_LinearIntArith (Single Query Track)

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

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

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

Logics:

• QF_IDL : 1203 benchmarks
• QF_LIA : 5229 benchmarks
• QF_LIRA : 7 benchmarks

Winners

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

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
2019-Par4n	0	6106	86936.727	25027.076	6106	3863	2243	333	0	321	12
Z3++	0	5819	289357.237	288931.192	5819	3819	2000	613	7	580	14
OpenSMT	0	5816	356193.01	355758.285	5816	3638	2178	616	7	612	0
cvc5	0	5802	369313.977	369092.548	5802	3601	2201	637	0	633	0
Yices2	0	5776	92916.787	92886.907	5776	3615	2161	663	0	664	0
SMTInterpol	0	5444	371590.438	280584.319	5444	3302	2142	995	0	995	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
2019-Par4n	0	6185	271140.027	76724.151	6185	3909	2276	254	0	242	12
Z3++	0	5819	289357.237	288931.192	5819	3819	2000	613	7	580	14
OpenSMT	0	5816	356193.01	355758.285	5816	3638	2178	616	7	612	0
cvc5	0	5802	369313.977	369092.548	5802	3601	2201	637	0	633	0
Yices2	0	5775	91716.967	91686.887	5775	3614	2161	664	0	664	0
SMTInterpol	0	5447	375468.798	283494.387	5447	3303	2144	992	0	992	0

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
2019-Par4n	0	3909	168378.274	48473.233	3909	3909	0	100	2430	242	12
Z3++	0	3819	122928.811	122619.712	3819	3819	0	189	2431	580	14
OpenSMT	0	3638	262121.331	261851.0	3638	3638	0	370	2431	612	0
Yices2	0	3614	72189.631	72166.596	3614	3614	0	395	2430	664	0
cvc5	0	3601	195784.282	195651.689	3601	3601	0	408	2430	633	0
SMTInterpol	0	3303	203585.396	173206.195	3303	3303	0	706	2430	992	0

UNSAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
2019-Par4n	0	2276	102761.753	28250.918	2276	0	2276	55	4108	242	12
cvc5	0	2201	173529.696	173440.859	2201	0	2201	130	4108	633	0
OpenSMT	0	2178	94071.679	93907.286	2178	0	2178	147	4114	612	0
Yices2	0	2161	19527.337	19520.29	2161	0	2161	170	4108	664	0
SMTInterpol	0	2144	171883.402	110288.192	2144	0	2144	187	4108	992	0
Z3++	0	2000	166428.427	166311.48	2000	0	2000	325	4114	580	14

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
2019-Par4n	0	5900	11989.103	4114.556	5900	3721	2179	539	0	527	12
Yices2	0	5453	4882.959	4843.938	5453	3365	2088	986	0	986	0
Z3++	0	4545	9804.337	9679.76	4545	3145	1400	1887	7	1873	14
OpenSMT	0	4244	10281.382	10155.056	4244	2600	1644	2188	7	2184	0
cvc5	0	4127	7013.425	6934.461	4127	2666	1461	2312	0	2312	0
SMTInterpol	0	3862	28254.605	11812.636	3862	2458	1404	2577	0	2577	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.