QF_ANIA (Single Query Track)

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

Results were generated on 2026-07-25

Benchmarks: 155
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	SMTInterpol	SMTInterpol

Sequential Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout
SMTInterpol	132	1022.08	698.66	132	116	16	23	11
Yices2	131	4287.06	4303.50	131	116	15	24	24
cvc5	108	3187.56	3201.23	108	95	13	47	47
cvc5-cvc5-xyz ^ne	108 (base +0)	3758.16	3771.79	108	95	13	47	47
Z3-alpha2 ^ne	104 (base +3)	9151.70	9111.07	104	86	18	51	51
Z3-alpha2-debug ⁿ	104	9348.94	9208.93	104	86	18	51	51
z3-BooledASS ^ne	95 (base -3)	6177.57	6189.69	95	77	18	60	60
Xolver	8	11.65	12.61	8	8	0	147	144
cvc5-cvc5-xyz-base ⁿ	108	3755.19	3768.90	108	95	13	47	47
Z3-alpha2-base ⁿ	101	9190.86	9204.26	101	83	18	54	54
z3-BooledASS-base ⁿ	98	9508.95	9521.92	98	80	18	57	57

(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	132	1022.08	698.66	132	116	16	23	11
Yices2	131	4287.06	4303.50	131	116	15	24	24
cvc5	108	3187.56	3201.23	108	95	13	47	47
cvc5-cvc5-xyz ^ne	108 (base +0)	3758.16	3771.79	108	95	13	47	47
Z3-alpha2 ^ne	104 (base +3)	9151.70	9111.07	104	86	18	51	51
Z3-alpha2-debug ⁿ	104	9348.94	9208.93	104	86	18	51	51
z3-BooledASS ^ne	95 (base -3)	6177.57	6189.69	95	77	18	60	60
Xolver	8	11.65	12.61	8	8	0	147	144
cvc5-cvc5-xyz-base ⁿ	108	3755.19	3768.90	108	95	13	47	47
Z3-alpha2-base ⁿ	101	9190.86	9204.26	101	83	18	54	54
z3-BooledASS-base ⁿ	98	9508.95	9521.92	98	80	18	57	57

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout
SMTInterpol	116	327.22	153.50	116	116	6	33	0
Yices2	116	3371.09	3385.59	116	116	6	33	6
cvc5	95	1470.58	1482.50	95	95	27	33	27
cvc5-cvc5-xyz ^ne	95 (base +0)	1558.00	1569.82	95	95	27	33	27
Z3-alpha2 ^ne	86 (base +3)	8661.70	8628.38	86	86	36	33	36
Z3-alpha2-debug ⁿ	86	8819.90	8704.38	86	86	36	33	36
z3-BooledASS ^ne	77 (base -3)	5837.68	5847.69	77	77	45	33	45
Xolver	8	11.65	12.61	8	8	114	33	111
cvc5-cvc5-xyz-base ⁿ	95	1550.56	1562.41	95	95	27	33	27
Z3-alpha2-base ⁿ	83	8332.92	8344.00	83	83	39	33	39
z3-BooledASS-base ⁿ	80	9177.70	9188.52	80	80	42	33	42

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout
z3-BooledASS ^ne	18 (base +0)	339.89	342.00	18	18	12	125	12
Z3-alpha2 ^ne	18 (base +0)	490.00	482.70	18	18	12	125	12
Z3-alpha2-debug ⁿ	18	529.04	504.55	18	18	12	125	12
SMTInterpol	16	694.86	545.17	16	16	14	125	11
Yices2	15	915.97	917.91	15	15	15	125	15
cvc5	13	1716.99	1718.73	13	13	17	125	17
cvc5-cvc5-xyz ^ne	13 (base +0)	2200.15	2201.97	13	13	17	125	17
Xolver	0	0.00	0.00	0	0	30	125	30
z3-BooledASS-base ⁿ	18	331.25	333.40	18	18	12	125	12
Z3-alpha2-base ⁿ	18	857.94	860.26	18	18	12	125	12
cvc5-cvc5-xyz-base ⁿ	13	2204.62	2206.49	13	13	17	125	17

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained
SMTInterpol	129	478.03	220.69	129	116	13	10	16
Yices2	98	199.31	211.36	98	86	12	0	57
cvc5	95	373.12	384.92	95	87	8	0	60
cvc5-cvc5-xyz ^ne	94 (base +0)	375.65	387.21	94	86	8	0	61
Z3-alpha2 ^ne	75 (base +9)	427.83	398.00	75	60	15	0	80
Z3-alpha2-debug ⁿ	75	590.37	488.69	75	60	15	0	80
z3-BooledASS ^ne	68 (base +0)	144.23	152.45	68	54	14	0	87
Xolver	8	11.65	12.61	8	8	0	0	147
cvc5-cvc5-xyz-base ⁿ	94	377.02	388.64	94	86	8	0	61
z3-BooledASS-base ⁿ	68	141.61	149.85	68	54	14	0	87
Z3-alpha2-base ⁿ	66	141.60	149.79	66	53	13	0	89

SMT-COMP 2026