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 2023-07-06 16:05:43 +0000
Benchmarks: 384 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 | 266 | 428.109 | 428.007 | 20 | 0 | |
2022-cvc5n | 0 | 251 | 115.389 | 115.371 | 19 | 0 | |
SMTInterpol | 0 | 0 | 114.964 | 78.283 | 18 | 0 | |
Vampire | 0 | 0 | 5213.591 | 1331.848 | 82 | 0 | |
UltimateEliminator+MathSAT | 50 | 131 | 3363.604 | 2226.692 | 19 | 0 |
Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Abstained | Timeout | Memout |
---|---|---|---|---|---|---|---|
cvc5 | 0 | 266 | 428.109 | 428.007 | 20 | 0 | |
2022-cvc5n | 0 | 251 | 115.389 | 115.371 | 19 | 0 | |
SMTInterpol | 0 | 0 | 114.964 | 78.283 | 18 | 0 | |
Vampire | 0 | 0 | 15177.211 | 3840.136 | 76 | 0 | |
UltimateEliminator+MathSAT | 50 | 131 | 3363.604 | 2226.692 | 19 | 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.