The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_FPLRA division in the Single Query Track.
Page generated on 2020-07-04 11:46:59 +0000
Benchmarks: 57 Time Limit: 1200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| COLIBRI | COLIBRI | COLIBRI | COLIBRI | COLIBRI |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| COLIBRI | 0 | 54 | 3677.786 | 3678.273 | 54 | 48 | 6 | 3 | 3 | 0 | |
| MathSAT5n | 0 | 48 | 11274.078 | 11276.181 | 48 | 45 | 3 | 9 | 9 | 0 | |
| z3n | 0 | 47 | 16959.87 | 16963.34 | 47 | 44 | 3 | 10 | 10 | 0 | |
| CVC4 | 0 | 46 | 13315.869 | 13317.881 | 46 | 42 | 4 | 11 | 11 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| COLIBRI | 0 | 54 | 3678.156 | 3678.243 | 54 | 48 | 6 | 3 | 3 | 0 | |
| MathSAT5n | 0 | 48 | 11275.648 | 11275.701 | 48 | 45 | 3 | 9 | 9 | 0 | |
| z3n | 0 | 47 | 16962.14 | 16962.85 | 47 | 44 | 3 | 10 | 10 | 0 | |
| CVC4 | 0 | 46 | 13317.379 | 13317.381 | 46 | 42 | 4 | 11 | 11 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| COLIBRI | 0 | 48 | 3655.788 | 3655.843 | 48 | 48 | 0 | 9 | 3 | 0 |
| MathSAT5n | 0 | 45 | 7674.469 | 7674.522 | 45 | 45 | 0 | 12 | 9 | 0 |
| z3n | 0 | 44 | 13362.012 | 13362.722 | 44 | 44 | 0 | 13 | 10 | 0 |
| CVC4 | 0 | 42 | 10851.916 | 10851.917 | 42 | 42 | 0 | 15 | 11 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| COLIBRI | 0 | 6 | 22.368 | 22.4 | 6 | 0 | 6 | 51 | 3 | 0 |
| CVC4 | 0 | 4 | 2465.463 | 2465.464 | 4 | 0 | 4 | 53 | 11 | 0 |
| z3n | 0 | 3 | 3600.128 | 3600.128 | 3 | 0 | 3 | 54 | 10 | 0 |
| MathSAT5n | 0 | 3 | 3601.179 | 3601.179 | 3 | 0 | 3 | 54 | 9 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| COLIBRI | 0 | 54 | 150.156 | 150.243 | 54 | 48 | 6 | 3 | 3 | 0 | |
| CVC4 | 0 | 44 | 330.92 | 330.918 | 44 | 41 | 3 | 13 | 13 | 0 | |
| MathSAT5n | 0 | 44 | 332.033 | 332.038 | 44 | 41 | 3 | 13 | 13 | 0 | |
| z3n | 0 | 19 | 1072.916 | 1072.924 | 19 | 16 | 3 | 38 | 38 | 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.