SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

Arith (Single Query Track)

Competition results for the Arith division in the Single Query Track. Chart

Results were generated on 2025-08-11

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

Logics:

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24 seconds Performance (parallel)
Z3-alphaZ3-alphaZ3-alphaZ3-alphaZ3-alpha

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Z3-alpha01474
(base -23)		30071.798145.931515588927151013910
YicesQS013821184.281353.56138257580728402840
cvc50138249381.6949558.83138252785528402840
UltimateEliminator+MathSAT0119219554.3514310.52119244774547402680
iProver v3.9.3035534918.579232.9943104311235012260
SMTInterpol02532592.361894.392532023314130980
SMT-RAT09626.5538.57964923156730
Amaya23965695.495745.7739813925915611121893
Z3-alpha-base n0149742872.9643062.49149758391416901621
(base +/- n): for derived solvers: increment over base solver
n: non-competing solver

Parallel Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Z3-alpha01515
(base +18)		143774.8636599.761515588927151013910
YicesQS013821184.281353.56138257580728402840
cvc50138249381.6949558.83138252785528402840
UltimateEliminator+MathSAT0119219554.3514310.52119244774547402680
iProver v3.9.30431262315.0866595.7643104311235012260
SMTInterpol02532592.361894.392532023314130980
SMT-RAT09626.5538.57964923156730
Amaya23965695.495745.7739813925915611121893
Z3-alpha-base n0149742872.9643062.49149758391416901621
(base +/- n): for derived solvers: increment over base solver
n: non-competing solver

SAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Z3-alpha0588
(base +5)		25036.636506.31588588088990835
YicesQS0575198.82269.2757557501019901010
cvc505276406.076471.9752752701499901490
UltimateEliminator+MathSAT044710352.618055.0044744702299901170
SMTInterpol02026.7215.7920200656990730
SMT-RAT0410.0710.574401166110
iProver v3.9.3000.000.000006769906730
Amaya21393579.023596.95141139211814071079
Z3-alpha-base n05837630.517703.20583583093990890
(base +/- n): for derived solvers: increment over base solver
n: non-competing solver

UNSAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Z3-alpha0927
(base +13)		118738.2330093.45927092757682505
cvc5085542975.6343086.8685508551296821290
YicesQS0807985.461084.2980708071776821770
UltimateEliminator+MathSAT07459201.746255.5374507452396821490
iProver v3.9.30431262315.0866595.7643104315536825470
Amaya02572116.472148.822570257331376814
SMTInterpol02332565.641878.602330233751682250
SMT-RAT09216.4828.00920921157310
Z3-alpha-base n091435242.4535359.28914091470682680
(base +/- n): for derived solvers: increment over base solver
n: non-competing solver

24 seconds Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Z3-alpha01415
(base +35)		5324.141893.631415568847025100
YicesQS01378420.94589.631378574804028800
cvc501168482.28626.831168471697049800
UltimateEliminator+MathSAT011377868.553405.53113742371420532400
iProver v3.9.302774224.071310.6427702774138500
SMTInterpol02501091.49473.6425020230125516100
SMT-RAT09626.5538.57964920157000
Amaya2375814.30861.3637712225536125300
Z3-alpha-base n013801871.202041.611380555825228400
(base +/- n): for derived solvers: increment over base solver
n: non-competing solver