SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_NonLinearRealArith (Unsat Core Track)

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

Results were generated on 2025-08-11

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

Logics:

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 186973 10165.92 10195.58 230 230 70 0 69 1
SMTInterpol 0 17191 15.30 5.60 3 3 297 0 0 0
cvc5 0 14415 51255.64 51298.05 286 286 14 0 14 0

Parallel Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved UNSAT Unsolved Abstained Timeout Memout
Yices2 0 186973 10165.92 10195.58 230 230 70 0 69 1
SMTInterpol 0 17191 15.30 5.60 3 3 297 0 0 0
cvc5 0 14415 51255.64 51298.05 286 286 14 0 14 0

UNSAT Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved UNSAT Unsolved Abstained Timeout Memout
Yices2 0 186973 10165.92 10195.58 230 230 70 0 69 1
SMTInterpol 0 17191 15.30 5.60 3 3 297 0 0 0
cvc5 0 14415 51255.64 51298.05 286 286 14 0 14 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 61372 759.64 779.50 161 161 0 139 0 0
SMTInterpol 0 17191 15.30 5.60 3 3 260 37 0 0
cvc5 0 13704 561.05 577.94 135 135 0 165 0 0