QF_Datatypes (Single Query Track)

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

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

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

Logics:

• QF_DT : 201 benchmarks
• QF_UFDT : 200 benchmarks

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	Abstained	Timeout	Memout
z3-4.8.17n	0	207	330289.389	330324.673	207	48	159	194	0	194	0
2021-z3n	0	205	331782.706	331814.081	205	47	158	196	0	196	0
cvc5	0	190	354197.135	354254.987	190	51	139	211	0	211	0
smtinterpol	0	17	472148.571	469249.257	17	0	17	384	0	384	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	207	330308.559	330318.623	207	48	159	194	0	194	0
2021-z3n	0	205	331799.096	331807.181	205	47	158	196	0	196	0
cvc5	0	190	354231.815	354245.847	190	51	139	211	0	211	0
smtinterpol	0	27	473834.091	467275.516	27	0	27	374	0	374	0

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
cvc5	0	51	204382.734	204387.914	51	51	0	149	201	211	0
z3-4.8.17n	0	48	211888.097	211890.903	48	48	0	152	201	194	0
2021-z3n	0	47	211779.365	211781.614	47	47	0	153	201	196	0
smtinterpol	0	0	240000.0	240000.0	0	0	0	200	201	374	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	159	118420.462	118427.719	159	0	159	42	200	194	0
2021-z3n	0	158	120019.731	120025.568	158	0	158	43	200	196	0
cvc5	0	139	149849.082	149857.933	139	0	139	62	200	211	0
smtinterpol	0	27	233834.091	227275.516	27	0	27	174	200	374	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	4	9584.032	9584.028	4	1	3	397	0	397	0
2021-z3n	0	4	9584.171	9584.174	4	1	3	397	0	397	0
smtinterpol	0	1	9618.688	9617.69	1	0	1	400	0	400	0
cvc5	0	0	9624.0	9624.0	0	0	0	401	0	401	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.