NRA (Single Query Track)

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

Results were generated on 2026-07-25

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

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24 seconds Performance (parallel)
SMT-RAT	SMT-RAT	SMT-RAT	SMT-RAT	SMT-RAT

Sequential Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout
SMT-RAT	96	20.07	32.02	96	4	92	3	3
Z3-alpha2	96 (base +2)	972.41	935.89	96	4	92	3	3
Z3-alpha2-debug ⁿ	96	1185.35	1055.99	96	4	92	3	3
Z3-GEX	95 (base +2)	34.65	35.70	95	3	92	4	4
z3-BooledASS ^ne	93 (base +0)	16.54	27.95	93	3	90	6	6
YicesQS	91	331.83	343.04	91	3	88	8	8
cvc5	88	2209.47	2220.59	88	4	84	11	11
cvc5-cvc5-xyz ^ne	88 (base +0)	2209.74	2220.75	88	4	84	11	11
SMTInterpol	40	28.18	22.13	40	1	39	59	0
UltimateEliminator+MathSAT	12	54.68	25.31	12	1	11	87	48
Z3-alpha2-base ⁿ	94	638.10	649.77	94	4	90	5	5
z3-BooledASS-base ⁿ	93	16.71	28.16	93	3	90	6	6
Z3-GEX-base ⁿ	93	22.01	33.69	93	3	90	6	6
cvc5-cvc5-xyz-base ⁿ	88	2210.07	2221.09	88	4	84	11	11

(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
SMT-RAT	96	20.07	32.02	96	4	92	3	3
Z3-alpha2	96 (base +2)	972.41	935.89	96	4	92	3	3
Z3-alpha2-debug ⁿ	96	1185.35	1055.99	96	4	92	3	3
Z3-GEX	95 (base +2)	34.65	35.70	95	3	92	4	4
z3-BooledASS ^ne	93 (base +0)	16.54	27.95	93	3	90	6	6
YicesQS	91	331.83	343.04	91	3	88	8	8
cvc5	88	2209.47	2220.59	88	4	84	11	11
cvc5-cvc5-xyz ^ne	88 (base +0)	2209.74	2220.75	88	4	84	11	11
SMTInterpol	40	28.18	22.13	40	1	39	59	0
UltimateEliminator+MathSAT	12	54.68	25.31	12	1	11	87	48
Z3-alpha2-base ⁿ	94	638.10	649.77	94	4	90	5	5
z3-BooledASS-base ⁿ	93	16.71	28.16	93	3	90	6	6
Z3-GEX-base ⁿ	93	22.01	33.69	93	3	90	6	6
cvc5-cvc5-xyz-base ⁿ	88	2210.07	2221.09	88	4	84	11	11

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout
SMT-RAT	4	4.28	4.77	4	4	1	94	1
cvc5	4	301.41	301.93	4	4	1	94	1
cvc5-cvc5-xyz ^ne	4 (base +0)	301.48	301.99	4	4	1	94	1
Z3-alpha2 ^ne	4 (base +0)	638.29	636.79	4	4	1	94	1
Z3-alpha2-debug ⁿ	4	655.16	649.80	4	4	1	94	1
z3-BooledASS ^ne	3 (base +0)	0.52	0.88	3	3	2	94	2
YicesQS	3	0.55	0.93	3	3	2	94	2
Z3-GEX ^ne	3 (base +0)	0.69	1.05	3	3	2	94	2
SMTInterpol	1	0.50	0.47	1	1	4	94	0
UltimateEliminator+MathSAT	1	3.99	1.87	1	1	4	94	0
cvc5-cvc5-xyz-base ⁿ	4	301.45	301.95	4	4	1	94	1
Z3-alpha2-base ⁿ	4	622.35	622.89	4	4	1	94	1
Z3-GEX-base ⁿ	3	0.50	0.89	3	3	2	94	2
z3-BooledASS-base ⁿ	3	0.54	0.92	3	3	2	94	2

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout
SMT-RAT	92	15.79	27.25	92	92	1	6	1
Z3-GEX	92 (base +2)	33.96	34.65	92	92	1	6	1
Z3-alpha2	92 (base +2)	334.12	299.10	92	92	1	6	1
Z3-alpha2-debug ⁿ	92	530.18	406.18	92	92	1	6	1
z3-BooledASS ^ne	90 (base +0)	16.02	27.07	90	90	3	6	3
YicesQS	88	331.28	342.11	88	88	5	6	5
cvc5	84	1908.06	1918.66	84	84	9	6	9
cvc5-cvc5-xyz ^ne	84 (base +0)	1908.26	1918.76	84	84	9	6	9
SMTInterpol	39	27.67	21.66	39	39	54	6	0
UltimateEliminator+MathSAT	11	50.69	23.44	11	11	82	6	48
Z3-alpha2-base ⁿ	90	15.75	26.88	90	90	3	6	3
z3-BooledASS-base ⁿ	90	16.18	27.24	90	90	3	6	3
Z3-GEX-base ⁿ	90	21.52	32.80	90	90	3	6	3
cvc5-cvc5-xyz-base ⁿ	84	1908.62	1919.14	84	84	9	6	9

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained
SMT-RAT	96	20.07	32.02	96	4	92	0	3
Z3-GEX ^ne	95 (base +2)	34.65	35.70	95	3	92	0	4
Z3-alpha2 ^ne	95 (base +2)	345.01	308.84	95	3	92	0	4
Z3-alpha2-debug ⁿ	95	547.43	419.38	95	3	92	0	4
z3-BooledASS ^ne	93 (base +0)	16.54	27.95	93	3	90	0	6
YicesQS	90	17.50	28.56	90	3	87	0	9
cvc5	81	15.86	25.97	81	3	78	0	18
cvc5-cvc5-xyz ^ne	81 (base +0)	16.25	26.25	81	3	78	0	18
SMTInterpol	40	28.18	22.13	40	1	39	59	0
UltimateEliminator+MathSAT	12	54.68	25.31	12	1	11	38	49
Z3-alpha2-base ⁿ	93	16.28	27.80	93	3	90	0	6
z3-BooledASS-base ⁿ	93	16.71	28.16	93	3	90	0	6
Z3-GEX-base ⁿ	93	22.01	33.69	93	3	90	0	6
cvc5-cvc5-xyz-base ⁿ	81	16.54	26.55	81	3	78	0	18

SMT-COMP 2026