QF_Equality+LinearArith (Single Query Track)

Competition results for the QF_Equality+LinearArith division in the Single Query Track.

Page generated on 2022-08-10 11:17:45 +0000

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

Logics:

• QF_ALIA : 116 benchmarks
• QF_AUFLIA : 539 benchmarks
• QF_UFDTLIRA : 9 benchmarks
• QF_UFIDL : 300 benchmarks
• QF_UFLIA : 300 benchmarks
• QF_UFLRA : 541 benchmarks

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24s Performance (parallel)
smtinterpol	smtinterpol	smtinterpol	Yices2	Yices2

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
z3-4.8.17n	0	1755	79873.917	79863.536	1755	942	813	50	0	50	0
2021-SMTInterpoln	0	1742	95380.955	86876.106	1742	954	788	63	0	53	0
smtinterpol	0	1739	110014.222	98907.984	1739	959	780	66	0	66	0
Yices2	0	1737	88273.846	88288.483	1737	926	811	59	9	59	0
cvc5	0	1717	148345.708	148371.876	1717	923	794	88	0	88	0
MathSATn	0	1714	120373.386	120327.856	1714	907	807	82	9	82	0
veriT	0	1047	142505.484	142516.664	1047	592	455	749	9	91	0
OpenSMT	0	834	10572.049	10562.852	834	552	282	7	964	7	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
z3-4.8.17n	0	1755	79880.157	79861.366	1755	942	813	50	0	50	0
2021-SMTInterpoln	0	1749	96025.815	85970.126	1749	955	794	56	0	46	0
smtinterpol	0	1742	110626.472	97692.333	1742	959	783	63	0	63	0
Yices2	0	1737	88280.596	88286.553	1737	926	811	59	9	59	0
cvc5	0	1717	148365.278	148368.146	1717	923	794	88	0	88	0
MathSATn	0	1714	120389.316	120324.236	1714	907	807	82	9	82	0
veriT	0	1047	142514.934	142513.754	1047	592	455	749	9	91	0
OpenSMT	0	834	10573.949	10562.442	834	552	282	7	964	7	0

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
smtinterpol	0	959	16229.253	13040.692	959	959	0	4	842	63	0
2021-SMTInterpoln	0	955	16953.798	13384.065	955	955	0	8	842	46	0
z3-4.8.17n	0	942	29013.83	29010.777	942	942	0	21	842	50	0
Yices2	0	926	44698.3	44701.536	926	926	0	32	847	59	0
cvc5	0	923	63611.984	63613.566	923	923	0	40	842	88	0
MathSATn	0	907	63558.096	63554.886	907	907	0	51	847	82	0
veriT	0	592	55131.325	55130.028	592	592	0	366	847	91	0
OpenSMT	0	552	8079.537	8070.15	552	552	0	5	1248	7	0

UNSAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
z3-4.8.17n	0	813	48466.327	48450.589	813	0	813	27	965	50	0
Yices2	0	811	41182.296	41185.017	811	0	811	25	969	59	0
MathSATn	0	807	54431.22	54369.349	807	0	807	29	969	82	0
2021-SMTInterpoln	0	794	76672.017	70186.061	794	0	794	46	965	46	0
cvc5	0	794	82353.294	82354.579	794	0	794	46	965	88	0
smtinterpol	0	783	91997.219	82251.642	783	0	783	57	965	63	0
veriT	0	455	84983.609	84983.726	455	0	455	381	969	91	0
OpenSMT	0	282	94.412	92.292	282	0	282	0	1523	7	0

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
z3-4.8.17n	0	1690	3520.773	3499.72	1690	915	775	115	0	115	0
Yices2	0	1688	2933.328	2937.703	1688	908	780	108	9	108	0
2021-SMTInterpoln	0	1660	10522.375	6185.768	1660	924	736	145	0	136	0
smtinterpol	0	1658	11498.036	6789.16	1658	927	731	147	0	147	0
MathSATn	0	1637	4938.749	4907.944	1637	894	743	159	9	159	0
cvc5	0	1581	6648.357	6645.133	1581	884	697	224	0	224	0
veriT	0	933	6905.146	6900.514	933	502	431	863	9	224	0
OpenSMT	0	822	1381.774	1370.066	822	541	281	19	964	19	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.