SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_Datatypes (Unsat Core Track)

Competition results for the QF_Datatypes division in the Unsat Core Track. Chart

Results were generated on 2025-08-11

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

Logics:

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24 seconds Performance (parallel)
cvc5cvc5-cvc5SMTInterpol

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc50128410733221.5833249.7918418421602120
SMTInterpol014033211076.175913.3715715724301400

Parallel Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc50128410733221.5833249.7918418421602120
SMTInterpol014033211076.175913.3715715724301400

UNSAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc50128410733221.5833249.7918418421602120
SMTInterpol014033211076.175913.3715715724301400

24 seconds Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved UNSATUnsolvedAbstainedTimeoutMemout
SMTInterpol02403569.34251.831371372823500
cvc50514203.53217.72114114028600