SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_UFLRA (Unsat Core Track)

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

Results were generated on 2025-08-11

Benchmarks: 101
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 UNSAT Unsolved Abstained Timeout Memout
cvc5 0 62 501.32 513.93 101 101 0 0 0 0
Yices2 0 58 27.50 39.97 101 101 0 0 0 0
SMTInterpol 0 55 381.03 188.04 98 98 3 0 3 0
OpenSMT (min-ucore) 16 68 127.08 137.12 82 82 19 0 1 0
OpenSMT 17 52 122.66 132.85 82 82 19 0 0 0

Parallel Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved UNSAT Unsolved Abstained Timeout Memout
cvc5 0 62 501.32 513.93 101 101 0 0 0 0
Yices2 0 58 27.50 39.97 101 101 0 0 0 0
SMTInterpol 0 55 381.03 188.04 98 98 3 0 3 0
OpenSMT (min-ucore) 16 68 127.08 137.12 82 82 19 0 1 0
OpenSMT 17 52 122.66 132.85 82 82 19 0 0 0

UNSAT Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved UNSAT Unsolved Abstained Timeout Memout
cvc5 0 62 501.32 513.93 101 101 0 0 0 0
Yices2 0 58 27.50 39.97 101 101 0 0 0 0
SMTInterpol 0 55 381.03 188.04 98 98 3 0 3 0
OpenSMT (min-ucore) 16 68 127.08 137.12 82 82 19 0 1 0
OpenSMT 17 52 122.66 132.85 82 82 19 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
cvc5 0 59 50.70 62.87 98 98 0 3 0 0
Yices2 0 58 27.50 39.97 101 101 0 0 0 0
SMTInterpol 0 55 309.60 132.62 97 97 0 4 0 0
OpenSMT (min-ucore) 16 65 21.77 31.41 79 79 18 4 0 0
OpenSMT 17 49 16.20 26.01 79 79 19 3 0 0