The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the Equality division in the Single Query Track.
Page generated on 2022-08-10 11:17:44 +0000
Benchmarks: 4407 Time Limit: 1200 seconds Memory Limit: 60 GB
Logics:| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| cvc5 | cvc5 | cvc5 | cvc5 | Vampire |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 1689 | 3527244.846 | 3566033.81 | 1689 | 514 | 1175 | 2718 | 0 | 2718 | 0 |
| 2020-CVC4n | 0 | 1685 | 3534578.137 | 3566530.631 | 1685 | 521 | 1164 | 2722 | 0 | 2722 | 0 |
| Vampire | 0 | 1531 | 3551952.38 | 3463273.598 | 1531 | 471 | 1060 | 2876 | 0 | 2861 | 0 |
| z3-4.8.17n | 0 | 719 | 3423565.803 | 3431741.807 | 719 | 73 | 646 | 3688 | 0 | 2225 | 65 |
| veriT | 0 | 669 | 2599147.673 | 2599272.115 | 669 | 0 | 669 | 2188 | 1550 | 2050 | 75 |
| Yices2 | 0 | 345 | 3028209.76 | 3028546.539 | 345 | 39 | 306 | 2512 | 1550 | 2512 | 0 |
| smtinterpol | 0 | 296 | 4890223.459 | 4882335.731 | 296 | 7 | 289 | 4111 | 0 | 4043 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 22879.407 | 13970.289 | 0 | 0 | 0 | 4407 | 0 | 0 | 1 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 1689 | 3560323.426 | 3565900.77 | 1689 | 514 | 1175 | 2718 | 0 | 2718 | 0 |
| 2020-CVC4n | 0 | 1685 | 3560590.627 | 3566401.261 | 1685 | 521 | 1164 | 2722 | 0 | 2722 | 0 |
| Vampire | 0 | 1621 | 4294809.6 | 3419742.659 | 1621 | 487 | 1134 | 2786 | 0 | 2770 | 0 |
| z3-4.8.17n | 0 | 719 | 3424886.993 | 3431638.837 | 719 | 73 | 646 | 3688 | 0 | 2225 | 65 |
| veriT | 0 | 669 | 2599411.743 | 2599189.215 | 669 | 0 | 669 | 2188 | 1550 | 2050 | 75 |
| Yices2 | 0 | 345 | 3028480.45 | 3028452.179 | 345 | 39 | 306 | 2512 | 1550 | 2512 | 0 |
| smtinterpol | 0 | 299 | 5059928.909 | 4843219.989 | 299 | 8 | 291 | 4108 | 0 | 3929 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 22879.407 | 13970.289 | 0 | 0 | 0 | 4407 | 0 | 0 | 1 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2020-CVC4n | 0 | 521 | 358850.633 | 364051.413 | 521 | 521 | 0 | 95 | 3791 | 2722 | 0 |
| cvc5 | 0 | 514 | 374640.722 | 379756.213 | 514 | 514 | 0 | 102 | 3791 | 2718 | 0 |
| Vampire | 0 | 487 | 280621.388 | 171160.717 | 487 | 487 | 0 | 129 | 3791 | 2770 | 0 |
| z3-4.8.17n | 0 | 73 | 495639.774 | 498175.438 | 73 | 73 | 0 | 543 | 3791 | 2225 | 65 |
| Yices2 | 0 | 39 | 539261.894 | 539262.061 | 39 | 39 | 0 | 449 | 3919 | 2512 | 0 |
| smtinterpol | 0 | 8 | 716246.572 | 686609.701 | 8 | 8 | 0 | 608 | 3791 | 3929 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 3033.089 | 1778.478 | 0 | 0 | 0 | 616 | 3791 | 0 | 1 |
| veriT | 0 | 0 | 547095.18 | 546988.798 | 0 | 0 | 0 | 488 | 3919 | 2050 | 75 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 1175 | 185682.705 | 186144.558 | 1175 | 0 | 1175 | 116 | 3116 | 2718 | 0 |
| 2020-CVC4n | 0 | 1164 | 201739.994 | 202349.848 | 1164 | 0 | 1164 | 127 | 3116 | 2722 | 0 |
| Vampire | 0 | 1134 | 488562.652 | 249641.322 | 1134 | 0 | 1134 | 157 | 3116 | 2770 | 0 |
| veriT | 0 | 669 | 215249.502 | 215133.268 | 669 | 0 | 669 | 166 | 3572 | 2050 | 75 |
| z3-4.8.17n | 0 | 646 | 609890.636 | 610396.941 | 646 | 0 | 646 | 645 | 3116 | 2225 | 65 |
| Yices2 | 0 | 306 | 648418.555 | 648390.119 | 306 | 0 | 306 | 529 | 3572 | 2512 | 0 |
| smtinterpol | 0 | 291 | 1263512.012 | 1214907.348 | 291 | 0 | 291 | 1000 | 3116 | 3929 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 7552.172 | 4944.395 | 0 | 0 | 0 | 1291 | 3116 | 0 | 1 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Vampire | 0 | 1212 | 87205.783 | 79222.607 | 1212 | 371 | 841 | 3195 | 0 | 3181 | 0 |
| cvc5 | 0 | 944 | 84076.774 | 84076.829 | 944 | 13 | 931 | 3463 | 0 | 3463 | 0 |
| 2020-CVC4n | 0 | 921 | 84769.648 | 84767.013 | 921 | 11 | 910 | 3486 | 0 | 3486 | 0 |
| z3-4.8.17n | 0 | 648 | 90694.323 | 90693.2 | 648 | 68 | 580 | 3759 | 0 | 3690 | 65 |
| veriT | 0 | 622 | 54013.387 | 54002.354 | 622 | 0 | 622 | 2235 | 1550 | 2142 | 75 |
| Yices2 | 0 | 283 | 62265.264 | 62265.541 | 283 | 36 | 247 | 2574 | 1550 | 2574 | 0 |
| smtinterpol | 0 | 176 | 101968.313 | 100894.895 | 176 | 6 | 170 | 4231 | 0 | 4167 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 21703.407 | 12794.289 | 0 | 0 | 0 | 4407 | 0 | 0 | 1 |
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.