SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_RDL (Single Query Track)

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

Results were generated on 2025-08-11

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

Winners

Sequential Performance Parallel Performance SAT Performance (parallel) UNSAT Performance (parallel) 24 seconds Performance (parallel)
Yices2 Yices2 Yices2 Yices2 Yices2

Sequential Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
Yices2 0 215 3790.72 3817.66 215 106 109 32 0 32 0
cvc5 0 209 3978.42 4004.69 209 101 108 38 0 38 0
Z3-alpha 0 203
(base -7) 		10399.57 2676.86 207 99 108 40 0 40 0
OpenSMT 0 197 13874.97 13901.10 197 103 94 50 0 50 0
SMTInterpol 0 177 8587.34 6336.30 177 99 78 70 0 65 0
Z3-alpha-base n 0 210 7409.90 7437.26 210 102 108 37 0 37 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
Yices2 0 215 3790.72 3817.66 215 106 109 32 0 32 0
cvc5 0 209 3978.42 4004.69 209 101 108 38 0 38 0
Z3-alpha 0 207
(base -3) 		22546.24 5715.89 207 99 108 40 0 40 0
OpenSMT 0 197 13874.97 13901.10 197 103 94 50 0 50 0
SMTInterpol 0 177 8587.34 6336.30 177 99 78 70 0 65 0
Z3-alpha-base n 0 210 7409.90 7437.26 210 102 108 37 0 37 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
Yices2 0 106 1346.10 1359.35 106 106 0 0 141 0 0
OpenSMT 0 103 8527.23 8541.02 103 103 0 3 141 3 0
cvc5 0 101 1095.01 1107.51 101 101 0 5 141 5 0
Z3-alpha 0 99
(base -3) 		12056.42 3052.59 99 99 0 7 141 7 0
SMTInterpol 0 99 4440.12 3590.50 99 99 0 7 141 7 0
Z3-alpha-base n 0 102 5881.49 5895.03 102 102 0 4 141 4 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
Yices2 0 109 2444.62 2458.32 109 0 109 0 138 0 0
Z3-alpha 0 108
(base +0) 		10489.82 2663.30 108 0 108 1 138 1 0
cvc5 0 108 2883.41 2897.18 108 0 108 1 138 1 0
OpenSMT 0 94 5347.74 5360.08 94 0 94 15 138 15 0
SMTInterpol 0 78 4147.22 2745.79 78 0 78 31 138 27 0
Z3-alpha-base n 0 108 1528.41 1542.24 108 0 108 1 138 1 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
Yices2 0 197 331.45 355.76 197 99 98 0 50 0 0
Z3-alpha 0 179
(base -6) 		1819.63 519.65 179 89 90 0 68 0 0
cvc5 0 178 601.60 623.56 178 93 85 0 69 0 0
OpenSMT 0 150 385.35 403.90 150 81 69 0 97 0 0
SMTInterpol 0 136 1551.70 730.13 136 76 60 0 111 0 0
Z3-alpha-base n 0 185 424.05 447.28 185 90 95 0 62 0 0
(base +/- n): for derived solvers: increment over base solver
n: non-competing solver