SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_ALIA (Unsat Core Track)

Competition results for the QF_ALIA logic in the Unsat Core Track. Chart

Results were generated on 2025-08-11

Benchmarks: 30
Time Limit: 1200 seconds
Memory Limit: 30720 GB

Winners

Sequential Performance Parallel Performance SAT Performance (parallel) UNSAT Performance (parallel) 24 seconds Performance (parallel)
Yices2 Yices2 - Yices2 Yices2

Sequential Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved UNSAT Unsolved Abstained Timeout Memout
Yices2 0 621 4.61 8.34 30 30 0 0 0 0
SMTInterpol 0 615 24.38 17.22 30 30 0 0 0 0
OpenSMT 0 591 4.66 8.42 30 30 0 0 0 0
OpenSMT (min-ucore) 0 564 2108.04 2111.98 29 29 1 0 1 0
cvc5 0 0 5.13 9.05 30 30 0 0 0 0

Parallel Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved UNSAT Unsolved Abstained Timeout Memout
Yices2 0 621 4.61 8.34 30 30 0 0 0 0
SMTInterpol 0 615 24.38 17.22 30 30 0 0 0 0
OpenSMT 0 591 4.66 8.42 30 30 0 0 0 0
OpenSMT (min-ucore) 0 564 2108.04 2111.98 29 29 1 0 1 0
cvc5 0 0 5.13 9.05 30 30 0 0 0 0

UNSAT Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved UNSAT Unsolved Abstained Timeout Memout
Yices2 0 621 4.61 8.34 30 30 0 0 0 0
SMTInterpol 0 615 24.38 17.22 30 30 0 0 0 0
OpenSMT 0 591 4.66 8.42 30 30 0 0 0 0
OpenSMT (min-ucore) 0 564 2108.04 2111.98 29 29 1 0 1 0
cvc5 0 0 5.13 9.05 30 30 0 0 0 0

24 seconds Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved UNSAT Unsolved Abstained Timeout Memout
Yices2 0 621 4.61 8.34 30 30 0 0 0 0
SMTInterpol 0 615 24.38 17.22 30 30 0 0 0 0
OpenSMT 0 591 4.66 8.42 30 30 0 0 0 0
OpenSMT (min-ucore) 0 458 36.36 39.28 24 24 0 6 0 0
cvc5 0 0 5.13 9.05 30 30 0 0 0 0