SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_NIA (Unsat Core Track)

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

Results were generated on 2025-08-11

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

Winners

Sequential Performance Parallel Performance SAT Performance (parallel) UNSAT Performance (parallel) 24 seconds Performance (parallel)
Yices2 Yices2 - Yices2 Yices2

Sequential Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved UNSAT Unsolved Abstained Timeout Memout
Yices2 0 29419 25901.88 26168.71 2159 2159 316 0 316 0
cvc5 0 26590 86554.45 86812.18 1976 1976 499 0 499 0
SMTInterpol 0 403 451.25 284.96 26 26 2449 0 2 0

Parallel Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved UNSAT Unsolved Abstained Timeout Memout
Yices2 0 29419 25901.88 26168.71 2159 2159 316 0 316 0
cvc5 0 26590 86554.45 86812.18 1976 1976 499 0 499 0
SMTInterpol 0 403 451.25 284.96 26 26 2449 0 2 0

UNSAT Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved UNSAT Unsolved Abstained Timeout Memout
Yices2 0 29419 25901.88 26168.71 2159 2159 316 0 316 0
cvc5 0 26590 86554.45 86812.18 1976 1976 499 0 499 0
SMTInterpol 0 403 451.25 284.96 26 26 2449 0 2 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 28097 3313.27 3562.20 2040 2040 0 435 0 0
cvc5 0 22140 4316.31 4517.37 1629 1629 0 846 0 0
SMTInterpol 0 396 46.85 27.27 22 22 2442 11 0 0