QF_ALIA (Single Query Track)

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

Results were generated on 2026-07-25

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

Winners

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

Sequential Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout
SMTInterpol	168	1141.55	609.66	168	96	72	8	4
Yices2	162	1913.33	1933.50	162	90	72	14	14
OpenSMT-SMTS-seq ^ne	159 (base +0)	6037.93	5937.37	159	87	72	17	17
OpenSMT	158	3933.90	3953.82	158	86	72	18	18
cvc5	157	3470.18	3490.02	157	85	72	19	19
cvc5-cvc5-xyz ^ne	156 (base -1)	3420.24	3439.64	156	85	71	20	20
z3-BooledASS ^ne	155 (base +0)	11728.26	11748.37	155	83	72	21	21
OpenSMT-SMTS-seq-base ⁿ	159	4841.89	4862.07	159	87	72	17	17
cvc5-cvc5-xyz-base ⁿ	157	3622.73	3642.57	157	85	72	19	19
z3-BooledASS-base ⁿ	155	11778.48	11798.61	155	83	72	21	21

(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	Unsolved	Timeout
SMTInterpol	168	1141.55	609.66	168	96	72	8	4
Yices2	162	1913.33	1933.50	162	90	72	14	14
OpenSMT-SMTS-seq ^ne	159 (base +0)	6037.93	5937.37	159	87	72	17	17
OpenSMT	158	3933.90	3953.82	158	86	72	18	18
cvc5	157	3470.18	3490.02	157	85	72	19	19
cvc5-cvc5-xyz ^ne	156 (base -1)	3420.24	3439.64	156	85	71	20	20
z3-BooledASS ^ne	155 (base +0)	11728.26	11748.37	155	83	72	21	21
OpenSMT-SMTS-seq-base ⁿ	159	4841.89	4862.07	159	87	72	17	17
cvc5-cvc5-xyz-base ⁿ	157	3622.73	3642.57	157	85	72	19	19
z3-BooledASS-base ⁿ	155	11778.48	11798.61	155	83	72	21	21

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout
SMTInterpol	96	535.78	226.54	96	96	6	74	2
Yices2	90	1899.33	1910.51	90	90	12	74	12
OpenSMT-SMTS-seq ^ne	87 (base +0)	5659.07	5556.95	87	87	15	74	15
OpenSMT	86	3610.60	3621.53	86	86	16	74	16
cvc5	85	1513.50	1524.04	85	85	17	74	17
cvc5-cvc5-xyz ^ne	85 (base +0)	1804.23	1814.77	85	85	17	74	17
z3-BooledASS ^ne	83 (base +0)	11671.23	11682.56	83	83	19	74	19
OpenSMT-SMTS-seq-base ⁿ	87	4509.58	4520.81	87	87	15	74	15
cvc5-cvc5-xyz-base ⁿ	85	1642.50	1653.15	85	85	17	74	17
z3-BooledASS-base ⁿ	83	11721.29	11732.53	83	83	19	74	19

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout
Yices2	72	14.01	22.98	72	72	0	104	0
z3-BooledASS ^ne	72 (base +0)	57.03	65.81	72	72	0	104	0
OpenSMT	72	323.30	332.29	72	72	0	104	0
OpenSMT-SMTS-seq ^ne	72 (base +0)	378.86	380.41	72	72	0	104	0
SMTInterpol	72	605.77	383.12	72	72	0	104	0
cvc5	72	1956.68	1965.98	72	72	0	104	0
cvc5-cvc5-xyz ^ne	71 (base -1)	1616.01	1624.88	71	71	1	104	1
z3-BooledASS-base ⁿ	72	57.19	66.08	72	72	0	104	0
OpenSMT-SMTS-seq-base ⁿ	72	332.31	341.27	72	72	0	104	0
cvc5-cvc5-xyz-base ⁿ	72	1980.23	1989.42	72	72	0	104	0

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Abstained
SMTInterpol	163	721.84	302.88	163	95	68	13
Yices2	160	79.79	99.60	160	88	72	16
cvc5	135	253.10	269.92	135	69	66	41
cvc5-cvc5-xyz ^ne	135 (base +0)	256.30	272.87	135	69	66	41
OpenSMT	125	266.42	281.87	125	57	68	51
z3-BooledASS ^ne	123 (base +0)	228.95	244.01	123	52	71	53
OpenSMT-SMTS-seq ^ne	121 (base -2)	222.40	232.92	121	53	68	55
cvc5-cvc5-xyz-base ⁿ	135	258.80	275.54	135	69	66	41
OpenSMT-SMTS-seq-base ⁿ	123	228.38	243.56	123	55	68	53
z3-BooledASS-base ⁿ	123	231.60	246.79	123	52	71	53

SMT-COMP 2026