SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_NonLinearRealArith (Model Validation Track)

Competition results for the QF_NonLinearRealArith division in the Model Validation Track. Chart

Results were generated on 2025-08-11

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

Logics:

Winners

Sequential Performance Parallel Performance SAT Performance (parallel) UNSAT Performance (parallel) 24 seconds Performance (parallel)
SMT-RAT SMT-RAT SMT-RAT - SMT-RAT

Sequential Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
SMT-RAT 0 2090 22988.57 23250.71 2090 2090 687 0 161 0
cvc5 0 2017 10890.68 11139.67 2017 2017 760 0 188 0
SMTInterpol 0 13 1893.89 1712.80 13 13 2764 0 0 0
Yices2 435 2105 7970.61 8234.82 2105 2105 672 0 103 0

Parallel Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
SMT-RAT 0 2090 22988.57 23250.71 2090 2090 687 0 161 0
cvc5 0 2017 10890.68 11139.67 2017 2017 760 0 188 0
SMTInterpol 0 13 1893.89 1712.80 13 13 2764 0 0 0
Yices2 435 2105 7970.61 8234.82 2105 2105 672 0 103 0

SAT Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
SMT-RAT 0 2090 22988.57 23250.71 2090 2090 687 0 161 0
cvc5 0 2017 10890.68 11139.67 2017 2017 760 0 188 0
SMTInterpol 0 13 1893.89 1712.80 13 13 2764 0 0 0
Yices2 435 2105 7970.61 8234.82 2105 2105 672 0 103 0

24 seconds Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
SMT-RAT 0 2024 628.55 879.06 2024 2024 520 233 0 0
cvc5 0 2000 525.22 770.78 2000 2000 550 227 0 0
SMTInterpol 0 7 38.25 17.37 7 7 2759 11 0 0
Yices2 431 2075 646.72 905.88 2075 2075 561 141 0 0