SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

ALIA (Single Query Track)

Competition results for the ALIA logic in the Single Query Track. Chart

Results were generated on 2025-08-11

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

Winners

Sequential Performance Parallel Performance SAT Performance (parallel) UNSAT Performance (parallel) 24 seconds Performance (parallel)
cvc5 cvc5 UltimateEliminator+MathSAT iProver v3.9.3 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 329 27861.67 27905.47 329 50 279 1208 0 608 0
iProver v3.9.3 0 266 23078.29 6206.60 299 0 299 1238 0 1227 0
SMTInterpol 0 220 10185.09 7856.56 221 18 203 1316 0 389 0
UltimateEliminator+MathSAT 0 158 655.72 309.67 158 136 22 1379 0 0 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 329 27861.67 27905.47 329 50 279 1208 0 608 0
iProver v3.9.3 0 299 107315.40 27519.75 299 0 299 1238 0 1227 0
SMTInterpol 0 221 11585.39 8813.39 221 18 203 1316 0 389 0
UltimateEliminator+MathSAT 0 158 655.72 309.67 158 136 22 1379 0 0 0

SAT Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
UltimateEliminator+MathSAT 0 136 557.38 264.18 136 136 0 46 1355 0 0
cvc5 0 50 10658.57 10665.95 50 50 0 132 1355 4 0
SMTInterpol 0 11 91.05 73.31 11 11 0 171 1355 5 0
iProver v3.9.3 0 0 0.00 0.00 0 0 0 182 1355 182 0

UNSAT Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
iProver v3.9.3 0 299 107315.40 27519.75 299 0 299 60 1178 60 0
cvc5 0 279 17203.10 17239.53 279 0 279 80 1178 48 0
SMTInterpol 0 200 10863.57 8229.65 200 0 200 159 1178 85 0
UltimateEliminator+MathSAT 0 22 98.34 45.49 22 0 22 337 1178 0 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 246 180.50 210.72 246 26 220 346 945 0 0
iProver v3.9.3 0 188 2702.74 851.39 188 0 188 10 1339 0 0
SMTInterpol 0 173 339.98 196.46 173 16 157 790 574 0 0
UltimateEliminator+MathSAT 0 158 655.72 309.67 158 136 22 1379 0 0 0