The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_S logic in the Single Query Track.
Page generated on 2022-08-10 11:17:45 +0000
Benchmarks: 545 Time Limit: 1200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| cvc5 | cvc5 | cvc5 | Z3str4 | cvc5 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 545 | 1404.937 | 1432.963 | 545 | 373 | 172 | 0 | 0 | 0 |
| Z3str4 | 0 | 544 | 1551.343 | 1551.799 | 544 | 372 | 172 | 1 | 1 | 0 |
| 2020-CVC4n | 0 | 543 | 6398.935 | 6437.442 | 543 | 371 | 172 | 2 | 2 | 0 |
| z3-4.8.17n | 0 | 540 | 6151.397 | 6151.817 | 540 | 368 | 172 | 5 | 5 | 0 |
| OSTRICH | 0 | 540 | 11299.845 | 8552.056 | 540 | 368 | 172 | 5 | 5 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 545 | 1404.937 | 1432.963 | 545 | 373 | 172 | 0 | 0 | 0 |
| Z3str4 | 0 | 544 | 1551.583 | 1551.709 | 544 | 372 | 172 | 1 | 1 | 0 |
| 2020-CVC4n | 0 | 543 | 6399.595 | 6437.322 | 543 | 371 | 172 | 2 | 2 | 0 |
| z3-4.8.17n | 0 | 540 | 6152.557 | 6151.687 | 540 | 368 | 172 | 5 | 5 | 0 |
| OSTRICH | 0 | 540 | 11299.845 | 8552.056 | 540 | 368 | 172 | 5 | 5 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 373 | 1401.286 | 1429.362 | 373 | 373 | 0 | 0 | 172 | 0 | 0 |
| Z3str4 | 0 | 372 | 1548.409 | 1548.474 | 372 | 372 | 0 | 1 | 172 | 1 | 0 |
| 2020-CVC4n | 0 | 371 | 6384.795 | 6421.802 | 371 | 371 | 0 | 2 | 172 | 2 | 0 |
| z3-4.8.17n | 0 | 368 | 6146.168 | 6145.586 | 368 | 368 | 0 | 5 | 172 | 5 | 0 |
| OSTRICH | 0 | 368 | 10888.167 | 8307.472 | 368 | 368 | 0 | 5 | 172 | 5 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Z3str4 | 0 | 172 | 3.174 | 3.235 | 172 | 0 | 172 | 0 | 373 | 1 | 0 |
| cvc5 | 0 | 172 | 3.651 | 3.601 | 172 | 0 | 172 | 0 | 373 | 0 | 0 |
| z3-4.8.17n | 0 | 172 | 6.389 | 6.1 | 172 | 0 | 172 | 0 | 373 | 5 | 0 |
| 2020-CVC4n | 0 | 172 | 14.799 | 15.52 | 172 | 0 | 172 | 0 | 373 | 2 | 0 |
| OSTRICH | 0 | 172 | 411.677 | 244.584 | 172 | 0 | 172 | 0 | 373 | 5 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 540 | 301.602 | 301.546 | 540 | 368 | 172 | 5 | 5 | 0 |
| z3-4.8.17n | 0 | 539 | 221.319 | 220.429 | 539 | 367 | 172 | 6 | 6 | 0 |
| Z3str4 | 0 | 539 | 360.232 | 360.342 | 539 | 367 | 172 | 6 | 6 | 0 |
| OSTRICH | 0 | 529 | 3942.805 | 1862.739 | 529 | 357 | 172 | 16 | 16 | 0 |
| 2020-CVC4n | 0 | 516 | 1229.543 | 1229.602 | 516 | 344 | 172 | 29 | 29 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.