SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

UFDTLIRA (Single Query Track)

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

Results were generated on 2025-08-11

Benchmarks: 3382
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 2988 5457.48 5826.33 2988 553 2435 394 0 147 5
iProver v3.9.3 0 2286 52298.13 15298.30 2354 0 2354 1028 0 1028 0
SMTInterpol 1 2762 8252.54 5650.98 2763 469 2294 619 0 150 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 2988 5457.48 5826.33 2988 553 2435 394 0 147 5
iProver v3.9.3 0 2354 241216.95 63097.72 2354 0 2354 1028 0 1028 0
SMTInterpol 1 2762 8252.54 5650.98 2763 469 2294 619 0 150 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 553 5025.98 5093.03 553 553 0 0 2829 0 0
SMTInterpol 0 462 287.89 241.28 462 462 0 91 2829 0 0
iProver v3.9.3 0 0 0.00 0.00 0 0 0 553 2829 553 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 2435 431.50 733.30 2435 0 2435 1 946 1 0
iProver v3.9.3 0 2354 241216.95 63097.72 2354 0 2354 82 946 82 0
SMTInterpol 1 2294 7950.84 5403.70 2295 1 2294 141 946 106 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 2964 594.47 959.63 2964 529 2435 1 417 0 0
iProver v3.9.3 0 2138 14159.53 5274.39 2138 0 2138 0 1244 0 0
SMTInterpol 1 2748 4485.92 2367.40 2749 469 2280 433 200 0 0