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

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

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Timeout
Z3-alpha	1 (base +0)	4.64	4.76	1	1	1	1
z3siri	1 (base +0)	4.73	4.85	1	1	1	1
cvc5	1	236.92	237.09	1	1	1	1
SMTInterpol	0	0.00	0.00	0	0	2	1
Yices2	0	0.00	0.00	0	0	2	2
Z3-alpha-base ⁿ	1	4.55	4.67	1	1	1	1
z3siri-base ⁿ	1	4.80	4.93	1	1	1	1

(base +/- n): for derived solvers: increment over base solver
ⁿ: non-competing solver

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Timeout
Z3-alpha	1 (base +0)	4.64	4.76	1	1	1	1
z3siri	1 (base +0)	4.73	4.85	1	1	1	1
cvc5	1	236.92	237.09	1	1	1	1
SMTInterpol	0	0.00	0.00	0	0	2	1
Yices2	0	0.00	0.00	0	0	2	2
Z3-alpha-base ⁿ	1	4.55	4.67	1	1	1	1
z3siri-base ⁿ	1	4.80	4.93	1	1	1	1

(base +/- n): for derived solvers: increment over base solver
ⁿ: non-competing solver

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout
Z3-alpha	1 (base +0)	4.64	4.76	1	1	0	1	0
z3siri	1 (base +0)	4.73	4.85	1	1	0	1	0
cvc5	1	236.92	237.09	1	1	0	1	0
SMTInterpol	0	0.00	0.00	0	0	1	1	0
Yices2	0	0.00	0.00	0	0	1	1	1
Z3-alpha-base ⁿ	1	4.55	4.67	1	1	0	1	0
z3siri-base ⁿ	1	4.80	4.93	1	1	0	1	0

(base +/- n): for derived solvers: increment over base solver
ⁿ: non-competing solver

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Abstained
Z3-alpha	1 (base +0)	4.64	4.76	1	1	1
z3siri	1 (base +0)	4.73	4.85	1	1	1
Z3-alpha-base ⁿ	1	4.55	4.67	1	1	1
z3siri-base ⁿ	1	4.80	4.93	1	1	1

(base +/- n): for derived solvers: increment over base solver
ⁿ: non-competing solver

SMT-COMP 2025