SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_UFNIA (Single Query Track)

Competition results for the QF_UFNIA logic in the Single Query Track. Chart

Results were generated on 2025-08-11

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

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24 seconds Performance (parallel)
Yices2Yices2Yices2cvc5Yices2

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices2026411704.6111739.3426422836750732
cvc5017110974.4910997.231711254616801680
SMTInterpol013422361.1620265.99134103312050860

Parallel Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices2026411704.6111739.3426422836750732
cvc5017110974.4910997.231711254616801680
SMTInterpol013422361.1620265.99134103312050860

SAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices202289951.029980.992282280510632
cvc5012510515.5510532.4612512501081061080
SMTInterpol010320307.1718493.161031030130106410

UNSAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc5046458.95464.7646046928490
Yices20361753.601758.353603619284190
SMTInterpol0312053.981772.82310312428460

24 seconds Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices20203575.98601.3420317132013600
cvc50133237.71254.221339241020600
SMTInterpol058266.61143.465837219718400