The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the Arith division in the Unsat Core Track.
Page generated on 2022-08-10 11:18:51 +0000
Benchmarks: 359 Time Limit: 1200 seconds Memory Limit: 60 GB
Logics:Sequential Performance | Parallel Performance |
---|---|
cvc5 | cvc5 |
Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Abstained | Timeout | Memout |
---|---|---|---|---|---|---|---|
cvc5 | 0 | 262 | 26012.503 | 26013.088 | 20 | 0 | |
2020-CVC4-ucn | 0 | 220 | 29112.195 | 29120.673 | 24 | 0 | |
z3-4.8.17n | 0 | 69 | 39747.315 | 39743.913 | 30 | 0 | |
Vampire | 0 | 10 | 110646.86 | 104211.832 | 85 | 0 | |
smtinterpol | 0 | 0 | 30097.043 | 29781.401 | 22 | 0 | |
UltimateEliminator+MathSAT | 21 | 196 | 28412.932 | 27355.275 | 21 | 0 |
Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Abstained | Timeout | Memout |
---|---|---|---|---|---|---|---|
cvc5 | 0 | 262 | 26016.743 | 26012.038 | 20 | 0 | |
2020-CVC4-ucn | 0 | 220 | 29119.205 | 29119.173 | 24 | 0 | |
z3-4.8.17n | 0 | 69 | 39752.455 | 39742.573 | 30 | 0 | |
Vampire | 0 | 10 | 121339.11 | 101490.779 | 81 | 0 | |
smtinterpol | 0 | 0 | 30097.043 | 29781.401 | 22 | 0 | |
UltimateEliminator+MathSAT | 21 | 196 | 28412.932 | 27355.275 | 21 | 0 |
n Non-competing.
Abstained: Total of benchmarks in logics in this division that solver chose to abstain from. For SAT/UNSAT scores, this column also includes benchmarks not known to be SAT/UNSAT.