The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_SLIA logic in the Single Query Track.
Page generated on 2022-08-10 11:17:45 +0000
Benchmarks: 15143 Time Limit: 1200 seconds Memory Limit: 60 GB
| 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 | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2020-CVC4n | 0 | 14802 | 536682.088 | 557032.73 | 14802 | 10496 | 4306 | 341 | 341 | 0 |
| cvc5 | 0 | 14779 | 551905.049 | 554481.219 | 14779 | 10477 | 4302 | 364 | 363 | 0 |
| z3-4.8.17n | 0 | 14245 | 1244652.211 | 1244293.993 | 14245 | 10115 | 4130 | 898 | 898 | 0 |
| Z3str4 | 0 | 14218 | 975076.776 | 974935.121 | 14218 | 10059 | 4159 | 925 | 740 | 0 |
| OSTRICH | 0 | 8444 | 8198921.279 | 8098488.938 | 8444 | 4760 | 3684 | 6699 | 6567 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2020-CVC4n | 0 | 14802 | 551178.488 | 557008.79 | 14802 | 10496 | 4306 | 341 | 341 | 0 |
| cvc5 | 0 | 14779 | 552974.219 | 554462.879 | 14779 | 10477 | 4302 | 364 | 363 | 0 |
| z3-4.8.17n | 0 | 14245 | 1244836.681 | 1244251.953 | 14245 | 10115 | 4130 | 898 | 898 | 0 |
| Z3str4 | 0 | 14218 | 975196.686 | 974900.201 | 14218 | 10059 | 4159 | 925 | 740 | 0 |
| OSTRICH | 0 | 8447 | 8199024.689 | 8098263.788 | 8447 | 4762 | 3685 | 6696 | 6564 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2020-CVC4n | 0 | 10496 | 218460.218 | 223560.881 | 10496 | 10496 | 0 | 91 | 4556 | 341 | 0 |
| cvc5 | 0 | 10477 | 213818.039 | 214963.419 | 10477 | 10477 | 0 | 110 | 4556 | 363 | 0 |
| z3-4.8.17n | 0 | 10115 | 728174.892 | 727606.964 | 10115 | 10115 | 0 | 472 | 4556 | 898 | 0 |
| Z3str4 | 0 | 10059 | 514720.759 | 514460.986 | 10059 | 10059 | 0 | 528 | 4556 | 740 | 0 |
| OSTRICH | 0 | 4762 | 7207958.115 | 7133085.909 | 4762 | 4762 | 0 | 5825 | 4556 | 6564 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2020-CVC4n | 0 | 4306 | 186318.271 | 187047.91 | 4306 | 0 | 4306 | 128 | 10709 | 341 | 0 |
| cvc5 | 0 | 4302 | 192756.18 | 193099.46 | 4302 | 0 | 4302 | 132 | 10709 | 363 | 0 |
| Z3str4 | 0 | 4159 | 314075.927 | 314039.216 | 4159 | 0 | 4159 | 275 | 10709 | 740 | 0 |
| z3-4.8.17n | 0 | 4130 | 370261.789 | 370244.989 | 4130 | 0 | 4130 | 304 | 10709 | 898 | 0 |
| OSTRICH | 0 | 3685 | 848258.866 | 822373.386 | 3685 | 0 | 3685 | 749 | 10709 | 6564 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 14419 | 27454.047 | 27359.648 | 14419 | 10218 | 4201 | 724 | 723 | 0 |
| 2020-CVC4n | 0 | 14228 | 33640.129 | 33660.517 | 14228 | 10057 | 4171 | 915 | 915 | 0 |
| Z3str4 | 0 | 13564 | 49336.4 | 49196.585 | 13564 | 9433 | 4131 | 1579 | 1579 | 0 |
| z3-4.8.17n | 0 | 13328 | 61569.771 | 61209.048 | 13328 | 9244 | 4084 | 1815 | 1815 | 0 |
| OSTRICH | 0 | 7403 | 255174.238 | 211160.786 | 7403 | 3949 | 3454 | 7740 | 7609 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.