The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_S division in the Single Query Track.
Page generated on 2020-07-04 11:46:59 +0000
Benchmarks: 925 Time Limit: 1200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| CVC4 | CVC4 | CVC4 | CVC4 | CVC4 |
Note: the division has disagreements
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| CVC4 | 0 | 922 | 6697.245 | 6709.055 | 922 | 441 | 481 | 3 | 3 | 0 | |
| Z3str4 | 0 | 862 | 76283.199 | 76226.745 | 862 | 383 | 479 | 63 | 63 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| CVC4 | 0 | 922 | 6697.775 | 6708.815 | 922 | 441 | 481 | 3 | 3 | 0 | |
| Z3str4 | 0 | 862 | 76291.869 | 76224.525 | 862 | 383 | 479 | 63 | 63 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| CVC4 | 0 | 441 | 5488.28 | 5499.207 | 441 | 441 | 0 | 484 | 3 | 0 |
| Z3str4 | 0 | 383 | 72676.366 | 72612.351 | 383 | 383 | 0 | 542 | 63 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| CVC4 | 0 | 481 | 9.495 | 9.608 | 481 | 0 | 481 | 444 | 3 | 0 |
| Z3str4 | 0 | 479 | 2415.503 | 2412.174 | 479 | 0 | 479 | 446 | 63 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| CVC4 | 0 | 905 | 985.719 | 969.158 | 905 | 424 | 481 | 20 | 20 | 0 | |
| Z3str4 | 0 | 858 | 2022.177 | 1957.61 | 858 | 379 | 479 | 67 | 67 | 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.