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 2021-07-18 17:29:07 +0000
Benchmarks: 22985 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 | 22718 | 469507.334 | 472428.312 | 22718 | 14879 | 7839 | 267 | 267 | 0 |
| cvc5 | 0 | 22695 | 465113.711 | 507965.761 | 22695 | 14859 | 7836 | 290 | 289 | 0 |
| cvc5 - fixedn | 0 | 22682 | 466170.667 | 516180.293 | 22682 | 14848 | 7834 | 303 | 302 | 0 |
| z3n | 0 | 22272 | 1069375.484 | 1069024.75 | 22272 | 14597 | 7675 | 713 | 713 | 0 |
| Z3str4 | 117 | 19019 | 4015542.251 | 4016153.988 | 19019 | 11437 | 7582 | 3966 | 3323 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2020-CVC4n | 0 | 22717 | 470904.364 | 472415.102 | 22717 | 14878 | 7839 | 268 | 268 | 0 |
| cvc5 | 0 | 22695 | 506119.113 | 507953.321 | 22695 | 14859 | 7836 | 290 | 289 | 0 |
| cvc5 - fixedn | 0 | 22682 | 514393.684 | 516164.703 | 22682 | 14848 | 7834 | 303 | 302 | 0 |
| z3n | 0 | 22272 | 1069502.414 | 1068992.92 | 22272 | 14597 | 7675 | 713 | 713 | 0 |
| Z3str4 | 117 | 19019 | 4016005.811 | 4016002.088 | 19019 | 11437 | 7582 | 3966 | 3323 | 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 | 14878 | 234172.112 | 235402.471 | 14878 | 14878 | 0 | 94 | 8013 | 268 | 0 |
| cvc5 | 0 | 14859 | 264599.211 | 266006.8 | 14859 | 14859 | 0 | 113 | 8013 | 289 | 0 |
| cvc5 - fixedn | 0 | 14848 | 271100.762 | 272395.687 | 14848 | 14848 | 0 | 124 | 8013 | 302 | 0 |
| z3n | 0 | 14597 | 655941.196 | 655461.66 | 14597 | 14597 | 0 | 375 | 8013 | 713 | 0 |
| Z3str4 | 0 | 11437 | 3733980.405 | 3733976.218 | 11437 | 11437 | 0 | 3535 | 8013 | 3323 | 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 | 7839 | 78332.252 | 78612.631 | 7839 | 0 | 7839 | 42 | 15104 | 268 | 0 |
| cvc5 | 0 | 7836 | 83119.902 | 83546.521 | 7836 | 0 | 7836 | 45 | 15104 | 289 | 0 |
| cvc5 - fixedn | 0 | 7834 | 84892.922 | 85369.016 | 7834 | 0 | 7834 | 47 | 15104 | 302 | 0 |
| z3n | 0 | 7675 | 255161.218 | 255131.26 | 7675 | 0 | 7675 | 206 | 15104 | 713 | 0 |
| Z3str4 | 117 | 7582 | 136750.262 | 136750.725 | 7582 | 0 | 7582 | 299 | 15104 | 3323 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 - fixedn | 0 | 22094 | 34433.704 | 34264.724 | 22094 | 14384 | 7710 | 891 | 890 | 0 |
| cvc5 | 0 | 22093 | 34338.581 | 34237.329 | 22093 | 14383 | 7710 | 892 | 891 | 0 |
| 2020-CVC4n | 0 | 22085 | 33962.23 | 33858.591 | 22085 | 14365 | 7720 | 900 | 900 | 0 |
| z3n | 0 | 21215 | 65246.293 | 64935.396 | 21215 | 13607 | 7608 | 1770 | 1770 | 0 |
| Z3str4 | 117 | 18918 | 86711.046 | 86703.464 | 18918 | 11336 | 7582 | 4067 | 3440 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.