The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_SLIA division in the Single Query Track.
Page generated on 2019-07-23 17:57:14 +0000
Benchmarks: 23175 Time Limit: 2400 seconds Memory Limit: 60 GB
This division is experimental. Solvers are only ranked by performance, but no winner is selected.
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| CVC4 | 0 | 23102 | 431446.836 | 433519.411 | 23102 | 18624 | 4478 | 73 | 73 | 0 | |
| 2018-CVC4n | 0 | 22641 | 1484330.321 | 1485372.228 | 22641 | 18181 | 4460 | 534 | 533 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| CVC4 | 0 | 23102 | 431823.756 | 433516.171 | 23102 | 18624 | 4478 | 73 | 73 | 0 | |
| 2018-CVC4n | 0 | 22641 | 1485225.351 | 1485348.298 | 22641 | 18181 | 4460 | 534 | 533 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| CVC4 | 0 | 18624 | 236998.87 | 238376.285 | 18624 | 18624 | 0 | 4551 | 73 | 0 |
| 2018-CVC4n | 0 | 18181 | 1264224.602 | 1264345.076 | 18181 | 18181 | 0 | 4994 | 533 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| CVC4 | 0 | 4478 | 34024.887 | 34339.886 | 4478 | 0 | 4478 | 18697 | 73 | 0 |
| 2018-CVC4n | 0 | 4460 | 60200.749 | 60203.223 | 4460 | 0 | 4460 | 18715 | 533 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| CVC4 | 0 | 22463 | 25644.82 | 25572.808 | 22463 | 18045 | 4418 | 712 | 712 | 0 | |
| 2018-CVC4n | 0 | 22145 | 37021.923 | 36927.919 | 22145 | 17705 | 4440 | 1030 | 1030 | 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.