SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

BV (Unsat Core Track)

Competition results for the BV logic in the Unsat Core Track. Chart

Results were generated on 2025-08-11

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

Winners

Sequential Performance Parallel Performance SAT Performance (parallel) UNSAT Performance (parallel) 24 seconds Performance (parallel)
cvc5 cvc5 - cvc5 cvc5

Sequential Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved UNSAT Unsolved Abstained Timeout Memout
cvc5 0 64 12549.61 12586.29 283 283 17 0 17 0
Bitwuzla 0 19 1448.51 1477.61 230 230 70 0 70 0
UltimateEliminator+MathSAT 0 0 10.20 4.33 2 2 298 0 0 0
SMTInterpol 0 0 16.55 5.62 1 1 299 0 36 0

Parallel Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved UNSAT Unsolved Abstained Timeout Memout
cvc5 0 64 12549.61 12586.29 283 283 17 0 17 0
Bitwuzla 0 19 1448.51 1477.61 230 230 70 0 70 0
UltimateEliminator+MathSAT 0 0 10.20 4.33 2 2 298 0 0 0
SMTInterpol 0 0 16.55 5.62 1 1 299 0 36 0

UNSAT Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved UNSAT Unsolved Abstained Timeout Memout
cvc5 0 64 12549.61 12586.29 283 283 17 0 17 0
Bitwuzla 0 19 1448.51 1477.61 230 230 70 0 70 0
UltimateEliminator+MathSAT 0 0 10.20 4.33 2 2 298 0 0 0
SMTInterpol 0 0 16.55 5.62 1 1 299 0 36 0

24 seconds Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved UNSAT Unsolved Abstained Timeout Memout
cvc5 0 46 353.63 379.71 212 212 0 88 0 0
Bitwuzla 0 19 86.88 113.87 216 216 0 84 0 0
UltimateEliminator+MathSAT 0 0 10.20 4.33 2 2 298 0 0 0
SMTInterpol 0 0 16.55 5.62 1 1 212 87 0 0