The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the UFNIA logic in the Single Query Track.
Page generated on 2022-08-10 11:17:45 +0000
Benchmarks: 6278 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 |
|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 3525 | 3341707.262 | 3430606.874 | 3525 | 693 | 2832 | 2753 | 2747 | 0 |
| 2020-CVC4n | 0 | 3434 | 3355504.528 | 3460402.414 | 3434 | 691 | 2743 | 2844 | 2759 | 0 |
| z3-4.8.17n | 0 | 2766 | 2835397.781 | 2836671.512 | 2766 | 608 | 2158 | 3512 | 2037 | 10 |
| Vampire | 0 | 2378 | 4938743.177 | 4706083.636 | 2378 | 0 | 2378 | 3900 | 3855 | 1 |
| UltimateEliminator+MathSAT | 0 | 568 | 634193.401 | 621320.004 | 568 | 397 | 171 | 5710 | 483 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 3526 | 3428154.429 | 3430424.894 | 3526 | 693 | 2833 | 2752 | 2746 | 0 |
| 2020-CVC4n | 0 | 3434 | 3454973.444 | 3460234.164 | 3434 | 691 | 2743 | 2844 | 2759 | 0 |
| z3-4.8.17n | 0 | 2766 | 2836446.771 | 2836591.882 | 2766 | 608 | 2158 | 3512 | 2037 | 10 |
| Vampire | 0 | 2651 | 5725630.607 | 4517275.462 | 2651 | 0 | 2651 | 3627 | 3579 | 1 |
| UltimateEliminator+MathSAT | 0 | 568 | 634225.641 | 621264.864 | 568 | 397 | 171 | 5710 | 480 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 693 | 56190.574 | 56291.513 | 693 | 693 | 0 | 28 | 5557 | 2746 | 0 |
| 2020-CVC4n | 0 | 691 | 44452.24 | 44773.119 | 691 | 691 | 0 | 30 | 5557 | 2759 | 0 |
| z3-4.8.17n | 0 | 608 | 102094.441 | 102083.864 | 608 | 608 | 0 | 113 | 5557 | 2037 | 10 |
| UltimateEliminator+MathSAT | 0 | 397 | 328416.958 | 327469.983 | 397 | 397 | 0 | 324 | 5557 | 480 | 0 |
| Vampire | 0 | 0 | 969604.87 | 865099.43 | 0 | 0 | 0 | 721 | 5557 | 3579 | 1 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 2833 | 537563.855 | 539733.381 | 2833 | 0 | 2833 | 362 | 3083 | 2746 | 0 |
| 2020-CVC4n | 0 | 2743 | 646931.645 | 651799.362 | 2743 | 0 | 2743 | 452 | 3083 | 2759 | 0 |
| Vampire | 0 | 2651 | 1575137.807 | 818905.234 | 2651 | 0 | 2651 | 544 | 3083 | 3579 | 1 |
| z3-4.8.17n | 0 | 2158 | 754023.509 | 754005.56 | 2158 | 0 | 2158 | 1037 | 3083 | 2037 | 10 |
| UltimateEliminator+MathSAT | 0 | 171 | 182141.757 | 174525.609 | 171 | 0 | 171 | 3024 | 3083 | 480 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 2807 | 86240.987 | 86204.648 | 2807 | 625 | 2182 | 3471 | 3465 | 0 |
| 2020-CVC4n | 0 | 2775 | 86675.834 | 86655.647 | 2775 | 601 | 2174 | 3503 | 3493 | 0 |
| z3-4.8.17n | 0 | 2612 | 83880.454 | 83776.656 | 2612 | 586 | 2026 | 3666 | 3251 | 10 |
| Vampire | 0 | 1516 | 125005.827 | 116799.568 | 1516 | 0 | 1516 | 4762 | 4738 | 1 |
| UltimateEliminator+MathSAT | 0 | 534 | 43761.57 | 32008.526 | 534 | 364 | 170 | 5744 | 576 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.