SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

AUFBV (Single Query Track)

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

Results were generated on 2025-08-11

Benchmarks: 761
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 528 29616.10 29688.30 528 143 385 233 0 220 1
cvc5 0 214 28271.49 28301.96 214 11 203 547 0 444 0
SMTInterpol 0 28 10431.64 9591.18 28 0 28 733 0 611 0
UltimateEliminator+MathSAT 0 3 34.95 15.73 3 0 3 758 0 46 219

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 528 29616.10 29688.30 528 143 385 233 0 220 1
cvc5 0 214 28271.49 28301.96 214 11 203 547 0 444 0
SMTInterpol 0 28 10431.64 9591.18 28 0 28 733 0 611 0
UltimateEliminator+MathSAT 0 3 34.95 15.73 3 0 3 758 0 46 219

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 143 5909.59 5928.54 143 143 0 0 618 0 0
cvc5 0 11 1901.79 1903.33 11 11 0 132 618 72 0
SMTInterpol 0 0 0.00 0.00 0 0 0 143 618 82 0
UltimateEliminator+MathSAT 0 0 0.00 0.00 0 0 0 143 618 8 98

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 385 23706.51 23759.76 385 0 385 5 371 5 0
cvc5 0 203 26369.69 26398.63 203 0 203 187 371 162 0
SMTInterpol 0 28 10431.64 9591.18 28 0 28 362 371 322 0
UltimateEliminator+MathSAT 0 3 34.95 15.73 3 0 3 387 371 34 81

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 410 1384.95 1435.62 410 120 290 12 339 0 0
cvc5 0 157 651.97 671.41 157 4 153 18 586 0 0
SMTInterpol 0 9 211.02 92.17 9 0 9 49 703 0 0
UltimateEliminator+MathSAT 0 3 34.95 15.73 3 0 3 475 283 0 0