SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

NRA (Single Query Track)

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

Results were generated on 2025-08-11

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 YicesQS SMT-RAT SMT-RAT

Sequential Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
SMT-RAT 0 96 26.55 38.57 96 4 92 3 0 3 0
Z3-alpha 0 95
(base +2) 		30.42 38.10 95 3 92 4 0 1 3
YicesQS 0 92 249.10 260.44 92 4 88 7 0 7 0
cvc5 0 87 621.18 632.09 87 3 84 12 0 12 0
iProver v3.9.3 0 74 4774.90 1264.05 77 0 77 22 0 22 0
SMTInterpol 0 40 26.47 21.54 40 1 39 59 0 0 0
UltimateEliminator+MathSAT 0 14 58.68 27.82 14 1 13 85 0 47 0
Z3-alpha-base n 0 93 22.38 33.85 93 3 90 6 0 6 0
(base +/- n): for derived solvers: increment over base solver
n: non-competing solver

Parallel Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
SMT-RAT 0 96 26.55 38.57 96 4 92 3 0 3 0
Z3-alpha 0 95
(base +2) 		30.42 38.10 95 3 92 4 0 1 3
YicesQS 0 92 249.10 260.44 92 4 88 7 0 7 0
cvc5 0 87 621.18 632.09 87 3 84 12 0 12 0
iProver v3.9.3 0 77 13691.19 3501.30 77 0 77 22 0 22 0
SMTInterpol 0 40 26.47 21.54 40 1 39 59 0 0 0
UltimateEliminator+MathSAT 0 14 58.68 27.82 14 1 13 85 0 47 0
Z3-alpha-base n 0 93 22.38 33.85 93 3 90 6 0 6 0
(base +/- n): for derived solvers: increment over base solver
n: non-competing solver

SAT Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
YicesQS 0 4 1.03 1.52 4 4 0 1 94 1 0
SMT-RAT 0 4 10.07 10.57 4 4 0 1 94 1 0
Z3-alpha 0 3
(base +0) 		0.84 1.16 3 3 0 2 94 0 2
cvc5 0 3 0.92 1.29 3 3 0 2 94 2 0
SMTInterpol 0 1 0.54 0.50 1 1 0 4 94 0 0
UltimateEliminator+MathSAT 0 1 3.83 1.87 1 1 0 4 94 0 0
iProver v3.9.3 0 0 0.00 0.00 0 0 0 5 94 5 0
Z3-alpha-base n 0 3 0.50 0.87 3 3 0 2 94 2 0
(base +/- n): for derived solvers: increment over base solver
n: non-competing solver

UNSAT Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
SMT-RAT 0 92 16.48 28.00 92 0 92 1 6 1 0
Z3-alpha 0 92
(base +2) 		29.59 36.94 92 0 92 1 6 0 1
YicesQS 0 88 248.07 258.91 88 0 88 5 6 5 0
cvc5 0 84 620.27 630.79 84 0 84 9 6 9 0
iProver v3.9.3 0 77 13691.19 3501.30 77 0 77 16 6 16 0
SMTInterpol 0 39 25.92 21.05 39 0 39 54 6 0 0
UltimateEliminator+MathSAT 0 13 54.84 25.96 13 0 13 80 6 47 0
Z3-alpha-base n 0 90 21.88 32.98 90 0 90 3 6 3 0
(base +/- n): for derived solvers: increment over base solver
n: non-competing solver

24 seconds Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
SMT-RAT 0 96 26.55 38.57 96 4 92 0 3 0 0
Z3-alpha 0 95
(base +2) 		30.42 38.10 95 3 92 0 4 0 0
YicesQS 0 91 17.22 28.39 91 4 87 0 8 0 0
cvc5 0 85 16.58 27.15 85 3 82 0 14 0 0
iProver v3.9.3 0 69 835.23 265.22 69 0 69 0 30 0 0
SMTInterpol 0 40 26.47 21.54 40 1 39 59 0 0 0
UltimateEliminator+MathSAT 0 14 58.68 27.82 14 1 13 38 47 0 0
Z3-alpha-base n 0 93 22.38 33.85 93 3 90 0 6 0 0
(base +/- n): for derived solvers: increment over base solver
n: non-competing solver