SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_IDL (Single Query Track)

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

Results were generated on 2025-08-11

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

Winners

Sequential Performance Parallel Performance SAT Performance (parallel) UNSAT Performance (parallel) 24 seconds Performance (parallel)
Yices2 Z3-alpha Z3-alpha cvc5 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 977 30949.40 31074.60 977 642 335 231 0 231 0
Z3-alpha 0 969
(base -67) 		72399.51 19081.93 1039 668 371 169 0 164 5
cvc5 0 921 66905.67 67029.12 921 544 377 287 0 282 5
OpenSMT 0 892 45637.59 45754.08 892 571 321 316 0 316 0
SMTInterpol 0 594 40514.47 31639.81 594 331 263 614 0 353 0
Z3-alpha-base n 0 1036 50978.99 51115.07 1036 654 382 172 0 172 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 1039
(base +3) 		252103.06 64197.56 1039 668 371 169 0 164 5
Yices2 0 977 30949.40 31074.60 977 642 335 231 0 231 0
cvc5 0 921 66905.67 67029.12 921 544 377 287 0 282 5
OpenSMT 0 892 45637.59 45754.08 892 571 321 316 0 316 0
SMTInterpol 0 594 40514.47 31639.81 594 331 263 614 0 353 0
Z3-alpha-base n 0 1036 50978.99 51115.07 1036 654 382 172 0 172 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
Z3-alpha 0 668
(base +14) 		144769.18 36954.77 668 668 0 59 481 54 5
Yices2 0 642 21714.34 21796.82 642 642 0 85 481 85 0
OpenSMT 0 571 36735.79 36811.38 571 571 0 156 481 156 0
cvc5 0 544 42463.89 42537.22 544 544 0 183 481 178 5
SMTInterpol 0 331 24845.47 21151.41 331 331 0 396 481 242 0
Z3-alpha-base n 0 654 26643.64 26728.86 654 654 0 73 481 73 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
cvc5 0 377 24441.78 24491.91 377 0 377 49 782 49 0
Z3-alpha 0 371
(base -11) 		107333.88 27242.79 371 0 371 55 782 55 0
Yices2 0 335 9235.07 9277.79 335 0 335 91 782 91 0
OpenSMT 0 321 8901.79 8942.70 321 0 321 105 782 105 0
SMTInterpol 0 263 15669.00 10488.40 263 0 263 163 782 95 0
Z3-alpha-base n 0 382 24335.35 24386.20 382 0 382 44 782 44 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 864 1274.14 1381.42 864 564 300 0 344 0 0
Z3-alpha 0 806
(base -14) 		7535.96 2264.46 806 531 275 0 402 0 0
OpenSMT 0 644 2068.53 2148.57 644 371 273 0 564 0 0
cvc5 0 634 2227.57 2305.68 634 343 291 0 574 0 0
SMTInterpol 0 423 4705.07 2186.80 423 227 196 173 612 0 0
Z3-alpha-base n 0 820 2024.01 2125.71 820 528 292 0 388 0 0
(base +/- n): for derived solvers: increment over base solver
n: non-competing solver