SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_UFBV (Incremental Track)

Competition results for the QF_UFBV logic in the Incremental Track. Chart

Results were generated on 2025-08-11

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

Winners

Parallel Performance SAT Performance (parallel) UNSAT Performance (parallel) 24 seconds Performance (parallel)
Bitwuzla - - Bitwuzla

Parallel Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Unsolved Abstained Timeout Memout
Bitwuzla 0 2589 844.76 844.76 0 1165 0 0 0
Yices2 0 2584 533.96 533.96 0 1165 0 3 0
cvc5 0 2463 6061.97 6061.97 0 1165 0 7 0
SMTInterpol 0 2051 364770.45 358455.47 0 1165 0 176 0

24 seconds Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Unsolved Abstained Timeout Memout
Bitwuzla 0 2515 345.84 345.84 0 1162 3 0 0
Yices2 0 2450 196.25 196.25 0 1162 3 2 0
cvc5 0 2272 1618.96 1618.96 0 1136 29 0 0
SMTInterpol 0 795 3463.89 3463.89 0 387 778 5 0