SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_ADT_BitVec (Model Validation Track)

Competition results for the QF_ADT_BitVec division in the Model Validation Track. Chart

Results were generated on 2025-08-11

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

Logics:

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 5226 3265.60 3900.44 5226 5226 13 10 3 1
cvc5 0 4771 68365.87 68960.10 4771 4771 478 0 468 7
SMTInterpol 0 3886 307681.94 272191.10 3898 3898 1351 0 1259 0

Parallel Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
Bitwuzla 0 5226 3265.60 3900.44 5226 5226 13 10 3 1
cvc5 0 4771 68365.87 68960.10 4771 4771 478 0 468 7
SMTInterpol 0 3898 322296.69 286326.88 3898 3898 1351 0 1259 0

SAT Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
Bitwuzla 0 5226 3265.60 3900.44 5226 5226 13 10 3 1
cvc5 0 4771 68365.87 68960.10 4771 4771 478 0 468 7
SMTInterpol 0 3898 322296.69 286326.88 3898 3898 1351 0 1259 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 5204 1296.26 1927.97 5204 5204 6 39 0 0
cvc5 0 4220 5834.45 6351.07 4220 4220 3 1026 0 0
SMTInterpol 0 2846 13504.66 5898.18 2846 2846 37 2366 0 0