SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_ABV (Single Query Track)

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

Results were generated on 2025-08-11

Benchmarks: 7574
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 Bitwuzla

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 7555 9266.28 10205.41 7555 5191 2364 19 0 18 1
Yices2 0 7546 12646.28 13586.79 7546 5190 2356 28 0 28 0
Z3-Owl 0 7472
(base +39) 		35396.77 36343.43 7472 5143 2329 102 0 97 4
cvc5 0 7337 91241.19 92160.09 7337 5043 2294 237 0 235 2
SMTInterpol 0 5804 373574.53 331043.61 5815 3878 1937 1759 0 1676 0
Z3-Owl-base n 0 7433 38195.63 39117.90 7433 5117 2316 141 0 140 1
(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 7555 9266.28 10205.41 7555 5191 2364 19 0 18 1
Yices2 0 7546 12646.28 13586.79 7546 5190 2356 28 0 28 0
Z3-Owl 0 7472
(base +39) 		35396.77 36343.43 7472 5143 2329 102 0 97 4
cvc5 0 7337 91241.19 92160.09 7337 5043 2294 237 0 235 2
SMTInterpol 0 5815 387617.25 343937.96 5815 3878 1937 1759 0 1676 0
Z3-Owl-base n 0 7433 38195.63 39117.90 7433 5117 2316 141 0 140 1
(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 5191 3458.09 4102.64 5191 5191 0 4 2379 3 1
Yices2 0 5190 5593.86 6240.03 5190 5190 0 5 2379 5 0
Z3-Owl 0 5143
(base +26) 		24200.72 24852.56 5143 5143 0 52 2379 49 2
cvc5 0 5043 77801.80 78434.68 5043 5043 0 152 2379 150 2
SMTInterpol 0 3878 314359.05 278408.39 3878 3878 0 1317 2379 1244 0
Z3-Owl-base n 0 5117 26026.49 26661.17 5117 5117 0 78 2379 77 1
(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 2364 5808.19 6102.77 2364 0 2364 15 5195 15 0
Yices2 0 2356 7052.42 7346.76 2356 0 2356 23 5195 23 0
Z3-Owl 0 2329
(base +13) 		11196.05 11490.87 2329 0 2329 50 5195 48 2
cvc5 0 2294 13439.39 13725.41 2294 0 2294 85 5195 85 0
SMTInterpol 0 1937 73258.20 65529.57 1937 0 1937 442 5195 432 0
Z3-Owl-base n 0 2316 12169.14 12456.73 2316 0 2316 63 5195 63 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
Bitwuzla 0 7516 4552.41 5485.64 7516 5175 2341 0 58 0 0
Yices2 0 7483 2186.63 3117.64 7483 5161 2322 0 91 0 0
Z3-Owl 0 7360
(base +69) 		9317.03 10246.01 7360 5069 2291 0 214 0 0
cvc5 0 6883 8236.43 9087.41 6883 4650 2233 0 691 0 0
SMTInterpol 0 4551 15910.73 7307.31 4551 2835 1716 30 2993 0 0
Z3-Owl-base n 0 7291 3675.07 4574.71 7291 5019 2272 0 283 0 0
(base +/- n): for derived solvers: increment over base solver
n: non-competing solver