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 2021-07-18 17:29:07 +0000
Benchmarks: 807 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 | 807 | 2253.576 | 2272.851 | 807 | 463 | 344 | 0 | 0 | 0 |
| cvc5 - fixedn | 0 | 806 | 1710.332 | 2625.6 | 806 | 462 | 344 | 1 | 1 | 0 |
| 2020-CVC4n | 0 | 806 | 5675.096 | 5654.206 | 806 | 462 | 344 | 1 | 1 | 0 |
| z3n | 0 | 804 | 3831.824 | 3832.804 | 804 | 460 | 344 | 3 | 3 | 0 |
| Z3str4 | 0 | 799 | 10214.872 | 10213.339 | 799 | 455 | 344 | 8 | 8 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 807 | 2253.576 | 2272.851 | 807 | 463 | 344 | 0 | 0 | 0 |
| cvc5 - fixedn | 0 | 806 | 2610.32 | 2625.51 | 806 | 462 | 344 | 1 | 1 | 0 |
| 2020-CVC4n | 0 | 806 | 5675.206 | 5654.186 | 806 | 462 | 344 | 1 | 1 | 0 |
| z3n | 0 | 804 | 3832.374 | 3832.624 | 804 | 460 | 344 | 3 | 3 | 0 |
| Z3str4 | 0 | 799 | 10217.582 | 10212.849 | 799 | 455 | 344 | 8 | 8 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 463 | 2246.292 | 2265.714 | 463 | 463 | 0 | 0 | 344 | 0 | 0 |
| cvc5 - fixedn | 0 | 462 | 2603.022 | 2618.294 | 462 | 462 | 0 | 1 | 344 | 1 | 0 |
| 2020-CVC4n | 0 | 462 | 5667.955 | 5646.77 | 462 | 462 | 0 | 1 | 344 | 1 | 0 |
| z3n | 0 | 460 | 3821.354 | 3821.57 | 460 | 460 | 0 | 3 | 344 | 3 | 0 |
| Z3str4 | 0 | 455 | 10211.494 | 10206.726 | 455 | 455 | 0 | 8 | 344 | 8 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Z3str4 | 0 | 344 | 6.088 | 6.124 | 344 | 0 | 344 | 0 | 463 | 8 | 0 |
| cvc5 | 0 | 344 | 7.285 | 7.137 | 344 | 0 | 344 | 0 | 463 | 0 | 0 |
| cvc5 - fixedn | 0 | 344 | 7.298 | 7.216 | 344 | 0 | 344 | 0 | 463 | 1 | 0 |
| 2020-CVC4n | 0 | 344 | 7.251 | 7.415 | 344 | 0 | 344 | 0 | 463 | 1 | 0 |
| z3n | 0 | 344 | 11.02 | 11.054 | 344 | 0 | 344 | 0 | 463 | 3 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| z3n | 0 | 802 | 230.722 | 230.847 | 802 | 458 | 344 | 5 | 5 | 0 |
| cvc5 - fixedn | 0 | 797 | 455.749 | 452.489 | 797 | 453 | 344 | 10 | 10 | 0 |
| cvc5 | 0 | 797 | 454.149 | 452.887 | 797 | 453 | 344 | 10 | 10 | 0 |
| Z3str4 | 0 | 797 | 754.067 | 749.326 | 797 | 453 | 344 | 10 | 10 | 0 |
| 2020-CVC4n | 0 | 780 | 1205.45 | 1197.316 | 780 | 436 | 344 | 27 | 27 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.