SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_ABV (Incremental Track)

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

Results were generated on 2025-08-11

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

Winners

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

Parallel Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Unsolved Abstained Timeout Memout
Bitwuzla 0 1348 20590.04 20594.54 0 636 0 8 0
Yices2 0 1322 9583.15 9584.97 0 636 0 12 0
SMTInterpol 0 1086 74420.32 72474.87 0 636 0 47 0
cvc5 0 1066 227515.10 227625.81 0 636 0 190 6

24 seconds Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Unsolved Abstained Timeout Memout
Yices2 0 1153 436.55 436.55 0 615 21 3 0
Bitwuzla 0 1051 576.95 576.95 0 589 47 0 0
SMTInterpol 0 866 1644.84 1644.84 0 491 145 5 0
cvc5 0 733 630.61 630.61 0 408 228 4 0