SMT-COMP 2026

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2026

QF_NIA (Unsat Core Track)

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

Results were generated on 2026-07-25

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

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24 seconds Performance (parallel)
Yices2Yices2-Yices2Yices2

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices20105798521.698616.08756756810810
cvc50978930746.6130836.2970370313401340
z3-BooledASS ne08663
(base -41)		3542.933644.42823823140130
SMTInterpol021414.148.731010827000
z3-BooledASS-base n087043648.943751.00824824130130
(base +/- n): for derived solvers: increment over base solver
ne: not eligible for winning as it does not substantially improve over the base solver (at least 10 % improvement in PAR2 score) n: non-competing solver

Parallel Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices20105798521.698616.08756756810810
cvc50978930746.6130836.2970370313401340
z3-BooledASS ne08663
(base -41)		3542.933644.42823823140130
SMTInterpol021414.148.731010827000
z3-BooledASS-base n087043648.943751.00824824130130
(base +/- n): for derived solvers: increment over base solver
ne: not eligible for winning as it does not substantially improve over the base solver (at least 10 % improvement in PAR2 score) n: non-competing solver

UNSAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices20105798521.698616.08756756810810
cvc50978930746.6130836.2970370313401340
z3-BooledASS ne08663
(base -41)		3542.933644.42823823140130
SMTInterpol021414.148.731010827000
z3-BooledASS-base n087043648.943751.00824824130130
(base +/- n): for derived solvers: increment over base solver
ne: not eligible for winning as it does not substantially improve over the base solver (at least 10 % improvement in PAR2 score) n: non-competing solver

24 seconds Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices20101121273.931364.09727727011000
cvc5089261366.381441.05606606023100
z3-BooledASS ne08528
(base -39)		1330.331428.9680280203500
SMTInterpol021414.148.731010827000
z3-BooledASS-base n085671303.631402.6080180103600
(base +/- n): for derived solvers: increment over base solver
ne: not eligible for winning as it does not substantially improve over the base solver (at least 10 % improvement in PAR2 score) n: non-competing solver