SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_DT (Unsat Core Track)

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

Results were generated on 2025-08-11

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

Winners

Sequential Performance Parallel Performance SAT Performance (parallel) UNSAT Performance (parallel) 24 seconds Performance (parallel)
cvc5 cvc5 - cvc5 SMTInterpol

Sequential Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved UNSAT Unsolved Abstained Timeout Memout
cvc5 0 1146650 15982.48 16004.34 155 155 145 0 142 0
SMTInterpol 0 38120 2207.96 1201.72 142 142 158 0 71 0

Parallel Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved UNSAT Unsolved Abstained Timeout Memout
cvc5 0 1146650 15982.48 16004.34 155 155 145 0 142 0
SMTInterpol 0 38120 2207.96 1201.72 142 142 158 0 71 0

UNSAT Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved UNSAT Unsolved Abstained Timeout Memout
cvc5 0 1146650 15982.48 16004.34 155 155 145 0 142 0
SMTInterpol 0 38120 2207.96 1201.72 142 142 158 0 71 0

24 seconds Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved UNSAT Unsolved Abstained Timeout Memout
SMTInterpol 0 2403 569.34 251.83 137 137 28 135 0 0
cvc5 0 514 203.53 217.72 114 114 0 186 0 0