SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

UFLIA (Single Query Track)

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

Results were generated on 2025-08-11

Benchmarks: 2849
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 SMTInterpol 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 1656 33743.71 33950.87 1656 2 1654 1193 0 1176 0
iProver v3.9.3 0 664 81662.42 21773.15 786 0 786 2063 0 2063 0
SMTInterpol 0 381 28140.69 22980.50 382 4 378 2467 0 1754 0
UltimateEliminator+MathSAT 0 0 0.00 0.00 0 0 0 2849 0 1 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 1656 33743.71 33950.87 1656 2 1654 1193 0 1176 0
iProver v3.9.3 0 786 436647.04 111469.05 786 0 786 2063 0 2063 0
SMTInterpol 0 382 29636.45 23994.28 382 4 378 2467 0 1754 0
UltimateEliminator+MathSAT 0 0 0.00 0.00 0 0 0 2849 0 1 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 4 2.72 2.16 4 4 0 5 2840 0 0
cvc5 0 2 1081.38 1081.81 2 2 0 7 2840 3 0
UltimateEliminator+MathSAT 0 0 0.00 0.00 0 0 0 9 2840 0 0
iProver v3.9.3 0 0 0.00 0.00 0 0 0 9 2840 9 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 1654 32662.33 32869.06 1654 0 1654 52 1143 52 0
iProver v3.9.3 0 786 436647.04 111469.05 786 0 786 920 1143 920 0
SMTInterpol 0 378 29633.73 23992.12 378 0 378 1328 1143 1140 0
UltimateEliminator+MathSAT 0 0 0.00 0.00 0 0 0 1706 1143 1 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 1505 1896.97 2081.17 1505 0 1505 0 1344 0 0
iProver v3.9.3 0 424 11855.72 3543.22 424 0 424 0 2425 0 0
SMTInterpol 0 296 2107.51 941.41 296 4 292 72 2481 0 0
UltimateEliminator+MathSAT 0 0 0.00 0.00 0 0 0 2843 6 0 0