QF_Equality (Model Validation Track)

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

Results were generated on 2026-07-25

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

Logics:

QF_UF : 714 benchmarks

Winners

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

Sequential Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved
Yices2	714	129.49	219.23	714	714	0
OpenSMT	714	185.81	274.19	714	714	0
cvc5	714	232.73	320.22	714	714	0
SMTInterpol	714	1614.58	726.45	714	714	0
plat-smt	703	139.61	227.34	703	703	11
z3-BooledASS ^ne	2 (base +0)	0.32	0.56	2	2	712
z3-BooledASS-base ⁿ	2	0.34	0.59	2	2	712

(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
Yices2	714	129.49	219.23	714	714	0
OpenSMT	714	185.81	274.19	714	714	0
cvc5	714	232.73	320.22	714	714	0
SMTInterpol	714	1614.58	726.45	714	714	0
plat-smt	703	139.61	227.34	703	703	11
z3-BooledASS ^ne	2 (base +0)	0.32	0.56	2	2	712
z3-BooledASS-base ⁿ	2	0.34	0.59	2	2	712

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved
Yices2	714	129.49	219.23	714	714	0
OpenSMT	714	185.81	274.19	714	714	0
cvc5	714	232.73	320.22	714	714	0
SMTInterpol	714	1614.58	726.45	714	714	0
plat-smt	703	139.61	227.34	703	703	11
z3-BooledASS ^ne	2 (base +0)	0.32	0.56	2	2	712
z3-BooledASS-base ⁿ	2	0.34	0.59	2	2	712

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved
Yices2	714	129.49	219.23	714	714	0
OpenSMT	714	185.81	274.19	714	714	0
cvc5	714	232.73	320.22	714	714	0
SMTInterpol	714	1614.58	726.45	714	714	0
plat-smt	703	139.61	227.34	703	703	11
z3-BooledASS ^ne	2 (base +0)	0.32	0.56	2	2	712
z3-BooledASS-base ⁿ	2	0.34	0.59	2	2	712

SMT-COMP 2026