QF_NonLinearRealArith (Model Validation Track)

Competition results for the QF_NonLinearRealArith division in the Model Validation Track. Chart

Results were generated on 2026-07-25

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

Logics:

QF_NRA : 936 benchmarks

Winners

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

Sequential Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Timeout
z3-BooledASS ^ne	743 (base +0)	1433.41	1524.95	743	743	193	28
SMT-RAT	722	7209.81	7299.79	722	722	214	49
Yices2	720	3897.74	3988.35	720	720	216	35
cvc5	693	3914.34	4000.92	693	693	243	56
SMTInterpol	3	897.35	822.86	3	3	933	0
z3-BooledASS-base ⁿ	743	1433.52	1524.82	743	743	193	28

(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	Unsolved	Timeout
z3-BooledASS ^ne	743 (base +0)	1433.41	1524.95	743	743	193	28
SMT-RAT	722	7209.81	7299.79	722	722	214	49
Yices2	720	3897.74	3988.35	720	720	216	35
cvc5	693	3914.34	4000.92	693	693	243	56
SMTInterpol	3	897.35	822.86	3	3	933	0
z3-BooledASS-base ⁿ	743	1433.52	1524.82	743	743	193	28

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Timeout
z3-BooledASS ^ne	743 (base +0)	1433.41	1524.95	743	743	193	28
SMT-RAT	722	7209.81	7299.79	722	722	214	49
Yices2	720	3897.74	3988.35	720	720	216	35
cvc5	693	3914.34	4000.92	693	693	243	56
SMTInterpol	3	897.35	822.86	3	3	933	0
z3-BooledASS-base ⁿ	743	1433.52	1524.82	743	743	193	28

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained
z3-BooledASS ^ne	731 (base +0)	361.06	451.00	731	731	164	41
Yices2	709	221.49	310.37	709	709	181	46
SMT-RAT	700	189.24	275.89	700	700	164	72
cvc5	688	161.80	247.49	688	688	185	63
SMTInterpol	1	0.39	0.41	1	1	931	4
z3-BooledASS-base ⁿ	731	361.47	451.22	731	731	164	41

SMT-COMP 2026