SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_UFBV (Unsat Core Track)

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

Results were generated on 2025-08-11

Benchmarks: 566
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

Sequential Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved UNSAT Unsolved Abstained Timeout Memout
Bitwuzla 0 296756 12807.79 12874.35 518 518 48 0 48 0
Yices2 0 262868 76730.09 76801.07 494 494 72 0 72 0
SMTInterpol 0 227554 13484.10 6415.50 536 536 30 0 10 0
cvc5 0 46390 133718.46 133805.08 493 493 73 0 41 32

Parallel Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved UNSAT Unsolved Abstained Timeout Memout
Bitwuzla 0 296756 12807.79 12874.35 518 518 48 0 48 0
Yices2 0 262868 76730.09 76801.07 494 494 72 0 72 0
SMTInterpol 0 227554 13484.10 6415.50 536 536 30 0 10 0
cvc5 0 46390 133718.46 133805.08 493 493 73 0 41 32

UNSAT Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved UNSAT Unsolved Abstained Timeout Memout
Bitwuzla 0 296756 12807.79 12874.35 518 518 48 0 48 0
Yices2 0 262868 76730.09 76801.07 494 494 72 0 72 0
SMTInterpol 0 227554 13484.10 6415.50 536 536 30 0 10 0
cvc5 0 46390 133718.46 133805.08 493 493 73 0 41 32

24 seconds Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved UNSAT Unsolved Abstained Timeout Memout
Bitwuzla 0 238383 4064.69 4111.03 369 369 0 197 0 0
Yices2 0 204292 1450.29 1473.84 191 191 0 375 0 0
SMTInterpol 0 203713 10657.21 4346.73 503 503 11 52 0 0
cvc5 0 2890 174.03 183.65 78 78 0 488 0 0