SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_ANIA (Single Query Track)

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

Results were generated on 2025-08-11

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

Winners

Sequential Performance Parallel Performance SAT Performance (parallel) UNSAT Performance (parallel) 24 seconds Performance (parallel)
SMTInterpol SMTInterpol SMTInterpol SMTInterpol SMTInterpol

Sequential Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
SMTInterpol 0 132 993.38 653.51 132 116 16 23 0 11 0
Yices2 0 130 3927.52 3944.12 130 115 15 25 0 25 0
cvc5 0 126 7113.62 7130.05 126 111 15 29 0 29 0

Parallel Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
SMTInterpol 0 132 993.38 653.51 132 116 16 23 0 11 0
Yices2 0 130 3927.52 3944.12 130 115 15 25 0 25 0
cvc5 0 126 7113.62 7130.05 126 111 15 29 0 29 0

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 116 333.87 143.78 116 116 0 6 33 0 0
Yices2 0 115 3339.06 3353.75 115 115 0 7 33 7 0
cvc5 0 111 5089.86 5104.18 111 111 0 11 33 11 0

UNSAT Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
SMTInterpol 0 16 659.52 509.73 16 0 16 14 125 11 0
Yices2 0 15 588.46 590.37 15 0 15 15 125 15 0
cvc5 0 15 2023.76 2025.87 15 0 15 15 125 15 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
SMTInterpol 0 129 503.14 224.89 129 116 13 10 16 0 0
cvc5 0 106 369.02 382.10 106 96 10 0 49 0 0
Yices2 0 99 186.92 199.23 99 86 13 0 56 0 0