SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

Equality_NonLinearArith (Single Query Track)

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

Results were generated on 2025-08-11

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

Logics:

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24 seconds Performance (parallel)
cvc5cvc5cvc5cvc5cvc5

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc506722268105.11268967.71672271260103510031361
iProver v3.9.303992393224.91103781.3645110451157210568239
SMTInterpol0292422955.3315345.6829248028447308034040
UltimateEliminator+MathSAT06199612.568253.36619434185634132724760

Parallel Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc506722268105.11268967.71672271260103510031361
iProver v3.9.3045111893686.16481584.8145110451157210568239
SMTInterpol0292422955.3315345.6829248028447308034040
UltimateEliminator+MathSAT06199612.568253.36619434185634132724760

SAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc5071231881.7331973.82712712081943950
UltimateEliminator+MathSAT04348600.117645.99434434035994392360
SMTInterpol08056.0845.04808007139439590
iProver v3.9.3000.000.0000079394397930

UNSAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc506010236223.38236993.8960100601037138512971
iProver v3.9.3045111893686.16481584.8145110451118703851183139
SMTInterpol0284422899.2515300.642844028443537385117620
UltimateEliminator+MathSAT01851012.45607.371850185324468031480

24 seconds Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc5058754500.965224.8658756425233362399500
iProver v3.9.30311639898.2512635.103116031160711600
SMTInterpol028769704.944353.1628768027962700465600
UltimateEliminator+MathSAT05903617.732332.735904071835806383600