The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_LIA logic in the Unsat Core Track.
Page generated on 2021-07-18 17:31:25 +0000
Benchmarks: 276 Time Limit: 1200 seconds Memory Limit: 60 GB
Sequential Performance | Parallel Performance |
---|---|
Yices2 | Yices2 |
Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Timeout | Memout |
---|---|---|---|---|---|---|
Yices2 | 0 | 945405 | 33114.227 | 33121.372 | 24 | 0 |
2020-Yices2-fixedn | 0 | 945405 | 33125.446 | 33121.74 | 24 | 0 |
z3n | 0 | 944017 | 70716.3 | 70724.838 | 57 | 0 |
cvc5-uc | 0 | 924885 | 107676.567 | 107664.412 | 83 | 0 |
MathSAT5n | 0 | 924346 | 106928.191 | 106947.388 | 89 | 0 |
SMTInterpol | 0 | 811034 | 35403.421 | 34340.353 | 22 | 0 |
SMTInterpol-remus | 0 | 199339 | 149349.515 | 143924.708 | 35 | 0 |
Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Timeout | Memout |
---|---|---|---|---|---|---|
Yices2 | 0 | 945405 | 33118.777 | 33120.202 | 24 | 0 |
2020-Yices2-fixedn | 0 | 945405 | 33133.376 | 33120.72 | 24 | 0 |
z3n | 0 | 944017 | 70722.82 | 70723.088 | 57 | 0 |
cvc5-uc | 0 | 924885 | 107686.147 | 107661.332 | 83 | 0 |
MathSAT5n | 0 | 924346 | 106943.181 | 106943.228 | 89 | 0 |
SMTInterpol | 0 | 811034 | 35403.421 | 34340.353 | 22 | 0 |
SMTInterpol-remus | 0 | 277415 | 149370.985 | 143865.128 | 33 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.