SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_FP (Single Query Track)

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

Results were generated on 2025-08-11

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

Winners

Sequential Performance Parallel Performance SAT Performance (parallel) UNSAT Performance (parallel) 24 seconds Performance (parallel)
Bitwuzla Bitwuzla Bitwuzla Bitwuzla COLIBRI

Sequential Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
Bitwuzla 0 255 12529.71 12564.26 255 140 115 20 0 20 0
COLIBRI 0 232 1682.03 1710.85 232 133 99 43 0 43 0
cvc5 0 230 18499.13 18530.31 230 139 91 45 0 43 2
colibri2 0 199 5739.55 5764.52 199 117 82 76 0 10 0
Z3-Owl 0 173
(base +34) 		23773.08 23798.55 173 104 69 102 0 56 19
Z3-Owl-base n 0 139 27555.63 27576.01 139 82 57 136 0 89 16
(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
Bitwuzla 0 255 12529.71 12564.26 255 140 115 20 0 20 0
COLIBRI 0 232 1682.03 1710.85 232 133 99 43 0 43 0
cvc5 0 230 18499.13 18530.31 230 139 91 45 0 43 2
colibri2 0 199 5739.55 5764.52 199 117 82 76 0 10 0
Z3-Owl 0 173
(base +34) 		23773.08 23798.55 173 104 69 102 0 56 19
Z3-Owl-base n 0 139 27555.63 27576.01 139 82 57 136 0 89 16
(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
Bitwuzla 0 140 6872.07 6891.13 140 140 0 1 134 1 0
cvc5 0 139 6686.87 6705.09 139 139 0 2 134 2 0
COLIBRI 0 127 364.26 380.01 127 127 0 14 134 14 0
colibri2 0 117 4859.61 4874.39 117 117 0 24 134 6 0
Z3-Owl 0 104
(base +22) 		13441.35 13456.36 104 104 0 37 134 9 8
Z3-Owl-base n 0 82 15304.25 15316.20 82 82 0 59 134 30 11
(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
Bitwuzla 0 115 5657.64 5673.14 115 0 115 8 152 8 0
COLIBRI 0 97 425.88 437.87 97 0 97 26 152 26 0
cvc5 0 91 11812.26 11825.23 91 0 91 32 152 32 0
colibri2 0 82 879.94 890.13 82 0 82 41 152 2 0
Z3-Owl 0 69
(base +12) 		10331.73 10342.20 69 0 69 54 152 42 5
Z3-Owl-base n 0 57 12251.39 12259.81 57 0 57 66 152 54 5
(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
COLIBRI 0 220 409.80 436.97 220 126 94 0 55 0 0
Bitwuzla 0 197 624.40 648.74 197 106 91 0 78 0 0
colibri2 0 175 263.09 284.55 175 103 72 61 39 0 0
cvc5 0 158 692.73 712.19 158 100 58 0 117 0 0
Z3-Owl 0 70
(base +25) 		741.71 750.77 70 36 34 0 205 0 0
Z3-Owl-base n 0 45 418.98 424.58 45 30 15 0 230 0 0
(base +/- n): for derived solvers: increment over base solver
n: non-competing solver