The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_UF division in the Single Query Track.
Page generated on 2019-07-23 17:56:09 +0000
Benchmarks: 3512 Time Limit: 2400 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| Yices 2.6.2 | Par4 | Yices 2.6.2 | Par4 | Par4 |
| 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 | 3512 | 417.659 | 422.382 | 3512 | 1452 | 2060 | 0 | 0 | 0 | |
| 2018-Yicesn | 0 | 3512 | 444.924 | 446.419 | 3512 | 1452 | 2060 | 0 | 0 | 0 | |
| Par4 | 0 | 3512 | 478.936 | 380.621 | 3512 | 1452 | 2060 | 0 | 0 | 0 | |
| veriT | 0 | 3512 | 1519.372 | 1517.538 | 3512 | 1452 | 2060 | 0 | 0 | 0 | |
| CVC4 | 0 | 3510 | 15684.755 | 15682.539 | 3510 | 1452 | 2058 | 2 | 2 | 0 | |
| OpenSMT2 | 0 | 3510 | 17079.175 | 17063.675 | 3510 | 1451 | 2059 | 2 | 2 | 0 | |
| Z3n | 0 | 3476 | 93821.293 | 93797.963 | 3476 | 1452 | 2024 | 36 | 36 | 0 | |
| SMTInterpol | 0 | 3474 | 116925.145 | 109649.844 | 3474 | 1452 | 2022 | 38 | 38 | 0 | |
| Alt-Ergo | 0 | 1606 | 2531524.051 | 1973594.705 | 1606 | 0 | 1606 | 1906 | 667 | 21 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 3512 | 478.936 | 380.621 | 3512 | 1452 | 2060 | 0 | 0 | 0 | |
| Yices 2.6.2 | 0 | 3512 | 417.659 | 422.382 | 3512 | 1452 | 2060 | 0 | 0 | 0 | |
| 2018-Yicesn | 0 | 3512 | 444.924 | 446.419 | 3512 | 1452 | 2060 | 0 | 0 | 0 | |
| veriT | 0 | 3512 | 1519.372 | 1517.538 | 3512 | 1452 | 2060 | 0 | 0 | 0 | |
| CVC4 | 0 | 3510 | 15685.195 | 15682.429 | 3510 | 1452 | 2058 | 2 | 2 | 0 | |
| OpenSMT2 | 0 | 3510 | 17079.705 | 17063.535 | 3510 | 1451 | 2059 | 2 | 2 | 0 | |
| Z3n | 0 | 3476 | 93829.333 | 93796.383 | 3476 | 1452 | 2024 | 36 | 36 | 0 | |
| SMTInterpol | 0 | 3474 | 116925.145 | 109649.844 | 3474 | 1452 | 2022 | 38 | 38 | 0 | |
| Alt-Ergo | 0 | 1883 | 3259319.061 | 1638425.685 | 1883 | 0 | 1883 | 1629 | 371 | 21 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Yices 2.6.2 | 0 | 1452 | 51.502 | 53.823 | 1452 | 1452 | 0 | 2060 | 0 | 0 |
| 2018-Yicesn | 0 | 1452 | 53.633 | 54.355 | 1452 | 1452 | 0 | 2060 | 0 | 0 |
| Par4 | 0 | 1452 | 24.354 | 59.967 | 1452 | 1452 | 0 | 2060 | 0 | 0 |
| veriT | 0 | 1452 | 148.176 | 148.054 | 1452 | 1452 | 0 | 2060 | 0 | 0 |
| Z3n | 0 | 1452 | 319.131 | 319.217 | 1452 | 1452 | 0 | 2060 | 36 | 0 |
| SMTInterpol | 0 | 1452 | 3215.728 | 1323.107 | 1452 | 1452 | 0 | 2060 | 38 | 0 |
| CVC4 | 0 | 1452 | 1387.755 | 1387.829 | 1452 | 1452 | 0 | 2060 | 2 | 0 |
| OpenSMT2 | 0 | 1451 | 5884.11 | 5884.949 | 1451 | 1451 | 0 | 2061 | 2 | 0 |
| Alt-Ergo | 0 | 0 | 943721.256 | 737444.437 | 0 | 0 | 0 | 3512 | 371 | 21 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 2060 | 454.582 | 320.654 | 2060 | 0 | 2060 | 1452 | 0 | 0 |
| Yices 2.6.2 | 0 | 2060 | 366.157 | 368.56 | 2060 | 0 | 2060 | 1452 | 0 | 0 |
| 2018-Yicesn | 0 | 2060 | 391.292 | 392.064 | 2060 | 0 | 2060 | 1452 | 0 | 0 |
| veriT | 0 | 2060 | 1371.196 | 1369.485 | 2060 | 0 | 2060 | 1452 | 0 | 0 |
| OpenSMT2 | 0 | 2059 | 11195.595 | 11178.587 | 2059 | 0 | 2059 | 1453 | 2 | 0 |
| CVC4 | 0 | 2058 | 14297.439 | 14294.6 | 2058 | 0 | 2058 | 1454 | 2 | 0 |
| Z3n | 0 | 2024 | 93510.202 | 93477.166 | 2024 | 0 | 2024 | 1488 | 36 | 0 |
| SMTInterpol | 0 | 2022 | 113709.417 | 108326.737 | 2022 | 0 | 2022 | 1490 | 38 | 0 |
| Alt-Ergo | 0 | 1883 | 2315597.805 | 900981.247 | 1883 | 0 | 1883 | 1629 | 371 | 21 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 3510 | 348.876 | 339.452 | 3510 | 1452 | 2058 | 2 | 2 | 0 | |
| Yices 2.6.2 | 0 | 3509 | 355.218 | 359.935 | 3509 | 1452 | 2057 | 3 | 3 | 0 | |
| 2018-Yicesn | 0 | 3509 | 371.652 | 373.132 | 3509 | 1452 | 2057 | 3 | 3 | 0 | |
| veriT | 0 | 3508 | 491.257 | 489.321 | 3508 | 1452 | 2056 | 4 | 4 | 0 | |
| OpenSMT2 | 0 | 3457 | 3591.845 | 3574.987 | 3457 | 1441 | 2016 | 55 | 55 | 0 | |
| CVC4 | 0 | 3455 | 3253.438 | 3249.493 | 3455 | 1446 | 2009 | 57 | 57 | 0 | |
| Z3n | 0 | 3428 | 3454.353 | 3450.486 | 3428 | 1448 | 1980 | 84 | 84 | 0 | |
| SMTInterpol | 0 | 3412 | 13490.059 | 6898.352 | 3412 | 1451 | 1961 | 100 | 100 | 0 | |
| Alt-Ergo | 0 | 959 | 93869.855 | 66814.792 | 959 | 0 | 959 | 2553 | 2311 | 21 |
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.