SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_Equality_NonLinearArith (Single Query Track)

Competition results for the QF_Equality_NonLinearArith division in the Single Query Track. Chart

Results were generated on 2025-08-11

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

Logics:

Winners

Sequential Performance Parallel Performance SAT Performance (parallel) UNSAT Performance (parallel) 24 seconds Performance (parallel)
Yices2 Yices2 Yices2 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 450 15859.71 15917.97 450 376 74 101 80 99 2
cvc5 0 381 28356.84 28407.67 381 296 85 250 0 250 0
SMTInterpol 0 306 25908.44 22972.61 306 240 66 325 0 104 0

Parallel Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
Yices2 0 450 15859.71 15917.97 450 376 74 101 80 99 2
cvc5 0 381 28356.84 28407.67 381 296 85 250 0 250 0
SMTInterpol 0 306 25908.44 22972.61 306 240 66 325 0 104 0

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 376 13511.12 13559.88 376 376 0 12 243 10 2
cvc5 0 296 24928.26 24968.09 296 296 0 121 214 121 0
SMTInterpol 0 240 21723.91 19438.14 240 240 0 177 214 41 0

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 85 3428.58 3439.58 85 0 85 37 509 37 0
Yices2 0 74 2348.59 2358.09 74 0 74 34 523 34 0
SMTInterpol 0 66 4184.53 3534.47 66 0 66 56 509 17 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
Yices2 0 356 796.24 840.58 356 288 68 0 275 0 0
cvc5 0 285 783.27 818.52 285 212 73 0 346 0 0
SMTInterpol 0 212 1006.77 462.76 212 164 48 172 247 0 0