SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_UFNIA (Unsat Core Track)

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

Results were generated on 2025-08-11

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

Winners

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

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc5045300511.14534.971911915040
SMTInterpol0137051272.121088.5415115145010
Yices2012112127.05149.71184184120120

Parallel Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc5045300511.14534.971911915040
SMTInterpol0137051272.121088.5415115145010
Yices2012112127.05149.71184184120120

UNSAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc5045300511.14534.971911915040
SMTInterpol0137051272.121088.5415115145010
Yices2012112127.05149.71184184120120

24 seconds Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices201010789.82112.3218318301300
cvc50448159.6882.6718518511000
SMTInterpol0205992.6075.4614414444800