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 2021-07-18 17:29:05 +0000
Benchmarks: 4409 Time Limit: 1200 seconds Memory Limit: 60 GB
Logics:| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| Vampire | Vampire | Vampire | 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 | 1675 | 3534021.964 | 3564804.099 | 1675 | 507 | 1168 | 2734 | 0 | 2734 | 0 |
| Vampire | 0 | 1503 | 3581898.115 | 3511587.015 | 1503 | 451 | 1052 | 2906 | 0 | 2905 | 0 |
| 2020-Vampiren | 0 | 1493 | 3566620.258 | 3494353.262 | 1493 | 448 | 1045 | 2916 | 0 | 2891 | 0 |
| Vampire - fixedn | 0 | 1476 | 3585368.269 | 3513541.563 | 1476 | 443 | 1033 | 2933 | 0 | 2906 | 0 |
| cvc5 | 0 | 1382 | 1810657.266 | 3768038.808 | 1382 | 236 | 1146 | 3027 | 0 | 3027 | 0 |
| iProver - fixed2n | 0 | 1012 | 4158556.093 | 4092508.372 | 1012 | 215 | 797 | 3397 | 0 | 3170 | 221 |
| iProver - fixedn | 0 | 996 | 4166641.663 | 4106742.199 | 996 | 213 | 783 | 3413 | 0 | 3154 | 250 |
| veriT | 0 | 693 | 2573610.821 | 2573921.446 | 693 | 0 | 693 | 2164 | 1552 | 2044 | 62 |
| z3n | 0 | 462 | 2178898.243 | 2180506.489 | 462 | 58 | 404 | 2395 | 1552 | 1390 | 36 |
| Yices2 | 0 | 349 | 3027820.971 | 3028157.786 | 349 | 39 | 310 | 2508 | 1552 | 2508 | 0 |
| SMTInterpol | 0 | 221 | 3168208.061 | 3162365.695 | 221 | 9 | 212 | 2636 | 1552 | 2617 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 15142.87 | 8638.235 | 0 | 0 | 0 | 2857 | 1552 | 0 | 0 |
| iProver | 12 | 1086 | 4053565.089 | 3985959.191 | 1086 | 214 | 872 | 3323 | 0 | 3067 | 235 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2020-CVC4n | 0 | 1675 | 3559523.194 | 3564676.979 | 1675 | 507 | 1168 | 2734 | 0 | 2734 | 0 |
| Vampire | 0 | 1572 | 3697541.225 | 3475934.333 | 1572 | 455 | 1117 | 2837 | 0 | 2835 | 0 |
| 2020-Vampiren | 0 | 1567 | 3694311.798 | 3457200.384 | 1567 | 472 | 1095 | 2842 | 0 | 2811 | 0 |
| Vampire - fixedn | 0 | 1547 | 3695052.419 | 3474601.191 | 1547 | 447 | 1100 | 2862 | 0 | 2832 | 0 |
| cvc5 | 0 | 1382 | 3765383.252 | 3767884.958 | 1382 | 236 | 1146 | 3027 | 0 | 3027 | 0 |
| iProver - fixed2n | 0 | 1054 | 4212963.403 | 4068213.031 | 1054 | 219 | 835 | 3355 | 0 | 3126 | 221 |
| iProver - fixedn | 0 | 1040 | 4234709.203 | 4084357.701 | 1040 | 216 | 824 | 3369 | 0 | 3110 | 250 |
| veriT | 0 | 693 | 2573855.701 | 2573844.546 | 693 | 0 | 693 | 2164 | 1552 | 2044 | 62 |
| z3n | 0 | 462 | 2179799.123 | 2180444.109 | 462 | 58 | 404 | 2395 | 1552 | 1390 | 36 |
| Yices2 | 0 | 349 | 3028078.401 | 3028073.076 | 349 | 39 | 310 | 2508 | 1552 | 2508 | 0 |
| SMTInterpol | 0 | 227 | 3330026.391 | 3138872.245 | 227 | 9 | 218 | 2630 | 1552 | 2525 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 15142.87 | 8638.235 | 0 | 0 | 0 | 2857 | 1552 | 0 | 0 |
| iProver | 13 | 1124 | 4102600.259 | 3961871.716 | 1124 | 217 | 907 | 3285 | 0 | 3026 | 235 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2020-CVC4n | 0 | 507 | 353049.369 | 357919.386 | 507 | 507 | 0 | 96 | 3806 | 2734 | 0 |
| 2020-Vampiren | 0 | 472 | 270462.648 | 181731.649 | 472 | 472 | 0 | 131 | 3806 | 2811 | 0 |
| Vampire | 0 | 455 | 215471.936 | 186423.238 | 455 | 455 | 0 | 148 | 3806 | 2835 | 0 |
| Vampire - fixedn | 0 | 447 | 214802.265 | 187221.228 | 447 | 447 | 0 | 156 | 3806 | 2832 | 0 |
| cvc5 | 0 | 236 | 547212.017 | 549612.395 | 236 | 236 | 0 | 367 | 3806 | 3027 | 0 |
| iProver - fixed2n | 0 | 219 | 470166.879 | 457883.862 | 219 | 219 | 0 | 384 | 3806 | 3126 | 221 |
| iProver | 0 | 217 | 453492.948 | 442880.718 | 217 | 217 | 0 | 386 | 3806 | 3026 | 235 |
| iProver - fixedn | 0 | 216 | 470261.272 | 459690.661 | 216 | 216 | 0 | 387 | 3806 | 3110 | 250 |
| z3n | 0 | 58 | 362832.59 | 363361.109 | 58 | 58 | 0 | 411 | 3940 | 1390 | 36 |
| Yices2 | 0 | 39 | 516147.715 | 516147.864 | 39 | 39 | 0 | 430 | 3940 | 2508 | 0 |
| SMTInterpol | 0 | 9 | 568504.578 | 527817.881 | 9 | 9 | 0 | 460 | 3940 | 2525 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 2399.753 | 1394.121 | 0 | 0 | 0 | 469 | 3940 | 0 | 0 |
| veriT | 0 | 0 | 521861.826 | 521856.521 | 0 | 0 | 0 | 469 | 3940 | 2044 | 62 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2020-CVC4n | 0 | 1168 | 273673.825 | 273957.593 | 1168 | 0 | 1168 | 194 | 3047 | 2734 | 0 |
| cvc5 | 0 | 1146 | 285371.235 | 285472.563 | 1146 | 0 | 1146 | 216 | 3047 | 3027 | 0 |
| Vampire | 0 | 1117 | 542062.928 | 356713.175 | 1117 | 0 | 1117 | 245 | 3047 | 2835 | 0 |
| Vampire - fixedn | 0 | 1100 | 543850.113 | 354606.283 | 1100 | 0 | 1100 | 262 | 3047 | 2832 | 0 |
| 2020-Vampiren | 0 | 1095 | 491049.149 | 342668.735 | 1095 | 0 | 1095 | 267 | 3047 | 2811 | 0 |
| iProver - fixed2n | 0 | 835 | 809964.744 | 678147.631 | 835 | 0 | 835 | 527 | 3047 | 3126 | 221 |
| iProver - fixedn | 0 | 824 | 831647.931 | 691867.04 | 824 | 0 | 824 | 538 | 3047 | 3110 | 250 |
| veriT | 0 | 693 | 281078.045 | 281071.766 | 693 | 0 | 693 | 219 | 3497 | 2044 | 62 |
| z3n | 0 | 404 | 493182.144 | 493202.608 | 404 | 0 | 404 | 508 | 3497 | 1390 | 36 |
| Yices2 | 0 | 310 | 740730.686 | 740725.213 | 310 | 0 | 310 | 602 | 3497 | 2508 | 0 |
| SMTInterpol | 0 | 218 | 887807.013 | 854480.675 | 218 | 0 | 218 | 694 | 3497 | 2525 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 4866.299 | 2774.282 | 0 | 0 | 0 | 912 | 3497 | 0 | 0 |
| iProver | 13 | 907 | 716445.524 | 589343.799 | 907 | 0 | 907 | 455 | 3047 | 3026 | 235 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2020-Vampiren | 0 | 1211 | 86358.004 | 78990.115 | 1211 | 367 | 844 | 3198 | 0 | 3179 | 0 |
| Vampire | 0 | 1206 | 87683.444 | 79750.348 | 1206 | 364 | 842 | 3203 | 0 | 3203 | 0 |
| Vampire - fixedn | 0 | 1184 | 87676.701 | 79802.396 | 1184 | 356 | 828 | 3225 | 0 | 3206 | 0 |
| cvc5 | 0 | 973 | 83416.912 | 83382.51 | 973 | 14 | 959 | 3436 | 0 | 3436 | 0 |
| 2020-CVC4n | 0 | 950 | 84075.274 | 84044.294 | 950 | 13 | 937 | 3459 | 0 | 3459 | 0 |
| iProver - fixed2n | 0 | 829 | 98719.369 | 89353.068 | 829 | 196 | 633 | 3580 | 0 | 3353 | 221 |
| iProver - fixedn | 0 | 818 | 98381.497 | 89464.391 | 818 | 195 | 623 | 3591 | 0 | 3335 | 250 |
| veriT | 0 | 650 | 53301.039 | 53293.096 | 650 | 0 | 650 | 2207 | 1552 | 2128 | 62 |
| z3n | 0 | 425 | 58880.078 | 58877.524 | 425 | 54 | 371 | 2432 | 1552 | 2396 | 36 |
| Yices2 | 0 | 288 | 62205.668 | 62198.453 | 288 | 37 | 251 | 2569 | 1552 | 2569 | 0 |
| SMTInterpol | 0 | 142 | 66274.158 | 65516.037 | 142 | 8 | 134 | 2715 | 1552 | 2702 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 15142.87 | 8638.235 | 0 | 0 | 0 | 2857 | 1552 | 0 | 0 |
| iProver | 4 | 889 | 98817.996 | 88244.687 | 889 | 196 | 693 | 3520 | 0 | 3275 | 235 |
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.