SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_NonLinearIntArith (Model Validation Track)

Competition results for the QF_NonLinearIntArith division in the Model Validation Track. Chart

Results were generated on 2025-08-11

Benchmarks: 7516
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 - Yices2

Sequential Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
Yices2 0 6673 43422.54 44254.28 6673 6673 843 0 838 0
cvc5 0 6221 1570875.68 1571841.93 6221 6221 1295 0 1142 148
SMTInterpol 0 1 225.75 197.92 1 1 7515 0 2 0

Parallel Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
Yices2 0 6673 43422.54 44254.28 6673 6673 843 0 838 0
cvc5 0 6221 1570875.68 1571841.93 6221 6221 1295 0 1142 148
SMTInterpol 0 1 225.75 197.92 1 1 7515 0 2 0

SAT Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
Yices2 0 6673 43422.54 44254.28 6673 6673 843 0 838 0
cvc5 0 6221 1570875.68 1571841.93 6221 6221 1295 0 1142 148
SMTInterpol 0 1 225.75 197.92 1 1 7515 0 2 0

24 seconds Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
Yices2 0 6385 14022.22 14813.49 6385 6385 5 1126 0 0
cvc5 0 2940 7900.50 8259.25 2940 2940 5 4571 0 0
SMTInterpol 0 0 0.00 0.00 0 0 7471 45 0 0