The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_AUFBV division in the Challenge Track (non-incremental).
Page generated on 2019-07-23 17:57:29 +0000
Benchmarks: 15 Time Limit: 43200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| Yices 2.6.2 | Yices 2.6.2 | Yices 2.6.2 | Poolector | Yices 2.6.2 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Yices 2.6.2 | 0 | 10 | 226776.086 | 226787.281 | 10 | 9 | 1 | 5 | 5 | 0 | |
| Z3n | 0 | 8 | 259238.116 | 259268.178 | 8 | 7 | 1 | 7 | 5 | 0 | |
| Boolector | 0 | 5 | 173174.008 | 173186.179 | 5 | 4 | 1 | 10 | 4 | 0 | |
| Poolector | 0 | 4 | 216680.247 | 216173.112 | 4 | 3 | 1 | 11 | 4 | 1 | |
| 2018-CVC4n | 0 | 3 | 239216.642 | 240991.473 | 3 | 2 | 1 | 12 | 4 | 0 | |
| CVC4 | 0 | 3 | 354363.865 | 356633.43 | 3 | 2 | 1 | 12 | 7 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Yices 2.6.2 | 0 | 10 | 226782.286 | 226787.081 | 10 | 9 | 1 | 5 | 5 | 0 | |
| Z3n | 0 | 8 | 259256.016 | 259267.978 | 8 | 7 | 1 | 7 | 5 | 0 | |
| Boolector | 0 | 5 | 173182.008 | 173185.979 | 5 | 4 | 1 | 10 | 4 | 0 | |
| Poolector | 0 | 4 | 216680.247 | 216173.112 | 4 | 3 | 1 | 11 | 4 | 1 | |
| 2018-CVC4n | 0 | 3 | 239236.442 | 240991.273 | 3 | 2 | 1 | 12 | 4 | 0 | |
| CVC4 | 0 | 3 | 354389.765 | 356633.23 | 3 | 2 | 1 | 12 | 7 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Yices 2.6.2 | 0 | 9 | 53963.205 | 53969.5 | 9 | 9 | 0 | 6 | 5 | 0 |
| Z3n | 0 | 7 | 124712.244 | 124716.154 | 7 | 7 | 0 | 8 | 5 | 0 |
| Boolector | 0 | 4 | 351.731 | 351.797 | 4 | 4 | 0 | 11 | 4 | 0 |
| Poolector | 0 | 3 | 43820.627 | 43357.957 | 3 | 3 | 0 | 12 | 4 | 1 |
| 2018-CVC4n | 0 | 2 | 209777.33 | 210433.897 | 2 | 2 | 0 | 13 | 4 | 0 |
| CVC4 | 0 | 2 | 316357.17 | 317437.836 | 2 | 2 | 0 | 13 | 7 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Poolector | 0 | 1 | 59.62 | 15.156 | 1 | 0 | 1 | 14 | 4 | 1 |
| Yices 2.6.2 | 0 | 1 | 17.582 | 17.581 | 1 | 0 | 1 | 14 | 5 | 0 |
| 2018-CVC4n | 0 | 1 | 18.142 | 18.146 | 1 | 0 | 1 | 14 | 4 | 0 |
| CVC4 | 0 | 1 | 18.645 | 18.644 | 1 | 0 | 1 | 14 | 7 | 0 |
| Z3n | 0 | 1 | 19.292 | 19.293 | 1 | 0 | 1 | 14 | 5 | 0 |
| Boolector | 0 | 1 | 34.177 | 34.182 | 1 | 0 | 1 | 14 | 4 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Yices 2.6.2 | 0 | 3 | 305.966 | 305.966 | 3 | 2 | 1 | 12 | 12 | 0 | |
| Poolector | 0 | 2 | 229.367 | 184.573 | 2 | 1 | 1 | 13 | 6 | 1 | |
| Z3n | 0 | 2 | 331.916 | 331.918 | 2 | 1 | 1 | 13 | 13 | 0 | |
| Boolector | 0 | 1 | 192.31 | 192.31 | 1 | 1 | 0 | 14 | 8 | 0 | |
| 2018-CVC4n | 0 | 1 | 354.142 | 354.146 | 1 | 0 | 1 | 14 | 14 | 0 | |
| CVC4 | 0 | 1 | 354.645 | 354.644 | 1 | 0 | 1 | 14 | 14 | 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.