SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_IDL (Unsat Core Track)

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

Results were generated on 2025-08-11

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

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
cvc505257076510.326513.992121790790
SMTInterpol02905991635.57787.641212880820
Yices201503279395.899399.031515850850
OpenSMT0957766849.076851.511111890890
OpenSMT (min-ucore)01938423.5923.7111990990

Parallel Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc505257076510.326513.992121790790
SMTInterpol02905991635.57787.641212880820
Yices201503279395.899399.031515850850
OpenSMT0957766849.076851.511111890890
OpenSMT (min-ucore)01938423.5923.7111990990

UNSAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc505257076510.326513.992121790790
SMTInterpol02905991635.57787.641212880820
Yices201503279395.899399.031515850850
OpenSMT0957766849.076851.511111890890
OpenSMT (min-ucore)01938423.5923.7111990990

24 seconds Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved UNSATUnsolvedAbstainedTimeoutMemout
SMTInterpol060927134.2366.436609400
OpenSMT (min-ucore)01938423.5923.711109900
cvc50193596.596.711109900
OpenSMT01916114.4014.531109900