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 2021-07-18 17:31:25 +0000
Benchmarks: 22821 Time Limit: 1200 seconds Memory Limit: 60 GB
Logics:| Sequential Performance | Parallel Performance |
|---|---|
| cvc5-uc | cvc5-uc |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|
| cvc5-uc | 0 | 1407812 | 389756.63 | 389701.433 | 304 | 0 | |
| 2020-CVC4-ucn | 0 | 1407110 | 407622.165 | 407692.789 | 318 | 0 | |
| 2020-z3n | 0 | 1083727 | 400108.203 | 400350.49 | 242 | 14 | |
| z3n | 0 | 1082260 | 401077.391 | 404766.259 | 243 | 4 | |
| SMTInterpol | 0 | 778848 | 2439773.633 | 2422309.371 | 1948 | 0 | |
| SMTInterpol-remus | 0 | 676156 | 4754314.111 | 4513260.972 | 2387 | 0 | |
| UltimateEliminator+MathSAT | 3 | 13528 | 124169.242 | 89179.355 | 25 | 4 | |
| Vampire | 19 | 1092544 | 1782337.947 | 1218637.028 | 832 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|
| cvc5-uc | 0 | 1407812 | 389810.94 | 389688.113 | 304 | 0 | |
| 2020-CVC4-ucn | 0 | 1407110 | 407702.695 | 407678.379 | 318 | 0 | |
| 2020-z3n | 0 | 1083727 | 400434.713 | 400339.28 | 242 | 14 | |
| z3n | 0 | 1082260 | 404263.211 | 404755.489 | 243 | 4 | |
| SMTInterpol | 0 | 780240 | 2480065.723 | 2403021.805 | 1900 | 0 | |
| SMTInterpol-remus | 0 | 773710 | 4859431.461 | 4461611.885 | 1908 | 0 | |
| UltimateEliminator+MathSAT | 3 | 13528 | 124169.242 | 89179.355 | 25 | 4 | |
| Vampire | 19 | 1097086 | 2016231.347 | 1019077.325 | 541 | 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.