SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_NIRA (Single Query Track)

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

Results were generated on 2025-08-11

Benchmarks: 2
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 - Z3-alpha Z3-alpha

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 1
(base +0) 		4.64 4.76 1 0 1 1 0 1 0
z3siri 0 1
(base +0) 		4.73 4.85 1 0 1 1 0 1 0
cvc5 0 1 236.92 237.09 1 0 1 1 0 1 0
SMTInterpol 0 0 0.00 0.00 0 0 0 2 0 1 0
Yices2 0 0 0.00 0.00 0 0 0 2 0 2 0
Z3-alpha-base n 0 1 4.55 4.67 1 0 1 1 0 1 0
z3siri-base n 0 1 4.80 4.93 1 0 1 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 1
(base +0) 		4.64 4.76 1 0 1 1 0 1 0
z3siri 0 1
(base +0) 		4.73 4.85 1 0 1 1 0 1 0
cvc5 0 1 236.92 237.09 1 0 1 1 0 1 0
SMTInterpol 0 0 0.00 0.00 0 0 0 2 0 1 0
Yices2 0 0 0.00 0.00 0 0 0 2 0 2 0
Z3-alpha-base n 0 1 4.55 4.67 1 0 1 1 0 1 0
z3siri-base n 0 1 4.80 4.93 1 0 1 1 0 1 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 1
(base +0) 		4.64 4.76 1 0 1 0 1 0 0
z3siri 0 1
(base +0) 		4.73 4.85 1 0 1 0 1 0 0
cvc5 0 1 236.92 237.09 1 0 1 0 1 0 0
SMTInterpol 0 0 0.00 0.00 0 0 0 1 1 0 0
Yices2 0 0 0.00 0.00 0 0 0 1 1 1 0
Z3-alpha-base n 0 1 4.55 4.67 1 0 1 0 1 0 0
z3siri-base n 0 1 4.80 4.93 1 0 1 0 1 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
Z3-alpha 0 1
(base +0) 		4.64 4.76 1 0 1 0 1 0 0
z3siri 0 1
(base +0) 		4.73 4.85 1 0 1 0 1 0 0
Z3-alpha-base n 0 1 4.55 4.67 1 0 1 0 1 0 0
z3siri-base n 0 1 4.80 4.93 1 0 1 0 1 0 0
(base +/- n): for derived solvers: increment over base solver
n: non-competing solver