QF_Datatypes (Model Validation Track)

Competition results for the QF_Datatypes division in the Model Validation Track. Chart

Results were generated on 2026-07-25

Benchmarks: 871
Time Limit: 1200 seconds
Memory Limit: 30720 GB

Logics:

QF_DT : 768 benchmarks
QF_UFDT : 103 benchmarks

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24 seconds Performance (parallel)
cvc5	cvc5	cvc5	-	cvc5

Sequential Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Timeout
cvc5	539	10643.78	10711.76	539	539	332	19
z3-BooledASS ^ne	524 (base +0)	5781.78	5846.92	524	524	347	108
SMTInterpol	321	4989.91	4637.97	321	321	550	93
z3-BooledASS-base ⁿ	524	5788.93	5854.87	524	524	347	108

(base +/- n): for derived solvers: increment over base solver
^ne: not eligible for winning as it does not substantially improve over the base solver (at least 10 % improvement in PAR2 score) ⁿ: non-competing solver

Parallel Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Timeout
cvc5	539	10643.78	10711.76	539	539	332	19
z3-BooledASS ^ne	524 (base +0)	5781.78	5846.92	524	524	347	108
SMTInterpol	321	4989.91	4637.97	321	321	550	93
z3-BooledASS-base ⁿ	524	5788.93	5854.87	524	524	347	108

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Timeout
cvc5	539	10643.78	10711.76	539	539	332	19
z3-BooledASS ^ne	524 (base +0)	5781.78	5846.92	524	524	347	108
SMTInterpol	321	4989.91	4637.97	321	321	550	93
z3-BooledASS-base ⁿ	524	5788.93	5854.87	524	524	347	108

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained
z3-BooledASS ^ne	514 (base +0)	87.74	151.19	514	514	238	119
cvc5	461	351.29	408.60	461	461	312	98
SMTInterpol	304	280.01	210.11	304	304	457	110
z3-BooledASS-base ⁿ	514	87.38	151.58	514	514	238	119

SMT-COMP 2026