SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

AUFLIRA (Single Query Track)

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

Results were generated on 2025-08-11

Benchmarks: 1683
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 - 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 1575 5371.33 5567.28 1575 0 1575 108 0 106 0
iProver v3.9.3 0 1348 58649.32 16100.75 1433 0 1433 250 0 250 0
SMTInterpol 0 1217 25295.42 18478.11 1220 0 1220 463 0 307 0
UltimateEliminator+MathSAT 0 12 63.31 27.14 12 0 12 1671 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 1575 5371.33 5567.28 1575 0 1575 108 0 106 0
iProver v3.9.3 0 1433 303158.38 77966.71 1433 0 1433 250 0 250 0
SMTInterpol 0 1220 29726.15 21512.77 1220 0 1220 463 0 307 0
UltimateEliminator+MathSAT 0 12 63.31 27.14 12 0 12 1671 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
SMTInterpol 0 0 0.00 0.00 0 0 0 42 1641 40 0
UltimateEliminator+MathSAT 0 0 0.00 0.00 0 0 0 42 1641 0 0
cvc5 0 0 0.00 0.00 0 0 0 42 1641 40 0
iProver v3.9.3 0 0 0.00 0.00 0 0 0 42 1641 42 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 1575 5371.33 5567.28 1575 0 1575 0 108 0 0
iProver v3.9.3 0 1433 303158.38 77966.71 1433 0 1433 142 108 142 0
SMTInterpol 0 1220 29726.15 21512.77 1220 0 1220 355 108 230 0
UltimateEliminator+MathSAT 0 12 63.31 27.14 12 0 12 1563 108 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 1515 320.50 508.33 1515 0 1515 0 168 0 0
iProver v3.9.3 0 1196 10183.92 3448.10 1196 0 1196 0 487 0 0
SMTInterpol 0 1084 5594.49 3425.06 1084 0 1084 1 598 0 0
UltimateEliminator+MathSAT 0 12 63.31 27.14 12 0 12 1671 0 0 0