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 Performance Parallel Performance SAT Performance (parallel) UNSAT Performance (parallel) 24 seconds Performance (parallel)
cvc5 cvc5 - cvc5 Yices2

Sequential Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved UNSAT Unsolved Abstained Timeout Memout
cvc5 0 45300 511.14 534.97 191 191 5 0 4 0
SMTInterpol 0 13705 1272.12 1088.54 151 151 45 0 1 0
Yices2 0 12112 127.05 149.71 184 184 12 0 12 0

Parallel Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved UNSAT Unsolved Abstained Timeout Memout
cvc5 0 45300 511.14 534.97 191 191 5 0 4 0
SMTInterpol 0 13705 1272.12 1088.54 151 151 45 0 1 0
Yices2 0 12112 127.05 149.71 184 184 12 0 12 0

UNSAT Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved UNSAT Unsolved Abstained Timeout Memout
cvc5 0 45300 511.14 534.97 191 191 5 0 4 0
SMTInterpol 0 13705 1272.12 1088.54 151 151 45 0 1 0
Yices2 0 12112 127.05 149.71 184 184 12 0 12 0

24 seconds Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved UNSAT Unsolved Abstained Timeout Memout
Yices2 0 10107 89.82 112.32 183 183 0 13 0 0
cvc5 0 4481 59.68 82.67 185 185 1 10 0 0
SMTInterpol 0 2059 92.60 75.46 144 144 44 8 0 0