SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_Equality_NonLinearArith (Unsat Core Track)

Competition results for the QF_Equality_NonLinearArith division in the Unsat Core Track. Chart

Results were generated on 2025-08-11

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

Logics:

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 127567 3055.05 3086.36 248 248 18 0 17 0
SMTInterpol 0 105344 2324.66 1925.28 193 193 73 0 12 0
Yices2 0 91860 624.21 651.44 221 221 40 5 38 2

Parallel Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved UNSAT Unsolved Abstained Timeout Memout
cvc5 0 127567 3055.05 3086.36 248 248 18 0 17 0
SMTInterpol 0 105344 2324.66 1925.28 193 193 73 0 12 0
Yices2 0 91860 624.21 651.44 221 221 40 5 38 2

UNSAT Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved UNSAT Unsolved Abstained Timeout Memout
cvc5 0 127567 3055.05 3086.36 248 248 18 0 17 0
SMTInterpol 0 105344 2324.66 1925.28 193 193 73 0 12 0
Yices2 0 91860 624.21 651.44 221 221 40 5 38 2

24 seconds Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved UNSAT Unsolved Abstained Timeout Memout
Yices2 0 89356 118.34 144.98 217 217 0 49 0 0
SMTInterpol 0 86537 346.84 185.56 183 183 59 24 0 0
cvc5 0 39628 187.43 216.70 236 236 1 29 0 0