The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the BVFP division in the Single Query Track.
Page generated on 2019-07-23 17:56:09 +0000
Benchmarks: 24 Time Limit: 2400 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| CVC4 | CVC4 | CVC4 | CVC4 | CVC4 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Z3n | 0 | 24 | 1416.267 | 1423.638 | 24 | 20 | 4 | 0 | 0 | 0 | |
| CVC4 | 0 | 8 | 38402.852 | 38405.981 | 8 | 4 | 4 | 16 | 16 | 0 | |
| 2018-CVC4n | 0 | 8 | 38403.088 | 38406.407 | 8 | 4 | 4 | 16 | 16 | 0 | |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 1 | 81.649 | 57.463 | 1 | 1 | 0 | 23 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Z3n | 0 | 24 | 1416.267 | 1423.638 | 24 | 20 | 4 | 0 | 0 | 0 | |
| CVC4 | 0 | 8 | 38405.382 | 38405.381 | 8 | 4 | 4 | 16 | 16 | 0 | |
| 2018-CVC4n | 0 | 8 | 38406.008 | 38406.007 | 8 | 4 | 4 | 16 | 16 | 0 | |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 1 | 81.649 | 57.463 | 1 | 1 | 0 | 23 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Z3n | 0 | 20 | 1211.717 | 1219.047 | 20 | 20 | 0 | 4 | 0 | 0 |
| CVC4 | 0 | 4 | 38402.871 | 38402.871 | 4 | 4 | 0 | 20 | 16 | 0 |
| 2018-CVC4n | 0 | 4 | 38403.227 | 38403.226 | 4 | 4 | 0 | 20 | 16 | 0 |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 1 | 68.185 | 47.71 | 1 | 1 | 0 | 23 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| CVC4 | 0 | 4 | 2.511 | 2.51 | 4 | 0 | 4 | 20 | 16 | 0 |
| 2018-CVC4n | 0 | 4 | 2.78 | 2.781 | 4 | 0 | 4 | 20 | 16 | 0 |
| Z3n | 0 | 4 | 204.55 | 204.591 | 4 | 0 | 4 | 20 | 0 | 0 |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 0 | 13.464 | 9.753 | 0 | 0 | 0 | 24 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Z3n | 0 | 12 | 337.37 | 337.372 | 12 | 9 | 3 | 12 | 12 | 0 | |
| CVC4 | 0 | 8 | 389.382 | 389.381 | 8 | 4 | 4 | 16 | 16 | 0 | |
| 2018-CVC4n | 0 | 8 | 390.008 | 390.007 | 8 | 4 | 4 | 16 | 16 | 0 | |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 1 | 81.649 | 57.463 | 1 | 1 | 0 | 23 | 0 | 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.