SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_ABV (Unsat Core Track)

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

Results were generated on 2025-08-11

Benchmarks: 1865
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 189316 3682.18 3913.54 1855 1855 10 0 10 0
Yices2 0 182279 10856.85 11085.68 1851 1851 14 0 14 0
SMTInterpol 0 172015 6336.51 5147.62 1723 1723 142 0 140 0
cvc5 0 152584 6397.74 6628.38 1852 1852 13 0 13 0

Parallel Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved UNSAT Unsolved Abstained Timeout Memout
Bitwuzla 0 189316 3682.18 3913.54 1855 1855 10 0 10 0
Yices2 0 182279 10856.85 11085.68 1851 1851 14 0 14 0
SMTInterpol 0 172015 6336.51 5147.62 1723 1723 142 0 140 0
cvc5 0 152584 6397.74 6628.38 1852 1852 13 0 13 0

UNSAT Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved UNSAT Unsolved Abstained Timeout Memout
Bitwuzla 0 189316 3682.18 3913.54 1855 1855 10 0 10 0
Yices2 0 182279 10856.85 11085.68 1851 1851 14 0 14 0
SMTInterpol 0 172015 6336.51 5147.62 1723 1723 142 0 140 0
cvc5 0 152584 6397.74 6628.38 1852 1852 13 0 13 0

24 seconds Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved UNSAT Unsolved Abstained Timeout Memout
Bitwuzla 0 179297 2109.66 2338.54 1837 1837 0 28 0 0
Yices2 0 171633 1356.51 1580.82 1826 1826 0 39 0 0
SMTInterpol 0 154074 1746.39 1141.91 1702 1702 1 162 0 0
cvc5 0 141855 532.50 747.56 1734 1734 0 131 0 0