SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

UFBVLIA (Single Query Track)

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

Results were generated on 2025-08-11

Benchmarks: 208
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 2 26.47 26.72 2 0 2 206 0 206 0
SMTInterpol 0 0 0.00 0.00 0 0 0 208 0 208 0
UltimateEliminator+MathSAT 0 0 0.00 0.00 0 0 0 208 0 65 48

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 2 26.47 26.72 2 0 2 206 0 206 0
SMTInterpol 0 0 0.00 0.00 0 0 0 208 0 208 0
UltimateEliminator+MathSAT 0 0 0.00 0.00 0 0 0 208 0 65 48

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 20 188 20 0
UltimateEliminator+MathSAT 0 0 0.00 0.00 0 0 0 20 188 0 0
cvc5 0 0 0.00 0.00 0 0 0 20 188 20 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 2 26.47 26.72 2 0 2 6 200 6 0
SMTInterpol 0 0 0.00 0.00 0 0 0 8 200 8 0
UltimateEliminator+MathSAT 0 0 0.00 0.00 0 0 0 8 200 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 1 1.08 1.20 1 0 1 0 207 0 0