SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

Bitvec (Single Query Track)

Competition results for the Bitvec division in the Single Query Track. Chart

Results were generated on 2025-08-11

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

Logics:

Winners

Sequential Performance Parallel Performance SAT Performance (parallel) UNSAT Performance (parallel) 24 seconds Performance (parallel)
cvc5 cvc5 Bitwuzla cvc5 YicesQS

Sequential Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
cvc5 0 952 33547.27 33669.48 952 225 727 88 0 80 0
YicesQS 0 886 18086.23 18198.41 886 230 656 154 0 144 1
Bitwuzla 0 839 8895.96 9001.83 839 232 607 201 0 193 0
UltimateEliminator+MathSAT 0 336 3698.71 2637.22 336 32 304 704 0 119 21
SMTInterpol 0 281 347.45 218.44 281 1 280 759 0 188 0

Parallel Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
cvc5 0 952 33547.27 33669.48 952 225 727 88 0 80 0
YicesQS 0 886 18086.23 18198.41 886 230 656 154 0 144 1
Bitwuzla 0 839 8895.96 9001.83 839 232 607 201 0 193 0
UltimateEliminator+MathSAT 0 336 3698.71 2637.22 336 32 304 704 0 119 21
SMTInterpol 0 281 347.45 218.44 281 1 280 759 0 188 0

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 232 2676.45 2705.68 232 232 0 23 785 15 0
YicesQS 0 230 10124.95 10154.84 230 230 0 25 785 17 0
cvc5 0 225 14908.57 14938.38 225 225 0 30 785 22 0
UltimateEliminator+MathSAT 0 32 1471.50 1231.60 32 32 0 223 785 76 9
SMTInterpol 0 1 0.86 0.59 1 1 0 254 785 95 0

UNSAT Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
cvc5 0 727 18638.70 18731.10 727 0 727 35 278 35 0
YicesQS 0 656 7961.28 8043.57 656 0 656 106 278 104 1
Bitwuzla 0 607 6219.51 6296.15 607 0 607 155 278 155 0
UltimateEliminator+MathSAT 0 304 2227.21 1405.62 304 0 304 458 278 31 11
SMTInterpol 0 280 346.59 217.86 280 0 280 482 278 82 0

24 seconds Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
YicesQS 0 842 341.85 445.96 842 206 636 8 190 0 0
Bitwuzla 0 792 512.12 610.06 792 218 574 8 240 0 0
cvc5 0 689 1076.69 1161.81 689 62 627 8 343 0 0
UltimateEliminator+MathSAT 0 323 1676.98 815.98 323 25 298 523 194 0 0
SMTInterpol 0 280 295.28 179.89 280 1 279 511 249 0 0