SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_AX (Single Query Track)

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

Results were generated on 2025-08-11

Benchmarks: 300
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 Yices2

Sequential Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
Yices2 0 300 46.58 83.85 300 148 152 0 0 0 0
cvc5 0 300 106.98 144.13 300 148 152 0 0 0 0
OpenSMT 0 300 136.31 173.55 300 148 152 0 0 0 0
SMTInterpol 0 300 636.65 315.09 300 148 152 0 0 0 0

Parallel Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
Yices2 0 300 46.58 83.85 300 148 152 0 0 0 0
cvc5 0 300 106.98 144.13 300 148 152 0 0 0 0
OpenSMT 0 300 136.31 173.55 300 148 152 0 0 0 0
SMTInterpol 0 300 636.65 315.09 300 148 152 0 0 0 0

SAT Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
Yices2 0 148 22.16 40.54 148 148 0 0 152 0 0
cvc5 0 148 27.17 45.49 148 148 0 0 152 0 0
OpenSMT 0 148 32.01 50.36 148 148 0 0 152 0 0
SMTInterpol 0 148 145.02 90.63 148 148 0 0 152 0 0

UNSAT Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
Yices2 0 152 24.42 43.31 152 0 152 0 148 0 0
cvc5 0 152 79.81 98.64 152 0 152 0 148 0 0
OpenSMT 0 152 104.31 123.19 152 0 152 0 148 0 0
SMTInterpol 0 152 491.63 224.46 152 0 152 0 148 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
Yices2 0 300 46.58 83.85 300 148 152 0 0 0 0
cvc5 0 300 106.98 144.13 300 148 152 0 0 0 0
OpenSMT 0 300 136.31 173.55 300 148 152 0 0 0 0
SMTInterpol 0 300 636.65 315.09 300 148 152 0 0 0 0