QF_UFDT (Single Query Track)

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

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

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

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24s Performance (parallel)
cvc5	cvc5	cvc5	cvc5	SMTInterpol

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
2022-z3-4.8.17n	0	98	35999.15	36003.645	98	6	92	102	102	0
cvc5	0	96	46826.618	46778.053	96	22	74	104	104	0
SMTInterpol	0	38	17482.522	13364.529	38	20	18	162	162	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
2022-z3-4.8.17n	0	98	35999.15	36003.645	98	6	92	102	102	0
cvc5	0	96	46826.618	46778.053	96	22	74	104	104	0
SMTInterpol	0	47	30552.153	21593.211	47	21	26	153	153	0

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	N/A	Timeout	Memout
cvc5	0	22	10467.154	10469.121	22	22	0	78	100	104	0
SMTInterpol	0	21	7814.207	7405.416	21	21	0	79	100	153	0
2022-z3-4.8.17n	0	6	3027.498	3027.77	6	6	0	94	100	102	0

UNSAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	N/A	Timeout	Memout
2022-z3-4.8.17n	0	92	32971.652	32975.875	92	0	92	8	100	102	0
cvc5	0	74	36359.464	36308.932	74	0	74	26	100	104	0
SMTInterpol	0	26	22737.945	14187.795	26	0	26	74	100	153	0

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
SMTInterpol	0	3	79.914	45.508	3	3	0	197	197	0
2022-z3-4.8.17n	0	1	23.823	23.822	1	0	1	199	199	0
cvc5	0	0	0.0	0.0	0	0	0	200	200	0

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