SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_ABV (Model Validation Track)

Competition results for the QF_ABV logic in the Model Validation Track. Chart

Results were generated on 2025-08-11

Benchmarks: 5214
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 SAT Unsolved Abstained Timeout Memout
Bitwuzla 0 5201 2609.08 3240.72 5201 5201 13 0 3 1
cvc5 0 4749 67426.48 68017.84 4749 4749 465 0 458 5
SMTInterpol 0 3875 304943.37 269652.26 3887 3887 1327 0 1247 0

Parallel Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
Bitwuzla 0 5201 2609.08 3240.72 5201 5201 13 0 3 1
cvc5 0 4749 67426.48 68017.84 4749 4749 465 0 458 5
SMTInterpol 0 3887 319558.12 283788.03 3887 3887 1327 0 1247 0

SAT Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
Bitwuzla 0 5201 2609.08 3240.72 5201 5201 13 0 3 1
cvc5 0 4749 67426.48 68017.84 4749 4749 465 0 458 5
SMTInterpol 0 3887 319558.12 283788.03 3887 3887 1327 0 1247 0

24 seconds Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
Bitwuzla 0 5188 1270.07 1899.79 5188 5188 6 20 0 0
cvc5 0 4202 5723.20 6237.62 4202 4202 2 1010 0 0
SMTInterpol 0 2842 13491.05 5892.83 2842 2842 31 2341 0 0