The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_UFLRA division in the Single Query Track.
Page generated on 2020-07-04 11:46:59 +0000
Benchmarks: 432 Time Limit: 1200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| Yices2 | Yices2 | Yices2 | Yices2 | Yices2 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-SMTInterpoln | 0 | 431 | 3979.857 | 2865.784 | 431 | 250 | 181 | 1 | 1 | 0 | |
| Yices2 | 0 | 430 | 2435.753 | 2436.894 | 430 | 249 | 181 | 2 | 2 | 0 | |
| Yices2-fixedn | 0 | 430 | 2435.76 | 2437.429 | 430 | 249 | 181 | 2 | 2 | 0 | |
| veriT | 0 | 430 | 2475.953 | 2476.367 | 430 | 249 | 181 | 2 | 2 | 0 | |
| MathSAT5n | 0 | 430 | 2511.952 | 2512.67 | 430 | 249 | 181 | 2 | 2 | 0 | |
| CVC4 | 0 | 430 | 2994.438 | 2995.111 | 430 | 249 | 181 | 2 | 2 | 0 | |
| SMTInterpol | 0 | 430 | 4241.553 | 3214.897 | 430 | 249 | 181 | 2 | 2 | 0 | |
| SMTInterpol-fixedn | 0 | 430 | 4266.487 | 3218.192 | 430 | 249 | 181 | 2 | 2 | 0 | |
| z3n | 0 | 412 | 24281.095 | 24283.533 | 412 | 231 | 181 | 20 | 20 | 0 | |
| Alt-Ergo | 0 | 170 | 138940.3 | 74346.897 | 170 | 0 | 170 | 262 | 32 | 8 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-SMTInterpoln | 0 | 431 | 3979.857 | 2865.784 | 431 | 250 | 181 | 1 | 1 | 0 | |
| Yices2 | 0 | 430 | 2435.923 | 2436.764 | 430 | 249 | 181 | 2 | 2 | 0 | |
| Yices2-fixedn | 0 | 430 | 2435.93 | 2437.329 | 430 | 249 | 181 | 2 | 2 | 0 | |
| veriT | 0 | 430 | 2476.263 | 2476.297 | 430 | 249 | 181 | 2 | 2 | 0 | |
| MathSAT5n | 0 | 430 | 2512.562 | 2512.62 | 430 | 249 | 181 | 2 | 2 | 0 | |
| CVC4 | 0 | 430 | 2995.068 | 2994.991 | 430 | 249 | 181 | 2 | 2 | 0 | |
| SMTInterpol | 0 | 430 | 4241.553 | 3214.897 | 430 | 249 | 181 | 2 | 2 | 0 | |
| SMTInterpol-fixedn | 0 | 430 | 4266.487 | 3218.192 | 430 | 249 | 181 | 2 | 2 | 0 | |
| z3n | 0 | 412 | 24282.585 | 24282.653 | 412 | 231 | 181 | 20 | 20 | 0 | |
| Alt-Ergo | 0 | 172 | 150111.79 | 65655.268 | 172 | 0 | 172 | 260 | 19 | 8 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-SMTInterpoln | 0 | 250 | 2064.865 | 1399.948 | 250 | 250 | 0 | 182 | 1 | 0 |
| Yices2 | 0 | 249 | 1229.894 | 1230.338 | 249 | 249 | 0 | 183 | 2 | 0 |
| Yices2-fixedn | 0 | 249 | 1229.898 | 1230.671 | 249 | 249 | 0 | 183 | 2 | 0 |
| veriT | 0 | 249 | 1268.023 | 1268.073 | 249 | 249 | 0 | 183 | 2 | 0 |
| MathSAT5n | 0 | 249 | 1301.549 | 1301.587 | 249 | 249 | 0 | 183 | 2 | 0 |
| CVC4 | 0 | 249 | 1759.028 | 1759.005 | 249 | 249 | 0 | 183 | 2 | 0 |
| SMTInterpol | 0 | 249 | 2363.334 | 1764.03 | 249 | 249 | 0 | 183 | 2 | 0 |
| SMTInterpol-fixedn | 0 | 249 | 2370.627 | 1764.507 | 249 | 249 | 0 | 183 | 2 | 0 |
| z3n | 0 | 231 | 23043.083 | 23043.132 | 231 | 231 | 0 | 201 | 20 | 0 |
| Alt-Ergo | 0 | 0 | 103020.926 | 44808.936 | 0 | 0 | 0 | 432 | 19 | 8 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Yices2 | 0 | 181 | 6.029 | 6.426 | 181 | 0 | 181 | 251 | 2 | 0 |
| Yices2-fixedn | 0 | 181 | 6.032 | 6.659 | 181 | 0 | 181 | 251 | 2 | 0 |
| veriT | 0 | 181 | 8.24 | 8.224 | 181 | 0 | 181 | 251 | 2 | 0 |
| MathSAT5n | 0 | 181 | 11.013 | 11.033 | 181 | 0 | 181 | 251 | 2 | 0 |
| CVC4 | 0 | 181 | 36.04 | 35.986 | 181 | 0 | 181 | 251 | 2 | 0 |
| z3n | 0 | 181 | 39.501 | 39.521 | 181 | 0 | 181 | 251 | 20 | 0 |
| SMTInterpol | 0 | 181 | 678.22 | 250.867 | 181 | 0 | 181 | 251 | 2 | 0 |
| SMTInterpol-fixedn | 0 | 181 | 695.86 | 253.685 | 181 | 0 | 181 | 251 | 2 | 0 |
| 2019-SMTInterpoln | 0 | 181 | 714.992 | 265.835 | 181 | 0 | 181 | 251 | 1 | 0 |
| Alt-Ergo | 0 | 172 | 45890.864 | 19646.332 | 172 | 0 | 172 | 260 | 19 | 8 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Yices2 | 0 | 430 | 83.923 | 84.764 | 430 | 249 | 181 | 2 | 2 | 0 | |
| Yices2-fixedn | 0 | 430 | 83.93 | 85.329 | 430 | 249 | 181 | 2 | 2 | 0 | |
| veriT | 0 | 430 | 124.263 | 124.297 | 430 | 249 | 181 | 2 | 2 | 0 | |
| MathSAT5n | 0 | 429 | 157.561 | 157.618 | 429 | 248 | 181 | 3 | 3 | 0 | |
| SMTInterpol-fixedn | 0 | 427 | 1523.489 | 645.988 | 427 | 246 | 181 | 5 | 5 | 0 | |
| SMTInterpol | 0 | 427 | 1506.36 | 648.54 | 427 | 246 | 181 | 5 | 5 | 0 | |
| 2019-SMTInterpoln | 0 | 427 | 1532.293 | 656.306 | 427 | 246 | 181 | 5 | 5 | 0 | |
| CVC4 | 0 | 426 | 243.183 | 243.072 | 426 | 245 | 181 | 6 | 6 | 0 | |
| z3n | 0 | 409 | 656.627 | 656.671 | 409 | 228 | 181 | 23 | 23 | 0 | |
| Alt-Ergo | 0 | 66 | 13248.031 | 9138.717 | 66 | 0 | 66 | 366 | 307 | 8 |
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.