SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

Equality_LinearArith (Single Query Track)

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

Results were generated on 2025-08-11

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

Logics:

Winners

Sequential Performance Parallel Performance SAT Performance (parallel) UNSAT Performance (parallel) 24 seconds Performance (parallel)
cvc5 cvc5 cvc5 cvc5 cvc5

Sequential Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
cvc5 0 13158 172759.48 174403.67 13158 866 12292 3778 0 2891 7
iProver v3.9.3 0 10081 462761.07 127843.03 10597 0 10597 6339 0 6214 0
UltimateEliminator+MathSAT 0 253 1082.74 504.87 253 160 93 7506 9177 1 0
SMTInterpol 1 9424 123710.57 91610.57 9434 576 8858 7502 0 4612 0

Parallel Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
cvc5 0 13158 172759.48 174403.67 13158 866 12292 3778 0 2891 7
iProver v3.9.3 0 10597 1901532.52 491707.38 10597 0 10597 6339 0 6214 0
UltimateEliminator+MathSAT 0 253 1082.74 504.87 253 160 93 7506 9177 1 0
SMTInterpol 1 9433 136639.72 100911.09 9434 576 8858 7502 0 4612 0

SAT Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
cvc5 0 866 57143.55 57254.98 866 866 0 197 15873 50 0
SMTInterpol 0 561 424.02 356.85 561 561 0 502 15873 80 0
UltimateEliminator+MathSAT 0 160 658.35 311.41 160 160 0 265 16511 0 0
iProver v3.9.3 0 0 0.00 0.00 0 0 0 1063 15873 959 0

UNSAT Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
cvc5 0 12292 115615.93 117148.69 12292 0 12292 216 4428 184 0
iProver v3.9.3 0 10597 1901532.52 491707.38 10597 0 10597 1911 4428 1902 0
UltimateEliminator+MathSAT 0 93 424.39 193.46 93 0 93 4838 12005 1 0
SMTInterpol 1 8855 135569.74 100037.05 8856 1 8855 3652 4428 2900 0

24 seconds Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
cvc5 0 12563 6458.28 8008.22 12563 716 11847 356 4017 0 0
iProver v3.9.3 0 8684 81061.24 27761.55 8684 0 8684 97 8155 0 0
UltimateEliminator+MathSAT 0 253 1082.74 504.87 253 160 93 7497 9186 0 0
SMTInterpol 1 8991 28395.66 14572.79 8992 574 8418 1599 6345 0 0