The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the Equality+LinearArith division in the Unsat Core Track.
Page generated on 2022-08-10 11:18:51 +0000
Benchmarks: 23260 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 |
|---|---|---|---|---|---|---|---|
| 2021-cvc5-ucn | 0 | 1480936 | 693308.268 | 710216.866 | 565 | 0 | |
| z3-4.8.17n | 0 | 1428341 | 682739.844 | 683765.021 | 470 | 6 | |
| cvc5 | 0 | 1336111 | 724827.294 | 724898.504 | 573 | 0 | |
| Vampire | 0 | 1181277 | 1722492.476 | 1127469.606 | 770 | 0 | |
| smtinterpol | 0 | 1093221 | 3190115.934 | 3148844.307 | 2529 | 0 | |
| UltimateEliminator+MathSAT | 3 | 9052 | 131035.894 | 83912.049 | 8 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|
| 2021-cvc5-ucn | 0 | 1480936 | 708944.388 | 710186.816 | 565 | 0 | |
| z3-4.8.17n | 0 | 1428341 | 682861.574 | 683742.951 | 470 | 6 | |
| cvc5 | 0 | 1336111 | 724964.054 | 724872.634 | 573 | 0 | |
| Vampire | 0 | 1193299 | 2059716.786 | 963128.245 | 518 | 0 | |
| smtinterpol | 0 | 1093993 | 3231786.834 | 3135362.76 | 2493 | 0 | |
| UltimateEliminator+MathSAT | 3 | 9052 | 131035.894 | 83912.049 | 8 | 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.