QF_NonLinearRealArith (Unsat Core Track)

Competition results for the QF_NonLinearRealArith division in the Unsat Core Track. Chart

Results were generated on 2026-07-25

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

Logics:

QF_NRA : 300 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 UNSAT	Unsolved	Timeout
z3-BooledASS ^ne	208454 (base +0)	6224.34	6256.81	263	263	37	37
Yices2	197203	9443.16	9475.18	249	249	51	51
cvc5	4899	42706.28	42744.64	281	281	19	19
SMTInterpol	4325	5.42	2.27	2	2	298	0
z3-BooledASS-base ⁿ	208454	6036.60	6069.23	263	263	37	37

(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 UNSAT	Unsolved	Timeout
z3-BooledASS ^ne	208454 (base +0)	6224.34	6256.81	263	263	37	37
Yices2	197203	9443.16	9475.18	249	249	51	51
cvc5	4899	42706.28	42744.64	281	281	19	19
SMTInterpol	4325	5.42	2.27	2	2	298	0
z3-BooledASS-base ⁿ	208454	6036.60	6069.23	263	263	37	37

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Timeout
z3-BooledASS ^ne	208454 (base +0)	6224.34	6256.81	263	263	37	37
Yices2	197203	9443.16	9475.18	249	249	51	51
cvc5	4899	42706.28	42744.64	281	281	19	19
SMTInterpol	4325	5.42	2.27	2	2	298	0
z3-BooledASS-base ⁿ	208454	6036.60	6069.23	263	263	37	37

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained
z3-BooledASS ^ne	86761 (base -1786)	822.87	849.05	213	213	0	87
Yices2	57020	744.18	768.32	193	193	0	107
SMTInterpol	4325	5.42	2.27	2	2	256	42
cvc5	4000	596.71	615.52	151	151	0	149
z3-BooledASS-base ⁿ	88547	865.16	891.59	215	215	0	85

SMT-COMP 2026