SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

UFNIA (Single Query Track)

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

Results were generated on 2025-08-11

Benchmarks: 6313
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 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 3772 204859.93 205350.15 3772 707 3065 2541 0 2537 0
iProver v3.9.3 0 1774 254272.00 66708.55 2076 0 2076 4237 0 4237 0
SMTInterpol 0 1032 8121.61 6088.49 1032 76 956 5281 0 2240 0
UltimateEliminator+MathSAT 0 614 9580.35 8240.20 614 431 183 5699 0 467 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 3772 204859.93 205350.15 3772 707 3065 2541 0 2537 0
iProver v3.9.3 0 2076 1134264.25 288106.29 2076 0 2076 4237 0 4237 0
SMTInterpol 0 1032 8121.61 6088.49 1032 76 956 5281 0 2240 0
UltimateEliminator+MathSAT 0 614 9580.35 8240.20 614 431 183 5699 0 467 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 707 30800.88 30892.22 707 707 0 1 5605 1 0
UltimateEliminator+MathSAT 0 431 8587.50 7640.09 431 431 0 277 5605 235 0
SMTInterpol 0 76 54.28 43.23 76 76 0 632 5605 8 0
iProver v3.9.3 0 0 0.00 0.00 0 0 0 708 5605 708 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 3065 174059.05 174457.93 3065 0 3065 110 3138 110 0
iProver v3.9.3 0 2076 1134264.25 288106.29 2076 0 2076 1099 3138 1099 0
SMTInterpol 0 956 8067.33 6045.26 956 0 956 2219 3138 1062 0
UltimateEliminator+MathSAT 0 183 992.86 600.11 183 0 183 2992 3138 142 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 3119 3035.58 3419.91 3119 639 2480 0 3194 0 0
iProver v3.9.3 0 1240 22150.57 6797.26 1240 0 1240 0 5073 0 0
SMTInterpol 0 1019 2867.85 1290.93 1019 76 943 2416 2878 0 0
UltimateEliminator+MathSAT 0 585 3585.52 2319.57 585 404 181 5173 555 0 0