SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_NonLinearIntArith (Unsat Core Track)

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

Results were generated on 2025-08-11

Benchmarks: 2477
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 29446 25902.02 26168.97 2160 2160 317 0 317 0
cvc5 0 26614 86637.44 86895.43 1978 1978 499 0 499 0
SMTInterpol 0 430 451.78 285.45 27 27 2450 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 29446 25902.02 26168.97 2160 2160 317 0 317 0
cvc5 0 26614 86637.44 86895.43 1978 1978 499 0 499 0
SMTInterpol 0 430 451.78 285.45 27 27 2450 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 29446 25902.02 26168.97 2160 2160 317 0 317 0
cvc5 0 26614 86637.44 86895.43 1978 1978 499 0 499 0
SMTInterpol 0 430 451.78 285.45 27 27 2450 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 28124 3313.41 3562.45 2041 2041 0 436 0 0
cvc5 0 22164 4316.47 4517.66 1630 1630 0 847 0 0
SMTInterpol 0 423 47.37 27.75 23 23 2442 12 0 0