SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_NonLinearIntArith (Incremental Track)

Competition results for the QF_NonLinearIntArith division in the Incremental Track. Chart

Results were generated on 2025-08-11

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

Logics:

Winners

Parallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24 seconds Performance (parallel)
Z3-Inc-Z3++--Yices2

Parallel Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedUnsolvedAbstainedTimeoutMemout
Z3-Inc-Z3++04228444
(base +1576)		37335.6637336.380119070
SMTInterpol0420245930562.6430304.7801190160
cvc501693653129698.38129769.63011901060
Yices2031414199078.2999125.4801190860
Z3-Inc-Z3++-base n0422686890321.7990360.2801190690
(base +/- n): for derived solvers: increment over base solver
n: non-competing solver

24 seconds Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedUnsolvedAbstainedTimeoutMemout
Yices203659154.16154.1601910010
SMTInterpol01585288.24288.240645500
Z3-Inc-Z3++01250
(base -81)		40.1540.150911000
cvc50103521.1721.170511400
Z3-Inc-Z3++-base n0133168.6168.6101210720
(base +/- n): for derived solvers: increment over base solver
n: non-competing solver