SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_UFLIA (Unsat Core Track)

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

Results were generated on 2025-08-11

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

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24 seconds Performance (parallel)
SMTInterpolSMTInterpol-SMTInterpolYices2

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved UNSATUnsolvedAbstainedTimeoutMemout
SMTInterpol0123129705.68572.8223230000
Yices20123052379.04381.9523230000
cvc50103371339.45342.2922221010
OpenSMT (min-ucore)2202.224.0515158050
OpenSMT3192.103.9615158040

Parallel Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved UNSATUnsolvedAbstainedTimeoutMemout
SMTInterpol0123129705.68572.8223230000
Yices20123052379.04381.9523230000
cvc50103371339.45342.2922221010
OpenSMT (min-ucore)2202.224.0515158050
OpenSMT3192.103.9615158040

UNSAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved UNSATUnsolvedAbstainedTimeoutMemout
SMTInterpol0123129705.68572.8223230000
Yices20123052379.04381.9523230000
cvc50103371339.45342.2922221010
OpenSMT (min-ucore)2202.224.0515158050
OpenSMT3192.103.9615158040

24 seconds Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices201046188.8211.4121210200
cvc501041616.9319.4620200300
SMTInterpol0929147.9724.8219190400
OpenSMT (min-ucore)1202.224.0515152600
OpenSMT2192.103.9615153500