The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_Strings division in the Single Query Track.
Page generated on 2022-08-10 11:17:45 +0000
Benchmarks: 15758 Time Limit: 1200 seconds Memory Limit: 60 GB
Logics:| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| cvc5 | cvc5 | cvc5 | cvc5 | cvc5 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 15394 | 553312.043 | 555916.207 | 15394 | 10920 | 4474 | 364 | 0 | 363 | 0 |
| 2020-CVC4n | 0 | 15345 | 543081.023 | 563470.172 | 15345 | 10867 | 4478 | 343 | 70 | 343 | 0 |
| z3-4.8.17n | 0 | 14855 | 1250806.284 | 1250448.355 | 14855 | 10553 | 4302 | 903 | 0 | 903 | 0 |
| Z3str4 | 0 | 14762 | 976628.118 | 976486.921 | 14762 | 10431 | 4331 | 926 | 70 | 741 | 0 |
| OSTRICH | 0 | 9054 | 8210412.544 | 8107150.502 | 9054 | 5198 | 3856 | 6704 | 0 | 6572 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 15394 | 554381.213 | 555897.867 | 15394 | 10920 | 4474 | 364 | 0 | 363 | 0 |
| 2020-CVC4n | 0 | 15345 | 557578.083 | 563446.112 | 15345 | 10867 | 4478 | 343 | 70 | 343 | 0 |
| z3-4.8.17n | 0 | 14855 | 1250991.914 | 1250406.185 | 14855 | 10553 | 4302 | 903 | 0 | 903 | 0 |
| Z3str4 | 0 | 14762 | 976748.268 | 976451.911 | 14762 | 10431 | 4331 | 926 | 70 | 741 | 0 |
| OSTRICH | 0 | 9057 | 8210515.954 | 8106925.352 | 9057 | 5200 | 3857 | 6701 | 0 | 6569 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 10920 | 215221.383 | 216394.806 | 10920 | 10920 | 0 | 110 | 4728 | 363 | 0 |
| 2020-CVC4n | 0 | 10867 | 224845.013 | 229982.682 | 10867 | 10867 | 0 | 93 | 4798 | 343 | 0 |
| z3-4.8.17n | 0 | 10553 | 734323.735 | 733755.095 | 10553 | 10553 | 0 | 477 | 4728 | 903 | 0 |
| Z3str4 | 0 | 10431 | 516269.168 | 516009.46 | 10431 | 10431 | 0 | 529 | 4798 | 741 | 0 |
| OSTRICH | 0 | 5200 | 7219037.703 | 7141502.888 | 5200 | 5200 | 0 | 5830 | 4728 | 6569 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2020-CVC4n | 0 | 4478 | 186333.07 | 187063.43 | 4478 | 0 | 4478 | 128 | 11152 | 343 | 0 |
| cvc5 | 0 | 4474 | 192759.831 | 193103.061 | 4474 | 0 | 4474 | 132 | 11152 | 363 | 0 |
| Z3str4 | 0 | 4331 | 314079.101 | 314042.451 | 4331 | 0 | 4331 | 275 | 11152 | 741 | 0 |
| z3-4.8.17n | 0 | 4302 | 370268.178 | 370251.09 | 4302 | 0 | 4302 | 304 | 11152 | 903 | 0 |
| OSTRICH | 0 | 3857 | 848670.544 | 822617.97 | 3857 | 0 | 3857 | 749 | 11152 | 6569 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 15029 | 27757.707 | 27663.218 | 15029 | 10656 | 4373 | 729 | 0 | 728 | 0 |
| 2020-CVC4n | 0 | 14744 | 34869.672 | 34890.118 | 14744 | 10401 | 4343 | 944 | 70 | 944 | 0 |
| Z3str4 | 0 | 14103 | 49696.631 | 49556.927 | 14103 | 9800 | 4303 | 1585 | 70 | 1585 | 0 |
| z3-4.8.17n | 0 | 13937 | 61793.767 | 61432.022 | 13937 | 9681 | 4256 | 1821 | 0 | 1821 | 0 |
| OSTRICH | 0 | 8002 | 259308.463 | 213133.032 | 8002 | 4376 | 3626 | 7756 | 0 | 7625 | 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.