The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the Equality+NonLinearArith division in the Single Query Track.
Page generated on 2021-07-18 17:29:05 +0000
Benchmarks: 7816 Time Limit: 1200 seconds Memory Limit: 60 GB
Logics:| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| Vampire | iProver | UltimateEliminator+MathSAT | cvc5 | Vampire |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2020-CVC4n | 0 | 4593 | 3615878.594 | 3719904.921 | 4593 | 715 | 3878 | 3210 | 13 | 2976 | 0 |
| cvc5 - fixedn | 0 | 4586 | 1678708.602 | 3725455.291 | 4586 | 699 | 3887 | 3230 | 0 | 3055 | 0 |
| Vampire | 0 | 3455 | 5630077.959 | 5272572.533 | 3455 | 0 | 3455 | 4348 | 13 | 4285 | 0 |
| Vampire - fixedn | 0 | 3421 | 5606296.345 | 5253466.282 | 3421 | 0 | 3421 | 4382 | 13 | 4270 | 0 |
| 2020-Vampiren | 0 | 3171 | 5815285.979 | 5507208.325 | 3171 | 0 | 3171 | 4632 | 13 | 4493 | 0 |
| z3n | 0 | 2796 | 2853768.586 | 2856426.796 | 2796 | 639 | 2157 | 3785 | 1235 | 1947 | 10 |
| iProver | 0 | 1748 | 6663277.165 | 6568574.233 | 1748 | 0 | 1748 | 5452 | 616 | 5413 | 33 |
| UltimateEliminator+MathSAT | 0 | 521 | 848773.392 | 834372.034 | 521 | 334 | 187 | 6060 | 1235 | 657 | 0 |
| SMTInterpol | 0 | 176 | 16507.651 | 14720.999 | 176 | 83 | 93 | 6102 | 1538 | 10 | 0 |
| cvc5 | 5 | 4593 | 1676347.527 | 3710207.094 | 4593 | 702 | 3891 | 3223 | 0 | 3040 | 0 |
| 2019-Par4n | 7 | 3819 | 3541076.013 | 3423877.126 | 3819 | 733 | 3086 | 2759 | 1238 | 2751 | 1 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2020-CVC4n | 0 | 4593 | 3715235.603 | 3719727.331 | 4593 | 715 | 3878 | 3210 | 13 | 2976 | 0 |
| cvc5 - fixedn | 0 | 4586 | 3724178.364 | 3725278.931 | 4586 | 699 | 3887 | 3230 | 0 | 3055 | 0 |
| Vampire - fixedn | 0 | 3499 | 5865235.555 | 5129849.299 | 3499 | 0 | 3499 | 4304 | 13 | 4085 | 0 |
| 2020-Vampiren | 0 | 3443 | 6495194.049 | 5341645.404 | 3443 | 0 | 3443 | 4360 | 13 | 4142 | 0 |
| z3n | 0 | 2796 | 2854439.116 | 2856348.646 | 2796 | 639 | 2157 | 3785 | 1235 | 1947 | 10 |
| iProver | 0 | 1957 | 7036594.175 | 6476461.5 | 1957 | 0 | 1957 | 5243 | 616 | 5204 | 33 |
| UltimateEliminator+MathSAT | 0 | 521 | 848773.392 | 834372.034 | 521 | 334 | 187 | 6060 | 1235 | 657 | 0 |
| SMTInterpol | 0 | 176 | 18263.131 | 14391.29 | 176 | 83 | 93 | 6102 | 1538 | 9 | 0 |
| cvc5 | 5 | 4593 | 3709218.063 | 3710038.994 | 4593 | 702 | 3891 | 3223 | 0 | 3040 | 0 |
| 2019-Par4n | 7 | 3839 | 3549594.293 | 3416508.279 | 3839 | 737 | 3102 | 2739 | 1238 | 2731 | 1 |
| Vampire | 26 | 3556 | 5903838.529 | 5119602.87 | 3556 | 0 | 3556 | 4247 | 13 | 4054 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2020-CVC4n | 0 | 715 | 49494.682 | 49740.994 | 715 | 715 | 0 | 36 | 7065 | 2976 | 0 |
| cvc5 - fixedn | 0 | 699 | 58841.71 | 59019.981 | 699 | 699 | 0 | 52 | 7065 | 3055 | 0 |
| z3n | 0 | 639 | 102207.513 | 102206.812 | 639 | 639 | 0 | 112 | 7065 | 1947 | 10 |
| UltimateEliminator+MathSAT | 0 | 334 | 445329.539 | 444413.325 | 334 | 334 | 0 | 417 | 7065 | 657 | 0 |
| SMTInterpol | 0 | 83 | 9957.044 | 9873.081 | 83 | 83 | 0 | 665 | 7068 | 9 | 0 |
| Vampire | 0 | 0 | 884400.73 | 869983.16 | 0 | 0 | 0 | 751 | 7065 | 4054 | 0 |
| iProver | 0 | 0 | 890456.643 | 890425.759 | 0 | 0 | 0 | 748 | 7068 | 5204 | 33 |
| Vampire - fixedn | 0 | 0 | 926423.68 | 901155.65 | 0 | 0 | 0 | 751 | 7065 | 4085 | 0 |
| 2020-Vampiren | 0 | 0 | 915600.95 | 901181.39 | 0 | 0 | 0 | 751 | 7065 | 4142 | 0 |
| cvc5 | 5 | 702 | 57169.339 | 57254.431 | 702 | 702 | 0 | 49 | 7065 | 3040 | 0 |
| 2019-Par4n | 7 | 737 | 49768.518 | 33538.206 | 737 | 737 | 0 | 14 | 7065 | 2731 | 1 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 3891 | 732382.543 | 733102.238 | 3891 | 0 | 3891 | 700 | 3225 | 3040 | 0 |
| cvc5 - fixedn | 0 | 3887 | 745593.718 | 746510.266 | 3887 | 0 | 3887 | 704 | 3225 | 3055 | 0 |
| 2020-CVC4n | 0 | 3878 | 770113.794 | 774359.562 | 3878 | 0 | 3878 | 706 | 3232 | 2976 | 0 |
| Vampire - fixedn | 0 | 3499 | 1927410.445 | 1267284.589 | 3499 | 0 | 3499 | 1085 | 3232 | 4085 | 0 |
| 2020-Vampiren | 0 | 3443 | 2528363.749 | 1504001.795 | 3443 | 0 | 3443 | 1141 | 3232 | 4142 | 0 |
| 2019-Par4n | 0 | 3102 | 607825.774 | 490970.073 | 3102 | 0 | 3102 | 315 | 4399 | 2731 | 1 |
| z3n | 0 | 2157 | 881127.624 | 881010.832 | 2157 | 0 | 2157 | 1263 | 4396 | 1947 | 10 |
| iProver | 0 | 1957 | 3504937.532 | 2944835.741 | 1957 | 0 | 1957 | 2294 | 3565 | 5204 | 33 |
| UltimateEliminator+MathSAT | 0 | 187 | 346285.374 | 337576.086 | 187 | 0 | 187 | 3233 | 4396 | 657 | 0 |
| SMTInterpol | 0 | 93 | 6000.115 | 2548.829 | 93 | 0 | 93 | 3261 | 4462 | 9 | 0 |
| Vampire | 26 | 3556 | 2018235.679 | 1288057.52 | 3556 | 0 | 3556 | 1028 | 3232 | 4054 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 - fixedn | 0 | 4127 | 89263.882 | 89204.076 | 4127 | 678 | 3449 | 3689 | 0 | 3556 | 0 |
| 2020-CVC4n | 0 | 3909 | 93393.206 | 93308.278 | 3909 | 622 | 3287 | 3894 | 13 | 3749 | 0 |
| z3n | 0 | 2649 | 88272.747 | 88189.244 | 2649 | 612 | 2037 | 3932 | 1235 | 3403 | 10 |
| Vampire | 0 | 2292 | 159717.871 | 139756.935 | 2292 | 0 | 2292 | 5511 | 13 | 5511 | 0 |
| Vampire - fixedn | 0 | 2238 | 159125.997 | 140003.683 | 2238 | 0 | 2238 | 5565 | 13 | 5535 | 0 |
| 2020-Vampiren | 0 | 2061 | 153605.265 | 141983.044 | 2061 | 0 | 2061 | 5742 | 13 | 5707 | 0 |
| iProver | 0 | 1466 | 157828.176 | 143406.233 | 1466 | 0 | 1466 | 5734 | 616 | 5695 | 33 |
| UltimateEliminator+MathSAT | 0 | 453 | 49602.671 | 37281.247 | 453 | 271 | 182 | 6128 | 1235 | 791 | 0 |
| SMTInterpol | 0 | 175 | 4733.862 | 2952.455 | 175 | 82 | 93 | 6103 | 1538 | 11 | 0 |
| cvc5 | 2 | 4131 | 89132.865 | 89077.08 | 4131 | 681 | 3450 | 3685 | 0 | 3548 | 0 |
| 2019-Par4n | 7 | 3240 | 86529.668 | 83543.725 | 3240 | 678 | 2562 | 3338 | 1238 | 3330 | 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.