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 2021-07-18 17:29:07 +0000
Benchmarks: 23797 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 |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2020-CVC4n | 0 | 23524 | 475182.43 | 478082.517 | 23524 | 15341 | 8183 | 268 | 5 | 268 | 0 |
| cvc5 | 0 | 23507 | 467367.414 | 510238.737 | 23507 | 15327 | 8180 | 290 | 0 | 289 | 0 |
| cvc5 - fixedn | 0 | 23493 | 467881.125 | 518806.017 | 23493 | 15315 | 8178 | 304 | 0 | 303 | 0 |
| z3n | 0 | 23076 | 1073207.308 | 1072857.554 | 23076 | 15057 | 8019 | 716 | 5 | 716 | 0 |
| Z3str4 | 117 | 19818 | 4025757.226 | 4026367.432 | 19818 | 11892 | 7926 | 3979 | 0 | 3331 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2020-CVC4n | 0 | 23523 | 476579.57 | 478069.287 | 23523 | 15340 | 8183 | 269 | 5 | 269 | 0 |
| cvc5 | 0 | 23507 | 508372.816 | 510226.297 | 23507 | 15327 | 8180 | 290 | 0 | 289 | 0 |
| cvc5 - fixedn | 0 | 23493 | 517004.13 | 518790.337 | 23493 | 15315 | 8178 | 304 | 0 | 303 | 0 |
| z3n | 0 | 23076 | 1073334.788 | 1072825.544 | 23076 | 15057 | 8019 | 716 | 5 | 716 | 0 |
| Z3str4 | 117 | 19818 | 4026223.496 | 4026215.042 | 19818 | 11892 | 7926 | 3979 | 0 | 3331 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2020-CVC4n | 0 | 15340 | 239840.067 | 241049.241 | 15340 | 15340 | 0 | 95 | 8362 | 269 | 0 |
| cvc5 | 0 | 15327 | 266845.63 | 268272.639 | 15327 | 15327 | 0 | 113 | 8357 | 289 | 0 |
| cvc5 - fixedn | 0 | 15315 | 273703.911 | 275014.105 | 15315 | 15315 | 0 | 125 | 8357 | 303 | 0 |
| z3n | 0 | 15057 | 659762.55 | 659283.231 | 15057 | 15057 | 0 | 378 | 8362 | 716 | 0 |
| Z3str4 | 0 | 11892 | 3744192.001 | 3744183.047 | 11892 | 11892 | 0 | 3548 | 8357 | 3331 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2020-CVC4n | 0 | 8183 | 78339.503 | 78620.046 | 8183 | 0 | 8183 | 42 | 15572 | 269 | 0 |
| cvc5 | 0 | 8180 | 83127.186 | 83553.658 | 8180 | 0 | 8180 | 45 | 15572 | 289 | 0 |
| cvc5 - fixedn | 0 | 8178 | 84900.22 | 85376.232 | 8178 | 0 | 8178 | 47 | 15572 | 303 | 0 |
| z3n | 0 | 8019 | 255172.238 | 255142.313 | 8019 | 0 | 8019 | 206 | 15572 | 716 | 0 |
| Z3str4 | 117 | 7926 | 136756.35 | 136756.849 | 7926 | 0 | 7926 | 299 | 15572 | 3331 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 - fixedn | 0 | 22896 | 34889.579 | 34717.337 | 22896 | 14842 | 8054 | 901 | 0 | 900 | 0 |
| cvc5 | 0 | 22895 | 34792.857 | 34690.341 | 22895 | 14841 | 8054 | 902 | 0 | 901 | 0 |
| 2020-CVC4n | 0 | 22865 | 35167.68 | 35055.908 | 22865 | 14801 | 8064 | 927 | 5 | 927 | 0 |
| z3n | 0 | 22017 | 65477.015 | 65166.243 | 22017 | 14065 | 7952 | 1775 | 5 | 1775 | 0 |
| Z3str4 | 117 | 19715 | 87465.216 | 87452.894 | 19715 | 11789 | 7926 | 4082 | 0 | 3450 | 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.