SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_AUFBV (Unsat Core Track)

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

Results were generated on 2025-08-11

Benchmarks: 36
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 18398 1388.50 1392.79 33 33 3 0 3 0
Yices2 0 18036 480.00 483.85 31 31 5 0 5 0
SMTInterpol 0 10228 223.51 136.77 22 22 14 0 13 0
cvc5 0 4427 16.80 19.88 25 25 11 0 10 1

Parallel Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved UNSAT Unsolved Abstained Timeout Memout
Bitwuzla 0 18398 1388.50 1392.79 33 33 3 0 3 0
Yices2 0 18036 480.00 483.85 31 31 5 0 5 0
SMTInterpol 0 10228 223.51 136.77 22 22 14 0 13 0
cvc5 0 4427 16.80 19.88 25 25 11 0 10 1

UNSAT Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved UNSAT Unsolved Abstained Timeout Memout
Bitwuzla 0 18398 1388.50 1392.79 33 33 3 0 3 0
Yices2 0 18036 480.00 483.85 31 31 5 0 5 0
SMTInterpol 0 10228 223.51 136.77 22 22 14 0 13 0
cvc5 0 4427 16.80 19.88 25 25 11 0 10 1

24 seconds Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved UNSAT Unsolved Abstained Timeout Memout
Bitwuzla 0 16038 132.30 135.89 29 29 0 7 0 0
Yices2 0 13094 91.31 94.36 25 25 0 11 0 0
SMTInterpol 0 9450 105.03 42.80 21 21 0 15 0 0
cvc5 0 4427 16.80 19.88 25 25 0 11 0 0