The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the AUFBV logic in the Single Query Track.
Page generated on 2021-07-18 17:29:04 +0000
Benchmarks: 761 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 |
|---|---|---|---|---|---|---|---|---|---|---|
| z3n | 0 | 163 | 659907.948 | 661635.736 | 163 | 50 | 113 | 598 | 514 | 10 |
| cvc5 - fixedn | 0 | 152 | 344529.509 | 687872.038 | 152 | 9 | 143 | 609 | 527 | 0 |
| cvc5 | 0 | 150 | 356766.273 | 688948.453 | 150 | 10 | 140 | 611 | 529 | 0 |
| UltimateEliminator+MathSAT | 0 | 4 | 867155.959 | 866404.329 | 4 | 0 | 4 | 757 | 716 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| z3n | 0 | 163 | 661100.848 | 661614.196 | 163 | 50 | 113 | 598 | 514 | 10 |
| cvc5 - fixedn | 0 | 152 | 685886.521 | 687841.418 | 152 | 9 | 143 | 609 | 527 | 0 |
| cvc5 | 0 | 150 | 687143.12 | 688916.693 | 150 | 10 | 140 | 611 | 529 | 0 |
| UltimateEliminator+MathSAT | 0 | 4 | 867155.959 | 866404.329 | 4 | 0 | 4 | 757 | 716 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| z3n | 0 | 50 | 4249.581 | 4249.944 | 50 | 50 | 0 | 4 | 707 | 514 | 10 |
| cvc5 | 0 | 10 | 29294.402 | 29779.409 | 10 | 10 | 0 | 44 | 707 | 529 | 0 |
| cvc5 - fixedn | 0 | 9 | 30957.038 | 31403.688 | 9 | 9 | 0 | 45 | 707 | 527 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 56801.167 | 56700.994 | 0 | 0 | 0 | 54 | 707 | 716 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 - fixedn | 0 | 143 | 64278.18 | 64899.676 | 143 | 0 | 143 | 46 | 572 | 527 | 0 |
| cvc5 | 0 | 140 | 65051.46 | 65504.783 | 140 | 0 | 140 | 49 | 572 | 529 | 0 |
| z3n | 0 | 113 | 95775.657 | 95740.549 | 113 | 0 | 113 | 76 | 572 | 514 | 10 |
| UltimateEliminator+MathSAT | 0 | 4 | 203288.763 | 202878.94 | 4 | 0 | 4 | 185 | 572 | 716 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 - fixedn | 0 | 118 | 15719.512 | 15721.18 | 118 | 1 | 117 | 643 | 630 | 0 |
| cvc5 | 0 | 118 | 15725.761 | 15726.159 | 118 | 1 | 117 | 643 | 630 | 0 |
| z3n | 0 | 108 | 15804.417 | 15803.42 | 108 | 38 | 70 | 653 | 623 | 10 |
| UltimateEliminator+MathSAT | 0 | 3 | 18151.4 | 17970.888 | 3 | 0 | 3 | 758 | 739 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.