SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_LIRA (Single Query Track)

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

Results were generated on 2025-08-11

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

Winners

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

Sequential Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
Z3-alpha 0 6
(base +0) 		71.76 72.50 6 1 5 1 0 1 0
Yices2 0 6 191.53 192.28 6 1 5 1 0 1 0
cvc5 0 6 839.09 840.00 6 1 5 1 0 1 0
SMTInterpol 0 4 122.45 70.09 4 1 3 3 0 3 0
Z3-alpha-base n 0 6 71.98 72.73 6 1 5 1 0 1 0
(base +/- n): for derived solvers: increment over base solver
n: non-competing solver

Parallel Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
Z3-alpha 0 6
(base +0) 		71.76 72.50 6 1 5 1 0 1 0
Yices2 0 6 191.53 192.28 6 1 5 1 0 1 0
cvc5 0 6 839.09 840.00 6 1 5 1 0 1 0
SMTInterpol 0 4 122.45 70.09 4 1 3 3 0 3 0
Z3-alpha-base n 0 6 71.98 72.73 6 1 5 1 0 1 0
(base +/- n): for derived solvers: increment over base solver
n: non-competing solver

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 1 0.19 0.31 1 1 0 0 6 0 0
Z3-alpha 0 1
(base +0) 		2.33 2.44 1 1 0 0 6 0 0
cvc5 0 1 2.40 2.51 1 1 0 0 6 0 0
SMTInterpol 0 1 20.12 8.79 1 1 0 0 6 0 0
Z3-alpha-base n 0 1 2.29 2.41 1 1 0 0 6 0 0
(base +/- n): for derived solvers: increment over base solver
n: non-competing solver

UNSAT Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
Z3-alpha 0 5
(base +0) 		69.43 70.05 5 0 5 0 2 0 0
Yices2 0 5 191.34 191.97 5 0 5 0 2 0 0
cvc5 0 5 836.70 837.48 5 0 5 0 2 0 0
SMTInterpol 0 3 102.33 61.30 3 0 3 2 2 2 0
Z3-alpha-base n 0 5 69.69 70.32 5 0 5 0 2 0 0
(base +/- n): for derived solvers: increment over base solver
n: non-competing solver

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 5 0.95 1.55 5 1 4 0 2 0 0
Z3-alpha 0 5
(base +0) 		7.51 8.11 5 1 4 0 2 0 0
cvc5 0 5 10.02 10.63 5 1 4 0 2 0 0
SMTInterpol 0 3 33.95 13.97 3 1 2 0 4 0 0
Z3-alpha-base n 0 5 7.37 7.99 5 1 4 0 2 0 0
(base +/- n): for derived solvers: increment over base solver
n: non-competing solver