SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

Participants
Results

QF_NonLinearIntArith (QF_NIA, QF_NIRA) - Single Query Track

Competition results for the QF_NonLinearIntArith (QF_NIA, QF_NIRA) division in the Single Query Track.

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

Benchmarks: 9197
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	Yices2	Yices2

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
2019-Par4ⁿ	0	7135	5481907.704	5093219.306	7135	4909	2226	2060	2043	17
CVC4	0	6347	4543064.713	4567229.327	6347	4594	1753	2850	2850	0
MathSAT5ⁿ	0	6331	3793979.039	3794165.242	6331	4377	1954	2866	2866	0
Yices2	0	6074	3895818.056	3896055.294	6074	4075	1999	3123	3123	0
Yices2-fixedⁿ	0	6073	3878148.151	3905869.476	6073	4074	1999	3124	3124	0
z3ⁿ	0	5956	3870611.356	3870556.201	5956	4334	1622	3241	2647	6
AProVE	0	3186	6099923.269	7377852.192	3186	3186	0	6009	5935	0
SMT-RAT	0	1998	8812124.534	8813309.03	1998	1801	197	7199	7166	3
2018-SMTRAT-Ratⁿ	0	2	314.192	314.222	2	0	2	0	0	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
2019-Par4ⁿ	0	7183	9513422.984	2631993.077	7183	4952	2231	2012	1995	17
CVC4	0	6347	4543064.713	4567229.327	6347	4594	1753	2850	2850	0
MathSAT5ⁿ	0	6331	3793979.039	3794165.242	6331	4377	1954	2866	2866	0
Yices2	0	6074	3895818.056	3896055.294	6074	4075	1999	3123	3123	0
Yices2-fixedⁿ	0	6073	3878148.151	3905869.476	6073	4074	1999	3124	3124	0
z3ⁿ	0	5956	3870611.356	3870556.201	5956	4334	1622	3241	2647	6
AProVE	0	3186	6099923.269	7377852.192	3186	3186	0	6009	5935	0
SMT-RAT	0	1998	8812124.534	8813309.03	1998	1801	197	7199	7166	3
2018-SMTRAT-Ratⁿ	0	2	314.192	314.222	2	0	2	0	0	0

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
2019-Par4ⁿ	0	4952	2331252.466	647393.097	4952	4952	0	4243	1995	17
CVC4	0	4594	1930954.745	1941324.4	4594	4594	0	4603	2850	0
MathSAT5ⁿ	0	4377	1460544.343	1460341.54	4377	4377	0	4820	2866	0
z3ⁿ	0	4334	1407150.169	1406954.63	4334	4334	0	4863	2647	6
Yices2	0	4075	1655656.317	1655659.928	4075	4075	0	5122	3123	0
Yices2-fixedⁿ	0	4074	1652152.451	1662563.811	4074	4074	0	5123	3124	0
AProVE	0	3186	1932597.783	2839227.499	3186	3186	0	6009	5935	0
SMT-RAT	0	1801	4460184.923	4460626.888	1801	1801	0	7396	7166	3
2018-SMTRAT-Ratⁿ	0	0	0.0	0.0	0	0	0	2	0	0

UNSAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
2019-Par4ⁿ	0	2231	565798.168	160819.05	2231	0	2231	6964	1995	17
Yices2	0	1999	429503.119	429528.287	1999	0	1999	7198	3123	0
Yices2-fixedⁿ	0	1999	427948.481	432431.115	1999	0	1999	7198	3124	0
MathSAT5ⁿ	0	1954	522984.696	522955.182	1954	0	1954	7243	2866	0
CVC4	0	1753	809910.756	815019.956	1753	0	1753	7444	2850	0
z3ⁿ	0	1622	909747.799	909759.109	1622	0	1622	7575	2647	6
SMT-RAT	0	197	2541332.271	2541809.062	197	0	197	9000	7166	3
2018-SMTRAT-Ratⁿ	0	2	314.192	314.222	2	0	2	0	0	0
AProVE	0	0	2410884.399	2790128.222	0	0	0	9195	5935	0

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
2019-Par4ⁿ	0	6288	127657.453	86631.865	6288	4279	2009	2907	2890	17
Yices2	0	5345	104238.735	104050.702	5345	3486	1859	3852	3852	0
Yices2-fixedⁿ	0	5337	104525.715	104405.874	5337	3480	1857	3860	3860	0
MathSAT5ⁿ	0	4687	129123.367	128782.012	4687	3132	1555	4510	4510	0
z3ⁿ	0	4233	139943.251	139696.852	4233	3051	1182	4964	4941	6
CVC4	0	3517	151476.081	151226.567	3517	2359	1158	5680	5680	0
AProVE	0	2404	175808.845	169727.717	2404	2404	0	6791	6717	0
SMT-RAT	0	1333	195238.621	195079.377	1333	1163	170	7864	7857	3
2018-SMTRAT-Ratⁿ	0	0	48.0	48.0	0	0	0	2	2	0

n Non-competing.