QF_AX (Single Query Track)

Competition results for the QF_AX logic in the Single Query Track. Chart

Results were generated on 2026-07-25

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

Winners

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

Sequential Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT
Yices2	300	45.97	83.16	300	142	158
z3-BooledASS ^ne	300 (base +0)	56.60	93.34	300	142	158
cvc5-cvc5-xyz ^ne	300 (base +0)	99.50	136.33	300	142	158
cvc5	300	100.50	137.82	300	142	158
OpenSMT	300	132.25	169.48	300	142	158
OpenSMT-SMTS-seq ^ne	300 (base +0)	187.46	221.19	300	142	158
SMTInterpol	300	584.30	292.48	300	142	158
z3-BooledASS-base ⁿ	300	56.91	93.75	300	142	158
cvc5-cvc5-xyz-base ⁿ	300	99.10	136.24	300	142	158
OpenSMT-SMTS-seq-base ⁿ	300	133.88	170.91	300	142	158

(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	Solved UNSAT
Yices2	300	45.97	83.16	300	142	158
z3-BooledASS ^ne	300 (base +0)	56.60	93.34	300	142	158
cvc5-cvc5-xyz ^ne	300 (base +0)	99.50	136.33	300	142	158
cvc5	300	100.50	137.82	300	142	158
OpenSMT	300	132.25	169.48	300	142	158
OpenSMT-SMTS-seq ^ne	300 (base +0)	187.46	221.19	300	142	158
SMTInterpol	300	584.30	292.48	300	142	158
z3-BooledASS-base ⁿ	300	56.91	93.75	300	142	158
cvc5-cvc5-xyz-base ⁿ	300	99.10	136.24	300	142	158
OpenSMT-SMTS-seq-base ⁿ	300	133.88	170.91	300	142	158

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Abstained
Yices2	142	21.20	38.75	142	142	158
z3-BooledASS ^ne	142 (base +0)	24.48	41.83	142	142	158
cvc5-cvc5-xyz ^ne	142 (base +0)	26.16	43.65	142	142	158
cvc5	142	26.42	44.15	142	142	158
OpenSMT	142	31.95	49.62	142	142	158
OpenSMT-SMTS-seq ^ne	142 (base +0)	47.95	64.34	142	142	158
SMTInterpol	142	127.42	82.33	142	142	158
z3-BooledASS-base ⁿ	142	24.50	41.91	142	142	158
cvc5-cvc5-xyz-base ⁿ	142	26.23	43.84	142	142	158
OpenSMT-SMTS-seq-base ⁿ	142	32.10	49.61	142	142	158

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Abstained
Yices2	158	24.77	44.41	158	158	142
z3-BooledASS ^ne	158 (base +0)	32.12	51.51	158	158	142
cvc5-cvc5-xyz ^ne	158 (base +0)	73.34	92.68	158	158	142
cvc5	158	74.08	93.67	158	158	142
OpenSMT	158	100.30	119.86	158	158	142
OpenSMT-SMTS-seq ^ne	158 (base +0)	139.52	156.85	158	158	142
SMTInterpol	158	456.88	210.15	158	158	142
z3-BooledASS-base ⁿ	158	32.41	51.84	158	158	142
cvc5-cvc5-xyz-base ⁿ	158	72.87	92.40	158	158	142
OpenSMT-SMTS-seq-base ⁿ	158	101.78	121.30	158	158	142

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Abstained
Yices2	300	45.97	83.16	300	142	158	0
z3-BooledASS ^ne	300 (base +0)	56.60	93.34	300	142	158	0
cvc5-cvc5-xyz ^ne	300 (base +0)	99.50	136.33	300	142	158	0
cvc5	300	100.50	137.82	300	142	158	0
OpenSMT	300	132.25	169.48	300	142	158	0
SMTInterpol	300	584.30	292.48	300	142	158	0
OpenSMT-SMTS-seq ^ne	299 (base -1)	148.22	182.51	299	142	157	1
z3-BooledASS-base ⁿ	300	56.91	93.75	300	142	158	0
cvc5-cvc5-xyz-base ⁿ	300	99.10	136.24	300	142	158	0
OpenSMT-SMTS-seq-base ⁿ	300	133.88	170.91	300	142	158	0

SMT-COMP 2026